Commit 0bbd0c43 authored by Benoit Barbot's avatar Benoit Barbot
Browse files

improve modelconvert

parent b3a6ac10
Pipeline #1321 failed with stages
in 3 minutes and 8 seconds
...@@ -6,7 +6,7 @@ o : [0..2] init 0; ...@@ -6,7 +6,7 @@ o : [0..2] init 0;
x : clock; x : clock;
y : clock; y : clock;
invariant invariant
((o=0) | (o=1)) => (x<5)&(y<3) (x<5)&(y<3)
endinvariant endinvariant
[a] (o=0) & (y<=1) -> (y'=0); [a] (o=0) & (y<=1) -> (y'=0);
......
...@@ -132,6 +132,9 @@ def WeightsPdfCdf(f): #Compute one iteration of operator Op with all weights/pdf ...@@ -132,6 +132,9 @@ def WeightsPdfCdf(f): #Compute one iteration of operator Op with all weights/pdf
pdf=R(0); pdf=R(0);
pol=integral(pdf,t); pol=integral(pdf,t);
z=trans['zone']; z=trans['zone'];
low = z[0]-clockO(x,i,z[1]);
#print("state:%i" %i);
#print(low);
cdf=pol - pol(t=z[0]-clockO(x,i,z[1])); cdf=pol - pol(t=z[0]-clockO(x,i,z[1]));
weight=pol(t=z[2]-clockO(x,i,z[3]))-pol(t=z[0]-clockO(x,i,z[1])); weight=pol(t=z[2]-clockO(x,i,z[3]))-pol(t=z[0]-clockO(x,i,z[1]));
psiDeltaf[i][j]=psiDeltaf[i][j]+(edge['prob'])*weight; psiDeltaf[i][j]=psiDeltaf[i][j]+(edge['prob'])*weight;
......
open Type open Type
type expType = IntT | BoolT | DoubleT | IntVar | BoolVar | FunT | Clock type expType = IntT | BoolT | DoubleT | IntVar | BoolVar | FunT | Clock
let allInt = ref false let allInt = ref false
let allReal = ref false let allReal = ref false
let (mapType:expType StringMap.t ref) = ref let (mapType:expType StringMap.t ref) = ref
(StringMap.empty (StringMap.empty
|> StringMap.add "min" FunT |> StringMap.add "min" FunT
|> StringMap.add "max" FunT) |> StringMap.add "max" FunT)
let add_int s = let add_int s =
(*Printf.printf "add int var %s\n" s;*) (*Printf.printf "add int var %s\n" s;*)
mapType := StringMap.add s IntT !mapType mapType := StringMap.add s IntT !mapType
let add_bool s = mapType := StringMap.add s BoolT !mapType let add_bool s = mapType := StringMap.add s BoolT !mapType
let add_double s = mapType := StringMap.add s DoubleT !mapType let add_double s = mapType := StringMap.add s DoubleT !mapType
let add_var s t = mapType := StringMap.add s t !mapType let add_var s t = mapType := StringMap.add s t !mapType
let add_copy s1 s2 = try let t = StringMap.find s1 !mapType in let add_copy s1 s2 = try let t = StringMap.find s1 !mapType in
mapType := StringMap.add s2 t !mapType mapType := StringMap.add s2 t !mapType
with Not_found -> () with Not_found -> ()
let find_action sl = let find_action sl =
...@@ -31,24 +31,24 @@ type update = IntUp of int expr' | BoolUp of bool expr' ...@@ -31,24 +31,24 @@ type update = IntUp of int expr' | BoolUp of bool expr'
let print_update f = function let print_update f = function
| IntUp i -> printH_expr f i | IntUp i -> printH_expr f i
| BoolUp b -> printH_expr f b | BoolUp b -> printH_expr f b
type varKind = IntK of string * (int expr'*int expr') * int expr' type varKind = IntK of string * (int expr'*int expr') * int expr'
| BoolK of string * (int expr'*int expr') * int expr' | BoolK of string * (int expr'*int expr') * int expr'
| ClockK of string | ClockK of string
module Guard = struct module Guard = struct
type sing = string * Type.cmp * int Type.expr' type sing = string * Type.cmp * int Type.expr'
type conj = (Type.cmp * int Type.expr') list StringMap.t type conj = (Type.cmp * int Type.expr') list StringMap.t
type t = conj list type t = conj list
let fold f s c = let fold f s c =
StringMap.fold (fun v vl s2 -> StringMap.fold (fun v vl s2 ->
List.fold_left (fun s3 (cmp,expr) -> List.fold_left (fun s3 (cmp,expr) ->
f s3 (v,cmp,expr) f s3 (v,cmp,expr)
) s2 vl ) s2 vl
) c s ) c s
let map f c = let map f c =
StringMap.fold (fun v vl nsm -> StringMap.fold (fun v vl nsm ->
let nv = ref v in let nv = ref v in
...@@ -57,24 +57,24 @@ module Guard = struct ...@@ -57,24 +57,24 @@ module Guard = struct
nv := v2;(cmp2,expr2)) vl in nv := v2;(cmp2,expr2)) vl in
StringMap.add !nv nl nsm StringMap.add !nv nl nsm
) c StringMap.empty ) c StringMap.empty
let to_list g = let to_list g =
fold (fun l x -> x::l) [] g fold (fun l x -> x::l) [] g
let iter f g = let iter f g =
fold (fun () a -> f a) () g fold (fun () a -> f a) () g
let print_conj f conj = let print_conj f conj =
ignore @@ fold (fun b (v,cmp,expr) -> ignore @@ fold (fun b (v,cmp,expr) ->
Printf.fprintf f "%s %s %a %a " (if b then "" else "&") v printH_cmp cmp printH_expr expr; false) true conj Printf.fprintf f "%s %s %a %a " (if b then "" else "&") v printH_cmp cmp printH_expr expr; false) true conj
let print f g = let print f g =
g |> print_list2 (fun _ conj -> g |> print_list2 (fun _ conj ->
Printf.fprintf f "( "; Printf.fprintf f "( ";
print_conj f conj; print_conj f conj;
Printf.fprintf f " )"; Printf.fprintf f " )";
) " | " f ) " | " f
let simplify_conj c = let simplify_conj c =
try try
StringMap.map (fun l -> StringMap.map (fun l ->
...@@ -99,21 +99,21 @@ module Guard = struct ...@@ -99,21 +99,21 @@ module Guard = struct
| (SG, Int i1)::(SL, i2) :: q -> | (SG, Int i1)::(SL, i2) :: q ->
(SG, Int i1) :: (SL, i2)::q (SG, Int i1) :: (SL, i2)::q
| x -> Printf.printf "strange guard: "; | x -> Printf.printf "strange guard: ";
ignore @@ List.fold_left (fun b (cmp,expr) -> ignore @@ List.fold_left (fun b (cmp,expr) ->
Printf.fprintf stdout "%s %s %a %a " (if b then "" else "&") "var" printH_cmp cmp printH_expr expr; false) true x ; Printf.fprintf stdout "%s %s %a %a " (if b then "" else "&") "var" printH_cmp cmp printH_expr expr; false) true x ;
Printf.printf "\n"; x Printf.printf "\n"; x
) )
) c ) c
|> fun x -> Some x |> fun x -> Some x
with Not_found -> None with Not_found -> None
let simplify g = let simplify g =
List.fold_left (fun acc c -> match simplify_conj c with List.fold_left (fun acc c -> match simplify_conj c with
Some c2 -> c2::acc Some c2 -> c2::acc
| None -> acc) [] g | None -> acc) [] g
let conj g1 g2 = let conj g1 g2 =
List.fold_left (fun acc c1 -> List.fold_left (fun acc c1 ->
acc@( List.map (fun c2-> acc@( List.map (fun c2->
...@@ -121,34 +121,38 @@ module Guard = struct ...@@ -121,34 +121,38 @@ module Guard = struct
) g2 ) g2
|> simplify ) |> simplify )
) [] g1 ) [] g1
let rec flatten x = let rec flatten x =
let nb (v,cmp,i) = StringMap.singleton v [cmp,i] in let nb (v,cmp,i) = StringMap.singleton v [cmp,i] in
match x with match x with
| Bool true -> [ StringMap.empty ] | Bool true -> [ StringMap.empty ]
| Bool false -> [] | Bool false -> []
| And (e1,e2) -> | And (e1,e2) ->
let l= flatten e1 let l= flatten e1
and l2 = flatten e2 in and l2 = flatten e2 in
conj l l2 conj l l2
| Or (e1,e2) -> (flatten e1)@(flatten e2) | Or (e1,e2) -> (flatten e1)@(flatten e2)
| IntAtom ((IntName v),NEQ,j) -> [nb (v,SL,j);nb (v,SG,j)] | IntAtom ((IntName v),NEQ,j) -> [nb (v,SL,j);nb (v,SG,j)]
| IntAtom ((IntName v),cmp,j) -> [nb (v,cmp,j)] | IntAtom ((IntName v),cmp,j) -> [nb (v,cmp,j)]
| FloatAtom ((CastInt (IntName v)),SL,j) -> [nb (v,SL,Ceil j)] | FloatAtom ((CastInt (IntName v)),SL,j) -> [nb (v,SL,Ceil j)]
| FloatAtom ((CastInt (IntName v)),LE,j) -> [nb (v,LE,Ceil j)] | FloatAtom ((CastInt (IntName v)),LE,j) -> [nb (v,LE,Ceil j)]
| FloatAtom ((CastInt (IntName v)),SG,j) -> [nb (v,SG,Floor j)] | FloatAtom ((CastInt (IntName v)),SG,j) -> [nb (v,SG,Floor j)]
| FloatAtom ((CastInt (IntName v)),GE,j) -> [nb (v,GE,Floor j)] | FloatAtom ((CastInt (IntName v)),GE,j) -> [nb (v,GE,Floor j)]
| BoolName v -> [nb (v,SG,Int 0)] | BoolName v -> [nb (v,SG,Int 0)]
| Not (BoolName v) -> [nb (v,EQ,Int 0)] | Not (BoolName v) -> [nb (v,EQ,Int 0)]
| Not e -> flatten (neg_bool e) | Not e -> flatten (neg_bool e)
| FloatAtom (FloatName v, SL,j) -> [nb (v,SL,Ceil j)]
| FloatAtom (FloatName v, LE,j) -> [nb (v,LE,Ceil j)]
| FloatAtom (FloatName v,SG,j) -> [nb (v,SG,Floor j)]
| FloatAtom (FloatName v,GE,j) -> [nb (v,GE,Floor j)]
| e-> printH_expr stderr e; | e-> printH_expr stderr e;
failwith "Not yet supported guard shape" failwith "Not yet supported guard shape"
end end
type rule = string option * Guard.t * (( float expr' * ((string*update) list)) list) type rule = string option * Guard.t * (( float expr' * ((string*update) list)) list)
type prism_module = { type prism_module = {
name:string; name:string;
varlist: varKind list; varlist: varKind list;
...@@ -160,7 +164,7 @@ type moduledef = Full of prism_module | Renaming of string*string*(string*string ...@@ -160,7 +164,7 @@ type moduledef = Full of prism_module | Renaming of string*string*(string*string
type modelKind = DTMC | MDP | CTMC | PTA type modelKind = DTMC | MDP | CTMC | PTA
type labels = (string*(bool Type.expr')) list type labels = (string*(bool Type.expr')) list
type prism_file = { type prism_file = {
consts: constdef; consts: constdef;
modlist: moduledef list; modlist: moduledef list;
...@@ -169,19 +173,20 @@ type prism_file = { ...@@ -169,19 +173,20 @@ type prism_file = {
formulas: (string*full_expr) list; formulas: (string*full_expr) list;
} }
let print_prism_mod f m = let print_prism_mod f m =
Printf.fprintf f "module %s\n" m.name; Printf.fprintf f "module %s\n" m.name;
List.iter (function List.iter (function
| IntK(s,(l,m),init) -> | IntK(s,(l,m),init) ->
Printf.fprintf f "\t%s: [%a..%a] init %a;\n" s printH_expr l printH_expr m printH_expr init; Printf.fprintf f "\t%s: [%a..%a] init %a;\n" s printH_expr l printH_expr m printH_expr init;
| ClockK (s)-> Printf.fprintf f "\t%s: clock;\n" s;
| _ -> failwith "unsupported" | _ -> failwith "unsupported"
) m.varlist; ) m.varlist;
List.iter (fun (sto,guard, taillist ) -> List.iter (fun (sto,guard, taillist ) ->
Printf.fprintf f "\t[%s] %a -> " (sto |>>| "") Guard.print guard; Printf.fprintf f "\t[%s] %a -> " (sto |>>| "") Guard.print guard;
ignore @@ List.fold_left (fun b (prob,update) -> ignore @@ List.fold_left (fun b (prob,update) ->
if b then Printf.fprintf f " + "; if b then Printf.fprintf f " + ";
Printf.fprintf f "%a :" printH_expr prob; Printf.fprintf f "%a :" printH_expr prob;
...@@ -194,9 +199,9 @@ let print_prism_mod f m = ...@@ -194,9 +199,9 @@ let print_prism_mod f m =
) false taillist; ) false taillist;
Printf.fprintf f ";\n"; Printf.fprintf f ";\n";
) m.actionlist; ) m.actionlist;
Printf.fprintf f "endmodule\n" Printf.fprintf f "endmodule\n"
let print_prism f p = let print_prism f p =
let passocfo fo s (n,e) = Printf.fprintf f "%s \"%s\" = %a\n" s n fo e in let passocfo fo s (n,e) = Printf.fprintf f "%s \"%s\" = %a\n" s n fo e in
let passoc s (n,e) = passocfo printH_expr s (n,e) in let passoc s (n,e) = passocfo printH_expr s (n,e) in
......
...@@ -3,7 +3,7 @@ ...@@ -3,7 +3,7 @@
mkdir -p ../bin mkdir -p ../bin
rm -rf tmp rm -rf tmp
#ocamlbuild -use-ocamlfind -j 4 -pp "camlp4o pa_macro.cmo -DHAS_XML -DHAS_ZIP" -I ClessParser prism2SPT.native modelConvert.native parserUnparseAttribute.native #ocamlbuild -use-ocamlfind -j 4 -pp "camlp4o pa_macro.cmo -DHAS_XML -DHAS_ZIP" -I ClessParser prism2SPT.native modelConvert.native parserUnparseAttribute.native
ocamlbuild -use-ocamlfind -j 4 -I ClessParser -I Prism -I Semantics prism2SPT.native StochasticPetriNet.cmo SemanticPT.cmo StochasticSymmetricNet.cmo modelConvert.native stochasticBound.native parserUnparseAttribute.native modelConvert.byte CosmosSimulink.native ocamlbuild -use-ocamlfind -j 4 -I ClessParser -I Prism -I Semantics prism2SPT.native StochasticPetriNet.cmo SemanticPT.cmo StochasticSymmetricNet.cmo modelConvert.native stochasticBound.native parserUnparseAttribute.native modelConvert.byte CosmosSimulink.native prismTrans.cma prismTrans.cmxa
ocamlmktop -o petriscript -I _build str.cma type.cmo Prism/prismType.cmo Prism/parserPrism.cmo Prism/lexerPrism.cmo PetriNet.cmo StochPTPrinter.cmo Semantics/SemanticPT.cmo StochasticPetriNet.cmo StochasticSymmetricNet.cmo ocamlmktop -o petriscript -I _build str.cma type.cmo Prism/prismType.cmo Prism/parserPrism.cmo Prism/lexerPrism.cmo PetriNet.cmo StochPTPrinter.cmo Semantics/SemanticPT.cmo StochasticPetriNet.cmo StochasticSymmetricNet.cmo
......
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