Commit 36d7d2a2 authored by Maximilien Colange's avatar Maximilien Colange

Merge commit master into packaging

parents 7b2db400 54338713
......@@ -3,5 +3,5 @@ S uppaal_parser
B _build/src/
B _build/uppaal_parser/
PKG batteries udbml xml-light
PKG udbml xml-light
B @UDBML_ROOT@/udbml
......@@ -2,14 +2,14 @@ TiAMo (Timed Automata Model-checker)
M. Colange
O. Sankur
This tools is also based on the DBM library from Uppaal and on the timed automata parser library from Uppaal.
This tool is also based on the DBM library from Uppaal and on the timed automata parser library from Uppaal.
The name of the authors and contributors of these libraries can be found in their respective folders.
Both libraries have been adapted by M. Colange (essentially to drop dependency on Boost, and to work with C++11).
INSTALLATION NOTES
Requires ocaml, batteries, ocamlbuild, camlp4 (you can obtain them through opam)
Requires ocaml, ocamlbuild, camlp4 (you can obtain them through opam).
Requires libxml2 (for the parser).
Requires a C++11-compatible compiler.
Tested (and works fine) with gcc-4.7, gcc-4.8, gcc-4.9 and gcc-5 (5.3.0).
......@@ -17,5 +17,5 @@ Requires a C++11-compatible compiler.
- install udbml (see github.com/osankur/udbml.git)
- install TiAMo
The script 'build.sh' retrieves udbml, compiles and installing it (locally), then compiles
The script 'build.sh' retrieves udbml, compiles and installs it (locally), then compiles
TiAMo. Simply run this script, or modify it if you want a custom installation.
# AC_INIT (package, version, [bug-report], [tarname])
AC_INIT(tiamo,0.1,[Maximilien.Colange@lsv.fr])
AC_INIT(tiamo,0.2,[Maximilien.Colange@lsv.fr])
# We use automake to build makefiles
AM_INIT_AUTOMAKE([foreign -Wall, subdir-objects])
......
<*>: 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 Reachability
module Best_DFS : WAIT_CONTAINER =
functor (Elem : Set.OrderedType) ->
struct
type t = Elem.t list ref
let create () = ref []
let push x l =
l := List.merge Elem.compare [x] !l
let pop l =
let res = List.hd !l in
l := List.tl !l;
res
let is_empty l = !l = []
let length l = List.length !l
end
module Best_BFS : WAIT_CONTAINER =
functor (Elem : Set.OrderedType) ->
struct
type t = Elem.t list ref
let create () = ref []
let push x l =
l := List.merge Elem.compare !l [x]
let pop l =
let res = List.hd !l in
l := List.tl !l;
res
let is_empty l = !l = []
let length l = List.length !l
end
module Deque =
struct
exception Empty
......@@ -93,6 +52,7 @@ end
module WSTS_WO (Key : Hashtbl.HashedType)
(BDbm : Dbm.BIG_IDBM)
(COMP : INCLUSION with type dbm_t := BDbm.Dbm.t)
(Best : WaitOrderedType with type t = Key.t * BDbm.Dbm.t * COMP.arg_t * Key.t _path)
: WALK_ORDER with type key = Key.t and type dbm_t := BDbm.Dbm.t and type arg_t := COMP.arg_t =
struct
......@@ -171,80 +131,4 @@ struct
flush stdout
end
(* a non-polymorphimic Stack. I think it could be better *)
module WOStack (Elem : Set.OrderedType) =
struct
type t = Elem.t Stack.t
let create = Stack.create
let push = Stack.push
let pop = Stack.pop
let is_empty = Stack.is_empty
let length = Stack.length
end
module WOQueue (Elem : Set.OrderedType) =
struct
end
(* WIP *)
(* Best BFS: insert an element x before y as soon as x < y
* Best DFS: insert an element x before y as soon as x <= y
*)
module MyList : WAIT_CONTAINER =
functor (Elem : Set.OrderedType) ->
struct
exception Empty
type cell = { content : Elem.t; mutable next : cell; }
type t = { mutable length : int; mutable tail : cell; }
let create () =
{ length = 0; tail = Obj.magic None; }
let push x l =
if l.length = 0 then (
let rec cell = {
content = x;
next = cell;
}
in
l.length <- 1;
l.tail <- cell
) else (
let head = l.tail.next in
let rec aux c =
(* if x < c.content, insert [Best BFS] *)
if (Elem.compare x c.next.content <= 0) then
let newcell = { content = x; next = c.next; } in
c.next <- newcell;
(* if c is the last element of the list *)
else if (c.next == head) then
let newcell = { content = x; next = head; } in
c.next <- newcell;
l.tail <- newcell;
else
aux c.next
in
l.length <- l.length + 1;
aux l.tail
)
let pop l =
if l.length = 0 then raise Empty;
let res = l.tail.next.content in
if l.length = 1 then (
l.tail <- Obj.magic None
) else (
l.tail.next <- l.tail.next.next
);
l.length <- l.length - 1;
res
let is_empty l = l.length = 0
let length l = l.length
end
module Walk_Best = Walk_Order(MyList)
open Querybuilder
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)
......@@ -60,20 +65,10 @@ let set_command arg =
) else anon_arguments arg
let main() =
(* Printexc.record_backtrace true; *)
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,20 +8,22 @@ 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) ->
functor (Dbm : BIG_IDBM with type dbm_t = t) ->
functor (COMP : INCLUSION with type dbm_t := Dbm.Dbm.t) ->
WALK_ORDER with type key = Key.t
and type dbm_t := Dbm.Dbm.t
and type arg_t := COMP.arg_t
functor (Best : WaitOrderedType with type t = Key.t * Dbm.Dbm.t * COMP.arg_t * Key.t _path) ->
WALK_ORDER with type key = Key.t
and type dbm_t := Dbm.Dbm.t
and type arg_t := COMP.arg_t
val walk_order : (module PARTIAL_WO) ref
module ITA_WO (TA : ITA)
(COMP : INCLUSION with type dbm_t := TA.MDbm.Dbm.t and module TA = TA)
(Best : BEST)
(Pwo : PARTIAL_WO) :
WALK_ORDER with type key = TA.discrete_state
and type dbm_t := TA.MDbm.Dbm.t
......@@ -37,6 +39,8 @@ sig
val abstraction : (module ITA_ABSTRACTION) ref
val inclusion : (module ITA_INCLUSION) ref
val bestcompare : (module BEST) ref
type res_t
module type MC_FUNCTOR =
......@@ -74,12 +78,11 @@ struct
functor (Key : Hashtbl.HashedType) ->
functor (Dbm : BIG_IDBM with type dbm_t = M.Dbm.dbm_t) ->
functor (COMP : INCLUSION with type dbm_t := Dbm.Dbm.t) ->
WALK_ORDER with type key = Key.t
and type dbm_t := Dbm.Dbm.t
and type arg_t := COMP.arg_t
functor (Best : WaitOrderedType with type t = Key.t * Dbm.Dbm.t * COMP.arg_t * Key.t _path) ->
WALK_ORDER with type key = Key.t
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
......@@ -89,9 +92,12 @@ struct
module ITA_WO (TA : ITA)
(COMP : INCLUSION with type dbm_t := TA.MDbm.Dbm.t and module TA = TA)
(Best : BEST)
(Pwo : PARTIAL_WO)
= Pwo(TA.DS)(TA.MDbm)(COMP)
= Pwo(TA.DS)(TA.MDbm)(COMP)(Best(TA)(COMP))
let bestcompare = ref (module BestCost : BEST)
type res_t = M.res_t
module type MC_FUNCTOR =
......@@ -112,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 =
[
......@@ -120,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.");
]
......@@ -132,7 +151,7 @@ struct
include Option_common(struct module Dbm = UDbm type res_t = bool end)
let walk_order = ref (module Walk_BFS : PARTIAL_WO)
let walk_order = ref (module Waiting.Walk_BFS : PARTIAL_WO)
let abstraction = ref (module Extra_LU : ITA_ABSTRACTION)
let inclusion = ref (module Inclusion : ITA_INCLUSION)
let initial_value = ref false
......@@ -143,8 +162,8 @@ struct
[
( "-order",
Arg.String (function
| "DFS" -> walk_order := (module Walk_DFS : PARTIAL_WO)
| "BFS" -> walk_order := (module Walk_BFS : PARTIAL_WO)
| "DFS" -> walk_order := (module Waiting.Walk_DFS : PARTIAL_WO)
| "BFS" -> walk_order := (module Waiting.Walk_BFS : PARTIAL_WO)
| "SBFS" -> walk_order := (module Best_wait.WSTS_WO : PARTIAL_WO)
| _ -> raise (Arg.Bad "Invalid argument for option -order")),
" Sets the order in which the RG is explored
......@@ -182,27 +201,40 @@ struct
include Option_common(struct module Dbm = PDbm type res_t = int end)
let walk_order = ref (module Walk_BFS : PARTIAL_WO)
let walk_order = ref (module Waiting.Walk_BFS : PARTIAL_WO)
let abstraction = ref (module ID_abstraction : ITA_ABSTRACTION)
let inclusion = ref (module Inclusion : ITA_INCLUSION)
let initial_value = ref Dbm.PDbm.Dbm.infty
module MC = OptReachability
let arguments = Arg.align (common_args @
[
( "-order",
Arg.String (function
| "DFS" -> walk_order := (module Walk_DFS : PARTIAL_WO)
| "BFS" -> walk_order := (module Walk_BFS : PARTIAL_WO)
| "BFS" -> walk_order := (module Waiting.Walk_BFS : PARTIAL_WO)
| "DFS" -> walk_order := (module Waiting.Walk_DFS : PARTIAL_WO)
| "BBFS" -> walk_order := (module Waiting.BBFS : PARTIAL_WO)
| "BDFS" -> walk_order := (module Waiting.BDFS : PARTIAL_WO)
| "BBFST" -> walk_order := (module Waiting.BBFST : PARTIAL_WO)
| "BDFST" -> walk_order := (module Waiting.BDFST : PARTIAL_WO)
| "SBFS" -> walk_order := (module Best_wait.WSTS_WO : PARTIAL_WO)
| "Best" -> walk_order := (module Best_wait.Walk_Best : PARTIAL_WO)
| _ -> raise (Arg.Bad "Invalid argument for option -order")),
" Sets the order in which the RG is explored
\tBFS [default] Bread-First Search
\tSBFS Smart BFS
\tDFS Depth-First Search
\tBest The waiting state with the best cost so far is picked first.");
\tBBFS Best first (see option -best), BFS on equivalent ones
\tBDFS Best first (see option -best), DFS on equivalent ones
\tSBFS Smart BFS");
( "-best",
Arg.String (function
| "cost" -> bestcompare := (module BestCost : BEST)
| "pref" -> bestcompare := (module HighPrio : BEST)
| _ -> raise (Arg.Bad "Invalid argument for option -best")),
" Sets the way to chose the best candidate in waiting list (see 'BBSF' and 'BDFS' arguments of option -order)
\tcost [default] Choose the symbolic state with the smallest minimal cost (i.e. the most promising one cost-wise)
\tpref Choose the symbolic state with the highest priority, encoded in the variable \"preference\" of the model");
( "-incl",
Arg.String (function
......@@ -231,14 +263,40 @@ 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
let module WO = O.ITA_WO(TA)(struct include INCL(TA) module TA = TA end)(WO_tmp) in
let module B = (val !O.bestcompare) in
let module WO = O.ITA_WO(TA)(struct include INCL(TA) module TA = TA end)(B)(WO_tmp) in
let module Verifier = O.MC(TA)(ABS(TA))(INCL(TA))(WO) in
let result = Verifier.reach ta !O.initial_value in
Verifier.to_string ta result
......
#include <utap/abstractbuilder.h>
#include <utap/expressionbuilder.h>
class QueryBuilder : public UTAP::AbstractBuilder
class QueryBuilder : public UTAP::ExpressionBuilder
{
public:
// constructor
explicit QueryBuilder(UTAP::TimedAutomataSystem *ta)
: _system(ta) {}
: ExpressionBuilder(ta) {}
// destructor
virtual ~QueryBuilder() {}
void exprDot(const char *) override;
void exprId(const char *) override;
void exprNat(int32_t) override;
void exprUnary(Constants::kind_t) override;
void exprBinary(Constants::kind_t) override;
void property() override {}
// TODO dummy implems of pure virtual methods
void addPosition(uint32_t position, uint32_t offset, uint32_t line, std::string path) override {}
void handleError(std::string) override {}
void handleWarning(std::string) override {}
void
exprProbaQuantitative(int,Constants::kind_t,bool=false) override
{
......@@ -42,154 +32,10 @@ public:
throw "simulation is not supported";
}
CAMLprim value getResult() const
const expression_t &getResult() const
{
CAMLparam0();
CAMLreturn(caml_callback(*caml_named_value("cb_qb_get_query"), Val_unit));
assert(getExpressions().size() == 1);
return getExpressions()[0];
}
private:
UTAP::TimedAutomataSystem * _system;
std::string _proc_name;
};
void
QueryBuilder::exprId(const char *id)
{
// an identifier is
// - either a global variable
// - or a local variable or location, in which case it is followed by a call to `exprDot`
CAMLparam0();
CAMLlocal1(tmp);
tmp = caml_callback(*caml_named_value("cb_global_var_index"), caml_copy_string(id));
// if it is a global variable, its index is positive
if (Int_val(tmp) >= 0)
{
caml_callback(*caml_named_value("cb_qb_push_variable"), tmp);
}
else
{
// it is not a global variable, store it for the call to `exprDot` to follow
_proc_name = std::string(id);
}
CAMLreturn0;
}
void
QueryBuilder::exprDot(const char *localName)
{
CAMLparam0();
CAMLlocal1(tmp);
tmp = Val_int(-1);
size_t procId = 0;
for (auto &process : _system->getProcesses())
{
if (! process.uid.getName().compare(_proc_name))
{
size_t locId = 0;
for (auto &state : process.templ->states)
{
// if a location with the appropriate name is found
if (! state.uid.getName().compare(localName))
{
caml_callback2(*caml_named_value("cb_qb_make_location"),
Val_int(procId),
Val_int(locId));
break;
}
++locId;
}
// localName is not a location
if (locId == process.templ->states.size())
{
tmp = caml_callback2(*caml_named_value("cb_local_var_index"),
Val_int(procId),
caml_copy_string(localName));
assert(Int_val(tmp) >= 0);
caml_callback(*caml_named_value("cb_qb_push_variable"), tmp);
}
break;
}
++procId;
}
assert(procId < _system->getProcesses().size());
// reset _proc_name to avoid pollution
_proc_name = "";
CAMLreturn0;
}
void
QueryBuilder::exprNat(int32_t n)
{
caml_callback(*caml_named_value("cb_qb_push_constant"), Val_int(n));
}
void
QueryBuilder::exprUnary(Constants::kind_t op)
{
switch (op)
{
case Constants::EF:
// nothing to do
break;
default:
// other unary ops are not supported
throw "unsupported unary op in query";
break;
}