Implement EG as the negation of AF

RELEASES.md

@@ -6,12 +6,14 @@
 ### Major features
 * Updates are now fully sequential in the model, including clock updates; **WARNING**: this might result in backward-incompatibility for elaborate models involving discrete and continuous updates in the same transition.
 * New user-defined functions: imperative instructions, function calls, definition of local variables, variable shadowing…
-* New AG ("global invariant") algorithm
+* New AG ("global invariant") algorithm, implemented as the negation of EF
 * New EU ("Exists … until") algorithm
+* New EW ("exists … weak until") algorithm
 * New AF ("always eventually") algorithm, and variants:
 	- AR ("always … release")
 	- AU ("always … until")
 	- AW ("always … weak until")
+	- EG ("exists globally"), implemented as the negation of AF
 * New timed variants of EF, EU, AF, AR, AU, AW
 
 ### Syntax improvement

doc/IMITATOR-user-manual.tex

@@ -2294,6 +2294,19 @@ \section{Unavoidability synthesis: \styleTCTL{AF}, \styleTCTL{AU}, \styleTCTL{AR
 These algorithms work recursively using a depth-first search (DFS), as formalized in~\cite{JLR15}.
 
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\section{Exists-globally synthesis: \styleTCTL{EG}}\label{section:algorithm:EG}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+The property syntax is as follows:
+
+\begin{IMITATORproperty}
+property := #synth EG (state_predicate);
+\end{IMITATORproperty}
+
+\styleTCTL{EG} is implemented exactly as the negation of the result of \styleTCTL{AF} called on the negation of the state predicate.
+See \cref{section:algorithm:AF}.
+
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \section{Timed CTL}\label{section:algorithm:timedCTL}
@@ -2968,6 +2981,7 @@ \section{Summary}\label{section:algorithm:summary}
 			Unavoidability                 & \styleIMI{A(sp\_1)R(sp\_2)}               & \cellYes{} & \cellNo{}  & \cellNo{} \\
 			Unavoidability                 & \styleIMI{A(sp\_1)U(sp\_2)}               & \cellYes{} & \cellNo{}  & \cellNo{} \\
 			Unavoidability                 & \styleIMI{A(sp\_1)W(sp\_2)}               & \cellYes{} & \cellNo{}  & \cellNo{} \\
+			Exists-globally                & \styleIMI{EG(state\_predicate)}               & \cellYes{} & \cellNo{}  & \cellNo{} \\
 
 			% Cycles
 
@@ -3076,6 +3090,7 @@ \section{Summary}\label{section:algorithm:summary}
 			Unavoidability           & \styleIMI{A(sp\_1)R(sp\_2)}                  & \cellNo{} & \styleOption{equality} \\
 			Unavoidability           & \styleIMI{A(sp\_1)U(sp\_2)}                  & \cellNo{} & \styleOption{equality} \\
 			Unavoidability           & \styleIMI{A(sp\_1)W(sp\_2)}                  & \cellNo{} & \styleOption{equality} \\
+			Exists globally          & \styleIMI{EG(state\_predicate)}                  & \cellNo{} & \styleOption{equality} \\
 
 			% Cycles
 
@@ -3886,7 +3901,7 @@ \chapter{List of options}\label{chapter:options}
 This explains why this option, while preserving the correctness, is not default for reachability algorithms.
 \end{description}
 
-In reachability algorithms (\cref{section:algorithm:EFsynth,section:algorithm:AGnot,section:algorithm:AG,section:algorithm:EFmin,section:algorithm:EFmax,section:algorithm:EFopt,section:algorithm:EU,section:algorithm:patterns,section:algorithm:PRP}), \styleOption{-comparison inclusion} is usually enabled by default; however, for loop synthesis algorithms (\cref{section:algorithm:LoopSynth,section:algorithm:Zeno}) and for unavoidability (\cref{section:algorithm:AF}, \styleOption{-comparison equality} is used, as inclusion may introduce spurious cycles.
+In reachability algorithms (\cref{section:algorithm:EFsynth,section:algorithm:AGnot,section:algorithm:AG,section:algorithm:EFmin,section:algorithm:EFmax,section:algorithm:EFopt,section:algorithm:EU,section:algorithm:patterns,section:algorithm:PRP}), \styleOption{-comparison inclusion} is usually enabled by default; however, for loop synthesis algorithms (\cref{section:algorithm:LoopSynth,section:algorithm:Zeno}) and for unavoidability (\cref{section:algorithm:AF,section:algorithm:EG}, \styleOption{-comparison equality} is used, as inclusion may introduce spurious cycles.
 %
 See \cref{table:summary:options} for the default behavior of algorithms \wrt{} this option.
 
@@ -5573,6 +5588,7 @@ \section{Grammar of the property file}\label{section:grammar-property}
 	$|$ & \styleIMI{AGnot} \nt{state\_predicate}                                                                               \\
 	$|$ & \styleIMI{AG} \nt{state\_predicate}                                                                               \\
 	$|$ & \styleIMI{E} \styleIMI{(} \nt{state\_predicate} \styleIMI{)} \styleIMI{U} \styleIMI{(} \nt{state\_predicate} \styleIMI{)} \\
+	$|$ & \styleIMI{E} \styleIMI{(} \nt{state\_predicate} \styleIMI{)} \styleIMI{W} \styleIMI{(} \nt{state\_predicate} \styleIMI{)} \\
 
 	% Optimized reachability
 
@@ -5583,8 +5599,12 @@ \section{Grammar of the property file}\label{section:grammar-property}
 	% AF
 
 	$|$ & \styleIMI{AF} \styleIMI{(} \nt{state\_predicate} \styleIMI{)} \\
+	$|$ & \styleIMI{A} \styleIMI{(} \nt{state\_predicate} \styleIMI{)} \styleIMI{R} \styleIMI{(} \nt{state\_predicate} \styleIMI{)} \\
 	$|$ & \styleIMI{A} \styleIMI{(} \nt{state\_predicate} \styleIMI{)} \styleIMI{U} \styleIMI{(} \nt{state\_predicate} \styleIMI{)} \\
 	$|$ & \styleIMI{A} \styleIMI{(} \nt{state\_predicate} \styleIMI{)} \styleIMI{W} \styleIMI{(} \nt{state\_predicate} \styleIMI{)} \\
+	$|$ & \styleIMI{EG} \styleIMI{(} \nt{state\_predicate} \styleIMI{)} \\
+
+	% TODO: add supported timed CTL operators
 
 	% Cycles
 

src/bin/IMITATOR.ml

@@ -802,9 +802,8 @@ match options#imitator_mode with
 			(************************************************************)
 			(* Exists globally *)
 			(************************************************************)
-			| EG _ (* state_predicate *) ->
-				raise (NotImplemented("EG"))
-(* 				let myalgo :> AlgoGeneric.algoGeneric = new AlgoEU.algoEU model property options state_predicate_phi state_predicate_psi in myalgo *)
+			| EG state_predicate ->
+				let myalgo :> AlgoGeneric.algoGeneric = new AlgoAUgen.algoEG model property options state_predicate in myalgo
 
 			(************************************************************)
 			(* Exists release *)

src/lib/AlgoAUgen.ml

@@ -779,7 +779,7 @@ class virtual algoAUgen (model : AbstractModel.abstract_model) (property : Abstr
 		start_time <- Unix.gettimeofday();
 
 (* !!! NOTE : de-BUG !!! *)
-		print_warning "There is an unstability in AF, AU, AW and AR algorithms (presumably due to PPL) for sufficiently complex models and constraints. The analysis might crash with segmentation fault but, if it does not, then there is most probably no problem.";
+		print_warning "There is an instability in AF, AU, AW, AR and EG algorithms (presumably due to PPL) for sufficiently complex models and constraints. The analysis might crash with segmentation fault but, if it does not, then there is most probably no problem.";
 (* !!! NOTE : de-BUG !!! *)
 
 		(* Build initial state *)
@@ -906,6 +906,85 @@ end;;
 (************************************************************)
 (************************************************************)
 
+(************************************************************)
+(************************************************************)
+(* Class definition: EG *)
+(************************************************************)
+(************************************************************)
+(*** NOTE: EG is implemented as the negation of the result of AF called on the **negation** of the state predicate ***)
+class algoEG (model : AbstractModel.abstract_model) (property : AbstractProperty.abstract_property) (options : Options.imitator_options) (state_predicate : AbstractProperty.state_predicate) =
+	object (self) inherit algoAUgen model property options false None (State_predicate_term (State_predicate_factor (State_predicate_factor_NOT (State_predicate state_predicate)))) None (*as super*)
+
+
+	(************************************************************)
+	(* Class variables *)
+	(************************************************************)
+
+	(*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*)
+	(** Name of the algorithm *)
+	(*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*)
+	method algorithm_name = "EG"
+
+
+	(*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*)
+	(* Method packaging the result output by the algorithm *)
+	(*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*)
+	method! private compute_result =
+		(* Print some information *)
+		self#print_algo_message_newline Verbose_standard (
+			"Algorithm completed " ^ (after_seconds ()) ^ "."
+		);
+
+		(* Perform result = initial_state|P \ synthesized_constraint *)
+
+		(* Retrieve and copy the initial parameter constraint *)
+		let result : LinearConstraint.p_nnconvex_constraint = LinearConstraint.p_nnconvex_constraint_of_p_linear_constraint parameters_consistent_with_init in
+
+		if verbose_mode_greater Verbose_medium then(
+			self#print_algo_message Verbose_medium "As a reminder, the initial constraint is:";
+			self#print_algo_message Verbose_medium (LinearConstraint.string_of_p_nnconvex_constraint model.variable_names result);
+			self#print_algo_message Verbose_medium "As a reminder, the result constraint is:";
+			self#print_algo_message Verbose_medium (LinearConstraint.string_of_p_nnconvex_constraint model.variable_names synthesized_constraint);
+		);
+
+		(* Perform the difference *)
+		LinearConstraint.p_nnconvex_difference_assign result synthesized_constraint;
+
+		(* Projecting onto some parameters if required by the property *)
+		let result = AlgoStateBased.project_p_nnconvex_constraint_if_requested model property result in
+
+		(* Constraint is exact if termination is normal, possibly under-approximated otherwise *)
+		(*** TODO: double check ***)
+		let soundness = if property.synthesis_type = Synthesis && termination_status = Regular_termination then Constraint_exact else Constraint_maybe_invalid in
+
+		(* Return the result *)
+		Single_synthesis_result
+		{
+			(* Non-necessarily convex constraint guaranteeing the reachability of the desired states *)
+			result				= Good_constraint (result, soundness);
+
+			(* English description of the constraint *)
+			constraint_description = "constraint guaranteeing " ^ self#algorithm_name;
+
+			(* Explored state space *)
+			state_space			= state_space;
+
+			(* Total computation time of the algorithm *)
+			computation_time	= time_from start_time;
+
+			(* Termination *)
+			termination			= termination_status;
+		}
+
+
+(************************************************************)
+(************************************************************)
+end;;
+(************************************************************)
+(************************************************************)
+
+
+
 
 (************************************************************)
 (************************************************************)

src/lib/AlgoAUgen.mli

@@ -64,6 +64,28 @@ class algoAF : AbstractModel.abstract_model -> AbstractProperty.abstract_propert
 end
 
 
+(************************************************************)
+(* Class definition: EG *)
+(************************************************************)
+class algoEG : AbstractModel.abstract_model -> AbstractProperty.abstract_property -> Options.imitator_options -> AbstractProperty.state_predicate ->
+	object inherit algoAUgen
+		(************************************************************)
+		(* Class variables *)
+		(************************************************************)
+
+		(*------------------------------------------------------------*)
+		(** Name of the algorithm *)
+		(*------------------------------------------------------------*)
+		method algorithm_name : string
+
+
+		(************************************************************)
+		(* Class methods *)
+		(************************************************************)
+
+end
+
+
 (************************************************************)
 (* Class definition: AF (timed) *)
 (************************************************************)

tests/regression_tests_data.py

@@ -19441,7 +19441,7 @@
 	,
 
 	#*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-
-	# AF
+	# BEGIN : TEST AF
 	#*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-
 
 	#------------------------------------------------------------
@@ -20024,6 +20024,49 @@
 	} # end test case
 	#------------------------------------------------------------
 
+	#*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-
+	# END : TEST AF
+	#*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-
+
+	,
+
+	#*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-
+	# BEGIN : TEST EG
+	#*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-
+	#------------------------------------------------------------
+	{
+		# Test version             : 1
+		# Test author              : Étienne André
+		# Test since               : 2024/05/03
+		# Last modified            : 2024/05/03
+		# Test for IMITATOR version: 3.4
+		'purpose'    : 'Test EG: simple example',
+		'tags'       : 'EG,algorithm,semantic',
+		'input_files': ['EG/EG-simple.imi' , 'EG/EG-simple.imiprop'],
+		'options'    : '',
+		'expectations' : [
+			{'file': 'EG-simple.res' , 'content' : """
+BEGIN CONSTRAINT
+ p = 4
+OR
+  p = 2
+OR
+  p = 1
+END CONSTRAINT
+
+------------------------------------------------------------
+Constraint soundness                    : exact
+		"""
+			} # end result file
+			,
+		] # end expectations
+	} # end test case
+	#------------------------------------------------------------
+
+	#*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-
+	# END : TEST EG
+	#*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-
+
 	,
 
 	#------------------------------------------------------------

tests/testcases/EG/EG-simple.imi

@@ -0,0 +1,108 @@
+(************************************************************
+ *                                IMITATOR MODEL
+ *
+ * Title            : Simple example to test EG
+ * Description      : Simple example to test EG
+ * Correctness      : N/A
+ * Scalable         : no
+ * Generated        : no
+ * Categories       : toy
+ * Source           : Own work
+ * bibkey           : 
+ * Author           : Étienne André
+ * Modeling         : Étienne André
+ * Input by         : Étienne André
+ * License          : Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0)
+ *
+ * Created          : 2024/05/03
+ * Last modified    : 2024/05/03
+ * Model version    : 0.1
+ *
+ * IMITATOR version : 3.4-alpha
+ ************************************************************)
+
+var
+
+(* Clocks *)
+ 	x,
+		: clock;
+
+(* Discrete *)
+	i,
+		: int;
+
+(* Parameters *)
+	p,
+		: parameter;
+
+
+
+(************************************************************)
+  automaton pta
+(************************************************************)
+actions: ;
+
+loc l1: invariant x <= 4
+	when p = 1 goto l1;
+	when p = 2 goto l2;
+	when p = 3 goto l3;
+	when p = 4 goto l4;
+	(* To avoid a parameter deadlock in l1 *)
+	when True do {i := 1} goto lF;
+
+(* Timelock *)
+loc l2: invariant x <= 4
+	when x = 2 do {i := 1} goto lF;
+
+(* No timelock *)
+loc l3: invariant x <= 4
+	when x = 4 do {i := 1} goto lF;
+
+(* Livelock *)
+loc l4: invariant True
+	when x = 4 do {i := 1} goto lF;
+
+(* Bad location, with i=1 *)
+loc lF: invariant True
+
+end (* pta *)
+
+
+
+(************************************************************)
+(* Initial state *)
+(************************************************************)
+
+init := {
+
+    discrete =
+		(*------------------------------------------------------------*)
+		(* Initial location *)
+		(*------------------------------------------------------------*)
+		loc[pta] := l1,
+
+		(*------------------------------------------------------------*)
+		(* Initial discrete variables assignments *)
+		(*------------------------------------------------------------*)
+		i := 0,
+
+    ;
+
+    continuous =        
+		(*------------------------------------------------------------*)
+		(* Initial clock constraints *)
+		(*------------------------------------------------------------*)
+		& x = 0
+
+		(*------------------------------------------------------------*)
+		(* Parameter constraints *)
+		(*------------------------------------------------------------*)
+		& p >= 0
+	;
+}
+
+
+(************************************************************)
+(* The end *)
+(************************************************************)
+end

tests/testcases/EG/EG-simple.imiprop

@@ -0,0 +1 @@
+property := #synth EG (i=0);