EXAMPLES
EXAMPLES
Example I: Ether Net Is the capacity of Medium Unbounded Is the order of the message respected Sender Medium Receiver 2021年1月27日星期三上海交通大学计算机系 BASICS实验室
2021年1月27日星期三 上海交通大学计算机系BASICS实验室 33 Example I: Ether Net Sender Medium Receiver ◼ Is the Capacity of Medium Unbounded? ◼ Is the Order of the Message Respected?
Example ii: Vending machine Vending Machine The slot can accept 1c coin The buttons can be pressed for a cup of tea or coffee Tea or coffee can be tea collected from the tray Interaction between Machine and buyer 2021年1月27日星期三上海交通大学计算机系 BASICS实验室
2021年1月27日星期三 上海交通大学计算机系BASICS实验室 34 Example II: Vending Machine ◼ Vending Machine ◼ The slot can accept 1c coin ◼ The buttons can be pressed for a cup of tea or coffee ◼ Tea or coffee can be collected from the tray ◼ Interaction between Machine and Buyer tea coffee
Transition The state transition Blue is the initial state Green is the state after collect-tea receiving lc One of the other two states is reached after cofree the tea-button or the collect-coffee coffee-button is pressed 2021年1月27日星期三上海交通大学计算机系 BASICS实验室
2021年1月27日星期三 上海交通大学计算机系BASICS实验室 35 Transition ◼ The State Transition ◼ Blue is the initial state ◼ Green is the state after receiving 1c ◼ One of the other two states is reached after the tea-button or the coffee-button is pressed collect-tea collect-coffee tea coffee 1c
Nondeterminism The vending machine Out of order tea Having taking in 1c, the vending machine collect-tea disable the tea-button or coffee-button collect-coffee nondeterministically 2021年1月27日星期三上海交通大学计算机系 BASICS实验室
2021年1月27日星期三 上海交通大学计算机系BASICS实验室 36 Nondeterminism ◼ The Vending Machine Out of Order ◼ Having taking in 1c, the vending machine disable the tea-button or coffee-button nondeterministically 1c 1c tea coffee collect-tea collect-coffee