Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_many_files / A1_PP.LUSTREC.lus @ cd1faebc

History | View | Annotate | Download (2.51 KB)

1 4748b215 hbourbou
-- This file has been generated by CoCoSim2.
2
3
-- Compiler: Lustre compiler 2 (ToLustre.m)
4
-- Time: 03-Dec-2018 22:19:27
5
(*
6
Original block name: A1_PP/Assumption/viewdvc
7
*)
8
node  viewdvc_258_027(In1_1 : real;
9
	In1_2 : real;
10
	__time_step : real;
11
	__nb_step : int;)
12
returns(VerificationSubsystem_virtual : bool;);
13
let
14
	VerificationSubsystem_virtual = true;
15
tel
16
17
(*
18
Original block name: A1_PP/Assumption1/viewdvc
19
*)
20
node  viewdvc_263_041(In1_1 : real;
21
	__time_step : real;
22
	__nb_step : int;)
23
returns(VerificationSubsystem_virtual : bool;);
24
let
25
	VerificationSubsystem_virtual = true;
26
tel
27
28
(*
29
Original block name: A1_PP/Assumption2/viewdvc
30
*)
31
node  viewdvc_270_031(In1_1 : real;
32
	__time_step : real;
33
	__nb_step : int;)
34
returns(VerificationSubsystem_virtual : bool;);
35
let
36
	VerificationSubsystem_virtual = true;
37
tel
38
39
(*
40
Original block name: A1_PP/Assumption3/viewdvc
41
*)
42
node  viewdvc_277_026(In1_1 : real;
43
	In1_2 : real;
44
	In1_3 : real;
45
	In1_4 : real;
46
	__time_step : real;
47
	__nb_step : int;)
48
returns(VerificationSubsystem_virtual : bool;);
49
let
50
	VerificationSubsystem_virtual = true;
51
tel
52
53
(*
54
Original block name: A1_PP/Assumption4/viewdvc
55
*)
56
node  viewdvc_284_025(In1_1 : real;
57
	__time_step : real;
58
	__nb_step : int;)
59
returns(VerificationSubsystem_virtual : bool;);
60
let
61
	VerificationSubsystem_virtual = true;
62
tel
63
64
(*
65
Original block name: A1_PP/Assumption5/viewdvc
66
*)
67
node  viewdvc_291_026(In1_1 : bool;
68
	__time_step : real;
69
	__nb_step : int;)
70
returns(VerificationSubsystem_virtual : bool;);
71
let
72
	VerificationSubsystem_virtual = true;
73
tel
74
75
(*
76
Original block name: A1_PP
77
*)
78
node  A1_PP(In1_1 : real;
79
	In1_2 : real;
80
	In2_1 : real;
81
	In3_1 : real;
82
	In4_1 : real;
83
	In4_2 : real;
84
	In4_3 : real;
85
	In4_4 : real;
86
	In5_1 : real;
87
	In6_1 : bool;
88
	In7_1 : bool;)
89
returns(Out1_1 : bool;);
90
var Assumption5_1 : bool;
91
	LogicalOperator_1 : bool;
92
	__time_step : real;
93
	__nb_step : int;
94
let
95
	assert ( ((0.000000000000000 <= In1_1) and (In1_1 < 1.000000000000000)) or (In1_1 = 1.000000000000000) );
96
	assert ( (In2_1 = 0.000000000000000) or (In2_1 = 5.000000000000000) );
97
	assert ((1.000000000000000 <= In3_1) and (In3_1 <= 2.000000000000000));
98
	assert ( (In4_1 = 0.000000000000000) or ((1.000000000000000 <= In4_1) and (In4_1 <= 3.000000000000000)) );
99
	assert ( ((0.000000000000000 <= In5_1) and (In5_1 < 1.000000000000000)) or (In5_1 = 1.000000000000000) );
100
	Assumption5_1 = In6_1;
101
	assert (In6_1 = true);
102
	LogicalOperator_1 = ( Assumption5_1 and In7_1 );
103
	Out1_1 = LogicalOperator_1;
104
	__time_step = (0.0 -> ((pre __time_step) + 0.200000000000000));
105
	__nb_step = (0 -> ((pre __nb_step) + 1));
106
tel