Kleene-star graph with the builtin implementation, removed Gtk UI, mi…

…nor changes
fadoss · Jan 5, 2024 · ef6a53b · ef6a53b
1 parent bd23553
commit ef6a53b
Show file tree

Hide file tree

Showing 26 changed files with 831 additions and 884 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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-')