Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / stateflow / models / model_stopwatch.ml @ 9c654082

History | View | Annotate | Download (7.29 KB)

1
open Datatype
2
(* open Transformer2 *)
3
open SF
4

    
5
let verbose = false
6
let actionv x = no_action (*TODO if verbose then action x else no_action*)
7
let action x = no_action (* TODO *)
8
let condition x = condition {
9
  expr = Corelang.mkexpr Location.dummy_loc (LustreSpec.Expr_const (Corelang.const_of_bool true));
10
  cinputs = [];
11
  coutputs = [];
12
  cvariables = [];
13
}
14
let name = "stopwatch"
15

    
16
let model =
17
  let smain    = "main" in
18
  let sstop    = "stop" in
19
  let sreset   = "reset" in
20
  let slapstop = "lap_stop" in
21
  let srun     = "run" in
22
  let srunning = "running" in
23
  let slap     = "lap" in
24

    
25
  let tinitstop = {
26
    event = no_event;
27
    condition = no_condition;
28
    condition_act  = actionv "ac_cond_init_stop";
29
    transition_act = actionv "ac_trans_init_stop";
30
    dest = DPath [smain;sstop];
31
  }
32
  in
33
  let tinitreset = {
34
    event = no_event;
35
    condition = no_condition;
36
    condition_act  = actionv "ac_cond_init_reset";
37
    transition_act = actionv "ac_cond_init_stop";
38
    dest = DPath [smain;sstop;sreset];
39
  }
40
  in
41
  let treset = {
42
    event = event "LAP";
43
    condition = no_condition;
44
    condition_act  = action "reset counter";
45
    transition_act = actionv "ac_trans_reset_junction";
46
    dest = DJunction "jreset" (* [smain;sstop;sreset]; ou bien mettre une junction.  Verifier
47
				 si il y a des effets de bords non
48
				 desirés de fermeture/ouverture de
49
				 noeud *)
50
  }
51
  in
52
  let treset_start  = {
53
    event = event "START";
54
    condition = no_condition;
55
    condition_act  = actionv "ac_cond_reset->running";
56
    transition_act = actionv "ac_trans_reset->running";
57
    dest = DPath [smain;srun;srunning];
58
  }
59
  in
60

    
61
  let tlapstop_lap  = {
62
    event = event "LAP";
63
    condition = no_condition;
64
    condition_act  = actionv "ac_cond_lap_stop->reset";
65
    transition_act = actionv "ac_trans_lap_stop->reset";
66
    dest = DPath [smain;sstop;sreset];
67
  }
68
  in
69

    
70
  let tlapstop_start  = {
71
    event = event "START";
72
    condition = no_condition;
73
    condition_act  = actionv "ac_cond_lap_stop->lap";
74
    transition_act = actionv "ac_trans_lap_stop->lap";
75
    dest = DPath [smain;srun;slap];
76
  }
77
  in
78
  let ttic   = {
79
    event = event "TIC";
80
    condition = no_condition;
81
    condition_act  = action "cent+=1";
82
    transition_act = actionv "ac_trans_->J1";
83
    dest = DJunction "j1";
84
  }
85
  in
86
  let trunning_start  = {
87
    event = event "START";
88
    condition = no_condition;
89
    condition_act  = actionv "ac_cond_running->reset";
90
    transition_act = actionv "ac_trans_running->reset";
91
    dest = DPath [smain;sstop;sreset];
92
  }
93
  in
94
  let tlap_start  = {
95
    event = event "START";
96
    condition = no_condition;
97
    condition_act  = actionv "ac_cond_lap->lap_stop";
98
    transition_act = actionv "ac_trans_lap->lap_stop";
99
    dest = DPath [smain;sstop;slapstop];
100
  }
101
  in
102
  let tlap_lap  = {
103
    event = event "LAP";
104
    condition = no_condition;
105
    condition_act  = actionv "ac_cond_lap->running";
106
    transition_act = actionv "ac_trans_lap->running";
107
    dest = DPath [smain;srun;srunning];
108
  }
109
  in
110
  let trunning_lap  = {
111
    event = event "LAP";
112
    condition = no_condition;
113
    condition_act  = actionv "ac_cond_running->lap";
114
    transition_act = actionv "ac_trans_running->lap";
115
    dest = DPath [smain;srun;slap];
116
  }
117
  in
118
  let tj1j2 = {
119
    event = no_event;
120
    condition = condition "cent==100";
121
    condition_act  = action "cont=0;sec+=1";
122
    transition_act = actionv "ac_trans_J1->J2";
123
    dest = DJunction "j2";
124
  }
125
  in
126
  let tj1j3 =    {
127
    event = no_event;
128
    condition = condition "cent!=100";
129
    condition_act  = actionv "ac_cond_J1->J3";
130
    transition_act = actionv "ac_trans_J1->J3";
131
    dest = DJunction "j3";
132
  }
133
  in
134
  let tj2j3gauche   = {
135
    event = no_event;
136
    condition = condition "sec!=60";
137
    condition_act  = actionv "ac_cond_J2->J3_left";
138
    transition_act = actionv "ac_trans_J2->J3_left";
139
    dest = DJunction "j3";
140
  }
141
  in
142
  let tj2j3droite    = {
143
    event = no_event;
144
    condition = condition "sec==60";
145
    condition_act  = action "sec=0; min+=1";
146
    transition_act = actionv "ac_trans_J2->J3_right";
147
    dest = (*DPath [smain;srun];*) DJunction "j3";
148
  }
149
  in
150
  let def_main = {
151
    state_actions = {
152
      entry_act  = actionv "ac_main_entry";
153
      during_act = actionv "ac_main_during";
154
      exit_act   = actionv "ac_main_exit";
155
    };
156
    outer_trans = [];
157
    inner_trans = [];
158
    internal_composition = Or ([tinitstop], [sstop; srun])
159
  }
160
  in
161

    
162
  let def_stop = {
163
    state_actions = {
164
      entry_act  = actionv "ac_stop_entry";
165
      during_act = actionv "ac_stop_during";
166
      exit_act   = actionv "ac_stop_exit";
167
    };
168
    outer_trans = [];
169
    inner_trans = [];
170
    internal_composition = Or ([tinitreset], [sreset; slapstop])
171
  }
172
  in
173

    
174
  let def_reset = {
175
    state_actions = {
176
      entry_act  = actionv "ac_reset_entry";
177
      during_act = actionv "ac_reset_during";
178
      exit_act   = actionv "ac_reset_exit";
179
    };
180
    outer_trans = [treset_start];
181
    inner_trans = [treset];
182
    internal_composition = Or ([treset_start], [])
183
  }
184
  in
185

    
186
  let def_lapstop = {
187
    state_actions = {
188
      entry_act  = actionv "ac_lapstop_entry";
189
      during_act = actionv "ac_lapstop_during";
190
      exit_act   = actionv "ac_lapstop_exit";
191
    };
192
    outer_trans = [tlapstop_lap; tlapstop_start];
193
    inner_trans = [];
194
    internal_composition = Or ([], [])
195
  }
196
  in
197

    
198
  let def_run = {
199
    state_actions = {
200
      entry_act  = actionv "ac_run_entry";
201
      during_act = actionv "ac_run_during";
202
      exit_act   = actionv "ac_run_exit";
203
    };
204
    outer_trans = [];
205
    inner_trans = [ttic];
206
    internal_composition = Or ([], [srunning; slap])
207
  }
208
  in
209

    
210
  let def_running = {
211
    state_actions = {
212
      entry_act  = actionv "ac_running_entry";
213
      during_act = action "disp=(cent,sec,min)";
214
      exit_act   = actionv "ac_running_exit";
215
    };
216
    outer_trans = [trunning_start; trunning_lap];
217
    inner_trans = [];
218
    internal_composition = Or ([], [])
219
  }
220
  in
221

    
222
  let def_lap = {
223
    state_actions = {
224
      entry_act  = actionv "ac_lap_entry";
225
      during_act = actionv "ac_lap_during";
226
      exit_act   = actionv "ac_lap_exit";
227
    };
228
    outer_trans = [tlap_start; tlap_lap];
229
    inner_trans = [];
230
    internal_composition = Or ([], [])
231
  }
232
  in
233

    
234
  let src = [
235
    State([smain;srun;srunning], def_running);
236
    State([smain;srun;slap], def_lap);
237
    State([smain;srun], def_run);
238
    State([smain;sstop;sreset], def_reset);
239
    State([smain;sstop;slapstop], def_lapstop);
240
    State([smain;sstop], def_stop);
241
    State([smain], def_main);
242
    Junction("jreset", []);
243
    Junction("j1", [tj1j2;tj1j3]);
244
    Junction("j2", [tj2j3droite; tj2j3gauche]);
245
    Junction("j3", []);
246
  ]
247
  in
248
  let globals =
249
    let int_typ = Corelang.mktyp Location.dummy_loc LustreSpec.Tydec_int in
250
    List.map (fun k ->
251
      Corelang.mkvar_decl
252
	Location.dummy_loc
253
	(k, (* name *)
254
	 int_typ, (* type *)
255
	 Corelang.dummy_clock_dec, (* clock *)
256
	 false, (* not a constant *)
257
	 None, (* no default value *)
258
	 None (* no parent known *)
259
	),
260
      (* Default value is zero *)
261
      Corelang.mkexpr Location.dummy_loc (LustreSpec.Expr_const (LustreSpec.Const_int 0))
262
      
263
    )
264
      ["cent";
265
       "sec";
266
       "min";
267
       "cont"
268
      ]
269
  in
270
  Program (smain, src, globals)
271

    
272
let traces : trace_t list =
273
  [
274
    [None; Some "TIC"; Some "START"; Some "TIC"; Some "TIC"];
275
    [None; Some "START"; Some "START"; Some "START"];
276
    [None; Some "START"; Some "TIC"; Some "START"; Some "TIC"]
277
  ]