Project

General

Profile

« Previous | Next » 

Revision 7a1b2819

Added by LĂ©lio Brun 9 months ago

missing file

View differences:

src/spec_types.ml
1
open Lustre_types
2

  
3
type state_t =
4
  | In
5
  | Out
6

  
7
type expression_t =
8
  | Cst of constant
9
  | Var of var_decl
10
  | Instance of state_t * ident
11
  | Memory of state_t * ident
12

  
13
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
19

  
20
type transition_t = {
21
  tname: node_desc;
22
  tindex: int;
23
  tlocals: var_decl list;
24
  toutputs: var_decl list;
25
  tpredicate: predicate_t list;
26
}

Also available in: Unified diff