15238eaf8b
- contrenum.ept includes contracts and controllable variable: moved to sdc test directory - lnum_simple.ept: added "enforce true" contract (at least one objective in the syntax) - script compile_sdc_run: heptc options to point to local Heptagon library
15 lines
No EOL
176 B
Text
15 lines
No EOL
176 B
Text
type mode = Idle | Active
|
|
|
|
node f(x:bool) returns (y:bool)
|
|
|
|
contract
|
|
enforce (not y)
|
|
with (c:mode)
|
|
|
|
let
|
|
switch c
|
|
| Idle do y = false
|
|
| Active do y = true
|
|
end
|
|
tel
|
|
|