Süsteemide modelleerimine 2018/19 sügis

TLA Homework

See information about Extra Credit.

For this homework, you have some choices. In all case, you should work through Chapter 10 of Practical TLA. You can then decide between the following options.

Option 1: Just Analyze

If you want an easy way out, you can just work through the example provided in the book. You will submit a text document about your experience. This document will contain three components:

• Your declaration of which steps you have completed (see checklist below). I will trust that you are honest, so you do not need to prove this. You will simply copy each bullet point into your document when you have done it. If you do have comments or questions about any of these steps, you may add them to the document.
• You will write a paragraph about why modelling in TLA is incredibly useful. If you are not a convert yourself, you can use phrases like "Hillel Wayne writes", "According to the book", "TLA fanboys claim", and so on. Either way, you should attempt to express why people find value in this.
• Once you have clearly stated why (some people say) TLA is tremendously useful, I would like to hear your opinion. This should be an informed opinion. I don't care if you are positive or negative, but you should provide some sensible argumentation.

The steps to be completed when working through the example:

• We read the requirements and created a module with the initial version of the example. We created the OneCopyPerBook model and got it to run.
• We added the Type Invariant and tried a change that introduced a type error to make sure the check was enabled.
• We added the Liveness condition stating that people eventually get the books they want and ran the model checker. We understood why this failed.
• We tried the set of reservations and understood the problem with sets.
• We added the invariant for ordered queues without duplicate elements and added the code the prevents duplicates. (Note: Range is defined here.)
• We were reminded that one also should remove reservations, so we added this as well.
• We verified that the system was correct for a single person and single book, so we then created a model with two books. We saw that this failed.
• We updated the assumption on how people behave to only check out books they want to read. We saw that this results in a deadlock.
• We added the possibility for people to want to read more books as time passes. We saw that this violates the Liveness condition as specified before.
• We updated the Liveness condition, but saw that People can still just insist on reading the same book and not reach their reading ambitions. We modified the user behavior to see if the system works for people who complete their reading list.
• We then finally tried this for two people! In this model, we found a deadlock and understood the trace.
• We implemented expiring reservations and relaxed the Liveness condition to only require that a person has the opportunity to check out the book. We tried this and found that users can still block others, and this happens even if they only reserve books they want to read.
• Finally, we tried and verified the design if restricted to people who only want to read a single book at a time.

Option 2: More Creative Exercise

Having looked a few examples, such as the above-mentioned or Wayne's eSpark learning, try to model something of interest to yourself. If you work in software development, maybe you can analyze some system at work using TLA+.

You should submit your TLA source file as well as brief experience report containing what you tried and whether you gained any insight. This creative effort will be grade extremely generously: any decent attempt to model something semi-realistic and check one meaningful property, will receive full grades. Your experience need not be positive: if the only "insight" you gained was that TLA was a complete waste of time, you can freely state so in your conclusion.

If you run into problems during this exercise, you can get help! During this course, I offer free consultations on TLA+ modelling. You could also hire Hillel Wayne, but that could cost more; of course, you get what you pay for... But, seriously, I would love to chat and if you are trying to model some real-world application.

Option 3: Exam Exercise

The original plan was to guide you to model a system based on Chapter 10 of the book. I have not been able to turn this into a guided exercise, so we will instead have an exercise where you are given the system specification in the PlusCal language and use TLA (or your brain) to model check the system.

---------------------------- MODULE deliverybots ----------------------------
EXTENDS Sequences, Integers

CONSTANT Users
CONSTANT Robots
CONSTANT Goods

(* --algorithm deliverybots

variables
  orders = <<>>,
  deliveries = <<>>,
  warehouse = Goods,
  postbox = [u \in Users |-> {}],
  status = [u \in Users |-> "OPEN"],
  satisfied = [u \in Users |-> FALSE]

define
  OrderStatus == {"OPEN", "ACCEPT", "REJECT"}
  TypeOK == /\ orders \in Seq( [product : Goods, client : Users] )
            /\ status \in [Users -> OrderStatus] 
            /\ warehouse \subseteq Goods 
end define

macro add(set, e)    begin set := set \cup {e} end macro
macro remove(set, e) begin set := set \ {e}    end macro

macro dequeue(queue, result)
begin
  await queue /= <<>>;
  result := Head(queue);
  queue := Tail(queue)
end macro
macro enqueue(queue, e) begin queue := Append(queue,e) end macro

fair process purchasing = "procurer"
begin
  Restock:
    await warehouse /= Goods;
    with p \in Goods \ warehouse do 
      add(warehouse, p);
    end with;
  goto Restock
end process

fair process sales = "seller"
variable order
begin
  ProcessOrder: 
    dequeue(orders, order);
  CheckStatus:
  if order.product \in warehouse then
    remove(warehouse, order.product);
    status[order.client] := "ACCEPT";
    enqueue(deliveries, order);
  else
    status[order.client] := "REJECT"
  end if;
  goto ProcessOrder
end process

fair process robot \in Robots
variable delivery
begin
  ProcessDelivery:
    dequeue(deliveries, delivery);
  Deliver:
    add(postbox[delivery.client], delivery.product);
  goto ProcessDelivery
end process

fair process user \in Users
variable
  current
begin
  PrepareOrder:
    satisfied[self] := FALSE;
    with g \in Goods do current := g end with;
  PlaceOrder:
    enqueue(orders, [product |-> current, client |-> self]);
    status[self] := "OPEN";
  WaitForResponse:
    await status[self] /= "OPEN";
  CheckResponse:
    if status[self] = "REJECT" then 
      goto PlaceOrder
    end if;
  WaitForDelivery: 
    await current \in postbox[self];
  UseIt:
    remove(postbox[self], current);
    satisfied[self] := TRUE;
    goto PrepareOrder
end process
end algorithm *)
=============================================================================

Try to understand the above model. It helps if you have read the textbook. We have four processes here modelling a delivery system. The users places orders and these are prepared for delivery robots to deliver. When the warehouse is empty it is replenished. This should all be familiar from previous examples, so your first task is to understand the above formal specification.

1. The variable satisfied is added only to allow us to specify the key liveness property. Define a predicate in temporal logic that expresses our expectation that all users will always be eventually satisfied.
2. Create a model and check this property with one user and one robot. (This should work!) Then, add another user and explain the error trace!
3. Fix the system (along the lines of the book chapter to allow reservations). This is somewhat open-ended and not the sort of thing you will be asked in the exam.

You should submit a PDF where you explain you answers. If you extended the model, also submit the tla source file.