Commit 7c787430 authored by Maximilien Colange's avatar Maximilien Colange

Merge branch 'master' into tests

parents 7e66225e a0eda0df
......@@ -147,10 +147,8 @@ struct
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)
| "BBFS" -> walk_order := (module Waiting.BBFST : PARTIAL_WO)
| "BDFS" -> 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:
......
......@@ -208,16 +208,13 @@ struct
let model =
let ta = BareTA.model in
let clocks = VarContext.create () in
(* the reference clock *)
let i0 = VarContext.add clocks "t(0)" in
assert(i0 = 0);
for i = 1 to BareTA.nb_clocks ta do
let j = VarContext.add clocks (BareTA.string_of_clock ta i) in
assert(i = j)
done;
(* the reference clock *)
let _ =
try
VarContext.add clocks "t(0)"
with Var_already_defined -> -1 (* OK, uppaalta already defines t(0) *)
in
{
t = BareTA.model;
clocks = clocks;
......
......@@ -552,10 +552,6 @@ handle_declaration(variable_t &var, value proc, const std::map<symbol_t, express
cb_array = caml_callback(cb_array, proc);
cb_cell = caml_callback(cb_cell, proc);
// first, register array name
caml_callback(cb_array,
caml_copy_string(var.uid.getName().c_str()));
// if varType.getSub() is itself an array type, this makes arrays of arrays
// to handle the general case, we need to retrieve all dimensions, say in a vector
// BEWARE of the order: top-most in the type = right-most in the declaration
......@@ -576,6 +572,18 @@ handle_declaration(variable_t &var, value proc, const std::map<symbol_t, express
currentType = currentType.getSub();
}
indices = caml_callback(*caml_named_value("cb_empty_list"), Val_unit);
for (auto it = multiSize.rbegin(); it != multiSize.rend(); ++it)
{
indices = caml_callback2(*caml_named_value("cb_build_list"),
Val_int(*it),
indices);
}
// first, register array name with its full dimension
caml_callback2(cb_array,
caml_copy_string(var.uid.getName().c_str()),
indices);
std::vector<int> index(multiSize.size(), 0);
bool index_is_zero = true;
do
......
......@@ -205,15 +205,17 @@ struct
(function
| Constant c -> sprintf "%d" c
| Array(aid, indices) ->
List.fold_left (fun s x -> s ^ (string_of_exp x)) (VarContext.array_of_index ta.vars aid) indices
let arrayName = VarContext.array_of_index ta.vars aid in
List.fold_left (fun s x -> s ^ "[" ^ (string_of_exp x) ^ "]") arrayName indices
| ConstArray(aid, indices) ->
List.fold_left (fun s x -> s ^ (string_of_exp x)) (VarContext.array_of_index ta.constants aid) indices
| Variable(id) -> 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
let arrayName = VarContext.array_of_index ta.constants aid in
List.fold_left (fun s x -> s ^ "[" ^ (string_of_exp x) ^ "]") arrayName indices
| 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
| ConstVariable(id) -> VarContext.var_of_index ta.constants id
| Clock(id) -> VarContext.var_of_index ta.clocks id
| Product(e1,e2) ->
sprintf "%s * %s" (string_of_exp e1)
(string_of_exp e2)
......@@ -380,19 +382,17 @@ struct
*)
let rec eval_exp ta vars = function
| Constant c -> Constant c
| ConstVariable(id) ->
if ( id < 0 || id >= Array.length ta.constvalues ) then
failwith (sprintf "Const var index %d out of bounds (%d)" id (Array.length ta.constvalues));
| ConstVariable id ->
assert(id >= 0 && id < Array.length ta.constvalues);
Constant ta.constvalues.(id)
| Variable(id) ->
if ( id < 0 || id >= Array.length vars ) then
failwith (sprintf "Var index %d out of bounds (%d)" id (Array.length vars));
| Variable id ->
assert(id >= 0 && id < Array.length vars);
Constant vars.(id)
| Clock(c) -> Clock(c)
| Clock c -> Clock c
| ClockArray(arrayId, l) ->
let indices = List.map (fun x -> eval_disc_exp ta vars x) l in
let cellindex = VarContext.index_of_cell ta.clocks arrayId indices in
Clock(cellindex)
Clock cellindex
| Array(arrayId, l) ->
let indices = List.map (fun x -> eval_disc_exp ta vars x) l in
let cellindex = VarContext.index_of_cell ta.vars arrayId indices in
......@@ -477,11 +477,11 @@ struct
(********** TIMED_AUTOMATON interface **********)
let clocks ta = ta.clocks
let nb_clocks ta = VarContext.size (clocks ta)
let nb_clocks ta = (VarContext.size (clocks ta))-1
let string_of_clock ta cl =
assert(cl > 0 && cl <= nb_clocks ta);
VarContext.var_of_index (clocks ta) (cl-1)
assert(cl > 0 && cl <= VarContext.size (clocks ta));
VarContext.var_of_index (clocks ta) cl
let initial_state ta = ta.init
......@@ -607,24 +607,6 @@ struct
(********** LOADING FUNCTIONS **********)
(** given a set of expressions, simplify it to retain only its maximal
* constant and all non-constant *)
(* TODO check that the input does not contain ConstVariable or constant ConstArray *)
let simplify_max exprs =
let new_max = function
| None -> (function
| Constant k -> Some k
| _ -> None)
| Some m as e -> (function
| Constant k when k > m -> Some k
| _ -> e)
in
match List.fold_left new_max None exprs with
| None -> exprs
| Some k -> List.filter (function
| Constant l when l < k -> false
| _ -> true) exprs
(* given a process, a location l and a clock c, compute the set of expressions
* against which c is compared from l until it is reset.
* Formally, the result S is the smallest set of expressions such that:
......@@ -633,6 +615,7 @@ struct
* if x is compared to e in the guard of t, then e \in S
* if x is not reset in t, then comp_expressions p l' c \subset S
* returns a pair (L,U)
* NB: the compExpr arrays are initialized by the function build_lu.
*)
let comp_expressions ta p l c =
ta.procs.(p).procLocations.(l).compExpr.(c)
......@@ -641,41 +624,32 @@ struct
(* this should be used from another function that caches the results *)
(* TODO some clocks already have their constant known, cache them *)
let _lubounds ta state =
let n = nb_clocks ta in
let n = VarContext.size ta.clocks in
let lb, ub = Array.make n 0, Array.make n 0 in
for cl=0 to n-1 do
let lexpr, uexpr = Array.fold_left
(fun (lacc, uacc) loc ->
let eval = eval_exp ta state.stateVars in
for cl=1 to n-1 do
Array.iter
(fun loc ->
let ltmp, utmp = loc.compExpr.(cl) in
(lacc @ ltmp, uacc @ utmp)) ([],[])
(* instantiate found expressions, and retain only the maximal constant *)
List.iter (fun e ->
match eval e with
| Constant k when k > lb.(cl) -> lb.(cl) <- k
| Constant _ -> ()
| _ -> failwith "expression does not evaluate to constant")
ltmp;
List.iter (fun e ->
match eval e with
| Constant k when k > ub.(cl) -> ub.(cl) <- k
| Constant _ -> ()
| _ -> failwith "expression does not evaluate to constant")
utmp)
state.stateLocs
in
(* instantiate found expressions, and retain only the maximal constant *)
let lcst, ucst =
simplify_max (List.map (fun e -> eval_exp ta state.stateVars e) lexpr),
simplify_max (List.map (fun e -> eval_exp ta state.stateVars e) uexpr)
in
begin
match lcst with
| (Constant k)::_ -> lb.(cl) <- max lb.(cl) k
| _ -> (* TODO can it happen? *) ()
end;
begin
match ucst with
| (Constant k)::_ -> ub.(cl) <- max ub.(cl) k
| _ -> (* TODO can it happen? *) ()
end;
done;
lb, ub
let lubounds ta state =
try
DSHashtbl.find ta.lubounds_tbl state
with
| Not_found ->
let res = _lubounds ta state in
DSHashtbl.add ta.lubounds_tbl state res;
res
_lubounds ta state
(* tells whether a given clock is set by a given update *)
(* the difficult part is when the lhs of the update is an array cell *)
......@@ -694,6 +668,39 @@ struct
| ClockArray(a,_) -> (*TODO*) failwith "cannot compute bounds for arrays of clocks"
| _ -> []
(* a non-recursive constant evaluation *)
let flat_constant_eval ta = function
| ConstVariable id ->
assert(id >= 0 && id < Array.length ta.constvalues);
Constant ta.constvalues.(id)
| ClockArray (a, l) when List.for_all (function | Constant _ -> true | _ -> false) l ->
let cellindex = VarContext.index_of_cell ta.clocks a (List.map (function Constant k -> k) l) in
Clock cellindex
| Array (a, l) when List.for_all (function | Constant _ -> true | _ -> false) l ->
let cellindex = VarContext.index_of_cell ta.vars a (List.map (function Constant k -> k) l) in
Variable cellindex
| ConstArray (a, l) when List.for_all (function | Constant _ -> true | _ -> false) l ->
let cellindex = VarContext.index_of_cell ta.constants a (List.map (function Constant k -> k) l) in
Constant ta.constvalues.(cellindex)
| _ as e -> e
let rec constant_eval ta = function
| ClockArray (a, l) ->
flat_constant_eval ta (ClockArray (a, List.map (constant_eval ta) l))
| Array (a, l) ->
flat_constant_eval ta (Array (a, List.map (constant_eval ta) l))
| ConstArray (a, l) ->
flat_constant_eval ta (ConstArray (a, List.map (constant_eval ta) l))
| Sum (e1, e2) ->
flat_constant_eval ta (Sum (constant_eval ta e1, constant_eval ta e2))
| Product (e1, e2) ->
flat_constant_eval ta (Product (constant_eval ta e1, constant_eval ta e2))
| Substraction (e1, e2) ->
flat_constant_eval ta (Substraction (constant_eval ta e1, constant_eval ta e2))
| Division (e1, e2) ->
flat_constant_eval ta (Division (constant_eval ta e1, constant_eval ta e2))
| _ as e -> flat_constant_eval ta e
(* compute all the local LU bounds *)
let build_lu ta =
let nclocks = VarContext.size ta.clocks in
......@@ -803,8 +810,25 @@ struct
end
done
) loc.locEdges
done
done
done (* location loop *)
done; (* fixpoint loop *)
(* We try to simplify the sets of expressions
* i.e. do constant propagation.
* TODO we should also remove duplicates if any
*)
(* for each location *)
for l=0 to (Array.length proc.procLocations)-1 do
let loc = proc.procLocations.(l) in
(* for each clock *)
for cl=0 to nclocks-1 do
let lcur, ucur = loc.compExpr.(cl) in
let lnew = List.map (constant_eval ta) lcur
and unew = List.map (constant_eval ta) ucur
in
loc.compExpr.(cl) <- lnew, unew;
done (* clock loop *)
done (* location loop *)
done
......
......@@ -42,6 +42,47 @@ sig
val iter : t -> (var_t -> int -> unit) -> unit
end
(**
* a custom type to store array cells
*)
module ArrayCell =
struct
type arr = Leaf of int array | Node of arr array
let rec make_array = function
| [] -> failwith "an array cannot be empty"
| [n] -> Leaf (Array.make n 0)
| n::l -> Node (Array.init n (fun _ -> make_array l))
let rec get_leaf = function
| Leaf a -> begin function
| [n] -> a.(n)
| _ -> failwith "wrong array dimension"
end
| Node a -> begin function
| n::l -> get_leaf a.(n) l
| _ -> failwith "wrong array dimension"
end
let rec set_leaf value = function
| Leaf a -> begin function
| [n] -> a.(n) <- value
| _ -> failwith "wrong array dimension"
end
| Node a -> begin function
| n::l -> set_leaf value a.(n) l
| _ -> failwith "wrong array dimension"
end
let rec _get_cells = function
| Leaf a -> Array.to_list a
| Node a -> Array.fold_left (fun acc x -> acc @ (_get_cells x)) [] a
let get_cells x =
List.sort Pervasives.compare (_get_cells x)
end
module VarContextFunctor =
functor (Vars : sig type var_t type array_t val cell2var : array_t -> int list -> var_t end) ->
struct
......@@ -56,7 +97,7 @@ struct
index2array : (int,arr_t) Hashtbl.t;
array2index : (arr_t,int) Hashtbl.t;
cells2vars : (int * int list, int) Hashtbl.t;
mutable cells2vars : ArrayCell.arr array;
mutable nextVarIndex : int;
mutable nextArrayIndex : int;
......@@ -70,7 +111,7 @@ struct
index2array = Hashtbl.create 16;
array2index = Hashtbl.create 16;
cells2vars = Hashtbl.create 16;
cells2vars = [||];
nextVarIndex = 0;
nextArrayIndex = 0;
......@@ -91,7 +132,7 @@ struct
Hashtbl.mem vc.array2index arr
let index_of_cell vc arrayId indices =
Hashtbl.find vc.cells2vars (arrayId,indices)
ArrayCell.get_leaf vc.cells2vars.(arrayId) indices
let add vc varName =
if (Hashtbl.mem vc.var2index varName) then (
......@@ -103,20 +144,21 @@ struct
Hashtbl.add vc.var2index varName index;
index
let add_array vc arrayName =
let add_array vc arrayName dims =
if (Hashtbl.mem vc.array2index arrayName) then (
raise Var_already_defined
);
let index = vc.nextArrayIndex in
vc.nextArrayIndex <- vc.nextArrayIndex + 1;
Hashtbl.add vc.index2array index arrayName;
Hashtbl.add vc.array2index arrayName index
Hashtbl.add vc.array2index arrayName index;
vc.cells2vars <- Array.append vc.cells2vars [|ArrayCell.make_array dims|]
let add_cell vc arrayName indices =
let arrayIndex = Hashtbl.find vc.array2index arrayName in
let cellVar = Vars.cell2var arrayName indices in
let cellIndex = add vc cellVar in
Hashtbl.add vc.cells2vars (arrayIndex,indices) cellIndex;
ArrayCell.set_leaf cellIndex vc.cells2vars.(arrayIndex) indices;
cellIndex
let size vc = Hashtbl.length vc.var2index
......@@ -174,7 +216,7 @@ struct
let arrList =
List.sort compare
(Hashtbl.fold (fun (p,v) index acc -> (index, prep v p)::acc) svc.array2index []) in
List.iter (fun (_,name) -> VarContext.add_array result name) arrList;
List.iter (fun (_,name) -> VarContext.add_array result name [0]) arrList;
(* Do not forget the mapping from cells to vars *)
{ result with VarContext.cells2vars = svc.cells2vars }
......
......@@ -37,69 +37,9 @@ module Walk_DFS = Walk_Order_Opt (WOStack)
module Walk_BFS = Walk_Order_Opt (WOQueue)
(**
* A custom, circular list, that allows inplace insertion, to keep it sorted
* A custom tree to represent sorted sets, with inplace insertion.
* Inspired by the representation of Sets in the standard library.
*)
module MyList (T : sig val threshold : int end) : WAIT_CONTAINER =
functor (Elem : WaitOrderedType) ->
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; }
(* insert as soon as x <= y [Stack] *)
let _should_insert x y = Elem.compare x y < T.threshold
let rec _push_aux c x l =
(* should x be inserted before c.next? *)
if (_should_insert x c.next.content) then
let newcell = { content = x; next = c.next; } in
c.next <- newcell;
l.length <- l.length + 1;
(* if we have reached the end of the list *)
else if (c.next == l.tail) then
let newcell = { content = x; next = c.next.next (*head*); } in
c.next.next <- newcell;
l.tail <- newcell;
l.length <- l.length + 1;
(* go to next element in the list *)
else
_push_aux c.next x l
let push x l =
if l.length = 0 then (
let rec cell = {
content = x;
next = cell;
}
in
l.length <- 1;
l.tail <- cell
) else (
_push_aux l.tail x l
)
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
(* Rework the ordered list as a binary tree *)
(* Inspired by the representation of Sets in the standard library *)
module MyBTree (T : sig val threshold : int end) : WAIT_CONTAINER =
functor (Elem : WaitOrderedType) ->
struct
......@@ -270,7 +210,6 @@ end
* insert an element x before y as soon as x <= y
* i.e. compare x y < 1
*)
module Priority_Stack : WAIT_CONTAINER = MyList (struct let threshold = 1 end)
module Priority_StackTree : WAIT_CONTAINER = MyBTree (struct let threshold = 1 end)
(*
......@@ -278,12 +217,9 @@ module Priority_StackTree : WAIT_CONTAINER = MyBTree (struct let threshold = 1 e
* insert an element x before y as soon as x < y
* i.e. compare x y < 0
*)
module Priority_Queue : WAIT_CONTAINER = MyList (struct let threshold = 0 end)
module Priority_QueueTree : WAIT_CONTAINER = MyBTree (struct let threshold = 0 end)
module BDFS = Walk_Order_Opt (Priority_Stack)
module BDFST = Walk_Order_Opt (Priority_StackTree)
module BBFS = Walk_Order_Opt (Priority_Queue)
module BBFST = Walk_Order_Opt (Priority_QueueTree)
//This file was generated from UPPAAL CORA 041109, Nov 2004
/*
*/
E<> KL101.done and KL108.done and KL115.done and KL122.done and KL129.done and KL136.done and KL143.done and KL150.done and KL157.done and KL164.done
......@@ -99,10 +99,10 @@ KL143 = Flight(124,138,577,30,30,0,1);
KL150 = Flight(126,140,573,30,30,0,1);
KL157 = Flight(135,150,591,30,30,0,1);
KL164 = Flight(160,180,657,30,30,0,1);
</instantiation><system>system runway0, runway1, KL101, KL108, KL122, KL129, KL136, KL143, KL150;</system>
</instantiation><system>system runway0, runway1, KL101, KL108, KL115, KL122, KL129, KL136, KL143, KL150, KL157, KL164;</system>
<queries>
<query>
<formula>E&lt;&gt; (KL101.done and KL108.done and KL122.done and KL129.done and KL136.done and KL143.done and KL150.done)
<formula>E&lt;&gt; (KL101.done and KL108.done and KL115.done and KL122.done and KL129.done and KL136.done and KL143.done and KL150.done and KL157.done and KL164.done)
</formula>
<comment>
</comment>
......
Aicraft Landing System model, reachability, BFS, simple inclusion test
./tiamo reach tests/als.xml -cora -order BFS -incl simple
Aicraft Landing System model, reachability, DFS, simple inclusion test
./tiamo reach tests/als.xml -cora -order DFS -incl simple
Input automaton parsed, computing LU bounds
Took 0 seconds to compute LU bounds
we have explored 285000 states, 10152 in the waiting listt
discrete states: 1736
states seen: 376461
states explored: 285190
max size of storage: 317837
incl tests: 1208691736
pos. incl tests: 1215266
discrete states: 41
states seen: 51
states explored: 20
max size of storage: 51
incl tests: 20
pos. incl tests: 0
Result of verification is Reachable!
Path is
Aicraft Landing System model, reachability, BFS, abstract inclusion test
./tiamo reach tests/als.xml -cora -order BFS -incl sri
Aicraft Landing System model, reachability, DFS, abstract inclusion test
./tiamo reach tests/als.xml -cora -order DFS -incl sri
Input automaton parsed, computing LU bounds
Took 0 seconds to compute LU bounds
we have explored 5000 states, 3000 in the waiting list
discrete states: 1736
states seen: 15918
states explored: 9722
max size of storage: 10087
incl tests: 433035
pos. incl tests: 47330
discrete states: 41
states seen: 51
states explored: 20
max size of storage: 51
incl tests: 20
pos. incl tests: 0
Result of verification is Reachable!
Path is
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