Outils Eclipse de transformation texte vers modèle

Désolée, je veux faire cette transformation avec des outils standards comme Xtext et Xtend sous Eclipse.

J'ai commencé avec le développement de la grammaire du DSL (Domain Specific Language) sous Xtext, concernant la méthode B, mais quand je veux faire l'exécution du projet et test de saisie d'un programme, ça ne fonctionne pas. Il y a un problème dans mon test.

Voilà mon DSL :

Code:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
grammar org.xtext.memoire.bmethod.Bmethod with org.eclipse.xtext.common.Terminals
 
generate bmethod "http://www.xtext.org/memoire/bmethod/Bmethod"
 
BMethod:
name=ID
(compose+=MACHINE)+
(herite+= REFINEMENT)*
(types+= Types)?
;
MACHINE:
REFINES|INCLUDES|EXTENDES|USES|SEES|
(operation+=OPERATION)*
(predicat+=PREDICAT)*
(initialisation+=INITIALISATION)?
(donnes+=DATA)+
(define+=DEFINITION)?
;
REFINES:'rafines' name=ID;
INCLUDES: 'includes' name=ID;
EXTENDES:'extendes' name=ID;
USES:'uses'name=ID;
SEES:'sees'name=ID;
Types:(sets+=SETS)*;
SETS: 'sets'name=STRING ';'|name=STRING'=''{'(valeur+=CONSTANTS)+'}'';'
;
CONSTANTS:'constants' val=STRING;
DATA:CONSTANTS|SETS;
REFINEMENT:'REFINEMENT' name=ID (refine=REFINES);
PREDICAT:Expression=STRING (ExpressionPrd+=EXPRESSION)+|VARIABLES|INVARIANT|PROPERTTIES;
PROPERTTIES:'PROPERTTIES'Expression=STRING;
VARIABLES:'VARIABLES'Expression=STRING valvariables=STRING;
INVARIANT:'INVARIANT'Expression=STRING ;
INITIALISATION:'INITIALISATION'ExpressionINITIALISATION=STRING (ExpIN=EXPRESSION)+|ANY;
DEFINITION:'DEFINITION'(def+=VARIABLES)+'==''('defconstant=CONSTANTS '..'defconstant=CONSTANTS')';
OPERATION:'OERATION' Expression=STRING
 
(syntoperation+=SYNTAXE)+;
ANY :'ANY' var=STRING (varAny+=VARIABLES)+|WHERE|THEN 'END';
WHERE:'WHERE' syntaxewhere=STRING (expwhere+=EXPRESSION)+;
THEN:'THEN'synthen=STRING (expTHEN+=EXPRESSION);
SELECT:'SELECT' synselect=STRING (expSELECT+=EXPRESSION)+|THEN|ELSE|ANY;
ELSE:'ELSE' synELES=STRING 'SKIP' 'END';
PRE:'PRE' syntaxePre=STRING (ExpPre+=EXPRESSION)+|THEN'END'|THEN|SELECT 'END'|ANY'END'|WHEN 'END';
WHEN:'WHEN' syntaxeWhen=STRING (Expwhen+=EXPRESSION)+|THEN|ELSE;
IF:'IF'syntaxeIf=STRING (ExpIf=EXPRESSION)+|THEN'END'|ELSE 'END'|BEGIN 'END'|ELSIF 'END'|VAR 'END';
BEGIN:'BEGIN'syntaxeBEGIN=STRING (ExpBegin+=EXPRESSION)+ 'END'|ELSIF|ELSE;
ELSIF:'ELSIF' syntaxeElsif=STRING (ExpElsif+=EXPRESSION)+|ELSE;
VAR:'VAR'syntaxeVar=STRING (ExpVar+=VARIABLES)+|IN|'IF' syntaxeIf=STRING (ExpIff+=EXPRESSION)+|THEN'END' ;
IN:'IN' syntaxeIn=STRING (ExpIn+=EXPRESSION)+;
SYNTAXE:IF|THEN|ELSE|ELSIF|ANY|WHERE|WHEN|VAR|IN|PRE|SELECT|BEGIN;
EXPRESSION: CONSTANTS|VARIABLES|SETS|OPERATEUR;
OPERATEUR:name='<:'|name='*'|name=':='|name='{'|name='}'|name='=='|name='='|name='('|name=')'|name=','|name=';'|name='&'|name='|->'|name='-'|name='-->'|name='=>'|name='~'|name='['|name=']'|name='!';

et voila mon test:

Code:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
/* Aggregat
* Author: siat555
* Creation date: 19/12/2015
*/
MACHINE
Aggregat
SEES
Types
USES
Clutch,
Gun,
Holster,
Motor,
Pump,
Display
VARIABLES
clutchPump,
gunPump,
holsterPump,
motorPump,
displayPump
INVARIANT
clutchPump∈ pump >->> clutch ∧
gunPump∈ pump >->> gun ∧
holsterPump∈ pump >->> holster ∧
motorPump∈ pump >->> motor ∧
displayPump∈ pump >->> display
INITIALISATION
ANY cp,gp,hp,mp,dp WHERE
cp∈ pump >->> clutch ∧
gp∈ pump >->> gun ∧
hp∈ pump >->> holster ∧
mp∈ pump >->> motor ∧
dp∈ pump >->> display
THEN
clutchPump := cp ||
gunPump := gp ||
holsterPump := hp ||
motorPump := mp ||
displayPump := dp
END
OPERATIONS
cc ←clutchOfPump(pp) =
PRE
pp ∈ pump
THEN
cc :=clutchPump(pp)
END;
dd←displayOfPump(pp) =
PRE
pp ∈ pump
THEN
dd := displayPump(pp)
END;
gg←gunOfPump(pp) =
PRE
pp ∈ pump
THEN
gg := gunPump(pp)
END;
mm←motorOfPump(pp) =
PRE
pp ∈ pump
THEN
mm := motorPump(pp)
END;
pp ←pumpOfGun(gg) =
PRE
gg∈ gun
THEN
pp := gunPump⁻¹(gg)
END;
pp ←pumpOfHolster(hh) =
PRE
hh∈ holster
THEN
pp := holsterPump⁻¹(hh)
END
 
 
END

Code:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
/* BasicMachine
* Author: siat555
* Creation date: 19/12/2015
*/
MACHINE
BasicMachine
SEES
Types
INCLUDES
Pump,
Clutch,
Gun,
Holster,
Motor,
Display,
Aggregat,
Delivery
PROMOTES
clutch_free,
clutch_engage,
gun_enable,
gun_disable,
gun_is_Enabled,
gun_depress_Trigger_Local,
gun_release_Trigger_Local,
holster_depress,
holster_release,
motor_start,
motor_stop,
pump_idOfPump,
pump_pumpOfId,
pump_is_Enabled,
pump_is_Disabled,
pump_enable_Local,
pump_disable_Local,
display_reset,
display_read_Display,
display_pulse,
delivery_create_Delivery,
clutchOfPump,
displayOfPump,
gunOfPump,
motorOfPump,
pumpOfGun,
pumpOfHolster
 
 
END

Code:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
/* Clutch
* Author: siat555
* Creation date: 19/12/2015
*/
MACHINE
Clutch
SEES
Types
VARIABLES
clutch, clutch_status
INVARIANT
clutch⊆ CLUTCH ∧
clutch_status∈ clutch → C_STATUS
INITIALISATION
ANY cc WHERE
cc ⊆ CLUTCH ∧
card(cc) = 5
THEN
clutch := cc ||
clutch_status := cc * {c_status_free}
END
OPERATIONS
clutch_free(cc) =
PRE
cc ∈ clutch
THEN
clutch_status(cc) := c_status_free
END;
clutch_engage(cc) =
PRE
cc ∈ clutch
THEN
clutch_status(cc) := c_status_engaged
END
 
 
END

Code:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
/* Delivery
* Author: siat555
* Creation date: 19/12/2015
*/
MACHINE
Delivery
SEES
Types
USES
Pump
VARIABLES
delivery,
delivery_cost,
delivery_volume,
delivery_grade,
delivery_pump_Id,
delivery_veh_Id
INVARIANT
delivery⊆ DELIVERY ∧
delivery_cost∈ delivery → COST ∧
delivery_volume∈ delivery → NAT ∧
delivery_grade∈ delivery → GRADE ∧
∀ deli.(deli ∈ delivery ⇒delivery_grade(deli) ↦delivery_cost(deli) ∈
costOfGrade) ∧delivery_pump_Id∈ delivery → PU_ID ∧
delivery_veh_Id∈ delivery → VEH_ID
INITIALISATION
delivery,
delivery_cost,
delivery_volume,
delivery_grade,
delivery_pump_Id,
delivery_veh_Id := ∅,∅,∅,∅,∅,∅
OPERATIONS
new←delivery_create_Delivery(cc,vv,gg,pi,vi) =
PRE
cc ∈ COST ∧
vv∈ NAT ∧
gg∈ GRADE ∧
gg↦ cc ∈costOfGrade∧
pi∈ ran(pump_pump_Id) ∧
vi∈ VEH_ID
THEN
ANY dd WHERE
dd∈ DELIVERY
THEN
delivery := delivery ∪ {dd} ||
delivery_cost(dd) := cc ||
delivery_grade(dd) := gg ||
delivery_volume(dd) := vv ||
delivery_pump_Id(dd) := pi ||
delivery_veh_Id(dd) := vi ||
new := dd
END
END
 
 
END

Code:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
/* Display
* Author: siat555
* Creation date: 19/12/2015
*/
MACHINE
Display
SEES
Types
VARIABLES
display,
display_cost,
display_volume,
display_grade,
display_veh_Id
INVARIANT
display⊆ DISPLAY ∧
display_cost∈ display → COST ∧
display_volume∈ display → NAT ∧
display_grade∈ display → GRADE ∧
∀ disp.(disp∈ display
⇒display_grade(disp) ↦display_cost(disp) ∈costOfGrade) ∧
display_veh_Id∈ display → VEH_ID
INITIALISATION
ANY dd,vi WHERE
dd⊆ DISPLAY ∧
card(dd) = 5 ∧
vi∈ VEH_ID
THEN
display := dd ||
display_cost := dd * {cost1} ||
display_volume := dd * {0} ||
display_grade := dd * {grade1} ||
display_veh_Id := dd * {vi}
END
OPERATIONS
display_reset(dd,gg,vi) =
PRE
dd∈ display ∧
gg∈ GRADE ∧
vi∈ VEH_ID
THEN
display_grade(dd) := gg ||
display_volume(dd) := 0 ||
display_cost(dd) := costOfGrade(gg)||
display_veh_Id(dd) := vi
END;
display_pulse(dd) =
PRE
dd∈ display
THEN
IF display_volume(dd) < MAXINT THEN
display_volume(dd) := display_volume(dd) + 1
ELSE
skip
END
END;
cc,vv,gg,vi←display_read_Display(dd) =
PRE
dd∈ display
THEN
cc :=display_cost(dd) ||
vv := display_volume(dd) ||
gg := display_grade(dd)||
vi := display_veh_Id(dd)
END
 
 
END

Code:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
 
/* Gun
* Author: siat555
* Creation date: 19/12/2015
*/
MACHINE
Gun
SEES
Types
VARIABLES
gun,gun_status,gun_trigger
INVARIANT
gun⊆ GUN ∧
gun_status∈ gun → PG_STATUS ∧
gun_trigger∈ gun → TH_STATUS
INITIALISATION
ANY gg WHERE
gg⊆ GUN ∧
card(gg) =5
THEN
gun := gg ||
gun_status := gg * {pg_status_disabled} ||
gun_trigger := gg * {th_status_released}
END
OPERATIONS
gun_enable(gg) =
PRE
gg∈ gun
THEN
gun_status(gg) := pg_status_enabled
END;
gun_disable(gg) =
PRE
gg∈ gun
THEN
gun_status(gg) := pg_status_disabled
END;
en←gun_is_Enabled(gg) =
PRE
gg∈ gun
THEN
en := bool(gun_status(gg) = pg_status_enabled)
END;
gun_depress_Trigger_Local(gg) =
PRE
gg∈ gun
THEN
gun_trigger(gg) := th_status_depressed
END;
gun_release_Trigger_Local(gg) =
PRE
gg∈ gun
THEN
gun_trigger(gg) := th_status_released
END
 
 
END

Code:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
/* Holster
* Author: siat555
* Creation date: 19/12/2015
*/
MACHINE
Holster
SEES
Types
VARIABLES
holster,holster_switch
INVARIANT
holster⊆ HOLSTER ∧
holster_switch∈ holster → TH_STATUS
INITIALISATION
ANY hh WHERE
hh⊆ HOLSTER ∧
card(hh) = 5
THEN
holster := hh ||
holster_switch := hh * {th_status_released}
END
OPERATIONS
holster_release(hh) =
PRE
hh∈ holster ∧
holster_switch(hh) = th_status_depressed
THEN
holster_switch(hh) := th_status_released
END;
holster_depress(hh) =
PRE
hh∈ holster ∧
holster_switch(hh) = th_status_released
THEN
holster_switch(hh) := th_status_depressed
END
 
 
END

Code:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
/* IntermediateMachine
* Author: siat555
* Creation date: 19/12/2015
*/
MACHINE
IntermediateMachine
SEES
Types
VARIABLES
clutch,
clutch_status,
gun,
gun_status,
gun_trigger,
holster,
holster_switch,
motor,
motor_status,
pump,
pump_pump_Id,
pump_status,
delivery,
delivery_cost,
delivery_volume,
delivery_grade,
delivery_pump_Id,
delivery_veh_Id,
display,
display_cost,
display_volume,
display_grade,
display_veh_Id,
clutchPump,
gunPump,
holsterPump,
motorPump,
displayPump
INVARIANT
clutch⊆ CLUTCH ∧
clutch_status∈ clutch → C_STATUS ∧
gun⊆ GUN ∧
gun_status∈ gun → PG_STATUS ∧
gun_trigger∈ gun → TH_STATUS ∧
holster⊆ HOLSTER ∧
holster_switch∈ holster → TH_STATUS ∧
motor⊆ MOTOR ∧
motor_status∈ motor → M_STATUS ∧
pump⊆ PUMP ∧
pump_pump_Id∈ pump ↣ PU_ID ∧
pump_status∈ pump → PG_STATUS ∧
delivery⊆ DELIVERY ∧
delivery_cost∈ delivery → COST ∧
delivery_volume∈ delivery → NAT ∧
delivery_grade∈ delivery → GRADE ∧
∀ deli.(deli ∈ delivery ⇒delivery_grade(deli) ↦delivery_cost(deli)
∈costOfGrade) ∧
delivery_pump_Id∈ delivery → PU_ID ∧
delivery_veh_Id∈ delivery → VEH_ID ∧
display⊆ DISPLAY ∧
display_cost∈ display → COST ∧
display_volume∈ display → NAT ∧
display_grade∈ display → GRADE ∧
∀ disp.(disp∈ display ⇒display_grade(disp) ↦display_cost(disp) ∈costOfGrade) ∧
display_veh_Id∈ display → VEH_ID ∧
clutchPump∈ pump >->> clutch ∧
gunPump∈ pump >->> gun ∧
holsterPump∈ pump >->> holster ∧
motorPump∈ pump >->> motor ∧
displayPump∈ pump >->> display
INITIALISATION
ANY cc,dd,gg,hh,mm,pp,vi WHERE
cc ⊆ CLUTCH ∧
card(cc) = 5 ∧
dd⊆ DISPLAY ∧
card(dd) = 5 ∧
gg⊆ GUN ∧
card(dd) = 5 ∧
hh⊆ HOLSTER ∧
card(hh) = 5 ∧
mm⊆ MOTOR ∧
card(mm) = 5 ∧
pp ⊆ PUMP ∧
card(pp) = 5 ∧
vi∈ VEH_ID
THEN
clutch := cc ||
clutch_status := cc * {c_status_free}||
gun := gg||
gun_status := gg * {pg_status_disabled} ||
gun_trigger := gg * {th_status_released}||
holster := hh ||
holster_switch := hh * {th_status_released} ||
motor := mm ||
motor_status := mm * {m_status_off} ||
ANY pi WHERE
pi∈ pp ↣ PU_ID
THEN
pump := pp ||
pump_pump_Id := pi ||
pump_status := pp * {pg_status_disabled}
END ||
display := dd ||
display_cost := dd * {cost1} ||
display_volume := dd * {0} ||
display_grade := dd * {grade1} ||
display_veh_Id := dd * {vi} ||
ANY cp,gp,hp,mp,dp WHERE
cp∈ pp >->> cc ∧
gp∈ pp >->>gg∧
hp∈ pp >->>hh∧
mp∈ pp >->> mm ∧
dp∈ pp >->>dd
THEN
clutchPump := cp ||
gunPump := gp ||
holsterPump := hp ||
motorPump := mp ||
displayPump := dp
END
END ||
 
 
delivery,
delivery_cost,
delivery_volume,
delivery_grade,
delivery_pump_Id,
delivery_veh_Id := ∅,∅,∅,∅,∅,∅
OPERATIONS
pump_enable(pp,gg,vi) =
PRE
pp ∈ pump ∧
gg∈ GRADE ∧
vi∈ VEH_ID
THEN
IF pump_status(pp) = pg_status_disabled THEN
pump_status(pp) := pg_status_enabled ||
display_grade(displayPump(pp)) := gg ||
display_cost(displayPump(pp)) := costOfGrade(gg) ||
display_volume(displayPump(pp)) := 0 ||
display_veh_Id(displayPump(pp)) := vi ||
motor_status(motorPump(pp)) := m_status_on ||
clutch_status(clutchPump(pp)) := c_status_free
ELSE
skip
END
END;
pump_delivery_Complete(pp) =
PRE
pp ∈ pump ∧
pump_status(pp) = pg_status_enabled
THEN
pump_status(pp) := pg_status_disabled ||
ANY dd WHERE
dd∈ DELIVERY
THEN
delivery := delivery ∪ {dd} ||
delivery_cost(dd) := display_cost(displayPump(pp)) ||
delivery_grade(dd) := display_grade(displayPump(pp)) ||
delivery_volume(dd) := display_volume(displayPump(pp)) ||
delivery_pump_Id(dd) := pump_pump_Id(pp) ||
delivery_veh_Id(dd) := display_veh_Id(displayPump(pp)) ||
motor_status(motorPump(pp)) := m_status_off
END
END;
pp ←pump_pumpOfId_Dum(pi) =
PRE
pi∈ PU_ID ∧
pi∈ ran(pump_pump_Id)
THEN
pp := pump_pump_Id⁻¹(pi)
END;
bb←pump_is_Enabled_Dum(pp) =
PRE
pp ∈ pump
THEN
bb := bool(pump_status(pp) = pg_status_enabled)
END;
gun_enable_Dum(gg) =
PRE
gg∈ gun
THEN
gun_status(gg) := pg_status_enabled
END;
gun_disable_Dum(gg) =
PRE
gg∈ gun
THEN
gun_status(gg) := pg_status_disabled
END;
en←gun_is_Enabled_Dum(gg) =
PRE
gg∈ gun
THEN
en := bool(gun_status(gg) = pg_status_enabled)
END;
gun_depress_Trigger_Local_Dum(gg) =
PRE
gg∈ gun
THEN
gun_trigger(gg) := th_status_depressed
END;
gun_release_Trigger_Local_Dum(gg) =
PRE
gg∈ gun
THEN
gun_trigger(gg) := th_status_released
END;
clutch_free_Dum(cc) =
PRE
cc ∈ clutch
THEN
clutch_status(cc) := c_status_free
END;
clutch_engage_Dum(cc) =
PRE
cc ∈ clutch
THEN
clutch_status(cc) := c_status_engaged
END;
holster_release_Dum(hh) =
PRE
hh∈ holster ∧
holster_switch(hh) = th_status_depressed
THEN
holster_switch(hh) := th_status_released
END;
holster_depress_Dum(hh) =
PRE
hh∈ holster ∧
holster_switch(hh) = th_status_released
THEN
holster_switch(hh) := th_status_depressed
END;
cc ←clutchOfPump_Dum(pp) =
PRE
pp ∈ pump
THEN
cc :=clutchPump(pp)
END;
gg←gunOfPump_Dum(pp) =
PRE
pp∈pump
THEN
gg :=gunPump(pp)
END;
pp ←pumpOfGun_Dum(gg) =
PRE
gg∈ gun
THEN
pp := gunPump⁻¹(gg)
END;
pp ←pumpOfHolster_Dum(hh) =
PRE
hh∈ holster
THEN
pp := holsterPump⁻¹(hh)
END;
display_pulse_Dum(disp) =
PRE
disp∈ display
THEN
IF display_volume(disp) < MAXINT THEN
display_volume(disp) := display_volume(disp) + 1
ELSE
skip
END
END
 
 
END

Code:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
/* IntermediateMachine_imp
* Author: siat555
* Creation date: 19/12/2015
*/
 
IMPLEMENTATION IntermediateMachine_imp
REFINES IntermediateMachine
 
SEES
Types
IMPORTS
BasicMachine
OPERATIONS
pump_enable(pp,gg,vi) =
VAR
pe,dd,mm,cc
IN
pe←pump_is_Disabled(pp);
IF
pe = TRUE THEN
pump_enable_Local(pp);
dd←displayOfPump(pp);
display_reset(dd,gg,vi);
mm←motorOfPump(pp);
motor_start(mm);
cc ←clutchOfPump(pp);
clutch_free(cc)
ELSE
skip
END
END;
pump_delivery_Complete(pp) =
VAR
disp,cc,vv,gg,pi,dd,mm,vi
IN
pump_disable_Local(pp);
disp←displayOfPump(pp);
cc,vv,gg,vi←display_read_Display(disp);
pi←pump_idOfPump(pp);
dd←delivery_create_Delivery(cc,vv,gg,pi,vi);
mm←motorOfPump(pp);
motor_stop(mm)
END;
pp ←pump_pumpOfId_Dum(pi) =
pp ←pump_pumpOfId(pi);
bb←pump_is_Enabled_Dum(pp) =
bb←pump_is_Enabled(pp);
gun_enable_Dum(gg) =
gun_enable(gg);
gun_disable_Dum(gg) =
gun_disable(gg);
en←gun_is_Enabled_Dum(gg) =
en←gun_is_Enabled(gg);
gun_depress_Trigger_Local_Dum(gg) =
gun_depress_Trigger_Local(gg);
gun_release_Trigger_Local_Dum(gg) =
gun_release_Trigger_Local(gg);
clutch_free_Dum(cc) =
clutch_free(cc);
clutch_engage_Dum(cc) =
clutch_engage(cc);
holster_release_Dum(hh) =
holster_release(hh);
holster_depress_Dum(hh) =
holster_depress(hh);
cc ←clutchOfPump_Dum(pp) =
cc ←clutchOfPump(pp);
gg←gunOfPump_Dum(pp) =
gg←gunOfPump(pp);
pp ←pumpOfGun_Dum(gg) =
pp ←pumpOfGun(gg);
pp ←pumpOfHolster_Dum(hh) =
pp ←pumpOfHolster(hh);
display_pulse_Dum(disp) =
display_pulse(disp)
 
END

Code:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
/* Motor
* Author: siat555
* Creation date: 19/12/2015
*/
MACHINE
Motor
SEES
Types
VARIABLES
motor,motor_status
INVARIANT
motor⊆ MOTOR ∧
motor_status∈ motor → M_STATUS
INITIALISATION
ANY mm WHERE
mm⊆ MOTOR ∧
card(mm) = 5
THEN
motor := mm ||
motor_status := mm * {m_status_off}
END
OPERATIONS
motor_start(mm) =
PRE
mm∈ motor
THEN
motor_status(mm) := m_status_on
END;
motor_stop(mm) =
PRE
mm∈ motor
THEN
motor_status(mm) := m_status_off
END
 
 
END

Code:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
/* Pump
* Author: siat555
* Creation date: 19/12/2015
*/
MACHINE
Pump
SEES
Types
VARIABLES
pump,
pump_pump_Id,
pump_status
INVARIANT
pump⊆ PUMP ∧
pump_pump_Id∈ pump ↣ PU_ID ∧
pump_status∈ pump → PG_STATUS
INITIALISATION
ANY pp,pi WHERE
pp ⊆ PUMP ∧
card(pp) = 5 ∧
pi∈ pp ↣ PU_ID
THEN
pump := pp ||
pump_pump_Id := pi ||
pump_status := pp * {pg_status_disabled}
END
OPERATIONS
pp ←pump_pumpOfId(pi) =
PRE
pi∈ PU_ID ∧
pi∈ ran(pump_pump_Id)
THEN
pp := pump_pump_Id⁻¹(pi)
END;
ip←pump_idOfPump(pp) =
PRE
pp ∈ pump
THEN
ip := pump_pump_Id(pp)
END;
bb←pump_is_Enabled(pp) =
PRE
pp ∈ pump
THEN
bb := bool(pump_status(pp) = pg_status_enabled)
END;
bb←pump_is_Disabled(pp) =
PRE
pp ∈ pump
THEN
bb := bool(pump_status(pp) = pg_status_disabled)
END;
pump_enable_Local(pp) =
PRE
pp ∈ pump ∧
pump_status(pp) = pg_status_disabled
THEN
pump_status(pp) := pg_status_enabled
END;
pump_disable_Local(pp) =
PRE
pp ∈ pump
THEN
pump_status(pp) := pg_status_disabled
END
 
END

Code:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
/* SystemMachine
* Author: siat555
* Creation date: 19/12/2015
*/
MACHINE
SystemMachine
SEES
Types
VARIABLES
clutch,
clutch_status,
gun,
gun_status,
gun_trigger,
holster,
holster_switch,
motor,
motor_status,
pump,
pump_pump_Id,
pump_status,
delivery,
delivery_cost,
delivery_volume,
delivery_grade,
delivery_pump_Id,
delivery_veh_Id,
display,
display_cost,
display_volume,
display_grade,
display_veh_Id,
clutchPump,
gunPump,
holsterPump,
motorPump,
displayPump
INVARIANT
clutch⊆ CLUTCH ∧
clutch_status∈ clutch → C_STATUS ∧
gun⊆ GUN ∧
gun_status∈ gun → PG_STATUS ∧
gun_trigger∈ gun → TH_STATUS ∧
holster⊆ HOLSTER ∧
holster_switch∈ holster → TH_STATUS ∧
motor⊆ MOTOR ∧
motor_status∈ motor → M_STATUS ∧
pump⊆ PUMP ∧
pump_pump_Id∈ pump ↣ PU_ID ∧
pump_status∈ pump → PG_STATUS ∧
delivery⊆ DELIVERY ∧
delivery_cost∈ delivery → COST ∧
delivery_volume∈ delivery → NAT ∧
delivery_grade∈ delivery → GRADE ∧
∀ deli.(deli ∈ delivery ⇒delivery_grade(deli) ↦delivery_cost(deli) ∈costOfGrade) ∧
delivery_pump_Id∈ delivery → PU_ID ∧
delivery_veh_Id∈ delivery → VEH_ID ∧
display⊆ DISPLAY ∧
display_cost∈ display → COST ∧
display_volume∈ display → NAT ∧
display_grade∈ display → GRADE ∧
∀ disp.(disp∈ display ⇒display_grade(disp) ↦display_cost(disp) ∈costOfGrade) ∧
display_veh_Id∈ display → VEH_ID ∧
clutchPump∈ pump >->> clutch ∧
gunPump∈ pump >->> gun ∧
holsterPump∈ pump >->> holster ∧
motorPump∈ pump >->> motor ∧
displayPump∈ pump >->> display
INITIALISATION
ANY cc,dd,gg,hh,mm,pp,vi WHERE
cc ⊆ CLUTCH ∧
card(cc) = 5 ∧
dd⊆ DISPLAY ∧
card(dd) = 5 ∧
gg⊆ GUN ∧
card(dd) = 5 ∧
hh⊆ HOLSTER ∧
card(hh) = 5 ∧
mm⊆ MOTOR ∧
card(mm) = 5 ∧
pp ⊆ PUMP ∧
card(pp) = 5 ∧
vi∈ VEH_ID
THEN
clutch := cc ||
clutch_status := cc * {c_status_free} ||
gun := gg ||
gun_status := gg * {pg_status_disabled} ||
gun_trigger := gg * {th_status_released} ||
holster := hh ||
holster_switch := hh * {th_status_released} ||
motor := mm ||
motor_status := mm * {m_status_off} ||
ANY pi WHERE
pi∈ pp ↣ PU_ID
THEN
pump := pp ||
pump_pump_Id := pi ||
pump_status := pp * {pg_status_disabled}
END||
display := dd ||
display_cost := dd * {cost1} ||
display_volume := dd * {0} ||
display_grade := dd * {grade1} ||
display_veh_Id := dd * {vi} ||
ANY cp,gp,hp,mp,dp WHERE
cp∈ pp >->> cc ∧
gp∈ pp >->>gg∧
hp∈ pp >->>hh∧
mp∈ pp >->> mm ∧
dp∈ pp >->>dd
THEN
clutchPump := cp ||
gunPump := gp ||
holsterPump := hp ||
motorPump := mp ||
displayPump := dp
END
END||
delivery,
delivery_cost,
delivery_volume,
delivery_grade,
delivery_pump_Id,
delivery_veh_Id := ∅,∅,∅,∅,∅,∅
OPERATIONS
pump_enable_Pump(pi,gg,vi) =
PRE
pi∈ PU_ID ∧
pi∈ ran(pump_pump_Id) ∧
gg∈ GRADE ∧
vi∈ VEH_ID
THEN
IF pump_status(pump_pump_Id⁻¹(pi)) = pg_status_disabled THEN
pump_status(pump_pump_Id⁻¹(pi)) := pg_status_enabled ||
display_grade(displayPump(pump_pump_Id⁻¹(pi))) := gg ||
display_cost(displayPump(pump_pump_Id⁻¹(pi))) := costOfGrade(gg) ||
display_volume(displayPump(pump_pump_Id⁻¹(pi))) := 0 ||
display_veh_Id(displayPump(pump_pump_Id⁻¹(pi))) := vi ||
motor_status(motorPump(pump_pump_Id⁻¹(pi))) := m_status_on ||
clutch_status(clutchPump(pump_pump_Id⁻¹(pi))) := c_status_free
ELSE
skip
END
END;
holster_remove_Gun(hh) =
PRE
hh∈ holster ∧
holster_switch(hh) = th_status_depressed
THEN
holster_switch(hh) := th_status_released ||
gun_status(gunPump(holsterPump⁻¹(hh))) := pg_status_enabled
END;
gun_depress_Trigger(gg) =
PRE
gg∈ gun
THEN
gun_trigger(gg) := th_status_depressed ||
IF
pump_status(gunPump⁻¹(gg)) = pg_status_enabled∧
gun_status(gg) = pg_status_enabled
THEN
clutch_status(clutchPump(gunPump⁻¹(gg))) := c_status_engaged
ELSE
skip
END
END;
gun_release_Trigger(gg) =
PRE
gg∈ gun
THEN
gun_trigger(gg) := th_status_released ||
IF pump_status(gunPump⁻¹(gg)) = pg_status_enabled∧
gun_status(gg) = pg_status_enabled
THEN
clutch_status(clutchPump(gunPump⁻¹(gg))) := c_status_free
ELSE
skip
END
END;
holster_replace_Gun(hh) =
PRE
hh∈ holster ∧
holster_switch(hh) = th_status_released
THEN
holster_switch(hh) := th_status_depressed ||
gun_status(gunPump(holsterPump⁻¹(hh))) :=pg_status_disabled ||
IF
pump_status(holsterPump⁻¹(hh)) = pg_status_enabled
THEN
pump_status(holsterPump⁻¹(hh)) := pg_status_disabled ||
ANY dd WHERE
dd∈ DELIVERY
THEN
delivery := delivery ∪ {dd} ||
delivery_cost(dd) := display_cost(displayPump(holsterPump⁻¹(hh))) ||
delivery_grade(dd) := display_grade(displayPump(holsterPump⁻¹(hh))) ||
delivery_volume(dd):= display_volume(displayPump(holsterPump⁻¹(hh))) ||
delivery_pump_Id(dd) := pump_pump_Id(holsterPump⁻¹(hh)) ||
delivery_veh_Id(dd) := display_veh_Id(displayPump(holsterPump⁻¹(hh))) ||
motor_status(motorPump(holsterPump⁻¹(hh))) := m_status_off
END
END
END;
display_pulse_Dum_Dum(disp) =
PRE
disp∈ display
THEN
IF display_volume(disp) < MAXINT THEN
display_volume(disp) := display_volume(disp) + 1
ELSE
skip
END
END
 
 
END

Code:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
/* System_imp
* Author: siat555
* Creation date: 19/12/2015
*/
 
IMPLEMENTATION System_imp
REFINES SystemMachine
 
SEES
Types
IMPORTS
IntermediateMachine
OPERATIONS
pump_enable_Pump(pi,gg,vi) =
VAR
pp
IN
pp ←pump_pumpOfId_Dum(pi);
pump_enable(pp,gg,vi)
END;
holster_remove_Gun(hh) =
VAR
pp,gg
IN
pp ←pumpOfHolster_Dum(hh);
gg←gunOfPump_Dum(pp);
holster_release_Dum(hh);
gun_enable_Dum(gg)
END;
 
 
gun_depress_Trigger(gg) =
VAR
pp,ge,pe,cc
IN
gun_depress_Trigger_Local_Dum(gg);
pp ←pumpOfGun_Dum(gg);
pe←pump_is_Enabled_Dum(pp);
ge←gun_is_Enabled_Dum(gg);
IF
pe = TRUE ∧ge = TRUE
THEN
cc ←clutchOfPump_Dum(pp);
clutch_engage_Dum(cc)
END
END;
 
 
gun_release_Trigger(gg) =
VAR
pp,ge,pe,cc
IN
gun_release_Trigger_Local_Dum(gg);
pp ←pumpOfGun_Dum(gg);
pe←pump_is_Enabled_Dum(pp);
ge←gun_is_Enabled_Dum(gg);
IF
pe = TRUE ∧ge = TRUE
THEN
cc ←clutchOfPump_Dum(pp);
clutch_free_Dum(cc)
END
END;
 
holster_replace_Gun(hh) =
VAR
pp,gg,pe
IN
holster_depress_Dum(hh);
pp ←pumpOfHolster_Dum(hh);
gg←gunOfPump_Dum(pp);
gun_disable_Dum(gg);
pe←pump_is_Enabled_Dum(pp);
IF pe = TRUE THEN
pump_delivery_Complete(pp)
ELSE
skip
END
END;
display_pulse_Dum_Dum(disp) =
display_pulse_Dum(disp)
 
END

Code:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
/* Types
* Author: siat555
* Creation date: 19/12/2015
*/
MACHINE
Types
SETS
OBJECTS;
GRADE = {grade1,grade2};
COST = {cost1,cost2};
PU_ID;
PG_STATUS = {pg_status_enabled,pg_status_disabled};
TH_STATUS = {th_status_depressed,th_status_released};
M_STATUS = {m_status_on,m_status_off};
C_STATUS = {c_status_engaged,c_status_free};
VEH_ID
CONSTANTS
costOfGrade,PUMP,DELIVERY,GUN,DISPLAY,HOLSTER,CLUTCH,MOTOR
PROPERTIES
costOfGrade∈ GRADE >->> COST ∧
costOfGrade(grade1) = cost1 ∧
costOfGrade(grade2) = cost2 ∧
PUMP ⊆ OBJECTS ∧
DELIVERY ⊆ OBJECTS ∧
GUN ⊆ OBJECTS ∧
DISPLAY ⊆ OBJECTS ∧
HOLSTER ⊆ OBJECTS ∧
CLUTCH ⊆ OBJECTS ∧
MOTOR ⊆ OBJECTS
 
 
END