Repository navigation
limited quantifiers in properties #5
Description
there is no real reason we could not use the parameters in the property specification, we having some kind of AndAll/OrAll (or forAll, forAny) quantifiers + bool expr over parameters would be nice
e.g. viking
typedef vik_t = 0..3;
property safe [reachable] : win==1 && forAll($vik : vik) { Soldier_state[$vik]==2 };
syntax to be discussed, but that forall is a boolean Expr.
Activity
yanntm commentedon Feb 9, 2018
smt aligned "forall" and "exists" keywords for these notions seem good.
yanntm commentedon Feb 9, 2018
(forall ($x : dom) : var[$x] == 0 || (exists ($y : dom) : $x!=$y && var[$y]==$x))yanntm commentedon Jun 24, 2018
commit was target bad issue number
Merge pull request #5 from lip6/master
Merge pull request #5 from lip6/dependabot/github_actions/actions/set…