Minor bug fixes, pyproject.toml, and TOML for tests

Makefile

@@ -8,7 +8,7 @@ PYTHON ?= /usr/bin/env python3
 # Bundle the all the Python and data file into single executable zip file
 # (based on Stack Overflow's question 17486578)
 
-RESOURCES = umaudemc/data/*.maude umaudemc/data/*.js umaudemc/data/*.css umaudemc/data/select.htm
+RESOURCES = umaudemc/data/*.maude umaudemc/data/*.js umaudemc/data/*.css umaudemc/data/*.htm
 CODE      = umaudemc/*.py umaudemc/*/*.py
 
 dist/umaudemc: dist $(RESOURCES) $(CODE)
@@ -22,13 +22,13 @@ dist/umaudemc: dist $(RESOURCES) $(CODE)
 	cd zip ; zip -q ../umaudemc.zip $(RESOURCES) $(CODE) __main__.py
 	rm -rf zip
 	# Put the shebang and then the zip file into the executable bundle
-	echo '#!$(PYTHON)' > dist/umaudemc
-	cat umaudemc.zip >> dist/umaudemc
+	echo '#!$(PYTHON)' > $@
+	cat umaudemc.zip >> $@
 	rm umaudemc.zip
-	chmod a+x dist/umaudemc
+	chmod a+x $@
 
 wheel:
-	python setup.py bdist_wheel
+	pip wheel --no-deps -w dist .
 
 dist:
 	mkdir -p dist

README.md

@@ -22,7 +22,7 @@ in the [GraphViz](https://graphviz.org/)'s DOT format.
 * `gui [--web]` to model check from a graphical user interface.
 * `test [--benchmark] <filename>` to test or benchmark model-checking cases.
 
-Formulae are expressed in a syntax extending the `LTL` module of the 
+Formulae are expressed in a syntax extending the `LTL` module of the
 `model-checker.maude` file in the official distribution. For CTL and CTL*, the
 universal `A_` and existential `E_` path quantifiers are available. For the
 μ-calculus, there are the universal `[_]_` and existential `<_>_` modalities,
@@ -32,7 +32,7 @@ be a dot to mean that any action is fine, and the list may be preceded by a
 negation symbol `~` to indicate its complement.
 
 Probabilistic model checking is available through the `pcheck` command with a
-syntax similar to `check`. By default, it calculates the probability of the 
+syntax similar to `check`. By default, it calculates the probability of the
 given LTL, CTL, or PCTL formula. For a reachability formula, the options
 `--steps` and `--reward <term>` can be passed to calculate instead the expected
 number of steps or reward, respectively. Formulae
@@ -207,4 +207,5 @@ References
 
 More details about the integration of the external classical model checkers can be found
 in [*Strategies, model checking and branching-time properties in Maude*](https://doi.org/10.1016/j.jlamp.2021.100700)
-and in [*Model checking of strategy-controlled systems in rewriting logic*](https://eprints.ucm.es/71531).
+and in [*Model checking of strategy-controlled systems in rewriting logic*](https://hdl.handle.net/20.500.14352/3553).
+Support for quantitative model checking is described in [*QMaude: quantitative specification and verification in rewriting logic*](https://doi.org/10.1007/978-3-031-27481-7_15).

pyproject.toml

@@ -0,0 +1,56 @@
+[project]
+name            = 'umaudemc'
+version         = '0.12.2'
+description     = 'Unified Maude model-checking utility'
+license.text    = 'GPLv3'
+classifiers     = [
+	'Programming Language :: Python :: 3',
+	'Intended Audience :: Science/Research',
+	'License :: OSI Approved :: GNU General Public License v3 (GPLv3)',
+	'Topic :: Scientific/Engineering',
+	'Operating System :: OS Independent',
+]
+requires-python = '>=3.7'
+dependencies    = ['maude >= 1.0']
+
+[[project.authors]]
+name  = 'ningit'
+email = 'ningit@users.noreply.github.com'
+
+[project.readme]
+content-type = 'text/markdown'
+text = '''# Unified Maude model-checking tool
+
+Uniform interface for model checking LTL, CTL, CTL*, and μ-calculus properties
+on standard and [strategy](https://maude.ucm.es/strategies)-controlled
+[Maude](https://maude.cs.illinois.edu) specifications using built-in and
+external backends. Models can also be extended with quantitative information
+and be applied probabilistic and statistical model-checking techniques.
+
+This tool can be used from the command line, from a graphical user interface,
+and as a Python library. See the
+[repository](https://github.com/fadoss/umaudemc) for additional information,
+documentation, and examples.'''
+
+[project.optional-dependencies]
+CTLStar = ['pyModelChecking >= 1.3.3']
+YAML    = ['pyaml']
+Plot    = ['matplotlib']
+SMC     = ['scipy']
+
+[project.urls]
+"Homepage"      = 'https://github.com/fadoss/umaudemc'
+"Bug Tracker"   = 'https://github.com/fadoss/umaudemc/issues'
+"Documentation" = 'https://github.com/fadoss/umaudemc'
+"Source Code"   = 'https://github.com/fadoss/umaudemc'
+
+[project.scripts]
+umaudemc = 'umaudemc.__main__:main'
+
+[build-system]
+requires      = ['setuptools', 'wheel']
+build-backend = 'setuptools.build_meta'
+
+[tool.setuptools]
+packages.find.include = ['umaudemc*']
+package-data.umaudemc = ['data/*']

test/api/apitest.py

@@ -9,17 +9,17 @@
 import maude
 import umaudemc.api as api
 
+# Init Maude and load its files
+maude.init(advise=False)
+maude.load('../check/vending')
+
 
 class APITest(unittest.TestCase):
 
 	def __init__(self, *args, **kwargs):
 		super().__init__(*args, **kwargs)
 
-		import maude
-		maude.init(advise=False)
-		maude.load('../check/vending')
-
-		self.m = maude.getCurrentModule()
+		self.m = maude.getModule('VENDING-MACHINE-CHECK')
 		self.t = self.m.parseTerm('initial')
 		self.a = self.m.parseStrategy('put1 ; apple | put1 ; put1 ; cake')
 		self.b = self.m.parseStrategy('put1 ; (apple | put1 ; cake)')

test/check/kleene.test

@@ -1,6 +1,8 @@
 # Test for the Kleene star semantics
 #+ for: spot maude ltsmin
 
+# The number of rewrites in the second command is not deterministic for LTSmin
+
 umaudemc check cupsballs initial '[] <> uncovered' cups
 umaudemc check cupsballs initial '[] <> uncovered' cups -k
 umaudemc check cupsballs initial '[] <> uncovered' cups --kleene-iteration

test/graph/dotp.expected

@@ -66,34 +66,39 @@ digraph {
 digraph {
 	0 [label="head"];
 	1 [label="tail"];
-	0 -> 1 [label="8/13 "];
+	0 -> 1 [label="8/13 ttail"];
 	2 [label="head"];
-	0 -> 2 [label="5/13 "];
+	0 -> 2 [label="5/13 thead"];
 	3 [label="tail"];
-	1 -> 3;
-	2 -> 3;
+	1 -> 3 [label="ttail"];
+	2 -> 3 [label="ttail"];
 }
 digraph {
 	0 [label="head"];
-	1 [label="tail"];
-	0 -> 1 [label="8/13 "];
-	2 [label="head"];
-	0 -> 2 [label="5/13 "];
-	1 -> 1 [label="8/13 "];
-	1 -> 2 [label="5/13 "];
-	2 -> 1 [label="8/13 "];
-	2 -> 2 [label="5/13 "];
+	1 [label="head"];
+	0 -> 1;
+	2 [label="tail"];
+	0 -> 2 [label="8/13 ttail"];
+	3 [label="head"];
+	0 -> 3 [label="5/13 thead"];
+	4 [label="tail"];
+	2 -> 4;
+	2 -> 2 [label="8/13 ttail"];
+	2 -> 3 [label="5/13 thead"];
+	3 -> 1;
+	3 -> 2 [label="8/13 ttail"];
+	3 -> 3 [label="5/13 thead"];
 }
 digraph {
 	0 [label="head"];
 	1 [label="tail"];
-	0 -> 1 [label="8/13 "];
+	0 -> 1 [label="8/13 ttail"];
 	2 [label="head"];
-	0 -> 2 [label="5/13 "];
+	0 -> 2 [label="5/13 thead"];
 	3 [label="tail"];
-	1 -> 3 [label="3/10 "];
+	1 -> 3 [label="3/10 ttail"];
 	4 [label="head"];
-	1 -> 4 [label="7/10 "];
-	2 -> 3 [label="3/10 "];
-	2 -> 4 [label="7/10 "];
+	1 -> 4 [label="7/10 thead"];
+	2 -> 3 [label="3/10 ttail"];
+	2 -> 4 [label="7/10 thead"];
 }

test/graph/prism.expected

@@ -70,9 +70,9 @@ module M
 	// 
 	[] x=0 -> 1.0:(x'=1);
 	// 
-	[] x=1 -> 0.16666666666666666:(x'=2) + 0.8333333333333333:(x'=6);
+	[] x=1 -> 0.16666666666666666:(x'=2) + 0.8333333333333334:(x'=6);
 	// 
-	[] x=2 -> 0.41666666666666663:(x'=3) + 0.5833333333333333:(x'=5);
+	[] x=2 -> 0.4166666666666667:(x'=3) + 0.5833333333333334:(x'=5);
 	// 
 	[] x=3 -> 1.0:(x'=4);
 	// 
@@ -137,38 +137,48 @@ endmodule
 label "head" = x=0 | x=2;
 label "tail" = x=1 | x=3;
 
+rewards
+	[] true: 1;
+endrewards
+mdp
+
+module M
+	x : [0..5] init 0;
+
+	// head
+	[] x=0 -> 1.0:(x'=1);
+	// head
+	[] x=0 -> 0.6153846153846154:(x'=2) + 0.38461538461538464:(x'=3);
+	// tail
+	[] x=2 -> 1.0:(x'=4);
+	// tail
+	[] x=2 -> 0.6153846153846154:(x'=2) + 0.38461538461538464:(x'=3);
+	// head
+	[] x=3 -> 1.0:(x'=1);
+	// head
+	[] x=3 -> 0.6153846153846154:(x'=2) + 0.38461538461538464:(x'=3);
+
+endmodule
+label "head" = x=0 | x=1 | x=3;
+label "tail" = x=2 | x=4;
+
 rewards
 	[] true: 1;
 endrewards
 dtmc
 
 module M
-	x : [0..3] init 0;
+	x : [0..5] init 0;
 
 	// head
 	[] x=0 -> 0.6153846153846154:(x'=1) + 0.38461538461538464:(x'=2);
 	// tail
-	[] x=1 -> 0.6153846153846154:(x'=1) + 0.38461538461538464:(x'=2);
+	[] x=1 -> 0.3:(x'=3) + 0.7:(x'=4);
 	// head
-	[] x=2 -> 0.6153846153846154:(x'=1) + 0.38461538461538464:(x'=2);
+	[] x=2 -> 0.3:(x'=3) + 0.7:(x'=4);
 
 endmodule
-label "head" = x=0 | x=2;
-label "tail" = x=1;
 
 rewards
 	[] true: 1;
 endrewards
-digraph {
-	0 [label="head"];
-	1 [label="tail"];
-	0 -> 1 [label="8/13 "];
-	2 [label="head"];
-	0 -> 2 [label="5/13 "];
-	3 [label="tail"];
-	1 -> 3 [label="3/10 "];
-	4 [label="head"];
-	1 -> 4 [label="7/10 "];
-	2 -> 3 [label="3/10 "];
-	2 -> 4 [label="7/10 "];
-}

test/graph/prism.test

@@ -11,5 +11,4 @@ umaudemc graph ../pcheck/coin head --passign metadata --format prism --aprops he
 umaudemc graph ../pcheck/coin head 'choice(8 : ttail, 5 : thead) ; ttail' --passign strategy --format prism --aprops head,tail
 umaudemc graph ../pcheck/coin head 'choice(8 : ttail, 5 : thead) *' --passign strategy --format prism --aprops head,tail
 
-# TODO: este no funciona como esperaba
-umaudemc graph ../pcheck/coin head 'choice(8 : ttail, 5 : thead) ; choice(3 : ttail, 7 : thead)' --passign strategy
+umaudemc graph ../pcheck/coin head 'choice(8 : ttail, 5 : thead) ; choice(3 : ttail, 7 : thead)' --passign strategy --format prism

test/pcheck/formula_prism.expected

@@ -7,8 +7,8 @@ The property is satisfied (2 system states, 8 rewrites).
 Result: 0.38461538461538464
 Result: 0.992211275420189
 The property is satisfied (2 system states, 8 rewrites).
-Result: 0.30000000000000004
-Result: 0.9717524751000003
+Result: 0.3
+Result: 0.9717524750999997
 The property is satisfied (2 system states, 8 rewrites).
 Result: 0.3
 Result: 0.9717524750999997
@@ -19,9 +19,9 @@ The property is satisfied (2 system states, 8 rewrites).
 Result: 0.3
 Result: 0.3
 The property is not satisfied (3 system states, 6 rewrites).
-Result: 0.3
-Result: 0.9717524750999997
-The property is satisfied (3 system states, 6 rewrites).
+Result: 0.0 to 0.3
+Result: 0.0 to 0.9717524750999997
+Result: 0.0
 Result: 0.3
 Result: 0.58
 The property is not satisfied (5 system states, 10 rewrites).