diff options
Diffstat (limited to 'abstract/transform.ml')
| -rw-r--r-- | abstract/transform.ml | 32 |
1 files changed, 2 insertions, 30 deletions
diff --git a/abstract/transform.ml b/abstract/transform.ml index 20512aa..eedec3e 100644 --- a/abstract/transform.ml +++ b/abstract/transform.ml @@ -7,7 +7,8 @@ open Typing open Interpret (* used for constant evaluation ! *) -(* Transform SCADE program to logical formula. +(* Transform SCADE program to logical formula. + See formula.ml for a description of the formula's AST. Convention : to access the last value of a variable, access the variable with the same name prefixed by "L". @@ -527,8 +528,6 @@ let f_of_prog_incl_init rp assume_guarantees = assume_guarantees in f_and clock_eq (f_and no_next_init_cond scope_f) - - (* Get expressions for guarantee violation @@ -583,30 +582,3 @@ and guarantees_of_prog rp = -(* - Extract variables accessed by a LAST -*) - -let rec extract_last_vars = function - | BRel(_, a, b, _) -> - elv_ne a @ elv_ne b - | BEnumCons c -> - elv_ec c - | BAnd(a, b) | BOr (a, b) -> - extract_last_vars a @ extract_last_vars b - | BNot(e) -> extract_last_vars e - | BTernary(c, a, b) -> extract_last_vars c @ - extract_last_vars a @ extract_last_vars b - | _ -> [] - -and elv_ne = function - | NIdent i when i.[0] = 'L' -> [i] - | NBinary(_, a, b, _) -> elv_ne a @ elv_ne b - | NUnary (_, a, _) -> elv_ne a - | _ -> [] - -and elv_ec (_, v, q) = - (if v.[0] = 'L' then [v] else []) @ - (match q with - | EIdent i when i.[0] = 'L' -> [i] - | _ -> []) |