danesabo/Class_Work
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

TLAgit add .

Browse Source
This commit is contained in:
Dane Sabo 2025-02-28 17:41:22 -05:00
parent 2980d41cb4
commit 61c0615e05
2 changed files with 50 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
TLA+/DieHard.cfg Normal file
View File

@ -0,0 +1,3 @@
INIT Init
NEXT Next
INVARIANT TypeOk Impossible

47
TLA+/DieHard.tla Normal file
View File

@ -0,0 +1,47 @@
----------------------------- MODULE DieHard -----------------------------
EXTENDS Naturals
VARIABLES small, big
Init == /\ small = 0
/\ big = 0
TypeOk == /\ big \in 0..5
/\ small \in 0..3
FillBig == /\ big' = 5
/\ small' = small
FillSmall == /\ small' = 3
/\ big' = big
EmptyBig == /\ big' = 0
/\ small' = small
EmptySmall == /\ small' = 0
/\ big' = big
Small2Big == IF big + small > 5
THEN /\ big' = 5
/\ small' = (big + small) - 5
ELSE /\ big' = big + small
/\ small' = 0
Big2Small == IF big + small > 3
THEN /\ small' = 3
/\ big' = (big + small) - 3
ELSE /\ small' = big + small
/\ big' = 0
Next == \/ Big2Small
\/ Small2Big
\/ EmptyBig
\/ EmptySmall
\/ FillBig
\/ FillSmall
Impossible == big # 4
=============================================================================
\* Modification History
\* Last modified Fri Feb 28 17:31:43 EST 2025 by danesabo
\* Created Fri Feb 28 17:23:34 EST 2025 by danesabo