Süsteemide modelleerimine 2019/20 sügis

Lecture Exercises

We can do a couple simple examples and a larger examples from last year. The larger ones are more interesting, but they require too much time to be suitable as exam exercises.

Exam Example 1

Consider a system where each process simply assigns values to a variable x by going through the values from zero up to 5 then down to 0 and then again up again. If we run this as a single process it should just yield the trace where the values of x are 0, 1, 2, 3, 4, 5, 4, 3, 2, 1, 0, 1, 2, 3, 4, 5, ...

• State in temporal logic that the values of the variable x is always between 0 and 5.
• State that whenever we look at the system, we will from that point eventually reach a state where x has the value 5.
• Is any of the above properties a liveness property?
• Do the above properties hold for a single thread?
• What about two threads, assuming strong fairness and that checks and increments are atomic (as in the spec below)?
• If any property does not hold, provide a counter-example. (In this case, just a sequence of the values of x would suffice, but you may also indicate who set it by using two columns.)

-------------------------------- MODULE cyclic --------------------------------
EXTENDS Integers 
CONSTANT Threads

(* --algorithm cyclic

variables x = 0

fair+ process cycle \in Threads
begin 
  Inc:
  while x < 5 do
    x := x + 1
  end while;
  Dec:
  while x > 0 do
    x := x - 1
  end while;
  goto Inc
end process

end algorithm *)
=============================================================================

Exam Example 2

Assume we have two processes that share a single integer variable x. The first process (U) increases or decreases this variable at will (nondeterministic choice) under the constraint that it will only decide to increase if x < 1 and only decides to decrease if x > -1. The decision to do this and the actual increment/decrement is not atomic. The second process (I) waits until x is zero and then immediately increases it. This process is atomic and strongly fair.

• State the following properties in temporal logic.
  • x is never 2.
  • x is eventually 2.
• Which of the following hold:
  • x is never -2.
  • x is never 2.
  • x is eventually -2.
  • x is eventually -1.
  • x is eventually 1.
  • x is eventually 2.
• If any of them fail, provide the counter example trace. For each step, you should at least indicate which process (U or I) made the move and whether it set or checked the value of x and what value it is assigned. For example, starting with x=0, U check x>-1 and decides to decrement, I sets x to 1, U now sets x to 0, ...
• Does anything change if the increment process would not be atomic?

-------------------------------- MODULE inc --------------------------------
EXTENDS Integers 
CONSTANT Threads

(* --algorithm inc

variables x = 0

fair+ process updown = "updown"
begin Decide:
  while TRUE do
  either
    when x < 1;
    Inc:
    x := x + 1;
  or 
    when x > -1;
    Dec:
    x := x - 1;
  end either;
  end while
end process

fair+ process inc = "inc"
begin 
  Check:
    await x = 0;
    x := x + 1;
  goto Check
end process
=============================================================================

Larger example: Elevators

------------------------------ MODULE elevator ------------------------------
EXTENDS Integers

CONSTANT Elevators
CONSTANT NumFloors


(* --algorithm elevator

variables
  loc = [e \in Elevators |-> 1],
  dir = [e \in Elevators |-> "UP"],
  idle = Elevators,
  req = {}

define
  Floors == 1..NumFloors
  current_floors == { loc[e] : e \in Elevators }
end define

fair process requesting = "req"
begin Press:
  with b \in Floors do
    if b \notin current_floors then
      req := req \cup {b}
    end if
  end with;
  goto Press
end process

fair process elevator \in Elevators
begin 
  Check:
  if loc[self] \in req then
    Open: 
    req := req \ {loc[self]};
    idle := idle \cup {self}
  end if;
  Move:
  await self \notin idle;
  if dir[self] = "UP" then
    loc[self] := loc[self] + 1
  else
    loc[self] := loc[self] - 1
  end if;
  goto Check
end process


fair process controller = "ctrl"
begin 
  Controller:
  await req /= {} /\ idle /= {};
  with e \in idle do
    if \E f \in req : f < loc[e] then 
      dir[e] := "DOWN"
    elsif \E f \in req : f > loc[e] then
      dir[e] := "UP"
    end if;
    idle := idle \ {e}
  end with;
  goto Controller
end process

end algorithm *)

=============================================================================

We are modelling an elevator controller. We track the following variables: loc (the location of each elevator), dir (the direction the elevator is moving), idle (the set of elevators without a destination) and req (the set of requested floors; that is, people can press buttons on the floors or within the elevator, we just consider the set of active requests).

We have three processes. The requesting process simply adds requests non-deterministically. Requests can happen at any time with the only exception is that we don’t add requests while the elevator is on the same floor. Dealing with this would make the task more complicated; typically, elevators opens the door again, but we’re not going to simulate this.

The second process is the elevator that just follows the instructions of the controller. Upon reaching a floor, it checks if this is a requested floor and removes the request and sets itself to idle and waits for instructions: as soon as the controller makes it not idle, it will move in whatever direction the controller indicates.

The controller handles all the logic. It waits until there are some requests and elevators ready to move. It then just picks an elevator and sends it to a floor very arbitrarily:

• if some request exists below, the elevator will be sent down
• else if some request exists above, the elevator moves up.
• Otherwise we keep moving in the same direction!

(We could have just had a simple if request exist above, move up, else move down, but we’re going to modify the strategy later and I want that change to be minimal.)

Analyze this system for defects and you may use TLA+ as an assistant. The there are two important things that I will grade here: first, precision and correctness of the temporal logic property, and second, the clarity of your explanation of the counter example trace. It's critical to narrate the situation that goes wrong; you don’t have to include every single step of the trace.

• First let’s explore if the system is safe: the controller will not send the elevators outside the given range. Specify a safety property NoCrash that states all elevators are located between floors 1 and NumFloors.
• Create a model with a single elevator (set of model values {e1}) and just two floors (ordinary assignment 2). This should work, but add a second elevator to the set and you should see an invariant violation. Explain the trace!
• Now specify the following liveness property that should say that all floors are eventually served. More precisely, specify the property AllServed to say that all floors are always eventually removed from the set of requests.
• Go back to a model with a single elevator. This should work for two floors, but try a single elevator and set NumFloors to 3. You should get a temporal property violation. Explain the trace!
• Can you think of a way to fix the problem? The code is written is such a way to really minimize the needed fix. We can make a small change in the controller, so elevators switch direction when all requests are below or above the current location. Can you clarify what needs to be changed?