# A comparison with TLA+¶

In this notebook we'll go through the example from Hillel Wayne's Learn TLA+ to find out how concepts in TLA+ correspond to concepts in Imandra.

This notebook is intended to be read side-by-side with Hillel's example. We'll quote certain snippets from Learn TLA+ and explain how we could achieve the same in Imandra.

## The Problem¶

You’re writing software for a bank. You have Alice and Bob as clients, each with a certain amount of money in their accounts. Alice wants to send some money to Bob. How do you model this? Assume all you care about is their bank accounts.

## Step One¶

For this example, we could model the transfer algorithm very simply as a single function in Imandra. However, for comparison we'll try to model in a similar way to the PlusCal style. To do this we'll write our algorithm as a state machine.

The example defines the PlusCal variables alice_account, bob_account and money. For this we'll define a state record:

In :
type state =
{ alice_account : int
; bob_account : int
; money : int
}

let init =
{ alice_account = 10
; bob_account = 10
; money = 5
}

Out:
type state = { alice_account : int; bob_account : int; money : int; }
val init : state = {alice_account = 10; bob_account = 10; money = 5}


A: and B: are labels. They define the steps the algorithm takes. Understanding how labels work is critical to writing more complex algorithms, as they define the places where your concurrency can go horribly awry.

We choose to model the steps A and B as a variant type action. The function step, given an action and a state, computes one step of the algorithm.

In :
type action =
| A
| B

let step action state =
match action with
| A -> { state with alice_account = state.alice_account - state.money }
| B -> { state with bob_account = state.bob_account + state.money }

Out:
type action = A | B
val step : action -> state -> state = <fun>


Now we can put everything together to define the transfer algorithm:

In :
let transfer state =
state |> step A |> step B

Out:
val transfer : state -> state = <fun>


So how do we run this? Well, we can’t.

In Imandra, this is real code! We can execute it, leveraging the OCaml runtime. Let's take a look at the results of executing each step:

In :
init;;
init |> step A;;
init |> step A |> step B;;

Out:
- : state = {alice_account = 10; bob_account = 10; money = 5}
- : state = {alice_account = 5; bob_account = 10; money = 5}
- : state = {alice_account = 5; bob_account = 15; money = 5}


## Assertions and Sets¶

Can Alice’s account go negative? Right now our spec allows that, which we don’t want. We can start by adding a basic assert check after the transaction.

In Imandra, we encode contracts and properties using verify statements.

In :
verify (fun state ->
state.alice_account = 10 &&
state.bob_account = 10 &&
state.money = 5
==>
let state' = transfer state in
state'.alice_account >= 0
)

Out:
- : state -> bool = <fun>

Proved
proof
ground_instances0
definitions0
inductions0
search_time
0.029s
details
Expand
smt_stats
 num checks 1 rlimit count 249 mk bool var 6 num allocs 2.57509e+06 memory 6.4 max memory 6.8
Expand
• start[0.029s]
:var_0:.alice_account = 10 && :var_0:.bob_account = 10 && :var_0:.money = 5
==> (if B = A
then
{alice_account = ….alice_account - ….money;
bob_account = ….bob_account; money = ….money}
else
{alice_account = ….alice_account;
bob_account = ….bob_account + ….money; money = ….money}).alice_account
>= 0
• #### simplify

 into not ((:var_0:.alice_account = 10 && :var_0:.bob_account = 10) && :var_0:.money = 5) || (:var_0:.alice_account + -1 * :var_0:.money) >= 0 expansions [] rewrite_steps forward_chaining
• #### unsat

(let ((a!1 (>= (+ (alice_account_15 state_27) (* (- 1) (money_17 state_27))) 0))
(a!2 (monoton…

Here we've used the ==> operator. a ==> b can be read as "a implies b". We're saying: if both Alice and Bob's accounts are 10, and money is 5, then after the transfer Alice's account will not be negative.

Imandra has shown that our statement is true!

At the very least, it works for the one number we tried. That doesn’t mean it works for all cases. When testing, it’s often hard to choose just the right test cases to surface the bugs you want to find. This is because most languages make it easy to test a specific state but not a large set of them. In TLA+, though, testing a wide range is simple.

The only thing we changed was money = 5 to money \in 1..20

Let's amend our verify statement to test the same range:

In :
verify (fun state ->
state.alice_account = 10 &&
state.bob_account = 10 &&
List.mem state.money List.(1 -- 20)
==>
let state' = transfer state in
state'.alice_account >= 0
)

Out:
- : state -> bool = <fun>
module CX : sig val state : state end

Counterexample (after 32 steps, 0.095s):
let (state : state) = {alice_account = 10; bob_account = 10; money = 11}

Refuted
proof attempt
ground_instances32
definitions0
inductions0
search_time
0.095s
details
Expand
smt_stats
 num checks 65 arith assert lower 26 rlimit count 12614 mk clause 82 datatype occurs check 127 mk bool var 323 arith assert upper 8 datatype splits 20 decisions 115 propagations 89 conflicts 77 datatype accessor ax 22 arith assert diseq 22 datatype constructor ax 66 num allocs 7.04482e+06 final checks 53 added eqs 263 del clause 71 arith eq adapter 27 memory 7.43 max memory 7.43
Expand
• start[0.095s]
:var_0:.alice_account = 10
&& :var_0:.bob_account = 10 && List.mem :var_0:.money (List.( -- ) 1 20)
==> (if B = A
then
{alice_account = ….alice_account - ….money;
bob_account = ….bob_account; money = ….money}
else
{alice_account = ….alice_account;
bob_account = ….bob_account + ….money; money = ….money}).alice_account
>= 0
• #### simplify

 into not ((:var_0:.alice_account = 10 && :var_0:.bob_account = 10) && List.mem :var_0:.money (List.( -- ) 1 20)) || (:var_0:.alice_account + -1 * :var_0:.money) >= 0 expansions [] rewrite_steps forward_chaining
• unroll
 expr (|List.--_533| 1 20) expansions
• unroll
 expr (|List.mem_1215| (money_17 state_30) (|List.--_533| 1 20)) expansions
• unroll
 expr (|List.--_533| (+ 1 1) 20) expansions
• unroll
 expr (|List.--_533| (+ 1 1 1) 20) expansions
• unroll
 expr (|List.mem_1215| (money_17 state_30) (|get.::.1_1214| (|List.--_533| 1 20))) expansions
• unroll
 expr (|List.--_533| (+ 1 1 1 1) 20) expansions
• unroll
 expr (|List.--_533| (+ 1 1 1 1 1) 20) expansions
• unroll
 expr (|List.mem_1215| (money_17 state_30) (|get.::.1_1214| (|get.::.1_1214| (|List.--_53… expansions
• unroll
 expr (|List.--_533| (+ 1 1 1 1 1 1) 20) expansions
• unroll
 expr (let ((a!1 (|get.::.1_1214| (|get.::.1_1214| (|get.::.1_1214| (|List.--_533| 1 … expansions
• unroll
 expr (|List.--_533| (+ 1 1 1 1 1 1 1) 20) expansions
• unroll
 expr (|List.--_533| (+ 1 1 1 1 1 1 1 1) 20) expansions
• unroll
 expr (let ((a!1 (|get.::.1_1214| (|get.::.1_1214| (|get.::.1_1214| (|List.--_533| 1 … expansions
• unroll
 expr (|List.--_533| (+ 1 1 1 1 1 1 1 1 1) 20) expansions
• unroll
 expr (let ((a!1 (|get.::.1_1214| (|get.::.1_1214| (|get.::.1_1214| (|List.--_533| 1 … expansions
• unroll
 expr (|List.--_533| (+ 1 1 1 1 1 1 1 1 1 1) 20) expansions
• unroll
 expr (|List.--_533| (+ 1 1 1 1 1 1 1 1 1 1 1) 20) expansions
• unroll
 expr (let ((a!1 (|get.::.1_1214| (|get.::.1_1214| (|get.::.1_1214| (|List.--_533| 1 … expansions
• unroll
 expr (|List.--_533| (+ 1 1 1 1 1 1 1 1 1 1 1 1) 20) expansions
• unroll
 expr (let ((a!1 (|get.::.1_1214| (|get.::.1_1214| (|get.::.1_1214| (|List.--_533| 1 … expansions
• unroll
 expr (|List.--_533| (+ 1 1 1 1 1 1 1 1 1 1 1 1 1) 20) expansions
• unroll
 expr (|List.--_533| (+ 1 1 1 1 1 1 1 1 1 1 1 1 1 1) 20) expansions
• unroll
 expr (let ((a!1 (|get.::.1_1214| (|get.::.1_1214| (|get.::.1_1214| (|List.--_533| 1 … expansions
• unroll
 expr (|List.--_533| (+ 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1) 20) expansions
• unroll
 expr (let ((a!1 (|get.::.1_1214| (|get.::.1_1214| (|get.::.1_1214| (|List.--_533| 1 … expansions
• unroll
 expr (|List.--_533| (+ 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1) 20) expansions
• unroll
 expr (|List.--_533| (+ 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1) 20) expansions
• unroll
 expr (let ((a!1 (|get.::.1_1214| (|get.::.1_1214| (|get.::.1_1214| (|List.--_533| 1 … expansions
• unroll
 expr (|List.--_533| (+ 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1) 20) expansions
• unroll
 expr (let ((a!1 (|get.::.1_1214| (|get.::.1_1214| (|get.::.1_1214| (|List.--_533| 1 … expansions
• unroll
 expr (|List.--_533| (+ 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1) 20) expansions
• unroll
 expr (|List.--_533| (+ 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1) 20) expansions
• Sat (Some let (state : state) = {alice_account = 10; bob_account = 10; money = 11} )

Now Imandra has found a counterexample to our verify statement. Like TLA+, Imandra gives us concrete values that make our statement false. We can also compute with these values to get more insight:

In :
CX.state;;
CX.state |> step A;;
CX.state |> step A |> step B;;

Out:
- : state = {alice_account = 10; bob_account = 10; money = 11}
- : state = {alice_account = -1; bob_account = 10; money = 11}
- : state = {alice_account = -1; bob_account = 21; money = 11}


We can fix this by wrapping the check in an if-block:

In :
let transfer state =
if state.alice_account >= state.money then
state |> step A |> step B
else
state

Out:
val transfer : state -> state = <fun>


Which now runs properly.

In :
verify (fun state ->
state.alice_account = 10 &&
state.bob_account = 10 &&
List.mem state.money List.(1 -- 20)
==>
let state' = transfer state in
state'.alice_account >= 0
)

Out:
- : state -> bool = <fun>

Proved
proof
ground_instances0
definitions0
inductions0
search_time
0.011s
details
Expand
smt_stats
 num checks 2 arith assert lower 1 arith pivots 2 rlimit count 646 mk clause 3 mk bool var 30 arith assert upper 5 decisions 2 arith add rows 5 propagations 5 conflicts 4 datatype accessor ax 3 arith conflicts 1 arith assert diseq 1 datatype constructor ax 2 num allocs 1.20429e+07 added eqs 24 del clause 1 arith eq adapter 3 memory 10.83 max memory 10.83
Expand
• start[0.011s]
:var_0:.alice_account = 10
&& :var_0:.bob_account = 10 && List.mem :var_0:.money (List.( -- ) 1 20)
==> (if :var_0:.alice_account >= :var_0:.money
then
if B = A then {alice_account = …; bob_account = …; money = …}
else {alice_account = …; bob_account = …; money = …}
else :var_0:).alice_account
>= 0
• #### simplify

 into not ((:var_0:.alice_account = 10 && :var_0:.bob_account = 10) && List.mem :var_0:.money (List.( -- ) 1 20)) || (if :var_0:.alice_account >= :var_0:.money then {alice_account = :var_0:.alice_account + -1 * :var_0:.money; bob_account = :var_0:.bob_account + :var_0:.money; money = :var_0:.money} else :var_0:).alice_account >= 0 expansions [] rewrite_steps forward_chaining
• #### unsat

(let ((a!1 (|rec_mk.state_1232|
(+ 10 (* (- 1) (money_17 state_35)))
(+ 10…

Quick aside: this is closer to testing all possible cases, but isn’t testing all possible cases. Would the algorithm break if money was, say, 4997? If we actually wanted to test all possible cases, we could replace money \in 1..20 with money \in Nat, where Nat is the set of natural numbers. This is perfectly valid TLA+. Unfortunately, it’s also something the model checker can’t handle. TLC can only check a subset of TLA+, and infinite sets aren’t part of that.

Imandra is capable of handling infinite sets. We can do this by simply removing the constraint that state.money is in the range 1 to 20. Instead, we'll require that it is non-negative:

In :
verify (fun state ->
state.alice_account = 10 &&
state.bob_account = 10 &&
state.money >= 0
==>
let state' = transfer state in
state'.alice_account >= 0
)

Out:
- : state -> bool = <fun>

Proved
proof
ground_instances0
definitions0
inductions0
search_time
0.058s
details
Expand
smt_stats
 num checks 1 arith assert lower 2 arith pivots 2 rlimit count 589 mk clause 3 mk bool var 30 arith assert upper 3 decisions 1 arith add rows 5 propagations 3 conflicts 2 datatype accessor ax 3 arith conflicts 1 datatype constructor ax 2 num allocs 2.58832e+07 added eqs 22 del clause 1 arith eq adapter 2 memory 14.04 max memory 14.51
Expand
• start[0.058s]
:var_0:.alice_account = 10
&& :var_0:.bob_account = 10 && :var_0:.money >= 0
==> (if :var_0:.alice_account >= :var_0:.money
then
if B = A then {alice_account = …; bob_account = …; money = …}
else {alice_account = …; bob_account = …; money = …}
else :var_0:).alice_account
>= 0
• #### simplify

 into not ((:var_0:.alice_account = 10 && :var_0:.bob_account = 10) && :var_0:.money >= 0) || (if :var_0:.alice_account >= :var_0:.money then {alice_account = :var_0:.alice_account + -1 * :var_0:.money; bob_account = :var_0:.bob_account + :var_0:.money; money = :var_0:.money} else :var_0:).alice_account >= 0 expansions [] rewrite_steps forward_chaining
• #### unsat

(let ((a!1 (|rec_mk.state_1258|
(+ 10 (* (- 1) (money_17 state_38)))
(+ 10…

Imandra has shown that this property holds for all possible non-negative integer values of money.

## TLA+ and Invariants¶

Can you transfer a negative amount of money? We could add an assert money > 0 to the beginning of the algorithm. This time, though, we’re going to introduce a new method in preparation for the next section.

TLA+ allows you write down invariants that will be checked for each state of the system.

We can achieve the same with Imandra:

In :
verify (fun action state ->
state.alice_account = 10 &&
state.bob_account = 10 &&
state.money >= 0
==>
let state' = step action state in
state'.money >= 0
)

Out:
- : action -> state -> bool = <fun>

Proved
proof
ground_instances0
definitions0
inductions0
search_time
0.021s
details
Expand
smt_stats
 num checks 1 arith assert lower 4 rlimit count 503 mk clause 3 mk bool var 36 arith assert upper 2 datatype splits 1 decisions 3 propagations 8 conflicts 4 datatype accessor ax 5 arith conflicts 1 arith assert diseq 1 datatype constructor ax 2 num allocs 5.02192e+07 added eqs 35 del clause 1 arith eq adapter 3 memory 14.51 max memory 14.91
Expand
• start[0.021s]
:var_0:.alice_account = 10
&& :var_0:.bob_account = 10 && :var_0:.money >= 0
==> (if :var_1: = A
then
{alice_account = :var_0:.alice_account - :var_0:.money;
bob_account = :var_0:.bob_account; money = :var_0:.money}
else
{alice_account = :var_0:.alice_account;
bob_account = :var_0:.bob_account + :var_0:.money;
money = :var_0:.money}).money
>= 0
• #### simplify

 into not ((:var_0:.alice_account = 10 && :var_0:.bob_account = 10) && :var_0:.money >= 0) || (if :var_1: = A then {alice_account = :var_0:.alice_account + -1 * :var_0:.money; bob_account = :var_0:.bob_account; money = :var_0:.money} else {alice_account = :var_0:.alice_account; bob_account = :var_0:.bob_account + :var_0:.money; money = :var_0:.money}).money >= 0 expansions [] rewrite_steps forward_chaining
• #### unsat

(let ((a!1 (|rec_mk.state_1277|
(+ 10 (* (- 1) (money_17 state_42)))
10
…

Imandra has proven that for any state and after processing any action, money is always non-negative: the invariant holds for all states of the system.

## One step further: checking Atomicity¶

So far we haven’t done anything too out of the ordinary. Everything so far is easily coverable in a real system by unit and property tests. There’s still a lot more ground to cover, but I want to show that we can already use what we’ve learned to find more complicated bugs. Alice wants to give Bob 1,000 dollars. If we’re unlucky, it could play out like this:

1. System checks that Alice has enough money
2. \$1,000 is deducted from her account 3. Eve smashes in the server with a baseball bat 4. Bob never receives the money 5. \$1,000 has completely disappeared from the system
6. The SEC shuts you down for fraud.

We already have all of the tools to check this. First, we need to figure out how to represent the broken invariant. We could do that by requiring the total money in the system is always the same:

In our Imandra model we could express this as follows: given any state and any action, the total money in the system at the start should be equal to the total money in the system afterwards:

In :
let account_total state =
state.alice_account + state.bob_account

verify (fun action state ->
state.money >= 0
==>
let state' = step action state in
account_total state = account_total state'
)

Out:
val account_total : state -> Z.t = <fun>
- : action -> state -> bool = <fun>
module CX : sig val action : action val state : state end

Counterexample (after 0 steps, 0.021s):
let (action : action) = B
let (state : state) = {alice_account = 0; bob_account = 8855; money = 1}

Refuted
proof attempt
ground_instances0
definitions0
inductions0
search_time
0.021s
details
Expand
smt_stats
 num checks 1 arith assert lower 3 arith pivots 3 rlimit count 618 mk clause 8 datatype occurs check 5 mk bool var 35 arith assert upper 4 datatype splits 1 decisions 3 arith add rows 6 propagations 3 arith fixed eqs 2 datatype accessor ax 6 arith assert diseq 1 datatype constructor ax 3 num allocs 8.20233e+07 final checks 1 added eqs 24 del clause 2 arith eq adapter 3 memory 15.06 max memory 15.55
Expand
• start[0.021s]
:var_0:.money >= 0
==> :var_0:.alice_account + :var_0:.bob_account =
(if :var_1: = A
then
{alice_account = :var_0:.alice_account - :var_0:.money;
bob_account = :var_0:.bob_account; money = :var_0:.money}
else
{alice_account = :var_0:.alice_account;
bob_account = :var_0:.bob_account + :var_0:.money;
money = :var_0:.money}).alice_account
+ (if :var_1: = A
then
{alice_account = :var_0:.alice_account - :var_0:.money;
bob_account = :var_0:.bob_account; money = :var_0:.money}
else
{alice_account = :var_0:.alice_account;
bob_account = :var_0:.bob_account + :var_0:.money;
money = :var_0:.money}).bob_account
• #### simplify

 into not (:var_0:.money >= 0) || :var_0:.alice_account + :var_0:.bob_account = (if :var_1: = A then {alice_account = :var_0:.alice_account + -1 * :var_0:.money; bob_account = :var_0:.bob_account; money = :var_0:.money} else {alice_account = :var_0:.alice_account; bob_account = :var_0:.bob_account + :var_0:.money; money = :var_0:.money}).alice_account + (if :var_1: = A then {alice_account = :var_0:.alice_account + -1 * :var_0:.money; bob_account = :var_0:.bob_account; money = :var_0:.money} else {alice_account = :var_0:.alice_account; bob_account = :var_0:.bob_account + :var_0:.money; money = :var_0:.money}).bob_account expansions [] rewrite_steps forward_chaining
• Sat (Some let (action : action) = B let (state : state) = {alice_account = 0; bob_account = 8855; money = 1} )

When we run this, TLC finds a counterexample: between steps A and B the invariant doesn’t hold.

Imandra has found this same counterexample.

How do we solve this? It depends on the level of abstraction we care about. If you were designing a database, you’d want to spec the exact steps required to keep the system consistent. At our level, though, we probably have access to database transactions and can ‘abstract out’ the atomicity checks. The way we do that is to combine A and B into a single “Transaction” step. That tells TLA+ that both actions happen simultaneously, and the system never passes through an invalid state.

There are many different ways we could choose to model this in Imandra. Here is one:

In :
type action =
| Transfer (* In this step we'll check whether Alice's balance is sufficient *)
| A (* In this step we'll transfer the funds *)
| End

type state =
{ alice_account : int
; bob_account : int
; money : int
; next_action : action (* The action that should be executed on the next call to step *)
}

let is_valid_initial_state state =
state.alice_account >= 0 &&
state.money >= 0 &&
state.next_action = Transfer

let step state =
match state.next_action with
| Transfer ->
if state.alice_account >= state.money then
{ state with next_action = A }
else
{ state with next_action = End }
| A ->
{ state with
alice_account = state.alice_account - state.money
; bob_account = state.bob_account + state.money
; next_action = End
}
| End ->
state

(* step_n repeatedly calls (step state) n times. *)
let rec step_n n state =
if n > 0 then
step_n (n-1) (step state)
else
state

let account_total state =
state.alice_account + state.bob_account

verify (fun n state ->
n < 5 &&
is_valid_initial_state state
==>
let state' = step_n n state in
account_total state = account_total state' &&
state'.alice_account >= 0
)

Out:
type action = Transfer | A | End
type state = {
alice_account : int;
bob_account : int;
money : int;
next_action : action;
}
val is_valid_initial_state : state -> bool = <fun>
val step : state -> state = <fun>
val step_n : int -> state -> state = <fun>
val account_total : state -> Z.t = <fun>
- : int -> state -> bool = <fun>

termination proof

### Termination proof

call step_n (n - 1) (step state) from step_n n state
originalstep_n n state
substep_n (n - 1) (step state)
original ordinalOrdinal.Int (if n >= 0 then n else 0)
sub ordinalOrdinal.Int (if (n - 1) >= 0 then n - 1 else 0)
path[n > 0]
proof
detailed proof
ground_instances1
definitions0
inductions0
search_time
0.019s
details
Expand
smt_stats
 num checks 3 arith assert lower 8 arith pivots 2 rlimit count 1035 mk clause 4 datatype occurs check 2 mk bool var 20 arith assert upper 3 decisions 2 arith add rows 3 propagations 2 conflicts 2 arith fixed eqs 2 datatype accessor ax 2 arith conflicts 1 num allocs 1.05918e+08 final checks 1 added eqs 6 del clause 4 arith eq adapter 2 memory 16.11 max memory 16.11
Expand
• start[0.019s]
n > 0
&& (if n >= 0 then n else 0) >= 0
&& (if (n - 1) >= 0 then n - 1 else 0) >= 0
==> not ((n - 1) > 0)
|| Ordinal.( << ) (Ordinal.Int (if (n - 1) >= 0 then n - 1 else 0))
(Ordinal.Int (if n >= 0 then n else 0))
• ##### simplify
 into (not ((not (n <= 0) && (if n >= 0 then n else 0) >= 0) && (if n >= 1 then -1 + n else 0) >= 0) || n <= 1) || Ordinal.( << ) (Ordinal.Int (if n >= 1 then -1 + n else 0)) (Ordinal.Int (if n >= 0 then n else 0)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (ite (>= n_1299 1) (+ (- 1) n_1299) 0)) (|Ordi… expansions
• ##### unsat
(let ((a!1 (not (= n_1299 (ite (>= n_1299 0) n_1299 0))))
(a!2 (+ n_1299 (* (- 1) (ite (>= n_1…

Proved
proof
ground_instances5
definitions0
inductions0
search_time
0.035s
details
Expand
smt_stats
 arith offset eqs 22 num checks 11 arith assert lower 128 arith pivots 86 rlimit count 13736 mk clause 193 datatype occurs check 62 mk bool var 504 arith assert upper 143 datatype splits 26 decisions 129 arith add rows 292 arith bound prop 13 propagations 388 interface eqs 7 conflicts 34 arith fixed eqs 98 datatype accessor ax 24 minimized lits 18 arith conflicts 3 arith assert diseq 38 datatype constructor ax 37 num allocs 1.33089e+08 final checks 12 added eqs 890 del clause 90 arith eq adapter 101 memory 17.15 max memory 17.15
Expand
• start[0.035s]
:var_0: < 5
&& :var_1:.alice_account >= 0
&& :var_1:.money >= 0 && :var_1:.next_action = Transfer
==> :var_1:.alice_account + :var_1:.bob_account =
(step_n :var_0: :var_1:).alice_account
+ (step_n :var_0: :var_1:).bob_account
&& (step_n :var_0: :var_1:).alice_account >= 0
• #### simplify

 into not (((not (5 <= :var_0:) && :var_1:.alice_account >= 0) && :var_1:.money >= 0) && :var_1:.next_action = Transfer) || :var_1:.alice_account + :var_1:.bob_account = (step_n :var_0: :var_1:).alice_account + (step_n :var_0: :var_1:).bob_account && (step_n :var_0: :var_1:).alice_account >= 0 expansions [] rewrite_steps forward_chaining
• unroll
 expr (step_n_64 n_69 state_70) expansions
• unroll
 expr (let ((a!1 (|rec_mk.state_1315| (+ (alice_account_56 state_70) (* (- 1) (money_58 state… expansions
• unroll
 expr (let ((a!1 (|rec_mk.state_1315| (+ (alice_account_56 state_70) (* (- 1) (money_58 state… expansions
• unroll
 expr (let ((a!1 (|rec_mk.state_1315| (+ (alice_account_56 state_70) (* (- 1) (money_58 state… expansions
• unroll
 expr (let ((a!1 (|rec_mk.state_1315| (+ (alice_account_56 state_70) (* (- 1) (money_58 state… expansions
• #### unsat

(let ((a!1 (>= (+ (alice_account_56 state_70) (* (- 1) (money_58 state_70))) 0))
(a!5 (= (mone…

## Multiprocess Algorithms¶

As a final part of our example, let’s discuss concurrency.

The accounts are global variables, while money is a local variable to the process.

In our model, we will treat state (which holds the accounts) as a global variable. The state of our processes will be represented by the process_state type - each has a local money variable. The world type will hold the global state of the accounts and the process_state for each process.

We'll then define a function run_world, which takes a world state and a scheduled execution order in the form of a list of process contexts, and executes the processes according to the schedule.

We want to verify that, given any initial world, the following invariants hold regardless of the order in which the processes are executed:

1. The total money in the system does not change.
2. Alice's account never goes negative.
In :
(** Global state of accounts *)
type state =
{ alice_account : int
; bob_account : int
}

(** Actions for an individual process *)
type process_action =
| Transfer
| A
| End

(** The state of a process *)
type process_state =
{ money : int
; next_action : process_action
}

(** State of the world *)
type world =
{ state : state
; p1_state : process_state
; p2_state : process_state
}

(** Step a process's next_action. Returns the updated global accounts
state and the new state of this process. *)
let step_process state process_state =
match process_state.next_action with
| Transfer ->
if state.alice_account >= process_state.money then
(state, { process_state with next_action = A })
else
(state, { process_state with next_action = End })
| A ->
( { alice_account = state.alice_account - process_state.money
; bob_account = state.bob_account + process_state.money
}
, { process_state with next_action = End }
)
| End ->
(state, process_state)

(** Current execution context *)
type context =
| Process_1
| Process_2

(** Step the world forward for a given execution context. *)
let step_world context world =
match context with
| Process_1 ->
let (state, p1_state) = step_process world.state world.p1_state in
{ world with state; p1_state }
| Process_2 ->
let (state, p2_state) = step_process world.state world.p2_state in
{ world with state; p2_state }

(** run_world takes an initial world state and executes the processes
according to the schedule specified by contexts *)
let run_world world contexts =
contexts |> List.fold_right step_world ~base:world

Out:
type state = { alice_account : int; bob_account : int; }
type process_action = Transfer | A | End
type process_state = { money : int; next_action : process_action; }
type world = {
state : state;
p1_state : process_state;
p2_state : process_state;
}
val step_process : state -> process_state -> state * process_state = <fun>
type context = Process_1 | Process_2
val step_world : context -> world -> world = <fun>
val run_world : world -> context list -> world = <fun>


Now we can verify that, for any initial state of the world and for any possible sequence of contexts, the invariants hold.

In :
(** A state is a valid initial state if the accounts are non-negative. *)
let is_valid_initial_state state =
state.alice_account >= 0 &&
state.bob_account >= 0

(** This function checks whether a process is in a valid starting state.
We'll use it to constrain the input to our verify statement below. *)
let is_valid_initial_process_state p =
p.money >= 0 &&
p.next_action = Transfer

(** The world is a valid initial state if the accounts and processes are all valid. *)
let is_valid_initial_world world =
is_valid_initial_state world.state &&
is_valid_initial_process_state world.p1_state &&
is_valid_initial_process_state world.p2_state

let account_total state =
state.alice_account + state.bob_account

verify (fun contexts world ->
(* Initial states are valid *)
is_valid_initial_world world
==>
let world' = run_world world contexts in
account_total world.state = account_total world'.state &&
world'.state.alice_account >= 0
)

Out:
val is_valid_initial_state : state -> bool = <fun>
val is_valid_initial_process_state : process_state -> bool = <fun>
val is_valid_initial_world : world -> bool = <fun>
val account_total : state -> Z.t = <fun>
- : context list -> world -> bool = <fun>
module CX : sig val contexts : context list val world : world end

Counterexample (after 5 steps, 0.238s):
let (contexts : context list) = [Process_1; Process_2; Process_1; Process_2]
let (world : world) =
{state = {alice_account = 18481; bob_account = 9270};
p1_state = {money = 11953; next_action = Transfer};
p2_state = {money = 14024; next_action = Transfer}}

Refuted
proof attempt
ground_instances5
definitions0
inductions0
search_time
0.238s
details
Expand
smt_stats
 arith offset eqs 830 num checks 11 arith assert lower 1092 arith pivots 436 rlimit count 196666 mk clause 1214 datatype occurs check 687 mk bool var 2528 arith assert upper 1036 datatype splits 524 decisions 1568 arith add rows 4942 arith bound prop 284 propagations 6657 interface eqs 23 conflicts 270 arith fixed eqs 970 datatype accessor ax 200 minimized lits 281 arith conflicts 38 arith assert diseq 282 datatype constructor ax 355 num allocs 2.11126e+08 final checks 41 added eqs 14500 del clause 486 arith eq adapter 671 memory 26.7 max memory 26.82
Expand
• start[0.238s]
(:var_0:.state.alice_account >= 0 && :var_0:.state.bob_account >= 0)
&& (:var_0:.p1_state.money >= 0 && :var_0:.p1_state.next_action = Transfer)
&& :var_0:.p2_state.money >= 0
&& :var_0:.p2_state.next_action = Transfer
==> :var_0:.state.alice_account + :var_0:.state.bob_account =
(List.fold_right step_world :var_0: :var_1:).state.alice_account
+ (List.fold_right step_world :var_0: :var_1:).state.bob_account
&& (List.fold_right step_world :var_0: :var_1:).state.alice_account >=
0
• #### simplify

 into not (((((:var_0:.state.alice_account >= 0 && :var_0:.state.bob_account >= 0) && :var_0:.p1_state.money >= 0) && :var_0:.p1_state.next_action = Transfer) && :var_0:.p2_state.money >= 0) && :var_0:.p2_state.next_action = Transfer) || :var_0:.state.alice_account + :var_0:.state.bob_account = (List.fold_right step_world :var_0: :var_1:).state.alice_account + (List.fold_right step_world :var_0: :var_1:).state.bob_account && (List.fold_right step_world :var_0: :var_1:).state.alice_account >= 0 expansions [] rewrite_steps forward_chaining
• unroll
 expr (|List.fold_right step_world_1655| world_112 contexts_111) expansions
• unroll
 expr (|List.fold_right step_world_1655| world_112 (|get.::.1_1651| contexts_111)) expansions
• unroll
 expr (|List.fold_right step_world_1655| world_112 (|get.::.1_1651| (|get.::.1_1651| contexts_111… expansions
• unroll
 expr (|List.fold_right step_world_1655| world_112 (|get.::.1_1651| (|get.::.1_1651| (|get.::.1_1… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1651| (|get.::.1_1651| (|get.::.1_1651| (|get.::.1_1651| contexts_111)))))) … expansions
• Sat (Some let (contexts : context list) = [Process_1; Process_2; Process_1; Process_2] let (world : world) = {state = {alice_account = 18481; bob_account = 9270}; p1_state = {money = 11953; next_action = Transfer}; p2_state = {money = 14024; next_action = Transfer}} )

There’s a gap between when we check that Alice has enough money and when we actually transfer the money. With one process this wasn’t a problem, but with two, it means her account can go negative. TLC is nice enough to provide the initial state and steps required to reproduce the bug.

Imandra has also found a counterexample. We can see from the contexts in the counterexample that one process interrupted the other.

We can also execute the counterexample to see the final state of the world in this case:

In :
run_world CX.world CX.contexts

Out:
- : world =
{state = {alice_account = -7496; bob_account = 35247};
p1_state = {money = 11953; next_action = End};
p2_state = {money = 14024; next_action = End}}


## Summary¶

We've shown how these TLA+ problems can be modeled in Imandra, in an apples-to-apples fashion.

In most cases we've translated the PlusCal examples into a state machine, which is closer to the underlying TLA+ representation. A PlusCal-like DSL for Imandra would be an interesting future project.

Both systems can go much deeper: TLA+ has theorem proving capabilities, and we haven't touched on Imandra's lemmas, theorems, rewrite rules or the induction waterfall. Browse the documentation to find out more!