learning_tla/learn_tla/core/06-nondeterminism.md

6. Non-determinism

with

with can be used for local variables within a label:

---- MODULE foo ----
(*--algorithm foo
begin
    with roll \in 1..6 do
      sum := sum + roll;
      print sum
    end with;
end algorithm *)
====

This is NOT a loop: all 6 values of roll will be applied, meaning at every pass, the RHS sum will be the initial value of 0, not mutating a shared value to increase it.

This is what is called nondeterministic: assigning values from a non-singleton set instead of a singleton.

The with has nothing to do with determinism: it can also be used with deterministic assignments.

either-or

either is a non-deterministic control flow: use as many or as needed:

begin
    either
      approve_pull_request();
    or
      request_changes();
    or
      reject_request();
end either;

Each statement within the either or an or can have labels: their are not atomic.

This is especially useful for state machines.

Using non-determinism

This is where we start to differ from programming languages, because we evaluate all cases, not a sequential flow.

Non-determinism is useful for outside actions, like in this example for a Web service:

RequestType == [from: Client, type: {"GET", "POST"}, params: ParamType]

with request \in RequestType do
  if request.type = "GET" then
    \* get logic
  elsif request.type = "POST" then
    \* post logic
  else
    \* something's wrong with our spec!
    assert FALSE;
  end if;
end with;