Fichier d'entrée B : clapet.b


MACHINE
  Clapet
SETS
  ETATCLAPET = {ouvert, ferme}
VARIABLES
  temp
, clapet

INVARIANT
  temp : NAT
& clapet : ETATCLAPET
& temp <= 30
& clapet = ferme

INITIALISATION
   temp := 20
|| clapet := ferme

OPERATIONS
  fermerClapet = 
  BEGIN
    clapet := ferme
  END
;
  ouvrirClapet = 
    clapet := ouvert
;
  monterTemp = 
  CHOICE
    temp := temp +1
  OR
    temp := temp +3
  END
;
  baisserTemp = 
  PRE
    temp > 10
  THEN
    temp := temp -1
  END
END