Commit 9550b8d2 authored by Maximilien Colange's avatar Maximilien Colange

Merge branch 'dynload'

parents aba08bdc 872d1c1f
<*>: bin_annot
<*.cm{o,x}> or <main.native>: package(batteries), debug, custom
<*.cm{o,x}> or <main.native>: debug, custom
<main.native>: package(dynlink)
<costs.ml>: pp(camlp4o pa_macro.cmo @TIAMO_MACROS@)
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 ==.
* Diagonal guards are not allowed.
*)
type atomic_guard =
LT of int * int
| LEQ of int * int
| GT of int * int
| GEQ of int * int
| EQ of int * int
(* a guard is a conjunction of atomic guards *)
type guard_t = atomic_guard list
(* a printer for an atomic guard *)
let print_ag clocks = function
| 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
| [] -> "TRUE"
| [ag] -> print_ag clocks ag
| ag :: l -> print_ag clocks ag ^ " && " ^ (print_guard clocks l)
(**
* a reset is a pair (c,k), where c is a clock id (see VarContext)
* and k is a constant.
*)
type reset_t = Common.clock_t * int
(* a printer for a list of resets *)
let rec print_resets clocks = function
| [] -> " "
| [(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
* your model as a compiled OCaml object.
*)
module type TA =
sig
type ta
type state
(* retrieves ALL the clocks of the model *)
val clocks : ta -> VarContext.t
(* the initial state *)
val initial_state : ta -> state
(* utility functions about states *)
val hash_state : state -> int
val equal_state : state -> state -> bool
(* encodes the query on the model *)
val is_target : ta -> state -> bool
(* priority_compare s1 s2 is true iff s1 should be explored before s2 *)
(* this allows the modeller to provide heuristics about the exploration of
* the state space *)
val priority_compare : state -> state -> int
(* the transitions out of a state *)
val transitions_from : ta -> state -> (state * guard_t * (reset_t list) * state) list
(* the invariant of a state *)
val invariant : ta -> state -> guard_t
(* whether time can elapse in the state *)
val is_urgent_or_committed : ta -> state -> bool
(* the rate of a state *)
val rate_of_state : ta -> state -> int
(* the LU bounds (per clock) of a state *)
(**
* NB: larger bounds do not impact correctness.
* When in doubt, pick too large bounds.
* Remember that tight bounds yield better performance.
*)
val lubounds : ta -> state -> int array * int array
(* the global M bounds (per clock) of an automaton *)
(* this required if you want to bound the automaton *)
val global_mbounds : ta -> int array
(* to load a TA from a file *)
val model : ta
(** PRINT FUNCTIONS **)
val string_of_state : ta -> state -> string
val print_timed_automaton : out_channel -> ta -> unit
end
(**
* If you want to load a compiled module, you must implement the TA
* interface above, and you should set this variable.
* E.g.
* module MyTA : TA = struct ... end
* let _ = Ita.loadedmodule := Some (module MyTA)
*
* It is the only way provided by the Ocaml Dynlink module to access the
* dynamically loaded data.
*)
let loadedmodule : (module TA) option ref = ref None
open Batteries
open Printf
type log_t = Info | Debug | Warning | Error | Fatal
......
open Batteries
open Options
open Printf
open Reachability
......@@ -8,19 +7,21 @@ open Dbm
(** For Arg.align to properly display help messages, do not forget to make them
* start with a space.
*)
let tafile = ref ""
let qfile = ref ""
let show_gc_stats = ref false
let anon_arguments arg =
if (Filename.check_suffix arg ".xml") then (
if Filename.check_suffix arg ".xml" then (
inputtype := XML;
tafile := arg
)
else if (Filename.check_suffix arg ".q") then (
else if Filename.check_suffix arg ".q" then (
inputtype := XML;
qfile := arg
)
else if Filename.check_suffix arg ".cmxs" then (
inputtype := CMXS;
ofile := arg
)
else (
Log.fatalf "File extension not recognized: %s\n" arg;
raise (Arg.Bad "Unrecognized file extension")
......@@ -37,11 +38,15 @@ Usage: tiamo <command> [options] <ta-file> [<query-file>]
For further information about the options for each command, type
tiamo <command> -help
<ta-file> is a .xml file in uppaal format.
Our parser is still a light version and does not support the whole syntax.
<ta-file> is a file describing the input model.
It can be one of the following format:
- a .xml using uppaal syntax. Note however that TiAMo does not support the full syntax of uppaal.
- a .cmxs (ocaml shared object file).
Beware of the extension, TiAMo relies on it to decide how to load the model.
<query-file> is a .q file in uppaal format.
If only a ta file 'foo.xml' is given, tiamo assumes the query file is 'foo.q'.
<query-file> should be a .q file in uppaal format.
If <ta-file> is not a .xml, this file is simply ignored.
This is for backward compatibility only, as the query can be embedded in the .xml file.
"
let mc_module = ref (module Unpriced : OPTIONS)
......@@ -63,17 +68,7 @@ let main() =
Printexc.record_backtrace true;
Arg.parse_dynamic arg_list set_command usage;
let module MC = (val !mc_module : OPTIONS) in
if ( !tafile = "" ) then
(
Arg.usage [] usage;
exit 1
);
if ( !qfile = "" ) then
(
qfile := (Filename.chop_suffix !tafile ".xml") ^ ".q";
(* Log.warningf "Guessing query file: %s\n" !qfile *)
);
let res = Options.verify (module MC) !tafile !qfile in
let res = Options.verify (module MC) in
Printf.printf "Result of verification is %s\n" res;
if (!show_gc_stats) then
Gc.print_stat stdout
......
......@@ -8,7 +8,7 @@ sig
module type ITA = TIMED_AUTOMATON with type MDbm.dbm_t = t
val ta_module : (module ITA) ref
val get_ta : unit -> (module ITA)
module type PARTIAL_WO =
functor (Key : Hashtbl.HashedType) ->
......@@ -83,8 +83,6 @@ struct
and type dbm_t := Dbm.Dbm.t
and type arg_t := COMP.arg_t
let ta_module = ref (module GenericUAutomaton(M.Dbm) : ITA)
module type ITA_ABSTRACTION = functor (TA : ITA) ->
ABSTRACTION with type arg_t = TA.timed_automaton * TA.discrete_state
and type dbm_t := TA.MDbm.Dbm.t
......@@ -120,6 +118,19 @@ struct
end
with type res_t = res_t
let do_bound = ref false
let get_ta () : (module ITA) =
match !Ita.loadedmodule with
| None -> failwith "No module loaded!"
| Some m ->
let module BTA = (val m : Ita.TA) in
let module TA = TimedAutomaton.MakeTimedAutomaton(BTA)(M.Dbm) in
if !do_bound then
(module TimedAutomaton.MBoundedAutomaton(TA))
else
(module TA)
(* TODO move common options here *)
let common_args =
[
......@@ -128,7 +139,7 @@ struct
" Print a witness path (not activated by default)");
( "-mbounded",
Arg.Unit (function () -> let module TA = (val !ta_module) in ta_module := (module MBoundedAutomaton(TA) : ITA)),
Arg.Unit (function () -> do_bound := true),
" Use the (global M)-bounded version of the input automaton.
\tThis induces a performance hit, but guarantees termination of algorithms when you are not sure whether the input automaton is bounded or not.");
]
......@@ -252,10 +263,35 @@ struct
])
end
let verify (module O : OPTIONS) tafile qfile =
let module TA = (val !O.ta_module) in
let ta = TA.from_file tafile qfile () in
(* TA.print_timed_automaton Batteries.stdout ta; *)
(* TODO ML, O and C are not supported yet *)
type input_type_t = XML | CMXS | ML | O | C
let inputtype = ref XML
(* filenames to load the model *)
let tafile = ref ""
let qfile = ref ""
let ofile = ref ""
let load () =
match !inputtype with
| XML -> assert(!tafile <> ""); Ita.loadedmodule := Some (module Uppaalta.GenericUAutomaton(struct let tafile = !tafile;; let qfile = !qfile end))
| CMXS ->
begin
assert(!ofile <> "");
try
Dynlink.loadfile !ofile;
with
| Dynlink.Error e -> failwith (Dynlink.error_message e)
end;
assert(!Ita.loadedmodule <> None)
| _ -> failwith "unsupported input format"
let verify (module O : OPTIONS) =
load ();
let module TA = (val (O.get_ta ())) in
let ta = TA.model in
(* TA.print_timed_automaton stdout ta; *)
let module WO_tmp = (val !O.walk_order : O.PARTIAL_WO) in
let module ABS = (val !O.abstraction) in
let module INCL = (val !O.inclusion) in
......
open Uta
open Expression
type atomic_guard =
| GuardLeq of expression * expression
......
open Common
open TimedAutomaton
open Uta
open Varcontext
let print_path = ref false
......@@ -401,7 +401,7 @@ struct
and apply_single_transition =
fun ta -> fun (sloc, szone) -> fun global_invariant -> fun path ->
fun succs_list -> fun (source, guard, resets, target, target_arg) ->
assert(TA.is_state_equal sloc source);
assert(TA.DS.equal sloc source);
let result_zone = Dbm.to_fed (Dbm.copy szone) in
Fed.intersect result_zone guard;
if (Fed.is_empty result_zone) then
......
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
......
(**
* To run this test, first compile it as a .cmxs.
* The easiest way to achieve this is, from the toplevel directory of TiAMo,
* and after having compiled TiAMo, to run the command:
* ocamlbuild tests/compiled.cmxs
* To use the compiled model, run:
* ./tiamo reach _build/tests/compiled.cmxs
*)
module Test : Ita.TA =
struct
type state = int
type ta =
{
clocks : Varcontext.VarContext.t;
init : state;
}
let clocks t = t.clocks
let initial_state t = t.init
let hash_state s = s
let equal_state s1 s2 = s1 = s2
let is_target _ _ = false
let priority_compare s1 s2 = compare s1 s2
let transitions_from _ _ = []
let invariant _ _ = []
let is_urgent_or_committed _ _ = false
let rate_of_state _ _ = 1
let lubounds t s =
Array.make (Varcontext.VarContext.size t.clocks) 10,
Array.make (Varcontext.VarContext.size t.clocks) 10
let global_mbounds t =
Array.make (Varcontext.VarContext.size t.clocks) 10
let model =
let cl = Varcontext.VarContext.create () in
let _ = Varcontext.VarContext.add cl "c0" in ();
{
clocks = cl;
init = 0;
}
let string_of_state _ _ = "state"
let print_timed_automaton chan _ = Printf.fprintf chan "dummy TA\n"
end
let _ =
Ita.loadedmodule := Some (module Test)
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