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 [1]:
type state =
  { alice_account : int
  ; bob_account : int
  ; money : int
  }

let init =
  { alice_account = 10
  ; bob_account = 10
  ; money = 5
  }
Out[1]:
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 [2]:
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[2]:
type action = A | B
val step : action -> state -> state = <fun>

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

In [3]:
let transfer state =
  state |> step A |> step B
Out[3]:
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 [4]:
init;;
init |> step A;;
init |> step A |> step B;;
Out[4]:
- : 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 [5]:
verify (fun state ->
  state.alice_account = 10 &&
  state.bob_account = 10 &&
  state.money = 5
  ==>
  let state' = transfer state in
  state'.alice_account >= 0
)
Out[5]:
- : state -> bool = <fun>
Proved
proof
ground_instances0
definitions0
inductions0
search_time
0.029s
details
Expand
smt_stats
num checks1
rlimit count249
mk bool var6
num allocs2575086
memory6.400000
max memory6.800000
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 [6]:
      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[6]:
      - : 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 checks65
      arith assert lower26
      rlimit count12614
      mk clause82
      datatype occurs check127
      mk bool var323
      arith assert upper8
      datatype splits20
      decisions115
      propagations89
      conflicts77
      datatype accessor ax22
      arith assert diseq22
      datatype constructor ax66
      num allocs7044821
      final checks53
      added eqs263
      del clause71
      arith eq adapter27
      memory7.430000
      max memory7.430000
      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 [7]:
                                                                          CX.state;;
                                                                          CX.state |> step A;;
                                                                          CX.state |> step A |> step B;;
                                                                          
                                                                          Out[7]:
                                                                          - : 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 [8]:
                                                                          let transfer state =
                                                                            if state.alice_account >= state.money then
                                                                              state |> step A |> step B
                                                                            else
                                                                              state
                                                                          
                                                                          Out[8]:
                                                                          val transfer : state -> state = <fun>
                                                                          

                                                                          Which now runs properly.

                                                                          In [9]:
                                                                          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[9]:
                                                                          - : state -> bool = <fun>
                                                                          
                                                                          Proved
                                                                          proof
                                                                          ground_instances0
                                                                          definitions0
                                                                          inductions0
                                                                          search_time
                                                                          0.011s
                                                                          details
                                                                          Expand
                                                                          smt_stats
                                                                          num checks2
                                                                          arith assert lower1
                                                                          arith pivots2
                                                                          rlimit count646
                                                                          mk clause3
                                                                          mk bool var30
                                                                          arith assert upper5
                                                                          decisions2
                                                                          arith add rows5
                                                                          propagations5
                                                                          conflicts4
                                                                          datatype accessor ax3
                                                                          arith conflicts1
                                                                          arith assert diseq1
                                                                          datatype constructor ax2
                                                                          num allocs12042919
                                                                          added eqs24
                                                                          del clause1
                                                                          arith eq adapter3
                                                                          memory10.830000
                                                                          max memory10.830000
                                                                          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 [10]:
                                                                              verify (fun state ->
                                                                                state.alice_account = 10 &&
                                                                                state.bob_account = 10 &&
                                                                                state.money >= 0
                                                                                ==>
                                                                                let state' = transfer state in
                                                                                state'.alice_account >= 0
                                                                              )
                                                                              
                                                                              Out[10]:
                                                                              - : state -> bool = <fun>
                                                                              
                                                                              Proved
                                                                              proof
                                                                              ground_instances0
                                                                              definitions0
                                                                              inductions0
                                                                              search_time
                                                                              0.058s
                                                                              details
                                                                              Expand
                                                                              smt_stats
                                                                              num checks1
                                                                              arith assert lower2
                                                                              arith pivots2
                                                                              rlimit count589
                                                                              mk clause3
                                                                              mk bool var30
                                                                              arith assert upper3
                                                                              decisions1
                                                                              arith add rows5
                                                                              propagations3
                                                                              conflicts2
                                                                              datatype accessor ax3
                                                                              arith conflicts1
                                                                              datatype constructor ax2
                                                                              num allocs25883206
                                                                              added eqs22
                                                                              del clause1
                                                                              arith eq adapter2
                                                                              memory14.040000
                                                                              max memory14.510000
                                                                              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 [11]:
                                                                                  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[11]:
                                                                                  - : action -> state -> bool = <fun>
                                                                                  
                                                                                  Proved
                                                                                  proof
                                                                                  ground_instances0
                                                                                  definitions0
                                                                                  inductions0
                                                                                  search_time
                                                                                  0.021s
                                                                                  details
                                                                                  Expand
                                                                                  smt_stats
                                                                                  num checks1
                                                                                  arith assert lower4
                                                                                  rlimit count503
                                                                                  mk clause3
                                                                                  mk bool var36
                                                                                  arith assert upper2
                                                                                  datatype splits1
                                                                                  decisions3
                                                                                  propagations8
                                                                                  conflicts4
                                                                                  datatype accessor ax5
                                                                                  arith conflicts1
                                                                                  arith assert diseq1
                                                                                  datatype constructor ax2
                                                                                  num allocs50219166
                                                                                  added eqs35
                                                                                  del clause1
                                                                                  arith eq adapter3
                                                                                  memory14.510000
                                                                                  max memory14.910000
                                                                                  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 [12]:
                                                                                      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[12]:
                                                                                      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 checks1
                                                                                      arith assert lower3
                                                                                      arith pivots3
                                                                                      rlimit count618
                                                                                      mk clause8
                                                                                      datatype occurs check5
                                                                                      mk bool var35
                                                                                      arith assert upper4
                                                                                      datatype splits1
                                                                                      decisions3
                                                                                      arith add rows6
                                                                                      propagations3
                                                                                      arith fixed eqs2
                                                                                      datatype accessor ax6
                                                                                      arith assert diseq1
                                                                                      datatype constructor ax3
                                                                                      num allocs82023314
                                                                                      final checks1
                                                                                      added eqs24
                                                                                      del clause2
                                                                                      arith eq adapter3
                                                                                      memory15.060000
                                                                                      max memory15.550000
                                                                                      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 [13]:
                                                                                          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[13]:
                                                                                          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 checks3
                                                                                          arith assert lower8
                                                                                          arith pivots2
                                                                                          rlimit count1035
                                                                                          mk clause4
                                                                                          datatype occurs check2
                                                                                          mk bool var20
                                                                                          arith assert upper3
                                                                                          decisions2
                                                                                          arith add rows3
                                                                                          propagations2
                                                                                          conflicts2
                                                                                          arith fixed eqs2
                                                                                          datatype accessor ax2
                                                                                          arith conflicts1
                                                                                          num allocs105917500
                                                                                          final checks1
                                                                                          added eqs6
                                                                                          del clause4
                                                                                          arith eq adapter2
                                                                                          memory16.110000
                                                                                          max memory16.110000
                                                                                          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 eqs22
                                                                                                num checks11
                                                                                                arith assert lower128
                                                                                                arith pivots86
                                                                                                rlimit count13736
                                                                                                mk clause193
                                                                                                datatype occurs check62
                                                                                                mk bool var504
                                                                                                arith assert upper143
                                                                                                datatype splits26
                                                                                                decisions129
                                                                                                arith add rows292
                                                                                                arith bound prop13
                                                                                                propagations388
                                                                                                interface eqs7
                                                                                                conflicts34
                                                                                                arith fixed eqs98
                                                                                                datatype accessor ax24
                                                                                                minimized lits18
                                                                                                arith conflicts3
                                                                                                arith assert diseq38
                                                                                                datatype constructor ax37
                                                                                                num allocs133088586
                                                                                                final checks12
                                                                                                added eqs890
                                                                                                del clause90
                                                                                                arith eq adapter101
                                                                                                memory17.150000
                                                                                                max memory17.150000
                                                                                                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 [14]:
                                                                                                              (** 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[14]:
                                                                                                              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 [15]:
                                                                                                              (** 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[15]:
                                                                                                              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 eqs830
                                                                                                              num checks11
                                                                                                              arith assert lower1092
                                                                                                              arith pivots436
                                                                                                              rlimit count196666
                                                                                                              mk clause1214
                                                                                                              datatype occurs check687
                                                                                                              mk bool var2528
                                                                                                              arith assert upper1036
                                                                                                              datatype splits524
                                                                                                              decisions1568
                                                                                                              arith add rows4942
                                                                                                              arith bound prop284
                                                                                                              propagations6657
                                                                                                              interface eqs23
                                                                                                              conflicts270
                                                                                                              arith fixed eqs970
                                                                                                              datatype accessor ax200
                                                                                                              minimized lits281
                                                                                                              arith conflicts38
                                                                                                              arith assert diseq282
                                                                                                              datatype constructor ax355
                                                                                                              num allocs211126067
                                                                                                              final checks41
                                                                                                              added eqs14500
                                                                                                              del clause486
                                                                                                              arith eq adapter671
                                                                                                              memory26.700000
                                                                                                              max memory26.820000
                                                                                                              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[0]`_1655| world_112 contexts_111)
                                                                                                                    expansions
                                                                                                                    • unroll
                                                                                                                      expr
                                                                                                                      (|`List.fold_right step_world[0]`_1655|
                                                                                                                        world_112
                                                                                                                        (|get.::.1_1651| contexts_111))
                                                                                                                      expansions
                                                                                                                      • unroll
                                                                                                                        expr
                                                                                                                        (|`List.fold_right step_world[0]`_1655|
                                                                                                                          world_112
                                                                                                                          (|get.::.1_1651| (|get.::.1_1651| contexts_111…
                                                                                                                        expansions
                                                                                                                        • unroll
                                                                                                                          expr
                                                                                                                          (|`List.fold_right step_world[0]`_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 [16]:
                                                                                                                            run_world CX.world CX.contexts
                                                                                                                            
                                                                                                                            Out[16]:
                                                                                                                            - : 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!