Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / tests / cocospec / DaysEnum_PP.KIND2.lus @ 1e3ae41f

History | View | Annotate | Download (2.34 KB)

1
-- This file has been generated by CoCoSim2.
2

    
3
-- Compiler: Lustre compiler 2 (ToLustre.m)
4
-- Time: 18-Jan-2019 19:01:54
5
type days = enum {Sunday, Monday, Tuesday, Wednesday, Thursday, Friday, Saturday};
6
(*
7
Original block name: DaysEnum_PP/contract/guarantee/EnumeratedConstant
8
*)
9
node  EnumeratedConstant_84_000(__time_step : real;
10
	__nb_step : int;)
11
returns(Out_1 : days;);
12
let
13
	Out_1 = ( Saturday );
14
tel
15

    
16
(*
17
Original block name: DaysEnum_PP/contract/guarantee/EnumeratedConstant1
18
*)
19
node  EnumeratedConstant1_85_000(__time_step : real;
20
	__nb_step : int;)
21
returns(Out_1 : days;);
22
let
23
	Out_1 = ( Sunday );
24
tel
25

    
26
(*
27
Original block name: DaysEnum_PP/contract/guarantee
28
*)
29
node  guarantee_81_000(day_1 : days;
30
	isWeekend_1 : bool;
31
	__time_step : real;
32
	__nb_step : int;)
33
returns(guarantee_1 : bool;);
34
let
35
	guarantee_1 = ( ( (not ( ( (( EnumeratedConstant_84_000(__time_step, __nb_step) ) <> day_1) ) and ( (day_1 <> ( EnumeratedConstant1_85_000(__time_step, __nb_step) )) ) )) ) or ( (not isWeekend_1) ) );
36
tel
37

    
38
(*
39
Original block name: DaysEnum_PP/subsystem/EnumeratedConstant
40
*)
41
node  EnumeratedConstant_113_000(__time_step : real;
42
	__nb_step : int;)
43
returns(Out_1 : days;);
44
let
45
	Out_1 = ( Saturday );
46
tel
47

    
48
(*
49
Original block name: DaysEnum_PP/subsystem/EnumeratedConstant1
50
*)
51
node  EnumeratedConstant1_114_000(__time_step : real;
52
	__nb_step : int;)
53
returns(Out_1 : days;);
54
let
55
	Out_1 = ( Sunday );
56
tel
57

    
58
(*
59
Original block name: DaysEnum_PP/contract
60
*)
61
contract contract_78_000(day_1 : days;
62
	__time_step : real;
63
	__nb_step : int;)
64
returns(isWeekend_1 : bool;);
65
let
66
	guarantee "guarantee_81_000" guarantee_81_000(day_1, isWeekend_1, __time_step, __nb_step);
67
tel
68

    
69
(*
70
Original block name: DaysEnum_PP/subsystem
71
*)
72
node  subsystem_111_000(day_1 : days;
73
	__time_step : real;
74
	__nb_step : int;)
75
returns(isWeekend_1 : bool;);
76
(*@contract
77
	import contract_78_000(day_1, __time_step, __nb_step) returns (isWeekend_1);
78
*)
79
let
80
	isWeekend_1 = ( ( (( EnumeratedConstant_113_000(__time_step, __nb_step) ) = day_1) ) or ( (day_1 = ( EnumeratedConstant1_114_000(__time_step, __nb_step) )) ) );
81
tel
82

    
83
(*
84
Original block name: DaysEnum_PP
85
*)
86
node  DaysEnum_PP(day_1 : days;)
87
returns(isWeekend_1 : bool;);
88
var __time_step : real;
89
	__nb_step : int;
90
let
91
	isWeekend_1 = ( subsystem_111_000(day_1, __time_step, __nb_step) );
92
	__time_step = (0.0 -> ((pre __time_step) + 1.0));
93
	__nb_step = (0 -> ((pre __nb_step) + 1));
94
tel
95