Commit 1d795a44 authored by Ocan Sankur's avatar Ocan Sankur

Added the CEGAR module though there is debugging left to do

parent 3166941c
S src/
S uppaal_parser
B _build/src/
B _build/uppaal_parser/
PKG udbml xml-light
B /home/osankur/ulb/tiamo/local/udbml
......@@ -3,5 +3,5 @@ S uppaal_parser
B _build/src/
B _build/uppaal_parser/
PKG udbml xml-light
PKG udbml xml-light batteries
B @UDBML_ROOT@/udbml
<*>: bin_annot
<*>: bin_annot, package(batteries)
<src>: include
<uppaal_parser>: include
......@@ -166,7 +166,7 @@ struct
KeyHashtbl.add h x y;
y
let add_to_waiting comp (passed, waiting) s =
let add_to_waiting str_of_state comp (passed, waiting) s =
let (l, z, a) = State.get s in
let bucket = find_or_add passed l in
if (not (List.exists (fun x -> let (_,z',_) = State.get x in comp a z z') !bucket)) then
......@@ -176,7 +176,7 @@ struct
let is_incomp x =
let (_,z',_) = State.get x in
if comp a z' z then (
State.subsume x;
State.subsume str_of_state x;
if not (State.is_waiting x) then (
State.set_rank s (max (State.rank s) (1 + State.get_rank_max x));
);
......@@ -235,6 +235,6 @@ struct
Printf.printf "cleaning: shrink from %d states to %d states stored\n" !size_before !size_after;
Printf.printf "still %d states waiting for treatment\n" (Cont.length waiting);
flush stdout
end
end
This diff is collapsed.
......@@ -48,7 +48,7 @@ sig
val to_dbm : t -> dbm_t list
val iter : t -> (dbm_t -> unit) -> unit
val map : t -> (dbm_t -> unit) -> t
val map : t -> (dbm_t -> dbm_t) -> t
val free_clock : t -> Udbml.Basic_types.cindex_t -> unit
val intersect_dbm : t -> Udbml_unpriced.Dbm.t -> unit
......@@ -117,7 +117,7 @@ struct
let map t f =
let newf = create (dimension t) in
iter t (fun z -> f z; add_dbm newf z);
iter t (fun z -> add_dbm newf (f z));
newf
end
......@@ -176,7 +176,7 @@ struct
let map t f =
let newf = create (dimension t) in
iter t (fun z -> f z; add_dbm newf z);
iter t (fun z -> add_dbm newf (f z));
newf
end
......
......@@ -7,7 +7,7 @@ sig
type arg_t
type dbm_t
val extrapolate : dbm_t -> arg_t -> unit
val extrapolate : arg_t -> dbm_t -> dbm_t
end
(** ID abstraction
......@@ -18,7 +18,7 @@ module ID_abstraction (TA : TIMED_AUTOMATON) :
struct
type arg_t = TA.timed_automaton * TA.discrete_state
let extrapolate _ _ = ()
let extrapolate _ z = z
end
(** LU abstraction
......@@ -29,9 +29,12 @@ module Extra_LU (TA : TIMED_AUTOMATON with type MDbm.dbm_t = Udbml_unpriced.Dbm.
struct
type arg_t = TA.timed_automaton * TA.discrete_state
let extrapolate zone (ta, loc) =
let extrapolate (ta, loc) zone =
(** FIXME Make a coherent interface: either no extrapolate function
modifies the given DBM or all of them do *)
let (lbounds, ubounds) = TA.lu_bounds ta loc in
Udbml_unpriced.Dbm.extrapolate_lu_bounds zone lbounds ubounds
Udbml_unpriced.Dbm.extrapolate_lu_bounds zone lbounds ubounds;
zone
end
open Varcontext
open Batteries
(**
* 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 ==.
......@@ -93,6 +93,9 @@ sig
(* this required if you want to bound the automaton *)
val global_mbounds : ta -> int array
val guard_constants : ta -> int array array array
val ocan : string
(* to load a TA from a file *)
val model : ta
......
(**
* 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
......@@ -58,6 +58,7 @@ let set_command arg =
(match arg with
| "reach" -> mc_module := (module Unpriced : OPTIONS)
| "optimal" -> mc_module := (module Priced : OPTIONS)
| "cegar" -> mc_module := (module Cegar : OPTIONS);
| _ as s -> raise (Arg.Bad ("unknown command " ^ s))
);
let module MC = (val !mc_module) in
......
open Inclusion
open Extrapolation
open Reachability
open Cegar
open TimedAutomaton
open Waiting
open SearchState
......@@ -153,7 +154,7 @@ struct
| "DFS" -> walk_order := (module Walk_DFS : PARTIAL_WO)
| "BBFS" -> walk_order := (module BBFST : PARTIAL_WO)
| "BDFS" -> walk_order := (module BDFST : PARTIAL_WO)
| "SBFS" -> walk_order := (module Best_wait.WSTS_WO : 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
......@@ -255,6 +256,42 @@ struct
])
end
module Cegar =
struct
type t = Udbml_unpriced.Dbm.t
include Option_common(struct module Dbm = UDbm type res_t = bool end)
let abstraction = ref (module Extra_LU : ITA_ABSTRACTION)
let inclusion = ref (module Inclusion : ITA_INCLUSION)
let initial_value = ref false
module MC = CegarSafety
let arguments = Arg.align (common_args @
[
( "-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:
\tLU [default] LU (per discrete state) abstraction
\tM M abstraction (unimplemented)
\tID No abstraction (use with bounded automata, otherwise
there is no guarantee of termination");
( "-incl",
Arg.String (function
| "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:
\tsimple [default] regular set inclusion
\tsri abstract inclusion (Z subset of abs_LU(Z'))");
])
end
(* TODO ML, O and C are not supported yet *)
type input_type_t = XML | CMXS | ML | O | C
let inputtype = ref XML
......
open Batteries
open Printf
open Common
open TimedAutomaton
......@@ -33,7 +34,7 @@ sig
(* create an empty walk_order *)
val create : unit -> t
(* add a symbolic state to the waiting list *)
val add_to_waiting : (arg_t -> dbm_t -> dbm_t -> bool) -> t -> state -> unit
val add_to_waiting : (state -> string) -> (arg_t -> dbm_t -> dbm_t -> bool) -> t -> state -> unit
(* ask whether a symbolic state is in the passed list *)
val is_in_passed : (arg_t -> dbm_t -> dbm_t -> bool) -> t -> state -> bool
(* add a symbolic state to the passed list *)
......@@ -43,6 +44,9 @@ sig
(* ask whether the waiting list is empty *)
val is_done : t -> bool
(* (* debug *)
val get_passed_ds : t -> (key -> string) -> string
*)
val clean : (dbm_t -> bool) -> t -> unit
val waiting_length : t -> int
end
......@@ -79,7 +83,7 @@ struct
and (d2,_,_) = State.get s2
in TA.priority_compare d1 d2
end
(*
(** Builds an effective walk order, given a WAIT_CONTAINER and an INCLUSION.
*)
module Walk_Order (ContFun : WAIT_CONTAINER)
......@@ -170,7 +174,9 @@ struct
Printf.printf "cleaning: shrink from %d states to %d states stored\n" !size_before !size_after;
Printf.printf "still %d states waiting for treatment\n" (Cont.length waiting);
flush stdout
let get_passed_ds ((passed, _) : t) (f : key -> string) = failwith ""
end
*)
(** Walk Order implementation with Passed and Waiting lists merged *)
module Walk_Order_Opt (ContFun : WAIT_CONTAINER)
......@@ -207,7 +213,7 @@ struct
KeyHashtbl.add h x y;
y
let add_to_waiting incl (passed, waiting) s =
let add_to_waiting (str_of_state : state -> string) incl (passed, waiting) s =
let (l, z, a) = State.get s in
let bucket = find_or_add passed l in
if (not (List.exists (fun x -> let (_,z',_) = State.get x in incl a z z') !bucket)) then
......@@ -216,10 +222,10 @@ struct
let old_size = List.length !bucket in
(* helper function, mark subsumed states as such *)
let is_incomp x =
let (_,z',_) = State.get x in
let (l,z',_) = State.get x in
if (incl a z' z) then (
(* printf "Subsumption:\n%s\nby\n%s\n\n" (BDbm.Dbm.to_string z') (BDbm.Dbm.to_string z); *)
State.subsume x;
(*printf "Subsumption:\n%s\nby\n%s\n\n" (BDbm.Dbm.to_string z') (BDbm.Dbm.to_string z);*)
SearchState.State.subsume str_of_state x;
false
) else true
in
......@@ -234,6 +240,7 @@ struct
let bucket = find_or_add passed l in
not (List.memq s !bucket)
let add_to_passed _ (_, waiting) _ =
incr Stats.states_explored;
if ((!Stats.states_explored mod Stats.modulo) = 0) then (
......@@ -241,6 +248,15 @@ struct
flush stdout
)
(* debug *)
module DSSet = Set.Make(struct type t = key let compare = compare end )
let get_passed_ds ((passed, _) : t) (f : key -> string) =
let ds = KeyHashtbl.fold (fun k _ acc -> DSSet.add k acc) passed DSSet.empty in
let buf = Buffer.create 4024 in
DSSet.iter (fun k -> Buffer.add_string buf (f k)) ds;
Buffer.contents buf
let get_next (_, waiting) = WaitCont.pop waiting
(* discards subsumed states that are on top of the waiting list *)
......@@ -307,7 +323,7 @@ struct
Fed.iter f (fun z' -> z:=z');
!z
let post ta (sloc,szone) (source, guard, resets, target) =
let post ta ?extrapolate:(extrapolate=(fun _ x->x)) (sloc,szone) (source, guard, resets, target) =
let result_zone = Dbm.to_fed (Dbm.copy szone) in
assert(TA.DS.equal sloc source);
Fed.intersect_dbm result_zone guard;
......@@ -321,6 +337,7 @@ struct
Fed.up result_zone (TA.rate_of_state ta target);
);
Fed.intersect_dbm result_zone (TA.invariant_of_discrete_state ta target);
let result_zone = Fed.map result_zone (extrapolate (ta, target)) in
(target, result_zone)
)
......@@ -354,11 +371,7 @@ struct
let initfed = Fed.from_dbm zinit in
Fed.up initfed (TA.rate_of_state ta init);
Fed.intersect_dbm initfed (TA.invariant_of_discrete_state ta init);
let extra_initfed = Fed.create (Fed.dimension initfed) in
List.iter (fun z ->
ABS.extrapolate z (ta, init);
Fed.add_dbm extra_initfed z;
) (Fed.to_dbm initfed);
let extra_initfed = Fed.map initfed (ABS.extrapolate (ta, init)) in
(init, extra_initfed)
(** Auxiliary function that expands the search tree and returns the list
......@@ -395,35 +408,36 @@ struct
fun succs_list -> fun (source, guard, resets, target, target_arg) ->
let (sloc, szone, _) = WO.State.get state in
assert(TA.DS.equal sloc source);
let (_, succs) = post ta (sloc, szone) (source, guard, resets, target) in
if (Fed.is_empty succs) then (
succs_list
) else (
(match global_invariant with
| None -> ()
| Some inv -> Fed.intersect_dbm succs inv);
if (Fed.is_empty succs) then
let (_, succs) = post ta (sloc, szone) (source, guard, resets, target) in
if (Fed.is_empty succs) then (
succs_list
else (
let succs = Fed.map succs (fun z -> ABS.extrapolate z (ta, target)) in
let succ_searchstates = ref [] in
Fed.iter succs (fun z ->
let newstate = WO.State.create (target, z, target_arg) state in
succ_searchstates := (guard, resets, newstate) :: !succ_searchstates);
WO.State.add_sons state !succ_searchstates;
(* TODO is it not redundant? *)
if (WO.State.is_subsumed state) then WO.State.subsume state;
if (TA.is_urgent_or_committed ta target) then
let tmp = List.map (fun (_,_,nstate) -> expand_state ta nstate) !succ_searchstates in
(List.flatten tmp) @ succs_list
else
(List.map (fun (_,_,nstate) -> nstate) !succ_searchstates) @ succs_list
) else (
(match global_invariant with
| None -> ()
| Some inv -> Fed.intersect_dbm succs inv);
if (Fed.is_empty succs) then
succs_list
else (
let succs = Fed.map succs (fun z -> ABS.extrapolate (ta, target) z) in
let succ_searchstates = ref [] in
Fed.iter succs (fun z ->
let newstate = WO.State.create (target, z, target_arg) state in
succ_searchstates := (guard, resets, newstate) :: !succ_searchstates);
WO.State.add_sons state !succ_searchstates;
(* TODO is it not redundant? *)
(*
if (WO.State.is_subsumed state) then WO.State.subsume state;
*)
if (TA.is_urgent_or_committed ta target) then
let tmp = List.map (fun (_,_,nstate) -> expand_state ta nstate) !succ_searchstates in
(List.flatten tmp) @ succs_list
else
(List.map (fun (_,_,nstate) -> nstate) !succ_searchstates) @ succs_list
)
)
)
(** Inner loop of the forward reachability algorithm. See function walk.
Auxiliary recursive function, not to call from the outside *)
......@@ -433,6 +447,10 @@ struct
* if S has a maximal element, we can compare result to it
*)
let rec walk_aux ta dbm_comp wot succs update_result result =
let str_of_state s =
let (l,z,_) = WO.State.get s in
TA.string_of_extended_state ta (l,z)
in
if (WO.is_done wot) then
result
else (
......@@ -454,7 +472,7 @@ struct
printf "Wait: %d\n" (WO.waiting_length wot);
(* /DEBUG *)
*)
List.iter (fun state -> WO.add_to_waiting dbm_comp wot state) gen_states;
List.iter (fun state -> WO.add_to_waiting str_of_state dbm_comp wot state) gen_states;
);
walk_aux ta dbm_comp wot succs update_result new_res
)
......@@ -463,6 +481,10 @@ struct
See Reachability and OptReachability modules for examples of usage.
*)
let walk ta expand_state update_result res0 =
let str_of_state s =
let (l,z,_) = WO.State.get s in
TA.string_of_extended_state ta (l,z)
in
let dbm_comp a x y =
incr Stats.inclusion_tests;
let r = COMP.inclusion a x y in
......@@ -473,9 +495,13 @@ struct
let (init, initfed) = initial_federation ta in
List.iter (fun z ->
let init_state = WO.State.create (init, z, COMP.get_arg ta init) WO.State.root in
WO.add_to_waiting dbm_comp wot init_state
WO.add_to_waiting str_of_state dbm_comp wot init_state
) (Fed.to_dbm initfed);
walk_aux ta dbm_comp wot (expand_state ta) update_result res0
let ret = walk_aux ta dbm_comp wot (expand_state ta) update_result res0 in
(*
printf "%s\n" (WO.get_passed_ds wot (TA.string_of_discrete_state ta));
*)
ret
(** A helper function to turn a state s into a string representing the path
* from the initial state to s *)
......
......@@ -11,7 +11,7 @@ sig
val root : 'a t
(* TODO Why don't we label this directly with TA edges? *)
val sons : 'a t -> (Dbm.UDbm.Dbm.t * ((clock_t * int) list) * 'a t) list
val subsume : 'a t -> unit
val subsume : ('a t -> string) -> 'a t -> unit
val is_subsumed : 'a t -> bool
val add_sons : 'a t -> (Dbm.UDbm.Dbm.t * ((clock_t * int) list) * 'a t) list -> unit
val depth : 'a t -> int
......@@ -50,9 +50,12 @@ struct
(* to be called when a state is subsumed: mark all successors as subsumed
* as well, exploiting the WSTS property.
*)
let rec subsume s =
let rec subsume str_of_state s =
(* mark all its successors as subsumed *)
List.iter (fun (_,_,t) -> subsume t) s.sons;
(*
Printf.printf "Subsuming:\n %s\n" (str_of_state s);
*)
List.iter (fun (_,_,t) -> subsume str_of_state t) s.sons;
(* remove reference to successors, to ease GC work *)
s.sons <- [];
(* mark as subsumed *)
......
......@@ -7,12 +7,15 @@ module type TIMED_AUTOMATON =
sig
module MDbm : BIG_IDBM
module BareTA : Ita.TA
type timed_automaton
type discrete_state
type edge
module DS : Hashtbl.HashedType with type t = discrete_state
val bare_ta : timed_automaton -> BareTA.ta
val clocks : timed_automaton -> VarContext.t
val priority_compare : discrete_state -> discrete_state -> int
val initial_extended_state : timed_automaton -> discrete_state * MDbm.Dbm.t
......@@ -27,6 +30,8 @@ sig
val global_m_bounds : timed_automaton -> int array
(** print functions *)
val print_discrete_state : out_channel -> timed_automaton -> discrete_state -> unit
val string_of_discrete_state : timed_automaton -> discrete_state -> string
val string_of_extended_state : timed_automaton -> (discrete_state * MDbm.Dbm.t) -> string
val print_timed_automaton : out_channel -> timed_automaton -> unit
val print_extended_state : out_channel -> timed_automaton -> (discrete_state * MDbm.Dbm.t) -> unit
val transition_to_string : timed_automaton ->
......@@ -90,7 +95,7 @@ struct
end
module MDbm = MDbm
module BareTA = BareTA
module DSHashtbl = Hashtbl.Make(DS)
type timed_automaton =
......@@ -102,6 +107,8 @@ struct
}
type discrete_state = BareTA.state
type edge (* TODO *)
let bare_ta ta = ta.t
(* indirection *)
let clocks ta = ta.clocks
......@@ -179,11 +186,17 @@ struct
(* indirection *)
let print_discrete_state chan ta s =
Printf.fprintf chan "%s" (BareTA.string_of_state ta.t s)
let string_of_discrete_state ta s =
Printf.sprintf "%s" (BareTA.string_of_state ta.t s)
let print_extended_state chan ta (s,z) =
print_discrete_state chan ta s;
Printf.fprintf chan "\n%s " (MDbm.Dbm.to_string z)
let string_of_extended_state ta (s,z) =
let s = string_of_discrete_state ta s in
Printf.sprintf "%s\n%s " s (MDbm.Dbm.to_string z)
(* indirection *)
let print_timed_automaton chan ta =
BareTA.print_timed_automaton chan ta.t
......
......@@ -213,7 +213,10 @@ struct
| ClockArray(aid,indices) ->
let arrayName = VarContext.array_of_index ta.clocks aid in
List.fold_left (fun s x -> s ^ "[" ^ (string_of_exp x) ^ "]") arrayName indices
| Variable(id) -> VarContext.var_of_index ta.vars id
| Variable(id) ->
printf "Accessing variable %d\n" id;
flush stdout;
VarContext.var_of_index ta.vars id
| ConstVariable(id) -> VarContext.var_of_index ta.constants id
| Clock(id) -> VarContext.var_of_index ta.clocks id
| Product(e1,e2) ->
......@@ -720,7 +723,6 @@ struct
for l=0 to (Array.length proc.procLocations)-1 do
let loc = proc.procLocations.(l) in
loc.compExpr <- Array.make nclocks ([],[]);
let ag_handle = function
| GuardLeq(lhs,e)
| GuardLess(lhs,e) ->
......@@ -759,7 +761,10 @@ struct
loc.compExpr.(cl) <- lnew, unew
)
(clocks_of ta lhs)
| _ -> failwith "cannot compute LU bounds, guard is not in normal form"
| _ as g ->
failwith
(Printf.sprintf "cannot compute LU bounds, guard is not in normal form: %s"
(string_of_guard ta [g]))
in
(* add invariant contribution *)
......@@ -1135,6 +1140,47 @@ struct
Callback.register "cb_set_query" ta_set_query;
utap_from_file tafile qfile
let guard_constants ta =
let module IntSet = Batteries.Set.Make(Batteries.Int) in
let dim = (nb_clocks ta) + 1 in
let abs = Array.init dim
(fun i -> Array.init dim
(fun j -> ref (IntSet.empty) )
) in
let add_to_abs guard =
(* Convert QueryBuilder.atomic_guard to Ita.atomic_guard *)
(List.map ag_to_pair guard)
|>
List.iter (function
Ita.LT(c, k) ->
abs.(c).(0) := IntSet.add k !(abs.(c).(0))
| Ita.LEQ(c,k) ->
abs.(c).(0) := IntSet.add k !(abs.(c).(0))
| Ita.GT(c,k) ->
abs.(0).(c) := IntSet.add (-k) !(abs.(0).(c))
| Ita.GEQ(c,k) ->
abs.(0).(c) := IntSet.add (-k) !(abs.(0).(c))
| Ita.EQ(c,k) ->
abs.(0).(c) := IntSet.add (-k) !(abs.(0).(c));
abs.(c).(0) := IntSet.add k !(abs.(c).(0))
)
in
Array.iter (fun proc ->
(Array.iter (fun loc ->
List.iter (fun edge ->
add_to_abs edge.edgeGuard
) loc.locEdges;
add_to_abs loc.locInvar
)
) proc.procLocations
) ta.procs;
let abs' =
Array.map (Array.map (fun s -> IntSet.to_array !s)) abs in
Array.iter (Array.iter (Array.sort compare)) abs';
abs'
let ocan = "ocan"
let from_file tafile qfile enable_cora ?scale:(scale=1) ?enlarge:(enlarge=0) () =
let ta = make_ta tafile qfile enable_cora in
ta
......
E<> (p1.c and (p2.b and p3.c) and id == 0)
E<> ( P1.error and P2.sender_transm)
<?xml version="1.0" encoding="utf-8"?><!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_1.dtd'><nta><declaration>// ------------------------------------------------------------
// CSMA/CD 9
// Carrier Sense, Multiple-Access with Collision Detection
//
// automatically generated by script genCSMA_CD.awk
// M. Oliver Moeller &lt;omoeller@brics.dk&gt;
// Wed Sep 19 11:48:20 2001
// ------------------------------------------------------------
chan begin, end, busy, cd1;</declaration><template><name>P0</name><declaration>clock x;</declaration><location id="id0" x="-120" y="80"><name x="-192" y="48">bus_idle</name></location><location id="id1" x="48" y="80"><name x="24" y="-8">bus_active</name></location><location id="id2" x="208" y="80"><name x="176" y="0">bus_collision1</name><label kind="invariant" x="176" y="24">x &lt;= 26</label></location><init ref="id0"/><transition><source ref="id2"/><target ref="id0"/><label kind="guard" x="40" y="176">x &lt;= 26</label><label kind="synchronisation" x="40" y="191">cd1 !</label><label kind="assignment" x="40" y="206">x=0</label><nail x="96" y="232"/><nail x="32" y="232"/></transition><transition><source ref="id0"/><target ref="id1"/><label kind="synchronisation" x="-72" y="40">begin ?</label><label kind="assignment" x="-72" y="56">x= 0</label></transition><transition><source ref="id1"/><target ref="id0"/><label kind="synchronisation" x="-40" y="120">end ?</label><label kind="assignment" x="-40" y="136">x= 0</label><nail x="48" y="112"/><nail x="-120" y="112"/></transition><transition><source ref="id1"/><target ref="id1"/><label kind="guard" x="24" y="-24">x &gt;= 26</label><label kind="synchronisation" x="24" y="8">busy !</label><nail x="16" y="32"/><nail x="80" y="32"/></transition><transition><source ref="id1"/><target ref="id2"/><label kind="guard" x="112" y="48">x &lt;= 26</label><label kind="synchronisation" x="112" y="88">begin ?</label><label kind="assignment" x="112" y="104">x= 0</label></transition></template><template><name>P1</name><declaration>clock x;</declaration><location id="id3" x="344" y="-24"><name x="334" y="-54">error</name></location><location id="id4" x="-48" y="72"><name x="-120" y="16">sender_wait</name></location><location id="id5" x="192" y="80"><name x="216" y="64">sender_transm</name><label kind="invariant" x="208" y="80">x&lt;= 808</label></location><location id="id6" x="190" y="230"><name x="180" y="200">sender_retry</name><label kind="invariant" x="180" y="245">x &lt;= 52</label></location><init ref="id4"/><transition><source ref="id5"/><target ref="id3"/><label kind="guard" x="224" y="0">x&gt;=53</label></transition><transition><source ref="id4"/><target ref="id5"/><label kind="synchronisation" x="32" y="-32">begin !</label><label kind="assignment" x="56" y="0">x= 0</label><nail x="80" y="-16"/></transition><transition><source ref="id4"/><target ref="id4"/><label kind="synchronisation" x="-108" y="57">cd1 ?</label><label kind="assignment" x="-108" y="72">x= 0</label><nail x="-78" y="42"/><nail x="-18" y="42"/></transition><transition><source ref="id4"/><target ref="id6"/><label kind="synchronisation" x="55" y="140">cd1 ?</label><label kind="assignment" x="55" y="155">x= 0</label></transition><transition><source ref="id4"/><target ref="id6"/><label kind="s