Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by Lélio Brun 8 months ago

reformatting

View differences:

src/tools/stateflow/models/model_stopwatch.ml
1 1
open Datatype
2 2
open Basetypes
3

  
3 4
(* open Transformer2 *)
4 5
open SF
5 6

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

  
9
let actionv _ = no_action
10
(*TODO if verbose then action x else no_action*)
11

  
12
let action _ = no_action
13
(* TODO *)
14

  
15
let condition _ =
16
  condition
17
    {
18
      expr =
19
        Corelang.mkexpr Location.dummy_loc
20
          (Lustre_types.Expr_const (Corelang.const_of_bool true));
21
      cinputs = [];
22
      coutputs = [];
23
      cvariables = [];
24
    }
25

  
15 26
let name = "stopwatch"
16 27

  
17 28
let model =
18
  let smain    = "main" in
19
  let sstop    = "stop" in
20
  let sreset   = "reset" in
29
  let smain = "main" in
30
  let sstop = "stop" in
31
  let sreset = "reset" in
21 32
  let slapstop = "lap_stop" in
22
  let srun     = "run" in
33
  let srun = "run" in
23 34
  let srunning = "running" in
24
  let slap     = "lap" in
35
  let slap = "lap" in
25 36

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

  
62
  let tlapstop_lap  = {
63
    event = event "LAP";
64
    condition = no_condition;
65
    condition_act  = actionv "ac_cond_lap_stop->reset";
66
    transition_act = actionv "ac_trans_lap_stop->reset";
67
    dest = DPath [smain;sstop;sreset];
68
  }
77
  let tlapstop_lap =
78
    {
79
      event = event "LAP";
80
      condition = no_condition;
81
      condition_act = actionv "ac_cond_lap_stop->reset";
82
      transition_act = actionv "ac_trans_lap_stop->reset";
83
      dest = DPath [ smain; sstop; sreset ];
84
    }
69 85
  in
70 86

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

  
163
  let def_stop = {
164
    state_actions = {
165
      entry_act  = actionv "ac_stop_entry";
166
      during_act = actionv "ac_stop_during";
167
      exit_act   = actionv "ac_stop_exit";
168
    };
169
    outer_trans = [];
170
    inner_trans = [];
171
    internal_composition = Or ([tinitreset], [sreset; slapstop])
172
  }
192
  let def_stop =
193
    {
194
      state_actions =
195
        {
196
          entry_act = actionv "ac_stop_entry";
197
          during_act = actionv "ac_stop_during";
198
          exit_act = actionv "ac_stop_exit";
199
        };
200
      outer_trans = [];
201
      inner_trans = [];
202
      internal_composition = Or ([ tinitreset ], [ sreset; slapstop ]);
203
    }
173 204
  in
174 205

  
175
  let def_reset = {
176
    state_actions = {
177
      entry_act  = actionv "ac_reset_entry";
178
      during_act = actionv "ac_reset_during";
179
      exit_act   = actionv "ac_reset_exit";
180
    };
181
    outer_trans = [treset_start];
182
    inner_trans = [treset];
183
    internal_composition = Or ([treset_start], [])
184
  }
206
  let def_reset =
207
    {
208
      state_actions =
209
        {
210
          entry_act = actionv "ac_reset_entry";
211
          during_act = actionv "ac_reset_during";
212
          exit_act = actionv "ac_reset_exit";
213
        };
214
      outer_trans = [ treset_start ];
215
      inner_trans = [ treset ];
216
      internal_composition = Or ([ treset_start ], []);
217
    }
185 218
  in
186 219

  
187
  let def_lapstop = {
188
    state_actions = {
189
      entry_act  = actionv "ac_lapstop_entry";
190
      during_act = actionv "ac_lapstop_during";
191
      exit_act   = actionv "ac_lapstop_exit";
192
    };
193
    outer_trans = [tlapstop_lap; tlapstop_start];
194
    inner_trans = [];
195
    internal_composition = Or ([], [])
196
  }
220
  let def_lapstop =
221
    {
222
      state_actions =
223
        {
224
          entry_act = actionv "ac_lapstop_entry";
225
          during_act = actionv "ac_lapstop_during";
226
          exit_act = actionv "ac_lapstop_exit";
227
        };
228
      outer_trans = [ tlapstop_lap; tlapstop_start ];
229
      inner_trans = [];
230
      internal_composition = Or ([], []);
231
    }
197 232
  in
198 233

  
199
  let def_run = {
200
    state_actions = {
201
      entry_act  = actionv "ac_run_entry";
202
      during_act = actionv "ac_run_during";
203
      exit_act   = actionv "ac_run_exit";
204
    };
205
    outer_trans = [];
206
    inner_trans = [ttic];
207
    internal_composition = Or ([], [srunning; slap])
208
  }
234
  let def_run =
235
    {
236
      state_actions =
237
        {
238
          entry_act = actionv "ac_run_entry";
239
          during_act = actionv "ac_run_during";
240
          exit_act = actionv "ac_run_exit";
241
        };
242
      outer_trans = [];
243
      inner_trans = [ ttic ];
244
      internal_composition = Or ([], [ srunning; slap ]);
245
    }
209 246
  in
210 247

  
211
  let def_running = {
212
    state_actions = {
213
      entry_act  = actionv "ac_running_entry";
214
      during_act = action "disp=(cent,sec,min)";
215
      exit_act   = actionv "ac_running_exit";
216
    };
217
    outer_trans = [trunning_start; trunning_lap];
218
    inner_trans = [];
219
    internal_composition = Or ([], [])
220
  }
248
  let def_running =
249
    {
250
      state_actions =
251
        {
252
          entry_act = actionv "ac_running_entry";
253
          during_act = action "disp=(cent,sec,min)";
254
          exit_act = actionv "ac_running_exit";
255
        };
256
      outer_trans = [ trunning_start; trunning_lap ];
257
      inner_trans = [];
258
      internal_composition = Or ([], []);
259
    }
221 260
  in
222 261

  
223
  let def_lap = {
224
    state_actions = {
225
      entry_act  = actionv "ac_lap_entry";
226
      during_act = actionv "ac_lap_during";
227
      exit_act   = actionv "ac_lap_exit";
228
    };
229
    outer_trans = [tlap_start; tlap_lap];
230
    inner_trans = [];
231
    internal_composition = Or ([], [])
232
  }
262
  let def_lap =
263
    {
264
      state_actions =
265
        {
266
          entry_act = actionv "ac_lap_entry";
267
          during_act = actionv "ac_lap_during";
268
          exit_act = actionv "ac_lap_exit";
269
        };
270
      outer_trans = [ tlap_start; tlap_lap ];
271
      inner_trans = [];
272
      internal_composition = Or ([], []);
273
    }
233 274
  in
234 275

  
235
  let src = [
236
    State([smain;srun;srunning], def_running);
237
    State([smain;srun;slap], def_lap);
238
    State([smain;srun], def_run);
239
    State([smain;sstop;sreset], def_reset);
240
    State([smain;sstop;slapstop], def_lapstop);
241
    State([smain;sstop], def_stop);
242
    State([smain], def_main);
243
    Junction("jreset", []);
244
    Junction("j1", [tj1j2;tj1j3]);
245
    Junction("j2", [tj2j3droite; tj2j3gauche]);
246
    Junction("j3", []);
247
  ]
276
  let src =
277
    [
278
      State ([ smain; srun; srunning ], def_running);
279
      State ([ smain; srun; slap ], def_lap);
280
      State ([ smain; srun ], def_run);
281
      State ([ smain; sstop; sreset ], def_reset);
282
      State ([ smain; sstop; slapstop ], def_lapstop);
283
      State ([ smain; sstop ], def_stop);
284
      State ([ smain ], def_main);
285
      Junction ("jreset", []);
286
      Junction ("j1", [ tj1j2; tj1j3 ]);
287
      Junction ("j2", [ tj2j3droite; tj2j3gauche ]);
288
      Junction ("j3", []);
289
    ]
248 290
  in
249 291
  let globals =
250 292
    let int_typ = Corelang.mktyp Location.dummy_loc Lustre_types.Tydec_int in
251
    List.map (fun k ->
252
      Corelang.mkvar_decl
253
	Location.dummy_loc
254
	(k, (* name *)
255
	 int_typ, (* type *)
256
	 Corelang.dummy_clock_dec, (* clock *)
257
	 false, (* not a constant *)
258
	 None, (* no default value *)
259
	 None (* no parent known *)
260
	),
261
      (* Default value is zero *)
262
      Corelang.mkexpr Location.dummy_loc (Lustre_types.Expr_const (Lustre_types.Const_int 0))
263
      
264
    )
265
      ["cent";
266
       "sec";
267
       "min";
268
       "cont"
269
      ]
293
    List.map
294
      (fun k ->
295
        ( Corelang.mkvar_decl Location.dummy_loc
296
            ( k,
297
              (* name *)
298
              int_typ,
299
              (* type *)
300
              Corelang.dummy_clock_dec,
301
              (* clock *)
302
              false,
303
              (* not a constant *)
304
              None,
305
              (* no default value *)
306
              None (* no parent known *) ),
307
          (* Default value is zero *)
308
          Corelang.mkexpr Location.dummy_loc
309
            (Lustre_types.Expr_const (Lustre_types.Const_int 0)) ))
310
      [ "cent"; "sec"; "min"; "cont" ]
270 311
  in
271 312
  Program (smain, src, globals)
272 313

  
273 314
let traces : trace_t list =
274 315
  [
275
    [None; Some "TIC"; Some "START"; Some "TIC"; Some "TIC"];
276
    [None; Some "START"; Some "START"; Some "START"];
277
    [None; Some "START"; Some "TIC"; Some "START"; Some "TIC"]
316
    [ None; Some "TIC"; Some "START"; Some "TIC"; Some "TIC" ];
317
    [ None; Some "START"; Some "START"; Some "START" ];
318
    [ None; Some "START"; Some "TIC"; Some "START"; Some "TIC" ];
278 319
  ]

Also available in: Unified diff