learning_tla/learn_tla/core/02-writing-specs.md

2. Writing specifications

PlusCal and TLA

PlusCal is a DSL generating TLA+ specs.

• := is only used when we have an existing variable and want to update its value.
• Otherwise we just use =

The labels represent everything that can happen in a single step of the system. They represent the Temporal Logic of Actions, or TLA.

When using PlusCal while like:

Sum:
    while i <= Len(seq) do
        x := x + seq[i]
        i := i + 1
    end while;

each iteration of the loop is non-atomic: time passes between each passing in front of Sum.

Label rules

• each statement MUST belong to one label
  • implies that every algorithm starts with a label
• any variable can only be updated AT MOST ONCE per label
  • because a label represents an instant in time (a state)
• Simultaneous assignment: x := x+1 || x := 2*x

  • Avoids the problem with this being wrong because it causes two mutations:

    Label:
        x := x + 1
        x := 2 * x
    

PlusCal expressions

Statement level

• skip: no operation
• assert <expr>: fails the model if <expr> is FALSE.
  • Fails the model immediately without executing the rest of the code in the label
  • Needs an EXTENDS TLC
  • The error trace will NOT show the step with the failing assert. Prefer invariants.
• goto L where L is a label.
  • Another label must appear immediately after goto

Block level

if / then / else

if Expr then
  skip;
elsif Expr2 then
  skip;
else
  skip;
end if;

Branches can contain labels. If any does, the block must be followed by a label.

macro

Macros appear before the begin.

• Since they are not part of the algorithm, they cannot contain labels, complex statements, and they cannot be recursive
• They are just textual replacements, like m4.

macro inc(var) begin
  if var < 10 then
    var := var + 1;
  end if;
end macro;

with

These blocks create temporary assignments within a label, so they cannot contain labels.

The assignments use :=.

with tmp_x = x, tmp_y = y do
  y := tmp_x;
  x := tmp_y;
end with;

while

The while loop is non-atomic. It must be preceded by a label, and instants exist for each run of the loop passing by the label.

Sum:
  while i <= Len(seq) do
    x := x + seq[i];
    Inc:
      i := i + 1;
  end while;