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