Revision 75c459f4
Added by Lélio Brun about 2 years ago
| src/spec_types.ml | ||
|---|---|---|
| 4 | 4 |
| In |
| 5 | 5 |
| Out |
| 6 | 6 |
|
| 7 |
type expression_t = |
|
| 8 |
| Cst of constant |
|
| 7 |
type 'a expression_t = |
|
| 8 |
| Val of 'a |
|
| 9 |
| Tag of ident |
|
| 9 | 10 |
| Var of var_decl |
| 10 | 11 |
| Instance of state_t * ident |
| 11 | 12 |
| Memory of state_t * ident |
| 12 | 13 |
|
| 13 | 14 |
type predicate_t = |
| 14 |
| Atom of expression_t |
|
| 15 |
| Equal of predicate_t * predicate_t |
|
| 16 |
| Imply of predicate_t * predicate_t |
|
| 17 |
| Exists of var_decl list * predicate_t list |
|
| 18 |
| Forall of var_decl list * predicate_t list |
|
| 15 |
(* | Memory_pack *) |
|
| 16 |
| Clocked_on of ident |
|
| 17 |
| Transition |
|
| 18 |
| Initialization |
|
| 19 | 19 |
|
| 20 |
type transition_t = {
|
|
| 20 |
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 = {
|
|
| 21 | 39 |
tname: node_desc; |
| 22 |
tindex: int; |
|
| 40 |
tindex: int option;
|
|
| 23 | 41 |
tlocals: var_decl list; |
| 24 | 42 |
toutputs: var_decl list; |
| 25 |
tpredicate: predicate_t list;
|
|
| 43 |
tformula: 'a formula_t;
|
|
| 26 | 44 |
} |
| 45 |
|
|
Also available in: Unified diff
start with Spec AST generation