Commit a4001b2b authored by Maximilien Colange's avatar Maximilien Colange

Allow to use a 'preference' parameter (encoded as a variable with reserved...

Allow to use a 'preference' parameter (encoded as a variable with reserved name) to sort the WAITING list.
parent 84fc58ac
......@@ -52,6 +52,7 @@ end
module WSTS_WO (Key : Hashtbl.HashedType)
(BDbm : Dbm.BIG_IDBM)
(COMP : INCLUSION with type dbm_t := BDbm.Dbm.t)
(Best : Set.OrderedType 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
......
......@@ -14,14 +14,16 @@ sig
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 : Set.OrderedType 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,9 +78,10 @@ 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 : Set.OrderedType 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)
......@@ -89,9 +94,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 =
......@@ -186,7 +194,7 @@ struct
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 @
......@@ -202,9 +210,18 @@ struct
" Sets the order in which the RG is explored
\tBFS [default] Bread-First Search
\tDFS Depth-First Search
\tBBFS Best (see option -best) first, BFS on equivalent ones
\tBDFS Best (see option -best) first, DFS on equivalent ones
\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
......@@ -240,7 +257,8 @@ let verify (module O : OPTIONS) tafile qfile =
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
......
......@@ -116,6 +116,9 @@ struct
let get_arg ta loc = TA.m_bounds ta loc
end
(* a helper type to avoid redundant verbosity in WALK_ORDER implementations *)
type 'a _path = ('a * Dbm.UDbm.Dbm.t * ((clock_t * int) list) * 'a) list
(** An abstract type for the walk order of a graph *)
(** TODO Operations returning unit are very imperative style...
* but efficiency should prevail
......@@ -137,7 +140,7 @@ sig
* clock updates list
* discrete state (i.e. key)
*)
type path = (key * Dbm.UDbm.Dbm.t * ((clock_t * int) list) * key) list
type path = key _path
val create : unit -> t
val add_to_waiting : (arg_t -> dbm_t -> dbm_t -> bool) -> t -> key * dbm_t * arg_t * path -> unit
......@@ -167,12 +170,39 @@ sig
val length : t -> int
end
module type BEST =
functor (TA : TIMED_AUTOMATON) ->
functor (COMP : INCLUSION with type dbm_t := TA.MDbm.Dbm.t) ->
Set.OrderedType with type t = TA.discrete_state * TA.MDbm.Dbm.t * COMP.arg_t * TA.discrete_state _path
(** A module to compare two states in the waiting list by their infimum cost *)
module BestCost : BEST =
functor (TA : TIMED_AUTOMATON) ->
functor (COMP : INCLUSION with type dbm_t := TA.MDbm.Dbm.t) ->
struct
type t = TA.discrete_state * TA.MDbm.Dbm.t * COMP.arg_t * TA.discrete_state _path
let compare (_,z1,_,_) (_,z2,_,_) = TA.MDbm.Dbm.is_best z1 z2
end
(** A module to compare two states in the waiting list by their priority *)
module HighPrio (TA : TIMED_AUTOMATON)
(COMP : INCLUSION with type dbm_t := TA.MDbm.Dbm.t)
: (Set.OrderedType with type t = TA.discrete_state * TA.MDbm.Dbm.t * COMP.arg_t * TA.discrete_state _path) =
struct
type t = TA.discrete_state * TA.MDbm.Dbm.t * COMP.arg_t * TA.discrete_state _path
let compare (s1,_,_,_) (s2,_,_,_) = TA.priority_compare s1 s2
end
(** Builds an effective walk order, given a WAIT_CONTAINER and an INCLUSION.
*)
module Walk_Order (ContFun : WAIT_CONTAINER)
(Key : Hashtbl.HashedType)
(BDbm : Dbm.BIG_IDBM)
(COMP : INCLUSION with type dbm_t := BDbm.Dbm.t)
(Best : Set.OrderedType 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
......@@ -181,14 +211,10 @@ struct
type dbm_list = BDbm.Dbm.t list ref
type key = KeyHashtbl.key
(* cf. WALK_ORDER signature *)
type path = (key * Dbm.UDbm.Dbm.t * ((clock_t * int) list) * key) list
module Cont = ContFun(
struct
type t = key * BDbm.Dbm.t * COMP.arg_t * path
type path = key _path
let compare (_,z1,_,_) (_,z2,_,_) = BDbm.Dbm.is_best z1 z2
end)
module Cont = ContFun(Best)
type t = dbm_list KeyHashtbl.t * Cont.t
let create () = (KeyHashtbl.create 1024, Cont.create ())
......@@ -249,6 +275,7 @@ module Walk_Order_Opt (ContFun : WAIT_CONTAINER)
(Key : Hashtbl.HashedType)
(BDbm : Dbm.BIG_IDBM)
(COMP : INCLUSION with type dbm_t := BDbm.Dbm.t)
(Best : Set.OrderedType 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
......@@ -257,14 +284,9 @@ struct
type dbm_list = BDbm.Dbm.t list ref
type key = KeyHashtbl.key
(* cf. WALK_ORDER signature *)
type path = (key * Dbm.UDbm.Dbm.t * ((clock_t * int) list) * key) list
module Cont = ContFun(
struct
type t = key * BDbm.Dbm.t * COMP.arg_t * path
let compare (_,z1,_,_) (_,z2,_,_) = BDbm.Dbm.is_best z1 z2
end)
type path = key _path
module Cont = ContFun(Best)
type t = dbm_list KeyHashtbl.t * Cont.t
let create () = (KeyHashtbl.create 1024, Cont.create ())
......
......@@ -16,6 +16,7 @@ sig
val clocks : timed_automaton -> VarContext.t
val is_state_equal : discrete_state -> discrete_state -> bool
val priority_compare : discrete_state -> discrete_state -> int
val initial_discrete_state : timed_automaton -> discrete_state
(* does it belong here? If so, so does type for extended_state... *)
val initial_extended_state : timed_automaton -> discrete_state * MDbm.Dbm.t
......@@ -257,6 +258,10 @@ struct
module DSHashtbl = Hashtbl.Make(DS)
(* s1 < s2 iff s1.prio > s2.prio *)
let priority_compare s1 s2 =
- compare s1.stateVars.(0) s2.stateVars.(0)
(** A succinct version of the above to be used in hash tables *)
type _succinct_transition = int array * guard
......@@ -964,6 +969,11 @@ struct
for i = 0 to nvars-1 do
initVars.(i) <- Hashtbl.find var_init_values i;
done;
(* Check that the special-meaning variable is at the correct index *)
if (VarContext.index_of_var vars "preference" <> 0) then begin
Printf.printf "preference has a wrong index, but this is not supposed to happen\n Aborting...\n";
exit 1;
end;
let ta = {
procs = procs;
clocks = clocks;
......
......@@ -926,6 +926,7 @@ TimedAutomataSystem::TimedAutomataSystem(): syncUsed(0)
{
global.frame = frame_t::createFrame();
addVariable(&global, type_t::createPrimitive(CLOCK), "t(0)", expression_t());
addVariable(&global, type_t::createPrimitive(INT), "preference", expression_t());
#ifdef ENABLE_CORA
addVariable(&global, type_t::createPrimitive(COST), "cost", expression_t());
#endif
......
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