| Commit message (Collapse) | Author | Age |
| |
|
|
|
|
| |
codeexpr is made.
|
| |
|
|
|
|
|
| |
cleaned up the generation of mover checks (based on example from Chris)
added two examples from Chris to regressions
|
|
|
|
| |
refinement checking with all global variables
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
added annotation on an atomic action about the phases in which it exists
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
| |
ported all the examples
added the QED examples to runtest.bat
|
|
|
|
| |
added LookUp to multiset.bpl
|
|
|
|
| |
added "cnst" feature
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
optimized the FailurePreservationChecker to eliminate some quantifiers
|
|
|
|
|
|
| |
transition relation
changed the type checking of left movers; they are required to be non-blocking now
|
| |
|
| |
|
| |
|
|
|
|
| |
other bug fixes in QED stuff
|
| |
|
| |
|
| |
|
| |
|
|
|