Upload
sidonie-jaouen
View
103
Download
0
Embed Size (px)
Citation preview
Le tampon à deux places
Une idée de Steve Dunne, University of Teesside
Présentée dans cet amphi en 2002
Le tampon à deux places
in out
[in, in, out, in, out, in, out, out, in, in]
[in, in, out, out, out], [in, out, out], [in, in, in],… non possibles
Diagramme de transitions
0
2
1
out
outin
in
Événements modélisés commedes opérations gardées
Opérations qui NE SONT pasappelées, contrairement auxOpérations préconditionnées duB classique
Automate/ Arbre Jackson
M1
*
outin
*
outin
0
2
1
out
outin
in
M = (in . (in . Out) * out) *
Le tampon à 2 places
MACHINE M1
VARIABLESstate
INVARIANTstate : 0..2
INITIALISATIONstate := 0
Le tampon à 2 places, en B
OPERATIONSin =
SELECT state = 0 THEN state := 1 WHEN state = 1 THEN state := 2END;
out =SELECT state = 1 THEN state := 0WHEN state = 2 THEN state := 1END;
move = skip
END
Zoom
in out
in out
move
2 automates communicants
in out
move
producteur consommateur
Producteur et Consommateur
0
1
0
1
in move move out
PROD
*
in move
PROD CONSCONS
*
move out
L’automate du système
0
1
0
1
in move out
PROD CONS0,0
1,0
0,1
1,1
in
move
in
out
out
out
Produit d’automate
0,0
1,0
0, 1
1, 1
in move
in
out
out
out
Machine B Producteur
MACHINEPROD
VARIABLESpstate
INVARIANTpstate : 0..1
INITIALISATIONpstate := 0
OPERATIONSin = SELECT pstate = 0 THEN pstate := 1 END;pmove = SELECT pstate = 1 THEN pstate := 0END
END
0
1
in move
PROD
Machine B Consommateur
MACHINECONS
VARIABLEScstate
INVARIANTcstate : 0..1
INITIALISATIONcstate := 0
OPERATIONSout= SELECT cstate = 1 THEN cstate := 0 END;
cmove = SELECT cstate = 0 THEN cstate := 1END
0
1
move out
CONS
La machine SystèmeMACHINE
M2
INCLUDES
PROD, CONS
PROMOTES
in, out
OPERATIONS
move = pmove ||
cmove
END
PRODin
pmove
M2
INCLUDES
move
CONScmove
out
Implantation
IMPLEMENTATIONM1_I/* machine to prove that M2 simulates M1 , with the technique of Ken Robinson */
REFINESM1
IMPORTSM2
PROMOTESin, out, move
END