Assignment 5 - due before class on Wednesday, March 10 (NOTE ONLY 1.5 weeks)

Tasks you will need to do before starting:

• Read section 8. Note problem 2 is a toughie.

Resources you will need:

• Access to LTSA. Use this site to download: ltsa.jar. This should give you a jar file that is double-clickable.

Problem 1

See if you can replace IMPROVEDSAFETY on page 170 with fluent and assert. You can find the original code in the homework folder.

Turn-in: Turn in lts.

Problem 2

Do exercise 8.3 in back of chapter 8 (an extension of exercise 8.2).

The FIFO part of this problem is tricky. One idea is to define a QUEUE process and then use that in a safety property that unifies the QUEUE with the gas station. In essence, the property defines how things operate in a queue and then you make sure they work that way in gas station. Here is some code that starts down this approach:

const N = 3 //number of customers
const M = 2 //number of pumps

range P = 1..M
range C = 1..N
range A = 1..2 //Amount of money or Gas

CELL = (put[i:C] -> get[i]->CELL).
//minimal
||QUEUE = (cell[C]:CELL)
/...
property ||FIFO = QUEUE/{forall[i:C] { //link actions to gas station

There are several important notes about this problem:

• This is not an issue of a critical section: any number of customers can prepay at once. The problem is making sure that the order that they prepay is the order they get their gas.
• The property you are checking is a strange one in a real gas station. It says that it expects the model to have customers finish getting their gas in the order they prepaid. Of course, this is an odd requirement. What if someone only wants a gallon of gas. They have to wait for someone else to finish just because the other person prepaid first? Weird, but that is what the property checks.
• The model from 8.2 is *not* expected to meet the property. So 8.3 is asking you to write a property to show that the 8.2 model is broken.
• To reiterate, you do not have to build a *model* that meets the FIFO property, only a property that checks a model for it. In essence, you should get property failure. HOWEVER, if someone wants the challenge of trying to work the QUEUE into the model itself, please give it a shot!
• I'll tell you that the textbook solution has a twist on prepaying. If customer c prepays and a pump is free, c immediately gets the pump, *before* anyone else can prepay. If there is no pump free, c is in line for a pump. However, the line is only 1 long; can't have 2 customers in line. This finesses the need for a queue waiting for pumps. Just don't let customers prepay if someone is in line already. Hmmmmm.
• Exercise 3.2 might be a hint for defining the QUEUE model.

Turn-in: lts code.