1

open Lustre_types

2


3

type state_t =

4

 In

5

 Out

6


7

type 'a expression_t =

8

 Val of 'a

9

 Tag of ident

10

 Var of var_decl

11

 Instance of state_t * ident

12

 Memory of state_t * ident

13


14

type predicate_t =

15

(*  Memory_pack *)

16

 Clocked_on of ident

17

 Transition of ident * int option

18

 Initialization

19


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 = {

39

tname: node_desc;

40

tindex: int option;

41

tlocals: var_decl list;

42

toutputs: var_decl list;

43

tformula: 'a formula_t;

44

}

45

