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 
6cbbe1c1

Lélio Brun

 Transition of ident * int option

18 
75c459f4

Lélio Brun

 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

}
