Commit 332ae767 authored by Maximilien Colange's avatar Maximilien Colange

Refactoring: make filenames consistent with their contents.

parent 06cb9bf9
open Uta
open Expression
IFDEF ENABLE_CORA THEN
......
type expression =
| Constant of int
| Variable of int
| ConstVariable of int
| Clock of int
| ClockArray of int * expression list
| Array of int * expression list
| ConstArray of int * expression list
| Sum of expression * expression
| Product of expression * expression
| Substraction of expression * expression
| Division of expression * expression
open Varcontext
(**
* an atomic guard is a tuple (c,k,r), where c is a clock id (see VarContext)
* and k is a constant and r is one of <, <=, >, >= or ==.
......@@ -15,11 +17,11 @@ type guard_t = atomic_guard list
(* a printer for an atomic guard *)
let print_ag clocks = function
| LT(c,k) -> (Uta.VarContext.var_of_index clocks c) ^ " < " ^ (string_of_int k)
| LEQ(c,k) -> (Uta.VarContext.var_of_index clocks c) ^ " <= " ^ (string_of_int k)
| GT(c,k) -> (Uta.VarContext.var_of_index clocks c) ^ " > " ^ (string_of_int k)
| GEQ(c,k) -> (Uta.VarContext.var_of_index clocks c) ^ " <= " ^ (string_of_int k)
| EQ(c,k) -> (Uta.VarContext.var_of_index clocks c) ^ " == " ^ (string_of_int k)
| LT(c,k) -> (VarContext.var_of_index clocks c) ^ " < " ^ (string_of_int k)
| LEQ(c,k) -> (VarContext.var_of_index clocks c) ^ " <= " ^ (string_of_int k)
| GT(c,k) -> (VarContext.var_of_index clocks c) ^ " > " ^ (string_of_int k)
| GEQ(c,k) -> (VarContext.var_of_index clocks c) ^ " <= " ^ (string_of_int k)
| EQ(c,k) -> (VarContext.var_of_index clocks c) ^ " == " ^ (string_of_int k)
(* a printer for a guard *)
let rec print_guard clocks = function
......@@ -36,8 +38,8 @@ type reset_t = Common.clock_t * int
(* a printer for a list of resets *)
let rec print_resets clocks = function
| [] -> " "
| [(c,k)] -> Uta.VarContext.var_of_index clocks c ^ " := " ^ (string_of_int k)
| (c,k) :: l -> Uta.VarContext.var_of_index clocks c ^ " := " ^ (string_of_int k) ^ (print_resets clocks l)
| [(c,k)] -> VarContext.var_of_index clocks c ^ " := " ^ (string_of_int k)
| (c,k) :: l -> VarContext.var_of_index clocks c ^ " := " ^ (string_of_int k) ^ (print_resets clocks l)
(**
* The interface of Timed Automaton to implement when you want to provide
......@@ -49,7 +51,7 @@ sig
type state
(* retrieves ALL the clocks of the model *)
val clocks : ta -> Uta.VarContext.t
val clocks : ta -> VarContext.t
(* the initial state *)
val initial_state : ta -> state
......@@ -95,138 +97,3 @@ end
let loadedmodule : (module TA) option ref = ref None
(*let loaded_model : TA.ta option ref = ref None*)
module MakeTA (BareTA : TA) (MDbm : Dbm.BIG_IDBM)
: TimedAutomaton.TIMED_AUTOMATON with type MDbm.dbm_t = MDbm.dbm_t and type discrete_state = BareTA.state =
struct
module DS =
struct
type t = BareTA.state
let hash = BareTA.hash_state
let equal = BareTA.equal_state
end
module MDbm = MDbm
module DSHashtbl = Hashtbl.Make(DS)
type timed_automaton =
{
t : BareTA.ta;
lu_tbl : (Udbml.Carray.t * Udbml.Carray.t) DSHashtbl.t;
m_tbl : Udbml.Carray.t DSHashtbl.t;
}
type discrete_state = BareTA.state
type edge (* TODO *)
(* indirection *)
let clocks ta = BareTA.clocks ta.t
(* indirection *)
let priority_compare = BareTA.priority_compare
(* indirection *)
let is_urgent_or_committed ta = BareTA.is_urgent_or_committed ta.t
(* indirection *)
let is_target ta = BareTA.is_target ta.t
(* indirection *)
let rate_of_state ta = BareTA.rate_of_state ta.t
(* indirection *)
let global_m_bounds ta = BareTA.global_mbounds ta.t
let initial_extended_state ta =
let dim = (Uta.VarContext.size (clocks ta)) in
let z = MDbm.Dbm.create dim in
MDbm.Dbm.set_zero z;
(BareTA.initial_state ta.t, z)
(* a helper function to turn a guard into a Dbm *)
let guard_to_dbm ta s g =
let z = Dbm.UDbm.Dbm.create (Uta.VarContext.size (clocks ta)) in
Dbm.UDbm.Dbm.set_init z;
List.iter (function
| LT (c,k) ->
Dbm.UDbm.Dbm.constrain z (c, 0, (k, Udbml.Basic_types.DBM_STRICT))
| LEQ (c,k) ->
Dbm.UDbm.Dbm.constrain z (c, 0, (k, Udbml.Basic_types.DBM_WEAK))
| GT (c,k) ->
Dbm.UDbm.Dbm.constrain z (0, c, (-k, Udbml.Basic_types.DBM_STRICT))
| GEQ (c,k) ->
Dbm.UDbm.Dbm.constrain z (0, c, (-k, Udbml.Basic_types.DBM_WEAK))
| EQ (c,k) ->
Dbm.UDbm.Dbm.constrain z (0, c, (-k, Udbml.Basic_types.DBM_WEAK));
Dbm.UDbm.Dbm.constrain z (c, 0, (k, Udbml.Basic_types.DBM_WEAK))
) g;
z
let transitions_from ta state =
List.map (fun (s,g,r,s') -> (s,guard_to_dbm ta s g,r,s')) (BareTA.transitions_from ta.t state)
let invariant_of_discrete_state ta s =
guard_to_dbm ta s (BareTA.invariant ta.t s)
(* store LU bounds in their C form, to avoid repeated translations *)
let lu_bounds ta s =
try
DSHashtbl.find ta.lu_tbl s
with
| Not_found ->
let larr, uarr = BareTA.lubounds ta.t s in
let n = Array.length larr in
let ltmp, utmp = Udbml.Carray.to_c larr n, Udbml.Carray.to_c uarr n in
DSHashtbl.add ta.lu_tbl s (ltmp, utmp);
(ltmp, utmp)
(* store M bounds in their C form, to avoid repeated translations *)
let m_bounds ta s =
try
DSHashtbl.find ta.m_tbl s
with
| Not_found ->
let larr, uarr = BareTA.lubounds ta.t s in
let n = Array.length larr in
let marr = Array.make n 0 in
for i=0 to n-1 do
marr.(i) <- max larr.(i) uarr.(i)
done;
let mtmp = Udbml.Carray.to_c marr n in
DSHashtbl.add ta.m_tbl s mtmp;
mtmp
(* PRINT functions *)
(* indirection *)
let print_discrete_state chan ta s =
Printf.fprintf chan "%s" (BareTA.state_to_string ta.t s)
let print_extended_state chan ta (s,z) =
print_discrete_state chan ta s;
Printf.fprintf chan "%s " (MDbm.Dbm.to_string z)
(* indirection *)
let print_timed_automaton chan ta =
BareTA.print_timed_automaton chan ta.t
let transition_to_string ta (source, dbm, ulist, target) =
let (_,guard,_,_) = List.find (fun (_, g, u, t) ->
DS.equal target t && ulist = u && Dbm.UDbm.Dbm.equal dbm (guard_to_dbm ta source g))
(BareTA.transitions_from ta.t source)
in
let buf = Buffer.create 128 in
let out = Buffer.add_string buf in
out "(";
out (BareTA.state_to_string ta.t source);
out ",";
out (print_guard (clocks ta) guard);
out ",";
out (print_resets (clocks ta) ulist);
out ",";
out (BareTA.state_to_string ta.t target);
out ")";
Buffer.contents buf
let from_file filename _ ?scale:(scale=1) ?enlarge:(enlarge=0) () =
{
t = BareTA.from_file filename;
lu_tbl = DSHashtbl.create 1024;
m_tbl = DSHashtbl.create 1024;
}
end
......@@ -83,7 +83,7 @@ struct
and type dbm_t := Dbm.Dbm.t
and type arg_t := COMP.arg_t
let ta_module = ref (module GenericUAutomaton(M.Dbm) : ITA)
let ta_module = ref (module Uppaalta.GenericUAutomaton(M.Dbm) : ITA)
module type ITA_ABSTRACTION = functor (TA : ITA) ->
ABSTRACTION with type arg_t = TA.timed_automaton * TA.discrete_state
......
open Uta
open Expression
type atomic_guard =
| GuardLeq of expression * expression
......
open Common
open TimedAutomaton
open Uta
open Varcontext
let print_path = ref false
......
This diff is collapsed.
This diff is collapsed.
......@@ -2,19 +2,6 @@ open Printf
exception Var_already_defined
exception Var_undefined of string
type expression =
| Constant of int
| Variable of int
| ConstVariable of int
| Clock of int
| ClockArray of int * expression list
| Array of int * expression list
| ConstArray of int * expression list
| Sum of expression * expression
| Product of expression * expression
| Substraction of expression * expression
| Division of expression * expression
module type VARCONTEXT =
functor (Vars : sig type var_t type array_t val cell2var : array_t -> int list -> var_t end) ->
sig
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment