3dfbeffeb6
Contracts can now comprise a list of objectives (in any order). One objective can be (e being a Boolean heptagon expression) : - invariance, with the syntax "enforce e" - reachability, "reachable e" - attractivity, "attractive e" |
||
---|---|---|
.. | ||
clocking.ml | ||
interference.ml | ||
level_clock.ml |