Reachability example
Reachability example: use of reax to chech reachability of states.
This commit is contained in:
parent
15238eaf8b
commit
f284ff2872
2 changed files with 27 additions and 0 deletions
2
examples/reachability/build.sh
Executable file
2
examples/reachability/build.sh
Executable file
|
@ -0,0 +1,2 @@
|
|||
heptc -target ctrln reachability.ept
|
||||
reax -a 'sB:r' reachability_ctrln/reach_verif.ctrln
|
25
examples/reachability/reachability.ept
Normal file
25
examples/reachability/reachability.ept
Normal file
|
@ -0,0 +1,25 @@
|
|||
node reach_verif(day_event,night_event,noon_event:bool) = (day_state,evening_state:bool)
|
||||
|
||||
contract
|
||||
reachable evening_state
|
||||
|
||||
let
|
||||
automaton
|
||||
state Night do day_state = false; evening_state = false
|
||||
until day_event then Day
|
||||
state Day do
|
||||
day_state = true;
|
||||
automaton
|
||||
state Morning do
|
||||
evening_state = false;
|
||||
until noon_event then Afternoon
|
||||
state Afternoon do
|
||||
evening_state = false;
|
||||
until night_event then Evening
|
||||
state Evening do
|
||||
evening_state = true;
|
||||
until day_event then Morning
|
||||
end
|
||||
until night_event then Night
|
||||
end
|
||||
tel
|
Loading…
Reference in a new issue