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

Merge branch 'master' into parser

parents 5ee65c44 b06a4b4e
......@@ -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
SUBDIRS = utap
INCLUDEDIR=@UDBML_ROOT@/udbml
UPPAAL_DIR=@UDBML_ROOT@/uppaal/lib
BUILDDIR=_build
OCAMLBUILD=ocamlbuild -use-ocamlfind -classic-display -build-dir $(BUILDDIR) @OCAMLBUILDFLAGS@
OCAMLBUILD=OCAMLPATH=@UDBML_ROOT@ ocamlbuild -use-ocamlfind -classic-display -build-dir $(BUILDDIR) @OCAMLBUILDFLAGS@
UTAP_INCLUDEDIR=@abs_top_srcdir@/utap/src
UTAP_LIB=@abs_top_srcdir@/utap/src/libutap.a
CXX_FLAGS=-xc++ -std=c++11 -fPIC -O3 -g -DNDEBUG @TIAMO_MACROS@ -I$(UTAP_INCLUDEDIR) -I@abs_top_srcdir@/src
OCAML_CXX_FLAGS=$(foreach i,$(CXX_FLAGS),-ccopt $i)
CXX_FLAGS=-std=c++11 @TIAMO_MACROS@ -I$(UTAP_INCLUDEDIR) -I@abs_top_srcdir@/src
XML_LINK_FLAGS=$(foreach i,$(XML_LIBS),-cclib $i)
SUFFIXES = .native .ml
all-local: tiamo
tiamo: src/main.native
cp $(BUILDDIR)/$< tiamo
src/main.native: src/timedAutomatonBuilder.o
.ml.native:
XML_LINK_FLAGS="$(XML_LIBS)" CXX_FLAGS="$(CXX_FLAGS)" $(OCAMLBUILD) -pkg udbml -lflags "-cclib -L$(UPPAAL_DIR) -cclib -ludbm" $@
.c.o:
CXX_FLAGS="$(CXX_FLAGS)" $(OCAMLBUILD) -pkg udbml $@
all-local:
$(OCAMLBUILD) -cflags "-cc g++ $(OCAML_CXX_FLAGS)" timedAutomatonBuilder.o
$(OCAMLBUILD) -cflags "-g -noassert -I $(INCLUDEDIR)" -lflags "$(INCLUDEDIR)/udbml.cmxa src/timedAutomatonBuilder.o $(UTAP_LIB) $(XML_LINK_FLAGS) -cclib -L$(INCLUDEDIR)" src/main.native
cp `readlink -f $(BUILDDIR)/src/main.native` tiamo
clean-local:
ocamlbuild -clean
$(OCAMLBUILD) -clean
rm -f tiamo
......@@ -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.
......@@ -40,6 +40,51 @@ AC_SUBST(XML_CONFIG)
AC_SUBST(XML_CFLAGS)
AC_SUBST(XML_LIBS)
OCAMLTAGS=""
dnl Check for debug flags
enableval=no
AC_MSG_CHECKING([whether to compile with debug info])
AC_ARG_ENABLE(debugging,
AS_HELP_STRING([--enable-debugging], [compile with debugging information]))
case "${enableval}" in
yes)
AC_MSG_RESULT(yes)
OPT_FLAGS="$OPT_FLAGS -g"
OCAMLTAGS="$OCAMLTAGS, debug"
;;
no)
AC_MSG_RESULT(no)
OPT_FLAGS="$OPT_FLAGS -O3"
;;
*)
AC_MSG_ERROR([bad value ${enableval} for --enable-debugging, needs yes or no])
;;
esac
enableval=no
AC_MSG_CHECKING([whether to enable checking of run-time assertions])
AC_ARG_ENABLE(assertions,
AS_HELP_STRING([--enable-assertions], [check run-time assertions]))
case "${enableval}" in
yes)
AC_MSG_RESULT(yes)
;;
no)
AC_MSG_RESULT(no)
AC_DEFINE(NDEBUG, 1, [Assertions are disabled when this is defined])
OPT_FLAGS="$OPT_FLAGS -DNDEBUG"
OCAMLTAGS="$OCAMLTAGS, noassert"
;;
*)
AC_MSG_ERROR([bad value ${enableval} --enable-assertions, needs yes or no])
;;
esac
CFLAGS="$OPT_FLAGS"
CPPFLAGS="$OPT_FLAGS"
AC_SUBST(OCAMLTAGS)
AC_SUBST(OCAMLBUILDFLAGS)
AC_CONFIG_SUBDIRS([utap])
......
open Ocamlbuild_plugin (* open the main API module *)
open Command
(* TODO find a cleaner way to retrieve these informations from the environment
* maybe the CXX_FLAGS should be given as arguments to the 'c++' tag,
* thus allowing per-file CXX flags.
*)
let cxx = "g++"
(**
* Default CXX flags:
* -xc++ to be sure to compile .c files as c++
* -fPIC to ensure position-independent code
*)
let cxx_flags =
let env_cxx =
try Some (Sys.getenv "CXX_FLAGS")
with | Not_found -> None
in
match env_cxx with
| None -> ["-xc++"; "-fPIC"]
| Some x -> ["-xc++"; "-fPIC"; x]
(* a helper function *)
(* prefix every c++ flags with -ccopt *)
let ocaml_cxx_flags = fun flags ->
let camlflags = List.flatten (List.map (fun opt -> ["-ccopt"; opt]) flags) in
atomize camlflags
let _ =
dispatch begin function
| After_rules ->
(* a custom noassert flag, only for compilation, not preprocessing *)
flag ["compile";"noassert"] (A"-noassert");
(* set proper compilation flags for c++ *)
flag ["c++"] (S[A"-cc"; A cxx; ocaml_cxx_flags cxx_flags]);
flag ["c++";"debug"] (ocaml_cxx_flags ["-g"]);
flag ["c++";"noassert"] (ocaml_cxx_flags ["-DNDEBUG"]);
(* hard-coding the C file and utap library seems the easiest way
* to avoid problems in object ordering at link time.
* Unfortunately, the dependency is not handled through ocamlbuild,
* but in the Makefile directly.
*)
let xml_flags =
try
Sys.getenv "XML_LINK_FLAGS"
with Not_found -> "-lxml2"
in
flag ["ocaml"; "link"; "native"]
(S[ P"src/timedAutomatonBuilder.o";
A"-cclib"; A("-L"^(Pathname.pwd / "utap/src"));
A"-cclib"; A"-lutap";
A"-cclib"; A xml_flags
]);
| _ -> ()
end
<*>: bin_annot
<*.cm{o,x}> or <main.native>: package(batteries), debug, custom
<*.c> or <*.cm{o,x}> or <main.native>: custom @OCAMLTAGS@
<main.native>: use_dynlink
<costs.ml>: pp(camlp4o pa_macro.cmo @TIAMO_MACROS@)
<timedAutomatonBuilder.c>: c++
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) -> (clocks c) ^ " < " ^ (string_of_int k)
| LEQ(c,k) -> (clocks c) ^ " <= " ^ (string_of_int k)
| GT(c,k) -> (clocks c) ^ " > " ^ (string_of_int k)
| GEQ(c,k) -> (clocks c) ^ " <= " ^ (string_of_int k)
| EQ(c,k) -> (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)] -> clocks c ^ " := " ^ (string_of_int k)
| (c,k) :: l -> 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
(* the number of clocks *)
(**
* WARNING: clocks are numbered from 1 to nb_clocks
* the clock of index 0 (reference clock) is implicit.
* DO NOT account for clock 0 in nb_clocks.
*)
val nb_clocks : ta -> int
(* clock names *)
val string_of_clock : ta -> int -> string
(* 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
(**
* 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 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
(** Printing functions *)
(* they are provided to help you pretty-print your custom automaton *)
(* Those functions need to know the clock names, so the first argument
* you must provide is a function that associates a name to a clock index
* Typical usage:
* let print_timed_automaton channel ta =
* ...print locations and stuff...
* Printf.printf "%s" (print_guard (string_of_clock ta) my_fancy_guard);
* ...print other stuff...
* Printf.printf "%s" (print_resets (string_of_clock ta) my_fancy_resets);
* ...print more stuff...
*)
(* a printer for an atomic guard *)
val print_ag : (int -> string) -> atomic_guard -> string
(* a printer for a guard *)
val print_guard : (int -> string) -> guard_t -> string
(* a printer for a list of resets *)
val print_resets : (int -> string) -> reset_t list -> string
(**
* 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
(* the number of clocks *)
(**
* WARNING: clocks are numbered from 1 to nb_clocks
* the clock of index 0 (reference clock) is implicit.
* DO NOT account for clock 0 in nb_clocks.
*)
val nb_clocks : ta -> int
(* clock names *)
val string_of_clock : ta -> int -> string
(* 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.
*)
val loadedmodule : (module TA) option ref
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
......@@ -98,7 +96,8 @@ struct
(Pwo : PARTIAL_WO)
= Pwo(TA.DS)(TA.MDbm)(COMP)(Best(TA)(COMP))
let bestcompare = ref (module BestCost : BEST)
let walk_order = ref (module Waiting.Walk_BFS : PARTIAL_WO)
let bestcompare = ref (module HighPrio : BEST)
type res_t = M.res_t
......@@ -120,6 +119,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,9 +140,29 @@ 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.");
( "-order",
Arg.String (function
| "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)
| _ -> raise (Arg.Bad "Invalid argument for option -order")),
" Sets the order in which the RG is explored:
\tBFS [default] Bread-First Search
\tDFS Depth-First Search
\tBBFS Best first (i.e. higher preference, see state variable \"preference\"), BFS on equivalent ones
\t With optimality analysis (tiamo optimal), also see -best option.
\tBDFS Best first (i.e. higher preference, see state variable \"preference\"), DFS on equivalent ones
\t With optimality analysis (tiamo optimal), also see -best option.
\tSBFS Smart BFS");
]
end
......@@ -140,7 +172,6 @@ struct
include Option_common(struct module Dbm = UDbm type res_t = bool end)
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
......@@ -149,24 +180,13 @@ struct
let arguments = Arg.align (common_args @
[
( "-order",
Arg.String (function
| "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
\tBFS [default] Bread-First Search
\tSBFS Smart BFS
\tDFS Depth-First Search");
( "-abstr",
Arg.String (function
| "LU" -> abstraction := (module Extra_LU : ITA_ABSTRACTION)
| "M" -> raise (Arg.Bad "M abstraction is currently not implemented")
| "ID" -> abstraction := (module ID_abstraction : ITA_ABSTRACTION)
| _ -> raise (Arg.Bad "Invalid argument for option -abstr")),
" Sets the abstraction to use.
" Sets the abstraction to use:
\tLU [default] LU (per discrete state) abstraction
\tM M abstraction (unimplemented)
\tID No abstraction (use with bounded automata, otherwise
......@@ -177,7 +197,7 @@ struct
| "simple" -> inclusion := (module Inclusion : ITA_INCLUSION)
| "sri" -> inclusion := (module Sri : ITA_INCLUSION)
| _ -> raise (Arg.Bad "Invalid argument for option -incl")),
" Sets the inclusion to use
" Sets the inclusion to use:
\tsimple [default] regular set inclusion
\tsri abstract inclusion (Z subset of abs_LU(Z'))");
......@@ -190,7 +210,6 @@ struct
include Option_common(struct module Dbm = PDbm type res_t = int end)
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
......@@ -199,31 +218,14 @@ struct
let arguments = Arg.align (common_args @
[
( "-order",
Arg.String (function
| "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)
| _ -> raise (Arg.Bad "Invalid argument for option -order")),
" Sets the order in which the RG is explored
\tBFS [default] Bread-First Search
\tDFS Depth-First Search
\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");
" Sets the way to chose the best candidate in waiting list (see 'BBSF' and 'BDFS' arguments of option -order):
\tpref [default] Choose the symbolic state with the highest preference, encoded in the variable \"preference\" of the model
\tcost Choose the symbolic state with the smallest minimal cost (i.e. the most promising one cost-wise)");
( "-incl",
Arg.String (function
......@@ -252,10 +254,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
......