Systems Modelling 2019/20 fall

TLA Exercises

The PlusCal reference.

Lecture Example, part 1

Let's try to do the second example from Chapter 5 of Practical TLA+ together. You may start with the initial code from here:

------------------------------- MODULE cache -------------------------------

EXTENDS Integers, Sequences, TLC
CONSTANT ResourceCap, MaxConsumerReq

ASSUME ResourceCap > 0
ASSUME MaxConsumerReq \in 1..ResourceCap

(*--algorithm cache
variables resources_left = ResourceCap;
define
  ResourceInvariant == resources_left >= 0
end define;

process actor = "actor"
variables
  resources_needed \in 1..MaxConsumerReq
begin
  UseResources:
    while TRUE do
      (* Replace me with a check! *)
      resources_left := resources_left - resources_needed;  
    end while;
end process;

process time = "time"
begin
  Tick:
    resources_left := ResourceCap;
    goto Tick;
end process;
end algorithm; *)
=============================================================================

Try to create a model that satisfy the assumptions. See that it will fail the resource invariant because we aren't actually checking it. Then, add the following check await resources_left >= resources_needed; just before the resource is used. Make sure this now passes.

Lecture Example, part 2

Adding more actors... Change the actor process to have to processes: you can simply change the line process actor = "actor" to process actor \in {"actor1", "actor2"}. Or you can use model constants for this. Try to run this again. It should still be correct, but now let's see if consuming resources is not atomic and how that can be made safe. Change the body of the actor process to the following:

    WaitForResources:
    while TRUE do
      when resources_left >= resources_needed;
      UseResources:
        while resources_needed > 0 do
          resources_left := resources_left - 1;
          resources_needed := resources_needed - 1;
        end while;
      with x \in 1..MaxConsumerReq do
        resources_needed := x;
      end with;
    end while;

You should see that this does not work. Let's try to fix it by allowing us to reserve resources. Add a variable reserved = 0 and change the code checking resources:

await reserved + resources_needed <= resources_left;
reserved := reserved + resources_needed;

At each tick, when resources are restored, we can reset the reserved variable to zero, right?

Ferryman

A classic problem in model checking is the ferryman problem... You have a ferryman, goat, cabbage, and wolf who want to cross the river. The ferryman can cross with at most one passenger. The following combination of items violate the invariant of things remaining uneaten:

1. the goat and the cabbage on the same side without ferryman
2. the goat and the wolf on the same side without ferryman

Can the ferryman transport get them all over to the other side? Or more precisely, can TLA find a way to transport them over?