Project

General

Profile

« Previous | Next » 

Revision 6d1693b9

Added by Lélio Brun 7 months ago

work on spec generation almost done

View differences:

src/spec_common.ml
10 10
  | False -> true
11 11
  | _ -> false
12 12

  
13
let rec red = function
14
  | Equal (a, b) when a = b ->
13
let expr_eq: type a b. (a, left_v) expression_t -> (a, b) expression_t -> bool =
14
  fun a b ->
15
  match a, b with
16
  | Var x, Var y -> x = y
17
  | Memory r1, Memory r2 -> r1 = r2
18
  | _ -> false
19

  
20
let rec red: type a. a formula_t -> a formula_t = function
21
  | Equal (a, b) when expr_eq a b ->
15 22
    True
16 23

  
17 24
  | And l ->
......
45 52

  
46 53
  | Exists (x, p) ->
47 54
    let p' = red p in
48
    if is_true p' then True else Exists (x, p')
55
    if is_true p' then True else begin match x with
56
      | [] -> p'
57
      | x -> Exists (x, p')
58
    end
49 59

  
50 60
  | Forall (x, p) ->
51 61
    let p' = red p in
52
    if is_true p' then True else Forall (x, p')
62
    if is_true p' then True else begin match x with
63
      | [] -> p'
64
      | x -> Forall (x, p')
65
    end
53 66

  
54 67
  | Ternary (x, a, b) ->
55 68
    let a' = red a in
......
59 72
  | f -> f
60 73

  
61 74
(* smart constructors *)
62
let mk_condition x l =
63
  if l = tag_true then Ternary (Val x, True, False)
64
  else if l = tag_false then Ternary (Val x, False, True)
65
  else Equal (Val x, Tag l)
75
(* let mk_condition x l =
76
 *   if l = tag_true then Ternary (Val x, True, False)
77
 *   else if l = tag_false then Ternary (Val x, False, True)
78
 *   else Equal (Val x, Tag l) *)
66 79

  
67 80
let vals vs = List.map (fun v -> Val v) vs
68 81

  
69
let mk_pred_call pred vars =
70
  Predicate (pred, vals vars)
71

  
72
let mk_clocked_on id =
73
  mk_pred_call (Clocked_on id)
74

  
75
let mk_transition ?i id =
76
  mk_pred_call (Transition (id, i))
77

  
78
module type SPECVALUE = sig
79
  type t
80
  type ctx
81
  val pp_val: ctx -> Format.formatter -> t -> unit
82
end
83

  
84
module PrintSpec(SV: SPECVALUE) = struct
85

  
86
  open Utils.Format
87

  
88
  let pp_state fmt = function
89
    | In -> pp_print_string fmt "IN"
90
    | Out -> pp_print_string fmt "OUT"
91

  
92
  let pp_expr ctx fmt = function
93
    | Val v -> SV.pp_val ctx fmt v
94
    | Tag t -> pp_print_string fmt t
95
    | Var v -> pp_print_string fmt v.var_id
96
    | Instance (s, i) -> fprintf fmt "%a:%a" pp_state s pp_print_string i
97
    | Memory (s, i) -> fprintf fmt "%a:%a" pp_state s pp_print_string i
98

  
99
  let pp_predicate fmt = function
100
    | Clocked_on x -> fprintf fmt "On<%a>" pp_print_string x
101
    | Transition (f, i) ->
102
      fprintf fmt "Transition<%a>%a"
103
        pp_print_string f
104
        (pp_print_option pp_print_int) i
105
    | Initialization -> ()
106

  
107
  let pp_spec ctx =
108
    let pp_expr = pp_expr ctx in
109
    let rec pp_spec fmt f =
110
      match f with
111
      | True -> pp_print_string fmt "true"
112
      | False -> pp_print_string fmt "false"
113
      | Equal (a, b) ->
114
        fprintf fmt "%a == %a" pp_expr a pp_expr b
115
      | And fs ->
116
        pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt "/\\") pp_spec fmt fs
117
      | Or fs ->
118
        pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt "\\/") pp_spec fmt fs
119
      | Imply (a, b) ->
120
        fprintf fmt "%a -> %a" pp_spec a pp_spec b
121
      | Exists (xs, a) ->
122
        fprintf fmt "∃%a, %a" (pp_print_list Printers.pp_var) xs pp_spec a
123
      | Forall (xs, a) ->
124
        fprintf fmt "∀%a, %a" (pp_print_list Printers.pp_var) xs pp_spec a
125
      | Ternary (e, a, b) ->
126
        fprintf fmt "If %a Then %a Else %a" pp_expr e pp_spec a pp_spec b
127
      | Predicate (p, es) ->
128
        fprintf fmt "%a%a" pp_predicate p (pp_print_parenthesized pp_expr) es
129
    in
130
    pp_spec
131

  
132
end
82
let mk_pred_call pred =
83
  Predicate pred
84

  
85
(* let mk_clocked_on id =
86
 *   mk_pred_call (Clocked_on id) *)
87

  
88
let mk_transition ?i ?inst id inputs locals outputs =
89
  mk_pred_call
90
    (Transition (id, inst, i, vals inputs, vals locals, vals outputs))
91

  
92
let mk_memory_pack ?i ?inst id =
93
  mk_pred_call (MemoryPack (id, inst, i))
94

  
95
let mk_state_variable_pack x =
96
  StateVarPack (StateVar x)
97

  
98
let mk_state_assign_tr x v =
99
  Equal (Memory (StateVar x), Val v)
100

  
101
let mk_conditional_tr v t f =
102
  Ternary (Val v, t, f)
103

  
104
let mk_branch_tr x hl =
105
  And (List.map (fun (t, spec) -> Imply (Equal (Var x, Tag t), spec)) hl)
106

  
107
let mk_assign_tr x v =
108
  Equal (Var x, Val v)
109

  

Also available in: Unified diff