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

remove extra spaces

parent 0e650816
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
pta2maude/tests/examples/train-intruder-intrpr.maude
+ 29
− 28
View file @ ae1a61f7
......@@ -3,8 +3,8 @@ load analysis .
mod MODEL is
extending ANALYSIS .
ops approaching choosing crash down emergencylowering far gone initgate initintruder inittrain intruderdone lowering nopower up verynear waiting walkinghouse walkingsensor : -> Location [ctor] .
ops breaksensor choosehouse choosesensor endlowering noaction pass powercut sensorclose sensorfar startlowering : -> Action [ctor] .
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 gate intruder train : -> Agent [ctor] .
ops xgate xintruder xtrain : -> Clock [ctor] .
ops choice gatedown sensoractive start : -> DVariable [ctor] .
......@@ -13,49 +13,49 @@ mod MODEL is
op Train : -> Automaton .
eq Train = < train |
(@ inittrain inv true :
(when (start = 1) local noaction do { nothing } goto far)),
(@ far (inv xtrain <= pfar) :
(when ((xtrain = pfar) and (sensoractive = 0)) local noaction do { xtrain := 0 } goto approaching ,
(when (start = 1) local noactiontrain 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 = 1)) sync sensorfar do { xtrain := 0 } goto approaching)),
(@ approaching inv (xtrain <= papproaching) :
(when (xtrain = papproaching) sync sensorclose do { nothing } goto verynear)),
(@ verynear inv (xtrain <= papproaching) :
(when ((xtrain = papproaching) and (gatedown = 0)) sync pass do {xtrain := 0} goto crash ,
when ((xtrain = papproaching) and (gatedown = 1)) sync pass do {xtrain := 0} goto gone)),
(when ((xtrain = papproaching) and (gatedown = 0)) sync pass do { xtrain := 0 } goto crash ,
when ((xtrain = papproaching) and (gatedown = 1)) sync pass do { xtrain := 0 } goto gone)),
(@ gone inv (xtrain <= 0) : empty),
(@ crash inv (xtrain <= 0) : empty)>
(@ crash inv (xtrain <= 0) : empty) >
.
op Intruder : -> Automaton .
eq Intruder = < intruder |
eq Intruder = < intruder |
(@ choosing inv true :
(when (choice = 0) local choosesensor do { start := 1} goto walkingsensor ,
when (choice = 1) local choosehouse do { start := 1} goto walkinghouse)),
(when (choice = 0) local choosesensor do { start := 1 } goto walkingsensor ,
when (choice = 1) local choosehouse do { start := 1 } goto walkinghouse)),
(@ walkingsensor inv (xintruder <= pwalkingsensor) :
(when (xintruder = pwalkingsensor) local breaksensor do { xintruder := 0 ; sensoractive := 0} goto intruderdone)),
(when (xintruder = pwalkingsensor) local breaksensor do { xintruder := 0 ; sensoractive := 0 } goto intruderdone)),
(@ walkinghouse inv (xintruder <= pwalkinghouse) :
(when (xintruder = pwalkinghouse) sync powercut do { xintruder := 0 ; sensoractive := 0} goto intruderdone)),
(when (xintruder = pwalkinghouse) sync powercut do { xintruder := 0 ; sensoractive := 0 } goto intruderdone)),
(@ intruderdone inv true : empty) >
.
op Gate : -> Automaton .
eq Gate = < gate |
eq Gate = < gate |
(@ initgate inv true :
(when (start = 1) local noaction do { nothing } goto up)),
(when (start = 1) local noactiongate do { nothing } goto up)),
(@ up inv true :
(when true sync pass do { xgate := 0 } goto up ,
(when true sync pass do { xgate := 0 } goto up ,
when true sync sensorclose do { xgate := 0 } goto emergencylowering ,
when true sync powercut do { xgate := 0 } goto nopower ,
when true sync sensorfar do { xgate := 0 } goto waiting )),
when true sync powercut do { xgate := 0 } goto nopower ,
when true sync sensorfar do { xgate := 0 } goto waiting)),
(@ waiting inv (xgate <= pwaiting) :
(when true sync powercut do {xgate := 0} goto nopower ,
when true sync sensorclose do {xgate := 0} goto emergencylowering ,
when true sync pass do {xgate := 0} goto up ,
when (xgate = pwaiting) local startlowering do {xgate := 0} goto lowering)),
(when true sync powercut do { xgate := 0 } goto nopower ,
when true sync sensorclose do { xgate := 0 } goto emergencylowering ,
when true sync pass do { xgate := 0 } goto up ,
when (xgate = pwaiting) local startlowering do { xgate := 0 } goto lowering)),
(@ lowering inv (xgate <= plowering) :
(when true sync powercut do { nothing } goto lowering ,
when true sync sensorclose do { nothing } goto lowering ,
when true sync pass do { xgate := 0} goto up ,
when true sync pass do { xgate := 0 } goto up ,
when (xgate = plowering) local endlowering do { xgate := 0 ; gatedown := 1 } goto down)),
(@ down inv true :
(when true sync powercut do { nothing } goto down ,
......@@ -69,8 +69,8 @@ mod MODEL is
(@ emergencylowering inv (xgate <= pemergencylowering) :
(when true sync powercut do { nothing } goto emergencylowering ,
when true sync sensorclose do { nothing } goto emergencylowering ,
when true sync pass do {xgate := 0 } goto up ,
when (xgate = pemergencylowering) local endlowering do {xgate := 0 ; gatedown := 1 } goto down))>
when true sync pass do { xgate := 0 } goto up ,
when (xgate = pemergencylowering) local endlowering do { xgate := 0 ; gatedown := 1 } goto down)) >
.
op init : -> State .
......@@ -79,9 +79,10 @@ mod MODEL is
locs: (train @ inittrain, intruder @ choosing, gate @ initgate)
clocks: (xtrain : 0, xintruder : 0, xgate : 0)
parameters: (pfar : rr(var(pfar)), papproaching : rr(var(papproaching)), pverynear : rr(var(pverynear)), pwalkingsensor : rr(var(pwalkingsensor)), pwalkinghouse : rr(var(pwalkinghouse)), pwaiting : rr(var(pwaiting)), plowering : rr(var(plowering)), pemergencywaiting : rr(var(pemergencywaiting)), pemergencylowering : rr(var(pemergencylowering)))
dvariables: (choice: 0, gatedown : 0, sensoractive : 1, start : 0)
constraint: rr(var(pwalkingsensor)) >= 0 and rr(var(pwalkinghouse)) >= 0 and rr(var(choice)) >= 0 and rr(var(choice)) <= 1 and rr(var(pfar)) === 3 and rr(var(papproaching)) === 2 and rr(var(pverynear)) === 1 and rr(var(pwaiting)) === 1 and rr(var(pemergencywaiting)) === 1 and rr(var(plowering)) === 2 and rr(var(pemergencylowering)) === 1
n: 1 > .
dvariables: (choice : 0, gatedown : 0, sensoractive : 1, start : 0)
constraint: rr(var(pwalkingsensor)) >= 0 and rr(var(pwalkinghouse)) >= 0 and rr(var(choice)) >= 0 and rr(var(choice)) <= 1 and rr(var(pfar)) === 3 and rr(var(papproaching)) === 2 and rr(var(pverynear)) === 1 and rr(var(pwaiting)) === 1 and rr(var(pemergencywaiting)) === 1 and rr(var(plowering)) === 2 and rr(var(pemergencylowering)) === 1
n: 1 >
.
endm
red synthesis [ 1 ] in 'MODEL : init => (train @ crash) .
......
pta2maude/tests/examples/train-intruder-intrpr.imi → pta2maude/tests/examples/train-intruder.imi
+ 7
− 8
View file @ ae1a61f7
......@@ -7,13 +7,13 @@ var
(************************************************************)
automaton train
(************************************************************)
synclabs : sensorfar, sensorclose, pass, noaction;
synclabs : sensorfar, sensorclose, pass, noactiontrain;
loc inittrain : invariant True
when start = 1 sync noaction goto far ;
when start = 1 sync noactiontrain goto far ;
loc far : invariant xtrain <= pfar
when xtrain = pfar & sensoractive = 0 sync noaction do { xtrain := 0 } goto approaching ;
when xtrain = pfar & sensoractive = 0 sync noactiontrain 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 : noaction, pass, sensorclose, powercut, sensorfar, startlowering, endlowering ;
synclabs : noactiongate, pass, sensorclose, powercut, sensorfar, startlowering, endlowering ;
loc initgate : invariant True
when start = 1 sync noaction goto up ;
when start = 1 sync noactiongate goto up ;
loc up : invariant True
when True sync pass do {xgate:=0} goto up ;
......@@ -64,7 +64,7 @@ loc up : invariant True
when True sync powercut do {xgate:=0} goto nopower ;
when True sync sensorfar do {xgate:=0} goto waiting ;
loc waiting : invariant xgate <= plowering
loc waiting : invariant xgate <= pwaiting
when True sync powercut do {xgate:=0} goto nopower ;
when True sync sensorclose do {xgate:=0} goto emergencylowering ;
when True sync pass do {xgate:=0} goto up ;
......@@ -111,6 +111,7 @@ init :=
(*------------------------------------------------------------*)
(* Discrete assignments *)
(*------------------------------------------------------------*)
& choice = 0
& gatedown = 0
& sensoractive = 1
& start = 0
......@@ -120,8 +121,6 @@ init :=
(*------------------------------------------------------------*)
& pwalkingsensor >= 0
& pwalkinghouse >= 0
& choice >= 0
& choice <= 1
& pfar = 3
& papproaching = 2
& pverynear = 1
......
pta2maude/tests/test_parser.py
+ 1
− 0
View file @ ae1a61f7
......@@ -20,6 +20,7 @@ def remove_spaces(output_str):
("coffee.imi", "coffee-nc.maude", "no-collapsing"),
("coffee.imi", "coffee-intrpr.maude", "interpreter"),
("fischer.imi", "fischer-intrpr.maude", "interpreter"),
("train-intruder.imi", "train-intruder-intrpr.maude", "interpreter"),
],
)
def test_parser(examples_dir, imitator_file, maude_file, version):
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment