Project

General

Profile

Download (1.8 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 left_v
7

    
8
type right_v
9

    
10
type ('a, _) expression_t =
11
  | Val : 'a -> ('a, right_v) expression_t
12
  | Tag : ident -> ('a, right_v) expression_t
13
  | Var : var_decl -> ('a, left_v) expression_t
14
  | Memory : register_t -> ('a, left_v) expression_t
15

    
16
val type_of_l_value : ('a, left_v) expression_t -> Types.t
17

    
18
type 'a predicate_t =
19
  | Transition :
20
      bool (* stateless *)
21
      * ident (* node name *)
22
      * ident option
23
      (* instance *)
24
      * int option
25
      (* transition index *)
26
      * ('a, 'b) expression_t list
27
      (* variables *)
28
      * bool (* reset *)
29
      * Utils.ISet.t (* memory footprint *)
30
      * ident Utils.IMap.t
31
      (* memory instances footprint *)
32
      -> 'a predicate_t
33
  | Reset of ident * ident * 'a
34
  | MemoryPack of ident * ident option * int option
35
  | Initialization
36
  | ResetCleared of ident
37

    
38
type 'a formula_t =
39
  | True
40
  | False
41
  | Equal : ('a, left_v) expression_t * ('a, 'b) expression_t -> 'a formula_t
42
  | GEqual : ('a, left_v) expression_t * ('a, 'b) expression_t -> 'a formula_t
43
  | And of 'a formula_t list
44
  | Or of 'a formula_t list
45
  | Imply of 'a formula_t * 'a formula_t
46
  | Exists of var_decl list * 'a formula_t
47
  | Forall of var_decl list * 'a formula_t
48
  | Ternary :
49
      ('a, 'b) expression_t * 'a formula_t * 'a formula_t
50
      -> 'a formula_t
51
  | Predicate : 'a predicate_t -> 'a formula_t
52
  | StateVarPack of register_t
53
  | ExistsMem of ident * 'a formula_t * 'a formula_t
54
  | Value of 'a
55

    
56
type 'a transition_t = {
57
  tname : node_desc;
58
  tindex : int option;
59
  tvars : var_decl list;
60
  tformula : 'a formula_t;
61
  tmem_footprint : Utils.ISet.t;
62
  tinst_footprint : ident Utils.IMap.t;
63
}
64

    
65
type 'a memory_pack_t = {
66
  mpname : node_desc;
67
  mpindex : int option;
68
  mpformula : 'a formula_t;
69
}
(84-84/99)