Project

General

Profile

Download (7.32 KB) Statistics
| Branch: | Tag: | Revision:
1
open Lustrec
2
open Datatype
3
open Basetypes
4
(* open Transformer2 *)
5
open SF
6

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

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

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

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

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

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

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

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

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

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

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

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

    
274
let traces : trace_t list =
275
  [
276
    [None; Some "TIC"; Some "START"; Some "TIC"; Some "TIC"];
277
    [None; Some "START"; Some "START"; Some "START"];
278
    [None; Some "START"; Some "TIC"; Some "START"; Some "TIC"]
279
  ]
(4-4/4)