Skip to content

Instantly share code, notes, and snippets.

@mdmarek

mdmarek/DieHard.cfg

Created November 3, 2016 16:14
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save mdmarek/8bd347587821d735c2e42ca1e769b304 to your computer and use it in GitHub Desktop.
Save mdmarek/8bd347587821d735c2e42ca1e769b304 to your computer and use it in GitHub Desktop.
Download ZIP
TLA+ DieHard
Raw
DieHard.cfg
INIT
Init
NEXT
Next
INVARIANT
TypeOK
Raw
DieHard.tla
---- MODULE DieHard ----
EXTENDS Integers, TLC
VARIABLES big, small
TypeOK == /\ big \in 0..5
/\ small \in 0..3
BigNot4 == big /= 4
FillSmall == /\ small' = 3
/\ big' = big
FillBig == /\ big' = 5
/\ small' = small
EmptySmall == /\ small' = 0
/\ big' = big
EmptyBig == /\ big' = 0
/\ small' = small
Min(m,n) == IF m > n THEN n ELSE m
SmallToBig ==
LET poured == Min(big + small, 5) - big
IN /\ big' = big + poured
/\ small' = small - poured
BigToSmall ==
LET poured == Min(big + small, 3) - small
IN /\ small' = small + poured
/\ big' = big - poured
Init == /\ big = 0
/\ small = 0
Next == \/ FillSmall
\/ FillBig
\/ EmptySmall
\/ EmptyBig
\/ SmallToBig
\/ BigToSmall
====
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment