Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / tools / stateflow / src / models / model_stopwatch.ml @ 2de7fa82

History | View | Annotate | Download (6.52 KB)

1
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
    
8
let name = "stopwatch"
9
  
10
let model = 
11
  let smain    = "main" in
12
  let sstop    = "stop" in
13
  let sreset   = "reset" in
14
  let slapstop = "lap_stop" in
15
  let srun     = "run" in
16
  let srunning = "running" in
17
  let slap     = "lap" in
18

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

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

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

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

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

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

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

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

    
228
  let src = [
229
    State([smain;srun;srunning], def_running);
230
    State([smain;srun;slap], def_lap);
231
    State([smain;srun], def_run);
232
    State([smain;sstop;sreset], def_reset);
233
    State([smain;sstop;slapstop], def_lapstop);
234
    State([smain;sstop], def_stop);
235
    State([smain], def_main);
236
    Junction("jreset", []);
237
    Junction("j1", [tj1j2;tj1j3]);
238
    Junction("j2", [tj2j3droite; tj2j3gauche]);
239
    Junction("j3", []);
240
  ]
241
  in
242
  (smain, src)
243

    
244
let traces : trace_t list =
245
  [
246
    [None; Some "TIC"; Some "START"; Some "TIC"; Some "TIC"];
247
    [None; Some "START"; Some "START"; Some "START"];
248
    [None; Some "START"; Some "TIC"; Some "START"; Some "TIC"]
249
  ]