From 61c0615e0525f33ad1808702a9d16e77b7c3ad3b Mon Sep 17 00:00:00 2001 From: Dane Sabo Date: Fri, 28 Feb 2025 17:41:22 -0500 Subject: [PATCH] TLAgit add . --- TLA+/DieHard.cfg | 3 +++ TLA+/DieHard.tla | 47 +++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 50 insertions(+) create mode 100644 TLA+/DieHard.cfg create mode 100644 TLA+/DieHard.tla diff --git a/TLA+/DieHard.cfg b/TLA+/DieHard.cfg new file mode 100644 index 0000000..5364dc3 --- /dev/null +++ b/TLA+/DieHard.cfg @@ -0,0 +1,3 @@ +INIT Init +NEXT Next +INVARIANT TypeOk Impossible diff --git a/TLA+/DieHard.tla b/TLA+/DieHard.tla new file mode 100644 index 0000000..c1e2867 --- /dev/null +++ b/TLA+/DieHard.tla @@ -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