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" |
||
|---|---|---|
| .. | ||
| analysis | ||
| ctrln | ||
| main | ||
| sigali | ||
| transformations | ||
| _tags | ||
| minils.ml | ||
| mls_compare.ml | ||
| mls_mapfold.ml | ||
| mls_printer.ml | ||
| mls_utils.ml | ||