Project

General

Profile

« Previous | Next » 

Revision 75c459f4

Added by LĂ©lio Brun 9 months ago

start with Spec AST generation

View differences:

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