Yann Thierry-Mieg

hi, so you do need to do it "manually", the easiest approach is probably to create a labeled transition "invar" with an `if (!B(X)) abort;` then call it with `self."invar"`...

What would that look like syntactically, I'm not sure. Perhaps ``` // gal and composite definitions main Toto / [invariant] a

ok, interesting use case. I need some more time to think about how it could be done. Defining invariants at component level is nicer I guess than only for main....

ok, yes we could probably add that feature. So I add one optional "invariant" declaration per gal/composite declaration, basically we enforce it as a condition on the initial state (raise...

Just to say I still have this in the pipe, but I've been pretty busy. Did you manage to go around it manually (by adding the tests yourself) and did...

no, urgent channels, as well as several other features (e.g. global clocks) are not in there. But I can add them in if you need them.

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

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

commit was target bad issue number