Project

General

Profile

Download (934 Bytes) Statistics
| Branch: | Tag: | Revision:
1 7a1b2819 Lélio Brun
open Lustre_types
2
3
type state_t =
4
  | In
5
  | Out
6
7 75c459f4 Lélio Brun
type 'a expression_t =
8
  | Val of 'a
9
  | Tag of ident
10 7a1b2819 Lélio Brun
  | Var of var_decl
11
  | Instance of state_t * ident
12
  | Memory of state_t * ident
13
14
type predicate_t =
15 75c459f4 Lélio Brun
  (* | Memory_pack *)
16
  | Clocked_on of ident
17
  | Transition
18
  | Initialization
19 7a1b2819 Lélio Brun
20 75c459f4 Lélio Brun
type 'a formula_t =
21
  | True
22
  | False
23
  | Equal of 'a expression_t * 'a expression_t
24
  | And of 'a formula_t list
25
  | Or of 'a formula_t list
26
  | Imply of 'a formula_t * 'a formula_t
27
  | Exists of var_decl list * 'a formula_t
28
  | Forall of var_decl list * 'a formula_t
29
  | Ternary of 'a expression_t * 'a formula_t * 'a formula_t
30
  | Predicate of predicate_t * 'a expression_t list
31
32
(* type 'a simulation_t = {
33
 *   sname: node_desc;
34
 *   sindex: option int;
35
 *   sformula: 'a formula_t;
36
 * } *)
37
38
type 'a transition_t = {
39 7a1b2819 Lélio Brun
  tname: node_desc;
40 75c459f4 Lélio Brun
  tindex: int option;
41 7a1b2819 Lélio Brun
  tlocals: var_decl list;
42
  toutputs: var_decl list;
43 75c459f4 Lélio Brun
  tformula: 'a formula_t;
44 7a1b2819 Lélio Brun
}