Hardware#495
Conversation
AdamZsofi
left a comment
AdamZsofi
left a comment
There was a problem hiding this comment.
Overall the code looks nice - I can not comment on algorithmic correctness.
My main concern is lack of docs, because this is the time to document your understanding of these algorithms and the architecture you built around it.
Ideas for docs:
- Document in local markdowns, e.g. a markdown in the frame directory, but a few class level javadoc comments wouldn't hurt either,
- link to the papers about the original algorithms,
- link to your thesis/tdk about the specific works.
- Explain what is what in the doc on a high level,
- as you will see, I made some comments about not understanding some names, that's kind of the "architecture level" - what the building blocks are and how are, they connected,
- explain the optimizations and add any conventions / rule of thumbs you know about - what you would (not) use in different situations; if there are any constraints (don't use this with that, etc.), write down those as well.
If I saw correctly, the algorithms so far are only connected to the (x)sts clis. I would really like to have it for xcfas, but that can be a separate PR. If you need help with it, just find me, please.
(I'll check why the CI is failing in more detail in a sec, but for formatting, run ./gradlew spotlessApply.)
| import java.util.Set; | ||
| package hu.bme.mit.theta.analysis.algorithm.frame.base; | ||
|
|
||
| public class ProofObligation { |
There was a problem hiding this comment.
Why proof obligation , how is it more than a proof? (If it's "just" a proof, it could be connected to the Proof interface, etc.)
There was a problem hiding this comment.
This is called a proof obligation in IC3 literature, so I think we should stay consistent with that.
It's not connected to proofs in any way, it means a "state from the overapproximation, about which we have to prove if they are spurious or not"
| import java.util.HashSet; | ||
| import java.util.Set; | ||
|
|
||
| public class Node { |
There was a problem hiding this comment.
Maybe call this something more specific, like FrameNode?
|
|
||
| public class Frame { | ||
| private final Frame parent; | ||
| public class OverFrame { |
There was a problem hiding this comment.
Over, as in over approximation or is this a more CAR specific concept?
|
CI: I can see that you made version bumps, etc. 2 weeks ago - maybe we can just recheck and work out after changes were made and CI was re-executed, if the CI checks should be successful or not. |
|
@dantpu any open questions (i.e., are you blocked waiting for us) or is this just waiting for you to have time? :) |
There was a problem hiding this comment.
I think the PR is almost ready to be merged, only smaller questions remain (including the questions by @AdamZsofi ) as well as fixing the failing CI checks.
Would CAR and CARCEGAR also work on XCFA and STS in its current form? If yes, then I think it should also be introduced to XCFA and XSTS CLI.
| import java.util.Set; | ||
| import java.util.stream.Collectors; | ||
|
|
||
| public final class Cube { |
There was a problem hiding this comment.
Please add a short javadoc comment that explains what a cube is
| import java.util.Set; | ||
| import java.util.stream.Collectors; | ||
|
|
||
| public final class Clause { |
There was a problem hiding this comment.
Please add a short javadoc comment that explains what a clause is
There was a problem hiding this comment.
Does the current CarChecker work properly, or is this still needed?
3 participants
Refactored IC3Checker and added CarChecker and CarCegarChecker.
CarCegarChecker still depends on an earlier version of CarChecker. This will be fixed in the future.