open Common
open Expression
open Printf
open Varcontext

module GenericUAutomaton (Files : sig val tafile : string val qfile : string val enable_cora : bool end) : Ita.TA =
struct

  include Querybuilder

  (** Expression factory functions, to be registered as callbacks from C *)
  let cb_expression_constant i = Constant i

  let cb_expression_array varcont constcont clockcont tmp name sons =
    if ScopeVarContext.arraymem varcont (tmp, name) then
      let arrayid = ScopeVarContext.index_of_array varcont (tmp, name) in
      Array(arrayid, sons)
    else if (ScopeVarContext.arraymem varcont (None, name)) then
      let arrayid = ScopeVarContext.index_of_array varcont (None, name) in
      Array(arrayid, sons)
    else if (ScopeVarContext.arraymem constcont (tmp, name)) then
      let arrayid = ScopeVarContext.index_of_array constcont (tmp, name) in
      ConstArray(arrayid, sons)
    else if (ScopeVarContext.arraymem constcont (None, name)) then
      let arrayid = ScopeVarContext.index_of_array constcont (None, name) in
      ConstArray(arrayid, sons)
    else if (ScopeVarContext.arraymem clockcont (tmp, name)) then
      let arrayid = ScopeVarContext.index_of_array clockcont (tmp, name) in
      ClockArray(arrayid, sons)
    else if (ScopeVarContext.arraymem clockcont (None, name)) then
      let arrayid = ScopeVarContext.index_of_array clockcont (None, name) in
      ClockArray(arrayid, sons)
    else
      failwith (sprintf "Undefined array <%s>" name)

  let cb_expression_variable constcont const_values varcont tmp name =
    (* is it a local constant? *)
    if (ScopeVarContext.mem constcont (tmp, name)) then
      let varid = ScopeVarContext.index_of_var constcont (tmp, name) in
      Constant(Hashtbl.find const_values varid)
    (* is it a global constant? *)
    else if (ScopeVarContext.mem constcont (None, name)) then
      let varid = ScopeVarContext.index_of_var constcont (None, name) in
      Constant(Hashtbl.find const_values varid)
    (* is it a local variable? *)
    else if (ScopeVarContext.mem varcont (tmp, name)) then
      let varid = ScopeVarContext.index_of_var varcont (tmp, name) in
      Variable(varid)
    (* is it a global variable? *)
    else if (ScopeVarContext.mem varcont (None, name)) then
      let varid = ScopeVarContext.index_of_var varcont (None, name) in
      Variable(varid)
    else
      failwith (sprintf "Undefined variable <%s>" name)

  let cb_expression_clock clockcont tmp name =
    (* is it a local clock? *)
    if (ScopeVarContext.mem clockcont (tmp, name) ) then
      let varid = ScopeVarContext.index_of_var clockcont (tmp,name) in
      Clock(varid)
    (* is it a global clock? *)
    else if (ScopeVarContext.mem clockcont (None, name) ) then
      let varid = ScopeVarContext.index_of_var clockcont (None,name) in
      Clock(varid)
    else
      failwith (sprintf "Undefined clock <%s>" name)

  let cb_expression_sum a b = Sum (a,b)
  let cb_expression_product a b = Product (a,b)
  let cb_expression_substraction a b = Substraction (a,b)
  let cb_expression_division a b = Division (a,b)

  (** A guard is a conjunction of atomic guards *)
  type guard = atomic_guard list

  (** clocks and variables updates *)
  type lvalue =
      ClockRef of clock_t
    | ClockArrayRef of int * expression list
    | VarRef of int
    | ArrayRef of int * expression list
  type update = lvalue * expression

  type chanref =
      ChanId of int
    | ChanArray of int * expression list

  (* Channels are assumed to be global, so are handled by VarContext *)
  let cb_channel_simple chancont chanName =
    let aid = VarContext.index_of_var chancont chanName in
    ChanId(aid)

  let cb_channel_array chancont arrayName indices =
    let aid = VarContext.index_of_array chancont arrayName in
    ChanArray(aid, indices)

  type simplechan =
      SendChan of chanref
    | RecvChan of chanref


  type edge = {
    edgeSource : int;
    edgeGuard : guard;
    edgeDiscGuard : guard;
    edgeUpdates : update list;
    edgeTarget : int;
    edgeSync : simplechan option;
    edgeProc : int; (* proc id *)
    edgeControllable : bool;
    edgeCost : Costs.edge_cost; (* the cost of this edge [default is 0] *)
  }
  and location = {
    locId : int;
      (* the ID of the location *)
    mutable locName : string;
      (* the name of the location, for printing purposes *)
    locCommitted : bool;
    locUrgent : bool;
    locInvar : guard;
    locEdges : edge list;
    locProc : int; (* proc id *)
    locRate : Costs.loc_rate;
      (* the cost rate of time elapsing in this location [default is None] *)
      (* the cost rate of an array of location is the sum of their cost rates *)
    mutable compExpr : ((expression list) * (expression list)) array;
      (* compExpr.(cl) contains the set of expressions against which cl is
       * compared in any guard or invariant from the current location until
       * it is reset. First component for L bounds, second one for U bounds.
       * Local computation of LU bounds, useful for the global computation.
       *)
  }
  and process = {
    procName : string;
    procId : int;
    procLocations : location array;
    procInitLoc : int;
  }
  type state = {
    stateLocs : location array;
    stateVars : int array;
  }

  type transition = InternalTrans of state * edge
                  | SyncTrans of state * edge * edge


  let hash_state s =
    let tmp = Array.fold_right
      (fun x r -> r + x.locId + 0x9e3779b9 + (r lsl 6) + (r lsr 2))
      s.stateLocs 0
    in Array.fold_right
      (fun x r -> r + x + 0x9e3779b9 + (r lsl 6) + (r lsr 2))
      s.stateVars tmp

  let equal_state s t =
    let rec aux_loc a b n =
      if (n < 0) then true else
      if (a.(n).locId = b.(n).locId) then
        if (n > 0) then
          aux_loc a b (n-1)
        else true
      else false
    in
    let rec aux_var a b n =
      if (n < 0) then true else
      if (a.(n) = b.(n)) then
        if (n > 0) then
          aux_var a b (n-1)
        else true
      else false
    in
    (aux_loc s.stateLocs t.stateLocs (Array.length s.stateLocs - 1))
    &&
    (aux_var s.stateVars t.stateVars (Array.length s.stateVars - 1))

  module DS = struct
    type t = state
    let equal = equal_state
    let hash = hash_state
  end

  module DSHashtbl = Hashtbl.Make(DS)

  (* s1 < s2 iff s1.prio > s2.prio *)
  let priority_compare s1 s2 =
    - compare s1.stateVars.(0) s2.stateVars.(0)

  type ta = {
    procs : process array; (* forall i: procs.(i).procId = i *)
    clocks : VarContext.t;
    vars : VarContext.t;
    constants : VarContext.t;
    constvalues : int array;
    channels : VarContext.t;
    init : state;
    query : query;
    lubounds_tbl : (int array * int array) DSHashtbl.t;
    global_mbounds : int array;
  }

  (********** PRINTING AUXILIARY FUNCTIONS **********)
  let rec string_of_exp ta e =
    let string_of_exp = string_of_exp ta in
    (function
      | Constant c -> sprintf "%d" c
      | Array(aid, indices) ->
          let arrayName = VarContext.array_of_index ta.vars aid in
          List.fold_left (fun s x -> s ^ "[" ^ (string_of_exp x) ^ "]") arrayName indices
      | ConstArray(aid, indices) ->
          let arrayName = VarContext.array_of_index ta.constants aid in
          List.fold_left (fun s x -> s ^ "[" ^ (string_of_exp x) ^ "]") arrayName indices
      | ClockArray(aid,indices) ->
          let arrayName = VarContext.array_of_index ta.clocks aid in
          List.fold_left (fun s x -> s ^ "[" ^ (string_of_exp x) ^ "]") arrayName indices
      | Variable(id) -> VarContext.var_of_index ta.vars id
      | ConstVariable(id) -> VarContext.var_of_index ta.constants id
      | Clock(id) ->  VarContext.var_of_index ta.clocks id
      | Product(e1,e2) ->
        sprintf "%s * %s" (string_of_exp e1)
          (string_of_exp e2)
      | Sum(e1,e2) ->
        sprintf "(%s + %s)" (string_of_exp e1)
          (string_of_exp e2)
      | Division(e1,e2) ->
        sprintf "%s / %s" (string_of_exp e1)
          (string_of_exp e2)
      | Substraction(e1,e2) ->
        sprintf "(%s - %s)" (string_of_exp e1)
          (string_of_exp e2)
    ) e


  let string_of_atomic_guard ta =
    let string_of_exp = string_of_exp ta in
    function
    |  GuardLeq(v,exp) ->
      sprintf "%s <= %s" (string_of_exp v)(string_of_exp exp)
    | GuardLess(v,exp) ->
      sprintf "%s < %s" (string_of_exp v)(string_of_exp exp)
    | GuardGeq(v,exp)->
      sprintf "%s >= %s" (string_of_exp v)(string_of_exp exp)
    | GuardGreater(v,exp)->
      sprintf "%s > %s" (string_of_exp v) (string_of_exp exp)
    | GuardEqual(v,exp)->
      sprintf "%s == %s" (string_of_exp v) (string_of_exp exp)
    | GuardNeq(v,exp)->
      sprintf "%s != %s" (string_of_exp v) (string_of_exp exp)


  let xml_string_of_atomic_guard ta =
    let string_of_exp = string_of_exp ta in
    function
    |  GuardLeq(v,exp) ->
      sprintf "%s &lt;= %s" (string_of_exp v)(string_of_exp exp)
    | GuardLess(v,exp) ->
      sprintf "%s &lt; %s" (string_of_exp v)(string_of_exp exp)
    | GuardGeq(v,exp)->
      sprintf "%s &gt;= %s" (string_of_exp v)(string_of_exp exp)
    | GuardGreater(v,exp)->
      sprintf "%s &gt; %s" (string_of_exp v) (string_of_exp exp)
    | GuardEqual(v,exp)->
      sprintf "%s == %s" (string_of_exp v) (string_of_exp exp)
    | GuardNeq(v,exp)->
      sprintf "%s != %s" (string_of_exp v) (string_of_exp exp)


  let rec string_of_guard ta =
    function
    | [] -> ""
    | [x] -> string_of_atomic_guard ta x
    | x :: y :: l ->
      ((string_of_atomic_guard ta x) ^ " && ")
      ^ (string_of_guard ta (y::l))


  let rec xml_string_of_guard ta =
    function
    | [] -> ""
    | [x] -> xml_string_of_atomic_guard ta x
    | x :: y :: l ->
      ((xml_string_of_atomic_guard ta x) ^ " &amp;&amp; ")
      ^ (xml_string_of_guard ta (y::l))


  let string_of_updates ta ups =
    let ups_str =
      List.map (fun (var,exp) ->
        let lhsname = match var with
          | ClockRef(c) -> VarContext.var_of_index ta.clocks c
          | VarRef(v) -> VarContext.var_of_index ta.vars v
        in
        sprintf "%s = %s" lhsname (string_of_exp ta exp)) ups in
    String.concat ", " ups_str


  let string_of_state ta state =
    let out = Buffer.create 50 in
    Array.iter (fun loc -> Buffer.add_string out loc.locName;
                 Buffer.add_string out " ") state.stateLocs;
    if (Array.length state.stateVars > 0 ) then (
      Buffer.add_string out "\n";
      Array.iteri (fun i v ->
          let name = VarContext.var_of_index ta.vars i in
          Buffer.add_string out (sprintf "%s = %d, " name v)) state.stateVars;
    );
    (*    Buffer.add_string out "\n";*)
    Buffer.contents out


  let string_of_edge ta edge =
    let proc = ta.procs.(edge.edgeProc) in
    let print_chanref = function
      | ChanId(c) -> string_of_int c
      | ChanArray(aid,indices) ->
          List.fold_left (fun s x -> sprintf "%s[%s]" s (string_of_exp ta x)) (string_of_int aid) indices
    in
    let sync = match edge.edgeSync with
      |None -> ""
      |Some(SendChan(c)) -> (print_chanref c)^"!"
      |Some(RecvChan(c)) -> (print_chanref c)^"?"
    in
    let discguardstr = string_of_guard ta edge.edgeDiscGuard in
    let guardstr = string_of_guard ta edge.edgeGuard in
    sprintf "%s%s -> %s \tDiscGuard: %s \tGuard: %s \tUpdates:%s \tSync:%s"
      (if (edge.edgeControllable) then "" else "[E]")
      (proc.procLocations.(edge.edgeSource).locName)
      (proc.procLocations.(edge.edgeTarget).locName)
      discguardstr
      guardstr
      (string_of_updates ta edge.edgeUpdates)
      sync


  let string_of_location ta loc =
    let out = Buffer.create 128 in
    let utter = Buffer.add_string out in
    utter (sprintf "Location %d: %s "loc.locId loc.locName);
    if (loc.locCommitted) then
      utter "committed ";
    utter (string_of_guard ta loc.locInvar);
    utter "\n";
    utter (sprintf "Has %d edges:\n" (List.length loc.locEdges));
    let edgestrlist = (List.map (string_of_edge ta) loc.locEdges) in
    utter (String.concat "\n" edgestrlist);
    utter "\n";
    Buffer.contents out


  let string_of_process ta proc =
    let out = Buffer.create 1000 in
    let utter = Buffer.add_string out in
    utter (sprintf "Process(%d): %s\n"  proc.procId proc.procName);
    Array.iter (fun loc -> utter (string_of_location ta loc)) proc.procLocations;
    utter (sprintf "Initial location id: %d\n" proc.procInitLoc);
    Buffer.contents out


  let string_of_transition ta tr =
    let buf = Buffer.create 128 in
    let out = Buffer.add_string buf in
    let proc_name e = ta.procs.(e.edgeProc).procName in
    match tr with
      InternalTrans(state,e) ->
      out (sprintf "From global state: %s\n" (string_of_state ta state));
      out (string_of_edge ta e);
      Buffer.contents buf
    | SyncTrans(state,e1,e2) ->
      out (sprintf "Synchronized Transition btw Processes: %s - %s\n Source: %s\n" (proc_name e1) (proc_name e2)
             (string_of_state ta state));
      out "Sync:\n";
      out (string_of_edge ta e1);
      out "\n";
      out (string_of_edge ta e2);
      Buffer.contents buf


  (********** OTHER AUXILIARY FUNCTIONS **********)

  (* evaluate expression *)
  (* output is either Constant(_) or Clock(_)
   *)
  let rec eval_exp ta vars = function
    | Constant c -> Constant c
    | ConstVariable id ->
        assert(id >= 0 && id < Array.length ta.constvalues);
        Constant ta.constvalues.(id)
    | Variable id ->
        assert(id >= 0 && id < Array.length vars);
        Constant vars.(id)
    | Clock c -> Clock c
    | ClockArray(arrayId, l) ->
        let indices = List.map (fun x -> eval_disc_exp ta vars x) l in
        let cellindex = VarContext.index_of_cell ta.clocks arrayId indices in
        Clock cellindex
    | Array(arrayId, l) ->
        let indices = List.map (fun x -> eval_disc_exp ta vars x) l in
        let cellindex = VarContext.index_of_cell ta.vars arrayId indices in
        eval_exp ta vars (Variable cellindex)
    | ConstArray(arrayId, l) ->
        let indices = List.map (fun x -> eval_disc_exp ta vars x) l in
        let cellIndex = VarContext.index_of_cell ta.constants arrayId indices in
        eval_exp ta vars (ConstVariable cellIndex)
    | Product(e1,e2) -> Constant ((eval_disc_exp ta vars e1) * (eval_disc_exp ta vars e2))
    | Sum(e1,e2) -> Constant ((eval_disc_exp ta vars e1) + (eval_disc_exp ta vars e2))
    | Division(e1,e2) -> Constant ((eval_disc_exp ta vars e1) / (eval_disc_exp ta vars e2))
    | Substraction(e1,e2) -> Constant ((eval_disc_exp ta vars e1) - (eval_disc_exp ta vars e2))
  (* same as above, but fails if it encounters a clock *)
  and eval_disc_exp ta vars exp =
    match (eval_exp ta vars exp) with
      | Constant c -> c
      | _ -> failwith ("Unevaluable discrete expression" ^ (string_of_exp ta exp))

  let source_location_of_edge ta edge =
    ta.procs.(edge.edgeProc).procLocations.(edge.edgeSource)

  (* evaluate the discrete part of a guard
   * the result contains only clocks and constants (no clock array, no expression)
   *)
  let eval_ag ta state ag =
    let eval = eval_exp ta state.stateVars in
    match ag with
      | GuardLeq(a,b) -> GuardLeq(eval a, eval b)
      | GuardLess(a,b) -> GuardLess(eval a, eval b)
      | GuardEqual(a,b) -> GuardEqual(eval a, eval b)
      | GuardNeq(a,b) -> GuardNeq(eval a, eval b)
      | GuardGeq(a,b) -> GuardGeq(eval a, eval b)
      | GuardGreater(a,b) -> GuardGreater(eval a, eval b)

  (* completely evaluate a discrete guard to true or false.
   * fails if it encounters a clock *)
  let eval_disc_guard ta state =
    List.for_all (fun x ->
      match eval_ag ta state x with
        | GuardLeq(Constant(a),Constant(b)) -> a <= b
        | GuardLess(Constant(a),Constant(b)) -> a < b
        | GuardEqual(Constant(a),Constant(b)) -> a = b
        | GuardNeq(Constant(a),Constant(b)) -> a <> b
        | GuardGeq(Constant(a),Constant(b)) -> a >= b
        | GuardGreater(Constant(a),Constant(b)) -> a > b
        | _ -> failwith "Unevaluable discrete guard")

  let is_committed state =
    let rec aux ar n =
      if (ar.(n).locCommitted) then true
      else if (n > 0) then
        aux ar (n-1)
      else false
    in aux state.stateLocs (Array.length state.stateLocs - 1)


  let _copy_state state =
    { stateVars = Array.copy state.stateVars;
      stateLocs = Array.copy state.stateLocs}

  (** Apply discrete update of edge to state, result written in state'
   *  Along the way, instantiate clock updates and return them *)
  let _apply_edge ta state edge state' =
    let result = ref [] in
    state'.stateLocs.(edge.edgeProc) <- ta.procs.(edge.edgeProc).procLocations.(edge.edgeTarget);
    List.iter (fun (lhs,e) ->
      match lhs with
        | VarRef(id) -> state'.stateVars.(id) <- eval_disc_exp ta state'.stateVars e
        | ClockRef(id) -> result := !result @ [(id, eval_disc_exp ta state'.stateVars e)]
        | ArrayRef(id,ilist) ->
            let indices = List.map (fun x -> eval_disc_exp ta state'.stateVars x) ilist in
            let cellId = VarContext.index_of_cell ta.vars id indices in
            state'.stateVars.(cellId) <- eval_disc_exp ta state'.stateVars e
        | ClockArrayRef(id,ilist) ->
            let indices = List.map (fun x -> eval_disc_exp ta state'.stateVars x) ilist in
            let cellId = VarContext.index_of_cell ta.clocks id indices in
            result := !result @ [(cellId, eval_disc_exp ta state'.stateVars e)])
    edge.edgeUpdates;
    !result


  (********** TIMED_AUTOMATON interface **********)
  let clocks ta = ta.clocks

  let nb_clocks ta = (VarContext.size (clocks ta))-1

  let string_of_clock ta cl =
    assert(cl > 0 && cl <= VarContext.size (clocks ta));
    VarContext.var_of_index (clocks ta) cl

  let initial_state ta = ta.init

  let rate_of_state ta state =
    Costs.get_rate (Array.map (fun loc -> loc.locRate) state.stateLocs) (eval_disc_exp ta state.stateVars)

  let eval_chan ta state = function
    | ChanId(c) -> ChanId(c)
    | ChanArray(arrayId, l) ->
      let indices = List.map (fun x -> eval_disc_exp ta state.stateVars x) l in
      let cellindex = VarContext.index_of_cell ta.channels arrayId indices in
      ChanId (cellindex)

  let _transitions_from ta state =
    let committed = is_committed state in
    let transq = Queue.create () in
    (* Queue of synchronizing edges *)
    let rchan = Queue.create () in
    let schan = Queue.create () in
    let nproc = Array.length ta.procs in
    for i = 0 to nproc - 1 do
      let loc = state.stateLocs.(i) in
      let add_single = not committed || loc.locCommitted in
      List.iter
        (fun edge ->
          if (eval_disc_guard ta state edge.edgeDiscGuard) then
            (match edge.edgeSync with
              | Some (SendChan(c)) ->
                  Queue.add (eval_chan ta state c, edge) schan
              | Some (RecvChan(c)) ->
                  Queue.add (eval_chan ta state c, edge) rchan
              | None ->
                  if (add_single) then
                    Queue.add (InternalTrans (state, edge)) transq
            )
        ) loc.locEdges
    done;
    Queue.iter
      (fun (rname, redge) ->
        Queue.iter
          (fun (sname, sedge) ->
            (* Sync if same channels are used by different processes *)
            if (rname = sname && redge.edgeProc <> sedge.edgeProc) then (
              (* and if state not committed or one of the participating states is *)
              let sloc = source_location_of_edge ta sedge in
              let rloc = source_location_of_edge ta redge in
              if (not committed || sloc.locCommitted || rloc.locCommitted) then
                Queue.add (SyncTrans (state, redge, sedge)) transq
            )
          ) schan
      ) rchan;
    Queue.fold (fun l tr -> tr :: l) [] transq

  let guard_of_transition ta = function
    |InternalTrans(s,e) -> List.map (eval_ag ta s) e.edgeGuard
    |SyncTrans(s,e1,e2) -> List.map (eval_ag ta s) (e1.edgeGuard @ e2.edgeGuard)

  let transition_fields ta = function
    | InternalTrans(state, e) ->
        let state' = _copy_state state in
        let resets = _apply_edge ta state e state' in
        (state,
         List.map (eval_ag ta state) e.edgeGuard,
         resets,
         state')
    | SyncTrans(state, e1, e2) ->
        let state' = _copy_state state in
        let resets1 = _apply_edge ta state e1 state' in
        let resets2 = _apply_edge ta state e2 state' in
        (state, List.map (eval_ag ta state) (e1.edgeGuard @ e2.edgeGuard), resets1 @ resets2, state')

  let ag_to_pair = function
    | GuardLeq(Clock(cl),Constant(k)) -> Ita.LEQ(cl,k)
    | GuardLess(Clock(cl),Constant(k)) -> Ita.LT(cl,k)
    | GuardGeq(Clock(cl),Constant(k)) -> Ita.GEQ(cl,k)
    | GuardGreater(Clock(cl),Constant(k)) -> Ita.GT(cl,k)
    | GuardEqual(Clock(cl),Constant(k)) -> Ita.EQ(cl,k)
    | _ -> failwith "invalid guard form"

  let transitions_from ta state =
    List.map (fun tr ->
      let (s,g,u,t) = transition_fields ta tr in
      (s,List.map ag_to_pair g,u,t)) (_transitions_from ta state)

  let invariant ta state =
    Array.fold_left (fun acc loc -> (List.map (fun x -> ag_to_pair (eval_ag ta state x)) loc.locInvar) @ acc) [] state.stateLocs

  let transition_to_string = string_of_transition

  let is_urgent_or_committed ta state =
    let rec aux ar n =
      if (ar.(n).locCommitted || ar.(n).locUrgent) then true
      else if (n > 0) then
        aux ar (n-1)
      else false
    in aux state.stateLocs (Array.length state.stateLocs - 1)

  let is_target ta state =
    let rec eval_query = function
      | EmptyQuery -> true
      | QueryAnd(l,r) -> (eval_query l) && (eval_query r)
      | QueryOr(l,r) -> (eval_query l) || (eval_query r)
      | Location(procId,locId) -> state.stateLocs.(procId).locId = locId
      | Atomic(ag) -> eval_disc_guard ta state [ag]
    in
    eval_query ta.query

  (* TODO *)
  let global_mbounds ta =
    failwith "not implemented"

  (** print functions *)
  let print_discrete_state chan ta state =
    fprintf chan "%s\n" (string_of_state ta state)

  let print_transition chan ta trans =
    fprintf chan "%s\n" (string_of_transition ta trans)

  let print_timed_automaton chan ta =
    fprintf chan "Timed automaton with %d clocks and %d processes\n"
      (VarContext.size ta.clocks) (Array.length ta.procs);
    Array.iter (fun proc -> fprintf chan "%s\n-----\n" (string_of_process ta proc)) ta.procs

  (********** LOADING FUNCTIONS **********)

  (** given a set of expressions, simplify it to retain only its maximal
   * constant and all non-constant *)
  (* TODO check that the input does not contain ConstVariable or constant ConstArray *)
  let simplify_max exprs =
    let new_max = function
      | None -> (function
        | Constant k -> Some k
        | _ -> None)
      | Some m as e -> (function
        | Constant k when k > m -> Some k
        | _ -> e)
    in
    match List.fold_left new_max None exprs with
    | None -> exprs
    | Some k -> List.filter (function
      | Constant l when l < k -> false
      | _ -> true) exprs

  (* given a process, a location l and a clock c, compute the set of expressions
   * against which c is compared from l until it is reset.
   * Formally, the result S is the smallest set of expressions such that:
     * if x is compared to e in the invariant of l, then e \in S
     * for any transition t : l->l'
       * if x is compared to e in the guard of t, then e \in S
       * if x is not reset in t, then comp_expressions p l' c \subset S
   * returns a pair (L,U)
   *)
  let comp_expressions ta p l c =
    ta.procs.(p).procLocations.(l).compExpr.(c)

  (* computes the LU bounds in a given state *)
  (* this should be used from another function that caches the results *)
  (* TODO some clocks already have their constant known, cache them *)
  let _lubounds ta state =
    let n = VarContext.size ta.clocks in
    let lb, ub = Array.make n 0, Array.make n 0 in
    for cl=0 to n-1 do
      let lexpr, uexpr = Array.fold_left
        (fun (lacc, uacc) loc ->
          let ltmp, utmp = loc.compExpr.(cl) in
          (lacc @ ltmp, uacc @ utmp)) ([],[])
        state.stateLocs
      in
      (* instantiate found expressions, and retain only the maximal constant *)
      let lcst, ucst =
        simplify_max (List.map (fun e -> eval_exp ta state.stateVars e) lexpr),
        simplify_max (List.map (fun e -> eval_exp ta state.stateVars e) uexpr)
      in
      begin
        match lcst with
          | (Constant k)::_ -> lb.(cl) <- max lb.(cl) k
          | _ -> (* TODO can it happen? *) ()
      end;
      begin
        match ucst with
          | (Constant k)::_ -> ub.(cl) <- max ub.(cl) k
          | _ -> (* TODO can it happen? *) ()
      end;
    done;
    lb, ub
  
  let lubounds ta state =
    try
      DSHashtbl.find ta.lubounds_tbl state
    with
    | Not_found ->
        let res = _lubounds ta state in
        DSHashtbl.add ta.lubounds_tbl state res;
        res

  (* tells whether a given clock is set by a given update *)
  (* the difficult part is when the lhs of the update is an array cell *)
  let is_reset : clock_t -> update -> bool = fun cl -> function
    | ClockRef c, _ when c = cl -> true
    | ClockArrayRef (a,_), _ ->
        (* TODO true if cl is a cell of the array a, false otherwise *)
        (* TODO further refine: if all indices expressions are constant, we
         * can do an exact equality check *)
        failwith "cannot compute bounds for arrays of clocks"
    | _ -> false

  (* return the set of clock the argument can refer to *)
  let clocks_of ta = function
    | Clock c -> [c]
    | ClockArray(a,_) -> (*TODO*) failwith "cannot compute bounds for arrays of clocks"
    | _ -> []

  (* compute all the local LU bounds *)
  let build_lu ta =
    let nclocks = VarContext.size ta.clocks in
    (* for each process *)
    for p=0 to (Array.length ta.procs)-1 do
      let proc = ta.procs.(p) in
      
      (* initialization: for each location, add the expression of its invariant
       * and of guards of outgoing transitions
       *)
      for l=0 to (Array.length proc.procLocations)-1 do
        let loc = proc.procLocations.(l) in
        loc.compExpr <- Array.make nclocks ([],[]);

        let ag_handle = function
          | GuardLeq(lhs,e)
          | GuardLess(lhs,e) ->
              List.iter
                (fun cl ->
                  let ltmp, utmp = loc.compExpr.(cl) in
                  if not (List.mem e utmp) then
                    loc.compExpr.(cl) <- ltmp, e::utmp
                )
                (clocks_of ta lhs)
          | GuardGeq(lhs,e)
          | GuardGreater(lhs,e) ->
              List.iter
                (fun cl ->
                  let ltmp, utmp = loc.compExpr.(cl) in
                  if not (List.mem e ltmp) then
                    loc.compExpr.(cl) <- e::ltmp, utmp
                )
                (clocks_of ta lhs)
          | GuardEqual(lhs,e) ->
              List.iter
                (fun cl ->
                  let ltmp, utmp = loc.compExpr.(cl) in
                  let lnew =
                    if not (List.mem e ltmp) then
                      e::ltmp
                    else
                      ltmp
                  in
                  let unew =
                    if not (List.mem e utmp) then
                      e::utmp
                    else
                      utmp
                  in
                  loc.compExpr.(cl) <- lnew, unew
                )
                (clocks_of ta lhs)
          | _ -> failwith "cannot compute LU bounds, guard is not in normal form"
        in

        (* add invariant contribution *)
        List.iter ag_handle loc.locInvar;

        (* for each transition, add guard contribution *)
        List.iter (fun edge ->
          List.iter ag_handle edge.edgeGuard)
        loc.locEdges
      done;

      (* fixpoint computation
       * for each location l, for each transition t from l to l',
       * for each clock c,
       * if c is not reset by t, add the expressions for c from l' in l
       * if the set for l changes in the operation, remember to loop once more
       *)
      let stable = ref false in
      while not !stable do
        stable := true;
        (* for each location *)
        for l=0 to (Array.length proc.procLocations)-1 do
          let loc = proc.procLocations.(l) in
          (* iterate over the transitions *)
          List.iter (fun edge ->
            (* for each clock *)
            for cl=0 to nclocks-1 do
              (* if it is not reset *)
              if List.for_all (fun u -> not (is_reset cl u)) edge.edgeUpdates then
                begin
                  let lcurrent, ucurrent = loc.compExpr.(cl) in
                  (* update lower bounds *)
                  let lnew = List.fold_left (fun acc e ->
                    if not (List.mem e acc) then (
                      stable := false;
                      e::acc
                    ) else (
                      acc
                    )
                  ) lcurrent (fst proc.procLocations.(edge.edgeTarget).compExpr.(cl))
                  in
                  (* update upper bounds *)
                  let unew = List.fold_left (fun acc e ->
                    if not (List.mem e acc) then (
                      stable := false;
                      e::acc
                    ) else (
                      acc
                    )
                  ) ucurrent (snd proc.procLocations.(edge.edgeTarget).compExpr.(cl))
                  in
                  (* do the actual update *)
                  loc.compExpr.(cl) <- lnew, unew
                end
            done
          ) loc.locEdges
        done
      done
    done


  (** Constructs a timed_automaton from the C data structure produced by the
   *  library utap.
   *  If true, the boolean parameter enables CORA support.
   *  TODO compared to previous version, this lacks:
     *  parameterization by guard_of_transition
     *  parameterization by invariant_of_discrete_state
     *  scaling
     *  enlarging
   *  This hinders the ability to instantiate to other kinds of automata,
   *  such as enlarged automata
   *)
  external utap_from_file : string -> string -> bool -> ta = "xta_from_xmlfile";;

  let build_ta_from_processes channels clockcont varcont var_init_values constcont constvalues procs =
    (* Fill in the edgeProc and locProc fields in all locations and edges *)
    Array.iter (fun proc ->
        Array.iter (fun loc ->
            loc.locName <- proc.procName ^ "." ^ loc.locName;
          ) proc.procLocations
      )
      procs;
    let procNames = Array.map (fun p -> p.procName) procs in
    (* Prefix all names with the scope process names *)
    let clocks = ScopeVarContext.to_vc clockcont procNames in
    let vars = ScopeVarContext.to_vc varcont procNames in
    let constants = ScopeVarContext.to_vc constcont procNames in

    (* build the array of const values *)
    let nconst = (Hashtbl.length constvalues) in
    let const_val = Array.make nconst 0 in
    for i = 0 to nconst-1 do
      const_val.(i) <- Hashtbl.find constvalues i;
    done;
    let nvars = (Hashtbl.length var_init_values) in
    let initLocs = Array.map (fun proc -> proc.procLocations.(proc.procInitLoc)) procs in
    let initVars = Array.make nvars 0 in
    for i = 0 to nvars-1 do
      initVars.(i) <- Hashtbl.find var_init_values i;
    done;
    (* Check that the special-meaning variable is at the correct index *)
    if (VarContext.index_of_var vars "preference" <> 0) then begin
      Printf.printf "preference has a wrong index, but this is not supposed to happen\n Aborting...\n";
      exit 1;
    end;
    let ta = {
      procs = procs;
      clocks = clocks;
      vars = vars;
      constants = constants;
      constvalues = const_val;
      channels = channels;
      init = {stateLocs = initLocs; stateVars = initVars};
      query = EmptyQuery;
      lubounds_tbl = DSHashtbl.create 1024;
      global_mbounds = Array.make (VarContext.size clocks) min_int;
    }
    in

    let cb_find_process procName =
      let res = ref (-1) in
      Array.iteri (fun i p -> if p.procName = procName then res := i) ta.procs;
      !res
    in
    Callback.register "cb_get_proc" cb_find_process;
    let cb_find_location procId locName =
      let proc = ta.procs.(procId) in
      let res = ref (-1) in
      Array.iteri (fun i l -> if l.locName = locName then res := i) proc.procLocations;
      !res
    in
    Callback.register "cb_get_loc" cb_find_location;

    Printf.printf "Input automaton parsed, computing LU bounds\n";
    flush stdout;
    let (elapsed_seconds,_) = Time.measure_function (fun () -> build_lu ta) in
    Printf.printf "Took %d seconds to compute LU bounds\n" elapsed_seconds;
    ta

  let make_ta tafile qfile =
    (** Variable and clock contexts have initially keys of type (p,name)
     * where p is process option (None for global variables),
     * and name the name of the variable. *)
    (* Clocks *)
    let clockcont = ScopeVarContext.create () in
    (* Variables, with initial values *)
    let varcont = ScopeVarContext.create () in
    let var_init_values = Hashtbl.create 16 in
    (* Constants, with initial values *)
    let constcont = ScopeVarContext.create () in
    let const_values = Hashtbl.create 16 in

    (* Register C callbacks to build expressions *)
    Callback.register "cb_expression_constant" cb_expression_constant;
    Callback.register "cb_expression_variable"
      (cb_expression_variable constcont const_values varcont);
    Callback.register "cb_expression_clock" (cb_expression_clock clockcont);
    Callback.register "cb_expression_sum" cb_expression_sum;
    Callback.register "cb_expression_product" cb_expression_product;
    Callback.register "cb_expression_substraction" cb_expression_substraction;
    Callback.register "cb_expression_division" cb_expression_division;
    Callback.register "cb_expression_array"
      (cb_expression_array varcont constcont clockcont);

    (* C callbacks for arrays of integers *)
    let cb_reg_array_name procref arrayName =
      ScopeVarContext.add_array varcont (procref, arrayName)
    in
    Callback.register "cb_register_array_name" cb_reg_array_name;
    let cb_reg_array_cell procref arrayName indices value =
      let cellId = ScopeVarContext.add_cell varcont (procref, arrayName) indices
      in
      Hashtbl.add var_init_values cellId value
    in
    Callback.register "cb_register_array_cell" cb_reg_array_cell;

    (* C callbacks for const arrays of integers *)
    let cb_reg_const_array_name procref arrayName =
      ScopeVarContext.add_array constcont (procref, arrayName)
    in
    Callback.register "cb_register_const_array_name" cb_reg_const_array_name;
    let cb_reg_const_array_cell procref arrayName indices value =
      let cellId = ScopeVarContext.add_cell constcont (procref, arrayName) indices
      in
      Hashtbl.add const_values cellId value
    in
    Callback.register "cb_register_const_array_cell" cb_reg_const_array_cell;

    (* C callbacks for arrays of clocks *)
    let cb_reg_clock_array procref arrayName =
      ScopeVarContext.add_array clockcont (procref, arrayName)
    in
    Callback.register "cb_register_clock_array_name" cb_reg_clock_array;
    let cb_reg_clock_array_cell procref arrayName indices =
      let _ = ScopeVarContext.add_cell clockcont (procref, arrayName) indices in ()
    in
    Callback.register "cb_register_clock_array_cell" cb_reg_clock_array_cell;


    (* C callbacks for channels and arrays of channels *)
    (* Due to the very nature of channels, all channels and arrays of channels
     * should be global, which we assume here.
     * Thus, we directly use a VarContext, not a ScopeVarContext.
     *)
    let chans = VarContext.create () in
    Callback.register "cb_channel_simple" (cb_channel_simple chans);
    Callback.register "cb_channel_array" (cb_channel_array chans);
    (* first argument (reference to scope proc) kept for compatibility *)
    let cb_register_channel_array_name _ arrayName =
      VarContext.add_array chans arrayName
    in
    Callback.register "cb_register_channel_array_name" cb_register_channel_array_name;
    let cb_register_channel_array_cell _ arrayName indices =
      let _ = VarContext.add_cell chans arrayName indices in ()
    in
    Callback.register "cb_register_channel_array_cell" cb_register_channel_array_cell;

    (* C callbacks for constants *)
    let cb_register_constant tmp name value =
      let varid = ScopeVarContext.add constcont (tmp, name) in
      Hashtbl.add const_values varid value
    in
    Callback.register "cb_register_constant" cb_register_constant;
    (* C callbacks for variables *)
    let cb_register_variable tmp name value =
      let varid = ScopeVarContext.add varcont (tmp, name) in
      Hashtbl.add var_init_values varid value
    in
    Callback.register "cb_register_variable" cb_register_variable;
    (* C callback for clocks *)
    let cb_register_clock tmp name =
      let _ = ScopeVarContext.add clockcont (tmp, name) in ()
    in
    Callback.register "cb_register_clock" cb_register_clock;
    (* C callbacks for channels *)
    (* first argument (reference to scope proc) kept for compatibility *)
    let cb_register_channel _ name =
      let _ = VarContext.add chans name in ()
    in
    Callback.register "cb_register_channel" cb_register_channel;

    let rec evaluate_expression = function
      | Constant(c) -> c
      | Clock(_) | ClockArray(_,_) -> failwith "there should not be clocks in evaluated expressions"
      | Array(_,_) | ConstArray(_,_) -> failwith "there should not be array accesses in evaluated expressions"
      | Variable(i) -> Hashtbl.find var_init_values i
      | ConstVariable(i) -> Hashtbl.find const_values i
      | Sum(a,b) -> (evaluate_expression a) + (evaluate_expression b)
      | Product(a,b) -> (evaluate_expression a) * (evaluate_expression b)
      | Substraction(a,b) -> (evaluate_expression a) - (evaluate_expression b)
      | Division(a,b) -> (evaluate_expression a) / (evaluate_expression b)
    in
    Callback.register "cb_evaluate_expr" evaluate_expression;
    (** Get discrete guard from mixed guard *)
    let filter_disc_guard g =
      let rec filt_exp = function
        | Clock(_) | ClockArray(_,_) -> false
        | Sum(x,y) -> (filt_exp x) && (filt_exp y)
        | Product(x,y) -> (filt_exp x) && (filt_exp y)
        | Substraction(x,y) -> (filt_exp x) && (filt_exp y)
        | Division(x,y) -> (filt_exp x) && (filt_exp y)
        | Array(_, l) -> List.for_all (fun x -> filt_exp x) l
        | _ -> true
      in
      let filt_ag = function
        | GuardLess(x,y) -> (filt_exp x) && (filt_exp y)
        | GuardLeq(x,y) -> (filt_exp x) && (filt_exp y)
        | GuardGreater(x,y) -> (filt_exp x) && (filt_exp y)
        | GuardGeq(x,y) -> (filt_exp x) && (filt_exp y)
        | GuardEqual(x,y) -> (filt_exp x) && (filt_exp y)
        | GuardNeq(x,y) -> (filt_exp x) && (filt_exp y)
      in
      List.filter filt_ag g
    in
    (** Get clock guard from mixed guard *)
    let filter_clock_guard g =
      let rec filt_exp = function
        | Clock(_) | ClockArray(_,_) -> true
        | Sum(x,y) -> (filt_exp x) || (filt_exp y)
        | Product(x,y) -> (filt_exp x) || (filt_exp y)
        | Substraction(x,y) -> (filt_exp x) || (filt_exp y)
        | Division(x,y) -> (filt_exp x) || (filt_exp y)
        | Array(_, l) -> List.exists (fun x -> filt_exp x) l
        | _ -> false
      in
      let filt_ag = function
        | GuardLess(x,y) -> (filt_exp x) || (filt_exp y)
        | GuardLeq(x,y) -> (filt_exp x) || (filt_exp y)
        | GuardGreater(x,y) -> (filt_exp x) || (filt_exp y)
        | GuardGeq(x,y) -> (filt_exp x) || (filt_exp y)
        | GuardEqual(x,y) -> (filt_exp x) || (filt_exp y)
        | GuardNeq(x,y) -> (filt_exp x) || (filt_exp y)
      in
      List.filter filt_ag g
    in
    let cb_send_channel chan =
      Some(SendChan(chan))
    in
    let cb_recv_channel chan =
      Some(RecvChan(chan))
    in
    Callback.register "cb_send_channel" cb_send_channel;
    Callback.register "cb_recv_channel" cb_recv_channel;
    let build_edge src dst extGuard extUpdate sync procId control =
      {
        edgeSource = src;
        edgeGuard = filter_clock_guard extGuard;
        edgeDiscGuard = filter_disc_guard extGuard;
        edgeUpdates = List.rev (List.map (function
          | (Clock(x),e) -> ClockRef(x),e
          | (ClockArray(a,l),e) -> ClockArrayRef(a,l),e
          | (Variable(x),e) -> VarRef(x),e
          | (Array(a,l),e) -> ArrayRef(a,l),e
          | _ -> failwith "incorrect LHS for update")
        extUpdate);
        edgeTarget = dst;
        edgeSync = sync;
        edgeProc = procId;
        edgeControllable = control;
        (* TODO currently set to default *)
        edgeCost = Costs.edge_cost_def;
      }
    in
    Callback.register "cb_build_edge" build_edge;
    let build_location id name committed urgent guard edges procId costRate =
      {
        locId = id;
        locName = name;
        locCommitted = committed;
        locUrgent = urgent;
        locInvar = guard;
        locEdges = edges;
        locProc = procId;
        locRate = costRate;
        compExpr = Array.make 0 ([],[]); (* actually built during LU bounds computation *)
      }
    in
    Callback.register "cb_build_location" build_location;
    let build_process name id locations init =
      {
        procName = name;
        procId = id;
        procLocations = locations;
        procInitLoc = init;
      }
    in
    Callback.register "cb_build_process" build_process;
    let build_location_array n = Array.make n (build_location 0 "" false false [] [] 0 Costs.loc_rate_def) in
    Callback.register "cb_build_location_array" build_location_array;
    let build_process_array n = Array.make n (build_process "" 0 (build_location_array 0) 0) in
    Callback.register "cb_build_process_array" build_process_array;
    let build_ta procs = build_ta_from_processes
      chans clockcont varcont var_init_values constcont const_values procs in
    Callback.register "cb_build_ta" build_ta;
    let ta_set_query ta newquery = { ta with query = newquery; } in
    Callback.register "cb_set_query" ta_set_query;
    utap_from_file tafile qfile

  let from_file tafile qfile enable_cora ?scale:(scale=1) ?enlarge:(enlarge=0) () =
    let ta = make_ta tafile qfile enable_cora in
    ta

  let model = from_file Files.tafile Files.qfile Files.enable_cora ()

end