* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * 
  * 
  *                        IMITATOR 
  * 
  * Université Paris 13 , LIPN , CNRS , France 
  * 
  * Module description : Dynamic elimination of clocks not used in the future [ Andre13 , FSFMA ] 
  * 
  * File contributors :   ,   
  * Created            : 2015/11/27 
  * 
  * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
 *
 *                       IMITATOR
 *
 * Université Paris 13, LIPN, CNRS, France
 *
 * Module description: Dynamic elimination of clocks not used in the future [Andre13, FSFMA]
 *
 * File contributors : Étienne André, Jaime Arias
 * Created           : 2015/11/27
 *
 ************************************************************)


(**************************************************************)
(* Modules *)
(**************************************************************)
open OCamlUtilities
open ImitatorUtilities
open Exceptions
open Statistics
open AbstractModel





(**************************************************************)
(* Global variable *)
(**************************************************************)
let useless_clocks = ref None (* not yet initialized *)


(**************************************************************)
(* Statistics *)
(**************************************************************)
let counter_preparation = ref None
let counter_elimination = ref None


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

*  to the function defined in ModelConverter
let get_clocks_in_updates = ModelConverter.get_clocks_in_updates

let get_clocks_in_guard clocks : guard -> Automaton.clock_index list = function
  | True_guard -> []
  | False_guard -> []
  | Discrete_guard _ -> []
  | Continuous_guard continuous_guard -> LinearConstraint.pxd_find_variables clocks continuous_guard
  | Discrete_continuous_guard discrete_continuous_guard -> LinearConstraint.pxd_find_variables clocks discrete_continuous_guard.continuous_guard

let is_constrained_in_guard clock_index : guard -> bool = function
  | True_guard -> false
  | False_guard -> false
  | Discrete_guard _ -> false
  | Continuous_guard continuous_guard -> LinearConstraint.pxd_is_constrained continuous_guard clock_index
  | Discrete_continuous_guard discrete_continuous_guard -> LinearConstraint.pxd_is_constrained discrete_continuous_guard.continuous_guard clock_index


(*------------------------------------------------------------*)
(* Find the local clocks per automaton *)
(*------------------------------------------------------------*)
(*** WARNING: the use of clock_offset is not beautiful (and error prone) here ***)
let find_local_clocks () =
  (* Retrieve the model *)
  let model = Input.get_model() in

  (*** HACK: yes, clock_offset is the number of parameters, but quite hard coded ***)
  let clock_offset = model.nb_parameters in

  (* Create an empty array for the clocks of each automaton *)
  let clocks_per_automaton = Array.make model.nb_automata [] in

  (* Create an empty array for the local clocks of each automaton *)
  let local_clocks_per_automaton = Array.make model.nb_automata [] in

  (* Create an empty array for the automata associated with each clock *)
  let automata_per_clock = Array.make model.nb_clocks [] in

  (* For each automaton *)
  for automaton_index = 0 to model.nb_automata - 1 do
    (* Get the locations for this automaton *)
    let locations = model.locations_per_automaton automaton_index in

    (* For each location *)
    let clocks_for_locations = List.fold_left (fun list_of_clocks_for_previous_locations location_index ->
        (* Get the clocks in the invariant *)
        let invariant = model.invariants automaton_index location_index in
        let clocks_in_invariant = get_clocks_in_guard model.clocks invariant in
        (* Get the clocks from the stopwatches *)
        let clocks_in_stopwatches = model.stopwatches automaton_index location_index in

        (* Now find clocks in guards *)
        (* For each action for this automaton and location *)
        let actions_for_this_location = model.actions_per_location automaton_index location_index in
        let clocks_for_actions = List.fold_left (fun list_of_clocks_for_previous_actions action_index ->
            (* For each transition for this automaton, location and action *)
            let transitions_for_this_action = List.map model.transitions_description (model.transitions automaton_index location_index action_index) in

            let clocks_for_transitions = List.fold_left (fun list_of_clocks_for_previous_transitions transition ->
                (* Name the elements in the transition *)
                let guard , updates = transition.guard, transition.updates in

                let clocks_in_guards = get_clocks_in_guard model.clocks guard in
                let clocks_in_updates = get_clocks_in_updates updates in

  Add these 2 new lists to the current list
                List.rev_append (List.rev_append clocks_in_guards clocks_in_updates) list_of_clocks_for_previous_transitions
              ) [] transitions_for_this_action in

            (* Add the list for this action to the one for previous actions *)
            List.rev_append clocks_for_transitions list_of_clocks_for_previous_actions
          ) [] actions_for_this_location in

        (* Add all clocks *)
        List.rev_append (List.rev_append (List.rev_append clocks_in_invariant clocks_in_stopwatches) clocks_for_actions) list_of_clocks_for_previous_locations
      ) [] locations in

    (* Collapse the list *)
    let clocks_for_this_automaton = list_only_once clocks_for_locations in
    (* Update the clocks per automaton *)
    clocks_per_automaton.(automaton_index) <- clocks_for_this_automaton;
    (* Update the automaton for all clocks *)
    List.iter (fun clock ->
        (* Add current automaton to the list of automata for this clock *)
        automata_per_clock.(clock - clock_offset) <- (automaton_index :: automata_per_clock.(clock - clock_offset));
      ) clocks_for_this_automaton;
  done; (* end for each automaton *)

  (* Now compute the local clocks *)
  for clock_index = clock_offset to clock_offset + model.nb_clocks - 1 do
    (* Retrieve the automata in which this clock appears *)
    let automata_for_this_clock = automata_per_clock.(clock_index - clock_offset) in
  If size is 1 , the clock is local
    match automata_for_this_clock with
    (* Only one element: clock is local *)
    | [automaton_index] ->
      (* 				print_message Verbose_high ("Automaton " ^ (string_of_int automaton_index) ^ " has local clock " ^ (string_of_int clock_index)); *)
      (* Add the clock to the automaton *)
      local_clocks_per_automaton.(automaton_index) <- (clock_index) :: local_clocks_per_automaton.(automaton_index);
      (* Otherwise, clock is not local *)
    | _ -> ()
  done;

  local_clocks_per_automaton


(*------------------------------------------------------------*)
(* Find the useless clocks in automata locations *)
(*------------------------------------------------------------*)
(** NOTE: this function is not related to model conversion, and could (should?) be defined elsewhere *)
let find_useless_clocks_in_automata local_clocks_per_automaton =

  (* Retrieve the model *)
  let model = Input.get_model() in

  (* Create the data structure *)
  let useless_clocks_per_location = Array.make model.nb_automata (Array.make 0 []) in

  (* For each automaton *)
  for automaton_index = 0 to model.nb_automata - 1 do


    (* Get the locations for this automaton *)
    let locations_for_this_automaton = model.locations_per_automaton automaton_index in
    let nb_locations = List.length locations_for_this_automaton in

  Initialize the data structure for this automaton
    useless_clocks_per_location.(automaton_index) <- Array.make nb_locations [];

    (* Retrieve the local clocks for this automaton *)
    let local_clocks = local_clocks_per_automaton.(automaton_index) in

    (* Compute the predecessor locations and lists of local clock reset *)
    let predecessors = Array.make nb_locations [] in
    (* For each location in this automaton: *)
    List.iter (fun location_index ->
        (* Get the actions for this location *)
        let actions_for_this_location = model.actions_per_location automaton_index location_index in

        (* For each action available in this location *)
        List.iter (fun action_index ->
            (* Retrieve the transitions from this location & action *)
            let transitions = List.map model.transitions_description (model.transitions automaton_index location_index action_index) in

            (* For each transition starting from this location *)
            (** TODO: What happens here with the clock updates ?? *)
            List.iter (fun transition ->

                (* Get the clocks updated or reset *)
                let reset_clocks = ModelConverter.get_clocks_in_updates transition.updates in

                (* Compute the local clocks updated or reset *)
                let reset_local_clocks = list_inter reset_clocks local_clocks in
                (* Update the predecessors *)
                predecessors.(transition.target) <- (location_index, reset_local_clocks) :: predecessors.(transition.target);
              ) transitions; (* end for each transition *)
          ) actions_for_this_location; (* end for each action *)
      ) locations_for_this_automaton; (* end for each location *)

    (* Print some information *)
    if verbose_mode_greater Verbose_total then(
      print_message Verbose_total ("Computed predecessor locations and clock resets for automaton '" ^ (model.automata_names automaton_index) ^ "'");
      (* Iterate on locations *)
      List.iter (fun location_index ->
          print_message Verbose_total ("  Location '" ^ (model.location_names automaton_index location_index) ^ "' has predecessors:");
          let predecessors_string = string_of_list_of_string_with_sep ", " (List.map (
              fun (source_index, reset_local_clocks) ->
                (model.location_names automaton_index source_index) ^ "[resets: " ^ (string_of_list_of_string_with_sep ", " (List.map model.variable_names reset_local_clocks)) ^ "]"
            ) predecessors.(location_index)) in
          print_message Verbose_total ("    " ^ predecessors_string);
        ) locations_for_this_automaton; (* end for each location *)
    );

    (* For each local clock for this automaton *)
    List.iter(fun clock_index ->
        (* Create a list of marked locations (i.e., where the clock is useful) *)
        let marked = ref (list_union
                            (* All locations with an invariant involving this clock *)
                            (List.filter (fun location_index ->
                                 (* Retrieve the invariant *)
                                 let invariant = model.invariants automaton_index location_index in
                                 (* Check if the clock is present in the invariant *)
                                 let constrained = is_constrained_in_guard clock_index invariant in
                                 (* Print some information *)
                                 print_message Verbose_total ("Clock '" ^ (model.variable_names clock_index) ^ "' is " ^ (if constrained then "" else "NOT ") ^ "constrained in invariant of location '" ^ (model.location_names automaton_index location_index) ^ "'");
                                 (* Return true or false *)
                                 constrained
                               ) locations_for_this_automaton
                            )
                            (* All predecessor locations of transitions with a guard involving this clock *)
                            (
                              (* For each location *)
                              List.fold_left (fun current_list_of_locations location_index ->
                                  (* Get the actions for this location *)
                                  let actions_for_this_location = model.actions_per_location automaton_index location_index in
                                  (* For each action available in this location *)
                                  List.fold_left (fun current_list_of_locations action_index ->
                                      (* Retrieve the transitions from this location & action *)
                                      let transitions = List.map model.transitions_description (model.transitions automaton_index location_index action_index) in
                                      (* Check if there exists a guard in an outgoing transition where the clock is constrained *)
                                      let exists_guard = List.exists (fun transition ->
                                          (* Check if the clock is present in the guard *)
                                          let constrained = is_constrained_in_guard clock_index transition.guard in
                                          (* Print some information *)
                                          if constrained then (
                                            print_message Verbose_high ("Found a transition where clock '" ^ (model.variable_names clock_index) ^ "' is constrained in guard from location '" ^ (model.location_names automaton_index location_index) ^ "', through '" ^ (model.action_names action_index) ^ "'");
                                          ) else (
                                            print_message Verbose_total ("Clock '" ^ (model.variable_names clock_index) ^ "' is not constrained in guard from location '" ^ (model.location_names automaton_index location_index) ^ "' through '" ^ (model.action_names action_index) ^ "'");
                                          );
                                          (* Return true or false *)
                                          constrained
                                        ) transitions in
                                      (* Keep the location if there exists a guard *)
                                      if exists_guard then location_index :: current_list_of_locations
                                      else current_list_of_locations
                                    ) current_list_of_locations actions_for_this_location
                                ) [] locations_for_this_automaton
                            )
                         ) in

        (* Create a waiting list *)
        let waiting = ref !marked in

        (* Print some information *)
        if verbose_mode_greater Verbose_medium then(
          print_message Verbose_medium ("Starting the dynamic clock elimination algorithm for local clock '" ^ (model.variable_names clock_index) ^ "' in automaton '" ^ (model.automata_names automaton_index) ^ "', with initial marked states:");
          print_message Verbose_medium (	"  " ^ (string_of_list_of_string_with_sep ", " (List.map (model.location_names automaton_index) !marked)));
        );

        (* Start the algorithm *)
        while !waiting <> [] do
          (* Pick a location from the waiting list *)
          match !waiting with
          | location_index :: rest ->
            (* Print some information *)
            print_message Verbose_medium ("Pick up location '" ^ (model.location_names automaton_index location_index) ^ "'");
  Remove the first element
            waiting := rest;
            (* For each transition leading to this location *)
            List.iter (fun (source_index, reset_local_clocks) ->
                (* Print some information *)
                print_message Verbose_high ("Considering predecessor transition from '" ^ (model.location_names automaton_index source_index) ^ "'");
                (* If the clock is not reset by the transition *)
                if not (List.mem clock_index reset_local_clocks) then(
                  (* Print some information *)
                  print_message Verbose_high ("Clock not reset by a transition.");
                  (* If the source location does not belong to the marked list *)
                  if not (List.mem source_index !marked) then(
                    (* Add it to the marked list *)
                    marked := source_index :: !marked;
                    print_message Verbose_high ("Location marked.");
                    (* Add it to the waiting list (if not present) *)
                    if not (List.mem source_index !waiting) then
                      print_message Verbose_high ("Location added to waiting list.");
                    waiting := source_index :: !waiting;
                  ); (* end if not in marked list *)
                );(* end if clock not reset *)
              ) predecessors.(location_index); (* end for each transition *)

          | _ -> raise (InternalError "Impossible situation: list should not be empty.");

            (* End the algorithm *)
        done;

        (* Return the list of locations where the clock can be removed *)
        let useless_locations = list_diff locations_for_this_automaton !marked in

        (* Print some information *)
        if verbose_mode_greater Verbose_low then(
          print_message Verbose_low ("List of useless locations for local clock '" ^ (model.variable_names clock_index) ^ "' in automaton '" ^ (model.automata_names automaton_index) ^ "'");
          print_message Verbose_low ("  " ^ (string_of_list_of_string_with_sep ", " (List.map (model.location_names automaton_index) useless_locations)));
        );

        (* Update the data structure *)
        List.iter (fun location_index ->
            (useless_clocks_per_location.(automaton_index)).(location_index) <- clock_index :: (useless_clocks_per_location.(automaton_index)).(location_index);
          ) useless_locations;


      ) local_clocks; (* end for each local clock *)
  done; (* end for each automaton *)

  (* Return a functional structure *)
  (fun automaton_index location_index ->
     (useless_clocks_per_location.(automaton_index)).(location_index)
  )



(*------------------------------------------------------------*)
(* Function for preparing data structures for dynamic clock elimination *)
(*------------------------------------------------------------*)
(* NOTE: This function is only called if the dynamic clock elimination option is activated *)
let prepare_clocks_elimination () =
  (* Create counters *)
  let counter_preparation_ref = create_time_counter_and_register "dynamic clock elimination (preparation)" Algorithm_counter Verbose_standard in
  counter_preparation := Some counter_preparation_ref;
  counter_elimination := Some (create_hybrid_counter_and_register "dynamic clock elimination" Algorithm_counter Verbose_standard);

  (* Start counter *)
  counter_preparation_ref#start;

  (* Retrieve the model *)
  let model = Input.get_model() in

  (* Compute the local clocks per automaton *)
  print_message Verbose_low ("*** Building local clocks per automaton…");
  let local_clocks_per_automaton = find_local_clocks () in

  (* Debug print: local clocks per automaton *)
  if verbose_mode_greater Verbose_total then(
    print_message Verbose_total ("\n*** Local clocks per automaton:");
    (* For each automaton *)
    List.iter (fun automaton_index ->
        (* Get the actions *)
        let clocks = local_clocks_per_automaton.(automaton_index) in
        (* Print it *)
        let clocks_string = string_of_list_of_string_with_sep ", " (List.map model.variable_names clocks) in
        print_message Verbose_total ("  " ^ (model.automata_names automaton_index) ^ " : " ^ clocks_string)
      ) model.automata;
  );


  (* Compute and update useless clocks *)
  print_message Verbose_low ("*** Building useless clocks per location per automaton…");
  useless_clocks := Some (find_useless_clocks_in_automata local_clocks_per_automaton);

  (* Stop counter *)
  counter_preparation_ref#stop;

  (* The end *)
  ()


(*------------------------------------------------------------*)
(* Eliminating useless clocks in a linear constraint *)
(*------------------------------------------------------------*)
let dynamic_clock_elimination target_location current_constraint =
  (* Get counter *)
  let counter_elimination = match !counter_elimination with
    | Some counter_elimination -> counter_elimination
    | None -> raise (InternalError("Counter counter_elimination not yet initialized in ClockElimination.dynamic_clock_elimination"))
  in

  (* Start counter *)
  counter_elimination#start;
  (* Increment counter *)
  counter_elimination#increment;

  (* Retrieve the model *)
  let model = Input.get_model() in

  First check that initialization was performed
  let compute_clocks_to_eliminate =
    match !useless_clocks with
    | None -> raise (InternalError ("Trying to perform dynamic clock elimination before initializing the clocks to eliminate."))
    | Some f -> f
  in

  (* Compute the useless clocks *)
  let clocks_to_remove = List.fold_left (fun current_list_of_clocks automaton_index ->
      (* Retrieve target location for this automaton *)
      let location_index = Location.get_location target_location automaton_index in
      (* Get the clocks and append to previously computed clocks (rev_append because the order doesn't matter) *)
      List.rev_append current_list_of_clocks (compute_clocks_to_eliminate automaton_index location_index)
    ) [] model.automata in
  (* Print some information *)
  if verbose_mode_greater Verbose_low then(
    if clocks_to_remove = [] then print_message Verbose_low ("No clock will be dynamically removed.")
    else print_message Verbose_low ("The following clock" ^ (s_of_int (List.length clocks_to_remove)) ^ " will be dynamically removed: {" ^ (string_of_list_of_string_with_sep ", " (List.map model.variable_names clocks_to_remove)) ^ "}");
  );

  print_message Verbose_high ("\nRemoving useless clocks ");
  LinearConstraint.px_hide_assign clocks_to_remove current_constraint;
  (* Print some information *)
  if verbose_mode_greater Verbose_total then(
    print_message Verbose_total (LinearConstraint.string_of_px_linear_constraint model.variable_names current_constraint);
  );

  (* Stop counter *)
  counter_elimination#stop;

  (* The end *)
  ()

************************************************************
 Modules 
************************************************************
************************************************************
 Global variable 
************************************************************
 not yet initialized 
************************************************************
 Statistics 
************************************************************
************************************************************
 Functions 
************************************************************
------------------------------------------------------------
 Find the local clocks per automaton 
------------------------------------------------------------
** WARNING: the use of clock_offset is not beautiful (and error prone) here **
 Retrieve the model 
** HACK: yes, clock_offset is the number of parameters, but quite hard coded **
 Create an empty array for the clocks of each automaton 
 Create an empty array for the local clocks of each automaton 
 Create an empty array for the automata associated with each clock 
 For each automaton 
 Get the locations for this automaton 
 For each location 
 Get the clocks in the invariant 
 Get the clocks from the stopwatches 
 Now find clocks in guards 
 For each action for this automaton and location 
 For each transition for this automaton, location and action 
 Name the elements in the transition 
 Add the list for this action to the one for previous actions 
 Add all clocks 
 Collapse the list 
 Update the clocks per automaton 
 Update the automaton for all clocks 
 Add current automaton to the list of automata for this clock 
 end for each automaton 
 Now compute the local clocks 
 Retrieve the automata in which this clock appears 
 Only one element: clock is local 
 				print_message Verbose_high ("Automaton " ^ (string_of_int automaton_index) ^ " has local clock " ^ (string_of_int clock_index)); 
 Add the clock to the automaton 
 Otherwise, clock is not local 
------------------------------------------------------------
 Find the useless clocks in automata locations 
------------------------------------------------------------
* NOTE: this function is not related to model conversion, and could (should?) be defined elsewhere 
 Retrieve the model 
 Create the data structure 
 For each automaton 
 Get the locations for this automaton 
 Retrieve the local clocks for this automaton 
 Compute the predecessor locations and lists of local clock reset 
 For each location in this automaton: 
 Get the actions for this location 
 For each action available in this location 
 Retrieve the transitions from this location & action 
 For each transition starting from this location 
* TODO: What happens here with the clock updates ?? 
 Get the clocks updated or reset 
 Compute the local clocks updated or reset 
 Update the predecessors 
 end for each transition 
 end for each action 
 end for each location 
 Print some information 
 Iterate on locations 
 end for each location 
 For each local clock for this automaton 
 Create a list of marked locations (i.e., where the clock is useful) 
 All locations with an invariant involving this clock 
 Retrieve the invariant 
 Check if the clock is present in the invariant 
 Print some information 
 Return true or false 
 All predecessor locations of transitions with a guard involving this clock 
 For each location 
 Get the actions for this location 
 For each action available in this location 
 Retrieve the transitions from this location & action 
 Check if there exists a guard in an outgoing transition where the clock is constrained 
 Check if the clock is present in the guard 
 Print some information 
 Return true or false 
 Keep the location if there exists a guard 
 Create a waiting list 
 Print some information 
 Start the algorithm 
 Pick a location from the waiting list 
 Print some information 
 For each transition leading to this location 
 Print some information 
 If the clock is not reset by the transition 
 Print some information 
 If the source location does not belong to the marked list 
 Add it to the marked list 
 Add it to the waiting list (if not present) 
 end if not in marked list 
 end if clock not reset 
 end for each transition 
 End the algorithm 
 Return the list of locations where the clock can be removed 
 Print some information 
 Update the data structure 
 end for each local clock 
 end for each automaton 
 Return a functional structure 
------------------------------------------------------------
 Function for preparing data structures for dynamic clock elimination 
------------------------------------------------------------
 NOTE: This function is only called if the dynamic clock elimination option is activated 
 Create counters 
 Start counter 
 Retrieve the model 
 Compute the local clocks per automaton 
 Debug print: local clocks per automaton 
 For each automaton 
 Get the actions 
 Print it 
 Compute and update useless clocks 
 Stop counter 
 The end 
------------------------------------------------------------
 Eliminating useless clocks in a linear constraint 
------------------------------------------------------------
 Get counter 
 Start counter 
 Increment counter 
 Retrieve the model 
 Compute the useless clocks 
 Retrieve target location for this automaton 
 Get the clocks and append to previously computed clocks (rev_append because the order doesn't matter) 
 Print some information 
 Print some information 
 Stop counter 
 The end 
* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * 
  * 
  *                        IMITATOR 
  * 
  * Université Paris 13 , LIPN , CNRS , France 
  * 
  * Module description : Dynamic elimination of clocks not used in the future [ Andre13 , FSFMA ] 
  * 
  * File contributors :   ,   
  * Created            : 2015/11/27 
  * 
  * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
 *
 *                       IMITATOR
 *
 * Université Paris 13, LIPN, CNRS, France
 *
 * Module description: Dynamic elimination of clocks not used in the future [Andre13, FSFMA]
 *
 * File contributors : Étienne André, Jaime Arias
 * Created           : 2015/11/27
 *
 ************************************************************)


open OCamlUtilities
open ImitatorUtilities
open Exceptions
open Statistics
open AbstractModel







let counter_preparation = ref None
let counter_elimination = ref None



*  to the function defined in ModelConverter
let get_clocks_in_updates = ModelConverter.get_clocks_in_updates

let get_clocks_in_guard clocks : guard -> Automaton.clock_index list = function
  | True_guard -> []
  | False_guard -> []
  | Discrete_guard _ -> []
  | Continuous_guard continuous_guard -> LinearConstraint.pxd_find_variables clocks continuous_guard
  | Discrete_continuous_guard discrete_continuous_guard -> LinearConstraint.pxd_find_variables clocks discrete_continuous_guard.continuous_guard

let is_constrained_in_guard clock_index : guard -> bool = function
  | True_guard -> false
  | False_guard -> false
  | Discrete_guard _ -> false
  | Continuous_guard continuous_guard -> LinearConstraint.pxd_is_constrained continuous_guard clock_index
  | Discrete_continuous_guard discrete_continuous_guard -> LinearConstraint.pxd_is_constrained discrete_continuous_guard.continuous_guard clock_index


let find_local_clocks () =
  let model = Input.get_model() in

  let clock_offset = model.nb_parameters in

  let clocks_per_automaton = Array.make model.nb_automata [] in

  let local_clocks_per_automaton = Array.make model.nb_automata [] in

  let automata_per_clock = Array.make model.nb_clocks [] in

  for automaton_index = 0 to model.nb_automata - 1 do
    let locations = model.locations_per_automaton automaton_index in

    let clocks_for_locations = List.fold_left (fun list_of_clocks_for_previous_locations location_index ->
        let invariant = model.invariants automaton_index location_index in
        let clocks_in_invariant = get_clocks_in_guard model.clocks invariant in
        let clocks_in_stopwatches = model.stopwatches automaton_index location_index in

        let actions_for_this_location = model.actions_per_location automaton_index location_index in
        let clocks_for_actions = List.fold_left (fun list_of_clocks_for_previous_actions action_index ->
            let transitions_for_this_action = List.map model.transitions_description (model.transitions automaton_index location_index action_index) in

            let clocks_for_transitions = List.fold_left (fun list_of_clocks_for_previous_transitions transition ->
                let guard , updates = transition.guard, transition.updates in

                let clocks_in_guards = get_clocks_in_guard model.clocks guard in
                let clocks_in_updates = get_clocks_in_updates updates in

  Add these 2 new lists to the current list
                List.rev_append (List.rev_append clocks_in_guards clocks_in_updates) list_of_clocks_for_previous_transitions
              ) [] transitions_for_this_action in

            List.rev_append clocks_for_transitions list_of_clocks_for_previous_actions
          ) [] actions_for_this_location in

        List.rev_append (List.rev_append (List.rev_append clocks_in_invariant clocks_in_stopwatches) clocks_for_actions) list_of_clocks_for_previous_locations
      ) [] locations in

    let clocks_for_this_automaton = list_only_once clocks_for_locations in
    clocks_per_automaton.(automaton_index) <- clocks_for_this_automaton;
    List.iter (fun clock ->
        automata_per_clock.(clock - clock_offset) <- (automaton_index :: automata_per_clock.(clock - clock_offset));
      ) clocks_for_this_automaton;

  for clock_index = clock_offset to clock_offset + model.nb_clocks - 1 do
    let automata_for_this_clock = automata_per_clock.(clock_index - clock_offset) in
  If size is 1 , the clock is local
    match automata_for_this_clock with
    | [automaton_index] ->
      local_clocks_per_automaton.(automaton_index) <- (clock_index) :: local_clocks_per_automaton.(automaton_index);
    | _ -> ()
  done;

  local_clocks_per_automaton


let find_useless_clocks_in_automata local_clocks_per_automaton =

  let model = Input.get_model() in

  let useless_clocks_per_location = Array.make model.nb_automata (Array.make 0 []) in

  for automaton_index = 0 to model.nb_automata - 1 do


    let locations_for_this_automaton = model.locations_per_automaton automaton_index in
    let nb_locations = List.length locations_for_this_automaton in

  Initialize the data structure for this automaton
    useless_clocks_per_location.(automaton_index) <- Array.make nb_locations [];

    let local_clocks = local_clocks_per_automaton.(automaton_index) in

    let predecessors = Array.make nb_locations [] in
    List.iter (fun location_index ->
        let actions_for_this_location = model.actions_per_location automaton_index location_index in

        List.iter (fun action_index ->
            let transitions = List.map model.transitions_description (model.transitions automaton_index location_index action_index) in

            List.iter (fun transition ->

                let reset_clocks = ModelConverter.get_clocks_in_updates transition.updates in

                let reset_local_clocks = list_inter reset_clocks local_clocks in
                predecessors.(transition.target) <- (location_index, reset_local_clocks) :: predecessors.(transition.target);

    if verbose_mode_greater Verbose_total then(
      print_message Verbose_total ("Computed predecessor locations and clock resets for automaton '" ^ (model.automata_names automaton_index) ^ "'");
      List.iter (fun location_index ->
          print_message Verbose_total ("  Location '" ^ (model.location_names automaton_index location_index) ^ "' has predecessors:");
          let predecessors_string = string_of_list_of_string_with_sep ", " (List.map (
              fun (source_index, reset_local_clocks) ->
                (model.location_names automaton_index source_index) ^ "[resets: " ^ (string_of_list_of_string_with_sep ", " (List.map model.variable_names reset_local_clocks)) ^ "]"
            ) predecessors.(location_index)) in
          print_message Verbose_total ("    " ^ predecessors_string);
    );

    List.iter(fun clock_index ->
        let marked = ref (list_union
                            (List.filter (fun location_index ->
                                 let invariant = model.invariants automaton_index location_index in
                                 let constrained = is_constrained_in_guard clock_index invariant in
                                 print_message Verbose_total ("Clock '" ^ (model.variable_names clock_index) ^ "' is " ^ (if constrained then "" else "NOT ") ^ "constrained in invariant of location '" ^ (model.location_names automaton_index location_index) ^ "'");
                                 constrained
                               ) locations_for_this_automaton
                            )
                            (
                              List.fold_left (fun current_list_of_locations location_index ->
                                  let actions_for_this_location = model.actions_per_location automaton_index location_index in
                                  List.fold_left (fun current_list_of_locations action_index ->
                                      let transitions = List.map model.transitions_description (model.transitions automaton_index location_index action_index) in
                                      let exists_guard = List.exists (fun transition ->
                                          let constrained = is_constrained_in_guard clock_index transition.guard in
                                          if constrained then (
                                            print_message Verbose_high ("Found a transition where clock '" ^ (model.variable_names clock_index) ^ "' is constrained in guard from location '" ^ (model.location_names automaton_index location_index) ^ "', through '" ^ (model.action_names action_index) ^ "'");
                                          ) else (
                                            print_message Verbose_total ("Clock '" ^ (model.variable_names clock_index) ^ "' is not constrained in guard from location '" ^ (model.location_names automaton_index location_index) ^ "' through '" ^ (model.action_names action_index) ^ "'");
                                          );
                                          constrained
                                        ) transitions in
                                      if exists_guard then location_index :: current_list_of_locations
                                      else current_list_of_locations
                                    ) current_list_of_locations actions_for_this_location
                                ) [] locations_for_this_automaton
                            )
                         ) in

        let waiting = ref !marked in

        if verbose_mode_greater Verbose_medium then(
          print_message Verbose_medium ("Starting the dynamic clock elimination algorithm for local clock '" ^ (model.variable_names clock_index) ^ "' in automaton '" ^ (model.automata_names automaton_index) ^ "', with initial marked states:");
          print_message Verbose_medium (	"  " ^ (string_of_list_of_string_with_sep ", " (List.map (model.location_names automaton_index) !marked)));
        );

        while !waiting <> [] do
          match !waiting with
          | location_index :: rest ->
            print_message Verbose_medium ("Pick up location '" ^ (model.location_names automaton_index location_index) ^ "'");
  Remove the first element
            waiting := rest;
            List.iter (fun (source_index, reset_local_clocks) ->
                print_message Verbose_high ("Considering predecessor transition from '" ^ (model.location_names automaton_index source_index) ^ "'");
                if not (List.mem clock_index reset_local_clocks) then(
                  print_message Verbose_high ("Clock not reset by a transition.");
                  if not (List.mem source_index !marked) then(
                    marked := source_index :: !marked;
                    print_message Verbose_high ("Location marked.");
                    if not (List.mem source_index !waiting) then
                      print_message Verbose_high ("Location added to waiting list.");
                    waiting := source_index :: !waiting;

          | _ -> raise (InternalError "Impossible situation: list should not be empty.");

        done;

        let useless_locations = list_diff locations_for_this_automaton !marked in

        if verbose_mode_greater Verbose_low then(
          print_message Verbose_low ("List of useless locations for local clock '" ^ (model.variable_names clock_index) ^ "' in automaton '" ^ (model.automata_names automaton_index) ^ "'");
          print_message Verbose_low ("  " ^ (string_of_list_of_string_with_sep ", " (List.map (model.location_names automaton_index) useless_locations)));
        );

        List.iter (fun location_index ->
            (useless_clocks_per_location.(automaton_index)).(location_index) <- clock_index :: (useless_clocks_per_location.(automaton_index)).(location_index);
          ) useless_locations;



  (fun automaton_index location_index ->
     (useless_clocks_per_location.(automaton_index)).(location_index)
  )



let prepare_clocks_elimination () =
  let counter_preparation_ref = create_time_counter_and_register "dynamic clock elimination (preparation)" Algorithm_counter Verbose_standard in
  counter_preparation := Some counter_preparation_ref;
  counter_elimination := Some (create_hybrid_counter_and_register "dynamic clock elimination" Algorithm_counter Verbose_standard);

  counter_preparation_ref#start;

  let model = Input.get_model() in

  print_message Verbose_low ("*** Building local clocks per automaton…");
  let local_clocks_per_automaton = find_local_clocks () in

  if verbose_mode_greater Verbose_total then(
    print_message Verbose_total ("\n*** Local clocks per automaton:");
    List.iter (fun automaton_index ->
        let clocks = local_clocks_per_automaton.(automaton_index) in
        let clocks_string = string_of_list_of_string_with_sep ", " (List.map model.variable_names clocks) in
        print_message Verbose_total ("  " ^ (model.automata_names automaton_index) ^ " : " ^ clocks_string)
      ) model.automata;
  );


  print_message Verbose_low ("*** Building useless clocks per location per automaton…");
  useless_clocks := Some (find_useless_clocks_in_automata local_clocks_per_automaton);

  counter_preparation_ref#stop;

  ()


let dynamic_clock_elimination target_location current_constraint =
  let counter_elimination = match !counter_elimination with
    | Some counter_elimination -> counter_elimination
    | None -> raise (InternalError("Counter counter_elimination not yet initialized in ClockElimination.dynamic_clock_elimination"))
  in

  counter_elimination#start;
  counter_elimination#increment;

  let model = Input.get_model() in

  First check that initialization was performed
  let compute_clocks_to_eliminate =
    match !useless_clocks with
    | None -> raise (InternalError ("Trying to perform dynamic clock elimination before initializing the clocks to eliminate."))
    | Some f -> f
  in

  let clocks_to_remove = List.fold_left (fun current_list_of_clocks automaton_index ->
      let location_index = Location.get_location target_location automaton_index in
      List.rev_append current_list_of_clocks (compute_clocks_to_eliminate automaton_index location_index)
    ) [] model.automata in
  if verbose_mode_greater Verbose_low then(
    if clocks_to_remove = [] then print_message Verbose_low ("No clock will be dynamically removed.")
    else print_message Verbose_low ("The following clock" ^ (s_of_int (List.length clocks_to_remove)) ^ " will be dynamically removed: {" ^ (string_of_list_of_string_with_sep ", " (List.map model.variable_names clocks_to_remove)) ^ "}");
  );

  print_message Verbose_high ("\nRemoving useless clocks ");
  LinearConstraint.px_hide_assign clocks_to_remove current_constraint;
  if verbose_mode_greater Verbose_total then(
    print_message Verbose_total (LinearConstraint.string_of_px_linear_constraint model.variable_names current_constraint);
  );

  counter_elimination#stop;

  ()
