uppaalta.ml 41.6 KB
Newer Older
1 2 3 4 5
open Common
open Expression
open Printf
open Varcontext

6
module GenericUAutomaton (Files : sig val tafile : string val qfile : string val enable_cora : bool end) : Ita.TA =
7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34
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)
35

36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78
  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
79 80
    | ClockArrayRef of int * expression list
    | VarRef of int
81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96
    | 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)

97
  type simplechan =
98 99
      SendChan of chanref
    | RecvChan of chanref
100

101 102 103 104 105 106 107 108 109 110 111 112 113 114

  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;
115
      (* the ID of the location *)
116
    mutable locName : string;
117
      (* the name of the location, for printing purposes *)
118 119 120 121 122 123 124 125
    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 *)
126 127 128 129 130 131
    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.
       *)
132 133 134 135 136 137 138
  }
  and process = {
    procName : string;
    procId : int;
    procLocations : location array;
    procInitLoc : int;
  }
139
  type state = {
140 141 142 143
    stateLocs : location array;
    stateVars : int array;
  }

144 145
  type transition = InternalTrans of state * edge
                  | SyncTrans of state * edge * edge
146 147


148
  let hash_state s =
149 150 151 152 153 154 155
    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

156
  let equal_state s t =
157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177
    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
178 179 180
    type t = state
    let equal = equal_state
    let hash = hash_state
181 182 183 184 185
  end

  module DSHashtbl = Hashtbl.Make(DS)

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

189
  type ta = {
190 191 192 193 194 195
    procs : process array; (* forall i: procs.(i).procId = i *)
    clocks : VarContext.t;
    vars : VarContext.t;
    constants : VarContext.t;
    constvalues : int array;
    channels : VarContext.t;
196
    init : state;
197 198 199 200 201 202
    query : query;
    lubounds_tbl : (int array * int array) DSHashtbl.t;
    global_mbounds : int array;
  }

  (********** PRINTING AUXILIARY FUNCTIONS **********)
203
  let rec string_of_exp ta e =
204 205
    let string_of_exp = string_of_exp ta in
    (function
206 207
      | Constant c -> sprintf "%d" c
      | Array(aid, indices) ->
208 209
          let arrayName = VarContext.array_of_index ta.vars aid in
          List.fold_left (fun s x -> s ^ "[" ^ (string_of_exp x) ^ "]") arrayName indices
210
      | ConstArray(aid, indices) ->
211 212
          let arrayName = VarContext.array_of_index ta.constants aid in
          List.fold_left (fun s x -> s ^ "[" ^ (string_of_exp x) ^ "]") arrayName indices
213 214 215
      | 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
216 217 218
      | 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
219 220 221 222 223 224 225 226 227 228 229 230 231 232 233
      | 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


234
  let string_of_atomic_guard ta =
235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250
    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)


251 252
  let xml_string_of_atomic_guard ta =
    let string_of_exp = string_of_exp ta in
253 254 255 256 257 258 259 260 261 262 263 264 265 266 267
    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)


268
  let rec string_of_guard ta =
269 270 271
    function
    | [] -> ""
    | [x] -> string_of_atomic_guard ta x
272
    | x :: y :: l ->
273 274 275 276 277 278 279 280
      ((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
281
    | x :: y :: l ->
282 283 284 285
      ((xml_string_of_atomic_guard ta x) ^ " &amp;&amp; ")
      ^ (xml_string_of_guard ta (y::l))


286 287 288
  let string_of_updates ta ups =
    let ups_str =
      List.map (fun (var,exp) ->
289 290 291 292 293 294 295
        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

296

297
  let string_of_state ta state =
298
    let out = Buffer.create 50 in
299 300 301 302 303 304 305 306 307 308 309
    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

310 311

  let string_of_edge ta edge =
312 313 314 315 316 317
    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
318
    let sync = match edge.edgeSync with
319 320 321 322 323 324
      |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
325
    sprintf "%s%s -> %s \tDiscGuard: %s \tGuard: %s \tUpdates:%s \tSync:%s"
326 327 328 329 330 331 332 333
      (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

334

335 336 337 338 339 340 341 342 343 344 345 346 347 348 349
  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


350
  let string_of_process ta proc =
351 352 353 354 355 356 357 358 359 360 361 362
    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
363
    match tr with
364 365 366 367 368 369 370 371 372 373 374 375 376 377 378
      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 **********)
379

380 381 382 383 384
  (* evaluate expression *)
  (* output is either Constant(_) or Clock(_)
   *)
  let rec eval_exp ta vars = function
    | Constant c -> Constant c
385 386
    | ConstVariable id ->
        assert(id >= 0 && id < Array.length ta.constvalues);
387
        Constant ta.constvalues.(id)
388 389
    | Variable id ->
        assert(id >= 0 && id < Array.length vars);
390
        Constant vars.(id)
391
    | Clock c -> Clock c
392 393 394
    | 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
395
        Clock cellindex
396
    | Array(arrayId, l) ->
397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412
        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))
413

414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441
  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")
442

443 444 445 446 447 448 449 450
  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)

451 452

  let _copy_state state =
453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479
    { 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

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

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

486
  let initial_state ta = ta.init
487 488 489 490 491 492 493 494 495 496 497

  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)

498
  let _transitions_from ta state =
499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537
    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

538 539 540 541 542
  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
543 544 545 546 547 548 549 550 551 552 553 554
    | 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')
555

556 557 558 559 560 561 562
  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"
563 564

  let transitions_from ta state =
565 566 567 568 569 570
    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
571

572
  let transition_to_string = string_of_transition
573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591

  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

592
  (* TODO *)
593
  let global_mbounds ta =
594
    failwith "not implemented"
595 596 597 598

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

  let print_transition chan ta trans =
601 602 603 604 605 606
    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
607

608
  (********** LOADING FUNCTIONS **********)
609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635

  (** 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)
636
   *)
637 638 639 640 641 642 643
  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 =
644
    let n = VarContext.size ta.clocks in
645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697
    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 *)
698 699
  let build_lu ta =
    let nclocks = VarContext.size ta.clocks in
700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809
    (* 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

810 811 812

  (** Constructs a timed_automaton from the C data structure produced by the
   *  library utap.
813
   *  If true, the boolean parameter enables CORA support.
814 815 816 817 818 819 820 821
   *  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
   *)
822
  external utap_from_file : string -> string -> bool -> ta = "xta_from_xmlfile";;
823 824 825

  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 *)
826 827
    Array.iter (fun proc ->
        Array.iter (fun loc ->
828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864
            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;
865
      global_mbounds = Array.make (VarContext.size clocks) min_int;
866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884
    }
    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;
885 886
    let (elapsed_seconds,_) = Time.measure_function (fun () -> build_lu ta) in
    Printf.printf "Took %d seconds to compute LU bounds\n" elapsed_seconds;
887
    ta
888

889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946
  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;
947

948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003

    (* 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 *)
1004
    let filter_disc_guard g =
1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024
      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 *)
1025
    let filter_clock_guard g =
1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069
      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 *)
1070
        edgeCost = Costs.edge_cost_def;
1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083
      }
    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;
1084
        compExpr = Array.make 0 ([],[]); (* actually built during LU bounds computation *)
1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107
      }
    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

1108 1109
  let from_file tafile qfile enable_cora ?scale:(scale=1) ?enlarge:(enlarge=0) () =
    let ta = make_ta tafile qfile enable_cora in
1110
    ta
1111 1112

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

1114 1115
end