TLA+ PlusCal `transfer` module

transfer.tla

---- MODULE transfer ----
EXTENDS Naturals, TLC

(* --algorithm transfer
variables alice_account = 10, bob_account = 10,
          account_total = alice_account + bob_account;

process Transfer \in 1..2
  variable money \in 1..20;

begin
A:
    if alice_account >= money then
        alice_account := alice_account - money;
        bob_account := bob_account + money;
    end if;
B: assert alice_account >= 0;

end process

end algorithm *)

MoneyNotNegative == money >= 0
MoneyInvariant == alice_account + bob_account = account_total

====

Final transfer algorithm to the https://learntla.com/introduction/example/

# File -> TranslateCal Algorithm(Ctrl + T)

# What is the behavior spec?
# Temporal formula (Spec)

# What to check?
# Deadlock (checked)

# Invariants
# MoneyNotNegative (unchecked)
# MoneyInvariant (checked)