Probabilistic model checking with sample and discrete distributions a…

…nd other changes

README.md

@@ -56,7 +56,7 @@ Dependencies
 ------------
 
 The `umaudemc` tool requires the [`maude`](https://pypi.org/project/maude) package
-and Python 3.7 or newer. This provides support for LTL, CTL and μ-calculus
+and Python 3.9 or newer. This provides support for LTL, CTL and μ-calculus
 model checking. However, other external backends can be installed:
 
 * The built-in LTL model checker included in Maude and its extension for

pyproject.toml

@@ -1,6 +1,6 @@
 [project]
 name            = 'umaudemc'
-version         = '0.13.1'
+version         = '0.14.0'
 description     = 'Unified Maude model-checking utility'
 license.text    = 'GPLv3'
 classifiers     = [
@@ -10,7 +10,7 @@ classifiers     = [
 	'Topic :: Scientific/Engineering',
 	'Operating System :: OS Independent',
 ]
-requires-python = '>=3.7'
+requires-python = '>=3.9'
 dependencies    = ['maude >= 1.0']
 
 [[project.authors]]

test/api/apitest.py

@@ -35,7 +35,7 @@ def test_graph(self):
 			text = out.getvalue()
 			self.assertTrue(text.startswith('digraph {'))
 			self.assertTrue('[label="e e [empty]"]' in text)
-			self.assertTrue('label="rl e O:Soup [I:Soup] =>' in text)
+			self.assertTrue('label="rl [put1] : e O:Soup [I:Soup] =>' in text)
 
 		with io.StringIO() as out:
 			self.smodel.print_graph(out, sformat='{%t |= hasCake}', eformat='%l %l')

test/pcheck/sample.maude

@@ -0,0 +1,38 @@
+***
+*** Sample strategy with discrete distributions
+*** and related probabilistic strategies
+***
+
+mod FOO is
+	protecting FLOAT .
+	protecting INT .
+	protecting LIST{Float} .
+
+	sort Foo .
+
+	op <_> : Float -> Foo [ctor] .
+	op <<_>> : Int -> Foo [ctor] .
+
+	vars F G : Float .
+	vars N M : Int .
+
+	rl [set] : < F > => < G > [nonexec] .
+	rl [iset] : << N >> => << M >> [nonexec] .
+	rl [null] : F => 0.0 [nonexec] .
+endm
+
+smod FOO-STRAT is
+	protecting FOO .
+
+	strats ex-choice ex-bernou ex-unif ex-matchrew @ Foo .
+	strat ex-unif : Int @ Foo .
+
+	vars F G : Float .
+	vars N M : Int .
+
+	sd ex-choice := choice(1.0 : set[G <- 1.0], 2.0 : set[G <- 2.0]) .
+	sd ex-bernou := sample G := bernoulli(0.9) in set[G <- G] .
+	sd ex-unif := sample M := uniform(1, 3) in iset[M <- M] .
+	sd ex-unif(N) := sample M := uniform(1, N) in iset[M <- M] .
+	sd ex-matchrew := amatchrew F with weight F by F using null .
+endsm

test/pcheck/sample.test

@@ -0,0 +1,10 @@
+# Sample operator with discrete distributions
+#+ for: prism storm
+
+umaudemc pcheck sample '< 0.0 >' @steady ex-bernou --assign strategy --fraction
+umaudemc pcheck sample '<< 0 >>' @steady ex-unif --assign strategy --fraction
+umaudemc pcheck sample '<< 0 >>' @steady 'ex-unif(7)' --assign strategy --fraction
+
+umaudemc pcheck sample '< 0.0 >' @steady ex-choice --assign strategy --fraction
+umaudemc pcheck sample '1.0 2.0 3.0 4.0' @steady ex-matchrew --assign strategy --fraction
+umaudemc pcheck sample '1.0 2.0 3.0 4.0' @steady 'amatchrew F with weight 1 by F using null' --assign strategy --fraction

test/pcheck/sample_prism.expected

@@ -0,0 +1,22 @@
+ 9/10                 < 1.0 >
+ 1/10                 < 0.0 >
+ 1/3                  << 1 >>
+ 1/3                  << 2 >>
+ 1/3                  << 3 >>
+ 1/7                  << 1 >>
+ 1/7                  << 2 >>
+ 1/7                  << 3 >>
+ 1/7                  << 4 >>
+ 1/7                  << 5 >>
+ 1/7                  << 6 >>
+ 1/7                  << 7 >>
+ 2/3                  < 2.0 >
+ 1/3                  < 1.0 >
+ 2/5                  1.0 2.0 3.0 0.0
+ 3/10                 1.0 2.0 0.0 4.0
+ 1/5                  1.0 0.0 3.0 4.0
+ 1/10                 0.0 2.0 3.0 4.0
+ 1/4                  0.0 2.0 3.0 4.0
+ 1/4                  1.0 0.0 3.0 4.0
+ 1/4                  1.0 2.0 0.0 4.0
+ 1/4                  1.0 2.0 3.0 0.0

test/pcheck/sample_storm.expected

@@ -0,0 +1,22 @@
+ 9/10                 < 1.0 >
+ 1/10                 < 0.0 >
+ 1/3                  << 1 >>
+ 1/3                  << 2 >>
+ 1/3                  << 3 >>
+ 1/7                  << 1 >>
+ 1/7                  << 2 >>
+ 1/7                  << 3 >>
+ 1/7                  << 4 >>
+ 1/7                  << 5 >>
+ 1/7                  << 6 >>
+ 1/7                  << 7 >>
+ 2/3                  < 2.0 >
+ 1/3                  < 1.0 >
+ 2/5                  1.0 2.0 3.0 0.0
+ 3/10                 1.0 2.0 0.0 4.0
+ 1/5                  1.0 0.0 3.0 4.0
+ 1/10                 0.0 2.0 3.0 4.0
+ 1/4                  0.0 2.0 3.0 4.0
+ 1/4                  1.0 0.0 3.0 4.0
+ 1/4                  1.0 2.0 0.0 4.0
+ 1/4                  1.0 2.0 3.0 0.0

umaudemc/__init__.py

@@ -1 +1 @@
-__version__ = '0.13.1'
+__version__ = '0.14.0'

umaudemc/backend/_stormpy.py

@@ -80,7 +80,7 @@ def _build_dtmc(self, builder, graph, ctmc):
 			builder.add_next_value(row=st, column=st, value=1.0)
 
 	def _build_mdp(self, builder, graph):
-		"""Build an MDP from the probabilsitic rewrite graph"""
+		"""Build an MDP from the probabilistic rewrite graph"""
 
 		last_visited, row_index, num_states = -1, 0, len(graph)
 
@@ -127,7 +127,6 @@ def _build_model(self, graph, aprops, aprop_labels, reward, ctmc):
 			self._build_mdp(builder, graph)
 
 		transition_matrix = builder.build()
-		#input(transition_matrix)
 
 		# State labeling with atomic propositions
 		state_labeling = stormpy.storage.StateLabeling(num_states)
@@ -233,7 +232,7 @@ def check(self, graph=None, module=None, formula=None, formula_str=None,
 	def state_analysis(self, *args, **kwargs):
 		"""Steady and transient state analysis"""
 
-		# StormPy does not allow calculting state probabilities, as far as we know, so
+		# StormPy does not allow calculating state probabilities, as far as we know, so
 		# we delegate on the command-line interface to Storm
 		from ._storm import StormBackend as StormCmdLineBackend
 

umaudemc/backend/bmcalc.py

@@ -479,22 +479,22 @@ def ctl2mucalc(self, formula, universal=True, index=0):
 			return [modop, self.ctl2mucalc(rest[0], index=index)]
 		elif head == '_U_':
 			return ['mu_._', ['Var', f'Z{index}'], ['_\\/_',
-				  self.ctl2mucalc(rest[1], index=index + 1),
-				  ['_/\\_', self.ctl2mucalc(rest[0], index=index + 1),
-				  [modop, ['Var', f'Z{index}']]]]]
+			                                        self.ctl2mucalc(rest[1], index=index + 1),
+			                                        ['_/\\_', self.ctl2mucalc(rest[0], index=index + 1),
+			                                         [modop, ['Var', f'Z{index}']]]]]
 		elif head == '_R_':
 			return ['nu_._', ['Var', f'Z{index}'], ['_/\\_',
-				  self.ctl2mucalc(rest[1], index=index + 1),
-				  ['_\\/_', self.ctl2mucalc(rest[0], index=index + 1),
-				  [modop, ['Var', f'Z{index}']]]]]
+			                                        self.ctl2mucalc(rest[1], index=index + 1),
+			                                        ['_\\/_', self.ctl2mucalc(rest[0], index=index + 1),
+			                                         [modop, ['Var', f'Z{index}']]]]]
 		elif head == '`[`]_':
 			return ['nu_._', ['Var', f'Z{index}'], ['_/\\_',
-				  self.ctl2mucalc(rest[0], index=index + 1),
-				  [modop, ['Var', f'Z{index}']]]]
+			                                        self.ctl2mucalc(rest[0], index=index + 1),
+			                                        [modop, ['Var', f'Z{index}']]]]
 		elif head == '<>_':
 			return ['mu_._', ['Var', f'Z{index}'], ['_\\/_',
-				  self.ctl2mucalc(rest[0], index=index + 1),
-				  [modop, ['Var', f'Z{index}']]]]
+			                                        self.ctl2mucalc(rest[0], index=index + 1),
+			                                        [modop, ['Var', f'Z{index}']]]]
 		else:
 			return [head] + [self.ctl2mucalc(arg, index=index) for arg in rest]
 

umaudemc/backend/ltsmin.py

@@ -552,7 +552,7 @@ def run(self, filename, initial, strategy, biased_matchrew=True, opaque_strats=(
 		maude_lib_ltsmin = os.getenv('MAUDE_LIB_LTSMIN')
 		new_maude_lib = os.getenv('MAUDE_LIB', '') if maude_lib_ltsmin is None else maude_lib_ltsmin
 		new_maude_lib = ('' if new_maude_lib == '' else new_maude_lib + os.pathsep) \
-		                + os.path.dirname(filename)
+		                 + os.path.dirname(filename)
 
 		if raw:
 			os.execve(self.ltsmin.pins2lts[variant], [self.ltsmin.pins2lts[variant]] + args,

umaudemc/command/check.py

@@ -8,7 +8,7 @@
 import tempfile
 
 from ..common import parse_initial_data, usermsgs
-from ..backends import kleene_backends, get_backends, backend_for, format_statistics,\
+from ..backends import kleene_backends, get_backends, backend_for, format_statistics, \
 	advance_counterexample, advance_kleene
 from ..counterprint import SimplePrinter, JSONPrinter, HTMLPrinter, DOTPrinter, print_counterexample
 from ..formulae import Parser, collect_aprops, add_path_premise, formula_list2str

umaudemc/command/graph.py

@@ -71,7 +71,7 @@ def deduce_format(args):
 		usermsgs.print_warning('PDF output is only supported with DOT. Changing to DOT.')
 		return 'dot'
 
-	# Probabilitic information is not considered in some cases
+	# Probabilistic information is not considered in some cases
 	if args.passign and oformat not in ('dot', 'prism', 'jani', 'default'):
 		usermsgs.print_warning('Probabilistic graphs are only supported with PRISM, JANI and DOT output. '
 		                       'Ignoring probabilities.')
@@ -107,7 +107,6 @@ def graph(args):
 		else:
 			kleene_graph = True
 
-
 	# Select the appropriate rewriting graph
 	# (probabilistic, strategy-controlled, or standard)
 	if args.passign or oformat in ('prism', 'jani'):

umaudemc/command/pcheck.py

@@ -50,6 +50,7 @@ def _print_fraction(value):
 
 	return f'{num}/{den}' if num > 0 and den != 1 else num
 
+
 def _select_backend(known_backends, backend_list):
 	"""Get the first available backend according to the user preferences"""
 
@@ -78,7 +79,6 @@ def _select_backend(known_backends, backend_list):
 		elif first_known is None:
 			first_known = name
 
-
 	if first_available is None:
 		if first_known is None:
 			usermsgs.print_error('The backend list does not contain any valid option.')

umaudemc/command/test.py

@@ -280,7 +280,7 @@ def _depends_on_vars(node, variables):
 
 
 class ParameterSet:
-	"""Assignement to parameters to be replaced on test attributes"""
+	"""Assignment to parameters to be replaced on test attributes"""
 
 	def __init__(self, dic, is_subs=None):
 		# Dictionary with the parameter assignments

umaudemc/common.py

@@ -18,7 +18,8 @@
 	usermsgs.print_warning('Version 1.0 of the maude package adds some useful features for this program.\n'
 	                       'Please update.')
 
-	maude.Term.getVarName = lambda self: str(self).split(':')[0] if self.symbol() == self.symbol().getModule().parseTerm(f'$$$:{self.getSort()}').symbol() else None
+	maude.Term.getVarName = lambda self: str(self).split(':')[0] if self.symbol() == \
+		self.symbol().getModule().parseTerm(f'$$$:{self.getSort()}').symbol() else None
 	maude.Term.isVariable = lambda self: self.getVarName() is None
 
 

umaudemc/data/select.htm

@@ -85,7 +85,7 @@
 				<option value="metadata">Weighted by metadata</option>
 				<option value="strategy">Probabilistic strategy</option>
 			</select>
-			<input type="checkbox" id="mdp" style="margin-left: 1.5ex; display: none;"></input>
+			<input type="checkbox" id="mdp" style="margin-left: 1.5ex; display: none;"/>
 			<label for="mdp" style="display: none;">MDP</label>
 			<label for="parg" style="margin-left: 1.5ex; display: none;">Weight term:</label>
 			<input type="text" id="parg" style="flex-grow: 1; display: none;" onchange="buttonToggle()"

umaudemc/formatter.py

@@ -19,7 +19,7 @@ def apply_state_format(graph, index, sformat, terms, use_term=False, use_strat=F
 	:type sformat: str
 	:param terms: Term patterns to appear in the format string.
 	:type terms: list of string
-	:param use_term: Whether the term is actually used (only for effiency).
+	:param use_term: Whether the term is actually used (only for efficiency).
 	:type use_term: bool
 	:param use_strat: Whether the strategy is actually used (only for effiency).
 	:type use_strat: bool

umaudemc/opsem.py

@@ -65,7 +65,7 @@ def _load_values(self):
 
 	@classmethod
 	def get_instantiation(cls, module, metamodule=None, semantics_module=None, preds_module=None):
-		"""Get the Maude code to instantiate the sematnics for the given problem"""
+		"""Get the Maude code to instantiate the semantics for the given problem"""
 
 		# Use the default semantics and predicates module if not specified
 		if semantics_module is None:

umaudemc/probabilistic.py

@@ -714,7 +714,7 @@ def expand(self):
 			edges = []
 
 			for child, subs, ctx, rl in term.apply(None):
-				# Term.apply do not reduce the terms itself
+				# Term.apply does not reduce the terms itself
 				self.rewrite_count += 1 + child.reduce()
 				index = self.term_map.get(child)