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

fix tests

parent 7726433d
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
nptav2maude/tests/examples/coffee-intrpr.maude
+ 3
− 3
View file @ df0e7482
......@@ -18,9 +18,9 @@ mod MODEL is
when (y = p2) local cup do { nothing } goto preparing)),
(@ preparing inv (y <= p3) :
(when (y = p3) local coffee do { x := 0 } goto cdone)),
(@ cdone inv (x <= 10) :
(@ cdone inv (x <= 10/1) :
(when true local press do { x := 0 ; y := 0 } goto sugar ,
when (x = 10/1) local sleep do { nothing } goto idle)) >
when (x = 100/10) local sleep do { nothing } goto idle)) >
.
op init : -> State .
......@@ -30,7 +30,7 @@ mod MODEL is
clocks: (x : 0, y : 0)
parameters: (p1 : rr(var(p1)), p2 : rr(var(p2)), p3 : rr(var(p3)))
dvariables: empty
constraint: rr(var(p1)) >= 0 and rr(var(p2)) >= 0 and rr(var(p3)) >= 0
constraint: rr(var(p1)) >= 0/1 and rr(var(p2)) >= 0/1 and rr(var(p3)) >= 0/1
n: 1 >
.
endm
......
nptav2maude/tests/examples/fischer-intrpr.maude
+ 10
− 10
View file @ df0e7482
......@@ -13,13 +13,13 @@ mod MODEL is
op Proc1 : -> Automaton .
eq Proc1 = < proc1 |
(@ idle1 inv true :
(when (turn = -1) local try1 do { x1 := 0 } goto active1)),
(when (turn = -1/1) local try1 do { x1 := 0 } goto active1)),
(@ active1 inv (x1 <= delta) :
(when true local update1 do { turn := 1 ; x1 := 0 } goto check1)),
(@ check1 inv true :
(when ((x1 >= gamma) and (turn = 1)) local access1 do { nothing } goto locaccess1 ,
when ((x1 >= gamma) and (turn < 1)) local noaccess1 do { nothing } goto idle1 ,
when ((x1 >= gamma) and (turn > 1)) local noaccess1 do { nothing } goto idle1)),
(when ((x1 >= gamma) and (turn = 1/1)) local access1 do { nothing } goto locaccess1 ,
when ((x1 >= gamma) and (turn < 1/1)) local noaccess1 do { nothing } goto idle1 ,
when ((x1 >= gamma) and (turn > 1/1)) local noaccess1 do { nothing } goto idle1)),
(@ locaccess1 inv true :
(when true sync enter1 do { nothing } goto cs1)),
(@ cs1 inv true :
......@@ -29,13 +29,13 @@ mod MODEL is
op Proc2 : -> Automaton .
eq Proc2 = < proc2 |
(@ idle2 inv true :
(when (turn = -1) local try2 do { x2 := 0 } goto active2)),
(when (turn = -1/1) local try2 do { x2 := 0 } goto active2)),
(@ active2 inv (x2 <= delta) :
(when true local update2 do { turn := 2 ; x2 := 0 } goto check2)),
(@ check2 inv true :
(when ((x2 >= gamma) and (turn = 2)) local access2 do { nothing } goto locaccess2 ,
when ((x2 >= gamma) and (turn < 2)) local noaccess2 do { nothing } goto idle2 ,
when ((x2 >= gamma) and (turn > 2)) local noaccess2 do { nothing } goto idle2)),
(when ((x2 >= gamma) and (turn = 2/1)) local access2 do { nothing } goto locaccess2 ,
when ((x2 >= gamma) and (turn < 2/1)) local noaccess2 do { nothing } goto idle2 ,
when ((x2 >= gamma) and (turn > 2/1)) local noaccess2 do { nothing } goto idle2)),
(@ locaccess2 inv true :
(when true sync enter2 do { nothing } goto cs2)),
(@ cs2 inv true :
......@@ -62,8 +62,8 @@ mod MODEL is
locs: (proc1 @ idle1, proc2 @ idle2, observer @ obswaiting)
clocks: (x1 : 0, x2 : 0)
parameters: (delta : rr(var(delta)), gamma : rr(var(gamma)))
dvariables: (turn : -1)
constraint: rr(var(delta)) >= 0 and rr(var(gamma)) >= 0
dvariables: (turn : -1/1)
constraint: rr(var(delta)) >= 0/1 and rr(var(gamma)) >= 0/1
n: 1 >
.
......
nptav2maude/tests/examples/train-intruder-intrpr.maude
+ 12
− 12
View file @ df0e7482
......@@ -13,24 +13,24 @@ mod MODEL is
op Train : -> Automaton .
eq Train = < train |
(@ inittrain inv true :
(when (start = 1) local noaction do { nothing } goto far)),
(when (start = 1/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 ((xtrain = pfar) and (sensoractive = 1)) sync sensorfar do { xtrain := 0 } goto approaching)),
(when ((xtrain = pfar) and (sensoractive = 0/1)) local noaction do { xtrain := 0 } goto approaching ,
when ((xtrain = pfar) and (sensoractive = 1/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)),
(@ gone inv (xtrain <= 0) : empty),
(@ crash inv (xtrain <= 0) : empty) >
(when ((xtrain = papproaching) and (gatedown = 0/1)) sync pass do { xtrain := 0 } goto crash ,
when ((xtrain = papproaching) and (gatedown = 1/1)) sync pass do { xtrain := 0 } goto gone)),
(@ gone inv (xtrain <= 0/1) : empty),
(@ crash inv (xtrain <= 0/1) : empty) >
.
op Intruder : -> Automaton .
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/1) local choosesensor do { start := 1 } goto walkingsensor ,
when (choice = 1/1) local choosehouse do { start := 1 } goto walkinghouse)),
(@ walkingsensor inv (xintruder <= pwalkingsensor) :
(when (xintruder = pwalkingsensor) local breaksensor do { xintruder := 0 ; sensoractive := 0 } goto intruderdone)),
(@ walkinghouse inv (xintruder <= pwalkinghouse) :
......@@ -41,7 +41,7 @@ mod MODEL is
op Gate : -> Automaton .
eq Gate = < gate |
(@ initgate inv true :
(when (start = 1) local noaction do { nothing } goto up)),
(when (start = 1/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 ,
......@@ -79,8 +79,8 @@ 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(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
dvariables: (choice : 0/1, gatedown : 0/1, sensoractive : 1/1, start : 0/1)
constraint: rr(var(pwalkingsensor)) >= 0/1 and rr(var(pwalkinghouse)) >= 0/1 and rr(var(pfar)) === 3/1 and rr(var(papproaching)) === 2/1 and rr(var(pverynear)) === 1/1 and rr(var(pwaiting)) === 1/1 and rr(var(pemergencywaiting)) === 1/1 and rr(var(plowering)) === 2/1 and rr(var(pemergencylowering)) === 1/1
n: 1 >
.
endm
......
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