search

lip6 / ITSTools

A multi-formalism, multi-solution model-checker centered on the language GAL
GNU General Public License v3.0
21 stars 10 forks source link

limited quantifiers in properties #5

Open yanntm opened 7 years ago

yanntm commented 7 years ago

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.

yanntm commented 6 years ago

smt aligned "forall" and "exists" keywords for these notions seem good.

yanntm commented 6 years ago

(forall ($x : dom) : var[$x] == 0 || (exists ($y : dom) : $x!=$y && var[$y]==$x))

yanntm commented 6 years ago

commit was target bad issue number