Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / stateflow / models / model_stopwatch.ml @ 93119c3f

History | View | Annotate | Download (7.02 KB)

1 2de7fa82 ploc
open Datatype
2
(* open Transformer2 *)
3
open SF
4
5
let verbose = false
6
let actionv x = if verbose then action x else no_action
7 93119c3f ploc
let condition x = condition (Corelang.mkexpr Location.dummy_loc (LustreSpec.Expr_const (Corelang.const_of_bool true)))
8 2de7fa82 ploc
    
9
let name = "stopwatch"
10
  
11
let model = 
12
  let smain    = "main" in
13
  let sstop    = "stop" in
14
  let sreset   = "reset" in
15
  let slapstop = "lap_stop" in
16
  let srun     = "run" in
17
  let srunning = "running" in
18
  let slap     = "lap" in
19
20
  let tinitstop = {
21
    event = no_event;
22
    condition = no_condition;
23
    condition_act  = actionv "ac_cond_init_stop";
24
    transition_act = actionv "ac_trans_init_stop";
25
    dest = DPath [smain;sstop];
26
  }
27
  in
28
  let tinitreset = {
29
    event = no_event;
30
    condition = no_condition;
31
    condition_act  = actionv "ac_cond_init_reset";
32
    transition_act = actionv "ac_cond_init_stop";
33
    dest = DPath [smain;sstop;sreset];
34
  }
35
  in
36
  let treset = {
37
    event = event "LAP";
38
    condition = no_condition;
39
    condition_act  = action "reset counter";
40
    transition_act = actionv "ac_trans_reset_junction";
41
    dest = DJunction "jreset" (* [smain;sstop;sreset]; ou bien mettre une junction.  Verifier
42
				 si il y a des effets de bords non
43
				 desirés de fermeture/ouverture de
44
				 noeud *)
45
  }
46
  in
47
  let treset_start  = {
48
    event = event "START";
49
    condition = no_condition;
50
    condition_act  = actionv "ac_cond_reset->running";
51
    transition_act = actionv "ac_trans_reset->running";
52
    dest = DPath [smain;srun;srunning];
53
  }
54
  in
55
  
56
  let tlapstop_lap  = {
57
    event = event "LAP";
58
    condition = no_condition;
59
    condition_act  = actionv "ac_cond_lap_stop->reset";
60
    transition_act = actionv "ac_trans_lap_stop->reset";
61
    dest = DPath [smain;sstop;sreset];
62
  }
63
  in
64
65
  let tlapstop_start  = {
66
    event = event "START";
67
    condition = no_condition;
68
    condition_act  = actionv "ac_cond_lap_stop->lap";
69
    transition_act = actionv "ac_trans_lap_stop->lap";
70
    dest = DPath [smain;srun;slap];
71
  }
72
  in
73
  let ttic   = {
74
    event = event "TIC";
75
    condition = no_condition;
76
    condition_act  = action "cent+=1";
77
    transition_act = actionv "ac_trans_->J1";
78
    dest = DJunction "j1";
79
  }
80
  in
81
  let trunning_start  = {
82
    event = event "START";
83
    condition = no_condition;
84
    condition_act  = actionv "ac_cond_running->reset";
85
    transition_act = actionv "ac_trans_running->reset";
86
    dest = DPath [smain;sstop;sreset];
87
  }
88
  in
89
  let tlap_start  = {
90
    event = event "START";
91
    condition = no_condition;
92
    condition_act  = actionv "ac_cond_lap->lap_stop";
93
    transition_act = actionv "ac_trans_lap->lap_stop";
94
    dest = DPath [smain;sstop;slapstop];
95
  }
96
  in
97
  let tlap_lap  = {
98
    event = event "LAP";
99
    condition = no_condition;
100
    condition_act  = actionv "ac_cond_lap->running";
101
    transition_act = actionv "ac_trans_lap->running";
102
    dest = DPath [smain;srun;srunning];
103
  }
104
  in
105
  let trunning_lap  = {
106
    event = event "LAP";
107
    condition = no_condition;
108
    condition_act  = actionv "ac_cond_running->lap";
109
    transition_act = actionv "ac_trans_running->lap";
110
    dest = DPath [smain;srun;slap];
111
  }
112
  in
113
  let tj1j2 = {
114
    event = no_event;
115
    condition = condition "cent==100";
116
    condition_act  = action "cont=0;sec+=1";
117
    transition_act = actionv "ac_trans_J1->J2";
118
    dest = DJunction "j2";
119
  }
120
  in
121
  let tj1j3 =    {
122
    event = no_event;
123
    condition = condition "cent!=100";
124
    condition_act  = actionv "ac_cond_J1->J3";
125
    transition_act = actionv "ac_trans_J1->J3";
126
    dest = DJunction "j3";
127
  }
128
  in
129
  let tj2j3gauche   = {
130
    event = no_event;
131
    condition = condition "sec!=60";
132
    condition_act  = actionv "ac_cond_J2->J3_left";
133
    transition_act = actionv "ac_trans_J2->J3_left";
134
    dest = DJunction "j3";
135
  }
136
  in
137
  let tj2j3droite    = {
138
    event = no_event;
139
    condition = condition "sec==60";
140
    condition_act  = action "sec=0; min+=1";
141
    transition_act = actionv "ac_trans_J2->J3_right";
142
    dest = (*DPath [smain;srun];*) DJunction "j3";
143
  }
144
  in
145
  let def_main = {
146
    state_actions = {
147
      entry_act  = actionv "ac_main_entry";
148
      during_act = actionv "ac_main_during";
149
      exit_act   = actionv "ac_main_exit";
150
    };
151
    outer_trans = [];
152
    inner_trans = [];
153
    internal_composition = Or ([tinitstop], [sstop; srun])
154
  }
155
  in
156
157
  let def_stop = {
158
    state_actions = {
159
      entry_act  = actionv "ac_stop_entry";
160
      during_act = actionv "ac_stop_during";
161
      exit_act   = actionv "ac_stop_exit";
162
    };
163
    outer_trans = [];
164
    inner_trans = [];
165
    internal_composition = Or ([tinitreset], [sreset; slapstop])
166
  }
167
  in
168
169
  let def_reset = {
170
    state_actions = {
171
      entry_act  = actionv "ac_reset_entry";
172
      during_act = actionv "ac_reset_during";
173
      exit_act   = actionv "ac_reset_exit";
174
    };
175
    outer_trans = [treset_start];
176
    inner_trans = [treset];
177
    internal_composition = Or ([treset_start], [])
178
  }
179
  in
180
181
  let def_lapstop = {
182
    state_actions = {
183
      entry_act  = actionv "ac_lapstop_entry";
184
      during_act = actionv "ac_lapstop_during";
185
      exit_act   = actionv "ac_lapstop_exit";
186
    };
187
    outer_trans = [tlapstop_lap; tlapstop_start];
188
    inner_trans = [];
189
    internal_composition = Or ([], [])
190
  }
191
  in
192
193
  let def_run = {
194
    state_actions = {
195
      entry_act  = actionv "ac_run_entry";
196
      during_act = actionv "ac_run_during";
197
      exit_act   = actionv "ac_run_exit";
198
    };
199
    outer_trans = [];
200
    inner_trans = [ttic];
201
    internal_composition = Or ([], [srunning; slap])
202
  }
203
  in
204
205
  let def_running = {
206
    state_actions = {
207
      entry_act  = actionv "ac_running_entry";
208
      during_act = action "disp=(cent,sec,min)";
209
      exit_act   = actionv "ac_running_exit";
210
    };
211
    outer_trans = [trunning_start; trunning_lap];
212
    inner_trans = [];
213
    internal_composition = Or ([], [])
214
  }
215
  in
216
217
  let def_lap = {
218
    state_actions = {
219
      entry_act  = actionv "ac_lap_entry";
220
      during_act = actionv "ac_lap_during";
221
      exit_act   = actionv "ac_lap_exit";
222
    };
223
    outer_trans = [tlap_start; tlap_lap];
224
    inner_trans = [];
225
    internal_composition = Or ([], [])
226
  }
227
  in
228
229
  let src = [
230
    State([smain;srun;srunning], def_running);
231
    State([smain;srun;slap], def_lap);
232
    State([smain;srun], def_run);
233
    State([smain;sstop;sreset], def_reset);
234
    State([smain;sstop;slapstop], def_lapstop);
235
    State([smain;sstop], def_stop);
236
    State([smain], def_main);
237
    Junction("jreset", []);
238
    Junction("j1", [tj1j2;tj1j3]);
239
    Junction("j2", [tj2j3droite; tj2j3gauche]);
240
    Junction("j3", []);
241
  ]
242
  in
243 93119c3f ploc
  let globals =
244
    let int_typ = Corelang.mktyp Location.dummy_loc LustreSpec.Tydec_int in
245
    List.map (fun k ->
246
      Corelang.mkvar_decl
247
	Location.dummy_loc
248
	(k, (* name *)
249
	 int_typ, (* type *)
250
	 Corelang.dummy_clock_dec, (* clock *)
251
	 false, (* not a constant *)
252
	 None (* no default value *)
253
	)
254
    )
255
      ["cent";
256
       "sec";
257
       "min";
258
       "cont"
259
      ]
260
  in
261
  (smain, src, globals)
262 2de7fa82 ploc
263
let traces : trace_t list =
264
  [
265
    [None; Some "TIC"; Some "START"; Some "TIC"; Some "TIC"];
266
    [None; Some "START"; Some "START"; Some "START"];
267
    [None; Some "START"; Some "TIC"; Some "START"; Some "TIC"]
268
  ]