sally
sally copied to clipboard
SRI-CSL
A model checker for infinite-state systems.
Does Sally support exists and forall operators? I tried a simple example but it throws parser error at the location of "exists". ``` (define-state-type my_state ((x Real) (y Real)) )...
In the following model, `sally` successfully validates `ok1`, but returns `unknown` on `ok2`, which is the same as `ok1` but `or`-ed with another boolean value. ``` (define-state-type S ( (ok1...
It looks like the `mcmt` input parser is missing an entry for a `mod` operation at the moment. Could we add it? A quick grep through the source code shows...
The model below illustrates an example where `sally` (with engine `kind`) can solve the problem immediately, but if we add `--yices2-mcsat` Sally fails to find a solution (or is much...
Is there a function to perform euclidian integer division (like `div` from SMTLIB) in Sally? I can't seem to find one. It looks like the `/` operator works on integers,...
Consider the following model: `x` is the "state" proper, and `ok` is a bool that keeps track of some property of the state (in this case that `0
Hello, Consider the following trivial transition system: ``` (define-state-type S () ()) (define-transition-system TS S (= 1 2) (= 1 1)) (query TS (= 1 1)) ``` When I run...
For software verification and the SyGuS competition. Need to finish integration of Yices2 generalization for integers.
I am thankful to the contributors for the wonderful work they have done. I have found the format useful (and simple) to extend SMT2 format to state transition systems (finite...
