It’s relatively straight forward to specify a (simple) state machine using TLA+ (this video is a good intro). We can revisit a previous example…
There are two required functions (operators): Init which provides the initial variables:
VARIABLES state, balance
Init ==
/\ state = "open"
/\ balance = 0
The starting position (of the state machine) is the string “open”, and the balance is 0.
And the Next function defines the possible transitions:
Next ==
\/ \E amount \in 1..10:
Deposit(amount)
\/ \E amount \in 1..10:
Withdraw(amount)
\/ Close
\/ Reopen
With an imperative mindset, you can think of this as “choosing” at random one of four options every time round the loop (in reality, the model checker will exhaustively explore every possible path).
So some possible executions are:
Init
Next
Deposit(5)
Next
Withdraw(1)
Next
Deposit(3)
Next
Close
Next
Reopen
Next
...ad infinitum
The Deposit transition:
Deposit(amount) ==
/\ state = "open"
/\ balance < 100
/\ balance' = balance + amount
/\ UNCHANGED <<state>>
Has two pre-conditions: that the state machine is currently in the “open” state (see diagram in the post linked above), and that the balance is less than 100 (this is purely to ensure that the model checker does not run forever).
If those are satisfied, the remainder can run, and set the post balance to be the current balance plus the deposited amount.
The Withdraw is a mirror image;
Withdraw(amount) ==
/\ state = "open"
/\ (balance - amount) >= 0
/\ balance' = balance - amount
/\ UNCHANGED <<state>>
But this time, the guard clause is that the balance is sufficient to allow the withdrawal, and the amount is then subtracted.
And finally, Close and Reopen merely update the state:
Close ==
/\ state = "open"
/\ state' = "closed"
/\ UNCHANGED <<balance>>
Reopen ==
/\ state = "closed"
/\ state' = "open"
/\ UNCHANGED <<balance>>
And guarantee that a closed account can only be re-opened, and vice versa.
We also include an invariant:
NoNegativeBalance ==
balance >= 0
That the balance cannot drop below 0 (no overdraft facility here!)
We can then run the model, using the downloaded jar file, and a config file:
$ docker run --rm -it -v $PWD:/app -w /app openjdk:14-jdk-alpine java -XX:+UseParallelGC -cp tla2tools.jar tlc2.TLC -config bank.cfg -workers auto -cleanup bank.tla
TLC2 Version 2.18 of Day Month 20?? (rev: cab6f13)
Running breadth-first search Model-Checking with fp 17 and seed -6395706311673644266 with 8 workers on 8 cores with 3488MB heap and 64MB offheap memory [pid: 1] (Linux 6.2.1-arch1-1 amd64, Oracle Corporation 14-ea x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /app/bank.tla
Parsing file /tmp/tlc-5979345560125251717/Integers.tla (jar:file:/app/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /tmp/tlc-5979345560125251717/_TLCTrace.tla (jar:file:/app/tla2tools.jar!/tla2sany/StandardModules/_TLCTrace.tla)
Parsing file /tmp/tlc-5979345560125251717/Naturals.tla (jar:file:/app/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-5979345560125251717/TLC.tla (jar:file:/app/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/tlc-5979345560125251717/TLCExt.tla (jar:file:/app/tla2tools.jar!/tla2sany/StandardModules/TLCExt.tla)
Parsing file /tmp/tlc-5979345560125251717/Sequences.tla (jar:file:/app/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-5979345560125251717/FiniteSets.tla (jar:file:/app/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module TLCExt
Semantic processing of module _TLCTrace
Semantic processing of module bank
Starting... (2023-03-06 14:01:19)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2023-03-06 14:01:19.
Model checking completed. No error has been found.
Estimates of the probability that TLC did not check all reachable states
because two distinct states had the same fingerprint:
calculated (optimistic): val = 2.4E-14
2266 states generated, 220 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 15.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 8 and the 95th percentile is 3).
Finished in 00s at (2023-03-06 14:01:19)
And we see that the invariant was not breached, after 220 distinct states.
Obviously, this isn’t a very useful example, but next time we will add some concurrency!
Look on my works, ye Mighty, and despair! 