Commit e3ef678a authored by Benoît Barbot's avatar Benoît Barbot
Browse files

progress

parent 0b13eafe
Pipeline #1644 failed with stages
in 13 seconds
......@@ -32,8 +32,8 @@ module Make(Sem:Semantic.S) = struct
List.iter (fun tr ->
let weight,_,_ = tr.ZoneGraph.weight.(i) in
let w = eval_poly_state_full st weight in
let low = Sem.Bt.eval_min_bound st tr.ZoneGraph.lower_bound
and up = Sem.Bt.eval_max_bound st tr.ZoneGraph.upper_bound in
let low = Sem.Bt.eval_max_bound st tr.ZoneGraph.lower_bound
and up = Sem.Bt.eval_min_bound st tr.ZoneGraph.upper_bound in
fprintf f " [%c]-[%g;%g]--(%a)->%g " tr.ZoneGraph.action low up P.print weight w
) l) rgpoly.ZoneGraph.statelist.(get_loc st).ZoneGraph.transition
| Void | Timestamp | Timeword -> () in
......
......@@ -51,17 +51,6 @@ module type WeightStructure = sig
end
type 'a transChoice = Label of 'a | Rand of float | Fixed
module type BoundType = sig
type t
val zero : t
val print : VarSet.varset -> Format.formatter -> t -> unit
val map : int array -> t -> t
val get_bound : t -> Common.bound
type state = int *float array
val eval_min_bound : state -> t -> float
val eval_max_bound : state -> t -> float
end
module type S =
sig
......@@ -281,8 +270,8 @@ module Make (Bt: BoundType) (P: WeightStructure) = struct
(* Sample firing time of transition trans using random number u*)
let sample_time ?max_iter:(max_iter=20) i state trans u =
let low = Bt.eval_min_bound state trans.lower_bound
and up = Bt.eval_max_bound state trans.upper_bound in
let low = Bt.eval_max_bound state trans.lower_bound
and up = Bt.eval_min_bound state trans.upper_bound in
assert (low <= up);
assert (0.0 <= low);
if Array.length trans.weight =0 then
......@@ -329,8 +318,8 @@ module Make (Bt: BoundType) (P: WeightStructure) = struct
None -> l
| Some ff ->
List.filter (fun tr ->
let low = Bt.eval_min_bound (id,tab) tr.lower_bound
and up = Bt.eval_max_bound (id,tab) tr.upper_bound in
let low = Bt.eval_max_bound (id,tab) tr.lower_bound
and up = Bt.eval_min_bound (id,tab) tr.upper_bound in
ff (low,up) tr) l
)
......
......@@ -29,23 +29,11 @@ module type WeightStructure =
end
type 'a transChoice = Label of 'a | Rand of float | Fixed
exception Zero_derivative
module type BoundType = sig
type t
val zero : t
val print : Common.VarSet.varset -> Format.formatter -> t -> unit
val map : int array -> t -> t
type state = int * float array
val get_bound : t -> Common.bound
val eval_min_bound : state -> t -> float
val eval_max_bound : state -> t -> float
end
module type S =
sig
module P:WeightStructure
module Bt:BoundType
module Bt:ZoneGraphInput.BoundType
val t : P.var
val iterate_functionnal :
......@@ -90,4 +78,4 @@ sig
samplers:(int -> float) * (int -> float) -> unit
end
module Make (Bt : BoundType) (P : WeightStructure) : S with type P.t = P.t and type P.var=P.var and type Bt.t=Bt.t and type Bt.state=Bt.state
module Make (Bt : ZoneGraphInput.BoundType) (P : WeightStructure) : S with type P.t = P.t and type P.var=P.var and type Bt.t=Bt.t and type Bt.state=Bt.state
......@@ -100,7 +100,7 @@ let reachability ~verbose ~print_rg ~splitting_debug ta =
tex_out,reach
(* Split the reachability graph and export it to zone graphe *)
let splitting ~verbose ~print_rg ta (tex_out,reach) =
let splitting ~verbose ~print_rg ta tex_out reach =
if verbose >0 then (
printf "Splitting reachability graph ... ";
print_flush ());
......@@ -119,69 +119,105 @@ let splitting ~verbose ~print_rg ta (tex_out,reach) =
split_reach
let zone_graph_from_ta ?(verbose=1)
?(print_rg=false)
?(splitting_debug="")
?export_zone_graph ta =
if print_rg then TimedAutomaton.Uautomaton.print_timed_automaton stdout ta;
let reach = reachability ~verbose ~print_rg ~splitting_debug ta in
let split_reach = splitting ~verbose ~print_rg ta reach in
let rg =Forward_reach.Bfs.to_zone_graph ta split_reach in
if print_rg then Format.printf "%a@." (ZoneGraph.print Common.SBound.print) rg;
(match export_zone_graph with
None -> ()
| Some s -> let f = open_out s in
let ff = formatter_of_out_channel f in
Format.fprintf ff "ptavalue= %a@." (ZoneGraph.print Common.SBound.print) rg;
close_out f);
rg
let input_zone_graph ?verbose:(verbose=1)
?print_rg:(print_rg=false)
?splitting_debug:(splitting_debug="")
?export_zone_graph filename =
let e = Filename.extension filename in
match e with
| ".json" ->
(* Input is already a splitted zone graph *)
if verbose >0 then printf "Reading splitted reachability graph ... ";
let ptavalue = string_of_file filename in
let j = Yojson.Basic.from_string ptavalue in
let zg = ZoneGraph.of_json j in
if verbose >0 then printf "%i states found. [%.2fs]\n" (Array.length zg.ZoneGraph.statelist) (check_time ());
zg
| ".xml" | ".prism" ->
(* Input is a time automaton in prism or UPPAAL file format *)
let ta = try if e = ".xml" then
(* UPPAAL *)
let open TimedAutomaton.Uautomaton in
if verbose >0 then printf "Reading UPPAAL automaton file.";
let pta = UtaReader.nta_from_file filename in
make_ta (guard_of_transition, invariant_of_discrete_state) pta 1 0
else
(* Prism *)
let pmod = PrismTrans.read_prism (open_in filename) filename in
if verbose >0 then printf "Reading Prism automaton file.";
if print_rg then PrismType.print_prism stdout pmod;
Prism_to_ta.ta_from_prism pmod
with x -> eprintf "Fail to build automaton. "; raise x
in
if verbose>0 then printf " [%.2fs]@." (check_time ());
zone_graph_from_ta ~verbose ~print_rg ~splitting_debug ?export_zone_graph ta
| _ -> failwith ("Unkown file extension "^e)
let input_from_string ?(verbose=1)
?(print_rg=false)
?(splitting_debug="")
file_content =
ignore @@ check_time ();
(* Input is a time automaton in prism file format *)
let ta = try
let pmod = PrismTrans.read_from_string file_content in
if verbose >0 then printf "Reading Prism automaton file.";
if print_rg then PrismType.print_prism stdout pmod;
Prism_to_ta.ta_from_prism pmod
with x -> eprintf "Fail to build automaton. "; raise x
in
if verbose>0 then printf " [%.2fs]@." (check_time ());
zone_graph_from_ta ~verbose ~print_rg ~splitting_debug ta
module type BoundType = sig
type t
val zero : t
val print : VarSet.varset -> Format.formatter -> t -> unit
val map : int array -> t -> t
val get_bound : t -> bound
type state = int *float array
val eval_min_bound : state -> t -> float
val eval_max_bound : state -> t -> float
val split_to_zg : Forward_reach.Bfs.Model.timed_automaton ->
(Forward_reach.Bfs.state_space -> Forward_reach.Bfs.state_space) ->
Forward_reach.Bfs.state_space -> (unit, t) ZoneGraph.t
end
module type S = sig
type bt
val input_zone_graph :
?verbose:int ->
?print_rg:bool ->
?splitting_debug:string ->
?export_zone_graph:string ->
string -> (unit, bt) ZoneGraph.t
val input_from_string :
?verbose:int ->
?print_rg:bool ->
?splitting_debug:string ->
string -> (unit, bt) ZoneGraph.t
end
module Make (Bt:BoundType) =
struct
type bt = Bt.t
let zone_graph_from_ta ?(verbose=1)
?(print_rg=false)
?(splitting_debug="")
?export_zone_graph ta =
if print_rg then TimedAutomaton.Uautomaton.print_timed_automaton stdout ta;
let texout,reach = reachability ~verbose ~print_rg ~splitting_debug ta in
let split_reach_fun = splitting ~verbose ~print_rg ta texout in
let rg =Bt.split_to_zg ta split_reach_fun reach in
if print_rg then Format.printf "%a@." (ZoneGraph.print Bt.print) rg;
(match export_zone_graph with
None -> ()
| Some s -> let f = open_out s in
let ff = formatter_of_out_channel f in
Format.fprintf ff "ptavalue= %a@." (ZoneGraph.print Bt.print) rg;
close_out f);
rg
let input_zone_graph ?verbose:(verbose=1)
?print_rg:(print_rg=false)
?splitting_debug:(splitting_debug="")
?export_zone_graph filename =
let e = Filename.extension filename in
match e with
| ".json" ->
(* Input is already a splitted zone graph *)
if verbose >0 then printf "Reading splitted reachability graph ... ";
let ptavalue = string_of_file filename in
let j = Yojson.Basic.from_string ptavalue in
let zg = ZoneGraph.of_json j in
if verbose >0 then printf "%i states found. [%.2fs]\n" (Array.length zg.ZoneGraph.statelist) (check_time ());
(*zg*)
failwith "do not use"
| ".xml" | ".prism" ->
(* Input is a time automaton in prism or UPPAAL file format *)
let ta = try if e = ".xml" then
(* UPPAAL *)
let open TimedAutomaton.Uautomaton in
if verbose >0 then printf "Reading UPPAAL automaton file.";
let pta = UtaReader.nta_from_file filename in
make_ta (guard_of_transition, invariant_of_discrete_state) pta 1 0
else
(* Prism *)
let pmod = PrismTrans.read_prism (open_in filename) filename in
if verbose >0 then printf "Reading Prism automaton file.";
if print_rg then PrismType.print_prism stdout pmod;
Prism_to_ta.ta_from_prism pmod
with x -> eprintf "Fail to build automaton. "; raise x
in
if verbose>0 then printf " [%.2fs]@." (check_time ());
zone_graph_from_ta ~verbose ~print_rg ~splitting_debug ?export_zone_graph ta
| _ -> failwith ("Unkown file extension "^e)
let input_from_string ?(verbose=1)
?(print_rg=false)
?(splitting_debug="")
file_content =
ignore @@ check_time ();
(* Input is a time automaton in prism file format *)
let ta = try
let pmod = PrismTrans.read_from_string file_content in
if verbose >0 then printf "Reading Prism automaton file.";
if print_rg then PrismType.print_prism stdout pmod;
Prism_to_ta.ta_from_prism pmod
with x -> eprintf "Fail to build automaton. "; raise x
in
if verbose>0 then printf " [%.2fs]@." (check_time ());
zone_graph_from_ta ~verbose ~print_rg ~splitting_debug ta
end
......@@ -86,3 +86,4 @@ let eval (_,clocks) = function
| Const a -> float a
| Finite (a,b) -> (float a) -. clocks.(VarSet.int_of_var b-1)
end
......@@ -43,3 +43,4 @@ module SBound : sig
val print : VarSet.varset -> Format.formatter -> bound -> unit
val eval: 'a * float array -> bound -> float
end
......@@ -69,6 +69,8 @@ module ExactReachability (Model : TimedAutomaton.TIMED_AUTOMATON ) =
mutable visited : bool;
}
type state_space = (int, zg_node) Hashtbl.t
let print_edge ta o edge =
Format.fprintf o "([%a],%i-[%c]->%i), " (fun o -> Dbm.pretty_print o (Model.clocks ta)) edge.guard edge.source.id edge.action edge.target.id
let print_zone ta o zgn =
......
......@@ -48,6 +48,7 @@ module SX = Semantic.Make (struct
let get_bound x = x
let eval_max_bound _ _ = 0.0
let eval_min_bound _ _ = 0.0
let split_to_zg _ _ _ = {ZoneGraph.init=0; nb_poly=0; statelist =[||]; var_string=[||]; cardclocks=0; alphabet=[||]; printer = (fun _ _ -> ()) }
end) (PX)
let phi =1.61803398874989484820458683436563
......
......@@ -47,10 +47,41 @@ let precomp_exists =
else printf "Precomputation file found but file have change discard !@.")
!infile !frequency !npoly !rational_impl
module LinearBound = struct
type t = Common.bound
type state = int * float array
let get_bound x = x
let zero = Const 0
let map = Common.SBound.map
let print = Common.SBound.print
let eval_min_bound = Common.SBound.eval
let eval_max_bound = Common.SBound.eval
let split_to_zg ta split taz =
let split_reach = split taz in
Forward_reach.Bfs.to_zone_graph ta split_reach
end
module GeneralBound = struct
type t = Common.bound list
type state = int * float array
let get_bound x = assert false
let zero = [Const 0]
let map v = List.map (Common.SBound.map v)
let print vx f l = List.iter (Common.SBound.print vx f) l
let eval_min_bound st = List.fold_left (fun m b -> min m (Common.SBound.eval st b)) infinity
let eval_max_bound st = List.fold_left (fun m b -> min m (Common.SBound.eval st b)) 0.0
let split_to_zg ta _ taz =
Forward_reach.Bfs.to_zone_graph_no_split ta taz
end
module ZGI = (val if !npoly<0 then (module (ZoneGraphInput.Make (GeneralBound)):ZoneGraphInput.S )
else (module (ZoneGraphInput.Make(LinearBound)):ZoneGraphInput.S ))
(*Building the zone graph *)
let rgopt =
if precomp_exists = None then
Some (ZoneGraphInput.input_zone_graph
Some (ZGI.input_zone_graph
~verbose:!verbose ~print_rg:!print_rg ~splitting_debug:!splitting_debug
?export_zone_graph:!export_zone_graph !infile)
else None
......@@ -69,19 +100,8 @@ module Weight = (val if !frequency =0.0 then (module P:Semantic.WeightStructure)
let svar= P.var_of_int (P.nb_var-1)
end)))
module LinearBound = struct
type t = Common.bound
type state = int * float array
let get_bound x = x
let zero = Const 0
let map = Common.SBound.map
let print = Common.SBound.print
let eval_min_bound = Common.SBound.eval
let eval_max_bound = Common.SBound.eval
end
(* Build the functionnal iterator module based on the polynomial ring *)
module FunIt = Semantic.Make (LinearBound) (Weight)
module FunIt = Semantic.Make (GeneralBound) (Weight)
(* Compute Weight and distribution as polynomials *)
let rgpoly =
......
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