CristalCaveGem » LustreC » Lustrec-Tests

(* Generated Lustre Interface file from tawoa_automata.lus *)

(* by Lustre-C compiler version 1.3-458, 2016/10/21, 12:58:32 *)

(* Feel free to mask some of the definitions by removing them from this file. *)

type aut2__type = enum {C, D }; 

type aut1__type = enum {A, B }; 

function aut1__A_handler_until (aut1__restart_act: bool; input: int; x2: int) returns (aut1__restart_in: bool; aut1__state_in: aut1__type; x1_out: int; y1_out: int);

function aut1__A_unless (aut1__restart_in: bool) returns (aut1__restart_act: bool; aut1__state_act: aut1__type);

function aut1__B_handler_until (aut1__restart_act: bool) returns (aut1__restart_in: bool; aut1__state_in: aut1__type; x1_out: int; y1_out: int);

function aut1__B_unless (aut1__restart_in: bool) returns (aut1__restart_act: bool; aut1__state_act: aut1__type);

function aut2__C_handler_until (aut2__restart_act: bool; x1: int) returns (aut2__restart_in: bool; aut2__state_in: aut2__type; x2_out: int; y2_out: int);

function aut2__C_unless (aut2__restart_in: bool) returns (aut2__restart_act: bool; aut2__state_act: aut2__type);

function aut2__D_handler_until (aut2__restart_act: bool; input: int) returns (aut2__restart_in: bool; aut2__state_in: aut2__type; x2_out: int; y2_out: int);

function aut2__D_unless (aut2__restart_in: bool) returns (aut2__restart_act: bool; aut2__state_act: aut2__type);

node tawoa_automata (input: int) returns (ok: bool);