CoffeeorTea ::= Coffee | Tea
ReportError ::= Out_of_Sugar | Out_of_Tea | Out_of_Coffee
ReadyToServe ::= Ready | NotReady
WithorWithout ::= Sugar | Black
È_VendingMachine _______________________________
®Drink:
CoffeeorTea Ä WithorWithout
®CupVolume:
N1
®HowMuchSugar:
N1
®CoffeeLevel:
N
®MaxCoffeeLevel:
N1
®TeaLevel:
N
®MaxTeaLevel:
N1
®SugarLevel:
N
®MaxSugarLevel:
N1
®Status:
ReadyToServe
Ç_______________
®CoffeeLevel
ø
MaxCoffeeLevel
®CupVolume
ø
MaxCoffeeLevel ¦ CupVolume ø MaxTeaLevel
®HowMuchSugar
ø
MaxSugarLevel
®#
Drink = 1
®TeaLevel
ø
MaxTeaLevel
®SugarLevel
ø
MaxSugarLevel
Ð_______________________________________
È_RefilSupplies________________________________
®DVendingMachine
Ç_______________
®Status' =
NotReady
®CoffeeLevel'
= MaxCoffeeLevel
®TeaLevel'
= MaxTeaLevel
®SugarLevel'
= MaxSugarLevel
®MaxTeaLevel'
= MaxTeaLevel
®MaxCoffeeLevel'
= MaxCoffeeLevel
®MaxSugarLevel'
= MaxSugarLevel
®HowMuchSugar'
= HowMuchSugar
®CupVolume'
= CupVolume
Ð_______________________________________
È_DispenseCoffee _______________________________
® MakeSelection
Ç_______________
® Coffee e dom Drink
®Black e ran Drink
®Status
= Ready
®CoffeeLevel
ù
CupVolume
®CoffeeLevel'
= CoffeeLevel - CupVolume
®Status'
= NotReady
Ð_______________________________________
È_DispenseTea_________________________________
® MakeSelection
Ç_______________
® Tea e dom Drink
®Black e ran Drink
®Status
= Ready
®TeaLevel
ù
CupVolume
®TeaLevel'
= TeaLevel - CupVolume
®Status'
= NotReady
Ð_______________________________________
È_OutOfSugar _________________________________
® MakeSelection
®rep!:
ReportError
Ç_______________
® dom Drink ë 0
®Sugar e ran Drink
®SugarLevel
= 0
®Status'
= NotReady
®rep! =
Out_of_Sugar
Ð_______________________________________
È_MakeSelection________________________________
® D VendingMachine
®DrinkType?:
CoffeeorTea
®Sweetened?:
WithorWithout
Ç_______________
® dom Drink' = DrinkType?
®ran
Drink' = Sweetened?
®CoffeeLevel'
= CoffeeLevel
®TeaLevel'
= TeaLevel
®SugarLevel'
= SugarLevel
®MaxTeaLevel'
= MaxTeaLevel
®MaxCoffeeLevel'
= MaxCoffeeLevel
®MaxSugarLevel'
= MaxSugarLevel
®HowMuchSugar'
= HowMuchSugar
®CupVolume'
= CupVolume
®
Ð_______________________________________
È_DispenseCoffeeWithSugar___________________________
®DDispenseCoffee
Ç_______________
®Sugar e ran Drink
®SugarLevel
ù
HowMuchSugar
®SugarLevel'
= SugarLevel - HowMuchSugar
®Status'
= NotReady
Ð_______________________________________
È_DispenseTeaWithSugar ____________________________
®DDispenseTea
Ç_______________
®Sugar e ran Drink
®SugarLevel
ù
HowMuchSugar
®SugarLevel'
= SugarLevel - HowMuchSugar
®Status'
= NotReady
Ð_______________________________________
È_OutOfTea __________________________________
® MakeSelection
®rep!:
ReportError
Ç_______________
® Tea e dom Drink
®TeaLevel
= 0
®Status'
= NotReady
®rep! =
Out_of_Tea
Ð_______________________________________
È_ReadyState _________________________________
® DVendingMachine
Ç_______________
® Status =
NotReady
®
CoffeeLevel' = CoffeeLevel
®TeaLevel'
= TeaLevel
®SugarLevel'
= SugarLevel
®MaxTeaLevel'
= MaxTeaLevel
®MaxCoffeeLevel'
= MaxCoffeeLevel
®MaxSugarLevel'
= MaxSugarLevel
®HowMuchSugar'
= HowMuchSugar
®CupVolume'
= CupVolume
®Drink'
= 0
®Status'
= Ready
Ð_______________________________________
È_OutOfCoffee_________________________________
® MakeSelection
®rep!:
ReportError
Ç_______________
® Coffee e dom Drink
®CoffeeLevel
= 0
®Status'
= NotReady
®rep! =
Out_of_Coffee
Ð_______________________________________
DoDispenseCoffee ê (DispenseCoffee v DispenseCoffeeWithSugar v OutOfSugar v OutOfCoffee) ¦ ReadyState
DoDispenseTea ê (DispenseTea v DispenseTeaWithSugar v OutOfSugar v OutOf Tea) ¦ ReadyState
Refilling ê RefilSupplies ¦ ReadyState
Selection ê DoDispenseCoffee v DoDispenseTea v Refilling