Commit b86569d8 authored by mcolange's avatar mcolange

Initial commit.

parents
INSTALLATION NOTES
Requires Batteries
- install uppaal-dbm (say in uppaal_prefix)
- have udbm-config in PATH (typically export PATH=uppaal_prefix/bin:$PATH)
- install udbml
- install uppaal_parser
- install TiAMO
TODO: check whether uppaal_parser really depends on xml-light
TODO: make a global makefile that installs everything (especially udbml and uppaal_parser)
S .
S _build/
B _build/
PKG batteries uppaal_parser udbml
UPPAALINCLUDEDIR=$(shell udbm-config --inc)
UPPAALLIB=$(foreach i,$(shell udbm-config --libs),-cclib $i)
all:
ocamlbuild -use-ocamlfind -cflags '-cclib $(UPPAALINCLUDEDIR)' -lflags '-cclib -lstdc++ $(UPPAALLIB)' main.native
debug:
ocamlbuild -use-ocamlfind -cflags '-cclib $(UPPAALINCLUDEDIR)' -lflags '-cclib -lstdc++ $(UPPAALLIB)' main.byte
clean:
ocamlbuild -clean
<*>: bin_annot, package(batteries), package(udbml), package(uppaal_parser), debug
module StringSet = Set.Make(String)
module IntSet = Set.Make(
struct
let compare = Pervasives.compare
type t = int
end )
(** Clocks are given unique indices from 0 to nb_clocks -1.*)
type clock_t = int
module ClockSet = Set.Make(
struct
let compare = Pervasives.compare
type t = clock_t
end )
exception Found
exception DiagonalGuard
(*
type dbm_inequality_type = DBM_STRICT | DBM_WEAK
let string_of_ineq = function
|DBM_WEAK -> "<="
|DBM_STRICT -> "<"
(*
type extended_int = Infty | Int of int
let string_of_extint = function
|Int(a) -> string_of_int a
|Infty -> "INF"
let add_extint a b = match (a,b) with
Int(a),Int(b) -> Int(a+b)
|_,Infty -> Infty
|Infty,_ -> Infty
*)
let compare_inequality_type a b = match (a,b) with
DBM_STRICT, DBM_STRICT
| DBM_WEAK, DBM_WEAK -> 0
| DBM_STRICT, DBM_WEAK -> -1
| DBM_WEAK , DBM_STRICT -> 1
*)
open Batteries
open Printf
type log_t = Info | Debug | Warning | Error | Fatal
let log_level = ref Debug
let set_level level = log_level := level
let log_err_channel = stderr
let log_regular_channel = stdout
let logf level s f =
(match level with
| Error ->
Printf.fprintf log_err_channel "[ERROR] ";
Printf.fprintf log_err_channel s f
| Fatal ->
Printf.fprintf log_err_channel "[FATAL] ";
Printf.fprintf log_err_channel s f;
exit(-1)
| Warning ->
if ( !log_level = Debug || !log_level = Warning ) then
(
Printf.fprintf log_err_channel "[WARNING] ";
Printf.fprintf log_err_channel s f
)
| Info ->
if ( !log_level = Info || !log_level = Debug || !log_level = Warning ) then
(
Printf.fprintf log_regular_channel "[INFO] ";
Printf.fprintf log_regular_channel s f
)
| Debug ->
if ( !log_level = Debug ) then
(
Printf.fprintf log_regular_channel "[DEBUG] ";
Printf.fprintf log_regular_channel s f;
)
);
flush log_err_channel;
flush log_regular_channel
let fatal s =
logf Fatal "%s" s
let info s =
logf Info "%s" s
let warning s =
logf Warning "%s" s
let infof f s =
logf Info f s
let warningf f s =
logf Warning f s
let fatalf f s =
logf Fatal f s
let debug s =
logf Debug "%s" s
let debugf f s =
logf Debug f s
let log level s =
logf level "%s" s
(** Does it belong to log.ml, or rather to a stats.ml? *)
module SearchStatistics =
struct
let counter_visited = ref 0
let counter_gamma = ref 0
let counter_acceleration = ref 0
(** Number of iterations of the binary search *)
let counter_bsiterations = ref 0
let increment_visited () = incr(counter_visited)
let increment_gamma () = incr(counter_gamma)
let increment_acceleration () = incr(counter_acceleration)
let reset_counters () =
counter_visited := 0;
counter_gamma := 0;
counter_acceleration := 0;
counter_bsiterations := 0
(*
let print_statistics chan mode =
match mode with
Options.ExactReachability
| Options.Verifix ->
fprintf chan "[INF] Search Statistics:\n";
fprintf chan "[INF] Visited states: %d\n" !counter_visited
|Options.RobustReachability ->
fprintf chan "[INF] Search Statistics:\n";
fprintf chan "[INF] Visited states: %d\n[INF] Expanded gamma cycles: %d (%d new states)\n" !counter_visited !counter_acceleration !counter_gamma
*)
end
open Batteries
open Options
open Printf
open Reachability
open TimedAutomaton
open Udbml
(** For Arg.align to properly display help messages, do not forget to make them
* start with a space.
*)
let arguments = Arg.align
[ ( "-order",
Arg.String (function
| "DFS" -> Options.walk_order := (module Walk_DFS : WALK_ORDER)
| "BFS" -> Options.walk_order := (module Walk_BFS : WALK_ORDER)
| _ -> raise (Arg.Bad "Invalid argument for option -order")),
" Sets the order in which the RG is explored
\tBFS [default] Breadth-First Search
\tDFS Depth-First Search");
( "-abstr",
Arg.String (function
| "LU" -> Options.abstraction := (module Extra_LU(Uautomaton) : UTA_ABSTRACTION)
| "M" -> raise (Arg.Bad "M abstraction is currently not implemented")
| "ID" -> Options.abstraction := (module ID_abstraction(Uautomaton) : UTA_ABSTRACTION)
| _ -> raise (Arg.Bad "Invalid argument for option -abstr")),
" Sets the abstraction to use.
\tLU [default] LU abstraction
\tM M abstraction (unimplemented)
\tID No abstraction");
( "-incl",
Arg.String (function
| "simple" -> () (*(Options.inclusion := module Inclusion(Uautomaton) : UTA_INCLUSION)*)
| "sri" -> Options.inclusion := (module Sri(Uautomaton) : UTA_INCLUSION)
| _ -> raise (Arg.Bad "Invalid argument for option -incl")),
" Sets the inclusion to use
\tsimple [default] set inclusion
\tsri abstract inclusion (Z subset of abs_LU(Z'))")
]
let tafile = ref ""
let qfile = ref ""
let anon_arguments arg =
if (Filename.check_suffix arg ".xml") then (
tafile := arg
)
else if (Filename.check_suffix arg ".q") then (
qfile := arg
)
else (
Log.fatalf "File extension not recognized: %s\n" arg;
raise (Arg.Bad "Unrecognized file extension")
)
let usage =
"This is @@@@@@@.
Only reachability is implemented for now.
"
let execute tafile qfile =
let ta = Uautomaton.from_file tafile qfile () in
(* Uautomaton.print_timed_automaton BatIO.stdout ta;*)
let module WO = (val !Options.walk_order : WALK_ORDER) in
let module Abs = (val !Options.abstraction : UTA_ABSTRACTION) in
let module Incl = (val !Options.inclusion : UTA_INCLUSION) in
let module Reach = Reachability(Uautomaton)(WO)(Abs)(Incl) in
match (Reach.reach ta) with
| true -> Log.info "reachable!\n"
| false -> Log.info "not reachable...\n"
let main() =
Arg.parse arguments anon_arguments usage;
if ( !tafile = "" ) then
(
Log.fatal "No input files\n"
);
if ( !qfile = "" ) then
(
qfile := (Filename.chop_suffix !tafile ".xml") ^ ".q";
Log.warningf "Guessing query file: %s\n" !qfile
);
execute !tafile !qfile;
Gc.print_stat stdout
let _ = main ()
open Reachability
open TimedAutomaton
type ta_discrete = Uautomaton.timed_automaton * Uautomaton.discrete_state
module type UTA_ABSTRACTION = ABSTRACTION with type arg_t = ta_discrete
module type UTA_INCLUSION = INCLUSION with type arg_t = ta_discrete
let walk_order = ref (module Walk_BFS : WALK_ORDER)
let abstraction = ref (module Extra_LU(Uautomaton) : UTA_ABSTRACTION)
let inclusion = ref (module Inclusion(Uautomaton) : UTA_INCLUSION)
open Batteries
open Common
open TimedAutomaton
open Udbml
open Uta
module LUCache (TA : TIMED_AUTOMATON) =
struct
let lu_memo = Hashtbl.create 100
let lu_bounds ta loc =
try Hashtbl.find lu_memo (ta, loc)
with Not_found -> (
let dim = VarContext.size (TA.clocks ta) in
let (larr, uarr) =
(Array.make dim 0,
Array.make dim 0)
in
TA.lu_bounds ta loc larr uarr;
Hashtbl.add lu_memo (ta, loc) (larr, uarr);
(larr, uarr)
)
end
(** An abstract type for zone abstractions *)
module type ABSTRACTION =
sig
(* the abstract type for a possible additional argument *)
type arg_t
val extrapolate : Dbm.t -> arg_t -> unit
end
(** ID abstraction
*)
module ID_abstraction (TA : TIMED_AUTOMATON) :
ABSTRACTION with type arg_t = TA.timed_automaton * TA.discrete_state =
struct
type arg_t = TA.timed_automaton * TA.discrete_state
let extrapolate _ _ = ()
end
(** LU abstraction
*)
module Extra_LU (TA : TIMED_AUTOMATON) :
ABSTRACTION with type arg_t = TA.timed_automaton * TA.discrete_state =
struct
type arg_t = TA.timed_automaton * TA.discrete_state
module LUC = LUCache(TA)
let extrapolate zone (ta, loc) =
let (lbounds, ubounds) = LUC.lu_bounds ta loc in
Dbm.extrapolate_lu_bounds zone lbounds ubounds
end
(** An abstract type for zone inclusion test *)
(** In fact the inclusion module should take responsibility of the storage of
* visited zones, as search for a stored zone that compares favorably to a
* newly encountered one is crucial performance-wise.
*)
module type INCLUSION =
sig
(* the abstract type for a possible additional argument *)
type arg_t
val inclusion : arg_t -> Dbm.t -> Dbm.t -> bool
end
(** Vanilla inclusion *)
module Inclusion (TA : TIMED_AUTOMATON) :
INCLUSION with type arg_t = TA.timed_automaton * TA.discrete_state =
struct
type arg_t = TA.timed_automaton * TA.discrete_state
let inclusion _ = Dbm.leq
end
(** Smart inclusion test, based on (insert reference here)
* According to Theorem 32, we have the following equivalence
* (L and U are global, not per location)
* not (Z \subseteq a_{LU}(Z'))
* iff \exists x,y such that Z_{x,0} \geq (\leq, - U_x)
* and Z'_{x,y} < Z_{x,y}
* and Z'_{x,y} + (<, - L_y) < Z_{x,0}
*)
module Sri (TA : TIMED_AUTOMATON) :
INCLUSION with type arg_t = TA.timed_automaton * TA.discrete_state =
struct
type arg_t = TA.timed_automaton * TA.discrete_state
module LUC = LUCache(TA)
let inclusion (ta, loc) z1 z2 =
let (lbounds, ubounds) = LUC.lu_bounds ta loc in
Dbm.closure_leq lbounds ubounds z1 z2
end
(** An abstract type for the walk order of a graph *)
(** TODO Operations returning unit are very imperative style...
* but efficiency should prevail
*)
module type WALK_ORDER =
sig
type 'a t
val create : unit -> 'a t
val mark : ('a -> Dbm.t -> Dbm.t -> bool) -> 'a t -> 'a * Dbm.t -> unit
val is_marked : ('a -> Dbm.t -> Dbm.t -> bool) -> 'a t -> 'a * Dbm.t -> bool
val add : 'a t -> 'a * Dbm.t -> unit
val get_next : 'a t -> 'a * Dbm.t
val finished : 'a t -> bool
end
(** An abstract type for a container to store the nodes yet to explore.
* This implements the order in which nodes are explored.
*)
module type WAIT_CONTAINER =
sig
type 'a t
val create : unit -> 'a t
val push : 'a -> 'a t -> unit
val pop : 'a t -> 'a
val is_empty : 'a t -> bool
val length : 'a t -> int
end
(** Builds an effective walk order, given a WAIT_CONTAINER and an INCLUSION.
*)
module Walk_Order (Cont : WAIT_CONTAINER) : WALK_ORDER =
struct
type dbm_list = Dbm.t list ref
type 'a t = ('a, dbm_list) Hashtbl.t * ('a * Dbm.t) Cont.t
let create () = (Hashtbl.create 1000, Cont.create ())
let find_or_add : ('a, dbm_list) Hashtbl.t -> 'a -> dbm_list =
fun h -> fun x ->
try Hashtbl.find h x
with Not_found ->
(* Printf.printf "%d discrete states\n" (Hashtbl.length h);*)
let y = ref [] in
Hashtbl.add h x y;
y
let mark comp (v, _) (l, z) =
let bucket = find_or_add v l in
let is_incomp x = not (comp l x z) in
bucket := z :: (List.filter is_incomp !bucket)
let is_marked comp (v, _) (l, z) =
let bucket = find_or_add v l in
let is_included x = comp l z x in
let res = List.exists is_included !bucket in
(* if (res) then (
Printf.printf "marked!\n";
); *)
res
let add (_, t) s = Cont.push s t
let get_next (_, t) = Cont.pop t
let finished (_, t) =
(* Printf.printf "%d waiting\n" (Cont.length t); *)
Cont.is_empty t
end
module Walk_DFS = Walk_Order (Stack)
module Walk_BFS = Walk_Order (Queue)
(** Other walk orders will probably require some knowledge about the states,
* and will thus be functors of TIMED_AUTOMATON *)
module TA_RG_WALK =
functor (TA : TIMED_AUTOMATON) ->
functor (WO : WALK_ORDER) ->
functor (ABS : ABSTRACTION
with type arg_t = TA.timed_automaton * TA.discrete_state) ->
functor (COMP : INCLUSION
with type arg_t = TA.timed_automaton * TA.discrete_state) ->
struct
(** Auxiliary function that computes the list of successors of an
* extended state.
* Not intended to be called from the outside.
* TODO is returning succs in a list the most efficient way?
* TODO are committed/urgent states properly accounted for?
*)
let succ_zone ta (loc, zone) =
let apply_transition (sloc, szone) trans =
let (source, guard, resets, target) = TA.transition_fields ta trans in
assert(TA.is_state_equal ta sloc source);
let result_zone = Dbm.copy szone in
Dbm.intersect result_zone guard;
if (Dbm.is_empty result_zone) then
None
else (
ClockSet.iter (fun c -> Dbm.update_value result_zone c 0) resets;
if (not (TA.is_urgent_or_committed ta target)) then (
Dbm.up result_zone );
Dbm.intersect result_zone (TA.invariant_of_discrete_state ta target);
if (Dbm.is_empty result_zone) then
None
else (
ABS.extrapolate result_zone (ta, target);
(*
Printf.printf "Computed transition\n";
TA.print_extended_state stdout ta (loc, zone);
Printf.printf " -> ";
TA.print_extended_state stdout ta (target, result_zone);
Printf.printf "\n";
*)
Some (target, result_zone)
)
)
in
let large_zone = Dbm.copy zone in
Dbm.intersect large_zone (TA.invariant_of_discrete_state ta loc);
let fold l t =
match apply_transition (loc, large_zone) t with
| Some x -> x :: l
| None -> l
in
List.fold_left fold [] (TA.transitions_from ta loc)
(* a counter of stored states *)
let nb_states = ref 0
(* Auxiliary recursive function, not to call from the outside *)
(* TODO how can we early return?
* result should belong to an ordered set S,
* res0 should be inf S and update_result should be increasing.
* if S has a maximal element, we can compare result to it
*)
let rec walk_aux dbm_comp wot succs update_result result =
if (WO.finished wot) then
result
else (
let state = WO.get_next wot in
let new_res = update_result result state in
if (not (WO.is_marked dbm_comp wot state)) then (
assert (not (WO.is_marked dbm_comp wot state));
WO.mark dbm_comp wot state;
nb_states := !nb_states + 1;
if ((!nb_states mod 1000) = 0) then (
Printf.printf "we have seen %d states\r" !nb_states;
flush stdout
);
let add s =
if (not (WO.is_marked dbm_comp wot s)) then
WO.add wot s
in
List.iter add (succs state)
);
walk_aux dbm_comp wot succs update_result new_res
)
(* The real function to call *)
let walk ta update_result res0 =
let dbm_comp loc = COMP.inclusion (ta, loc) in
let init = TA.initial_extended_state ta in
let wot = WO.create () in
WO.add wot init;
walk_aux dbm_comp wot (succ_zone ta) update_result res0
end
module Reachability =
functor (TA : TIMED_AUTOMATON) ->
functor (WO : WALK_ORDER) ->
functor (ABS : ABSTRACTION
with type arg_t = TA.timed_automaton * TA.discrete_state) ->
functor (COMP : INCLUSION
with type arg_t = TA.timed_automaton * TA.discrete_state) ->
struct
module Walker = TA_RG_WALK(TA)(WO)(ABS)(COMP)
exception Found
let reach ta =
let update_result = function
| true -> raise Found
| false -> fun (l, _) ->
if (TA.is_target ta l) then
raise Found
else
false
in
let result =
try
Walker.walk ta update_result false
with Found -> true
in
Printf.printf "\n%d states explored\n" !Walker.nb_states;
result
end
This diff is collapsed.
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