diff --git a/pta2maude/src/Parser.py b/pta2maude/src/Parser.py index 47e623db509f0b6786b9818f8a8172c324fc2ff9..452d061f8360f30ea95c955f5b62f827e6ec94b6 100644 --- a/pta2maude/src/Parser.py +++ b/pta2maude/src/Parser.py @@ -4,7 +4,6 @@ import textwrap from abc import ABC, abstractmethod import antlr4 - from src.dist.ImitatorLexer import ImitatorLexer from src.dist.ImitatorParser import ImitatorParser from src.Imitator import Automaton, Location, Model diff --git a/pta2maude/tests/examples/coffee-intrpr.maude b/pta2maude/tests/examples/coffee-intrpr.maude new file mode 100644 index 0000000000000000000000000000000000000000..b4c299af88673ca4e80943dc6a961ebbedb00a1b --- /dev/null +++ b/pta2maude/tests/examples/coffee-intrpr.maude @@ -0,0 +1,43 @@ +load Semantics . + +mod COFFEE is + extending DYNAMICS . + + ops idle addsugar preparing done : -> Location [ctor] . + ops bstart bsugar cup coffee sleep : -> Action [ctor] . + ops coffee : -> Agent [ctor] . + ops x1 x2 : -> Clock [ctor] . + ops p1 p2 p3 : -> Parameter [ctor] . + + op Coffee : -> Automaton . + eq Coffee = < coffee @ idle | (@ idle inv True : + (when True local bstart do { x1 := 0 ; x2 := 0 } goto addsugar)), + (@ addsugar inv x2 <= p2 : + (when p1 <= x1 local bsugar do { x1 := 0 } goto addsugar ; + when x2 = p2 local cup goto preparing)), + (@ preparing inv x2 <= p3 : + (when x2 = p3 local coffee do { x1 := 0 } goto done)) , + (@ done inv x1 <= c(10) : + (when x1 = c(10) local sleep goto idle ; + when True local bstart do { x1 := 0 ; x2 := 0 } goto addsugar)) + > . + + op init : -> State . + eq init = { Coffee } + < tick: tickOk + clocks: (x1 : 0/1, x2 : 0/1) + parameters: (p1 : 1, p2 : 1, p3 : 1) + dvariables: empty > + . + + --- ------------------------- + var NET : Network . + var CLOCKS : SetAssignment . + var PARAMS : SetAssignment . + var DVARS : SetAssignment . + var SSTDEF : SStateDef . + --- ------------------------- + +endm + +search [1] init =>* { < coffee @ done | SSTDEF > } < tick: tickNotOk clocks: CLOCKS parameters: PARAMS dvariables: DVARS > . diff --git a/pta2maude/tests/test_parser.py b/pta2maude/tests/test_parser.py index 8818cb3ee0b4cecf14f3c3b1ef25835b0706ea8b..a6037ae1e1f34226c17e91531ad8244193df6812 100644 --- a/pta2maude/tests/test_parser.py +++ b/pta2maude/tests/test_parser.py @@ -11,18 +11,22 @@ def remove_spaces(output_str): @pytest.mark.parametrize( - "imitator_file,maude_file,collapsing", + "imitator_file,maude_file,version", [ - ("ex1x.imi", "ex1x.maude", True), - ("ex1xy.imi", "ex1xy.maude", True), - ("ex1x.imi", "ex1x-nc.maude", False), - ("ex1xy.imi", "ex1xy-nc.maude", False), - ("coffee.imi", "coffee-nc.maude", False), + ("ex1x.imi", "ex1x.maude", "collapsing"), + ("ex1xy.imi", "ex1xy.maude", "collapsing"), + ("ex1x.imi", "ex1x-nc.maude", "no-collapsing"), + ("ex1xy.imi", "ex1xy-nc.maude", "no-collapsing"), + ("coffee.imi", "coffee-nc.maude", "no-collapsing"), ], ) -def test_parser(examples_dir, imitator_file, maude_file, collapsing): +def test_parser(examples_dir, imitator_file, maude_file, version): # select the correct parser - parser = CollapsingParser() if collapsing else NoCollapsingParser() + parser = None + if version == "collapsing": + parser = CollapsingParser() + elif version == "no-collapsing": + parser = NoCollapsingParser() # parse the imitator file input_file = os.path.join(examples_dir, imitator_file)