Project

General

Profile

« Previous | Next » 

Revision aaa8e454

Added by LĂ©lio Brun 7 months ago

it works

View differences:

src/spec_types.ml
23 23
type ('a, 'b) expressions_t = ('a, 'b) expression_t list
24 24

  
25 25
type 'a predicate_t =
26
  | Transition: ident * ident option * int option
27
                * ('a, 'b) expressions_t
28
                * ('a, 'b) expressions_t
29
                * ('a, 'b) expressions_t -> 'a predicate_t
26
  | Transition: ident                        (* node name *)
27
                * ident option               (* instance *)
28
                * int option                 (* transition index *)
29
                * ('a, 'b) expressions_t       (* inputs *)
30
                * ('a, 'b) expressions_t       (* locals *)
31
                * ('a, 'b) expressions_t       (* outputs *)
32
                * bool                       (* reset *)
33
                * Utils.ISet.t               (* memory footprint *)
34
      -> 'a predicate_t
35
  | Reset of ident * ident * 'a
30 36
  | MemoryPack of ident * ident option * int option
31 37
  | Initialization
32 38
  | ResetCleared of ident
......
43 49
  | Ternary: ('a, 'b) expression_t * 'a formula_t * 'a formula_t -> 'a formula_t
44 50
  | Predicate: 'a predicate_t -> 'a formula_t
45 51
  | StateVarPack of register_t
46
  | ExistsMem of 'a formula_t * 'a formula_t
52
  | ExistsMem of ident * 'a formula_t * 'a formula_t
47 53

  
48 54
(* type 'a simulation_t = {
49 55
 *   sname: node_desc;
......
64 70
  tlocals: var_decl list;
65 71
  toutputs: var_decl list;
66 72
  tformula: 'a formula_t;
73
  tfootprint: Utils.ISet.t;
67 74
}
68 75

  

Also available in: Unified diff