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

improve syntax

parent a8e7f8dc
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
+ 80
− 93
View file @ 64d48d6d
load analysis .
***(
Train Example in
Étienne André, Michal Knapik, Wojciech Penczek, Laure Petrucci:
Controlling Actions and Time in Parametric Timed Automata. ACSD 2016: 45-54
The integer variable choice is used to determine the choice of the intruder
*)
load ../analysis .
mod TRAIN is
mod MODEL is
--- extending SEMANTICS-FME .
extending ANALYSIS .
......@@ -43,88 +34,81 @@ mod TRAIN is
--- Specification of the 3 automata
op aTrain : -> Automaton .
eq aTrain = < train |
( @ inittrain inv true :
( when (start = 1) local noaction goto far
)),
( @ far inv xtrain <= pfar :
(
when ( (xtrain = pfar) and (sensoractive = 1)) sync sensorfar do { xtrain := 0 } goto approaching ,
when ( (xtrain = pfar) and (sensoractive = 0)) local noaction do { xtrain := 0 } goto approaching
)
),
( @ approaching inv (xtrain <= (papproaching - pverynear)) :
( when ( (xtrain = (papproaching - pverynear))) sync sensorclose goto verynear)),
( @ verynear inv (xtrain <= papproaching) :
( 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)
),
( @ gone inv (xtrain <= 0) : empty),
( @ crash inv (xtrain <= 0) : empty)
> .
(@ inittrain inv true :
(when (start = 1) local noaction goto far)),
(@ far inv xtrain <= pfar :
(when ((xtrain = pfar) and (sensoractive = 1)) sync sensorfar do { xtrain := 0 } goto approaching ,
when ((xtrain = pfar) and (sensoractive = 0)) local noaction do { xtrain := 0 } goto approaching)),
(@ approaching inv (xtrain <= (papproaching - pverynear)) :
(when ( (xtrain = (papproaching - pverynear))) sync sensorclose goto verynear)),
(@ verynear inv (xtrain <= papproaching) :
(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)),
(@ gone inv (xtrain <= 0) : empty),
(@ crash inv (xtrain <= 0) : empty)>
.
op aIntruder : -> Automaton .
eq aIntruder = < intruder |
( @ choosing inv true : --- Note that choice =i according to the transition
( when (choice = 0) local choosesensor do { start := 1} goto walkingsensor ,
when (choice = 1) local choosehouse do { start := 1} goto walkinghouse )),
(@ choosing inv true : --- Note that choice =i according to the transition
(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 )),
( @ walkingsensor inv (xintruder <= pwalkingsensor) :
( 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)),
( @ walkinghouse inv (xintruder <= pwalkinghouse) :
( when (xintruder = pwalkinghouse) sync powercut do { xintruder := 0 ; sensoractive := 0} goto intruderdone)
),
( @ intruderdone inv true : empty )
> .
(@ intruderdone inv true : empty)>
.
op aGate : -> Automaton .
eq aGate = < gate |
( @ initgate inv true :
( when (start = 1) local noaction goto up
)),
( @ up inv true :
(
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 )
),
( @ waiting inv (xgate <= pwaiting) :
(
when true sync sensorclose do {xgate := 0} goto emergencylowering ,
when true sync pass do {xgate := 0} goto up ,
when true sync powercut do {xgate := 0} goto nopower ,
when (xgate = pwaiting) local startlowering do {xgate := 0} goto lowering
)
),
( @ lowering inv (xgate <= plowering) :
(@ initgate inv true :
(when (start = 1) local noaction goto up)),
(@ up inv true :
(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 )),
(@ waiting inv (xgate <= pwaiting) :
(when true sync sensorclose do {xgate := 0} goto emergencylowering ,
when true sync pass do {xgate := 0} goto up ,
when true sync powercut do {xgate := 0} goto nopower ,
when (xgate = pwaiting) local startlowering do {xgate := 0} goto lowering)),
(@ lowering inv (xgate <= plowering) :
( when true sync sensorclose goto lowering ,
when true sync powercut goto lowering ,
when (xgate = plowering) local endlowering do { xgate := 0 ; gatedown := 1 } goto down ,
when true sync pass do { xgate := 0} goto up )
),
( @ down inv true :
( when true sync sensorclose goto down ,
when true sync powercut goto down ,
when true sync pass do { xgate := 0 } goto up
)
),
( @ nopower inv (xgate <= pemergencywaiting) :
( when true sync sensorfar do { xgate := 0 } goto nopower ,
when true sync pass do { xgate := 0 } goto nopower ,
when true sync sensorclose do { xgate := 0 } goto emergencylowering ,
when (xgate = pemergencywaiting) local startlowering do { xgate := 0 } goto emergencylowering
)
),
( @ emergencylowering inv (xgate <= pemergencylowering) :
( when true sync powercut goto emergencylowering ,
when true sync sensorclose goto emergencylowering ,
when (xgate = pemergencylowering) local endlowering do {xgate := 0 ; gatedown := 1 } goto down ,
when true sync pass do {xgate := 0 } goto up
)
)
> .
--- Initial constraint for the parameters
when true sync pass do { xgate := 0} goto up )),
(@ down inv true :
(when true sync sensorclose goto down ,
when true sync powercut goto down ,
when true sync pass do { xgate := 0 } goto up)),
(@ nopower inv (xgate <= pemergencywaiting) :
(when true sync sensorfar do { xgate := 0 } goto nopower ,
when true sync pass do { xgate := 0 } goto nopower ,
when true sync sensorclose do { xgate := 0 } goto emergencylowering ,
when (xgate = pemergencywaiting) local startlowering do { xgate := 0 } goto emergencylowering)),
(@ emergencylowering inv (xgate <= pemergencylowering) :
(when true sync powercut goto emergencylowering ,
when true sync sensorclose goto emergencylowering ,
when (xgate = pemergencylowering) local endlowering do {xgate := 0 ; gatedown := 1 } goto down ,
when true sync pass do {xgate := 0 } goto up))>
.
op init-constraint : -> BoolExpr .
eq init-constraint =
rr(var(pwalkingsensor)) >= 0 and
......@@ -140,12 +124,13 @@ mod TRAIN is
rr(var(pemergencylowering)) === 1/1
.
--- Initial state
op init : -> State .
eq init = { aTrain, aIntruder, aGate }
< tick: tickOk
locs: (train @ inittrain, intruder @ choosing, gate @ initgate)
clocks: (xtrain : 0, xintruder : 0, xgate : 0)
parameters: (
pfar : rr(var(pfar)),
papproaching : rr(var(papproaching)),
......@@ -156,18 +141,20 @@ mod TRAIN is
plowering : rr(var(plowering)),
pemergencywaiting : rr(var(pemergencywaiting)),
pemergencylowering : rr(var(pemergencylowering)))
dvariables: (choice : rr(var(choice)),
sensoractive : 1,
gatedown : 0,
start : 0
)
start : 0)
constraint: init-constraint
n: 1 > .
endm
eof
--- EF(train in crash)
red synthesis [ 1 ] in 'TRAIN : init => (train @ crash) .
--- EF(train in crash) with folding
red search-folding in 'TRAIN : init => (train @ crash) .
--- Computing the whole PZG
red search-folding in 'TRAIN : init .
red synthesis [ 1 ] in 'MODEL : init => (train @ crash) .
red search-folding [ 1 ] in 'MODEL : init => (train @ crash) .
quit .
eof
\ No newline at end of file
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