Project

General

Profile

Download (1.62 KB) Statistics
| Branch: | Tag: | Revision:
1
open Utils
2
open Lustre_types
3

    
4
type register_t = ResetFlag | StateVar of var_decl
5

    
6
type 'a expression_t =
7
  | Val of 'a
8
  | Tag of ident * Types.t
9
  | Var of var_decl
10
  | Memory of register_t
11

    
12
type 'a predicate_t =
13
  | Transition :
14
      bool (* stateless *)
15
      * ident (* node name *)
16
      * ident option
17
      (* instance *)
18
      * int option
19
      (* transition index *)
20
      * 'a expression_t list
21
      (* variables *)
22
      * bool (* reset *)
23
      * Utils.ISet.t (* memory footprint *)
24
      * ident Utils.IMap.t
25
      (* memory instances footprint *)
26
      -> 'a predicate_t
27
  | Reset of ident * ident * 'a
28
  | MemoryPack of ident * ident option * int option
29
  | Initialization
30
  | ResetCleared of ident
31

    
32
type 'a formula_t =
33
  | True
34
  | False
35
  | Equal of 'a expression_t * 'a expression_t
36
  | GEqual of 'a expression_t * 'a expression_t
37
  | And of 'a formula_t list
38
  | Or of 'a formula_t list
39
  | Imply of 'a formula_t * 'a formula_t
40
  | Exists of var_decl list * 'a formula_t
41
  | Forall of var_decl list * 'a formula_t
42
  | Ternary of 'a expression_t * 'a formula_t * 'a formula_t
43
  | Predicate : 'a predicate_t -> 'a formula_t
44
  | StateVarPack of register_t
45
  | ExistsMem of ident * 'a formula_t * 'a formula_t
46
  | Value of 'a
47

    
48
(* type 'a simulation_t = {
49
 *   sname: node_desc;
50
 *   sindex: option int;
51
 *   sformula: 'a formula_t;
52
 * } *)
53

    
54
type 'a memory_pack_t = {
55
  mpname : node_desc;
56
  mpindex : int option;
57
  mpformula : 'a formula_t;
58
}
59

    
60
type 'a transition_t = {
61
  tname : node_desc;
62
  tindex : int option;
63
  tvars : var_decl list;
64
  tformula : 'a formula_t;
65
  tmem_footprint : Utils.ISet.t;
66
  tinst_footprint : ident Utils.IMap.t;
67
}
(83-83/99)