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

add fischer test

parent 5ebe532b
No related branches found
No related tags found
No related merge requests found
...@@ -1003,8 +1003,9 @@ class InterpreterParser(Parser): ...@@ -1003,8 +1003,9 @@ class InterpreterParser(Parser):
] ]
) )
agents = ", ".join([automaton.name.title() for automaton in model.automata]) agents = sorted([automaton.name.title() for automaton in model.automata])
init_eq_str = f"eq {label} = {{ {agents} }}\n{tab}< {config} >\n{tab}." agents_str = ", ".join(agents)
init_eq_str = f"eq {label} = {{ {agents_str} }}\n{tab}< {config} >\n{tab}."
eq = f""" eq = f"""
{init_op} {init_op}
......
...@@ -4,9 +4,9 @@ mod MODEL is ...@@ -4,9 +4,9 @@ mod MODEL is
extending ANALYSIS . extending ANALYSIS .
ops active1 active2 check1 check2 cs1 cs2 idle1 idle2 locaccess1 locaccess2 obs1 obs2 obsviolation obswaiting : -> Location [ctor] . ops active1 active2 check1 check2 cs1 cs2 idle1 idle2 locaccess1 locaccess2 obs1 obs2 obsviolation obswaiting : -> Location [ctor] .
ops access_1 access_2 enter_1 enter_2 exit_1 exit_2 no_access_1 no_access_2 try_1 try_2 update_1 update_2 : Action [ctor] . ops access_1 access_2 enter_1 enter_2 exit_1 exit_2 no_access_1 no_access_2 try_1 try_2 update_1 update_2 : -> Action [ctor] .
op observer proc1 proc2 : -> Agent [ctor] . ops observer proc1 proc2 : -> Agent [ctor] .
ops x1 x2 : Clock [ctor] . ops x1 x2 : -> Clock [ctor] .
op turn : -> DVariable [ctor] . op turn : -> DVariable [ctor] .
ops delta gamma : -> Parameter [ctor] . ops delta gamma : -> Parameter [ctor] .
...@@ -26,7 +26,7 @@ mod MODEL is ...@@ -26,7 +26,7 @@ mod MODEL is
(when true sync exit_1 do { turn := -1 } goto idle1)) > . (when true sync exit_1 do { turn := -1 } goto idle1)) > .
op Observer : -> Automaton . op Observer : -> Automaton .
eq Observer = < observer | eq Observer = < observer |
(@ obswaiting inv true : (@ obswaiting inv true :
( (when true sync enter_1 do {nothing} goto obs1) , ( (when true sync enter_1 do {nothing} goto obs1) ,
(when true sync enter_2 do {nothing} goto obs2))) , (when true sync enter_2 do {nothing} goto obs2))) ,
...@@ -40,7 +40,7 @@ mod MODEL is ...@@ -40,7 +40,7 @@ mod MODEL is
. .
op init : -> State . op init : -> State .
eq init = { Observer, Proc1, Proc2 } eq init = { Observer, Proc1, Proc2 }
< tick: tickOk < tick: tickOk
locs: (proc1 @ idle1, proc2 @ idle2, observer @ obswaiting) locs: (proc1 @ idle1, proc2 @ idle2, observer @ obswaiting)
clocks: (x1 : 0, x2 : 0) clocks: (x1 : 0, x2 : 0)
......
...@@ -19,6 +19,7 @@ def remove_spaces(output_str): ...@@ -19,6 +19,7 @@ def remove_spaces(output_str):
("ex1xy.imi", "ex1xy-nc.maude", "no-collapsing"), ("ex1xy.imi", "ex1xy-nc.maude", "no-collapsing"),
("coffee.imi", "coffee-nc.maude", "no-collapsing"), ("coffee.imi", "coffee-nc.maude", "no-collapsing"),
("coffee.imi", "coffee-intrpr.maude", "interpreter"), ("coffee.imi", "coffee-intrpr.maude", "interpreter"),
("fischer.imi", "fischer-intrpr.maude", "interpreter"),
], ],
) )
def test_parser(examples_dir, imitator_file, maude_file, version): def test_parser(examples_dir, imitator_file, maude_file, version):
......
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