Completely remove the concept of 'statespace nature', mostly unused

src/lib/AlgoAGnot.ml

@@ -129,13 +129,6 @@ class algoAGnot (model : AbstractModel.abstract_model) (options : Options.imitat
 			| None -> raise (InternalError ("Termination status not set in " ^ self#algorithm_name ^ ".compute_result"))
 			| Some status -> status
 		in
-
-(*		(* The tile nature is good if 1) it is not bad, and 2) the analysis terminated normally *)
-		let statespace_nature =
-			if statespace_nature = StateSpace.Unknown && termination_status = Regular_termination then StateSpace.Good
-			(* Otherwise: unchanged *)
-			else statespace_nature
-		in*)
 
 		(* Constraint is exact if termination is normal, possibly over-approximated otherwise (as it is the negation of a possible under-approximation of the bad constraint) *)
 		(*** NOTE/TODO: technically, if the constraint is true/false, its soundness can be further refined easily ***)

src/lib/AlgoEFopt.ml

@@ -444,9 +444,6 @@ class virtual algoEFopt (model : AbstractModel.abstract_model) (options : Option
 			(* If this is really a new state, or a state larger than a former state *)
 			| StateSpace.New_state new_state_index | StateSpace.State_replacing new_state_index ->
 
-				(* First check whether this is a bad tile according to the property and the nature of the state *)
-				self#update_statespace_nature new_state;
-
 				(* Will the state be added to the list of new states (the successors of which will be computed)? *)
 
 				(* Add the state_index to the list of new states (used to compute their successors at the next iteration) *)

src/lib/AlgoEFtminQueue.ml

@@ -851,10 +851,6 @@ if options#best_worst_case then (self#state_index_to_max_time suc_id) else
 		(* If this is really a new state, or a state larger than a former state *)
 		| StateSpace.New_state new_state_index | StateSpace.State_replacing new_state_index ->
 
-			(* First check whether this is a bad tile according to the property and the nature of the state *)
-			(*** NOTE: in fact not necessary for this algorithm ***)
-			self#update_statespace_nature new_state;
-
 			(* Add the state_index to the list of new states (used to compute their successors at the next iteration) *)
 			new_states_indexes <- new_state_index :: new_states_indexes;
 

src/lib/AlgoEUgen.ml

@@ -234,9 +234,6 @@ class virtual algoEUgen (model : AbstractModel.abstract_model) (options : Option
 		(* If this is really a new state, or a state larger than a former state *)
 		| StateSpace.New_state new_state_index | StateSpace.State_replacing new_state_index ->
 
-			(* First check whether this is a bad tile according to the property and the nature of the state *)
-			self#update_statespace_nature new_state;
-
 			(* Will the state be added to the list of new states (the successors of which will be computed)? *)
 			(*** NOTE: if the answer is false, then the new state is a target state ***)
 			(*** BADPROG: ugly bool ref that may be updated in an IF condition below ***)

src/lib/AlgoIM.ml

@@ -86,13 +86,6 @@ class algoIM (model : AbstractModel.abstract_model) (options : Options.imitator_
 			| Some status -> status
 		in
 
-		(* The state space nature is good if 1) it is not bad, and 2) the analysis terminated normally *)
-		let statespace_nature =
-			if statespace_nature = StateSpace.Unknown && termination_status = Regular_termination then StateSpace.Good
-			(* Otherwise: unchanged *)
-			else statespace_nature
-		in
-
 		(* Constraint is… *)
 		let soundness = 
 			let dangerous_inclusion = options#comparison_operator = AbstractAlgorithm.Inclusion_check || options#comparison_operator = AbstractAlgorithm.Including_check || options#comparison_operator = AbstractAlgorithm.Double_inclusion_check in
@@ -107,13 +100,7 @@ class algoIM (model : AbstractModel.abstract_model) (options : Options.imitator_
 			else Constraint_maybe_invalid
 		in
 
-		let result = match statespace_nature with
-			(*** NOTE: if a safety property is defined and if the state space reaches some unsafe states, then the constraint is considered as bad.
-	In any other case (safe state space, or no safety property defined), the constraint nature is considered as good. ***)
-			(*** NOTE: this can probably not happen anymore as there is no property in the model (ÉA, 2020/09/09) ***)
-			| StateSpace.Good | StateSpace.Unknown -> Good_constraint(LinearConstraint.p_nnconvex_constraint_of_p_linear_constraint p_constraint, soundness)
-			| StateSpace.Bad -> Bad_constraint(LinearConstraint.p_nnconvex_constraint_of_p_linear_constraint p_constraint, soundness)
-		in
+		let result = Good_constraint(LinearConstraint.p_nnconvex_constraint_of_p_linear_constraint p_constraint, soundness) in
 
 		(* Return result *)
 		Point_based_result
@@ -127,9 +114,6 @@ class algoIM (model : AbstractModel.abstract_model) (options : Options.imitator_
 			(* Explored state space *)
 			state_space			= state_space;
 
-			(* Nature of the state space *)
-(* 			statespace_nature	= statespace_nature; *)
-
 			(* Number of random selections of pi-incompatible inequalities performed *)
 (* 			nb_random_selections= nb_random_selections; *)
 

src/lib/AlgoIMK.ml

@@ -260,9 +260,6 @@ class algoIMK (model : AbstractModel.abstract_model) (options : Options.imitator
 				);*)
 
 
-				(* First check whether this is a bad tile according to the property and the nature of the state *)
-				self#update_statespace_nature new_state;
-
 				(* Add the state_index to the list of new states (used to compute their successors at the next iteration) *)
 				new_states_indexes <- new_state_index :: new_states_indexes;
 
@@ -381,21 +378,10 @@ class algoIMK (model : AbstractModel.abstract_model) (options : Options.imitator
 			| Some status -> status
 		in
 
-		(* The state space nature is good if 1) it is not bad, and 2) the analysis terminated normally *)
-		(*** NOTE: unsure of this computation (if it has any meaning for this algorithm anyway) ***)
-		let statespace_nature =
-			if statespace_nature = StateSpace.Unknown && termination_status = Regular_termination then StateSpace.Good
-			(* Otherwise: unchanged *)
-			else statespace_nature
-		in
-
 		(* Constraint is exact if termination is normal, possibly over-approximated otherwise (as there may be pi-incompatible inequalities missing) *)
 		let soundness = if termination_status = Regular_termination then Constraint_exact else Constraint_maybe_over in
 
-		let result = match statespace_nature with
-			| StateSpace.Good | StateSpace.Unknown -> Good_constraint(LinearConstraint.p_nnconvex_constraint_of_p_linear_constraint p_constraint, soundness)
-			| StateSpace.Bad -> Bad_constraint(LinearConstraint.p_nnconvex_constraint_of_p_linear_constraint p_constraint, soundness)
-		in
+		let result = Good_constraint(LinearConstraint.p_nnconvex_constraint_of_p_linear_constraint p_constraint, soundness) in
 
 		(* Return result *)
 		Point_based_result

src/lib/AlgoIMcomplete.ml

@@ -143,13 +143,6 @@ class algoIMcomplete (model : AbstractModel.abstract_model) (options : Options.i
 			| Some status -> status
 		in
 
-		(* The state space nature is good if 1) it is not bad, and 2) the analysis terminated normally *)
-		let statespace_nature =
-			if statespace_nature = StateSpace.Unknown && termination_status = Regular_termination then StateSpace.Good
-			(* Otherwise: unchanged *)
-			else statespace_nature
-		in
-
 		(* Constraint is… *)
 		let soundness =
 			let dangerous_inclusion = options#comparison_operator = AbstractAlgorithm.Inclusion_check || options#comparison_operator = AbstractAlgorithm.Including_check || options#comparison_operator = AbstractAlgorithm.Double_inclusion_check in
@@ -162,12 +155,7 @@ class algoIMcomplete (model : AbstractModel.abstract_model) (options : Options.i
 			else Constraint_maybe_invalid
 		in
 
-		let result = match statespace_nature with
-			(*** NOTE: if a safety property is defined and if the state space reaches some unsafe states, then the constraint is considered as bad.
-	In any other case (safe state space, or no safety property defined), the constraint nature is considered as good. ***)
-			| StateSpace.Good | StateSpace.Unknown -> Good_constraint(k_result, soundness)
-			| StateSpace.Bad -> Bad_constraint(k_result, soundness)
-		in
+		let result =  Good_constraint(k_result, soundness) in
 
 		(* Return result *)
 		Point_based_result
@@ -181,9 +169,6 @@ class algoIMcomplete (model : AbstractModel.abstract_model) (options : Options.i
 			(* Explored state space *)
 			state_space			= state_space;
 
-			(* Nature of the state space *)
-(* 			statespace_nature	= statespace_nature; *)
-
 			(* Total computation time of the algorithm *)
 			computation_time	= time_from start_time;
 

src/lib/AlgoIMunion.ml

@@ -107,21 +107,10 @@ class algoIMunion (model : AbstractModel.abstract_model) (options : Options.imit
 			| Some status -> status
 		in
 
-		(* The state space nature is good if 1) it is not bad, and 2) the analysis terminated normally *)
-		(*** NOTE: unsure of this computation (if it has any meaning for this algorithm anyway) ***)
-		let statespace_nature =
-			if statespace_nature = StateSpace.Unknown && termination_status = Regular_termination then StateSpace.Good
-			(* Otherwise: unchanged *)
-			else statespace_nature
-		in
-
 		(* Constraint is exact if termination is normal, unknown otherwise (on the one hand, pi-incompatible inequalities (that would restrain the constraint) may be missing, and on the other hand union of good states (that would enlarge the constraint) may be missing too) *)
 		let soundness = if termination_status = Regular_termination then Constraint_exact else Constraint_maybe_invalid in
 
-		let synthesized_constraint = match statespace_nature with
-			| StateSpace.Good | StateSpace.Unknown -> Good_constraint(synthesized_constraint, soundness)
-			| StateSpace.Bad -> Bad_constraint(synthesized_constraint, soundness)
-		in
+		let synthesized_constraint = Good_constraint(synthesized_constraint, soundness) in
 
 		(* Return result *)
 		Point_based_result

src/lib/AlgoNDFS.ml

@@ -1248,10 +1248,6 @@ class algoNDFS (model : AbstractModel.abstract_model) (options : Options.imitato
 		(* If this is really a new state, or a state larger than a former state *)
 		| StateSpace.New_state new_state_index | StateSpace.State_replacing new_state_index ->
 
-			(* First check whether this is a bad tile according to the property and the nature of the state *)
-			(*** NOTE: in fact not necessary for this algorithm ***)
-			self#update_statespace_nature new_state;
-
 			(* Add the state_index to the list of new states (used to compute their successors at the next iteration) *)
 			new_states_indexes <- new_state_index :: new_states_indexes;
 

src/lib/AlgoPRP.ml

@@ -171,9 +171,6 @@ class algoPRP (model : AbstractModel.abstract_model) (options : Options.imitator
 			(* If this is really a new state, or a state larger than a former state *)
 			| StateSpace.New_state new_state_index | StateSpace.State_replacing new_state_index ->
 
-				(* First check whether this is a bad tile according to the property and the nature of the state *)
-				self#update_statespace_nature new_state;
-
 				(* Will the state be added to the list of new states (the successors of which will be computed)? *)
 				let to_be_added = self#process_pi0_compatible_state new_state in
 
@@ -306,27 +303,21 @@ class algoPRP (model : AbstractModel.abstract_model) (options : Options.imitator
 			| Some status -> status
 		in
 
-		(* The state space nature is good if 1) it is not bad, and 2) the analysis terminated normally;
-			It is bad if any bad state was met. *)
-		let statespace_nature =
-			if statespace_nature = StateSpace.Unknown && termination_status = Regular_termination then StateSpace.Good
-			(* Otherwise: unchanged *)
-			else statespace_nature
-		in
-
-		(* Constraint is... *)
+		(* Constraint is… *)
 		let soundness =
 			(* EXACT if termination is normal, whatever the state space nature is *)
 			if termination_status = Regular_termination then Constraint_exact
 			(* POSSIBLY UNDERAPPROXIMATED if state space nature is bad and termination is not normal *)
-			else if statespace_nature = StateSpace.Bad then Constraint_maybe_under
+			else if bad_state_found then Constraint_maybe_under
 			(* INVALID if state space nature is good and termination is not normal *)
 			else Constraint_maybe_invalid
 		in
 
-		let result = match statespace_nature with
-			| StateSpace.Good | StateSpace.Unknown -> Good_constraint(result, soundness)
-			| StateSpace.Bad -> Bad_constraint(result, soundness)
+		let result = if bad_state_found
+			then
+				Bad_constraint(result, soundness)
+			else
+				Good_constraint(result, soundness)
 		in
 
 		(* Return result *)

src/lib/AlgoPostStar.ml

@@ -69,10 +69,6 @@ class algoPostStar (model : AbstractModel.abstract_model) (options : Options.imi
 		(* If this is really a new state, or a state larger than a former state *)
 		| StateSpace.New_state new_state_index | StateSpace.State_replacing new_state_index ->
 
-			(* First check whether this is a bad tile according to the property and the nature of the state *)
-			(*** NOTE: in fact not necessary for this algorithm ***)
-			self#update_statespace_nature new_state;
-
 			(* Add the state_index to the list of new states (used to compute their successors at the next iteration) *)
 			new_states_indexes <- new_state_index :: new_states_indexes;
 
@@ -126,22 +122,12 @@ class algoPostStar (model : AbstractModel.abstract_model) (options : Options.imi
 			| Some status -> status
 		in
 
-		(* The state space nature is good if 1) it is not bad, and 2) the analysis terminated normally *)
-		let statespace_nature =
-			if statespace_nature = StateSpace.Unknown && termination_status = Regular_termination then StateSpace.Good
-			(* Otherwise: unchanged *)
-			else statespace_nature
-		in
-
 		(* Return result *)
 		State_space_computation_result
 		{
 			(* Explored state space *)
 			state_space			= state_space;
 
-			(* Nature of the state space *)
-			statespace_nature	= statespace_nature;
-
 			(* Total computation time of the algorithm *)
 			computation_time	= time_from start_time;
 

src/lib/AlgoStateBased.ml

@@ -2537,10 +2537,6 @@ class virtual algoStateBased (model : AbstractModel.abstract_model) (options : O
 	(*** TODO: better have some option, or better initialize it to the good value from now on ***)
 	val mutable state_space : StateSpace.stateSpace = new StateSpace.stateSpace 0
 
-	(** Nature of the state space according to a property *)
-	val mutable statespace_nature = StateSpace.Unknown
-
-
 (*	(* Clock that may be reset at each transition *)
 	val mutable reset_clock : Automaton.clock_index option = None*)
 
@@ -2736,7 +2732,7 @@ class virtual algoStateBased (model : AbstractModel.abstract_model) (options : O
 			false
 		)
 
-
+(*
 	(*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*)
 	(* Update the nature of the trace set *)
 	(*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*)
@@ -2791,7 +2787,7 @@ class virtual algoStateBased (model : AbstractModel.abstract_model) (options : O
 					(* Cannot conclude anything from a single state yet *)
 					()
 
-		)
+		)*)
 
 
 

src/lib/AlgoStateBased.mli

@@ -196,9 +196,6 @@ class virtual algoStateBased : AbstractModel.abstract_model -> Options.imitator_
 		(*** TODO: make private (while accessible to subclasses ***)
 		val mutable state_space : StateSpace.stateSpace
 
-		(** Nature of the state space according to a property *)
-		val mutable statespace_nature : StateSpace.statespace_nature
-
 		(* Function to be called from the distributed IMITATOR *)
 		(*** TODO: make private (while accessible to subclasses ***)
 		val mutable patator_termination_function : (unit -> unit) option
@@ -278,12 +275,6 @@ class virtual algoStateBased : AbstractModel.abstract_model -> Options.imitator_
 		method check_whether_px_included_into_synthesized_constraint : LinearConstraint.px_linear_constraint -> bool
 
 
-		(*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*)
-		(** Update the nature of the trace set *)
-		(*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*)
-		method update_statespace_nature : State.state -> unit
-
-
 		(*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*)
 		(** Simple Boolean denoting whether we should abort if the initial state is unsatisfiable (basically, we should always abort, except for Validity-synthesis) *)
 		(*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*)