Commit 4fcfe085 authored by Maximilien Colange's avatar Maximilien Colange

Rework the way the input model is loaded, to allow loading of custom compiled models.

parent 392b40b2
......@@ -87,13 +87,22 @@ sig
val global_mbounds : ta -> int array
(* to load a TA from a file *)
val from_file : string -> string -> ?scale:int -> ?enlarge:int -> unit -> ta
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
(*let loaded_model : TA.ta option ref = ref None*)
......@@ -7,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")
......@@ -36,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)
......
......@@ -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 Uppaalta.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,9 +263,26 @@ struct
])
end
(* 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 -> assert(!ofile <> ""); Dynlink.loadfile !ofile; assert(!Ita.loadedmodule <> None)
| _ -> failwith "unsupported input format"
let verify (module O : OPTIONS) tafile qfile =
let module TA = (val !O.ta_module) in
let ta = TA.from_file tafile qfile () in
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
......
......@@ -30,7 +30,9 @@ sig
val print_extended_state : out_channel -> timed_automaton -> (discrete_state * MDbm.Dbm.t) -> unit
val transition_to_string : timed_automaton ->
(discrete_state * UDbm.Dbm.t * ((clock_t * int) list) * discrete_state) -> string
val from_file : string -> string -> ?scale:int -> ?enlarge:int -> unit -> timed_automaton
(* the loaded model *)
val model : timed_automaton
end
module MBoundedAutomaton (TA : TIMED_AUTOMATON) =
......@@ -202,11 +204,12 @@ struct
out ")";
Buffer.contents buf
let from_file filename queryname ?scale:(scale=1) ?enlarge:(enlarge=0) () =
let model =
{
t = BareTA.from_file filename queryname ~scale:scale ~enlarge:enlarge ();
t = BareTA.model;
lu_tbl = DSHashtbl.create 1024;
m_tbl = DSHashtbl.create 1024;
}
end
......@@ -3,7 +3,7 @@ open Expression
open Printf
open Varcontext
module GenericUAutomaton : Ita.TA =
module GenericUAutomaton (Files : sig val tafile : string val qfile : string end) : Ita.TA =
struct
include Querybuilder
......@@ -1039,5 +1039,7 @@ struct
let ta = make_ta tafile qfile in
ta
let model = from_file Files.tafile Files.qfile ()
end
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