Add parsing/converting/printing functionalities for AU algorithm

imitator-model-checker · Jan 26, 2024 · 5c97413 · 5c97413
1 parent 3167b75
commit 5c97413
Show file tree

Hide file tree

Showing 11 changed files with 64 additions and 10 deletions.
diff --git a/src/bin/IMITATOR.ml b/src/bin/IMITATOR.ml
@@ -791,6 +791,13 @@ match options#imitator_mode with
 			| AF state_predicate ->
 				let myalgo :> AlgoGeneric.algoGeneric = new AlgoAF.algoAF model property options state_predicate in myalgo
 
+			(************************************************************)
+			(* Always until *)
+			(************************************************************)
+			| AU (state_predicate_phi, state_predicate_psi) ->
+				let myalgo :> AlgoGeneric.algoGeneric = new AlgoAU.algoAU model property options state_predicate_phi state_predicate_psi in myalgo
+
+
 
 		(*------------------------------------------------------------*)
 		(* Optimized reachability *)

diff --git a/src/lib/AbstractProperty.mli b/src/lib/AbstractProperty.mli
@@ -86,7 +86,10 @@ type property =
 	(* Unavoidability *)
 	| AF of state_predicate
 
-
+	(* Always until *)
+	| AU of state_predicate * state_predicate
+
+
 	(*------------------------------------------------------------*)
 	(* Optimized reachability *)
 	(*------------------------------------------------------------*)

diff --git a/src/lib/AlgoAU.ml b/src/lib/AlgoAU.ml
@@ -26,7 +26,7 @@ open AlgoAUgen
 (* Class definition *)
 (************************************************************)
 (************************************************************)
-class algoAF (model : AbstractModel.abstract_model) (property : AbstractProperty.abstract_property) (options : Options.imitator_options) (state_predicate_phi : AbstractProperty.state_predicate) (state_predicate_psi : AbstractProperty.state_predicate) =
+class algoAU (model : AbstractModel.abstract_model) (property : AbstractProperty.abstract_property) (options : Options.imitator_options) (state_predicate_phi : AbstractProperty.state_predicate) (state_predicate_psi : AbstractProperty.state_predicate) =
 	object (*(self)*) inherit algoAUgen model property options (Some state_predicate_phi) state_predicate_psi (*as super*)
 
 

diff --git a/src/lib/AlgoAU.mli b/src/lib/AlgoAU.mli
@@ -21,7 +21,7 @@ open AlgoAUgen
 (************************************************************)
 (* Class definition *)
 (************************************************************)
-class algoAF : AbstractModel.abstract_model -> AbstractProperty.abstract_property -> Options.imitator_options -> AbstractProperty.state_predicate -> AbstractProperty.state_predicate ->
+class algoAU : AbstractModel.abstract_model -> AbstractProperty.abstract_property -> Options.imitator_options -> AbstractProperty.state_predicate -> AbstractProperty.state_predicate ->
 	object inherit algoAUgen
 		(************************************************************)
 		(* Class variables *)

diff --git a/src/lib/AlgorithmOptions.ml b/src/lib/AlgorithmOptions.ml
@@ -59,6 +59,10 @@ let default_state_comparison property : AbstractAlgorithm.state_comparison_opera
 	(*** TODO: decide heuristics ***)
 		-> Equality_check
 
+	(* Always until *)
+	| AU _
+	(*** TODO: decide heuristics ***)
+		-> Equality_check
 
 	(*------------------------------------------------------------*)
 	(* Optimized reachability *)
@@ -195,6 +199,12 @@ let is_state_comparison_correct (abstract_property : AbstractProperty.abstract_p
 		(* No inclusion allowed *)
 		-> state_comparison_operator = Equality_check || state_comparison_operator = No_check
 
+	(* Always until *)
+	| AU _
+		(*** TODO: decide heuristics ***)
+		(* No inclusion allowed *)
+		-> state_comparison_operator = Equality_check || state_comparison_operator = No_check
+
 	(*------------------------------------------------------------*)
 	(* Optimized reachability *)
 	(*------------------------------------------------------------*)
@@ -339,6 +349,10 @@ let merge_needed property =
 	(*** TODO: decide heuristics ***)
 		-> false
 
+	| AU _
+	(*** TODO: decide heuristics ***)
+		-> false
+
 	(*------------------------------------------------------------*)
 	(* Optimized reachability *)
 	(*------------------------------------------------------------*)
@@ -584,6 +598,8 @@ let supports_witness property =
 
 	(* Unavoidability *)
 	| AF _
+	(* Always until *)
+	| AU _
 		-> false
 
 	(*------------------------------------------------------------*)
@@ -780,6 +796,9 @@ let text_of_property property =
 	(* Unavoidability *)
 	| AF _ -> "unavoidability " ^ synthesis_or_witness
 
+	(* Always until *)
+	| AU _ -> "always until " ^ synthesis_or_witness
+
 	(*------------------------------------------------------------*)
 	(* Optimized reachability *)
 	(*------------------------------------------------------------*)

diff --git a/src/lib/Graphics.ml b/src/lib/Graphics.ml
@@ -157,6 +157,7 @@ let get_v0_option = function
 			| AG _
 			| EU _
 			| AF _
+			| AU _
 			| EFpmin _
 			| EFpmax _
 			| EFtmin _
@@ -1109,7 +1110,9 @@ let dot_of_statespace (model : AbstractModel.abstract_model) (property_option :
 				| Win (state_predicate)
 					-> [state_predicate]
 
-				| EU (state_predicate_1, state_predicate_2) -> [state_predicate_1; state_predicate_2]
+				| EU (state_predicate_1, state_predicate_2)
+				| AU (state_predicate_1, state_predicate_2)
+					-> [state_predicate_1; state_predicate_2]
 
 				| Cycle_through_generalized state_predicate_list
 					-> state_predicate_list

diff --git a/src/lib/ModelConverter.ml b/src/lib/ModelConverter.ml
@@ -1892,6 +1892,7 @@ let check_property_option (useful_parsing_model_information : useful_parsing_mod
 
 		(* Until *)
 		| Parsed_EU (parsed_state_predicate_phi, parsed_state_predicate_psi)
+		| Parsed_AU (parsed_state_predicate_phi, parsed_state_predicate_psi)
 			->
 			evaluate_and
 				(check_parsed_state_predicate useful_parsing_model_information parsed_state_predicate_phi)
@@ -2222,7 +2223,7 @@ let convert_property_option (useful_parsing_model_information : useful_parsing_m
 			,
 			None
 
-		(* Until *)
+		(* Exists until *)
 		| Parsed_EU (parsed_state_predicate_phi, parsed_state_predicate_psi)
 			->
 			(* Return a property and no observer *)
@@ -2240,6 +2241,17 @@ let convert_property_option (useful_parsing_model_information : useful_parsing_m
 			,
 			None
 
+		(* Always until *)
+		| Parsed_AU (parsed_state_predicate_phi, parsed_state_predicate_psi)
+			->
+			(* Return a property and no observer *)
+			AU
+				(PropertyConverter.convert_state_predicate useful_parsing_model_information parsed_state_predicate_phi
+				,
+				PropertyConverter.convert_state_predicate useful_parsing_model_information parsed_state_predicate_psi)
+			,
+			None
+
 
 		(*------------------------------------------------------------*)
 		(* Optimized reachability *)

diff --git a/src/lib/ModelPrinter.ml b/src/lib/ModelPrinter.ml
@@ -1007,6 +1007,9 @@ let string_of_abstract_property model property =
 		(* Unavoidability *)
 		| AF state_predicate -> "AF(" ^ (string_of_state_predicate model state_predicate) ^ ")"
 
+		(* Always until *)
+		| AU (state_predicate_phi, state_predicate_psi) -> "A(" ^ (string_of_state_predicate model state_predicate_phi) ^ ")U(" ^ (string_of_state_predicate model state_predicate_psi) ^ ")"
+
 		(*------------------------------------------------------------*)
 		(* Optimized reachability *)
 		(*------------------------------------------------------------*)

diff --git a/src/lib/ParsingStructure.mli b/src/lib/ParsingStructure.mli
@@ -388,13 +388,16 @@ type parsed_property_type =
 	(* Global invariant *)
 	| Parsed_AG of parsed_state_predicate
 
-	(* Until *)
+	(* Exists until *)
 	| Parsed_EU of parsed_state_predicate * parsed_state_predicate
 
 	(* Unavoidability *)
 	| Parsed_AF of parsed_state_predicate
 
-
+	(* Always until *)
+	| Parsed_AU of parsed_state_predicate * parsed_state_predicate
+
+
 	(*------------------------------------------------------------*)
 	(* Optimized reachability *)
 	(*------------------------------------------------------------*)

diff --git a/src/lib/PropertyLexer.mll b/src/lib/PropertyLexer.mll
@@ -45,14 +45,14 @@ rule token = parse
  	| "#synth"         { CT_SYNTH }
 
  	(* Keywords for properties *)
+	| "A"              { CT_A }
 	| "AccCycle"       { CT_ACCEPTINGCYCLE }
 	| "AcceptingCycle" { CT_ACCEPTINGCYCLE }
 	| "AccLoop"        { CT_ACCEPTINGCYCLE }
 	| "AcceptingLoop"  { CT_ACCEPTINGCYCLE }
 	| "AF"             { CT_AF }
 	| "AG"             { CT_AG }
 	| "AGnot"          { CT_AGnot }
- 	| "DeadlockFree"   { CT_DEADLOCKFREE }
  	| "BCcover"        { CT_COVERCARTOGRAPHY }
  	| "BClearn"        { CT_BCLEARN }
  	| "BCshuffle"      { CT_BCSHUFFLE }
@@ -61,6 +61,7 @@ rule token = parse
  	| "BCrandomseq"    { CT_BCRANDOMSEQ }
 	| "Cycle"          { CT_INFCYCLE }
 	| "CycleThrough"   { CT_INFCYCLETHROUGH }
+ 	| "DeadlockFree"   { CT_DEADLOCKFREE }
 	| "EF"             { CT_EF }
 	| "E"              { CT_E }
 	| "EFpmax"         { CT_EFpmax }

diff --git a/src/lib/PropertyParser.mly b/src/lib/PropertyParser.mly
@@ -53,7 +53,7 @@ let resolve_property l =
 %token COLON COMMA DOUBLEDOT SEMICOLON SYMBOL_AND SYMBOL_OR
 
 %token
-	CT_ACCEPTING CT_ACCEPTINGCYCLE CT_AF CT_AG CT_AGnot CT_ALWAYS
+	CT_A CT_ACCEPTING CT_ACCEPTINGCYCLE CT_AF CT_AG CT_AGnot CT_ALWAYS
 	CT_BCBORDER CT_BCLEARN CT_BCRANDOM CT_BCRANDOMSEQ CT_BCSHUFFLE CT_BEFORE
 	CT_COVERCARTOGRAPHY
 	CT_DEADLOCKFREE
@@ -145,12 +145,15 @@ property:
 	/* Global invariant */
 	| CT_AG state_predicate { Parsed_AG $2 }
 
-	/* Until */
+	/* Exists until */
 	| CT_E state_predicate CT_U state_predicate { Parsed_EU ($2, $4) }
 
 	/* Unavoidability */
 	| CT_AF state_predicate { Parsed_AF $2 }
 
+	/* Always until */
+	| CT_A state_predicate CT_U state_predicate { Parsed_AU ($2, $4) }
+
 
 	/*------------------------------------------------------------*/
 	/* Optimized reachability */