Systems Modelling 2018/19 fall

Lecture Exercises

DataOutputStream.html

------------------------------ MODULE writeint ------------------------------
EXTENDS Integers, Sequences

CONSTANT WordSize
CONSTANT Writers

(* --algorithm writeint

variables
  stream = <<>>;

fair process server = "server"
variable 
  words_read = 0,
  readnum = 0
begin 
  Read:
    while words_read < WordSize do
      await stream /= <<>>;
      readnum := readnum + Head(stream) * 256^words_read;
      stream := Tail(stream);
      words_read := words_read + 1
    end while;
  Again:
    words_read := 0;
    readnum := 0;
    goto Read
end process

fair process writer \in Writers
variable 
  words_written = 0,
  number \in {0, 1}
begin
  Write:
  while words_written < WordSize do
    stream := Append(stream, number % 256);
    number := number \div 256;
    words_written := words_written + 1
  end while

end process

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

Cinema.tla

Model a cinema ticket booking system.

• The room has a couple of seats :)
• Seats can be either free, booked, or purchased.
• The user can during seat selection either book more seats or unhook seats.
• In the end, the user can either purchase the tickets or cancel/timeout.

We want to make sure two people are not sold the same seat! What operations have to be atomic for this to hold. Atomicity is costly to implement, so use it sparingly!

Solution will appear after...