prismType.ml 7.54 KB
Newer Older
Benoit Barbot's avatar
Benoit Barbot committed
1
open Type
Benoit Barbot's avatar
in prog  
Benoit Barbot committed
2

Benoit Barbot's avatar
Benoit Barbot committed
3
type expType = IntT | BoolT | DoubleT | IntVar | BoolVar | FunT | Clock
Benoit Barbot's avatar
Benoit Barbot committed
4 5 6 7

let allInt = ref false
let allReal = ref false

Benoit Barbot's avatar
Benoit Barbot committed
8
let (mapType:expType StringMap.t ref) = ref
Benoit Barbot's avatar
change  
Benoit Barbot committed
9 10 11
  (StringMap.empty
      |> StringMap.add "min" FunT
      |> StringMap.add "max" FunT)
12

Benoit Barbot's avatar
Benoit Barbot committed
13
let add_int s =
Benoit Barbot's avatar
in prog  
Benoit Barbot committed
14 15 16 17
  (*Printf.printf "add int var %s\n" s;*)
  mapType := StringMap.add s IntT !mapType
let add_bool s = mapType := StringMap.add s BoolT !mapType
let add_double s = mapType := StringMap.add s DoubleT !mapType
18
let add_var s t = mapType := StringMap.add s t !mapType
Benoit Barbot's avatar
in prog  
Benoit Barbot committed
19
let add_copy s1 s2 = try let t = StringMap.find s1 !mapType in
Benoit Barbot's avatar
Benoit Barbot committed
20
                     mapType := StringMap.add s2 t !mapType
Benoit Barbot's avatar
in prog  
Benoit Barbot committed
21 22 23
  with Not_found -> ()

let find_action sl =
Benoît Barbot's avatar
pb  
Benoît Barbot committed
24
  List.fold_left (fun set (so,_,_) ->
Benoit Barbot's avatar
in prog  
Benoit Barbot committed
25 26 27
    match so with None -> set
      | Some a -> StringSet.add a set) StringSet.empty sl

Benoit Barbot's avatar
Benoit Barbot committed
28
type constdef = (string*(int expr' option)) list * (string*(float expr' option)) list
Benoit Barbot's avatar
in prog  
Benoit Barbot committed
29

30 31
type update = IntUp of int expr' | BoolUp of  bool expr'

Benoît Barbot's avatar
Benoît Barbot committed
32 33
let print_update f = function
  | IntUp i -> printH_expr f i
Benoit Barbot's avatar
Benoit Barbot committed
34 35
  | BoolUp b -> printH_expr f b

Benoit Barbot's avatar
Benoit Barbot committed
36
type varKind = IntK of string * (int expr'*int expr') * int expr'
Benoit Barbot's avatar
Benoit Barbot committed
37 38
               | BoolK of string * (int expr'*int expr') * int expr'
               | ClockK of string
Benoit Barbot's avatar
Benoit Barbot committed
39

Benoit Barbot's avatar
Benoit Barbot committed
40
module Guard = struct
Benoit Barbot's avatar
Benoit Barbot committed
41 42 43
  type sing = string * Type.cmp * int Type.expr'
  type conj = (Type.cmp * int Type.expr') list StringMap.t
  type t = conj list
Benoit Barbot's avatar
Benoit Barbot committed
44

Benoit Barbot's avatar
Benoit Barbot committed
45 46 47 48
  let fold f s c =
    StringMap.fold (fun v vl s2 ->
        List.fold_left (fun s3 (cmp,expr) ->
            f s3 (v,cmp,expr)
Benoit Barbot's avatar
Benoit Barbot committed
49
          ) s2 vl
Benoit Barbot's avatar
Benoit Barbot committed
50
      ) c s
Benoit Barbot's avatar
Benoit Barbot committed
51

Benoit Barbot's avatar
Benoit Barbot committed
52 53 54 55 56 57 58 59
  let map f c =
    StringMap.fold (fun v vl nsm ->
        let nv = ref v in
        let nl = List.map (fun (cmp,expr) ->
                     let v2,cmp2,expr2 = f (v,cmp,expr) in
                     nv := v2;(cmp2,expr2)) vl in
        StringMap.add !nv nl nsm
      ) c StringMap.empty
Benoit Barbot's avatar
Benoit Barbot committed
60

Benoit Barbot's avatar
Benoit Barbot committed
61 62
  let to_list g =
    fold (fun l x -> x::l) [] g
Benoit Barbot's avatar
Benoit Barbot committed
63

Benoit Barbot's avatar
Benoit Barbot committed
64 65
  let iter f g =
    fold (fun () a -> f a) () g
Benoît Barbot's avatar
Benoît Barbot committed
66 67 68 69

  let print_conj f conj =
    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
Benoit Barbot's avatar
Benoit Barbot committed
70

Benoit Barbot's avatar
Benoit Barbot committed
71 72 73
  let print f g =
    g |> print_list2 (fun _ conj ->
             Printf.fprintf f "( ";
Benoît Barbot's avatar
Benoît Barbot committed
74
             print_conj f conj;
Benoit Barbot's avatar
Benoit Barbot committed
75 76
             Printf.fprintf f " )";
           ) " | " f
Benoit Barbot's avatar
Benoit Barbot committed
77

Benoit Barbot's avatar
Benoit Barbot committed
78 79 80 81 82
  let simplify_conj c =
    try
      StringMap.map (fun l ->
          List.sort_uniq (fun (cmp1,v1) (cmp2,v2) -> if cmp1 = cmp2 then compare v1 v2 else
                                                       compare cmp1 cmp2) l
Benoit Barbot's avatar
Benoit Barbot committed
83 84 85 86
          |> (function
              | [] -> []
              | x :: [] -> x :: []
              | (EQ, Int i1) :: (EQ, Int i2)::_ when i1 !=i2 -> raise Not_found
Benoit Barbot's avatar
Benoit Barbot committed
87 88
              | (EQ, Int i1) :: (SG, Int i2)::_ when i1 <= i2 -> raise Not_found
              | (EQ, Int i1) :: (SG, Int i2)::q -> (EQ, Int i1)::q
Benoit Barbot's avatar
Benoit Barbot committed
89 90 91 92 93 94
              | (EQ, Int i1) :: (SL, Int i2)::_ when i1 >= i2 -> raise Not_found
              | (EQ, Int i1) :: (SL, Int i2)::q -> (EQ, Int i1)::q
              | (EQ, Int i1) :: (GE, Int i2)::_ when i1 < i2 -> raise Not_found
              | (EQ, Int i1) :: (GE, Int i2)::q -> (EQ, Int i1)::q
              | (EQ, Int i1) :: (LE, Int i2)::_ when i1 > i2 -> raise Not_found
              | (EQ, Int i1) :: (LE, Int i2)::q -> (EQ, Int i1)::q
Benoit Barbot's avatar
Benoit Barbot committed
95

Benoît Barbot's avatar
Benoît Barbot committed
96
              | (SL, Int i2)::(SG, Int i1) :: _ when i1>=i2 -> raise Not_found
97 98 99 100
              | (SL, i2)::(SG, Int i1) ::  q ->
                 (SG, Int i1) :: (SL, i2)::q
              | (SG, Int i1)::(SL, i2) ::  q ->
                 (SG, Int i1) :: (SL, i2)::q
Benoît Barbot's avatar
Benoît Barbot committed
101

Benoit Barbot's avatar
Benoit Barbot committed
102

Benoît Barbot's avatar
Benoît Barbot committed
103 104 105 106
              | x -> Printf.printf "strange guard: ";
                 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.printf "\n"; x
Benoit Barbot's avatar
Benoit Barbot committed
107 108
             )
        ) c
Benoit Barbot's avatar
Benoit Barbot committed
109 110
    |> fun x -> Some x
    with Not_found -> None
Benoit Barbot's avatar
Benoit Barbot committed
111 112 113 114 115

  let simplify g =
    List.fold_left (fun acc c -> match simplify_conj c with
                                   Some c2 -> c2::acc
                                 | None -> acc) [] g
Benoit Barbot's avatar
Benoit Barbot committed
116

Benoit Barbot's avatar
Benoit Barbot committed
117 118 119 120 121 122 123
  let conj g1 g2 =
    List.fold_left (fun acc c1 ->
        acc@( List.map (fun c2->
                  c2 |> StringMap.union (fun v b1 b2 -> Some (b1@b2)) c1
                ) g2
              |> simplify )
      ) [] g1
Benoit Barbot's avatar
Benoit Barbot committed
124

Benoit Barbot's avatar
Benoit Barbot committed
125
  let rec flatten x =
Benoit Barbot's avatar
Benoit Barbot committed
126
    let nb (v,cmp,i) = StringMap.singleton v [cmp,i] in
Benoit Barbot's avatar
Benoit Barbot committed
127 128 129 130
    match x with
    | Bool true -> [ StringMap.empty ]
    | Bool false -> []
    | And (e1,e2) ->
Benoit Barbot's avatar
Benoit Barbot committed
131
       let l= flatten e1
Benoit Barbot's avatar
Benoit Barbot committed
132 133 134 135
                and l2 = flatten e2 in
       conj l l2
    | Or (e1,e2) -> (flatten e1)@(flatten e2)
    | IntAtom ((IntName v),NEQ,j) -> [nb (v,SL,j);nb (v,SG,j)]
Benoit Barbot's avatar
Benoit Barbot committed
136
    | IntAtom ((IntName v),cmp,j) -> [nb (v,cmp,j)]
Benoit Barbot's avatar
Benoit Barbot committed
137 138 139 140
    | 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)),SG,j) -> [nb (v,SG,Floor j)]
    | FloatAtom ((CastInt (IntName v)),GE,j) -> [nb (v,GE,Floor j)]
Benoit Barbot's avatar
Benoit Barbot committed
141

Benoit Barbot's avatar
Benoit Barbot committed
142 143 144
    | BoolName v -> [nb (v,SG,Int 0)]
    | Not (BoolName v) -> [nb (v,EQ,Int 0)]
    | Not e -> flatten (neg_bool e)
Benoit Barbot's avatar
Benoit Barbot committed
145 146 147 148
    | 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)]
Benoit Barbot's avatar
Benoit Barbot committed
149 150
    | e-> printH_expr stderr e;
          failwith "Not yet supported guard shape"
Benoit Barbot's avatar
Benoit Barbot committed
151

Benoit Barbot's avatar
Benoit Barbot committed
152
end
Benoît Barbot's avatar
pb  
Benoît Barbot committed
153

Benoit Barbot's avatar
Benoit Barbot committed
154 155
type rule = string option * Guard.t * (( float expr' * ((string*update) list)) list)

Benoit Barbot's avatar
in prog  
Benoit Barbot committed
156 157
type prism_module = {
  name:string;
Benoit Barbot's avatar
Benoit Barbot committed
158
  varlist: varKind list;
Benoît Barbot's avatar
pb  
Benoît Barbot committed
159
  actionlist: rule list ;
Benoit Barbot's avatar
in prog  
Benoit Barbot committed
160 161 162 163 164
  actionset: StringSet.t
}

type moduledef = Full of prism_module | Renaming of string*string*(string*string) list

Benoît Barbot's avatar
pb  
Benoît Barbot committed
165
type modelKind = DTMC | MDP | CTMC | PTA
Benoît Barbot's avatar
Benoît Barbot committed
166
type labels = (string*(bool Type.expr')) list
Benoit Barbot's avatar
Benoit Barbot committed
167

Benoît Barbot's avatar
Benoît Barbot committed
168 169 170 171 172
type prism_file = {
    consts: constdef;
    modlist: moduledef list;
    kind: modelKind;
    labels: labels;
Benoît Barbot's avatar
Benoît Barbot committed
173
    formulas: (string*full_expr) list;
Benoît Barbot's avatar
Benoît Barbot committed
174
  }
Benoît Barbot's avatar
Benoît Barbot committed
175

Benoit Barbot's avatar
Benoit Barbot committed
176

Benoît Barbot's avatar
Benoît Barbot committed
177
let print_prism_mod f m =
Benoît Barbot's avatar
Benoît Barbot committed
178 179 180 181 182
  Printf.fprintf f "module %s\n" m.name;

  List.iter (function
   | 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;
Benoit Barbot's avatar
Benoit Barbot committed
183
   | ClockK (s)-> Printf.fprintf f "\t%s: clock;\n" s;
Benoît Barbot's avatar
Benoît Barbot committed
184 185 186
   | _ -> failwith "unsupported"
            ) m.varlist;

Benoit Barbot's avatar
Benoit Barbot committed
187
  List.iter (fun (sto,guard, taillist ) ->
Benoît Barbot's avatar
pb  
Benoît Barbot committed
188
      Printf.fprintf f "\t[%s] %a -> " (sto |>>| "") Guard.print guard;
Benoit Barbot's avatar
Benoit Barbot committed
189

Benoît Barbot's avatar
pb  
Benoît Barbot committed
190 191 192 193 194 195 196 197 198 199
      ignore @@ List.fold_left (fun b (prob,update) ->
                    if b then Printf.fprintf f " + ";
                    Printf.fprintf f "%a :" printH_expr prob;
                    ignore @@ List.fold_left (fun b (s,u) ->
                                  if b then Printf.fprintf f " & ";
                                  Printf.fprintf f "(%s'=%a)" s print_update u;
                                  true
                                ) false update;
                    true
                  ) false taillist;
Benoît Barbot's avatar
Benoît Barbot committed
200 201
    Printf.fprintf f ";\n";
    ) m.actionlist;
Benoit Barbot's avatar
Benoit Barbot committed
202

Benoît Barbot's avatar
Benoît Barbot committed
203
  Printf.fprintf f "endmodule\n"
Benoit Barbot's avatar
Benoit Barbot committed
204

Benoît Barbot's avatar
Benoît Barbot committed
205
let print_prism f p =
Benoît Barbot's avatar
Benoît Barbot committed
206 207
  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
Benoît Barbot's avatar
Benoît Barbot committed
208 209 210 211 212
  List.iter (function (n,Some e) -> passoc "const int" (n,e)
                    | (n,None) ->Printf.fprintf f "const int %s\n" n) (fst p.consts);
  List.iter (function (n,Some e) -> passoc "const double" (n,e)
            | (n,None) ->Printf.fprintf f "const double %s\n" n) (snd p.consts);
  List.iter (function Full pm -> print_prism_mod !logout pm |_ -> ()) p.modlist;
Benoît Barbot's avatar
Benoît Barbot committed
213 214
  List.iter (passoc "label") p.labels;
  List.iter (passocfo print_full_expr "formula") p.formulas