TLA Exercise (Exam 2)
We will model a payment system for a car sharing company here in Estonia. You will discover a bug that is based on a true story. The company CEO manually resolved the situation. Obviously, the system here is simplified. We have three processes: time models the fact that credit cards expire, the user process will either try to make a purchase or update the payment method with a valid credit card, and the payment process will attempt to make purchases. If a purchase fails, it will be added to the set of failed transactions. These have to be cleared before the user can make another purchase. Note that users are here identified with their credit cards, just as in the real world…
Task 5: TLA+ specification. Your task is primarily to understand this specification, write two simple properties and then simulate this either in your head or with the assistance of TLA to explain what goes wrong.
- First, write down the property that all purchases are valid. The variable purchases is only introduced in order for us to check this. Note that the check and purchase is actually atomic, but still this should fail. [Only graded at exam]
- Create a model (you can use a single credit card as customer). Run this with the property you defined above. Hint: I use the word property in the general sense here. This is a property that should hold globally; such properties are called invariants! It should fail. Explain the counter-example! [2 points]
- Remove that property because we check for failures and add them to the failed set. This can still cause a problem. Specify the property that all credit cards will always be eventually processed. [Only graded at exam]
- This should also fail! Find the counter-example that required manual intervention… [3 points]
The TLA source is available here: http://bit.ly/2SXEFYk