BOWLING HALL:

Purpose: To gain experience with and confidence in writing FSP descriptions and the model-based design approach given in [MK 8].

We will model a control system for a bowling hall.

Start up an editor and the LTS Analyser LTSA.

• [Step 1]: The first step is to analyse the informal requirement specification (we got from the manager):

  Bowling Hall requirement specification:
  "When a customer enters the bowling hall, (s)he pays me for getting a lane for a number of hours, and I record the payment with his/her name on a blackboard next to the clock. When a bowling lane becomes free, the customer will occupy it (with friends) and the customer will write his/her name (which is signaled to me). Then, the customer waits until I activate the lane (which means activating the computer calculating the score and the system for raising the pins). It must not be possible to use the lane for more hours than the customer pays for and the lane must not deactivate before the number of hours the customer has payed for has passed. When the lane deactivates, the customer leaves it and it becomes free again."
  Note: For simplicity, we assume that there is just a single bowling lane and two customers.

  Go through the four steps (cf. [MK 8.1.2]) and write down the result:

  • [Step 1a]: Identify the main actions(/events) and interactions;
  • [Step 1b]: Identify the main processes, and consider whether they are active or passive (and/or shared);
  • [Step 1c]: Identify the properties of interest; and
  • [Step 1d]: Structure the processes into an architecture (draw a structure diagram).

• [Step 2]: Write FSP descriptions (and/or draw the LTS) for each of the processes identified above.

• [Step 3]: Compare your analysis with this attempt of a model (Bowling.lts); explain the differences (if any) from what you expected from your analysis.

• [Step 4]: Specify and check the safety properties (if you give up, you may look here (HappyManager.lts) where the first one is specified).

• [Step 5]: Try to change the model such that the Manager always records that the customer pays for one hour even if (s)he pays for two. Verify the safety-property again.

• [Step 6]: Now we change the given model to...

  ||BOWLINGHALL = (LANE || MANAGER || BOARD || CUSTOMERS) /{take/acquire}.

  ...(i.e., leave and release do not synchronize).

  The result is that the customer may leave before the time is up, and the lane just deactivates when the time is up.

• [Step 7]: Now the HappyManager.lts safety property is violated, but only because the manager may receive more money than he expects (why?).

• [Step 8]: Change the model such that the manager only permits two paying customers in the hall at any given time. Verify that the HappyManager.lts safety property is now satisfied.

• [Step 9]: In his first description, the manager forgot an important progress property; after a customer has payed, (s)he should eventually get a lane. Specify this property and check it in LTSA for our first attempt of a model.

• [Step 10]: Is the progress property satisfied if one of the customers' take action gets high priority?

• [Step 11]: Is the progress property satisfied if a customer's take action gets low priority?

• [Step 12]: If you have time, try to extend the system to have two lanes.