package electrod

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file Invar_computation.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
(*******************************************************************************
 * electrod - a model finder for relational first-order linear temporal logic
 * 
 * Copyright (C) 2016-2020 ONERA
 * Authors: Julien Brunel (ONERA), David Chemouil (ONERA)
 * 
 * This Source Code Form is subject to the terms of the Mozilla Public
 * License, v. 2.0. If a copy of the MPL was not distributed with this
 * file, You can obtain one at http://mozilla.org/MPL/2.0/.
 * 
 * SPDX-License-Identifier: MPL-2.0
 * License-Filename: LICENSE.md
 ******************************************************************************)

open Containers

type goal_color =
  | Static_prop
  | Primed_prop
  | Invar
  | Init
  | Trans
  | Temporal

let to_string (gc : goal_color) =
  match gc with
  | Static_prop ->
      "Static_prop"
  | Primed_prop ->
      "Primed_prop"
  | Invar ->
      "Invar"
  | Init ->
      "Init"
  | Trans ->
      "Trans"
  | Temporal ->
      "Temporal"


let pp out gc = Fmtc.(pf out "%a" (styled `Yellow string) (to_string gc))

(* Computes the most general color between two colors *)
let max_color c1 c2 =
  match (c1, c2) with
  | Static_prop, Static_prop ->
      Static_prop
  | (Init | Static_prop), (Init | Static_prop) ->
      Init
  | (Primed_prop | Init | Static_prop), (Primed_prop | Init | Static_prop) ->
      Primed_prop
  | (Invar | Static_prop), (Invar | Static_prop) ->
      Invar
  | (Trans | Static_prop), (Trans | Static_prop) ->
      Trans
  | _, _ ->
      Temporal


(* same as max_color, but without Invar nor Trans *)
let max_color_wiwt c1 c2 =
  match (c1, c2) with
  | Static_prop, Static_prop ->
      Static_prop
  | (Init | Static_prop), (Init | Static_prop) ->
      Init
  | (Primed_prop | Init | Static_prop), (Primed_prop | Init | Static_prop) ->
      Primed_prop
  | _, _ ->
      Temporal


let rec remove_always_from_invar (Elo.Fml { node; _ } as fml) =
  let open Elo in
  match node with
  | LUn (G, subfml) ->
      remove_always_from_invar subfml
  | LBin (fml1, And, fml2) ->
      let fml1' = remove_always_from_invar fml1 in
      let fml2' = remove_always_from_invar fml2 in
      lbinary fml1' and_ fml2'
  | _ ->
      fml


let add_always_to_invar (Elo.Fml { node; _ } as fml) =
  let open Elo in
  match node with LUn (G, _) -> fml | _ -> lunary always fml


let is_const (elo : Elo.t) (name : Name.t) =
  assert (Domain.mem name elo.Elo.domain);
  Domain.get_exn name elo.Elo.domain |> Relation.is_const


class ['self] computer (elo : Elo.t) =
  object (_ : 'self)
    inherit ['self] Elo.fold

    method build_fml () f' _ = f'

    method build_Run () blk' = List.fold_left max_color_wiwt Static_prop blk'

    method build_Check () blk' = List.fold_left max_color_wiwt Static_prop blk'

    method build_True () = Static_prop

    method build_False () = Static_prop

    method build_Block () blk_colors =
      List.fold_left max_color Static_prop blk_colors

    method build_FIte () f t e =
      match (f, t, e) with
      | Static_prop, Static_prop, Static_prop ->
          Static_prop
      | (Init | Static_prop), (Init | Static_prop), (Init | Static_prop) ->
          Init
      | ( (Primed_prop | Init | Static_prop)
        , (Primed_prop | Init | Static_prop)
        , (Primed_prop | Init | Static_prop) ) ->
          Primed_prop
      | _, _, _ ->
          Temporal

    method build_Let () __bs' __block' = assert false

    (* SIMPLIFIED *)

    (* quant *)
    method build_Quant () quant' (_, _, range_color) blk_colors =
      let blk_color = List.fold_left max_color_wiwt Static_prop blk_colors in
      let sim_binding_color = max_color_wiwt Static_prop range_color in
      quant' sim_binding_color blk_color

    method build_All () = max_color

    method build_No () = max_color

    method build_Some_ () = max_color

    (* lbinop *)
    method build_LBin () f1' op' f2' = op' f1' f2'

    method build_And () = max_color

    method build_Iff () = max_color_wiwt

    method build_Imp () = max_color_wiwt

    method build_U () _ _ = Temporal

    method build_Or () = max_color_wiwt

    method build_R () _ _ = Temporal

    method build_S () _ _ = Temporal

    method build_T () _ _ = Temporal

    (* lunop *)
    method build_LUn () op' f' = op' f'

    method build_X () f' =
      match f' with Static_prop | Init -> Primed_prop | _ -> Temporal

    method build_F () _ = Temporal

    method build_G () f' =
      match f' with
      | Init | Static_prop | Invar ->
          Invar
      | Primed_prop | Trans ->
          Trans
      | _ ->
          Temporal

    method build_H () _ = Temporal

    method build_O () _ = Temporal

    method build_P () _ = Temporal

    method build_Not () f' = max_color_wiwt Static_prop f'

    (* compo_op *)
    method build_RComp () f1' op' f2' = op' f1' f2'

    method build_REq () = max_color_wiwt

    method build_In () = max_color_wiwt

    method build_NotIn () = max_color_wiwt

    method build_RNEq () = max_color_wiwt

    (* icomp_op *)
    method build_IComp () e1' op' e2' = op' e1' e2'

    method build_Gt () = max_color_wiwt

    method build_Gte () = max_color_wiwt

    method build_IEq () = max_color_wiwt

    method build_INEq () = max_color_wiwt

    method build_Lt () = max_color_wiwt

    method build_Lte () = max_color_wiwt

    (************************** exp  ********************************)
    method build_exp () pe' _ _ = pe'

    method build_oexp () color _ = color

    method build_Compr () sbs' b' =
      let blk_color = List.fold_left max_color_wiwt Static_prop b' in
      let max_color_for_simbindings
          (color_acc : goal_color)
          ((__disj1, __vars1, e1) : bool * int * goal_color) =
        max_color_wiwt color_acc e1
      in
      let sim_bindings_color =
        List.fold_left max_color_for_simbindings Static_prop sbs'
      in
      max_color_wiwt sim_bindings_color blk_color

    method build_Iden () = Static_prop

    method build_Name () r = if is_const elo r then Static_prop else Init

    method build_Var () __id = Static_prop

    method build_None_ () = Static_prop

    method build_Univ () = Static_prop

    method build_Prime () f' =
      match f' with Static_prop | Init -> Primed_prop | _ -> Temporal

    method build_RIte () f' t' e' =
      match (f', t', e') with
      | Static_prop, Static_prop, Static_prop ->
          Static_prop
      | (Init | Static_prop), (Init | Static_prop), (Init | Static_prop) ->
          Init
      | ( (Primed_prop | Init | Static_prop)
        , (Primed_prop | Init | Static_prop)
        , (Primed_prop | Init | Static_prop) ) ->
          Primed_prop
      | _, _, _ ->
          Temporal

    (* rbinop *)
    method build_RBin () f1' op' f2' = op' f1' f2'

    method build_Union () = max_color_wiwt

    method build_Inter () = max_color_wiwt

    method build_Join () = max_color_wiwt

    method build_LProj () = max_color_wiwt

    method build_Prod () = max_color_wiwt

    method build_RProj () = max_color_wiwt

    method build_Diff () = max_color_wiwt

    method build_Over () = max_color_wiwt

    (* runop *)
    method build_RUn () op' e' = op' e'

    method build_RTClos () = Fun.id

    method build_Transpose () = Fun.id

    method build_TClos () = Fun.id

    (*********************************** iexp **************************************)
    method build_iexp () iexp' _ = iexp'

    method build_IBin () i1' op' i2' = op' i1' i2'

    method build_IUn () op' i' = op' i'

    method build_Num () _ = Static_prop

    method build_Add () = max_color_wiwt

    method build_Neg () = max_color_wiwt Static_prop

    method build_Sub () = max_color_wiwt

    method build_Card () r' = r'
  end

(* Computes the color (Invar, Static_prop, Init or Temporal) of an
     elo formula *)
let color elo elo_fml = (new computer elo)#visit_fml () elo_fml
OCaml

Innovation. Community. Security.