Skip to content
Snippets Groups Projects
Commit 78d9548c authored by Jaime Arias's avatar Jaime Arias
Browse files

fix syntax

parent 41779125
No related branches found
No related tags found
No related merge requests found
......@@ -123,7 +123,7 @@ class InterpreterParser:
locations_str = self.maude.operators(locations, [], "Location", ["ctor"])
# actions
actions = sorted(model.actions)
actions = sorted(model.actions + ["noaction"])
actions_str = self.maude.operators(actions, [], "Action", ["ctor"])
# automata label
......@@ -236,7 +236,12 @@ class InterpreterParser:
# sync
actions = t.sync
sync_str = f"sync {actions}" if actions in sync_actions else f"local {actions}"
if actions is None:
sync_str = "local noaction"
else:
sync_str = (
f"sync {actions}" if actions in sync_actions else f"local {actions}"
)
# guard
guard = self._normalize_constraints(t.guard)
......
......@@ -4,7 +4,7 @@ mod MODEL is
extending ANALYSIS .
ops cdone idle preparing sugar : -> Location [ctor] .
ops coffee cup press sleep : -> Action [ctor] .
ops coffee cup noaction press sleep : -> Action [ctor] .
op machine : -> AutoId [ctor] .
ops x y : -> Clock [ctor] .
ops p1 p2 p3 : -> Parameter [ctor] .
......
......@@ -4,7 +4,7 @@ mod MODEL is
extending ANALYSIS .
ops active1 active2 check1 check2 cs1 cs2 idle1 idle2 locaccess1 locaccess2 obs1 obs2 obsviolation obswaiting : -> Location [ctor] .
ops access1 access2 enter1 enter2 exit1 exit2 noaccess1 noaccess2 try1 try2 update1 update2 : -> Action [ctor] .
ops access1 access2 enter1 enter2 exit1 exit2 noaccess1 noaccess2 noaction try1 try2 update1 update2 : -> Action [ctor] .
ops observer proc1 proc2 : -> AutoId [ctor] .
ops x1 x2 : -> Clock [ctor] .
op turn : -> DVariable [ctor] .
......
......@@ -4,7 +4,7 @@ mod MODEL is
extending ANALYSIS .
ops approaching choosing crash down emergencylowering far gone initgate inittrain intruderdone lowering nopower up verynear waiting walkinghouse walkingsensor : -> Location [ctor] .
ops breaksensor choosehouse choosesensor endlowering noactiongate noactiontrain pass powercut sensorclose sensorfar startlowering : -> Action [ctor] .
ops breaksensor choosehouse choosesensor endlowering noaction pass powercut sensorclose sensorfar startlowering : -> Action [ctor] .
ops gate intruder train : -> AutoId [ctor] .
ops xgate xintruder xtrain : -> Clock [ctor] .
ops choice gatedown sensoractive start : -> DVariable [ctor] .
......@@ -13,9 +13,9 @@ mod MODEL is
op Train : -> Automaton .
eq Train = < train |
(@ inittrain inv true :
(when (start = 1) local noactiontrain do { nothing } goto far)),
(when (start = 1) local noaction do { nothing } goto far)),
(@ far inv (xtrain <= pfar) :
(when ((xtrain = pfar) and (sensoractive = 0)) local noactiontrain do { xtrain := 0 } goto approaching ,
(when ((xtrain = pfar) and (sensoractive = 0)) local noaction do { xtrain := 0 } goto approaching ,
when ((xtrain = pfar) and (sensoractive = 1)) sync sensorfar do { xtrain := 0 } goto approaching)),
(@ approaching inv (xtrain <= papproaching) :
(when (xtrain = papproaching) sync sensorclose do { nothing } goto verynear)),
......@@ -41,7 +41,7 @@ mod MODEL is
op Gate : -> Automaton .
eq Gate = < gate |
(@ initgate inv true :
(when (start = 1) local noactiongate do { nothing } goto up)),
(when (start = 1) local noaction do { nothing } goto up)),
(@ up inv true :
(when true sync pass do { xgate := 0 } goto up ,
when true sync sensorclose do { xgate := 0 } goto emergencylowering ,
......
......@@ -7,13 +7,13 @@ var
(************************************************************)
automaton train
(************************************************************)
synclabs : sensorfar, sensorclose, pass, noactiontrain;
synclabs : sensorfar, sensorclose, pass;
loc inittrain : invariant True
when start = 1 sync noactiontrain goto far ;
when start = 1 goto far ;
loc far : invariant xtrain <= pfar
when xtrain = pfar & sensoractive = 0 sync noactiontrain do { xtrain := 0 } goto approaching ;
when xtrain = pfar & sensoractive = 0 do { xtrain := 0 } goto approaching ;
when xtrain = pfar & sensoractive = 1 sync sensorfar do { xtrain := 0} goto approaching ;
loc approaching : invariant xtrain <= papproaching
......@@ -52,11 +52,11 @@ end (* intruder *)
(************************************************************)
automaton gate
(************************************************************)
synclabs : noactiongate, pass, sensorclose, powercut, sensorfar, startlowering, endlowering ;
synclabs : pass, sensorclose, powercut, sensorfar, startlowering, endlowering ;
loc initgate : invariant True
when start = 1 sync noactiongate goto up ;
when start = 1 goto up ;
loc up : invariant True
when True sync pass do {xgate:=0} goto up ;
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment