(************************************************************
 *
 *                       IMITATOR
 * 
 * Laboratoire Spécification et Vérification (ENS Cachan & CNRS, France)
 * Université Sorbonne Paris Nord, LIPN, CNRS, France
 * Université de Lorraine, CNRS, Inria, LORIA, Nancy, France
 * 
 * Module description: All graphics handling (cartography, trace set…)
 * 
 * File contributors : Étienne André, Ulrich Kühne
 * Created           : 2010/07/05
 *
 ************************************************************)
 

(************************************************************)
(* Modules *)
(************************************************************)

open OCamlUtilities
open Exceptions
open Constants
open ImitatorUtilities
open Statistics
open AbstractAlgorithm
open AbstractModel
open AbstractProperty
open AbstractValue
open StateSpace
open State


(************************************************************)
(* Statistics *)
(************************************************************)
let counter_graphics_statespace = create_time_counter_and_register "state space drawing" Graphics_counter Verbose_standard


(************************************************************)
(* Plot (graph) Functions *)
(************************************************************)

(*** HACK: pass directly whether zones are good or bad ***)
type polyhedron_nature =
	| Good
	| Bad
	| Unknown

(*------------------------------------------------------------*)
(* General functions *)
(*------------------------------------------------------------*)

(*** WARNING! very dangerous here! may not work for big integers ***)
let bad_float_of_num_const = NumConst.to_float
(*	try(
		float_of_string (NumConst.string_of_numconst n)
	)with
	| Failure msg -> raise (InternalError ("Oops…! Error when converting a NumConst to a float using float_of_string. Error: '" ^ msg ^ "'. NumConst is '" ^ (NumConst.string_of_numconst n) ^ "'"))*)


(** Convert a pair of NumConst.t into a pair for plotutils *)
let draw_x_y x y =
	(* Print x *)
	(string_of_float (bad_float_of_num_const x))
	(* Separator *)
	^ " "
	(* Print y *)
	^ (string_of_float (bad_float_of_num_const y))
	

(** Prepare the comments at the end of a graph file *)
let draw_comments command =
	(* Retrieve the input options *)
	let options = Input.get_options () in

	"\n# File automatically generated by " ^ Constants.program_name ^ ""
	^ "\n" ^"# Version  : " ^ (ImitatorUtilities.program_name_and_version_and_nickname_and_build)
	^ "\n" ^"# Git      : " ^ (ImitatorUtilities.git_branch_and_hash)
	^ "\n" ^"# Model    : " ^ options#model_file_name ^ ""
	^ "\n" ^"# Command  : " ^ command ^ ""
	^ "\n" ^"# Generated: " ^ (now()) ^ ""


(** Actually run graph *)
let run_graph command =
	(* Print some information *)
	if verbose_mode_greater Verbose_medium then(
		print_message Verbose_medium ("About the execute the following command…:\n" ^ command ^ "");
	);
	
	(* Actually execute it *)
	let execution = Sys.command command in
	
	if execution <> 0 then
		(print_error ("Something went wrong in the command. Exit code: " ^ (string_of_int execution) ^ ". Maybe you forgot to install the 'graph' utility (from the 'plotutils' package in Debian)."););
	
	(* Print some information *)
	print_message Verbose_high ("Result of the cartography execution: exit code " ^ (string_of_int execution));
	
	(* Return exec code *)
	execution


(** Create a file name for a given signal (i.e. the evolution of a variable over time) in a valuations drawing *)
let make_concreterun_variable_file_name file_prefix file_index =
	file_prefix ^ "_signal_" ^ (string_of_int file_index) ^ ".graph"

(** Create a file name with radical cartography_file_prefix and number file_index for a given tile of the cartography *)
let make_cartography_tile_file_name cartography_file_prefix file_index =
	cartography_file_prefix ^ "_points_" ^ (string_of_int file_index) ^ ".txt"


(*------------------------------------------------------------*)
(** Convert a tile_index into a color for graph (actually an integer from 1 to 5) *)
(*------------------------------------------------------------*)
let graph_color_of_int (tile_index : int) (with_property : bool) (polyhedron_nature : polyhedron_nature) (dotted : bool) : string =
	(* Definition of the color *)
	let color_index =
	(* If bad state defined *)
	if with_property then(
		(* Go for a good / bad coloring *)
		match polyhedron_nature with
		| Good -> 2 (* green *)
		| Bad -> 1 (* red *)
		| Unknown -> 5 (* cyan *)
	(* Else random coloring *)
	)else(
		(* Only 5 colors from 1 to 5 *)
		(tile_index mod 5) + 1
	)
	in
	(* Add an offset of 20 for dotted, and convert to string *)
	string_of_int (color_index + (if dotted then 20 else 0))





(*------------------------------------------------------------*)
(* Draw (using the plotutils graph utility) the cartography corresponding to a list of constraints. Takes as second argument the file name prefix. *)
(*------------------------------------------------------------*)
exception CartographyError



(** Get the reference hyper rectangle for properties that have one, or return None otherwise *)
let get_v0_option = function
	(* First check whether there is a property *)
	| Some property -> AlgorithmOptions.v0_option_of_property property
	| None -> None


let draw_cartography (model : AbstractModel.abstract_model) (property_option : AbstractProperty.abstract_property option) (returned_constraint_list : (LinearConstraint.p_convex_or_nonconvex_constraint * polyhedron_nature) list) cartography_file_prefix : unit =
	(* Create counter *)
	let counter_graphics_cartography = create_time_counter_and_register "cartography drawing" Graphics_counter Verbose_standard in

	(* Statistics *)
	counter_graphics_cartography#start;
	
try(
	(* Retrieve the input options *)
	let options = Input.get_options () in
	
	(* Get the reference hyper rectangle from the property, if any *)
	let v0_option : HyperRectangle.hyper_rectangle option = get_v0_option property_option in

	(* No reason to draw a cartography: exception! *)
	if not (AbstractAlgorithm.cartography_drawing_possible options#imitator_mode) then(
		print_error "Cartography cannot be drawn in this mode.";
		raise CartographyError
	);
	
	(* No cartography if no zone *)
	if returned_constraint_list = [] then(
		print_warning ("No cartography can be drawn since the list of constraints is empty.");
		raise CartographyError
	);

	print_message Verbose_standard ("\nDrawing the cartography…");

	print_message Verbose_low "Starting to compute graphical cartography…";
	
	(* Converting to convex constraints *)
	(*** BADPROG: creating a list of singletons and lists, and then flatten ***)
	let returned_constraint_list = List.flatten (List.map (function
		| LinearConstraint.Convex_p_constraint p_linear_constraint, polyhedron_nature -> [LinearConstraint.render_non_strict_p_linear_constraint p_linear_constraint , polyhedron_nature]
		| LinearConstraint.Nonconvex_p_constraint p_nnconvex_constraint, polyhedron_nature ->
			(* Get the convex constraints *)
			let p_linear_constraints = LinearConstraint.p_linear_constraint_list_of_p_nnconvex_constraint p_nnconvex_constraint in
			(* Render non-strict *)
			List.map (fun p_linear_constraint -> LinearConstraint.render_non_strict_p_linear_constraint p_linear_constraint, polyhedron_nature) p_linear_constraints
		) returned_constraint_list
	)  in
	
	
	(*** TODO!!! for EF-synthesis, first draw a green background, since the non-red is necessarily green (well, unless approximations are used) ***)
	
	(*------------------------------------------------------------*)
	(* Constants *)
	(*------------------------------------------------------------*)
	
	let x_index = 0 in
	let y_index = 1 in

	
	(* Defaut min/max coordinates for the reference rectangle and the minimal bounds of the image, if none are specified using a v0 or some options *)
	let default_x_min = 0  in
	let default_x_max = 50 in
	let default_y_min = 0  in
	let default_y_max = 50 in
	
	(*------------------------------------------------------------*)
	(* First find the dimensions *)
	(*------------------------------------------------------------*)

	(* Print some information *)
	print_message Verbose_low "Looking for dimensions…";
	
	let range_params : int list ref = ref [] in
	
	(* The coordinates of the dotted rectangle to be printed *)
	let reference_rectangle_coordinates = Array.make 2 (NumConst.zero, NumConst.zero) in
	
	(* The coordinates of the min bounds rectangle (not really to be printed, but to ensure a minimal graphics size) *)
	let min_bounds_coordinates = Array.make 2 (0, 0) in
	min_bounds_coordinates.(x_index) <- default_x_min, default_x_max;
	min_bounds_coordinates.(y_index) <- default_y_min, default_y_max;
	
	
	(*------------------------------------------------------------*)

	begin
	match v0_option with
	
	(* Case a hyper rectangle is defined in the property *)
	| Some v0 ->
	(* If cartography: find indices of first two variables with a parameter range *)
	(*** TODO: take the projection into account! ***)
		
		print_message Verbose_low "Case real cartography: first 2 parameters with a range";
		for index = 0 to model.nb_parameters - 1 do
(* 			Array.iteri (fun index (a,b) ->  *)
			let a = v0#get_min index in
			let b = v0#get_max index in
			if NumConst.neq a b then(
				(* Add one more parameter *)
				print_message Verbose_medium "Found a parameter!";
				range_params := index :: !range_params;
			)
		(* ) v0;*)
		done;
		range_params := List.rev !range_params;
		
		if (List.length !range_params) < 2 then(
			print_warning "Could not plot cartography (region of interest has too few dimensions)";
			raise CartographyError
		);

		(* Get min/max *)
		let x_min = v0#get_min (List.nth !range_params 0) in
		let x_max = v0#get_max (List.nth !range_params 0) in
		let y_min = v0#get_min (List.nth !range_params 1) in
		let y_max = v0#get_max (List.nth !range_params 1) in
		
		(* Update coordinates of the dotted rectangle *)
		reference_rectangle_coordinates.(x_index) <- x_min, x_max;
		reference_rectangle_coordinates.(y_index) <- y_min, y_max;
		
		(* Also overwrite the bounds, ONLY if integers *)
		let old_x_min, old_x_max = min_bounds_coordinates.(x_index) in
		min_bounds_coordinates.(x_index) <-
			(if NumConst.is_int x_min then NumConst.to_int x_min else old_x_min)
			,
			(if NumConst.is_int x_max then (NumConst.to_int x_max) else old_x_max)
		;
		let old_y_min, old_y_max = min_bounds_coordinates.(y_index) in
		min_bounds_coordinates.(y_index) <-
			(if NumConst.is_int y_min then (NumConst.to_int y_min) else old_y_min)
			,
			(if NumConst.is_int y_max then (NumConst.to_int y_max) else old_y_max)
		;


	(* Otherwise: choose the first two parameters *)
	| None ->
	(*** TODO: take the projection into account! ***)
		print_message Verbose_low "Pick up the first 2 parameters to draw the cartography";
		(* First check that there are at least 2 parameters *)
		if model.nb_parameters < 2 then(
			print_warning ("Could not plot cartography (which requires at least 2 parameters) because there is " ^ (if model.nb_parameters = 1 then "only one parameter" else "no parameter at all") ^ " in this model.");
			raise CartographyError
		);
		(* Choose the first 2 *)
		range_params := [ List.nth model.parameters 0 ; List.nth model.parameters 1];
		
		(* Prepare the "V0" rectangle *)
		let ef_x_min =
		match options#output_cart_x_min with
			| None -> NumConst.numconst_of_int default_x_min
			| Some n -> NumConst.numconst_of_int n
		in
		let ef_x_max =
		match options#output_cart_x_max with
			| None -> NumConst.numconst_of_int default_x_max
			| Some n -> NumConst.numconst_of_int n
		in
		let ef_y_min =
		match options#output_cart_y_min with
			| None -> NumConst.numconst_of_int default_y_min
			| Some n -> NumConst.numconst_of_int n
		in
		let ef_y_max =
		match options#output_cart_y_max with
			| None -> NumConst.numconst_of_int default_y_max
			| Some n -> NumConst.numconst_of_int n
		in
		reference_rectangle_coordinates.(0) <- ef_x_min, ef_x_max;
		reference_rectangle_coordinates.(1) <- ef_y_min, ef_y_max;
	end;

		
	begin
	match options#output_cart_x_min with
		| None -> ()
		| Some n ->
			(* Update the bounds of the minimum size rectangle *)
			let (_, old_max) = min_bounds_coordinates.(x_index) in
			min_bounds_coordinates.(x_index) <- (n, old_max);
			
			let (old_min, old_max) = reference_rectangle_coordinates.(x_index) in
			let new_min = NumConst.numconst_of_int n in
			if NumConst.g new_min old_min then
				(* Shrink V0 bounds *)
				reference_rectangle_coordinates.(x_index) <- (new_min, old_max);
	end;
	begin
	match options#output_cart_x_max with
		| None -> ()
		| Some n ->
			(* Update the bounds of the minimum size rectangle *)
			let (old_min, _) = min_bounds_coordinates.(x_index) in
			min_bounds_coordinates.(x_index) <- (old_min, n);
			
			let (old_min, old_max) = reference_rectangle_coordinates.(x_index) in
			let new_max = NumConst.numconst_of_int n in
			if NumConst.l new_max old_max then
				(* Shrink V0 bounds *)
				reference_rectangle_coordinates.(x_index) <- (old_min, new_max);
	end;
	begin
	match options#output_cart_y_min with
		| None -> ()
		| Some n ->
			(* Update the bounds of the minimum size rectangle *)
			let (_, old_max) = min_bounds_coordinates.(y_index) in
			min_bounds_coordinates.(y_index) <- (n, old_max);
			
			let (old_min, old_max) = reference_rectangle_coordinates.(y_index) in
			let new_min = NumConst.numconst_of_int n in
			if NumConst.g new_min old_min then
				(* Shrink V0 bounds *)
				reference_rectangle_coordinates.(y_index) <- (new_min, old_max);
	end;
	begin
	match options#output_cart_y_max with
		| None -> ()
		| Some n ->
			(* Update the bounds of the minimum size rectangle *)
			let (old_min, _) = min_bounds_coordinates.(y_index) in
			min_bounds_coordinates.(y_index) <- (old_min, n);

			let (old_min, old_max) = reference_rectangle_coordinates.(y_index) in
			let new_max = NumConst.numconst_of_int n in
			if NumConst.l new_max old_max then
				(* Shrink V0 bounds *)
				reference_rectangle_coordinates.(y_index) <- (old_min, new_max);
	end;
	
	
	(*------------------------------------------------------------*)
	(* Handle the v0 rectangle, if any *)
	(*------------------------------------------------------------*)
	
	(* Create a temp file containing the V0 coordinates *)
	let file_v0_name = cartography_file_prefix ^ "_v0.txt" in
	let file_rectangle_v0 = open_out file_v0_name in
	
	let str_rectangle_v0 = match v0_option with
	| Some _ ->
	
		(* Convert a num_const to a string, specifically for Graph *)
		let graph_string_of_numconst n = 
			(* Check that it is an integer *)
			if not (NumConst.is_int n) then(
				raise (InternalError("Only integers can be handled for the cartography, so far. Found: '" ^ (NumConst.string_of_numconst n) ^ "'"))
			);
			(* Convert to a string, and add a "." at the end *)
			(NumConst.string_of_numconst n) ^ "."
		in

		(* Print some information *)
		print_message Verbose_low ("Computing the zone…");
		
		(* Create the file content *)
					(graph_string_of_numconst (fst (reference_rectangle_coordinates.(x_index))))
			^" "^(graph_string_of_numconst (snd (reference_rectangle_coordinates.(y_index))))
			^"\n"^(graph_string_of_numconst (snd (reference_rectangle_coordinates.(x_index))))
			^" "^ (graph_string_of_numconst (snd (reference_rectangle_coordinates.(y_index))))
			^"\n"^(graph_string_of_numconst (snd (reference_rectangle_coordinates.(x_index))))
			^" "^ (graph_string_of_numconst (fst (reference_rectangle_coordinates.(y_index))))
			^"\n"^(graph_string_of_numconst (fst (reference_rectangle_coordinates.(x_index))))
			^" "^ (graph_string_of_numconst (fst (reference_rectangle_coordinates.(y_index))))
			^"\n"^(graph_string_of_numconst (fst (reference_rectangle_coordinates.(x_index))))
			^" "^ (graph_string_of_numconst (snd (reference_rectangle_coordinates.(y_index))))
	
	| _ -> ""
	
	in
	
	output_string file_rectangle_v0 str_rectangle_v0;
	close_out file_rectangle_v0;

	(* Print some information *)
	if verbose_mode_greater Verbose_total then
		print_message Verbose_total ("str_rectangle_v0 = \n" ^ str_rectangle_v0);


	(*------------------------------------------------------------*)
	(* Handle the bounds rectangle, i.e., to make sure the image has at least the size of the min/max values given *)
	(*------------------------------------------------------------*)
	
	(* Convert an int to a string, specifically for Graph *)
	let graph_string_of_int n = 
		(* Convert to a string, and add a "." at the end *)
		(string_of_int n) ^ "."
	in

	
	(* Create a temp file containing the bounds rectangle coordinates *)
	let bounds_file_name = cartography_file_prefix ^ "_bounds.txt" in
	let file_rectangle_bounds = open_out bounds_file_name in
	
	(* Print some information *)
	print_message Verbose_low ("Computing the zone…");
	
	let str_rectangle_bounds =
				(graph_string_of_int (fst (min_bounds_coordinates.(x_index))))
		^" "^(graph_string_of_int (snd (min_bounds_coordinates.(y_index))))
		^"\n"^(graph_string_of_int (snd (min_bounds_coordinates.(x_index))))
		^" "^ (graph_string_of_int (snd (min_bounds_coordinates.(y_index))))
		^"\n"^(graph_string_of_int (snd (min_bounds_coordinates.(x_index))))
		^" "^ (graph_string_of_int (fst (min_bounds_coordinates.(y_index))))
		^"\n"^(graph_string_of_int (fst (min_bounds_coordinates.(x_index))))
		^" "^ (graph_string_of_int (fst (min_bounds_coordinates.(y_index))))
		^"\n"^(graph_string_of_int (fst (min_bounds_coordinates.(x_index))))
		^" "^ (graph_string_of_int (snd (min_bounds_coordinates.(y_index))))
	in
	output_string file_rectangle_bounds str_rectangle_bounds;
	close_out file_rectangle_bounds;

	(* Print some information *)
	if verbose_mode_greater Verbose_total then
		print_message Verbose_total ("str_rectangle_bounds = \n" ^ str_rectangle_bounds);

	
	(*------------------------------------------------------------*)
	(* Now start *)
	(*------------------------------------------------------------*)
		
	(* Retrieve parameters *)
	let x_param = List.nth !range_params x_index in
	let y_param = List.nth !range_params y_index in

	let x_name = model.variable_names x_param in
	let y_name = model.variable_names y_param in

	(* Print some information *)
(* 	print_message Verbose_standard ("Cartography will be drawn in 2D for parameters " ^ x_name ^  " and " ^ y_name ^  "."); *)
	

	(* Beginning of the script *)
	
	let script_line = ref ("graph -T " ^ cartography_extension ^ " --bitmap-size " ^ cartography_size ^ " -C -X \"" ^ x_name ^ "\" -Y \"" ^ y_name ^ "\" ") in
	(* find the minimum and maximum abscissa and ordinate for each constraint and store them in a list *)
	
	(* Add the min bounds rectangle *)
	script_line := !script_line ^ " --line-mode 0 --fill-fraction -1 " ^ bounds_file_name ^ " ";
	
	
	(* Print some information *)
	print_message Verbose_low ("Finding zone corners…");

	(* get corners of bounds *)
	let init_min_abs, init_max_abs = reference_rectangle_coordinates.(x_index) in
	let init_min_ord, init_max_ord = reference_rectangle_coordinates.(y_index) in

	(* Conversion to float, because all functions handle floats *)
	
	(* Print some information *)
	print_message Verbose_low ("Finding minima and maxima for axes…");

	(* Find mininma and maxima for axes (version Étienne, who finds imperative here better ) *)
	let min_abs = ref (bad_float_of_num_const init_min_abs) in
	let max_abs = ref (bad_float_of_num_const init_max_abs) in
	let min_ord = ref (bad_float_of_num_const init_min_ord) in
	let max_ord = ref (bad_float_of_num_const init_max_ord) in
	(* Update min / max for ONE linear_constraint *)
	let update_min_max linear_constraint =
		let points, _ = LinearConstraint.shape_of_poly x_param y_param linear_constraint in
		List.iter (fun (x,y) ->
			min_abs := min !min_abs x;
			max_abs := max !max_abs x;
			min_ord := min !min_ord y;
			max_ord := max !max_ord y;
		) points;
	in
	(* Update min / max for all returned constraint *)
	List.iter (function (p_linear_constraint, _) -> update_min_max p_linear_constraint) returned_constraint_list;

	(* Print some information *)
	print_message Verbose_low ("Adding a 1-unit margin…");

	(* Add a margin of 1 unit *)
	min_abs := !min_abs -. 1.0;
	max_abs := !max_abs +. 1.0;
	min_ord := !min_ord -. 1.0;
	max_ord := !max_ord +. 1.0;
	
	(* Overwrite bounds if options specified *)
	(*** WARNING: only works partially ***)
	begin
	match options#output_cart_x_min with
		| None -> ()
		| Some n -> min_abs := float_of_int n;
	end;
	begin
	match options#output_cart_x_max with
		| None -> ()
		| Some n -> max_abs := float_of_int n;
	end;
	begin
	match options#output_cart_y_min with
		| None -> ()
		| Some n -> min_ord := float_of_int n;
	end;
	begin
	match options#output_cart_y_max with
		| None -> ()
		| Some n -> max_ord := float_of_int n;
	end;
	(*** TODO!!! do something if some min > max ***)

	
	(*** BAD PROG : bouh pas beau ***)
	(*** WARNING: it looks like file_index = tile_index, always! ***)
	let file_index = ref 0 in
	let tile_index = ref 0 in
	(* Creation of files (Daphne wrote this?) *)
	let create_file_for_constraint k polyhedron_nature =
	
		(* Increment the file index *)
		file_index := !file_index + 1;

		(* Print some information *)
		if verbose_mode_greater Verbose_low then(
			print_message Verbose_low ("Computing points for constraint " ^ (string_of_int !tile_index) ^ " \n " ^ (LinearConstraint.string_of_p_linear_constraint model.variable_names k) ^ ".");
		);
		
		let file_name = make_cartography_tile_file_name cartography_file_prefix !file_index in
		
		(* find the points satisfying the constraint *)
		let s = LinearConstraint.plot_2d x_param y_param k !min_abs !min_ord !max_abs !max_ord in
		(* Get the points *)
		let the_points = snd s in

		(* Print some information *)
		if verbose_mode_greater Verbose_low then(
			print_message Verbose_low ("  Points \n " ^ the_points ^ "");
		);
		
		(* Comments at the end of the graph file *)
		let comments = (draw_comments (OCamlUtilities.string_of_array_of_string_with_sep " " Sys.argv))
		(*** WARNING: This line is used by Giuseppe Lipari: do not change without prior agreement ***)
		(*** OOPS: changed by ÉA without prior agreement (2024/01/08) ***)
		(*^ (if Input.has_property() then(
			"\n# Tile nature: " ^ (StateSpace.string_of_statespace_nature statespace_nature) ^ ""
		) else "")*)
		in
		
		(* Print some information *)
		if verbose_mode_greater Verbose_total then(
			print_message Verbose_total ("Writing content to file '" ^ (file_name) ^ "'…");
		);

		(* Export the file content to the file *)
		write_to_file file_name the_points;
		
		(* close the file and open it in a reading mode to read the first line *)
		
		let file_in = open_in file_name in
		let s2 = input_line file_in in
		(* close the file and open it in a write mode to copy the whole string in it and ensure that the polygon is closed*)
		close_in file_in;
		let file_out_bis = open_out file_name in
		output_string file_out_bis (the_points ^ s2 ^ comments);
		close_out file_out_bis;
		(* instructions to have the zones colored. If fst s = true then the zone is infinite *)
		if fst s
			(*** TODO : same color for one disjunctive tile ***)
			then script_line := !script_line ^ "--line-mode " ^ (graph_color_of_int !tile_index (property_option <> None) polyhedron_nature true) ^ " --fill-fraction 0.3 " ^ file_name ^ " "
			else script_line := !script_line ^ "--line-mode " ^ (graph_color_of_int !tile_index (property_option <> None) polyhedron_nature false) ^ " --fill-fraction 0.7 " ^ file_name ^ " "
		;
	in
	
	(* For all returned_constraint *)
	List.iter (fun (p_linear_constraint, polyhedron_nature) ->
		(* Test just in case! (otherwise an exception arises *)
		if LinearConstraint.p_is_false p_linear_constraint then(
			print_warning " Found a false constraint when computing the cartography. Ignored."
		)else(
			tile_index := !tile_index + 1;
			create_file_for_constraint p_linear_constraint polyhedron_nature
		)
	) returned_constraint_list;
	
	
	(* File in which the cartography will be printed *)
	let cartography_image_file = cartography_file_prefix ^ "." ^ cartography_extension in
	
	(* Last part of the script *)
	(* `-r 0.15 -u 0.12 -w 0.8 -h 0.75`: very, very ad-hoc attempt to reduce a bit the margins *)
	(*** TODO: add here the min bounds rectangle ***)
	script_line := !script_line
		(* Part to add the last file *)
		(*** NOTE: is `-C` needed? (2020/09/04, ÉA) ***)
		^ " -C --line-mode 2 --fill-fraction -1 " ^ file_v0_name
		
		(* Part to set global options and to redirect to the output *)
		^ " -L \"" ^ options#model_local_file_name ^ "\" -r 0.15 -u 0.12 -w 0.8 -h 0.75 --blankout 1.0 > " ^ cartography_image_file
	;
	
	(* Print some information *)
	print_message Verbose_standard (
		"Plot cartography in 2D projected on parameters " ^ x_name ^ " and " ^ y_name
		^ " to file '" ^ cartography_image_file ^ "'."); 

	(*------------------------------------------------------------*)
	(* execute the script *)
	(*------------------------------------------------------------*)
	let _ = run_graph !script_line in

	(*------------------------------------------------------------*)
	(* Remove files *)
	(*------------------------------------------------------------*)
	if not options#with_graphics_source then(
	
		(* Remove the file printing the dotted rectangle *)
		
		(* Print some information *)
		print_message Verbose_medium ("Removing V0 file…");
		delete_file file_v0_name;
		
		(* Print some information *)
		print_message Verbose_medium ("Removing bounds file…");
		delete_file bounds_file_name;
		
		(* Remove all constraints files *)
		
		for i = 1 to !file_index do
			(* Print some information *)
			print_message Verbose_medium ("Removing points file #" ^ (string_of_int i) ^ "…");
			
			delete_file (make_cartography_tile_file_name cartography_file_prefix i);
		done;
	);
	(* Statistics *)
	counter_graphics_cartography#stop;
	()

) with
	| CartographyError -> (print_warning "Error while printing the cartography";
	(* Statistics *)
	counter_graphics_cartography#stop;
	()
)


(*------------------------------------------------------------*)
(* Draw (using the plotutils graph utility) the evolution of clock and discrete variables valuations according to time. *)
(*------------------------------------------------------------*)

exception Found_flow of NumConst.t

(** Side function to get the flow of a variable in a given global_location *)
(*** NOTE: if incompatible flows are defined (i.e., a different flow in 2 different automata), the result is undefined (actually the first non-1 flow is returned) ***)
(*** NOTE: this function could be defined elsewhere… ***)
let get_flow
(*	(stopwatches     : Automaton.automaton_index -> Automaton.location_index -> Automaton.clock_index list)
	(flow            : Automaton.automaton_index -> Automaton.location_index -> (Automaton.clock_index * NumConst.t) list)*)
	(model           : AbstractModel.abstract_model)
	(global_location : DiscreteState.global_location)
	(variable_index  : Automaton.variable_index)
	:
	NumConst.t
	=
	(* First try to iterate over stopwatches *)
	if List.exists (fun automaton_index ->
		(* Get location index *)
		let location_index = DiscreteState.get_location global_location automaton_index in
		(* Get list of stopped clocks *)
		let stopwatches = model.stopwatches automaton_index location_index in
		(* Check for membership *)
		List.mem variable_index stopwatches
	) model.automata
	then NumConst.zero
	else
	(* Second: try for explicit flows *)
	(*** TODO: replace with `find_map` when using OCaml v4.10 ***)
	try(
		List.iter (fun automaton_index ->
			(* Get location index *)
			let location_index = DiscreteState.get_location global_location automaton_index in
			(* Get list of flows *)
			let flows = model.flow automaton_index location_index in
			(* Check for membership *)
			match List.find_opt (fun (clock_index, _) -> clock_index = variable_index) flows with
				(* We found a `<>1` flow: return! *)
				| Some clock_and_flow ->
					let _, flow = clock_and_flow in
					raise (Found_flow flow)
				(* No flow found for this variable: keep searching in the next automaton *)
				| None -> ()
		) model.automata;
		
		(* Otherwise: normal flow, i.e., 1 *)
		NumConst.one
		
	) with Found_flow flow -> flow


(** This generic function takes a list of "abstract steps", i.e., only the target and the duration; this is to unify concrete and impossible steps *)
(*** TODO: draw differently the impossible part of impossible concrete runs ***)
let draw_run_generic (model : AbstractModel.abstract_model) (initial_state : State.concrete_state) (abstract_steps : (NumConst.t * State.concrete_state) list) (file_prefix : string) : unit =
	(* Retrieve the input options *)
	let options = Input.get_options () in
	
	let file_index = ref 0 in

	(* Create one file per clock and discrete variable *)
	List.iter (fun variable_index ->
	
		(* Increment counter *)
		incr file_index;
		
		(* Print some information *)
		if verbose_mode_greater Verbose_medium then(
			print_message Verbose_medium ("Preparing signal plot for " ^ (ModelPrinter.string_of_var_type (model.type_of_variables variable_index)) ^  " `" ^ (model.variable_names variable_index) ^  "`…");
		);
		
		(*** TODO: remove consecutive identical points (not critical) ***)
		
		let file_content = string_of_list_of_string_with_sep "\n" (

			(* Track absolute time *)
			let absolute_time = ref NumConst.zero in
			
			(* Find the first valuation for 0-time *)
			
			(* Print some information *)
			if verbose_mode_greater Verbose_total then(
				print_message Verbose_total ("Computing value for `" ^ (model.variable_names variable_index) ^  "` at time zero…");
			);
			(* Get value *)
			let zero_value = match model.type_of_variables variable_index with
				| DiscreteType.Var_type_discrete _ ->
					DiscreteState.get_discrete_value initial_state.global_location variable_index
				| DiscreteType.Var_type_clock ->
				    let rational_value = initial_state.px_valuation variable_index in
				    Abstract_scalar_value (Abstract_number_value (Abstract_rat_value rational_value))
				| _ -> raise (InternalError "Clock or discrete variable expected in draw_concrete_run")
			in

			(* Used to keep the previous value *)
			let previous_value = ref zero_value in
			
			(* Used to get the flow of the variables *)
			let previous_location = ref initial_state.global_location in
			
			(* Consider the value at time 0 *)
			(
				(*** WARNING: do not use !absolute_time here, as it may be modified in the part FOLLOWING the :: (not sure how OCaml executes this!) ***)
				
				(* Print some information *)
				if verbose_mode_greater Verbose_total then(
					print_message Verbose_total ("Generating points for `" ^ (model.variable_names variable_index) ^  "` at time zero with value '" ^ (AbstractValue.string_of_value zero_value) ^  "'…");
				);

				(* Convert to the plotutils format *)
				(draw_x_y NumConst.zero (AbstractValue.to_rat_value zero_value))
			)
			
			::
			
			(* Iterate on the steps of the concrete run *)
			(List.map (fun ((step_time, step_target) : (NumConst.t * State.concrete_state)) ->
				(* Update absolute time *)
				absolute_time := NumConst.add !absolute_time step_time;
			
				(* Print some information *)
				if verbose_mode_greater Verbose_total then(
					print_message Verbose_total ("Considering value for `" ^ (model.variable_names variable_index) ^  "` at time " ^ (NumConst.string_of_numconst !absolute_time) ^ "…");
				);
				
				(* Handle the point just before the current point: if a clock, need to manage time elapsing if reset; if discrete, we imagine (so far) an immediate change of the value right at (technically "before") this point *)
				let previous_point_str , value =
					(* Print some information *)
					if verbose_mode_greater Verbose_total then(
						print_message Verbose_total ("Checking type of variable `" ^ (model.variable_names variable_index) ^  "`…");
					);
				
					match model.type_of_variables variable_index with
					
				(* If discrete: the previous value is still valid right before the current transition *)
					| DiscreteType.Var_type_discrete _ ->
					
						(* Get the discrete value *)
						let value = DiscreteState.get_discrete_value step_target.global_location variable_index in
						
						(* Print some information *)
						if verbose_mode_greater Verbose_total then(
							print_message Verbose_total ("About to perform comparison…");
							print_message Verbose_total ("Previous value = " ^ (AbstractValue.string_of_value !previous_value ) ^ "");
							print_message Verbose_total ("Current value = " ^ (AbstractValue.string_of_value value) ^ "");
						);
						
						(* If same value as before, no need to add a new point *)
						if AbstractValue.equal !previous_value value then(
							(* Print some information *)
							if verbose_mode_greater Verbose_total then(
								print_message Verbose_total ("Discrete `" ^ (model.variable_names variable_index) ^  "` did not evolve: skip");
							);
							(* No new point *)
							""
							,value
						)else(
							(* Print some information *)
							if verbose_mode_greater Verbose_total then(
								print_message Verbose_total ("New additional point for discrete `" ^ (model.variable_names variable_index) ^  "` at time " ^ (NumConst.string_of_numconst !absolute_time) ^ "…");
							);
							
							(* Same value, current time *)
							(* Convert to the plotutils format *)
							(draw_x_y !absolute_time (AbstractValue.to_rat_value !previous_value))
							(* Separator for next point *)
							^ "\n"
							,value
						)

				(* If clock: the previous value must be incremented by the timed elapsed since the last point *)
					| DiscreteType.Var_type_clock ->
						
						(* Get the clock value *)
						let value = step_target.px_valuation variable_index in
						
						(* Retrieve the time elapsed *)
						let time_elapsed = step_time in
						(* If no time elapsed: no need to add a point *)
						if NumConst.equal time_elapsed NumConst.zero then(
							""
							, Abstract_scalar_value (Abstract_number_value (Abstract_rat_value value))
						)else(
							(* Increment the value of the clock by the elapsed time *)
							
							(* Get the flow *)
							let flow = get_flow model !previous_location variable_index in
							
(*							(*** TODO: urgency / stopwatches! ***)
							let stopwatches = model.stopwatches (TODO) in
							
							let flow =
								(if *)
							
							(* Update the value of the clock using the flow *)
							(* Clock can only be updated by rationals so we use the numconst value of discrete variable *)
							let previous_numconst_value = AbstractValue.to_rat_value !previous_value in
							let clock_value_after_elapsing = NumConst.add previous_numconst_value (NumConst.mul time_elapsed flow) in
							
							(* Same value, current time *)
							(* Convert to the plotutils format *)
							(draw_x_y !absolute_time clock_value_after_elapsing)
							(* Separator for next point *)
							^ "\n"
							, Abstract_scalar_value (Abstract_number_value (Abstract_rat_value value))
						)
					
				(* Else error *)
					| _ -> raise (InternalError "Clock or discrete variable expected in draw_concrete_run")
					
				in
				
				(* Backup current point for next point *)
				previous_value := value;
				
				(* Backup current location for next point *)
				previous_location := step_target.global_location;
				
				(* Print some information *)
				if verbose_mode_greater Verbose_total then(
					print_message Verbose_total ("Generating points for `" ^ (model.variable_names variable_index) ^  "` at time " ^ (NumConst.string_of_numconst !absolute_time) ^ " with value '" ^ (AbstractValue.string_of_value value) ^  "'…");
				);

				(* First add "previous" point *)
				previous_point_str
				
				(* Then add the current point (easy) in the plotutils format *)
				^ (draw_x_y !absolute_time (AbstractValue.to_rat_value value))
			) abstract_steps
			)
		) in
		
		(* Create and fill file *)
		
		(* File name *)
		let file_name = make_concreterun_variable_file_name file_prefix !file_index in
		
		(* Comments at the end of the graph file *)
		let comments = (draw_comments (OCamlUtilities.string_of_array_of_string_with_sep " " Sys.argv)) in
		
		(* Create file content *)
		let file_content = file_content ^ "\n" ^ comments in
		
		(* Print some information *)
		if verbose_mode_greater Verbose_high then(
			print_message Verbose_high ("Writing content to file '" ^ (file_name) ^ "'…");
		);

		(* Print some information *)
		if verbose_mode_greater Verbose_total then(
			print_message Verbose_total ("File content: \n\n" ^ (file_content) ^ "\n");
		);

		(* Export the file content to the file *)
		write_to_file file_name file_content;
		
		()

		
	) model.clocks_and_discrete;
	
	let signals_image_file = file_prefix ^ "." ^ signals_image_extension in
		
	(* Create command *)
	let command =
		(* Base command *)
		(* -T: extension *)
		(* -L: label (title) *)
		(* -X: name of the X axis *)
		(* -r: right shift (by default 0.2) *)
		(* -u: upper shift (by default 0.2) *)
		"graph -T ps -L \"" ^ options#files_prefix ^ "\" -X \"t\" -r 0.0 -u 0.0 \\"
		^ (string_of_list_of_string (
			(* Store number of files *)
			let nb_files = !file_index in
			
			(* Get the size for each file *)
			(*** NOTE: add "+1" to keep a little space in between two files ***)
			let size = round3_float (1. /. (float_of_int (nb_files + 1))) in
			let width = string_of_float ((float_of_int nb_files) +. 0.5) in
			
			let file_index = ref 0 in
			List.map (fun variable_index ->
				incr file_index;
				
				let file_name = make_concreterun_variable_file_name file_prefix !file_index in

				let offset = round3_float (float_of_int (!file_index - 1) /. (float_of_int (nb_files))) in
				(* Objective: `--reposition .0 .44 .2 -h 1 -w 4.5 -Y "variable3" testCounterExSimple_signals_signal_2.txt \` *)
				(* -h: height *)
				(* -w: width *)
				(* -C: in color *)
				(* -m: the number of colors (modulo 25, managed automatically by graph) *)
				"\n\t--reposition .0 " ^ offset ^ " " ^ size ^ " -h 1 -w " ^ width ^ " -C -m " ^ (string_of_int !file_index) ^ " -Y \"" ^ (model.variable_names variable_index) ^ "\" " ^ file_name ^ " \\"
				
			) model.clocks_and_discrete
		))
		^ "\n\t--blankout 1.0 > " ^ signals_image_file ^ ""
	in

	(* Print some information *)
	print_message Verbose_standard (
		"Plot signal-representation of the counterexample to file '" ^ signals_image_file ^ "'."); 

	(* execute the script *)
	let _ = run_graph command in
	
	(* Remove temporary files *)
	if not options#with_graphics_source then(
		(* Removing all signal files *)
		for i = 1 to !file_index do
			print_message Verbose_medium ("Removing signal file #" ^ (string_of_int i) ^ "…");
			delete_file (make_concreterun_variable_file_name file_prefix i);
		done;
	);

	(* The end *)
	()



let draw_impossible_concrete_run (model : AbstractModel.abstract_model) (impossible_concrete_run : StateSpace.impossible_concrete_run) (file_prefix : string) : unit =
	(* Transforms steps to abstract pairs *)
	let abstract_steps = list_append
		(List.map (fun (concrete_step : StateSpace.concrete_step) -> concrete_step.time , concrete_step.target) impossible_concrete_run.steps)
		(List.map (fun (impossible_concrete_step : StateSpace.impossible_concrete_step) -> impossible_concrete_step.time , impossible_concrete_step.target) impossible_concrete_run.impossible_steps)
	in
	draw_run_generic model impossible_concrete_run.initial_state abstract_steps file_prefix
	
let draw_concrete_run (model : AbstractModel.abstract_model) (concrete_run : StateSpace.concrete_run) (file_prefix : string) : unit =
	(* Transforms steps to abstract pairs *)
	let abstract_steps = List.map (fun (concrete_step : StateSpace.concrete_step) -> concrete_step.time , concrete_step.target) concrete_run.steps in
	draw_run_generic model concrete_run.initial_state abstract_steps file_prefix



(************************************************************)
(* Dot Functions *)
(************************************************************)

let dot_colors = [
(* I ordered the first colors *)
(*"red" ; "green" ; *)"blue" ; "cyan" ; "magenta" ;
(* The rest : random ! *)
"yellowgreen"; "indianred1"; "goldenrod3"; "darkolivegreen4"; "slategray4"; "turquoise4"; "lightpink"; "salmon"; "pink3"; "chocolate4"; "lightslateblue"; "yellow3"; "red4"; "seashell3"; "cyan2"; "darkgoldenrod3"; "gainsboro"; "paleturquoise2"; "peachpuff1"; "oldlace"; "khaki"; "deepskyblue"; "maroon3"; "gold3"; "tan"; "mediumblue"; "lightyellow"; "ivory"; "lightcyan"; "lightsalmon4"; "maroon2"; "maroon4"; "tan3"; "green2"; "ivory2"; "navyblue"; "wheat1"; "navajowhite3"; "darkkhaki"; "whitesmoke"; "goldenrod"; "gold1"; "sandybrown"; "springgreen3"; "magenta2"; "lightskyblue1"; "lightcyan3"; "khaki2"; "khaki3"; "lavender"; "orchid1"; "wheat"; "lavenderblush1"; "firebrick2"; "navajowhite4"; "darkslategray3"; "palegreen2"; "lavenderblush3"; "skyblue3"; "deepskyblue3"; "darkorange"; "magenta1"; "darkorange3"; "violetred1"; "lawngreen"; "deeppink3"; "darkolivegreen1"; "darkorange1"; "darkorchid1"; "limegreen"; "lightslategray"; "deeppink"; "red2"; "goldenrod1"; "mediumorchid4"; "cornsilk1";
"lemonchiffon3"; "gold"; "orchid"; "yellow2"; "lightpink4"; "violetred2"; "mediumpurple"; "lightslategrey"; "lightsalmon1"; "violetred"; "coral2"; "slategray"; "plum2"; "turquoise3"; "lightyellow3"; "green4"; "mediumorchid1"; "lightcyan1"; "lightsalmon3"; "green3"; "lightseagreen"; "mediumpurple1"; "lightskyblue"; "lightyellow2"; "firebrick"; "honeydew2"; "slateblue3"; "navajowhite"; "seagreen1"; "springgreen4"; "peru"; "springgreen2"; "mediumvioletred"; "ivory4"; "olivedrab3"; "lightyellow1"; "hotpink"; "sienna4"; "lightcyan4"; "chartreuse4"; "lemonchiffon4"; "indianred3"; "hotpink4"; "sienna1"; "slategray3"; "darkseagreen2"; "tomato3"; "honeydew3"; "mistyrose2"; "rosybrown1"; "pink2"; "powderblue"; "cornflowerblue"; "tan1"; "indianred4"; "slateblue2"; "palevioletred3"; "ivory1"; "honeydew4"; "yellow"; (*"white"; *)"wheat3"; "steelblue4"; "purple2"; "deeppink4"; "royalblue4"; "lightgrey"; "forestgreen"; "palegreen"; "darkorange4"; "lightsteelblue2"; "tomato4"; "royalblue1"; "hotpink1"; "hotpink3";
"palegoldenrod"; "orange3"; "yellow1"; "orange2"; "slateblue"; "lightblue"; "lavenderblush2"; "chartreuse3"; "hotpink2"; "lightblue1"; "coral1"; "orange1"; "gold2"; "lightcoral"; "mediumseagreen"; "darkgreen"; "dodgerblue1"; "khaki1"; "khaki4"; "lightblue4"; "lightyellow4"; "firebrick3"; "crimson"; "olivedrab2"; "mistyrose3"; "lightsteelblue4"; "mediumpurple3"; "maroon"; "purple1"; "mediumorchid3"; "lightblue3"; "snow4"; "pink4"; "lightgray"; "lightsteelblue1"; "mistyrose"; "lightgoldenrodyellow"; "slategray1"; "peachpuff4"; "lightsalmon2"; "lightgoldenrod4"; "linen"; "darkgoldenrod1"; "goldenrod4"; "navy"; "lightcyan2"; "darkgoldenrod"; "mediumorchid2"; "lightsalmon"; "sienna"; "lightgoldenrod"; "plum1"; "orangered4"; "mistyrose1"; "mediumorchid"; "salmon1"; "chocolate3"; "palevioletred"; "purple3"; "turquoise"; "snow"; "paleturquoise"; "darkolivegreen"; "deepskyblue2"; "honeydew1"; "midnightblue"; "steelblue2"; "darkturquoise"; "dimgray"; "mediumpurple4"; "darkorchid"; "seashell2"; "cyan2";
"olivedrab1"; "royalblue2"; "violet"; "seagreen2"; "thistle3"; "cornsilk3"; "moccasin"; "magenta3"; "mediumslateblue"; "cadetblue3"; "mediumaquamarine"; "magenta4"; "mintcream"; "orangered3"; "mistyrose4"; "darkseagreen4"; "orangered"; "palegreen4"; "mediumspringgreen"; "saddlebrown"; "plum3"; "palegreen3"; "darkviolet"; "violetred3"; "orange"; "seagreen"; "springgreen1"; "deeppink2"; "navajowhite1"; "paleturquoise4"; "tan4"; "slategrey"; "lightsteelblue"; "azure3"; "salmon4"; "olivedrab4"; "darkorchid2"; "rosybrown"; "peachpuff2"; "springgreen"; "thistle2"; "tan2"; "aquamarine2"; "rosybrown4"; "palevioletred2"; "slateblue4"; "cyan4"; "red1"; "slateblue1"; "cornsilk2"; "ivory3"; "lightpink2"; "mediumpurple2"; "sienna2"; "chocolate1"; "lightsteelblue3"; "lightgoldenrod3"; "blueviolet"; "sienna3"; "orangered1"; "lightpink3"; "mediumturquoise"; "darkorange2"; "skyblue1"; "steelblue"; "seashell4"; "salmon2"; "lightpink1"; "skyblue4"; "darkslategray4"; "palevioletred4"; "orchid2"; "blue2"; "orchid3";
"peachpuff3"; "transparent"; "lavenderblush4"; "darkslategray1"; "lemonchiffon"; "papayawhip"; "maroon1"; "skyblue"; "chocolate"; "snow2"; "pink1"; "peachpuff"; "tomato1"; "blue1"; "dodgerblue2"; "orchid4"; "plum"; "orange4"; "purple"; "royalblue3"; "pink"; "floralwhite"; "palegreen1"; "dodgerblue4"; "chartreuse"; "bisque4"; "plum4"; "darkseagreen3"; "lightskyblue3"; "darkseagreen1"; "lightblue2"; "royalblue"; "red3"; "salmon3"; "palevioletred1"; "purple4"; "burlywood1"; "chocolate2"; "darkolivegreen3"; "goldenrod2"; "seashell1"; "indianred"; "brown2"; "lemonchiffon1"; "steelblue1"; "thistle1"; "yellow4"; "lightskyblue4"; "skyblue2"; "lemonchiffon2"; "thistle4"; "tomato2"; "violetred4"; "green1"; "greenyellow"; "paleturquoise1"; "chartreuse2"; "darkseagreen"; "turquoise2"; "cyan3"; "olivedrab"; "darkslategrey"; "firebrick4"; "lightgoldenrod1"; "seagreen3"; "seagreen4"; "tomato"; "firebrick1"; "steelblue3"; "orangered2"; "lavenderblush"; "cyan1"; "snow1"; "dodgerblue3"; "rosybrown2";
"indianred2"; "blanchedalmond"; "gold4"; "paleturquoise3"; "honeydew"; "bisque2"; "bisque3"; "snow3"; "brown"; "deeppink1"; "dimgrey"; "lightgoldenrod2"; "lightskyblue2"; "navajowhite2"; "seashell"; "black"; "cadetblue1"; "cadetblue2"; "darkslategray"; "wheat2"; "burlywood"; "brown1"; "deepskyblue4"; "darkslateblue"; "deepskyblue1"; "slategray2"; "darksalmon"; "burlywood3"; "dodgerblue"; "turquoise1"; "grey"; "ghostwhite"; "thistle"; "blue4"; "cornsilk"; "azure"; "darkgoldenrod2"; "darkslategray2"; "beige"; "burlywood2"; "coral3"; "indigo"; "darkorchid4"; "coral"; "burlywood4"; "brown3"; "cornsilk4"; "wheat4"; "darkgoldenrod4"; "cadetblue4"; "brown4"; "cadetblue"; "azure4"; "darkolivegreen2"; "rosybrown3"; "coral4"; "azure2"; "blue3"; "chartreuse1"; "bisque1"; "aquamarine1"; "azure1"; "bisque"; "aquamarine4"; "antiquewhite3"; "antiquewhite2"; "darkorchid3"; "antiquewhite4"; "aquamarine3"; "aquamarine"; "antiquewhite"; "antiquewhite1"; "aliceblue"
]

(** Convert a graph to a dot file *)
let dot_of_statespace (model : AbstractModel.abstract_model) (property_option : AbstractProperty.abstract_property option) (state_space : StateSpace.stateSpace) (algorithm_name : string) : (string * string) =
	(* Retrieve the input options *)
	let options = Input.get_options () in
	
	(* Retrieve info from the graph *)
	let transitions = state_space#get_transitions_table in
	let initial_state_index = state_space#get_initial_state_index in
	
	(* Create the array of dot colors *)
	let dot_colors = Array.of_list dot_colors in
	
	(* Local function checking whether a state is a target state *)
	let is_target_state (state : state) : bool =
		match property_option with
		| Some property ->
			
			(* Try to get the state predicate*)
			let state_predicate_list : state_predicate list = AlgorithmOptions.accepting_state_predicates_of_property property in

			(* Check if at least one state_predicate in hte list satisfies the current state (*** NOTE: not exactly the semantics of generalized conditions! but still visually interesting ***) *)
			List.exists (fun state_predicate ->
				(* Check whether the current state matches ths state predicate *)
				State.match_state_predicate model state_predicate state
			) state_predicate_list
		| None ->
			(* No property: no target state *)
			false
	in
	
	(* Coloring function for each location *)
	let get_location_color = fun location_index is_target ->
		try(
		(* If target location: red *)
		if is_target then "red"
		else 
		(* If normal location: pick color from array *)
			dot_colors.(location_index)
		)
		(* If more colors than our array: white *)
		with Invalid_argument _ -> "white"
	in
	
	
	print_message Verbose_high "\n[dot_of_statespace] Starting to convert states to a graphics.";
	
	let header =
		(* Header *)
	"/************************************************************"
		^ "\n * File automatically generated by " ^ Constants.program_name ^ ""
		^ "\n" ^" * Version  : " ^ (ImitatorUtilities.program_name_and_version_and_nickname_and_build)
		^ "\n" ^" * Model    : " ^ options#model_file_name ^ ""
		^ "\n" ^" * Algorithm: " ^ algorithm_name ^ ""
		^ "\n" ^" * Command  : " ^ (OCamlUtilities.string_of_array_of_string_with_sep " " Sys.argv) ^ ""
		^ "\n" ^" * Generated: " ^ (now()) ^ ""
(*		^ (
			match options#imitator_mode with
				| State_space_exploration -> "\n * State space exploration"
				| EF_synthesis -> "\n * EF-synthesis"
				(* Otherwise: IM / BC *)
				| _ -> 
					let pi0 = Input.get_pi0 () in
					"\n *"
					^ "\n * The following pi0 was considered:"
					^ "\n" ^ (ModelPrinter.string_of_pi0 model pi0)
		)*)
		^ "\n *"
		^ "\n * " ^ (string_of_int (state_space#nb_states)) ^ " states and "
			^ (string_of_int (state_space#nb_transitions)) ^ " transitions"
		^ "\n *" 
		^ "\n * " ^ Constants.program_name ^ " terminated " ^ (after_seconds ())
		^ "\n************************************************************/"
	in
	
	print_message Verbose_high "[dot_of_statespace] Header completed.";

	print_message Verbose_high "[dot_of_statespace] Retrieving states indexes…";

	(* Retrieve the states *)
	let state_indexes = state_space#all_state_indexes in
	
	(* Sort the list (for better presentation in the file) *)
	let state_indexes = List.sort (fun a b -> if a = b then 0 else if a < b then -1 else 1) state_indexes in
	
	print_message Verbose_high "[dot_of_statespace] Starting to convert states…";
	
	(* Sorting function for pairs (combined_transition, target_index) by increasing target_index *)
	let sort_by_target = (fun (_, a) (_, b) -> if a = b then 0 else if a < b then -1 else 1) in

	let states_description =	
		(* Give the state indexes in comments *)
		  "\n"
		^ "\n  DESCRIPTION OF THE STATES"
		^
		(**** BAD PROG ****)
		(let string_states = ref "" in
			List.iter (fun state_index ->
			(* Retrieve location and constraint *)
			let state = state_space#get_state state_index in
			let global_location, linear_constraint = state.global_location, state.px_constraint in

			print_message Verbose_high ("[dot_of_statespace] Converting state " ^ (string_of_int state_index) ^ "");

			(* Eliminate clocks *)
			let parametric_constraint = LinearConstraint.px_hide_nonparameters_and_collapse linear_constraint in
			
			(* Construct the string *)
			string_states := !string_states
				(* Add the state *)
				^ "\n\n  /************************************************************/"
				^ (if initial_state_index = state_index then ("\n  INITIAL") else "")
				^ "\n  STATE " ^ (string_of_int state_index) ^ ":"
				^ "\n  " ^ (ModelPrinter.string_of_state model {global_location = global_location ; px_constraint = linear_constraint;})
				(* Add the projection of the constraint onto the parameters *)
				^ (
					"\n\n  Projection onto the parameters:"
					^ "\n  " ^ (LinearConstraint.string_of_p_linear_constraint model.variable_names parametric_constraint);
				)
				^
				(* Add the projection onto selected parameters, if any *)
				(
				match property_option with
				| Some property ->
					let result =
					match property.projection with
					| None -> ""
					| Some parameter_indices_to_be_projected_onto ->
						(* Compute variables to eliminate *)
						(*** TODO: do only once for all… ***)
						let all_but_projectparameters = list_diff model.parameters parameter_indices_to_be_projected_onto in
						(* Project *)
						let projected_constraint = LinearConstraint.p_hide all_but_projectparameters parametric_constraint in
						(* Print *)
						"\n\n  Projection onto selected parameters {" ^ (string_of_list_of_string_with_sep "," (List.map model.variable_names parameter_indices_to_be_projected_onto)) ^ "}:"
						^ "\n  " ^ (LinearConstraint.string_of_p_linear_constraint model.variable_names projected_constraint);
					in result
				| None ->
					(* No property, no projection: empty string *)
					""
				)
				;
			) state_indexes;
		!string_states)
		^ "\n"
	in
	
	print_message Verbose_high "[dot_of_statespace] Starting to convert transitions…";

	let transitions_description =
		(* Convert the transitions for humans *)
		(*** NOTE: EASY VERSION BUT ORDER IS NON-SPECIFIED ***)
	(*	"\n  DESCRIPTION OF THE TRANSITIONS"
		(* We iterate by updating the current string *)
		^ (Hashtbl.fold (fun source_index successors current_string ->
			current_string ^ (string_of_list_of_string (
					…			
		) transitions ""
		)
		^ "\n"*)
		(*** NOTE: LESS EASY VERSION BUT ORDER IS SPECIFIED (we rank by source states indices, and then by target) ***)
		"\n  /************************************************************/\n  DESCRIPTION OF THE TRANSITIONS"
		(* We iterate on the states *)
		^ (List.fold_left (fun current_string source_index ->
			(* Get the successors *)
			let successors = hashtbl_get_or_default transitions source_index [] in

			current_string ^ (string_of_list_of_string (
				(* Order by successors *)
				let ordered_successors = List.sort sort_by_target successors in
				
				List.map (fun (combined_transition , target_index) ->
					(* Get the action of the combined_transition *)
					let action_index = StateSpace.get_action_from_combined_transition model combined_transition in
					
					(*** HACK! ***)
					let is_nosync action_name =
						String.length action_name >= 7 &&
						String.sub action_name 0 7 = "nosync_" in
						
					let action_name = model.action_names action_index in
					let label = if is_nosync action_name then (
						""
					) else (
						" via \"" ^ action_name ^ "\""
					) in
					
					  "\n  "
					^ "s_" ^ (string_of_int source_index)
					^ " -> "
					^ "s_" ^ (string_of_int target_index)
					^ label
				) ordered_successors
			))
		) "" state_indexes
		)
		^ "\n"
	in
	
	print_message Verbose_high "[dot_of_statespace] Generating dot file…";
	
	let dot_file =
		"\n\ndigraph G { label=\"Trace set for
" ^ options#model_local_file_name ^ "\" labeljust=\"c\" labelloc=\"top\" "
			
		(* Generator information *)
(*		^ "\ninfos[shape=record, style=filled, fillcolor=\"0.99,0.98,0.99\", fontsize=18, label=\"{Trace set for|" ^ options#model_file_name ^ "|Generated by " ^ (ImitatorUtilities.program_name_and_version_and_build) ^ "|Generation time: " ^ (now()) ^ "}\"];"*)
(*		^ "\nname[shape=none, style=bold, fontsize=24, label=\"\"];"
		^ "\ngenerator[shape=none, style=bold, fontsize=10, label=\"\"];"
		^ "\ndate[shape=none, style=bold, fontsize=10, label=\"\"];"*)
(*		(* To ensure the vertical ordering *)
		^ "\n traceset -> name [color=white];"
		^ "\n name -> generator [color=white];"
		^ "\n generator -> date [color=white];"*)
		
		(* Convert the transitions for dot *)
		(* We iterate on the states *)
		^ (List.fold_left (fun current_string source_index ->
			(* Get the successors *)
			let successors = hashtbl_get_or_default transitions source_index [] in
			current_string ^ (string_of_list_of_string (
				(* Order by successors *)
				let ordered_successors = List.sort sort_by_target successors in
				
				List.map (fun (combined_transition , target_index) ->
					(* Get the action of the combined_transition *)
					let action_index = StateSpace.get_action_from_combined_transition model combined_transition in
					
					(*** HACK! ***)
					let is_nosync action_name =
						String.length action_name >= 7 &&
						String.sub action_name 0 7 = "nosync_" in
						
					let action_name = model.action_names action_index in
					let label = if is_nosync action_name then (
						";"
					) else (
						" [label=\"" ^ action_name ^ "\"];"
					) in

					  "\n  "
					^ "s_" ^ (string_of_int source_index)
					^ " -> "
					^ "s_" ^ (string_of_int target_index)
					^ label
				) ordered_successors
			))
		) "" state_indexes
		)

		(* HANDLE INITIAL STATE *)
		^ "\n\n/* Initial state */"
		^ "\n  s_init [shape=none, label=\"init\"];"
		^ "\n  s_init -> s_" ^ (string_of_int initial_state_index) ^ ";"

		(* NOW HANDLE STATES *)
		^ "\n\n/* Colors */\n"

		(*** NOTE: here again, we (might) lose a little efficiency to rather order by increasing state id ***)
		^ (List.fold_left (fun current_string state_index ->
			(* Get the actual state *)
			let state = state_space#get_state state_index in
			let global_location, linear_constraint = state.global_location, state.px_constraint in
			
(*			(* Get the location *)
			let global_location = get_location state_space location_index in*)
			
			(* Get the location index *)
			let location_index = state_space#get_global_location_index state_index in
			
			(* Check whether is target *)
			let is_target = is_target_state state in
			
			(* Find the location color *)
			let location_color = get_location_color location_index is_target in
			
			(* create node index *)
			let node_index = "s_" ^ (string_of_int state_index) in

			if options#graphical_state_space = Graphical_state_space_normal || options#graphical_state_space = Graphical_state_space_verbose then (
				(* create record label with location names *)
				let loc_names = List.map (fun aut_index -> 
					(* Print a structure of the form "automaton_name : location_name" *)
					let loc_index = DiscreteState.get_location global_location aut_index in
					let automaton_name = model.automata_names aut_index in
					let location_name = model.location_names aut_index loc_index in
					automaton_name ^ " : " ^ location_name
				) model.automata in
				let label = string_of_list_of_string_with_sep "|" loc_names in
				let label_discrete = 
					if model.nb_discrete > 0 then (
						"|" ^ (string_of_list_of_string_with_sep "|" (
							List.map (fun discrete_index -> 
	(* 						let loc_index = DiscreteState.get_location global_location aut_index in *)
								"v("
								(* Variable name *)
								^ (model.variable_names discrete_index)
								(* Equal *)
								^ ")="
								(* Variable value *)
								^ (AbstractValue.string_of_value (DiscreteState.get_discrete_value global_location discrete_index))
							) model.discrete
						))
					) else ""
				in
				
				(* Print constraint if requested *)
				let pxd_constraint =
					if options#graphical_state_space = Graphical_state_space_verbose then "|{" ^ (escape_string_for_dot (LinearConstraint.string_of_px_linear_constraint model.variable_names linear_constraint)) else ""
				in
				let p_constraint =
					if options#graphical_state_space = Graphical_state_space_verbose then (
					(* Eliminate clocks *)
					(*** WARNING: already done earlier; hence loss of efficiency ***)
					let parametric_constraint = LinearConstraint.px_hide_nonparameters_and_collapse linear_constraint in
					"|"
					^ (escape_string_for_dot (LinearConstraint.string_of_p_linear_constraint model.variable_names parametric_constraint))
					^
					(* Add the projection onto selected parameters, if any *)
					(
					match property_option with
					| Some property ->
						let result =
						match property.projection with
							| None -> ""
							| Some parameters ->
								(* Compute variables to eliminate *)
								(*** TODO: do only once for all… ***)
								let all_but_projectparameters = list_diff model.parameters parameters in
								(* Project *)
								(*** WARNING: already done earlier; hence loss of efficiency ***)
								let projected_constraint = LinearConstraint.p_hide all_but_projectparameters parametric_constraint in
								(* Print *)
								"|" ^ (escape_string_for_dot (LinearConstraint.string_of_p_linear_constraint model.variable_names projected_constraint));
						in result
					| None ->
						(* No property, no projection: empty string *)
						""
					)
					^ "}"
					) else ""
				in
				
				(* Increase the dot string *)
				current_string
					^ "\n  " ^ node_index
					^ "[fillcolor=" ^ location_color
					^ ", style=filled, shape=Mrecord, label=\"" 
					^ node_index
					(* Add a tag if target location *)
					^ (if is_target then "\n acc" else "")
					^ "|{" 
					^ label ^ label_discrete ^ "}" ^ pxd_constraint ^ p_constraint ^ "\"];";
			) else (
				(* Increase the dot string *)
				current_string
					^ "\n  " ^ node_index
					^ " [color=" ^ location_color
					^ ", style=filled];";
			)
			) "" state_indexes
		)
		
		(* Version and generation time infos *)
		^ "\ngeneration[rotation=90.0, shape=rectangle, fontsize=10, label=\"Generated by " ^ (ImitatorUtilities.program_name_and_version_and_build) ^ "
Git hash: " ^ ImitatorUtilities.git_branch_and_hash ^ "
Generation time: " ^ (now()) ^ "\"];"
		
		^ "\n}"

	in
	print_message Verbose_high "[dot_of_statespace] Done.";

	(* Dot file *)
	header ^ dot_file,
	(* Description of the states (for human) *)
	header ^ states_description ^ transitions_description


(** Execute the `dot` utility with as argument the image format, the radical, and the source file. Returns `Some file_name` if successful, or None otherwise *)
let dot dot_image_extension radical dot_source_file : (string option) =
	(* Retrieve the input options *)
	let options = Input.get_options () in

	(* Get the file names *)
	let dot_file_name = (radical ^ "." ^ dot_file_extension) in
	let image_file_name = (radical ^ "." ^ dot_image_extension) in
	
	(* New line *)
	print_message Verbose_standard "";
	
	(* Create the input file *)
	print_message Verbose_medium ("Creating input file `" ^ dot_file_name ^ "` for dot…");

	(* Write dot file *)
	if options#with_graphics_source then(
		print_message Verbose_standard ("Creating source file for dot…");
	)else(
		print_message Verbose_medium ("Writing to dot file…");
	);
	write_to_file dot_file_name dot_source_file;

	(* Print some information *)
	print_message Verbose_low ("Generating graphical output to `" ^ image_file_name ^ "`…");
	
	let dot_success =
	try (
		(* Prepare the command *)
		let dot_command = Constants.dot_binary_name ^ " -T" ^ dot_image_extension ^ " " ^ dot_file_name ^ " -o " ^ image_file_name ^ "" in
		
		(* Print some information *)
		print_message Verbose_high ("About to execute the following command: " ^ dot_command);

		(* Actually call dot *)
		let command_result = Sys.command dot_command in
		
		(* Print some information *)
		print_message Verbose_medium ("Result of the `dot` command: " ^ (string_of_int command_result));
		
		if command_result <> 0 then(
			print_error ("Something went wrong when calling `dot`. Exit code: " ^ (string_of_int command_result) ^ ". Maybe you forgot to install the `dot` utility (from the `graphviz` package in Debian).");
			(* Something went wrong *)
			false
			)
		else(
			(* Print some information *)
			print_message Verbose_low ("Graphical output successfully generated to `" ^ image_file_name ^ "`.");
			
			(* Everything is fine *)
			true
		)
	) with 
		| Sys_error error_message ->
			print_error ("System error while calling `dot`. Error message: `" ^ error_message ^ "`.");
			(* Something went wrong *)
			false
	in
	
	(* Removing dot file (except if option) *)
	if not options#with_graphics_source then(
		print_message Verbose_medium ("Removing dot file…");
		delete_file dot_file_name;
	);
	
	(* Return None if something went wrong, or the file name otherwise *)
	if dot_success then
		Some image_file_name
	else None
	

(** `draw_statespace state_space algorithm_name radical` draws the state space using dot, if required by the options. *)
let draw_statespace_if_requested (model : AbstractModel.abstract_model) (property_option : AbstractProperty.abstract_property option) (state_space : StateSpace.stateSpace) algorithm_name radical : unit =
	(* Statistics *)
	counter_graphics_statespace#start;

	(* Retrieve the input options *)
	let options = Input.get_options () in
	
	(* Do not write if no dot AND no log *)
	if options#graphical_state_space <> Graphical_state_space_none || options#states_description then (
		(* Preliminary check: the state space shall not be empty *)
		if (state_space#nb_states) = 0 then (
			print_warning "State space is empty: not drawing";
		)else(

			let dot_model, states = dot_of_statespace model property_option state_space algorithm_name in

			(* Write states file if needed *)
			if options#states_description then (
				let states_file_name = (radical ^ "." ^ states_file_extension) in
				print_message Verbose_standard ("Writing the states description to file `" ^ states_file_name ^ "`…");
				write_to_file states_file_name states;
			);

			(* Generate graphical state space if needed *)
			if options#graphical_state_space <> Graphical_state_space_none then(
				(* Call the dedicated function that returns a string option *)
				let dot_success = dot state_space_image_format radical dot_model in

				match dot_success with
				| None -> print_error "Oops…! Something went wrong with dot when drawing the state space."
				| Some created_file -> print_message Verbose_standard ("Graphical state space successfully created in `" ^ created_file ^ "`.")
			);
		);

	);

	(* Statistics *)
	counter_graphics_statespace#stop;
	
	(* The end *)
	()





(************************************************************)
(* Meta programming (could have been written in Python for example) *)
(************************************************************)


(*let dot_colors = [

(* Then all the other one by alphabetic order *)
"aliceblue" ; "antiquewhite" ; "antiquewhite1" ; "antiquewhite2" ; "antiquewhite3" ;
"antiquewhite4" ; "aquamarine" ; "aquamarine1" ; "aquamarine2" ; "aquamarine3" ; 
"aquamarine4" ; "azure" ; "azure1" ; "azure2" ; "azure3" ; 
"azure4" ; "beige" ; "bisque" ; "bisque1" ; "bisque2" ; 
"bisque3" ; "bisque4" ; "black" ; "blanchedalmond" ; (*"blue" ;*) 
"blue1" ; "blue2" ; "blue3" ; "blue4" ; "blueviolet" ; 
"brown" ; "brown1" ; "brown2" ; "brown3" ; "brown4" ; 
"burlywood" ; "burlywood1" ; "burlywood2" ; "burlywood3" ; "burlywood4" ; 
"cadetblue" ; "cadetblue1" ; "cadetblue2" ; "cadetblue3" ; "cadetblue4" ; 
"chartreuse" ; "chartreuse1" ; "chartreuse2" ; "chartreuse3" ; "chartreuse4" ; 
"chocolate" ; "chocolate1" ; "chocolate2" ; "chocolate3" ; "chocolate4" ; 
"coral" ; "coral1" ; "coral2" ; "coral3" ; "coral4" ; 
"cornflowerblue" ; "cornsilk" ; "cornsilk1" ; "cornsilk2" ; "cornsilk3" ; 
"cornsilk4" ; "crimson" ; "cyan" ; "cyan1" ; "cyan2" ; 
"cyan3" ; "cyan4" ; "darkgoldenrod" ; "darkgoldenrod1" ; "darkgoldenrod2" ; 
"darkgoldenrod3" ; "darkgoldenrod4" ; "darkgreen" ; "darkkhaki" ; "darkolivegreen" ; 
"darkolivegreen1" ; "darkolivegreen2" ; "darkolivegreen3" ; "darkolivegreen4" ; "darkorange" ; 
"darkorange1" ; "darkorange2" ; "darkorange3" ; "darkorange4" ; "darkorchid" ; 
"darkorchid1" ; "darkorchid2" ; "darkorchid3" ; "darkorchid4" ; "darksalmon" ; 
"darkseagreen" ; "darkseagreen1" ; "darkseagreen2" ; "darkseagreen3" ; "darkseagreen4" ; 
"darkslateblue" ; "darkslategray" ; "darkslategray1" ; "darkslategray2" ; "darkslategray3" ; 
"darkslategray4" ; "darkslategrey" ; "darkturquoise" ; "darkviolet" ; "deeppink" ; 
"deeppink1" ; "deeppink2" ; "deeppink3" ; "deeppink4" ; "deepskyblue" ; 
"deepskyblue1" ; "deepskyblue2" ; "deepskyblue3" ; "deepskyblue4" ; "dimgray" ; 
"dimgrey" ; "dodgerblue" ; "dodgerblue1" ; "dodgerblue2" ; "dodgerblue3" ; 
"dodgerblue4" ; "firebrick" ; "firebrick1" ; "firebrick2" ; "firebrick3" ; 
"firebrick4" ; "floralwhite" ; "forestgreen" ; "gainsboro" ; "ghostwhite" ; 
"   gold   " ; "gold1" ; "gold2" ; "gold3" ; "gold4" ; 
"goldenrod" ; "goldenrod1" ; "goldenrod2" ; "goldenrod3" ; "goldenrod4" ; 
(*"   gray   " ; "gray0" ; "gray1" ; "gray2" ; "gray3" ; 
"gray4" ; "gray5" ; "gray6" ; "gray7" ; "gray8" ; 
"gray9" ; "gray10" ; "gray11" ; "gray12" ; "gray13" ; 
"gray14" ; "gray15" ; "gray16" ; "gray17" ; "gray18" ; 
"gray19" ; "gray20" ; "gray21" ; "gray22" ; "gray23" ; 
"gray24" ; "gray25" ; "gray26" ; "gray27" ; "gray28" ; 
"gray29" ; "gray30" ; "gray31" ; "gray32" ; "gray33" ; 
"gray34" ; "gray35" ; "gray36" ; "gray37" ; "gray38" ; 
"gray39" ; "gray40" ; "gray41" ; "gray42" ; "gray43" ; 
"gray44" ; "gray45" ; "gray46" ; "gray47" ; "gray48" ; 
"gray49" ; "gray50" ; "gray51" ; "gray52" ; "gray53" ; 
"gray54" ; "gray55" ; "gray56" ; "gray57" ; "gray58" ; 
"gray59" ; "gray60" ; "gray61" ; "gray62" ; "gray63" ; 
"gray64" ; "gray65" ; "gray66" ; "gray67" ; "gray68" ; 
"gray69" ; "gray70" ; "gray71" ; "gray72" ; "gray73" ; 
"gray74" ; "gray75" ; "gray76" ; "gray77" ; "gray78" ; 
"gray79" ; "gray80" ; "gray81" ; "gray82" ; "gray83" ; 
"gray84" ; "gray85" ; "gray86" ; "gray87" ; "gray88" ; 
"gray89" ; "gray90" ; "gray91" ; "gray92" ; "gray93" ; 
"gray94" ; "gray95" ; "gray96" ; "gray97" ; "gray98" ; 
"gray99" ; "gray100" ;*) (*"green" ;*) "green1" ; "green2" ; 
"green3" ; "green4" ; "greenyellow" ; "grey"; (* "grey0" ; 
"grey1" ; "grey2" ; "grey3" ; "grey4" ; "grey5" ; 
"grey6" ; "grey7" ; "grey8" ; "grey9" ; "grey10" ; 
"grey11" ; "grey12" ; "grey13" ; "grey14" ; "grey15" ; 
"grey16" ; "grey17" ; "grey18" ; "grey19" ; "grey20" ; 
"grey21" ; "grey22" ; "grey23" ; "grey24" ; "grey25" ; 
"grey26" ; "grey27" ; "grey28" ; "grey29" ; "grey30" ; 
"grey31" ; "grey32" ; "grey33" ; "grey34" ; "grey35" ; 
"grey36" ; "grey37" ; "grey38" ; "grey39" ; "grey40" ; 
"grey41" ; "grey42" ; "grey43" ; "grey44" ; "grey45" ; 
"grey46" ; "grey47" ; "grey48" ; "grey49" ; "grey50" ; 
"grey51" ; "grey52" ; "grey53" ; "grey54" ; "grey55" ; 
"grey56" ; "grey57" ; "grey58" ; "grey59" ; "grey60" ; 
"grey61" ; "grey62" ; "grey63" ; "grey64" ; "grey65" ; 
"grey66" ; "grey67" ; "grey68" ; "grey69" ; "grey70" ; 
"grey71" ; "grey72" ; "grey73" ; "grey74" ; "grey75" ; 
"grey76" ; "grey77" ; "grey78" ; "grey79" ; "grey80" ; 
"grey81" ; "grey82" ; "grey83" ; "grey84" ; "grey85" ; 
"grey86" ; "grey87" ; "grey88" ; "grey89" ; "grey90" ; 
"grey91" ; "grey92" ; "grey93" ; "grey94" ; "grey95" ; 
"grey96" ; "grey97" ; "grey98" ; "grey99" ; "grey100" ; *)
"honeydew" ; "honeydew1" ; "honeydew2" ; "honeydew3" ; "honeydew4" ; 
"hotpink" ; "hotpink1" ; "hotpink2" ; "hotpink3" ; "hotpink4" ; 
"indianred" ; "indianred1" ; "indianred2" ; "indianred3" ; "indianred4" ; 
"indigo" ; "ivory" ; "ivory1" ; "ivory2" ; "ivory3" ; 
"ivory4" ; "khaki" ; "khaki1" ; "khaki2" ; "khaki3" ; 
"khaki4" ; "lavender" ; "lavenderblush" ; "lavenderblush1" ; "lavenderblush2" ; 
"lavenderblush3" ; "lavenderblush4" ; "lawngreen" ; "lemonchiffon" ; "lemonchiffon1" ; 
"lemonchiffon2" ; "lemonchiffon3" ; "lemonchiffon4" ; "lightblue" ; "lightblue1" ; 
"lightblue2" ; "lightblue3" ; "lightblue4" ; "lightcoral" ; "lightcyan" ; 
"lightcyan1" ; "lightcyan2" ; "lightcyan3" ; "lightcyan4" ; "lightgoldenrod" ; 
"lightgoldenrod1" ; "lightgoldenrod2" ; "lightgoldenrod3" ; "lightgoldenrod4" ; "lightgoldenrodyellow" ; 
"lightgray" ; "lightgrey" ; "lightpink" ; "lightpink1" ; "lightpink2" ; 
"lightpink3" ; "lightpink4" ; "lightsalmon" ; "lightsalmon1" ; "lightsalmon2" ; 
"lightsalmon3" ; "lightsalmon4" ; "lightseagreen" ; "lightskyblue" ; "lightskyblue1" ; 
"lightskyblue2" ; "lightskyblue3" ; "lightskyblue4" ; "lightslateblue" ; "lightslategray" ; 
"lightslategrey" ; "lightsteelblue" ; "lightsteelblue1" ; "lightsteelblue2" ; "lightsteelblue3" ; 
"lightsteelblue4" ; "lightyellow" ; "lightyellow1" ; "lightyellow2" ; "lightyellow3" ; 
"lightyellow4" ; "limegreen" ; "linen" ; (*"magenta" ;*) "magenta1" ; 
"magenta2" ; "magenta3" ; "magenta4" ; "maroon" ; "maroon1" ; 
"maroon2" ; "maroon3" ; "maroon4" ; "mediumaquamarine" ; "mediumblue" ; 
"mediumorchid" ; "mediumorchid1" ; "mediumorchid2" ; "mediumorchid3" ; "mediumorchid4" ; 
"mediumpurple" ; "mediumpurple1" ; "mediumpurple2" ; "mediumpurple3" ; "mediumpurple4" ; 
"mediumseagreen" ; "mediumslateblue" ; "mediumspringgreen" ; "mediumturquoise" ; "mediumvioletred" ; 
"midnightblue" ; "mintcream" ; "mistyrose" ; "mistyrose1" ; "mistyrose2" ; 
"mistyrose3" ; "mistyrose4" ; "moccasin" ; "navajowhite" ; "navajowhite1" ; 
"navajowhite2" ; "navajowhite3" ; "navajowhite4" ; "   navy   " ; "navyblue" ; 
"oldlace" ; "olivedrab" ; "olivedrab1" ; "olivedrab2" ; "olivedrab3" ; 
"olivedrab4" ; "orange" ; "orange1" ; "orange2" ; "orange3" ; 
"orange4" ; "orangered" ; "orangered1" ; "orangered2" ; "orangered3" ; 
"orangered4" ; "orchid" ; "orchid1" ; "orchid2" ; "orchid3" ; 
"orchid4" ; "palegoldenrod" ; "palegreen" ; "palegreen1" ; "palegreen2" ; 
"palegreen3" ; "palegreen4" ; "paleturquoise" ; "paleturquoise1" ; "paleturquoise2" ; 
"paleturquoise3" ; "paleturquoise4" ; "palevioletred" ; "palevioletred1" ; "palevioletred2" ; 
"palevioletred3" ; "palevioletred4" ; "papayawhip" ; "peachpuff" ; "peachpuff1" ; 
"peachpuff2" ; "peachpuff3" ; "peachpuff4" ; "   peru   " ; "   pink   " ; 
"pink1" ; "pink2" ; "pink3" ; "pink4" ; "   plum   " ; 
"plum1" ; "plum2" ; "plum3" ; "plum4" ; "powderblue" ; 
"purple" ; "purple1" ; "purple2" ; "purple3" ; "purple4" ; 
(*"red" ;*) "red1" ; "   red2   " ; "   red3   " ; "   red4   " ; 
"rosybrown" ; "rosybrown1" ; "rosybrown2" ; "rosybrown3" ; "rosybrown4" ; 
"royalblue" ; "royalblue1" ; "royalblue2" ; "royalblue3" ; "royalblue4" ; 
"saddlebrown" ; "salmon" ; "salmon1" ; "salmon2" ; "salmon3" ; 
"salmon4" ; "sandybrown" ; "seagreen" ; "seagreen1" ; "seagreen2" ; 
"seagreen3" ; "seagreen4" ; "seashell" ; "seashell1" ; "seashell2" ; 
"seashell3" ; "seashell4" ; "sienna" ; "sienna1" ; "sienna2" ; 
"sienna3" ; "sienna4" ; "skyblue" ; "skyblue1" ; "skyblue2" ; 
"skyblue3" ; "skyblue4" ; "slateblue" ; "slateblue1" ; "slateblue2" ; 
"slateblue3" ; "slateblue4" ; "slategray" ; "slategray1" ; "slategray2" ; 
"slategray3" ; "slategray4" ; "slategrey" ; "   snow   " ; "snow1" ; 
"snow2" ; "snow3" ; "snow4" ; "springgreen" ; "springgreen1" ; 
"springgreen2" ; "springgreen3" ; "springgreen4" ; "steelblue" ; "steelblue1" ; 
"steelblue2" ; "steelblue3" ; "steelblue4" ; "   tan   " ; "   tan1   " ; 
"   tan2   " ; "   tan3   " ; "   tan4   " ; "thistle" ; "thistle1" ; 
"thistle2" ; "thistle3" ; "thistle4" ; "tomato" ; "tomato1" ; 
"tomato2" ; "tomato3" ; "tomato4" ; "transparent" ; "turquoise" ; 
"turquoise1" ; "turquoise2" ; "turquoise3" ; "turquoise4" ; "violet" ; 
"violetred" ; "violetred1" ; "violetred2" ; "violetred3" ; "violetred4" ; 
"wheat" ; "wheat1" ; "wheat2" ; "wheat3" ; "wheat4" ; 
"white" ; "whitesmoke" ; (*"yellow" ;*) "yellow1" ; "yellow2" ; 
"yellow3" ; "yellow4" ; "yellowgreen"
]*)


(*(* Shuffle dot colors: should be executed only once!! *)
let shuffle_dot_colors =
	let shuffle = 
		Array.sort (fun _ _ -> (Random.int 3) - 1)
	in
	let colors = Array.of_list dot_colors in
	shuffle colors;
	Array.iter (fun color ->
		print_string ("\"" ^ color ^ "\"; ");
	) colors;
	terminate_program();*)

