Spin Assignment solutions

                                                          - Siva Sylesh Vommi
                                                                 - 11QE30006

Q1. Model the above vending machine using spin. Using LTL, specify a response property thatasserts: If a request for a drink is sent to the vending machine then the corresponding drink will eventually be delivered. Verify that your model is correct with respect to your response property.

Answer 1:

Code: 1 mtype {coin5,coin10,coin15,coin20,tea,coffee,milk,juice} 2 chan coin_channel [1] of {mtype}; 3 chan drinks_channel [1] of {mtype}; 4 proctype cutomer () { 5 if 6 :: coin_channel!coin5; 7 drinks_channel?tea; 8 :: coin_channel!coin10; 9...