From 2f7bed218fea8ddc593da66ec54b8ab8b2d33939 Mon Sep 17 00:00:00 2001
From: Jaime Arias <arias@lipn.univ-paris13.fr>
Date: Wed, 22 Mar 2023 17:22:19 +0100
Subject: [PATCH] tests: add interpreter test
---
pta2maude/src/Parser.py | 1 -
pta2maude/tests/examples/coffee-intrpr.maude | 43 ++++++++++++++++++++
pta2maude/tests/test_parser.py | 20 +++++----
3 files changed, 55 insertions(+), 9 deletions(-)
create mode 100644 pta2maude/tests/examples/coffee-intrpr.maude
diff --git a/pta2maude/src/Parser.py b/pta2maude/src/Parser.py
index 47e623d..452d061 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 0000000..b4c299a
--- /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 8818cb3..a6037ae 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)
--
GitLab