Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / stateflow / models / model_stopwatch.ml @ 69c96b6c

History | View | Annotate | Download (7.07 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 (Corelang.mkexpr Location.dummy_loc (LustreSpec.Expr_const (Corelang.const_of_bool true)))
9
    
10
let name = "stopwatch"
11
  
12
let model = 
13
  let smain    = "main" in
14
  let sstop    = "stop" in
15
  let sreset   = "reset" in
16
  let slapstop = "lap_stop" in
17
  let srun     = "run" in
18
  let srunning = "running" in
19
  let slap     = "lap" in
20

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

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

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

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

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

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

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

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

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

    
264
let traces : trace_t list =
265
  [
266
    [None; Some "TIC"; Some "START"; Some "TIC"; Some "TIC"];
267
    [None; Some "START"; Some "START"; Some "START"];
268
    [None; Some "START"; Some "TIC"; Some "START"; Some "TIC"]
269
  ]