From ef6a53bb2da20351a7a0a52a1d4df93fbd9a527f Mon Sep 17 00:00:00 2001 From: ningit Date: Fri, 5 Jan 2024 12:00:00 +0100 Subject: [PATCH] Kleene-star graph with the builtin implementation, removed Gtk UI, minor changes --- pyproject.toml | 2 +- test/check/ctl_nusmv.expected | 6 +- test/check/kleene_maude.expected | 14 +- test/check/kleene_spot.expected | 14 +- test/check/ltl_maude.expected | 18 +- test/check/ltl_nusmv.expected | 18 +- test/check/ltl_spot.expected | 18 +- test/graph/dot.expected | 14 +- test/pcheck/formula_prism.expected | 4 +- test/pcheck/formula_storm.expected | 4 +- umaudemc/__main__.py | 5 + umaudemc/api.py | 2 +- umaudemc/backend/_spot.py | 15 +- umaudemc/command/graph.py | 32 +- umaudemc/common.py | 24 -- umaudemc/counterprint.py | 16 +- umaudemc/data/smcview.js | 71 ++-- umaudemc/formatter.py | 45 +-- umaudemc/grapher.py | 11 +- umaudemc/gtk.py | 587 +++++------------------------ umaudemc/kleene.py | 156 ++++++++ umaudemc/opsem.py | 2 +- umaudemc/probabilistic.py | 21 +- umaudemc/pyslang.py | 506 ++++++++++++++++--------- umaudemc/webui.py | 64 ++-- umaudemc/wrappers.py | 46 ++- 26 files changed, 831 insertions(+), 884 deletions(-) create mode 100644 umaudemc/kleene.py diff --git a/pyproject.toml b/pyproject.toml index fedc692..fe119d5 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -1,6 +1,6 @@ [project] name = 'umaudemc' -version = '0.12.2' +version = '0.13.0' description = 'Unified Maude model-checking utility' license.text = 'GPLv3' classifiers = [ diff --git a/test/check/ctl_nusmv.expected b/test/check/ctl_nusmv.expected index 07ad2a0..9637627 100644 --- a/test/check/ctl_nusmv.expected +++ b/test/check/ctl_nusmv.expected @@ -4,14 +4,14 @@ The property is satisfied in the initial state (5 system states, 11 rewrites) The property is satisfied in the initial state (5 system states, 10 rewrites) The property is not satisfied in the initial state (6 system states, 12 rewrites) | e e [empty] -∨ rl e O:Soup [I:Soup] => O:Soup [e I:Soup] [label put1] . +∨ rl [put1] : e O:Soup [I:Soup] => O:Soup [e I:Soup] . O e [e] The property is satisfied in the initial state (5 system states, 10 rewrites) The property is not satisfied in the initial state (3 system states, 9 rewrites) | e e [empty] -∨ rl e O:Soup [I:Soup] => O:Soup [e I:Soup] [label put1] . +∨ rl [put1] : e O:Soup [I:Soup] => O:Soup [e I:Soup] . O e [e] The property is not satisfied in the initial state (5 system states, 11 rewrites) | e e [empty] -∨ rl e O:Soup [I:Soup] => O:Soup [e I:Soup] [label put1] . +∨ rl [put1] : e O:Soup [I:Soup] => O:Soup [e I:Soup] . O e [e] diff --git a/test/check/kleene_maude.expected b/test/check/kleene_maude.expected index 967df84..91c0a08 100644 --- a/test/check/kleene_maude.expected +++ b/test/check/kleene_maude.expected @@ -1,18 +1,18 @@ The property is not satisfied in the initial state (16 system states, 43 rewrites, 2 Büchi states) | nothing ball nothing -∨ rl B?:MaybeBall => cup(B?:MaybeBall) [label cover] . +∨ rl [cover] : B?:MaybeBall => cup(B?:MaybeBall) . | cup(nothing) ball nothing -∨ rl B?:MaybeBall => cup(B?:MaybeBall) [label cover] . +∨ rl [cover] : B?:MaybeBall => cup(B?:MaybeBall) . | cup(nothing) cup(ball) nothing -∨ rl B?:MaybeBall => cup(B?:MaybeBall) [label cover] . +∨ rl [cover] : B?:MaybeBall => cup(B?:MaybeBall) . | cup(nothing) cup(ball) cup(nothing) -∨ rl cup(B1?:MaybeBall) T:Table cup(B2?:MaybeBall) => cup(B2?:MaybeBall) T:Table cup(B1?:MaybeBall) [label swap] . +∨ rl [swap] : cup(B1?:MaybeBall) T:Table cup(B2?:MaybeBall) => cup(B2?:MaybeBall) T:Table cup(B1?:MaybeBall) . | cup(ball) cup(nothing) cup(nothing) -∨ rl cup(B1?:MaybeBall) T:Table cup(B2?:MaybeBall) => cup(B2?:MaybeBall) T:Table cup(B1?:MaybeBall) [label swap] . +∨ rl [swap] : cup(B1?:MaybeBall) T:Table cup(B2?:MaybeBall) => cup(B2?:MaybeBall) T:Table cup(B1?:MaybeBall) . | cup(nothing) cup(ball) cup(nothing) -∨ rl cup(B1?:MaybeBall) T:Table cup(B2?:MaybeBall) => cup(B2?:MaybeBall) T:Table cup(B1?:MaybeBall) [label swap] . +∨ rl [swap] : cup(B1?:MaybeBall) T:Table cup(B2?:MaybeBall) => cup(B2?:MaybeBall) T:Table cup(B1?:MaybeBall) . | | cup(nothing) cup(nothing) cup(ball) -| ∨ rl cup(B1?:MaybeBall) T:Table cup(B2?:MaybeBall) => cup(B2?:MaybeBall) T:Table cup(B1?:MaybeBall) [label swap] . +| ∨ rl [swap] : cup(B1?:MaybeBall) T:Table cup(B2?:MaybeBall) => cup(B2?:MaybeBall) T:Table cup(B1?:MaybeBall) . < ∨ The property is satisfied in the initial state (48 system states, 13609 rewrites, 22 Büchi states) The property is satisfied in the initial state (48 system states, 13609 rewrites, 22 Büchi states) diff --git a/test/check/kleene_spot.expected b/test/check/kleene_spot.expected index 7769da3..8604142 100644 --- a/test/check/kleene_spot.expected +++ b/test/check/kleene_spot.expected @@ -1,14 +1,14 @@ The property is not satisfied in the initial state (22 system states, 71 rewrites, 2 Büchi states) | nothing ball nothing -∨ rl B?:MaybeBall => cup(B?:MaybeBall) [label cover] . +∨ rl [cover] : B?:MaybeBall => cup(B?:MaybeBall) . | cup(nothing) ball nothing -∨ rl B?:MaybeBall => cup(B?:MaybeBall) [label cover] . +∨ rl [cover] : B?:MaybeBall => cup(B?:MaybeBall) . | cup(nothing) cup(ball) nothing -∨ rl B?:MaybeBall => cup(B?:MaybeBall) [label cover] . +∨ rl [cover] : B?:MaybeBall => cup(B?:MaybeBall) . | cup(nothing) cup(ball) cup(nothing) -∨ rl cup(B1?:MaybeBall) T:Table cup(B2?:MaybeBall) => cup(B2?:MaybeBall) T:Table cup(B1?:MaybeBall) [label swap] . +∨ rl [swap] : cup(B1?:MaybeBall) T:Table cup(B2?:MaybeBall) => cup(B2?:MaybeBall) T:Table cup(B1?:MaybeBall) . | | cup(nothing) cup(nothing) cup(ball) -| ∨ rl cup(B1?:MaybeBall) T:Table cup(B2?:MaybeBall) => cup(B2?:MaybeBall) T:Table cup(B1?:MaybeBall) [label swap] . +| ∨ rl [swap] : cup(B1?:MaybeBall) T:Table cup(B2?:MaybeBall) => cup(B2?:MaybeBall) T:Table cup(B1?:MaybeBall) . < ∨ -The property is satisfied in the initial state (48 system states, 12944 rewrites, 2 Büchi states) -The property is satisfied in the initial state (48 system states, 12944 rewrites, 2 Büchi states) +The property is satisfied in the initial state (23 system states, 126 rewrites, 2 Büchi states) +The property is satisfied in the initial state (23 system states, 126 rewrites, 2 Büchi states) diff --git a/test/check/ltl_maude.expected b/test/check/ltl_maude.expected index 0b1cae6..644a22d 100644 --- a/test/check/ltl_maude.expected +++ b/test/check/ltl_maude.expected @@ -1,29 +1,29 @@ The property is not satisfied in the initial state (5 system states, 13 rewrites, 1 Büchi state) | e e [empty] -∨ rl e O:Soup [I:Soup] => O:Soup [e I:Soup] [label put1] . +∨ rl [put1] : e O:Soup [I:Soup] => O:Soup [e I:Soup] . | e [e] -∨ rl e O:Soup [I:Soup] => O:Soup [e I:Soup] [label put1] . +∨ rl [put1] : e O:Soup [I:Soup] => O:Soup [e I:Soup] . | empty [e e] -∨ rl O:Soup [e I:Soup] => a O:Soup [I:Soup] [label apple] . +∨ rl [apple] : O:Soup [e I:Soup] => a O:Soup [I:Soup] . | a [e] -∨ rl O:Soup [e I:Soup] => a O:Soup [I:Soup] [label apple] . +∨ rl [apple] : O:Soup [e I:Soup] => a O:Soup [I:Soup] . X a a [empty] The property is not satisfied in the initial state (6 system states, 16 rewrites, 2 Büchi states) | e e [empty] -∨ rl e O:Soup [I:Soup] => O:Soup [e I:Soup] [label put1] . +∨ rl [put1] : e O:Soup [I:Soup] => O:Soup [e I:Soup] . | e [e] -∨ rl e O:Soup [I:Soup] => O:Soup [e I:Soup] [label put1] . +∨ rl [put1] : e O:Soup [I:Soup] => O:Soup [e I:Soup] . | empty [e e] -∨ rl O:Soup [e e I:Soup] => c O:Soup [I:Soup] [label cake] . +∨ rl [cake] : O:Soup [e e I:Soup] => c O:Soup [I:Soup] . X c [empty] The property is satisfied in the initial state (7 system states, 29 rewrites, 3 Büchi states) The property is not satisfied in the initial state (3 system states, 9 rewrites, 1 Büchi state) | e e [empty] | @ put1 ; apple | put1 ; put1 ; cake -∨ rl e O:Soup [I:Soup] => O:Soup [e I:Soup] [label put1] . +∨ rl [put1] : e O:Soup [I:Soup] => O:Soup [e I:Soup] . | e [e] | @ apple -∨ rl O:Soup [e I:Soup] => a O:Soup [I:Soup] [label apple] . +∨ rl [apple] : O:Soup [e I:Soup] => a O:Soup [I:Soup] . X e a [empty] The property is not satisfied in the initial state (6 system states, 15 rewrites, 2 Büchi states) | e e [empty] @ put1 ; apple | put1 ; put1 ; cake diff --git a/test/check/ltl_nusmv.expected b/test/check/ltl_nusmv.expected index d731a83..259ea1a 100644 --- a/test/check/ltl_nusmv.expected +++ b/test/check/ltl_nusmv.expected @@ -1,29 +1,29 @@ The property is not satisfied in the initial state (7 system states, 15 rewrites) | e e [empty] -∨ rl e O:Soup [I:Soup] => O:Soup [e I:Soup] [label put1] . +∨ rl [put1] : e O:Soup [I:Soup] => O:Soup [e I:Soup] . | e [e] -∨ rl O:Soup [e I:Soup] => a O:Soup [I:Soup] [label apple] . +∨ rl [apple] : O:Soup [e I:Soup] => a O:Soup [I:Soup] . | e a [empty] -∨ rl e O:Soup [I:Soup] => O:Soup [e I:Soup] [label put1] . +∨ rl [put1] : e O:Soup [I:Soup] => O:Soup [e I:Soup] . | a [e] -∨ rl O:Soup [e I:Soup] => a O:Soup [I:Soup] [label apple] . +∨ rl [apple] : O:Soup [e I:Soup] => a O:Soup [I:Soup] . X a a [empty] The property is not satisfied in the initial state (7 system states, 15 rewrites) | e e [empty] -∨ rl e O:Soup [I:Soup] => O:Soup [e I:Soup] [label put1] . +∨ rl [put1] : e O:Soup [I:Soup] => O:Soup [e I:Soup] . | e [e] -∨ rl e O:Soup [I:Soup] => O:Soup [e I:Soup] [label put1] . +∨ rl [put1] : e O:Soup [I:Soup] => O:Soup [e I:Soup] . | empty [e e] -∨ rl O:Soup [e e I:Soup] => c O:Soup [I:Soup] [label cake] . +∨ rl [cake] : O:Soup [e e I:Soup] => c O:Soup [I:Soup] . X c [empty] The property is satisfied in the initial state (7 system states, 15 rewrites) The property is not satisfied in the initial state (6 system states, 12 rewrites) | e e [empty] | @ put1 ; apple | put1 ; put1 ; cake -∨ rl e O:Soup [I:Soup] => O:Soup [e I:Soup] [label put1] . +∨ rl [put1] : e O:Soup [I:Soup] => O:Soup [e I:Soup] . | e [e] | @ apple -∨ rl O:Soup [e I:Soup] => a O:Soup [I:Soup] [label apple] . +∨ rl [apple] : O:Soup [e I:Soup] => a O:Soup [I:Soup] . X e a [empty] The property is not satisfied in the initial state (6 system states, 12 rewrites) | e e [empty] @ put1 ; apple | put1 ; put1 ; cake diff --git a/test/check/ltl_spot.expected b/test/check/ltl_spot.expected index c269dba..f60baa9 100644 --- a/test/check/ltl_spot.expected +++ b/test/check/ltl_spot.expected @@ -1,29 +1,29 @@ The property is not satisfied in the initial state (7 system states, 15 rewrites, 1 Büchi state) | e e [empty] -∨ rl e O:Soup [I:Soup] => O:Soup [e I:Soup] [label put1] . +∨ rl [put1] : e O:Soup [I:Soup] => O:Soup [e I:Soup] . | e [e] -∨ rl e O:Soup [I:Soup] => O:Soup [e I:Soup] [label put1] . +∨ rl [put1] : e O:Soup [I:Soup] => O:Soup [e I:Soup] . | empty [e e] -∨ rl O:Soup [e I:Soup] => a O:Soup [I:Soup] [label apple] . +∨ rl [apple] : O:Soup [e I:Soup] => a O:Soup [I:Soup] . | a [e] -∨ rl O:Soup [e I:Soup] => a O:Soup [I:Soup] [label apple] . +∨ rl [apple] : O:Soup [e I:Soup] => a O:Soup [I:Soup] . X a a [empty] The property is not satisfied in the initial state (7 system states, 15 rewrites, 2 Büchi states) | e e [empty] -∨ rl e O:Soup [I:Soup] => O:Soup [e I:Soup] [label put1] . +∨ rl [put1] : e O:Soup [I:Soup] => O:Soup [e I:Soup] . | e [e] -∨ rl e O:Soup [I:Soup] => O:Soup [e I:Soup] [label put1] . +∨ rl [put1] : e O:Soup [I:Soup] => O:Soup [e I:Soup] . | empty [e e] -∨ rl O:Soup [e e I:Soup] => c O:Soup [I:Soup] [label cake] . +∨ rl [cake] : O:Soup [e e I:Soup] => c O:Soup [I:Soup] . X c [empty] The property is satisfied in the initial state (7 system states, 15 rewrites, 2 Büchi states) The property is not satisfied in the initial state (6 system states, 12 rewrites, 1 Büchi state) | e e [empty] | @ put1 ; apple | put1 ; put1 ; cake -∨ rl e O:Soup [I:Soup] => O:Soup [e I:Soup] [label put1] . +∨ rl [put1] : e O:Soup [I:Soup] => O:Soup [e I:Soup] . | e [e] | @ apple -∨ rl O:Soup [e I:Soup] => a O:Soup [I:Soup] [label apple] . +∨ rl [apple] : O:Soup [e I:Soup] => a O:Soup [I:Soup] . X e a [empty] The property is not satisfied in the initial state (6 system states, 12 rewrites, 2 Büchi states) | e e [empty] @ put1 ; apple | put1 ; put1 ; cake diff --git a/test/graph/dot.expected b/test/graph/dot.expected index 6ecb305..9558019 100644 --- a/test/graph/dot.expected +++ b/test/graph/dot.expected @@ -130,19 +130,19 @@ digraph { } digraph { 0 [label="0"]; - 0 -> 1 [label="rl e O:Soup [I:Soup] => O:Soup [e I:Soup] [label put1] ."]; + 0 -> 1 [label="rl [put1] : e O:Soup [I:Soup] => O:Soup [e I:Soup] ."]; 1 [label="1"]; - 1 -> 2 [label="rl e O:Soup [I:Soup] => O:Soup [e I:Soup] [label put1] ."]; + 1 -> 2 [label="rl [put1] : e O:Soup [I:Soup] => O:Soup [e I:Soup] ."]; 2 [label="2"]; - 2 -> 3 [label="rl O:Soup [e I:Soup] => a O:Soup [I:Soup] [label apple] ."]; + 2 -> 3 [label="rl [apple] : O:Soup [e I:Soup] => a O:Soup [I:Soup] ."]; 3 [label="3"]; - 3 -> 4 [label="rl O:Soup [e I:Soup] => a O:Soup [I:Soup] [label apple] ."]; + 3 -> 4 [label="rl [apple] : O:Soup [e I:Soup] => a O:Soup [I:Soup] ."]; 4 [label="4"]; - 2 -> 5 [label="rl O:Soup [e e I:Soup] => c O:Soup [I:Soup] [label cake] ."]; + 2 -> 5 [label="rl [cake] : O:Soup [e e I:Soup] => c O:Soup [I:Soup] ."]; 5 [label="5"]; - 1 -> 6 [label="rl O:Soup [e I:Soup] => a O:Soup [I:Soup] [label apple] ."]; + 1 -> 6 [label="rl [apple] : O:Soup [e I:Soup] => a O:Soup [I:Soup] ."]; 6 [label="6"]; - 6 -> 3 [label="rl e O:Soup [I:Soup] => O:Soup [e I:Soup] [label put1] ."]; + 6 -> 3 [label="rl [put1] : e O:Soup [I:Soup] => O:Soup [e I:Soup] ."]; } digraph { 0 [label="e e [empty] @ alpha "]; diff --git a/test/pcheck/formula_prism.expected b/test/pcheck/formula_prism.expected index b7b30d9..cbfb5e9 100644 --- a/test/pcheck/formula_prism.expected +++ b/test/pcheck/formula_prism.expected @@ -18,12 +18,12 @@ Result: 0.9826584700841672 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). +The property is not satisfied (3 system states, 8 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). +The property is not satisfied (5 system states, 16 rewrites). The property is not satisfied (2 system states, 8 rewrites). Result: 0.875 diff --git a/test/pcheck/formula_storm.expected b/test/pcheck/formula_storm.expected index b7b30d9..cbfb5e9 100644 --- a/test/pcheck/formula_storm.expected +++ b/test/pcheck/formula_storm.expected @@ -18,12 +18,12 @@ Result: 0.9826584700841672 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). +The property is not satisfied (3 system states, 8 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). +The property is not satisfied (5 system states, 16 rewrites). The property is not satisfied (2 system states, 8 rewrites). Result: 0.875 diff --git a/umaudemc/__main__.py b/umaudemc/__main__.py index 1182fca..bd157c6 100644 --- a/umaudemc/__main__.py +++ b/umaudemc/__main__.py @@ -206,6 +206,11 @@ def build_parser(): help='probability assignment method for adding them to the graph', metavar='METHOD' ) + parser_graph.add_argument( + '-k', '--kleene-iteration', + help='write annotations on the transitions starting and terminating an iteration', + action='store_true' + ) parser_graph.set_defaults(mode='graph') # diff --git a/umaudemc/api.py b/umaudemc/api.py index cc18072..53a921c 100644 --- a/umaudemc/api.py +++ b/umaudemc/api.py @@ -297,7 +297,7 @@ def check(self, formula, purge_fails='default', merge_states='default', wgraph = _wrappers.BoundedGraph(self.graph, depth) if depth > 0 else self.graph # Create and store the wrapped graph - wgraph = _wrappers.wrapGraph(wgraph, purge, merge) + wgraph = _wrappers.wrap_graph(wgraph, purge, merge) self.wgraphs[(purge, merge, depth > 0)] = wgraph # In case both purge and merge are used, we keep the purged diff --git a/umaudemc/backend/_spot.py b/umaudemc/backend/_spot.py index f6eb3f3..39a71d7 100644 --- a/umaudemc/backend/_spot.py +++ b/umaudemc/backend/_spot.py @@ -8,7 +8,6 @@ import spot from ..formulae import collect_aprops -from ..opsem import OpSemKleeneInstance, OpSemGraph from ..wrappers import create_graph @@ -136,9 +135,10 @@ class KleeneModelBuilder(SpotModelBuilder): """Generator of ω-automata for strategy-controlled models with an iteration like the Kleene star""" def __init__(self, module, initial, strategy, aprops, bdd_dict, metamodule=None, opaques=()): - self.instance = OpSemKleeneInstance.make_instance(module, metamodule) + from ..kleene import get_kleene_graph_mts - super().__init__(self.instance.make_graph(initial, strategy, opaques), aprops, bdd_dict) + # opaque strategies are ignored with the new implementation + super().__init__(get_kleene_graph_mts(module, initial, strategy), aprops, bdd_dict) # Table of distinct iterations (from their context to the index of # its accepting condition) @@ -166,7 +166,7 @@ def build(self): state = pending.pop() state_spot = self.state_map[state] - for next_state in self.graph.getNextStates(state): + for next_state, edge in self.graph.getTransitions(state): next_state_spot = self.state_map.get(next_state) if next_state_spot is None: @@ -175,10 +175,10 @@ def build(self): pending.append(next_state) # Check the iteration tags and set the accepting labels of the edges - next_state_term = self.instance.get_cterm(self.graph.getStateTerm(next_state)) + next_state_term = self.graph.getStateTerm(next_state) acc_set = [] - for tag, enter in self.instance.extract_tags(self.graph.getStateTerm(next_state)): + for tag, enter in edge.iterations: acc_index = self.iter_map.get(tag) if acc_index is None: @@ -299,7 +299,6 @@ def check(self, graph=None, module=None, metamodule_str=None, term=None, strateg stats['counterexample'] = model_builder.extract_counterexample(run, model_automaton) if get_graph: - stats['graph'] = model_builder.graph if not kleene_iteration \ - else OpSemGraph(model_builder.graph, model_builder.instance) + stats['graph'] = model_builder.graph return holds, stats diff --git a/umaudemc/command/graph.py b/umaudemc/command/graph.py index 75bc7b1..4a644c7 100644 --- a/umaudemc/command/graph.py +++ b/umaudemc/command/graph.py @@ -11,7 +11,7 @@ from ..common import maude, usermsgs, default_model_settings, parse_initial_data, split_comma from ..formatter import get_formatters from ..grapher import DOTGrapher, PDOTGrapher, TikZGrapher -from ..wrappers import wrapGraph +from ..wrappers import wrap_graph class ProcessStream: @@ -96,6 +96,18 @@ def graph(args): args.merge_states, args.strategy) + # Check the Kleene iteration flag + kleene_graph = False + + if args.kleene_iteration: + if not with_strategy: + usermsgs.print_warning('The --kleene-iteration flag should only be used with a strategy. Ignoring.') + elif args.passign: + usermsgs.print_warning('The --kleene-iteration flag cannot be used with probabilities. Ignoring.') + else: + kleene_graph = True + + # Select the appropriate rewriting graph # (probabilistic, strategy-controlled, or standard) if args.passign or oformat in ('prism', 'jani'): @@ -106,13 +118,18 @@ def graph(args): purge_fails=args.purge_fails, merge_states=args.merge_states) + elif kleene_graph: + from ..kleene import get_kleene_graph + rwgraph = get_kleene_graph(initial_data) + rwgraph = wrap_graph(rwgraph, purge_fails, merge_states) + elif not with_strategy: rwgraph = maude.RewriteGraph(initial_data.term) else: rwgraph = maude.StrategyRewriteGraph(initial_data.term, initial_data.strategy, initial_data.opaque, initial_data.full_matchrew) - rwgraph = wrapGraph(rwgraph, purge_fails, merge_states) + rwgraph = wrap_graph(rwgraph, purge_fails, merge_states) # If something has failed when creating the graph if rwgraph is None: @@ -129,8 +146,19 @@ def graph(args): else: aprops = [] + # State and edge labels slabel, elabel = get_formatters(args.slabel, args.elabel, with_strategy, only_labels=True) + if kleene_graph: + # Extend the label with the iteration flags + original_elabel = elabel + + def kleene_elabel(stmt): + iterations_txt = ''.join(f'{" +" if enter else " -"}{iid}' for iid, enter in stmt.iterations) + return f'{original_elabel(stmt)}{iterations_txt}' + + elabel = kleene_elabel + # Whether the graph should be seen as a CTMC and probabilities should not be normalized is_ctmc = args.passign and args.passign.startswith('ctmc-') diff --git a/umaudemc/common.py b/umaudemc/common.py index 159fadb..7c167f2 100644 --- a/umaudemc/common.py +++ b/umaudemc/common.py @@ -14,30 +14,6 @@ # Warn about old versions of the maude package installed # -if hasattr(maude, 'StateTransitionGraph'): - usermsgs.print_warning('Version 0.3 of the maude package contains bugs related to model checking.\n' - 'Please update.') - - # Anyhow, allow using it at their own risk, for which some adaptations are needed - maude.RewriteGraph = maude.StateTransitionGraph - maude.StrategyRewriteGraph = maude.StrategyTransitionGraph - - maude.Symbol.__call__ = lambda self, *args: self.makeTerm(args) - -if not hasattr(maude, 'Hook'): - usermsgs.print_warning('Version 0.5 of the maude package adds some useful features for this program.\n' - 'Please update.') - - maude.RewriteGraph.getNrRewrites = lambda: 0 - maude.StrategyRewriteGraph.getNrRewrites = lambda: 0 - maude.ModelCheckResult.nrBuchiStates = 0 - maude.downModule = lambda term: term.symbol().getModule().downModule(term) - maude.Sort.__le__ = lambda self, other: self.leq(other) - maude.Term.__eq__ = lambda self, other: self.equal(other) - -if not hasattr(maude.StrategyRewriteGraph, 'getNrRealStates'): - maude.StrategyRewriteGraph.getNrRealStates = maude.StrategyRewriteGraph.getNrStates - if not hasattr(maude.Term, 'getVarName'): usermsgs.print_warning('Version 1.0 of the maude package adds some useful features for this program.\n' 'Please update.') diff --git a/umaudemc/counterprint.py b/umaudemc/counterprint.py index a62f729..91d9804 100644 --- a/umaudemc/counterprint.py +++ b/umaudemc/counterprint.py @@ -78,17 +78,21 @@ def print_counterexample(graph, counter, printer_triple): next_index = lead_in[i+1] if i+1 < len(lead_in) else cycle[0] if graph.strategyControlled: + trans = graph.getTransition(index, next_index) + printer.next_step_strat( sformat(graph, index), graph.getStateStrategy(index), - eformat(graph, index, next_index), + eformat(trans), sformat(graph, next_index), first_index=index, second_index=next_index) else: + rule = graph.getRule(index, next_index) + printer.next_step( sformat(graph, index), - eformat(graph, index, next_index), + eformat(rule), sformat(graph, next_index), first_index=index, second_index=next_index) @@ -103,17 +107,21 @@ def print_counterexample(graph, counter, printer_triple): next_index = cycle[i+1] if i+1 < len(cycle) else cycle[0] if graph.strategyControlled: + trans = graph.getTransition(index, next_index) + printer.next_step_strat( sformat(graph, index), graph.getStateStrategy(index), - eformat(graph, index, next_index), + eformat(trans), sformat(graph, next_index), first_index=index, second_index=next_index) else: + rule = graph.getRule(index, next_index) + printer.next_step( sformat(graph, index), - eformat(graph, index, next_index), + eformat(rule), sformat(graph, next_index), first_index=index, second_index=next_index) diff --git a/umaudemc/data/smcview.js b/umaudemc/data/smcview.js index 8595b0f..90525db 100644 --- a/umaudemc/data/smcview.js +++ b/umaudemc/data/smcview.js @@ -38,13 +38,11 @@ function browseDir(dir) } } - var question = new FormData() - - question.append('question', 'ls') - question.append('url', dir) + var question = {question: 'ls', url: dir} request.open('post', 'ask') - request.send(question) + request.setRequestHeader('Content-Type', 'application/json') + request.send(JSON.stringify(question)) } function openFile(file) @@ -57,6 +55,23 @@ function openFile(file) loadSourceModules(file) } +function loadSourceNative() +{ + const request = new XMLHttpRequest() + + request.onreadystatechange = function() + { + if (this.readyState == XMLHttpRequest.DONE && this.status == 200) + { + console.log(this.responseText) + openFile(this.responseText) + } + } + + request.open('get', 'umaudemc://open/') + request.send() +} + function incompletePassign() { switch (document.getElementById('pmethod').value) { @@ -193,11 +208,10 @@ function loadSourceModules(file) // Discard modules from previous files smodule.options.length = 0 - var question = new FormData() - question.append('question', 'sourceinfo') - question.append('url', file) + var question = {question: 'sourceinfo', url: file} request.open('post', 'ask') - request.send(question) + request.setRequestHeader('Content-Type', 'application/json') + request.send(JSON.stringify(question)) } function addPropToFormula(prop) @@ -318,11 +332,11 @@ function loadModule() description.innerText = 'Please select a Maude file and a Maude module defining the system and properties specification.' - var question = new FormData() - question.append('question', 'modinfo') - question.append('mod', currentModule) + var question = {question: 'modinfo', mod: currentModule} + request.open('post', 'ask') - request.send(question) + request.setRequestHeader('Content-Type', 'application/json') + request.send(JSON.stringify(question)) } function modelcheck() @@ -356,14 +370,14 @@ function modelcheck() } } - var question = new FormData() - - question.append('question', 'modelcheck') - question.append('mod', document.getElementById('module').value) - question.append('initial', document.getElementById('initial').value) - question.append('formula', document.getElementById('formula').value) - question.append('strategy', document.getElementById('strategy').value) - question.append('opaques', document.getElementById('opaques').value) + const question = { + question: 'modelcheck', + mod: document.getElementById('module').value, + initial: document.getElementById('initial').value, + formula: document.getElementById('formula').value, + strategy: document.getElementById('strategy').value, + opaques: document.getElementById('opaques').value + } // Quantitative model checking stuff if (document.getElementById('command').value == 'qt') @@ -375,7 +389,8 @@ function modelcheck() } request.open('post', 'ask') - request.send(question) + request.setRequestHeader('Content-Type', 'application/json') + request.send(JSON.stringify(question)) } function escapeHTMLChars(text) { @@ -460,17 +475,15 @@ function waitModelChecker(mcref) { // Disable input until model checking has finished disableInput(true) - var question = new FormData() + const question = {question: 'wait', mcref: mcref} - question.append('question', 'wait') - question.append('mcref', mcref) request.open('post', 'ask') - request.send(question) + request.setRequestHeader('Content-Type', 'application/json') + request.send(JSON.stringify(question)) } function cancelChecking() { const request = new XMLHttpRequest() - const question = new FormData() request.onreadystatechange = function() { @@ -486,9 +499,9 @@ function cancelChecking() { } } - question.append('question', 'cancel') request.open('post', 'ask') - request.send(question) + request.setRequestHeader('Content-Type', 'application/json') + request.send('{"question": "cancel"}') } function closeResultDialog() diff --git a/umaudemc/formatter.py b/umaudemc/formatter.py index d6cd845..5ff49ed 100644 --- a/umaudemc/formatter.py +++ b/umaudemc/formatter.py @@ -89,23 +89,18 @@ def parse_state_format(sformat, strategy): tused > 0, sused > 0)) -def apply_edge_format(graph, origin, dest, eformat): +def apply_edge_format(stmt, eformat): """ Edge label generator using a prebuilt format string. - :param graph: Rewriting graph the transition belong to. - :type graph: Maude rewriting graph. - :param origin: Index of the origin state within the graph. - :type origin: int - :param dest: Index of the destination state within the graph. - :type dest: int + :param stmt: Rule that caused the transition + :type stmt: Rule :param eformat: Prebuilt format string. :type eformat: str :returns: Formatted edge label. :rtype str """ - stmt = graph.getRule(origin, dest) label = stmt.getLabel() line = stmt.getLineNumber() opaque = '' @@ -116,9 +111,8 @@ def apply_edge_format(graph, origin, dest, eformat): return eformat.format(stmt=stmt, label=label, line=line, opaque=opaque) -def apply_edge_format_strat(graph, origin, dest, eformat): +def apply_edge_format_strat(trans, eformat): """Edge label generator for strategy-controlled using a prebuilt format string""" - trans = graph.getTransition(origin, dest) opaque, label, stmt, line = '', '', '', '' if trans.getType() == maude.StrategyRewriteGraph.SOLUTION: @@ -150,9 +144,9 @@ def parse_edge_format(eformat, strategy): eformat = re.sub(r'%(.\d+)?n', r'{line:\1}', eformat) if strategy: - return lambda graph, origin, dest: apply_edge_format_strat(graph, origin, dest, eformat) + return lambda trans: apply_edge_format_strat(trans, eformat) else: - return lambda graph, origin, dest: apply_edge_format(graph, origin, dest, eformat) + return lambda stmt: apply_edge_format(stmt, eformat) # @@ -165,29 +159,30 @@ def print_term(graph, index): return graph.getStateTerm(index) -def print_transition(graph, origin, dest): +def print_transition(stmt): """Default edge-label printing function""" - return graph.getRule(origin, dest) + return stmt -def print_transition_strat(graph, origin, dest): +def print_transition_strat(trans): """Default edge-label printing function with strategies""" - trans = graph.getTransition(origin, dest) - return { - maude.StrategyRewriteGraph.RULE_APPLICATION : trans.getRule(), - maude.StrategyRewriteGraph.OPAQUE_STRATEGY : trans.getStrategy(), - maude.StrategyRewriteGraph.SOLUTION : '' - }[trans.getType()] + ttype = trans.getType() + + if ttype == maude.StrategyRewriteGraph.RULE_APPLICATION: + return trans.getRule() + elif ttype == maude.StrategyRewriteGraph.OPAQUE_STRATEGY: + return trans.getStrategy() + else: + return '' -def print_transition_label(graph, origin, dest): +def print_transition_label(stmt): """Alternative edge-label printing function (only rule label)""" - return graph.getRule(origin, dest).getLabel() + return stmt.getLabel() -def print_transition_strat_label(graph, origin, dest): +def print_transition_strat_label(trans): """Alternative edge-label printing function with strategies (only rule/strategy label)""" - trans = graph.getTransition(origin, dest) ttype = trans.getType() if ttype == maude.StrategyRewriteGraph.RULE_APPLICATION: diff --git a/umaudemc/grapher.py b/umaudemc/grapher.py index bb3dc2d..3132cc1 100644 --- a/umaudemc/grapher.py +++ b/umaudemc/grapher.py @@ -43,8 +43,8 @@ def exploreAndGraph(self, graph, stateNr, bound=-1): if bound == 0: return - for next_state in graph.getNextStates(stateNr): - elabel = self.elabel(graph, stateNr, next_state) if self.elabel else None + for next_state, edge in graph.getTransitions(stateNr): + elabel = self.elabel(edge) if self.elabel else None self.write_transition(stateNr, next_state, elabel) if next_state not in self.visited: @@ -67,7 +67,8 @@ def make_label(self, p, graph, start, end): num, den = Fraction(p).limit_denominator().as_integer_ratio() # Standard labels are used too - elabel = self.elabel(graph, start, end) + stmt = graph.getTransition(start, end) if graph.strategyControlled else graph.getRule(start, end) + elabel = self.elabel(stmt) return f'{num}/{den} {elabel}' if p != 1.0 else elabel @@ -123,14 +124,14 @@ def exploreAndGraph(self, graph, stateNr, bound=-1): if bound == 0: return - for next_state in graph.getNextStates(stateNr): + for next_state, edge in graph.getTransitions(stateNr): print(f'\t{self.printState(graph, stateNr)}', file=self.outfile, end='') next_visited = next_state in self.visited if self.elabel is None: print(f' -> ', file=self.outfile, end='') else: - label = str(self.elabel(graph, stateNr, next_state)).replace('"', '""') + label = str(self.elabel(edge)).replace('"', '""') print(f' ->["{label}"] ', file=self.outfile, end='') print(f'{self.printState(graph, next_state)};', file=self.outfile) diff --git a/umaudemc/gtk.py b/umaudemc/gtk.py index 9d48ccb..5797ebb 100644 --- a/umaudemc/gtk.py +++ b/umaudemc/gtk.py @@ -1,529 +1,109 @@ # -# Desktop interface with Gtk +# Desktop interface with Gtk (wrapper around the web interface) # -import threading -from xml.sax.saxutils import escape - import gi -gi.require_version('Gtk', '3.0') +gi.require_version('Gtk', '4.0') gi.require_version('Gio', '2.0') -gi.require_version('WebKit2', '4.0') -from gi.repository import Gtk, Gio, GLib, GObject, WebKit2 - -from . import resources -from . import mproc - - -MODULE_TYPE_NAMES = { - 'fmod' : 'Functional module', - 'mod' : 'System module', - 'smod' : 'Strategy module', - 'fth' : 'Functional theory', - 'th' : 'System theory', - 'sth' : 'Strategy theory' -} - - -class Banner(Gtk.Bin): - """Banner where module and counterexample information is presented""" - - __gsignals__ = { - # A strategy or atomic proposition name has been clicked - 'hint-clicked': (GObject.SignalFlags.RUN_FIRST, None, (bool, str, int)) - } - - def __init__(self): - # Three widgets may appear in the banner (only one at a time) to respectively - # show a fixed message, module information or a counterexample - - self.label = Gtk.Label( - label='Please select a Maude file and a Maude module defining the system and properties specification', - use_markup=True, - justify=Gtk.Justification.CENTER, - track_visited_links=False - ) - self.grid = None - self.canvas = None - - Gtk.Bin.__init__(self, child=self.label) - - def __makeGrid(self, info): - """Compose the grid where module information is presented""" - - # The grid has 2 columns and 4 rows starting with a header with the module - # name and type, and followed by some attributes of the module whose values - # appear in the second column - - self.module_type = Gtk.Label(label=f'{MODULE_TYPE_NAMES[info["type"]]}', use_markup=True) - self.module_name = Gtk.Label(label=f'{info["name"]}', use_markup=True) - - # Labels for each module attribute name - sort_label = Gtk.Label.new('State sort:') - props_label = Gtk.Label.new('Atomic propositions:') - self.strats_label = Gtk.Label.new('Strategies:') - - # Labels for each module attribute value (to be filled on its selection) - self.sort_value = Gtk.Label.new('') - self.props_value = Gtk.Label(label='', use_markup=True, track_visited_links=False) - self.strats_value = Gtk.Label(label='', use_markup=True, track_visited_links=False) - self.props_value.set_line_wrap(True) - self.strats_value.set_line_wrap(True) - - # Propositions and strategies can be clicked to be filled - # in their corresponding fields - self.props_value.connect('activate-link', self.hint_clicked) - self.strats_value.connect('activate-link', self.hint_clicked) - - # Align labels to the right and values to the left - self.module_type.set_halign(Gtk.Align.END) - sort_label.set_halign(Gtk.Align.END) - props_label.set_halign(Gtk.Align.END) - self.strats_label.set_halign(Gtk.Align.END) - self.module_name.set_halign(Gtk.Align.START) - self.sort_value.set_halign(Gtk.Align.START) - self.props_value.set_halign(Gtk.Align.START) - self.strats_value.set_halign(Gtk.Align.START) - - self.grid = Gtk.Grid.new() - self.grid.set_valign(Gtk.Align.CENTER) - self.grid.set_halign(Gtk.Align.CENTER) - self.grid.set_column_spacing(15) - self.grid.set_row_spacing(5) - self.grid.attach(self.module_type, 0, 0, 1, 1) - self.grid.attach(self.module_name, 1, 0, 1, 1) - self.grid.attach(sort_label, 0, 1, 1, 1) - self.grid.attach(self.sort_value, 1, 1, 1, 1) - self.grid.attach(props_label, 0, 2, 1, 1) - self.grid.attach(self.props_value, 1, 2, 1, 1) - self.grid.attach(self.strats_label, 0, 3, 1, 1) - self.grid.attach(self.strats_value, 1, 3, 1, 1) - - self.grid.show_all() - - def __set_current(self, widget): - """Set the current widget in the banner""" - - if self.get_child() != widget: - self.remove(self.get_child()) - self.add(widget) - - @staticmethod - def composeSignature(prefix, signature): - """Create a link with the signature of an atomic proposition or strategy""" - - # Displayed signature - composed = escape(signature[0]) if len(signature) == 1 else \ - '{}({})'.format(escape(signature[0]), ', '.join(signature[1:])) - - return f'{composed}' - - def show_modinfo(self, info): - """Process and presents the given module information""" - - if not info['valid']: - self.label.set_label(f'{MODULE_TYPE_NAMES[info["type"]]} {info["name"]}' - '\n\nNot valid for model checking') - - self.__set_current(self.label) - else: - if self.grid is None: - self.__makeGrid(info) - - self.module_type.set_label(f'{MODULE_TYPE_NAMES[info["type"]]}') - self.module_name.set_label(f'{info["name"]}') - - # State sort subtypes - self.sort_value.set_label(' '.join(info['state'])) - - # Atomic propositions - if info['prop']: - self.props_value.set_label(' '.join(map(lambda x: self.composeSignature('p', x), info['prop']))) - else: - self.props_value.set_label('none') - - # Strategies - if info['strat']: - self.strats_value.set_label(' '.join(map(lambda x: self.composeSignature('s', x), info['strat']))) - self.strats_value.set_visible(True) - self.strats_label.set_visible(True) - else: - self.strats_value.set_visible(False) - self.strats_label.set_visible(False) - - self.__set_current(self.grid) - - def hint_clicked(self, banner, uri): - """A link was clicked""" - - if len(uri) == 0 or uri[0] != '#': - return True - - # The URI contains the type of objects, its name and arity - kind, name, arity = uri[1:].split(':') - self.emit('hint-clicked', kind == 's', name, int(arity)) - - return True - - @classmethod - def dict2jsobj(cls, value): - """Convert a Python dictionary to a Javascript object literal""" - - if isinstance(value, bool): - return 'true' if value else 'false' - - elif value is None: - return 'null' - - elif isinstance(value, dict): - entries = [f'{key}: {cls.dict2jsobj(value)}' for key, value in value.items()] - return '{' + ', '.join(entries) + '}' - - elif isinstance(value, list): - return '[' + ', '.join(cls.dict2jsobj(elem) for elem in value) + ']' - - else: - return repr(value) - - def show_counterexample(self, result, background=None): - """Show a counterexample in the banner""" - - js_result = self.dict2jsobj(result) - - if self.canvas is None: - self.canvas = WebKit2.WebView.new() - # Enable inspector (for debugging purposes) - self.canvas.get_settings().props.enable_developer_extras = True - # Resolve files with the umaudemc scheme to static resources - self.canvas.get_context().register_uri_scheme('umaudemc', self.get_webview_resource, None) - self.html_load_id = self.canvas.connect('load-changed', self.html_load, f'initCanvas({js_result})') - # Load the input data page - self.canvas.load_html(resources.get_resource_content('result.htm')) - self.canvas.show_all() - else: - self.canvas.run_javascript(f'initCanvas({js_result})', None, self.js_callback, None) - - # Set the background color to that of the windows (if this is background) - if background is not None: - self.canvas.set_background_color(background) +gi.require_version('WebKit', '6.0') +from gi.repository import Gtk, Gio, GLib, WebKit - # Replace the current widget with this - self.__set_current(self.canvas) +import multiprocessing - def set_editable(self, value): - """Disable active widgets in the banner""" - if self.grid is not None: - self.grid.set_sensitive(value) +def start_server(queue): + """Start a server in a separate process""" + from . import webui + import http.server - def get_webview_resource(self, request, data): - """Get a resource from the package data""" - - path = request.get_path() - - if path == 'smcview.css': - content = resources.get_resource_binary(path) - request.finish(Gio.MemoryInputStream.new_from_data(content), len(content), 'text/css') - - elif path == 'smcgraph.js': - content = resources.get_resource_binary(path) - request.finish(Gio.MemoryInputStream.new_from_data(content), len(content), 'text/javascript') - - else: - request.finish_error(GLib.Error.new_literal(GLib.FileError(GLib.FileError.NOENT))) - - def js_callback(self, sender, result, data): - """Callback for run_javascript""" - - self.canvas.run_javascript_finish(result) - - def html_load(self, canvas, event, call): - """Callback when the page has been loaded""" - - if event == WebKit2.LoadEvent.FINISHED: - canvas.run_javascript(call, None, self.js_callback, None) - canvas.disconnect(self.html_load_id) + httpd = http.server.ThreadingHTTPServer(('127.0.0.1', 0), webui.RequestHandler) + httpd.info = webui.ConnectionInfo() + httpd.info.path_handler.set_default(None) + queue.put(httpd.server_port) + httpd.serve_forever() class ModelCheckerWindow(Gtk.ApplicationWindow): """The main window of the model checker GUI""" - __gsignals__ = { - # Model checking has finished - 'mc-finished': (GObject.SignalFlags.RUN_FIRST, None, (object, )) - } - - def __init__(self): - super().__init__(title='Maude strategy-aware model checker') - self.connect('delete-event', self.destroyed) - self.set_border_width(6) - self.resize(800, 600) - - # The window consists of a header (top), a banner (self.vbox). and two - # bottom containers (bottom1 and bottom2) vertically arranged - - self.vbox = Gtk.Box(orientation=Gtk.Orientation.VERTICAL, spacing=6) - top = Gtk.Box(spacing=6) - self.banner = Banner() - self.banner.connect('hint-clicked', self.link_click) - bottom1 = Gtk.Box(spacing=6) - bottom2 = Gtk.Box(spacing=6) - self.vbox.pack_start(top, False, False, 0) - self.vbox.pack_start(self.banner, True, True, 0) - self.vbox.pack_start(bottom1, False, False, 0) - self.vbox.pack_start(bottom2, False, False, 0) - self.add(self.vbox) - - # A header allow choosing and show the current file and module - self.openbutton = Gtk.FileChooserButton.new_with_dialog(self.make_open_dialog()) - self.add_labeled_widget(top, 'Maude file:', self.openbutton) - self.openbutton.connect('file-set', self.file_selected) - - self.module = Gtk.ComboBoxText() - self.add_labeled_widget(top, '_Module:', self.module) - self.module.connect('changed', self.module_selected) - - # A footer includes entries to input the problem data - self.initial = Gtk.Entry() - self.add_labeled_widget(bottom1, '_Initial term:', self.initial) - - self.formula = Gtk.Entry() - self.add_labeled_widget(bottom1, '_Formula:', self.formula) - - self.sexpr = Gtk.Entry() - self.add_labeled_widget(bottom2, '_Strategy:', self.sexpr) - - self.opaques = Gtk.Entry() - self.add_labeled_widget(bottom2, '_Opaque strategies:', self.opaques) - - # A button starts model checking - self.button = Gtk.Button(label='Model check', sensitive=False) - bottom2.pack_start(self.button, False, False, 0) - self.button.connect('clicked', self.model_check_clicked) - self.connect('mc-finished', self.model_check_finished) - - # When an entry changes, the usability of the model-checking - # button is updated - self.initial.connect('changed', self.entry_changed) - self.formula.connect('changed', self.entry_changed) - - # Widgets lists (for doing actions on all of them) - self.entry_widgets = [self.openbutton, self.module, self.initial, - self.formula, self.sexpr, self.opaques] - self.text_widgets = [self.initial, self.formula, self.sexpr, self.opaques] - - # Whether widgets are editable (not blocked by other operation) - self.editable = True - # A connection to an interruptable Maude session - self.maude_session = mproc.MaudeRemote() - - def signal_entry_error(self, entry, value): - """Mark an entry widget with a warning in case of syntax error""" - - entry.set_icon_from_icon_name(Gtk.EntryIconPosition.SECONDARY, - 'dialog-warning' if value else None) - - def add_labeled_widget(self, container, label, widget, expand=True): - """Add a widget together with a label to a container""" - - label_widget = Gtk.Label.new_with_mnemonic(label) - label_widget.set_mnemonic_widget(widget) - container.pack_start(label_widget, False, False, 0) - container.pack_start(widget, expand, expand, 0) + def __init__(self, port=8000): + super().__init__(title='Unified Maude model-checking tool') + self.connect('close-request', self.destroyed) + self.set_default_size(800, 600) + + # Use a WebView as the only content of the window + self.canvas = WebKit.WebView.new() + self.set_child(self.canvas) + # Enable inspector (for debugging purposes) + self.canvas.get_settings().props.enable_developer_extras = True + # Remove the header bar (there is already a window title) + user_manager = self.canvas.get_user_content_manager() + style = WebKit.UserStyleSheet('header { display: none; }', + WebKit.UserContentInjectedFrames.TOP_FRAME, + WebKit.UserStyleLevel.AUTHOR, None, None) + user_manager.add_style_sheet(style) + # Allow using the system open dialog + self.enable_open_dialog(user_manager) + + # Load the input page + self.canvas.load_uri(f'http://127.0.0.1:{port}/') + + def destroyed(self, window): + """When the window is closed""" + self.get_application().server_process.terminate() + + def enable_open_dialog(self, user_manager): + """Enable access to the open dialog in the browser""" + + # Register a script so that the native open dialog is used + # instead of the web-based file explorer + script = WebKit.UserScript('loadSource = loadSourceNative', + WebKit.UserContentInjectedFrames.TOP_FRAME, + WebKit.UserScriptInjectionTime.END, None, None) + user_manager.add_script(script) + + # Create a file open dialog + self.dialog = self.make_open_dialog() + + # Register the custom umaudemc scheme to open the file dialog + self.canvas.get_context().register_uri_scheme('umaudemc', self._umaudemc_request, None) + # Allow cross-origin requests to umaudemc (from localhost) + self.canvas.set_cors_allowlist(['umaudemc://*/*']) + # Disable catching (for the umaudemc request to be repeatable) + self.canvas.get_context().set_cache_model(WebKit.CacheModel.DOCUMENT_VIEWER) def make_open_dialog(self): """Build the Maude file open dialog""" - opendialog = Gtk.FileChooserDialog(title='Choose a Maude file', - parent=self, - action=Gtk.FileChooserAction.OPEN) - - opendialog.add_button(Gtk.STOCK_CANCEL, Gtk.ResponseType.CANCEL) - opendialog.add_button(Gtk.STOCK_OPEN, Gtk.ResponseType.OK) + opendialog = Gtk.FileDialog() + opendialog.props.title = 'Choose a Maude file' filter_maude = Gtk.FileFilter() filter_maude.set_name('Maude files (*.maude)') filter_maude.add_pattern('*.maude') - opendialog.add_filter(filter_maude) - - return opendialog - - def destroyed(self, event, other): - """Callback for the window destruction""" - - self.maude_session.shutdown() - return False - - def entry_changed(self, editable): - """Callback when some entry has changed (to disable/enable the MC button)""" - - complete = self.initial.get_text() and self.formula.get_text() \ - and self.openbutton.get_filename() and self.module.get_active_id() - self.button.set_sensitive(complete) - - def file_selected(self, data): - """A file has been selected to be loaded""" - - filename = self.openbutton.get_filename() - print('Loading', filename) - - if not self.maude_session.load(filename): - self.notify_error(f'Error loading the file {filename}.') - else: - last_id = None - for name, mtype in self.maude_session.getModules(): - self.module.append(name, f'{name} ({mtype})') - last_id = name - self.module.set_active_id(last_id) - self.entry_changed(self.openbutton) + filters = Gio.ListStore() + filters.append(filter_maude) + opendialog.props.filters = filters - def file_reload(self): - """Reload the currently selected file (after an interrupted session)""" - - filename = self.openbutton.get_filename() - print('Reloading', filename) - - if not self.maude_session.load(filename): - self.notify_error(f'Error reloading the file {filename}.') - else: - current_id = self.module.get_active_id() - - for name, mtype in self.maude_session.getModules(): - self.module.append(name, f'{name} ({mtype})') - - self.module.set_active_id(current_id) - - def module_selected(self, data): - """Callback for the selection of a module""" - - self.module_info = self.maude_session.getModuleInfo(self.module.get_active_id()) - self.show_modinfo() - - def link_click(self, sender, is_strat, text, arity): - """Callback for the activation of a banner link""" - - # An entry file is completed with the clicked object - entry = self.sexpr if is_strat else self.formula - - entry.delete_selection() - inserted_text = text + ('' if arity == 0 else '(') - entry.insert_text(inserted_text, entry.get_position()) - entry.set_position(entry.get_position() + len(inserted_text)) - - def model_check_clicked(self, sender): - """Callback for the model-checking/cancel button""" - - # The button acts as a cancel when model checking - if not self.editable: - self.set_editable(True) - self.maude_session.shutdown() - self.maude_session = mproc.MaudeRemote() - self.file_reload() - return - - # Pass the model checking data to Maude - data = { - 'file' : self.openbutton.get_filename(), - 'module' : self.module.get_active_id(), - 'initial' : self.initial.get_text(), - 'strat' : self.sexpr.get_text(), - 'formula' : self.formula.get_text(), - 'opaques' : self.opaques.get_text().split() - } - - info = self.maude_session.modelCheck(data) - - # Model checking has not been done yet, but the input data of the problem - # has been checked. info includes a reference to obtain the actual result. + return opendialog - if not info['ok']: - cause = info['cause'] - self.signal_entry_error(self.initial, cause == 'term') - self.signal_entry_error(self.formula, cause == 'formula') - self.signal_entry_error(self.sexpr, cause == 'strat') - self.signal_entry_error(self.opaques, cause == 'opaque') + def _umaudemc_request(self, request, data): + path = request.get_uri() - if cause == 'nobackend': - self.notify_error(f'No installed backend for the {info["logic"]} logic') + if path == 'umaudemc://open/': + self.dialog.open(self, None, self._file_selected, request) else: - # Hide previous error marks - for widget in self.text_widgets: - self.signal_entry_error(widget, False) - - self.set_editable(False) - - # Model checking is started in a separate thread not to block the - # interface (although most components are disabled) - self.thread = threading.Thread(target=self.model_check_action, args=(info['ref'], data, )) - self.thread.daemon = True - self.thread.start() - - def notify_error(self, text): - """Notify an error to the user (with a dialog)""" - - dialog = Gtk.MessageDialog(text=text, - buttons=Gtk.ButtonsType.OK, - message_type=Gtk.MessageType.ERROR) - dialog.run() - dialog.destroy() + request.finish_error(GLib.Error.new_literal(1, "Not found", 404)) - def set_editable(self, value): - """Enable or disable the active components of the window""" - - self.editable = value - - for widget in self.entry_widgets: - widget.set_sensitive(value) - self.banner.set_editable(value) - - self.button.set_label('Model check' if value else 'Cancel') - - def model_check_action(self, mcref, data): - """Callback for the result of the model-checking task""" - - # This is not run in the GTK thread - - result = self.maude_session.get_result(mcref) - - # Complement result with the initial data - result['formula'] = data['formula'] - result['initial'] = data['initial'] - result['strat'] = data.get('strat') - - def emit_mcfinished(): - # Instead of emitting the signal, its handler code can be done here - self.emit('mc-finished', result) - return False - - GLib.idle_add(emit_mcfinished) - - def model_check_finished(self, sender, result): - """Callback in the GTK thread for the model checking finalization""" - - # Join the model checker thread (just finished) - self.thread.join(2) - - holds = result['result'] - has_counterexample = result['hasCounterexample'] - - if not has_counterexample or holds: - # InfoBar will look more like the web version - dialog = Gtk.MessageDialog(text=('✔ The property holds.' if holds else '✗ The property does not hold.'), - buttons=Gtk.ButtonsType.OK) - dialog.run() - dialog.destroy() - - bg = self.get_style_context().get_background_color(self.get_state()) - if has_counterexample: - self.banner.show_counterexample(result, background=bg) - self.set_editable(True) - - def show_modinfo(self): - """Set the module information in the banner""" - - self.banner.show_modinfo(self.module_info) + def _file_selected(self, dialog, result, request): + """Callback on the selection of a file""" + try: + content = dialog.open_finish(result).get_path().encode('utf-8') + request.finish(Gio.MemoryInputStream.new_from_data(content), len(content), 'text/plain') + except GLib.Error: + request.finish_error(GLib.Error.new_literal(1, "Not found", 404)) def run_gtk(): @@ -531,12 +111,21 @@ def run_gtk(): app = Gtk.Application.new('es.ucm.maude.umaudemc', Gio.ApplicationFlags.FLAGS_NONE) def window_init(app): - window = ModelCheckerWindow() + # Start the web server + queue = multiprocessing.Queue() + app.server_process = multiprocessing.Process(target=start_server, args=(queue,)) + app.server_process.start() + + # The random server listening port is obtained through the queue + port = queue.get() + window = ModelCheckerWindow(port) + app.add_window(window) - window.show_all() + window.show() app.connect('activate', window_init) return app.run() + if __name__ == "__main__": run_gtk() diff --git a/umaudemc/kleene.py b/umaudemc/kleene.py new file mode 100644 index 0000000..a52a9f6 --- /dev/null +++ b/umaudemc/kleene.py @@ -0,0 +1,156 @@ +# +# Strategy execution machine and graph for the Kleene star semantics +# + +from .common import maude +from .pyslang import GraphRunner, GraphExecutionState + + +class KleeneExecutionState(GraphExecutionState): + """Execution state for generating a graph""" + + def __init__(self, term, pc, stack, conditional=False, graph_node=None, extra=None, iterations=None): + super().__init__(term, pc, stack, conditional, graph_node, + (extra, set() if iterations is None else iterations)) + + def copy(self, term=None, pc=None, stack=None, conditional=False, graph_node=None, extra=None): + """Clone state with possibly some changes""" + + return KleeneExecutionState( + self.term if term is None else term, + self.pc + 1 if pc is None else pc, + self.stack if stack is None else stack, + conditional, + self.graph_node if graph_node is None else graph_node, + self.extra[0] if extra is None else extra, + self.extra[1], + ) + + def add_kleene(self, args): + """Add iteration labels""" + self.extra = (self.extra[0], self.extra[1] | {args}) + + def reset_extra(self): + """Reset the extra attribute""" + self.extra = (self.extra[0], set()) + + +class KleeneRunner(GraphRunner): + """Runner that extract a Streett automaton with the Kleene star semantics""" + + def __init__(self, program, term): + super().__init__(program, term, state_class=KleeneExecutionState) + self.iter_contexts = {} + + def kleene(self, args, stack): + """Keep track of iterations""" + context_id = self.iter_contexts.setdefault(self.current_state.stack, len(self.iter_contexts)) + self.current_state.add_kleene(((args[0], context_id), args[1])) + super().kleene(args, stack) + + +class StrategyKleeneGraph: + """Strategy-controlled graph with iteration tracking""" + + # This is mostly copied from StrategyMarkovGraph + # (merging some of the code should be considered) + + # This graph is always strategy-controlled + strategyControlled = True + + class Transition: + """Transition of the StrategyKleeneGraph""" + + def __init__(self, pair=None): + self.rule, self.iterations = pair + + def getRule(self): + return self.rule + + def getType(self): + return (maude.StrategyRewriteGraph.SOLUTION if self.rule is None + else maude.StrategyRewriteGraph.RULE_APPLICATION) + + def __init__(self, root, nrew): + self.state_list = [root] + self.state_map = {root: 0} + self.nr_rewrites = nrew + + def getStateTerm(self, state): + return self.state_list[state].term + + def getStateStrategy(self, state): + return '' + + def getNrRewrites(self): + return self.nr_rewrites + + def getNrRealStates(self): + return len(self.state_list) + + def getNrStates(self): + return len(self.state_list) + + def states(self): + """Iterator through the states (numbers) of the graph""" + return range(len(self.state_list)) + + def getTransition(self, origin, dest): + """Get one of the transitions from one state to another""" + + actions = self.state_list[origin].actions[self.state_list[dest]] + return self.Transition(actions[0]) if actions else self.Transition() + + def getNextStates(self, stateNr): + """Iterator through the successors of a state""" + + for next_state in self.state_list[stateNr].children: + yield self.state_map[next_state] + + def getTransitions(self, stateNr): + """Iterator through the transitions of the graph""" + + state = self.state_list[stateNr] + for next_state in state.children: + actions = state.actions[next_state] + for action in (actions if actions else (None,)): + yield self.state_map[next_state], self.Transition(action) + + def expand(self): + """Expand the underlying graph""" + + for k, state in enumerate(self.state_list): + for child in state.children: + if child not in self.state_map: + self.state_map[child] = len(self.state_list) + self.state_list.append(child) + + +def get_kleene_graph(data): + """Get the Kleene-aware graph for a strategy (with InputData)""" + + return get_kleene_graph_mts(data.module, data.term, data.strategy) + + +def get_kleene_graph_mts(module, term, strategy): + """Get the Kleene-aware graph for a strategy""" + + from . import pyslang + + ml = maude.getModule('META-LEVEL') + + # Initialize the strategy compiler and optimizer + sc = pyslang.StratCompiler(module, ml, use_notify=True, use_kleene=True, ignore_one=True) + + # Compile the strategy + p = sc.compile(ml.upStrategy(strategy)) + + # Reduce the term + nrew_initial = term.reduce() + + root, nrew = KleeneRunner(p, term).run() + graph = StrategyKleeneGraph(root, nrew + nrew_initial) + + graph.expand() + + return graph diff --git a/umaudemc/opsem.py b/umaudemc/opsem.py index 7310246..c9b6108 100644 --- a/umaudemc/opsem.py +++ b/umaudemc/opsem.py @@ -125,7 +125,7 @@ def make_initial_term(self, term, strategy): return self.stack_state(term_meta, strategy_meta) def make_graph(self, initial, strategy, opaques=()): - """Get the strategy for the strategy-controlled rewriting""" + """Get the graph for the strategy-controlled rewriting""" # Build the initial term t = self.make_initial_term(initial, strategy) diff --git a/umaudemc/probabilistic.py b/umaudemc/probabilistic.py index e93f67e..a251e98 100644 --- a/umaudemc/probabilistic.py +++ b/umaudemc/probabilistic.py @@ -604,6 +604,9 @@ def strategyControlled(self): def getRule(self, *args): return self.graph.getRule(*args) + def getTransition(self, *args): + return self.graph.getTransition(*args) + def states(self): """Iterator through the states (numbers) of the graph""" return self.visited @@ -756,17 +759,17 @@ def getType(self): return (maude.StrategyRewriteGraph.SOLUTION if self.rule is None else maude.StrategyRewriteGraph.RULE_APPLICATION) - def __init__(self, root): + def __init__(self, root, nrew): self.state_list = [root] self.state_map = {root: 0} self.nondeterminism = False + self.nr_rewrites = nrew def getStateTerm(self, state): return self.state_list[state].term def getNrRewrites(self): - # The number of rewrites is not counted in this implementation - return 0 + return self.nr_rewrites def getNrRealStates(self): return len(self.state_list) @@ -816,8 +819,8 @@ def expand(self): class StrategyMetadataGraph(StrategyMarkovGraph): """Strategic graph with probabilities given by non-ground metadata""" - def __init__(self, root, mdp=False): - super().__init__(root) + def __init__(self, root, nrew, mdp=False): + super().__init__(root, nrew) self.nondeterminism = mdp def getTransition(self, origin, dest): @@ -887,11 +890,11 @@ def get_probabilistic_strategy_graph(module, strategy, term, stmt_map=None, mdp= # Execute the strategy with the corresponding runner if stmt_map is None: - root = pyslang.MarkovRunner(p, term).run() - graph = StrategyMarkovGraph(root) + root, nrew = pyslang.MarkovRunner(p, term).run() + graph = StrategyMarkovGraph(root, nrew) else: - root = pyslang.MetadataRunner(p, term, stmt_map).run() - graph = StrategyMetadataGraph(root, mdp) + root, nrew = pyslang.MetadataRunner(p, term, stmt_map).run() + graph = StrategyMetadataGraph(root, nrew, mdp) graph.expand() diff --git a/umaudemc/pyslang.py b/umaudemc/pyslang.py index b0c0749..9fc9dad 100644 --- a/umaudemc/pyslang.py +++ b/umaudemc/pyslang.py @@ -19,7 +19,7 @@ class Instruction: POP = 0 # no arguments JUMP = 1 # sequence of addresses STRAT = 2 # strategy (at the object level, for potential optimizations only) - RLAPP = 3 # (label, intial substitution, whether it is applied on top) + RLAPP = 3 # (label, initial substitution, whether it is applied on top) TEST = 4 # (match type, pattern, condition) CHOICE = 5 # sequence of pairs of term (weight) and address CALL = 6 # (call term, index of a named strategy within the program, whether the call is tail) @@ -34,10 +34,11 @@ class Instruction: WMATCHREW = 15 # like MATCHREW + (weight) ONE = 16 # no arguments CHECKPOINT = 17 # no arguments + KLEENE = 18 # (address of where the iteration begins, whether it enters or leaves) NAMES = ['POP', 'JUMP', 'STRAT', 'RLAPP', 'TEST', 'CHOICE', 'CALL', 'SUBSEARCH', 'NOFAIL', 'MATCHREW', 'NEXTSUBTERM', 'RWCSTART', 'RWCNEXT', 'NOTIFY', - 'SAMPLE', 'WMATCHREW', 'ONE', 'CHECKPOINT'] + 'SAMPLE', 'WMATCHREW', 'ONE', 'CHECKPOINT', 'KLEENE'] def __init__(self, itype, extra=None): self.type = itype @@ -209,7 +210,7 @@ def next_between(self, lbound, ubound): class StratCompiler: """Compiler of strategy expressions""" - def __init__(self, m, ml, use_notify=False, ignore_one=False): + def __init__(self, m, ml, use_notify=False, use_kleene=False, ignore_one=False): # Metalevel module self.ml = ml # Object-level module where the strategy lives @@ -219,6 +220,8 @@ def __init__(self, m, ml, use_notify=False, ignore_one=False): self.use_notify = use_notify # Whether the one combinator is ignored or not self.use_one = not ignore_one + # Whether to delimit iterations with the Kleene instruction + self.use_kleene = use_kleene # Table of strategy combinators self.op_table = {} @@ -453,22 +456,34 @@ def disj(self, s, p, tail): def ne_iter(self, s, p, tail): initial_pc = p.pc + if self.use_kleene: + p.append(Instruction.KLEENE, (initial_pc, True)) + # The non-empty iteration executes the body and then jumps # to the next instruction or to the body again self.generate(next(s.arguments()), p, False) p.append(Instruction.JUMP, (p.pc + 1, initial_pc)) + if self.use_kleene: + p.append(Instruction.KLEENE, (initial_pc, False)) + def iter(self, s, p, tail): # The empty iteration does the same with an additional initial jump initial_jump = p.append(Instruction.JUMP) initial_pc = p.pc + if self.use_kleene: + p.append(Instruction.KLEENE, (initial_pc, True)) + self.generate(next(s.arguments()), p, False) initial_jump.extra = (p.pc + 1, initial_pc) p.append(Instruction.JUMP, (p.pc + 1, initial_pc)) + if self.use_kleene: + p.append(Instruction.KLEENE, (initial_pc, False)) + def cond(self, s, p, tail): condition, true_branch, false_branch = s.arguments() @@ -907,7 +922,7 @@ def does_rewrite(inst): visited.add(next_state) dfs_stack.append(next_state) - # The reachable field has been calculated assumming that calls do not apply rewrites, + # The reachable field has been calculated assuming that calls do not apply rewrites, # but we can consider they do if every definition for it applies a rewrite # has_rewrite_strats holds for each strategy the definitions that do not apply a rewrite @@ -979,7 +994,7 @@ def does_rewrite(inst): jump_over_notify = [] # Jumps that should be added to skip notifies # Blocks that carry a notify to the block in the key notifiers = {} - # Blocks that jump to to the block in the key without address + # Blocks that jump to the block in the key without address not_notifiers = {} # Backward jumps are always non-notifying @@ -1198,6 +1213,13 @@ def add_to_seen_table(self, pc, term, value): self.seen[(pc, term, self.venv)] = value + def __eq__(self, other): + """Deep comparison of stack nodes""" + return self.pc == other.pc and self.venv == other.venv and self.parent == other.parent + + def __hash__(self): + return hash((self.pc, self.venv, self.parent)) + def __repr__(self): return f'StackNode({self.venv}, {self.pc})' @@ -1215,6 +1237,12 @@ def __init__(self, parent=None, index=0, subs=None, context=None): # Matching context self.context = context + def __eq__(self, other): + return self is other + + def __hash__(self): + return id(self) + def __repr__(self): return f'RwcNode({self.venv}, index={self.index})' @@ -1239,6 +1267,13 @@ def progress(self, var, value, pc): pending=self.pending[1:], done={**self.done, **{var: value}}, seen=self.seen.fork((pc, value))) + def __eq__(self, other): + return type(other) is type(self) and self.context == other.context and \ + self.done == other.done and len(self.pending) == len(other.pending) + + def __hash__(self): + return hash((self.context, self.donde, len(self.pending), super())) + def __repr__(self): return f'SubtermNode({self.venv}, {self.context}, {self.done}, {self.pending})' @@ -1353,12 +1388,17 @@ def __init__(self, program, term, state_class=State, seen_class=set): Instruction.WMATCHREW: self.wmatchrew, Instruction.ONE: self.one, Instruction.CHECKPOINT: self.checkpoint, + Instruction.KLEENE: self.kleene, } + # Number of rewrites + self.nr_rewrites = 0 + def reset(self, term): """Reset the runner with a given initial term""" self.current_state = self.state_class(term, 0, self.stack_root) + self.nr_rewrites = 0 self.pending.clear() def dump_state(self): @@ -1481,7 +1521,7 @@ def get_rewrites(self, args, stack): initial_subs = {var: stack.venv.instantiate(value) for var, value in initial_subs.items()} for value in initial_subs.values(): - value.reduce() + self.nr_rewrites += value.reduce() initial_subs = maude.Substitution(initial_subs) @@ -1489,10 +1529,15 @@ def get_rewrites(self, args, stack): initial_subs, maxDepth=-1 if top else maude.UNBOUNDED) + def reduced(self, t): + """Return the given term reduced and count the rewrites""" + self.nr_rewrites += t.reduce() + 1 + return t + def rlapp(self, args, stack): """Apply a rule""" - self.pending += [self.current_state.copy(term=(t.reduce(), t)[1]) + self.pending += [self.current_state.copy(term=self.reduced(t)) for t, *_ in self.get_rewrites(args, stack)] self.next_pending() @@ -1550,8 +1595,7 @@ def choice(self, args, stack): except ValueError: self.next_pending() - @staticmethod - def compute_weights(weights, venv): + def compute_weights(self, weights, venv): """Obtain the weights of a choice""" # Instantiate and reduce the weights @@ -1559,7 +1603,7 @@ def compute_weights(weights, venv): weights = [venv.instantiate(w) for w in weights] for w in weights: - w.reduce() + self.nr_rewrites += w.reduce() # Convert the weights to Python's float # (unreduced weights will be silently converted to zero) @@ -1578,7 +1622,7 @@ def do_call(self, args, stack): # Instantiate the call term with the variable context if stack.venv: call = stack.venv.instantiate(call) - call.reduce() + self.nr_rewrites += call.reduce() # Match the call term with every definition pending = [] @@ -1661,7 +1705,7 @@ def wmatchrew(self, args, stack): # Instantiated weight this_weight = merged_subs.instantiate(weight) - this_weight.reduce() + self.nr_rewrites += this_weight.reduce() match_data.append((merged_subs, context)) weights.append(float(this_weight)) @@ -1683,7 +1727,7 @@ def wmatchrew(self, args, stack): # Start evaluating the first subterm self.current_state = self.current_state.copy(term=merged_subs.instantiate(variables[0]), - stack=new_stack) + stack=new_stack) @staticmethod def process_match(venv, match, ctx, pattern, variables): @@ -1739,7 +1783,7 @@ def rwcstart(self, args, stack): initial_subs = {var: stack.venv.instantiate(value) for var, value in initial_subs.items()} for value in initial_subs.values(): - value.reduce() + self.nr_rewrites += value.reduce() initial_subs_obj = maude.Substitution(initial_subs) @@ -1758,7 +1802,7 @@ def rwcstart(self, args, stack): new_stack = RwcNode(parent=stack, index=k, subs=subs, context=(ctx(hole), hole)) # Start rewriting the left-hand side of the first condition fragment new_term = subs.instantiate(rwc_lhs) - new_term.reduce() + self.nr_rewrites += new_term.reduce() self.pending.append(self.current_state.copy(term=new_term, stack=new_stack)) self.next_pending() @@ -1781,12 +1825,12 @@ def rwcnext(self, args, stack): if is_final: context, hole = stack.context new_term = maude.Substitution({hole: subs.instantiate(rwc_lhs)}).instantiate(context) - new_term.reduce() + self.nr_rewrites += new_term.reduce() self.pending.append(self.current_state.copy(term=new_term, stack=stack.parent)) else: new_stack = RwcNode(parent=stack.parent, index=stack.index, subs=subs, context=stack.context) new_term = subs.instantiate(rwc_lhs) - new_term.reduce() + self.nr_rewrites += new_term.reduce() self.pending.append(self.current_state.copy(term=new_term, stack=new_stack)) self.next_pending() @@ -1801,7 +1845,7 @@ def sample(self, args, stack): # Reduce them for arg in dargs: - arg.reduce() + self.nr_rewrites += arg.reduce() dargs = [float(arg) for arg in dargs] @@ -1825,6 +1869,12 @@ def checkpoint(self, args, stack): # Do nothing (subclasses will) self.current_state.pc += 1 + def kleene(self, args, stack): + """Keep track of iterations""" + + # Do nothing (subclasses will) + self.current_state.pc += 1 + def rebuild_term(term, stack, args): """Rebuild the term within nested matchrews""" @@ -1848,7 +1898,7 @@ def rebuild_term(term, stack, args): subs = maude.Substitution({ # ...the subterms that have already been rewritten, and... **mrew_stack.done, - # ..the current and the pending subterms. + # ...the current and the pending subterms. **dict(zip(pending_vars, [new_term] + mrew_stack.pending)) }) # Rebuild the subterm @@ -1882,6 +1932,35 @@ def copy(self, term=None, pc=None, stack=None, conditional=False, graph_node=Non self.extra if extra is None else extra, ) + def reset_extra(self): + """Reset the extra field""" + pass # subclasses will + + +class GraphState: + """State of the rewrite graph""" + + def __init__(self, term): + self.term = term + # Set of graph states that follow by a rewrite + self.children = set() + # Temporary information about the last rewrite + self.last_rewrite = None + self.actions = {} + self.solution = False + self.valid = True + # Each graph state has its own list of pending execution states + self.pending = [] + # Subsearches for which a solution is reachable from here + self.solve_subsearch = set() + + @property + def has_children(self): + return self.children + + def __repr__(self): + return f'GraphState({self.term}, {self.children}, {self.solution})' + class BadProbStrategy(Exception): """Bad probabilitistic strategy that cannot engender MDPs or DTMCs""" @@ -1906,40 +1985,14 @@ def __repr__(self): return f'SubsearchNode(id={self.subsearch_id}, dfs_base={self.dfs_base})' -class MarkovRunner(StratRunner): - """Runner that extracts a DTMC or MDP""" - - class GraphState: - """State of the graph - - In addition to the actual states of the graph, there may be temporary fake - states used to gather the evolutions of the branches of a choice. They are - characterized by a None value in their term attribute. - """ - - def __init__(self, term): - self.term = term - # Set of graph states that follow by a rewrite - self.children = set() - # Set of choice alternatives (each an association of - # weights or probabilities to graph states) - self.child_choices = set() - # Temporary information about the last rewrite - self.last_rewrite = None - self.actions = {} - self.solution = False - self.valid = True - # Each graph state has its own list of pending execution states - self.pending = [] - # Subsearches for which a solution is reachable from here - self.solve_subsearch = set() - - def __repr__(self): - return f'GraphState({self.term}, {self.children}, {self.child_choices}, {self.solution})' +class GraphRunner(StratRunner): + """Runner that extracts a graph""" - def __init__(self, program, term): - super().__init__(program, term, state_class=GraphExecutionState, seen_class=dict) - self.root_node = self.GraphState(term) + def __init__(self, program, term, state_class=GraphExecutionState, graph_state_class=GraphState): + super().__init__(program, term, state_class=state_class, seen_class=dict) + # Class of the states of the graph + self.graph_state_class = graph_state_class + self.root_node = graph_state_class(term) self.dfs_stack = [self.root_node] # A dictionary from execution states to graph states: the latter @@ -1951,59 +2004,13 @@ def __init__(self, program, term): # different sucessor can be reached) self.solution_states = {} - def resolve_choice(self, choice, actions): - """Resolve a choice with weights into probabilities""" - - # While choice is a sequence of (weight, state), new_choice is - # a dictionary from state to probability - new_choice = {} - - for w, s in choice: - if not s.valid: - continue - - # If s is not a fake state - if s.term is not None: - old_w = new_choice.get(s, 0.0) - new_choice[s] = old_w + w - - else: - # Nondeteterministic and choice alternatives - nd_opts, ch_opts = len(s.children), len(s.child_choices) - - if nd_opts + ch_opts > 1: - raise BadProbStrategy - - # Copy the action information - for target, info in s.actions.items(): - old_info = actions.get(target) - - if old_info: - old_info.extend(info) - else: - actions[target] = info - - if nd_opts: - s, = s.children - old_w = new_choice.get(s, 0.0) - new_choice[s] = old_w + w - - if ch_opts: - child_choice, = s.child_choices - total_cw = sum(child_choice.values()) - for cs, cw in child_choice.items(): - old_w = new_choice.get(cs, 0.0) - new_choice[cs] = old_w + cw * w / total_cw - - return new_choice - def get_solution_state(self, term): """Get the solution state for the given term""" solution_state = self.solution_states.get(term) if not solution_state: - solution_state = self.GraphState(term) + solution_state = self.graph_state_class(term) self.solution_states[term] = solution_state return solution_state @@ -2028,7 +2035,7 @@ def next_pending(self): return True # This execution state is linked to a fake choice-generated graph state - # that should be pused to the DFS stack + # that should be pushed to the DFS stack elif push_state: self.dfs_stack.append(push_state) self.pending = push_state.pending @@ -2038,37 +2045,24 @@ def next_pending(self): return True # Check whether the graph state is valid - graph_state.valid = graph_state.solution or graph_state.children or graph_state.child_choices + graph_state.valid = graph_state.solution or graph_state.has_children # Link a solution state if there are children # (these states are needed to explicit the self-loop for the stuttering # extension of finite traces without introducing spurious executions) - if graph_state.solution and (graph_state.children or graph_state.child_choices) and \ + if graph_state.solution and graph_state.has_children and \ graph_state not in graph_state.children: solution_state = self.get_solution_state(graph_state.term) graph_state.children.add(solution_state) graph_state.actions[solution_state] = None - # Adjust the probilities of the choice operators - new_choices = [] - - for choice in graph_state.child_choices: - resolved_choice = self.resolve_choice(choice, graph_state.actions) - - if len(resolved_choice) == 1: - child, = resolved_choice.keys() - graph_state.children.add(child) - - elif resolved_choice: - new_choices.append(resolved_choice) - - graph_state.child_choices = tuple(new_choices) + self._on_state_exhausted(graph_state) self.dfs_stack.pop() if self.dfs_stack: dfs_top = self.dfs_stack[-1] - self.pending = dfs_top.pending + self.pending = self.dfs_stack[-1].pending # Add graph_state as a child if it is valid if graph_state.valid and graph_state.term is not None: @@ -2080,6 +2074,9 @@ def next_pending(self): self.current_state = None return False + def _on_state_exhausted(self, graph_state): + pass # nothing to do here + def pop(self, _, stack): """Return from a strategy call or similar construct""" @@ -2095,9 +2092,9 @@ def pop(self, _, stack): else: graph_state = self.dfs_stack[-1] - # Fake states are not marked as solutions but added a - # solution state as a child (this is also done later to - # marked states unless they do not have successors) + # Fake states (used in the subclass MarkovRunner) are not marked + # as solutions but added a solution state as a child (this is also + # done later to marked states unless they do not have successors) if graph_state.term is None: graph_state.children.add(self.get_solution_state(self.current_state.term)) else: @@ -2105,6 +2102,202 @@ def pop(self, _, stack): self.next_pending() + def notify(self, args, stack): + """Record a transition in the graph""" + + state = self.current_state + state.pc += 1 + + # Check whether this state has already been visited + successor = stack.already_seen_table(state.pc, state.term) + + # This is a new state, so add it to the graph + if successor is None: + new_term = rebuild_term(state.term, stack, args) + + new_state = self.graph_state_class(new_term) + stack.add_to_seen_table(state.pc, state.term, new_state) + self.dfs_stack.append(new_state) + self.pending = new_state.pending + + # The extra information for the last rewrite is recorded + self.dfs_stack[-2].last_rewrite = state.extra + state.reset_extra() + + else: + if successor.valid: + dfs_top = self.dfs_stack[-1] + dfs_top.children.add(successor) + dfs_top.actions.setdefault(successor, []).append(state.extra) + + state.reset_extra() + + # Handle the deactivation of the negative branch of + # a subsearch when this state leaded to a solution + to_be_solved = len(successor.solve_subsearch) + + while stack and to_be_solved: + subsearch_id = getattr(stack, 'subsearch_id', None) + if subsearch_id in successor.solve_subsearch: + stack.pc = None + to_be_solved -= 1 + stack = stack.parent + + self.next_pending() + + def checkpoint(self, args, stack): + """Check whether this state has been visited and interrupt the execution""" + + if stack.already_seen_table(self.current_state.pc, self.dfs_stack[-1]): + self.next_pending() + + else: + stack.add_to_seen_table(self.current_state.pc, self.dfs_stack[-1], True) + self.current_state.pc += 1 + + def subsearch(self, args, stack): + """Start a subsearch by pushing a stack node with continuation""" + + # The same as StratRunner.subsearch, but forking the seen set. Moreover, + # the size of the DFS stack is recorded to allow finding out which states + # lead to solutions within the search (identified by the current PC) + subsearch_stack = SubsearchNode(parent=stack, pc=args, + seen=stack.seen.fork(self.current_state.pc), + dfs_base=len(self.dfs_stack), + subsearch_id=self.current_state.pc) + self.current_state = self.current_state.copy(stack=subsearch_stack) + + # Exactly the same as StratRunner.subsearch + self.pending.append(self.current_state.copy(pc=args, stack=subsearch_stack, conditional=True)) + + def nofail(self, args, stack): + """Pop the stack and discard the continuation on failure""" + + # Annotate the graph states with the current subsearch, + # for which they provide a solution + for node in self.dfs_stack[stack.dfs_base:]: + node.solve_subsearch.add(stack.subsearch_id) + + super().nofail(args, stack) + + def rlapp(self, args, stack): + """Apply a rule""" + + # Like the parent implementation, but the rule is recorded + self.pending += [self.current_state.copy(term=self.reduced(t), extra=rl) + for t, _, _, rl in self.get_rewrites(args, stack)] + + self.next_pending() + + def run(self): + """Run the strategy to generate the graph""" + + self.solution = None + self.pending = self.root_node.pending + + while self.current_state: + state = self.current_state + + # The instruction to be executed + inst = self.code[state.pc] + + self.handlers[inst.type](inst.extra, state.stack) + + return self.root_node, self.nr_rewrites + + +class MarkovRunner(GraphRunner): + """Runner that extracts a DTMC or MDP""" + + class GraphState(GraphState): + """State of the graph + + In addition to the actual states of the graph, there may be temporary fake + states used to gather the evolutions of the branches of a choice. They are + characterized by a None value in their term attribute. + """ + + def __init__(self, term): + super().__init__(term) + + # Set of choice alternatives (each an association of + # weights or probabilities to graph states) + self.child_choices = set() + + @property + def has_children(self): + return self.children or self.child_choices + + def __repr__(self): + return f'GraphState({self.term}, {self.children}, {self.child_choices}, {self.solution})' + + def __init__(self, program, term): + super().__init__(program, term, graph_state_class=self.GraphState) + + def resolve_choice(self, choice, actions): + """Resolve a choice with weights into probabilities""" + + # While choice is a sequence of (weight, state), new_choice is + # a dictionary from state to probability + new_choice = {} + + for w, s in choice: + if not s.valid: + continue + + # If s is not a fake state + if s.term is not None: + old_w = new_choice.get(s, 0.0) + new_choice[s] = old_w + w + + else: + # Nondeterministic and choice alternatives + nd_opts, ch_opts = len(s.children), len(s.child_choices) + + if nd_opts + ch_opts > 1: + raise BadProbStrategy + + # Copy the action information + for target, info in s.actions.items(): + old_info = actions.get(target) + + if old_info: + old_info.extend(info) + else: + actions[target] = info + + if nd_opts: + s, = s.children + old_w = new_choice.get(s, 0.0) + new_choice[s] = old_w + w + + if ch_opts: + child_choice, = s.child_choices + total_cw = sum(child_choice.values()) + for cs, cw in child_choice.items(): + old_w = new_choice.get(cs, 0.0) + new_choice[cs] = old_w + cw * w / total_cw + + return new_choice + + def _on_state_exhausted(self, graph_state): + """When a graph state is exhausted""" + + # Adjust the probabilities of the choice operators + new_choices = [] + + for choice in graph_state.child_choices: + resolved_choice = self.resolve_choice(choice, graph_state.actions) + + if len(resolved_choice) == 1: + child, = resolved_choice.keys() + graph_state.children.add(child) + + elif resolved_choice: + new_choices.append(resolved_choice) + + graph_state.child_choices = tuple(new_choices) + def choice(self, args, stack): """A choice node""" @@ -2161,7 +2354,7 @@ def wmatchrew(self, args, stack): # Instantiated weight this_weight = merged_subs.instantiate(weight) - this_weight.reduce() + self.nr_rewrites += this_weight.reduce() this_weight = float(this_weight) if this_weight > 0.0: @@ -2242,65 +2435,6 @@ def notify(self, args, stack): self.next_pending() - def checkpoint(self, args, stack): - """Check whether this state has been visited and interrupt the execution""" - - if stack.already_seen_table(self.current_state.pc, self.dfs_stack[-1]): - self.next_pending() - - else: - stack.add_to_seen_table(self.current_state.pc, self.dfs_stack[-1], True) - self.current_state.pc += 1 - - def subsearch(self, args, stack): - """Start a subsearch by pushing a stack node with continuation""" - - # The same as StratRunner.subsearch, but forking the seen set. Moreover, - # the size of the DFS stack is recorded to allow finding out which states - # lead to solutions within the search (identified by the current PC) - subsearch_stack = SubsearchNode(parent=stack, pc=args, - seen=stack.seen.fork(self.current_state.pc), - dfs_base=len(self.dfs_stack), - subsearch_id=self.current_state.pc) - self.current_state = self.current_state.copy(stack=subsearch_stack) - - # Exactly the same as StratRunner.subsearch - self.pending.append(self.current_state.copy(pc=args, stack=subsearch_stack, conditional=True)) - - def nofail(self, args, stack): - """Pop the stack and discard the continuation on failure""" - - # Annotate the graph states with the current subsearch, - # for which they provides a solution - for node in self.dfs_stack[stack.dfs_base:]: - node.solve_subsearch.add(stack.subsearch_id) - - super().nofail(args, stack) - - def rlapp(self, args, stack): - """Apply a rule""" - - self.pending += [self.current_state.copy(term=(t.reduce(), t)[1], extra=rl) - for t, _, _, rl in self.get_rewrites(args, stack)] - - self.next_pending() - - def run(self): - """Run the strategy to generate the graph""" - - self.solution = None - self.pending = self.root_node.pending - - while self.current_state: - state = self.current_state - - # The instruction to be executed - inst = self.code[state.pc] - - self.handlers[inst.type](inst.extra, state.stack) - - return self.root_node - class MetadataRunner(MarkovRunner): """Runner for the metadata assignment method with non-ground weights""" @@ -2319,7 +2453,7 @@ def rlapp(self, args, stack): for t, sb, _, rl in self.get_rewrites(args, stack): # Term.apply does not normalize output terms - t.reduce() + self.nr_rewrites += t.reduce() + 1 # Evaluate the metadata weight weight = self.stmt_map.get(rl, 1.0) @@ -2327,7 +2461,7 @@ def rlapp(self, args, stack): # If it is not a literal, we should reduce the term if not isinstance(weight, float): weight = sb.instantiate(weight) - weight.reduce() + self.nr_rewrites += weight.reduce() weight = float(weight) self.pending.append(self.current_state.copy(term=t, extra=(rl, weight))) @@ -2338,7 +2472,7 @@ def rlapp(self, args, stack): class RandomRunner(StratRunner): """Runner that resolves every choice locally at random without backtracking. - Instead of solutions of the strategy, the run method returns the succesive steps + Instead of solutions of the strategy, the run method returns the successive steps of a single random rewriting path. Hence, conditionals do no work with this runner, since exploration is not exhaustive, and failed executions are not discarded.""" @@ -2355,7 +2489,7 @@ def detect_nondeterminism(self, usermsgs): subsearches, trivial_subsearch = [], False for k, inst in enumerate(self.code.inst): - # Jumps with multiple desinations + # Jumps with multiple destinations if inst.type == Instruction.JUMP and len(inst.extra) > 1: inst.extra = inst.extra[:1] usermsgs.print_warning(f'Unquantified nondeterminism detected in {current_name}. ' @@ -2396,9 +2530,9 @@ def next_pending(self): return False # Otherwise, a pending state is chosen at random and all other pending - # states are discarded. Indeed, pending states are not actually pending but + # states are discarded. Indeed, pending states are not actually pending, but # they have just been generated by a nondeterministic instruction (rule - # application, call, matchrew...) before calling this method. Reimplemeting + # application, call, matchrew...) before calling this method. Reimplementing # these instructions is avoided by this trick. self.current_state = random.choice(self.pending) self.pending.clear() diff --git a/umaudemc/webui.py b/umaudemc/webui.py index 3306f66..2e839b6 100644 --- a/umaudemc/webui.py +++ b/umaudemc/webui.py @@ -2,7 +2,6 @@ # Web-based user interface # -import cgi import http.server import json import math @@ -156,10 +155,10 @@ class RequestHandler(http.server.BaseHTTPRequestHandler): """Object charged of handling the requests""" STATIC_FILES = { - '/' : ('select.htm', 'text/html; charset=utf-8'), - '/smcview.css' : ('smcview.css', 'text/css; charset=utf-8'), - '/smcview.js' : ('smcview.js', 'text/javascript; charset=utf-8'), - '/smcgraph.js' : ('smcgraph.js', 'text/javascript; charset=utf-8'), + '/' : ('select.htm', 'text/html; charset=utf-8'), + '/smcview.css' : ('smcview.css', 'text/css; charset=utf-8'), + '/smcview.js' : ('smcview.js', 'text/javascript; charset=utf-8'), + '/smcgraph.js' : ('smcgraph.js', 'text/javascript; charset=utf-8'), } def do_GET(self): @@ -176,12 +175,11 @@ def do_GET(self): self.send_error(404) def do_POST(self): - form = cgi.FieldStorage(fp=self.rfile, headers=self.headers, - environ={'REQUEST_METHOD': 'POST', - 'CONTENT_TYPE': self.headers['Content-Type']}) + # Read the JSON body of the request + form = json.loads(self.rfile.read(int(self.headers['Content-Length']))) - question = form.getvalue('question') - url = form.getvalue('url', None) + question = form.get('question') + url = form.get('url', None) if question == 'ls': base, parent, dirs, files = self.server.info.path_handler.browse_dir(url) @@ -194,10 +192,10 @@ def do_POST(self): self.end_headers() response = { - 'base' : base, - 'parent' : parent, - 'dirs' : dirs, - 'files' : files + 'base' : base, + 'parent' : parent, + 'dirs' : dirs, + 'files' : files } self.wfile.write(json.dumps(response).encode('utf-8')) elif question == 'sourceinfo': @@ -217,16 +215,16 @@ def do_POST(self): self.send_response(200) self.send_header('Content-Type', 'text/json; charset=utf-8') self.end_headers() - mod = form.getvalue('mod') + mod = form.get('mod') minfo = self.server.info.remote.getModuleInfo(mod) response = { - 'name' : mod, - 'type' : minfo['type'], - 'params' : [], - 'valid' : minfo['valid'], - 'stateSorts' : minfo.get('state', []), - 'strategies' : [self.make_signature(signat) for signat in minfo.get('strat', ())], - 'props' : [self.make_signature(signat) for signat in minfo.get('prop', ())] + 'name' : mod, + 'type' : minfo['type'], + 'params' : [], + 'valid' : minfo['valid'], + 'stateSorts' : minfo.get('state', []), + 'strategies' : [self.make_signature(signat) for signat in minfo.get('strat', ())], + 'props' : [self.make_signature(signat) for signat in minfo.get('prop', ())] } self.wfile.write(json.dumps(response).encode('utf-8')) elif question == 'modelcheck': @@ -234,13 +232,13 @@ def do_POST(self): self.send_header('Content-Type', 'text/json; charset=utf-8') self.end_headers() data = { - 'module': form.getvalue('mod'), - 'initial': form.getvalue('initial'), - 'formula': form.getvalue('formula'), - 'strat': form.getvalue('strategy'), - 'opaques': form.getvalue('opaques'), - 'passign': self.make_passign(form), - 'reward': form.getvalue('reward', None), + 'module' : form.get('mod'), + 'initial' : form.get('initial'), + 'formula' : form.get('formula'), + 'strat' : form.get('strategy'), + 'opaques' : form.get('opaques'), + 'passign' : self.make_passign(form), + 'reward' : form.get('reward', None), } result = self.server.info.remote.modelCheck(data) response = { @@ -267,7 +265,7 @@ def do_POST(self): self.wfile.write(json.dumps(response).encode('utf-8')) elif question == 'wait': - mcref = int(form.getvalue('mcref')) + mcref = int(form.get('mcref')) # Model checking is actually done here result = self.server.info.remote.get_result(mcref) @@ -327,16 +325,16 @@ def make_signature(signat): def make_passign(form): """Build a passign term from its name and argument""" - name = form.getvalue('pmethod', None) + name = form.get('pmethod', None) if name is None: return None - argument = form.getvalue('pargument', '') + argument = form.get('pargument', '') # Add mdp- prefix when MDP is selected and admissible can_mdp = name not in ('uaction', 'strategy') - mdp = 'mdp-' if can_mdp and form.getvalue('mdp') == 'true' else '' + mdp = 'mdp-' if can_mdp and form.get('mdp') == 'true' else '' return f'{mdp}{name}({argument})' if argument else f'{mdp}{name}' diff --git a/umaudemc/wrappers.py b/umaudemc/wrappers.py index 3889cce..7c10f26 100644 --- a/umaudemc/wrappers.py +++ b/umaudemc/wrappers.py @@ -11,6 +11,8 @@ def default_getNextStates(self, stateNr): + """Generator of all the successors of a state""" + index = 0 next_state = self.getNextState(stateNr, index) @@ -20,10 +22,38 @@ def default_getNextStates(self, stateNr): next_state = self.getNextState(stateNr, index) +def standard_getTransitions(self, stateNr): + """Generator of all the transitions (target state and rule) of a rewrite graph""" + + index = 0 + next_state = self.getNextState(stateNr, index) + + while next_state != -1: + yield next_state, self.getRule(stateNr, next_state) + index = index + 1 + next_state = self.getNextState(stateNr, index) + + +def strategy_getTransitions(self, stateNr): + """Generator of all the transitions of a strategy-controlled rewrite graph""" + + index = 0 + next_state = self.getNextState(stateNr, index) + + while next_state != -1: + yield next_state, self.getTransition(stateNr, next_state) + index = index + 1 + next_state = self.getNextState(stateNr, index) + + # Add getNextStates to the original graphs maude.RewriteGraph.getNextStates = default_getNextStates maude.StrategyRewriteGraph.getNextStates = default_getNextStates +# Add getTransitions to the original graphs +maude.RewriteGraph.getTransitions = standard_getTransitions +maude.StrategyRewriteGraph.getTransitions = strategy_getTransitions + # Add a property to know whether the graph is strategy-controlled maude.RewriteGraph.strategyControlled = False maude.StrategyRewriteGraph.strategyControlled = True @@ -50,6 +80,9 @@ def getStateStrategy(self, stateNr): def getTransition(self, *args): return self.graph.getTransition(*args) + def getTransitions(self, stateNr): + return self.graph.getTransitions(stateNr) + def getNrStates(self): return self.graph.getNrStates() @@ -113,6 +146,11 @@ def getNextStates(self, stateNr): if self.valid_states[next_state]: yield next_state + def getTransitions(self, stateNr): + for next_state, edge in self.graph.getTransitions(stateNr): + if self.valid_states[next_state]: + yield next_state, edge + class MergedGraph: """A graph where states are merged""" @@ -141,6 +179,10 @@ def getTransition(self, origin, dest): return trans return None + def getTransitions(self, stateNr): + for next_state in self.getNextStates(stateNr): + yield next_state, self.getTransition(stateNr, next_state) + def getNrStates(self): return len(self.states) @@ -252,7 +294,7 @@ def getNextStates(self, stateNr): yield next_state -def wrapGraph(graph, purge_fails, merge_states): +def wrap_graph(graph, purge_fails, merge_states): """Wrap graphs according to the model modification options""" if purge_fails == 'yes': graph = FailFreeGraph(graph) @@ -277,4 +319,4 @@ def create_graph(term=None, strategy=None, opaque=(), full_matchrew=False, purge # Wrap the graph with the model modification for branching-time purge_fails, merge_states = default_model_settings(logic, purge_fails, merge_states, strategy, tableau=tableau) - return wrapGraph(graph, purge_fails, merge_states) + return wrap_graph(graph, purge_fails, merge_states)