(************************************************************
 *
 *                       IMITATOR
 * 
 * Université Sorbonne Paris Nord, LIPN, CNRS, France
 * Université de Lorraine, CNRS, Inria, LORIA, Nancy, France
 * 
 * Module description: Behavioral Cartography with exhaustive coverage of integer points and learning-based abstraction.
 * 
 * File contributors : Étienne André
 * Created           : 2016/07/22
 *
 ************************************************************)


(************************************************************)
(************************************************************)
(* Modules *)
(************************************************************)
(************************************************************)
open ImitatorUtilities
open Exceptions
open AbstractModel
open Result
open AlgoBCCover
open Statistics


(************************************************************)
(************************************************************)
(* Constants related to the interfacing with the learning programs *)
(************************************************************)
(************************************************************)

let interface_script_name = "interfaceCV.py"

(* Strings to be present at the first line of the file name generated by the learning-based program *)
let string_ABSTRACTION = "===ABSTRACTION==="
let string_COUNTEREXAMPLE = "===COUNTEREXAMPLE==="


(************************************************************)
(************************************************************)
(* Class-indepdendent types *)
(************************************************************)
(************************************************************)
type learning_result =
	| Abstraction
	| CounterExample

(************************************************************)
(************************************************************)
(* Class definition *)
(************************************************************)
(************************************************************)
class algoBCCoverLearning (model : AbstractModel.abstract_model) (property : AbstractProperty.abstract_property) (options : Options.imitator_options) (state_predicate : AbstractProperty.state_predicate) (v0 : HyperRectangle.hyper_rectangle) (step : NumConst.t) (algo_instance_function : (PVal.pval -> AlgoStateBased.algoStateBased)) (tiles_manager_type : AlgoCartoGeneric.tiles_storage) =
	object (self) inherit algoBCCover model property options v0 step algo_instance_function tiles_manager_type (*as super*)
	
	(************************************************************)
	(* Class variables *)
	(************************************************************)

	(** Backup the original model *)
	val original_model : AbstractModel.abstract_model = model

	(** Backup the original model file names *)
	val original_file = options#model_file_name
	val original_files_prefix = options#files_prefix
	
	val counter_interface = create_hybrid_counter_and_register "learning" Algorithm_counter Verbose_standard
	val counter_reparsing = create_hybrid_counter_and_register "learning: re-parsing" Algorithm_counter Verbose_standard
	
	val counter_learning_abstractions = create_discrete_counter_and_register "abstractions learnt" Algorithm_counter Verbose_standard
	val counter_learning_counterexamples = create_discrete_counter_and_register "counter-examples learnt" Algorithm_counter Verbose_standard
	
	
	(************************************************************)
	(* Class methods *)
	(************************************************************)

	(*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*)
	(** Name of the algorithm *)
	(*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*)
	method! algorithm_name = "BC (full coverage with learning-based abstraction)"

	
	(*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*)
	(** Call the algorithm on the current point: 1) run the abstraction 2) call either EFsynth or PRP depending on the result *)
	(*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*)
	method! call_point _ =
		(* Retrieve the current point *)
		let current_point = self#get_current_point_option in

		
		(*------------------------------------------------------------*)
		(* 1) Call the python script interfacing with the learning tool *)
		(*------------------------------------------------------------*)
		
		(* Create the file name for the model generated by learning *)
		let learning_based_model_filename_prefix = options#files_prefix ^ "_learning_" ^ (string_of_int current_iteration) in
		let learning_based_model_filename = learning_based_model_filename_prefix ^ "" ^ Constants.model_extension in
		
		(* Format the pi0 so that it is in the form param1=value1,param2=value2… *)
		let format_pi0 pi0 = 
			let pi0_string = ModelPrinter.string_of_pval model pi0 in
			(* Remove spaces *)
			(*** TODO: replace with a generic blank space… ***)
			let pi0_string = Str.global_replace (Str.regexp " ") "" pi0_string in
			let pi0_string = Str.global_replace (Str.regexp "\n") "" pi0_string in
			let pi0_string = Str.global_replace (Str.regexp "\t") "" pi0_string in
			(* Replace '&' with ',' *)
			let pi0_string = Str.global_replace (Str.regexp "&") "," pi0_string in
			(* Return *)
			pi0_string
		in
		
		(* Try to locate the interace script (and raises an exception if not found) *)
		let interface_script_path =

		(* Locate the current directory *)
		let current_dir = (Sys.getcwd ()) ^ "/" in
		
		(* Print some information *)
		print_message Verbose_medium ("Current directory: '" ^ current_dir ^ "'.");
		
		(* First try in the same directory *)
		if Sys.file_exists (current_dir ^ interface_script_name) then(
			print_message Verbose_low ("Interfacing script '" ^ interface_script_name ^ "' successfully found in the current directory.");
			current_dir ^ interface_script_name
		)
		(* Else try in the IMITATOR binary directory *)
		else if Sys.file_exists (Constants.path_to_program ^ interface_script_name) then(
			print_message Verbose_low ("Interfacing script '" ^ interface_script_name ^ "' successfully found in the " ^ (Constants.program_name) ^ " directory.");
			Constants.path_to_program ^ interface_script_name
		)
		(* Else try in the parent dir of the IMITATOR binary directory *)
		else if Sys.file_exists (Constants.path_to_program ^ "../" ^ interface_script_name) then(
			print_message Verbose_low ("Interfacing script '" ^ interface_script_name ^ "' successfully found in the parent directory of the " ^ (Constants.program_name) ^ " directory.");
			Constants.path_to_program ^ "../" ^ interface_script_name
		)
		(* Else not found *)
		else(
			raise (InternalError ("Interfacing script '" ^ interface_script_name ^ "' not found. Make sure this file is either in the current directory ('" ^ (current_dir) ^ "'), or in the same directory as the " ^ (Constants.program_name) ^ " binary ('" ^ (Constants.path_to_program) ^ "'), or in its parent directory ('" ^ (Constants.path_to_program ^ "../") ^ "')."))
		) in
		 
		(* Prepare command *)
		let script_line = "python " ^ interface_script_path
			(* 1st argument: input model *)
			^ " " ^ options#model_file_name
			(* 2nd argument: output model name *)
			^ " " ^ learning_based_model_filename
			(* 3rd argument: pi0 *)
			^ " " ^ (format_pi0 current_point) ^ ""
		 in
		 
		(* Print some information *)
		print_message Verbose_standard ("Executing: '" ^ script_line ^ "'");
		
		(* Call the script *)
		counter_interface#increment;
		counter_interface#start;
		let execution = Sys.command script_line in
		counter_interface#stop;
		if execution <> 0 then
			raise (InternalError ("Something went wrong in the command.\nExit code: " ^ (string_of_int execution) ^ ".\nCommand: '" ^ script_line ^ "'"))
		else
			print_message Verbose_low ("Script terminated successfully");
		
		
		(*------------------------------------------------------------*)
		(* 2) Check that the output file was correctly generated *)
		(*------------------------------------------------------------*)
		
		if not (Sys.file_exists learning_based_model_filename) then(
			print_error ("File '" ^ learning_based_model_filename ^ "' not found!");
			raise (InterfacingError ("The file '" ^ learning_based_model_filename ^ "' that should have been generated by learning could not be found."))
		);
		
		
		(*------------------------------------------------------------*)
		(* 3) Find out whether this is a counter-example or an abstraction *)
		(*------------------------------------------------------------*)
		
		(* Read first line of the file *)
		let first_line = OCamlUtilities.read_first_line_from_file learning_based_model_filename in
		
		(* Remove comments and look for text *)
		let analysis_type =
			if Str.string_match (Str.regexp (".*(\\*\\(" ^ string_ABSTRACTION ^ "\\)\\*).*")) first_line 0 then(
				(* Statistics *)
				counter_learning_abstractions#increment;
				Abstraction
			)
			else if Str.string_match (Str.regexp (".*(\\*\\(" ^ string_COUNTEREXAMPLE ^ "\\)\\*).*")) first_line 0 then(
				(* Statistics *)
				counter_learning_counterexamples#increment;
				CounterExample
			)
			else(
				print_error ("First line not recognized: " ^ first_line);
				raise (InterfacingError ("The type of the analysis (that should have been at the first line of the file generated by '" ^ interface_script_name ^ "') could not be recognized"))
			)
		in
		
		(* Print some information *)
		print_message Verbose_standard ("Model generated by learning: " ^ (match analysis_type with | Abstraction -> "abstraction" | CounterExample -> "counter-example"));
		

		(*------------------------------------------------------------*)
		(* 4) Parse and set the new model *)
		(*------------------------------------------------------------*)
		
		(* Set model name and model prefix name (needed before compiling!) *)
		options#set_file learning_based_model_filename;
		options#set_files_prefix learning_based_model_filename_prefix;
		
		counter_reparsing#increment;
		counter_reparsing#start;
		let new_model, _ = ParsingUtility.compile_model_and_property options in
		counter_reparsing#stop;
		
		(* Print some information *)
		print_message Verbose_standard ("Original model: " ^ (string_of_int original_model.nb_automata) ^ " automata. New model: " ^ (string_of_int new_model.nb_automata) ^ "");
		
		
		(*------------------------------------------------------------*)
		(* 5) Call the proper algorithm *)
		(*------------------------------------------------------------*)
		
		(* Save the verbose mode as it may be modified *)
		let global_verbose_mode = get_verbose_mode() in

		(* Prevent the verbose messages (except in verbose medium, high or total) *)
		(*------------------------------------------------------------*)
		if not (verbose_mode_greater Verbose_medium) then
			set_verbose_mode Verbose_mute;

		(* Select the right algorithm according to the analysis type *)
		let algo_instance = match analysis_type with
			(* If counter-exemple: run EF on the parametric trace *)
			| CounterExample -> let myalgo :> AlgoStateBased.algoStateBased = new AlgoEF.algoEF new_model {synthesis_type = Synthesis; property = EF state_predicate; projection = (*** TODO: if one day one allows for projection on cartography ***) None} options state_predicate in myalgo
			
			(* If abstraction: run PRP on this abstraction *)
			(*** NOTE: the current valuation (current_point) is already set in Input ***)
			| Abstraction -> let myalgo :> AlgoStateBased.algoStateBased = new AlgoPRP.algoPRP new_model {synthesis_type = Synthesis; property = PRP(state_predicate, current_point); projection = (*** TODO: if one day one allows for projection on cartography ***) None} options current_point state_predicate in myalgo
		in
		current_algo_instance <- algo_instance;
		
		(* Run! *)
		let imitator_result : imitator_result = current_algo_instance#run in
		
		(* Create auxiliary files with the proper file prefix, if requested *)
		self#create_auxiliary_files imitator_result;

		(* Get the verbose mode back *)
		set_verbose_mode global_verbose_mode;
		(*------------------------------------------------------------*)

		
		(*------------------------------------------------------------*)
		(* 6) Remove the temporary model *)
		(*------------------------------------------------------------*)
		
		(* If option asks to keep the files: keep *)

		(*** TODO (not implemented yet as we need to create files manually for now...) ***)

		
		(* Set model name and model prefix name back to their original value *)
		options#set_file original_file;
		options#set_files_prefix original_files_prefix;

		(*------------------------------------------------------------*)
		(* Return result *)
		(*------------------------------------------------------------*)
		imitator_result
		


(************************************************************)
(************************************************************)
end;;
(************************************************************)
(************************************************************)
