From 973fdd04ff0ef93a3d16ac928b569ea7db4f9edc Mon Sep 17 00:00:00 2001 From: ningit Date: Fri, 3 Jan 2025 12:00:00 +0100 Subject: [PATCH] Probabilistic model checking with sample and discrete distributions and other changes --- README.md | 2 +- pyproject.toml | 4 +- test/api/apitest.py | 2 +- test/pcheck/sample.maude | 38 ++++++ test/pcheck/sample.test | 10 ++ test/pcheck/sample_prism.expected | 22 ++++ test/pcheck/sample_storm.expected | 22 ++++ umaudemc/__init__.py | 2 +- umaudemc/backend/_stormpy.py | 5 +- umaudemc/backend/bmcalc.py | 20 ++-- umaudemc/backend/ltsmin.py | 2 +- umaudemc/command/check.py | 2 +- umaudemc/command/graph.py | 3 +- umaudemc/command/pcheck.py | 2 +- umaudemc/command/test.py | 2 +- umaudemc/common.py | 3 +- umaudemc/data/select.htm | 2 +- umaudemc/formatter.py | 2 +- umaudemc/opsem.py | 2 +- umaudemc/probabilistic.py | 2 +- umaudemc/pyslang.py | 187 +++++++++++++++++++++++------- umaudemc/quatex.py | 4 +- umaudemc/resources.py | 38 ++---- umaudemc/statistical.py | 4 +- umaudemc/webui.py | 2 +- 25 files changed, 279 insertions(+), 105 deletions(-) create mode 100644 test/pcheck/sample.maude create mode 100644 test/pcheck/sample.test create mode 100644 test/pcheck/sample_prism.expected create mode 100644 test/pcheck/sample_storm.expected diff --git a/README.md b/README.md index c96c927..f37538b 100644 --- a/README.md +++ b/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 diff --git a/pyproject.toml b/pyproject.toml index 3806bec..ca05f54 100644 --- a/pyproject.toml +++ b/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]] diff --git a/test/api/apitest.py b/test/api/apitest.py index 2ad20f7..00e20c4 100644 --- a/test/api/apitest.py +++ b/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') diff --git a/test/pcheck/sample.maude b/test/pcheck/sample.maude new file mode 100644 index 0000000..9672916 --- /dev/null +++ b/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 diff --git a/test/pcheck/sample.test b/test/pcheck/sample.test new file mode 100644 index 0000000..02fb7db --- /dev/null +++ b/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 diff --git a/test/pcheck/sample_prism.expected b/test/pcheck/sample_prism.expected new file mode 100644 index 0000000..86a9da3 --- /dev/null +++ b/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 diff --git a/test/pcheck/sample_storm.expected b/test/pcheck/sample_storm.expected new file mode 100644 index 0000000..86a9da3 --- /dev/null +++ b/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 diff --git a/umaudemc/__init__.py b/umaudemc/__init__.py index deea98b..ef91994 100644 --- a/umaudemc/__init__.py +++ b/umaudemc/__init__.py @@ -1 +1 @@ -__version__ = '0.13.1' +__version__ = '0.14.0' diff --git a/umaudemc/backend/_stormpy.py b/umaudemc/backend/_stormpy.py index 0076de7..81bd61a 100644 --- a/umaudemc/backend/_stormpy.py +++ b/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 diff --git a/umaudemc/backend/bmcalc.py b/umaudemc/backend/bmcalc.py index 61bd6d1..ec05e15 100644 --- a/umaudemc/backend/bmcalc.py +++ b/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] diff --git a/umaudemc/backend/ltsmin.py b/umaudemc/backend/ltsmin.py index cbad6b4..3fb84cc 100644 --- a/umaudemc/backend/ltsmin.py +++ b/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, diff --git a/umaudemc/command/check.py b/umaudemc/command/check.py index c442ff3..ad1cf9d 100644 --- a/umaudemc/command/check.py +++ b/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 diff --git a/umaudemc/command/graph.py b/umaudemc/command/graph.py index 4a644c7..cdeabfc 100644 --- a/umaudemc/command/graph.py +++ b/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'): diff --git a/umaudemc/command/pcheck.py b/umaudemc/command/pcheck.py index d53b994..9f3cfec 100644 --- a/umaudemc/command/pcheck.py +++ b/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.') diff --git a/umaudemc/command/test.py b/umaudemc/command/test.py index 508e22e..6fe36c8 100644 --- a/umaudemc/command/test.py +++ b/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 diff --git a/umaudemc/common.py b/umaudemc/common.py index 7c167f2..5ab7508 100644 --- a/umaudemc/common.py +++ b/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 diff --git a/umaudemc/data/select.htm b/umaudemc/data/select.htm index 9fc2421..233b840 100644 --- a/umaudemc/data/select.htm +++ b/umaudemc/data/select.htm @@ -85,7 +85,7 @@ - + = (3, 9): - - def get_resource_path(name): - """Get a temporary filename for a given named resource""" - return pkg_resources.as_file(pkg_resources.files(data) / name) +# Root for static resources +_DATA_ROOT = pkg_resources.files(data) - def get_resource_content(name): - """Get the string content of a given named resource""" - return (pkg_resources.files(data) / name).read_text() - def get_resource_binary(name): - """Get the string content of a given named resource""" - return (pkg_resources.files(data) / name).read_bytes() +def get_resource_path(name): + """Get a temporary filename for a given named resource""" + return pkg_resources.as_file(_DATA_ROOT / name) -# For compatibility with Python 3.8 -else: - def get_resource_path(name): - """Get a temporary filename for a given named resource""" - return pkg_resources.path(data, name) +def get_resource_content(name): + """Get the string content of a given named resource""" + return (_DATA_ROOT / name).read_text() - def get_resource_content(name): - """Get the string content of a given named resource""" - return pkg_resources.read_text(data, name) +def get_resource_binary(name): + """Get the string content of a given named resource""" + return (_DATA_ROOT / name).read_bytes() - def get_resource_binary(name): - """Get the string content of a given named resource""" - return pkg_resources.read_binary(data, name) def get_templog(): """Get a temporary filename for the templog Maude file""" diff --git a/umaudemc/statistical.py b/umaudemc/statistical.py index 069cc0b..01fb286 100644 --- a/umaudemc/statistical.py +++ b/umaudemc/statistical.py @@ -233,7 +233,7 @@ def run_parallel(program, qdata, num_sims, max_sim, simulator, alpha, delta, blo # Process communication stuff # Random number seeds - seeds = [random.randint(0, 1e6) for _ in range(jobs)] + seeds = [random.getrandbits(20) for _ in range(jobs)] # Queue for transferring the query evaluations queue = mp.Queue() barrier = mp.Barrier(jobs + 1) @@ -329,7 +329,7 @@ def check(program, simulator, seed, alpha, delta, block, min_sim, max_sim, jobs, for idict in make_parameter_dicts(qinfo[2])] # Run the simulations - if jobs == 1: + if jobs == 1 and num_sims != 1: return run_single(program, qdata, num_sims, max_sim, simulator, alpha, delta, block, verbose=verbose) else: diff --git a/umaudemc/webui.py b/umaudemc/webui.py index 2e839b6..dd30ab3 100644 --- a/umaudemc/webui.py +++ b/umaudemc/webui.py @@ -142,7 +142,7 @@ def browse_dir(self, path): class ConnectionInfo: - """Persisent server information""" + """Persistent server information""" def __init__(self): self.path_handler = WinPathHandler() if sys.platform == 'win32' else PathHandler()