From 818c6456cff9a612399f27e432056c21cefa40ec Mon Sep 17 00:00:00 2001 From: hillium Date: Sat, 12 Oct 2024 14:45:18 +0800 Subject: [PATCH 1/5] added WriteAndVerify committing --- PutAndVerify/MC.cfg | 17 +++++++++ PutAndVerify/MC.tla | 21 +++++++++++ PutAndVerify/README.md | 4 ++ PutAndVerify/WriteAndVerify.tla | 65 +++++++++++++++++++++++++++++++++ 4 files changed, 107 insertions(+) create mode 100755 PutAndVerify/MC.cfg create mode 100755 PutAndVerify/MC.tla create mode 100644 PutAndVerify/README.md create mode 100755 PutAndVerify/WriteAndVerify.tla diff --git a/PutAndVerify/MC.cfg b/PutAndVerify/MC.cfg new file mode 100755 index 0000000..f031352 --- /dev/null +++ b/PutAndVerify/MC.cfg @@ -0,0 +1,17 @@ +\* MV CONSTANT declarations +CONSTANTS +Alice = Alice +Bob = Bob +\* MV CONSTANT definitions +CONSTANT +CLIENTS <- const_171964209906974000 +\* SYMMETRY definition +SYMMETRY symm_171964209906975000 +\* SPECIFICATION definition +SPECIFICATION +WVSpec +\* INVARIANT definition +INVARIANT +WVConsistency +WVTypeOk +\* Generated on Sat Jun 29 14:21:39 CST 2024 \ No newline at end of file diff --git a/PutAndVerify/MC.tla b/PutAndVerify/MC.tla new file mode 100755 index 0000000..ccd5c00 --- /dev/null +++ b/PutAndVerify/MC.tla @@ -0,0 +1,21 @@ +---- MODULE MC ---- +EXTENDS WriteAndVerify, TLC + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +Alice, Bob +---- + +\* MV CONSTANT definitions CLIENTS +const_171964209906974000 == +{Alice, Bob} +---- + +\* SYMMETRY definition +symm_171964209906975000 == +Permutations(const_171964209906974000) +---- + +============================================================================= +\* Modification History +\* Created Sat Jun 29 14:21:39 CST 2024 by Hillium diff --git a/PutAndVerify/README.md b/PutAndVerify/README.md new file mode 100644 index 0000000..b7d7c53 --- /dev/null +++ b/PutAndVerify/README.md @@ -0,0 +1,4 @@ +# Put and Verify Committing + +This algorithm allows you write to a file exactly-once in a object storage +supports `PUT` and `LIST` and the two operations have strong consistency. diff --git a/PutAndVerify/WriteAndVerify.tla b/PutAndVerify/WriteAndVerify.tla new file mode 100755 index 0000000..a3f932f --- /dev/null +++ b/PutAndVerify/WriteAndVerify.tla @@ -0,0 +1,65 @@ +--------------------------- MODULE WriteAndVerify --------------------------- + +CONSTANT CLIENTS + +VARIABLE storage, clState + +WVTypeOk == /\ storage \in [ CLIENTS -> { "none", "empty", "written" } ] + /\ clState \in [ CLIENTS -> { "begin", "precheck-done", "blank-written", + "write-check-done", "committed", "aborted" } ] + +WVInit == /\ storage = [ cli \in CLIENTS |-> "none" ] + /\ clState = [ cli \in CLIENTS |-> "begin" ] + +(* Only one execution can be committed. *) +(* Once committed, the file has been written. *) +WVConsistency == /\ \A i, j \in CLIENTS : + (* If i != j, clState[i] and clState[j] cannot be both committed. *) + i /= j /\ clState[i] = "committed" => ~clState[j] = "committed" + /\ \A i, j \in CLIENTS : + i /= j /\ storage[i] = "written" => ~storage[j] = "written" + /\ \A i \in CLIENTS : clState[i] = "committed" <=> storage[i] = "written" + +(* "Verify" condition: storage only contains our file or nothing. *) +Check(c) == /\ \A f \in CLIENTS : f = c \/ storage[f] = "none" + +Precheck(c) == /\ clState[c] = "begin" + /\ IF Check(c) + THEN clState' = [ clState EXCEPT ![c] = "precheck-done" ] + ELSE clState' = [ clState EXCEPT ![c] = "aborted" ] + /\ UNCHANGED << storage >> + +WriteBlank(c) == /\ clState[c] = "precheck-done" + /\ storage' = [ storage EXCEPT ![c] = "empty" ] + /\ clState' = [ clState EXCEPT ![c] = "blank-written" ] + +ConflictCheck(c) == /\ clState[c] = "blank-written" + /\ IF Check(c) + THEN clState' = [ clState EXCEPT ![c] = "write-check-done" ] + ELSE clState' = [ clState EXCEPT ![c] = "aborted" ] + /\ UNCHANGED << storage >> + +(* Delete the file when aborted. *) +RollBack(c) == /\ clState[c] = "aborted" + /\ storage[c] /= "none" + /\ storage' = [ storage EXCEPT ![c] = "none" ] + /\ clState' = [ clState EXCEPT ![c] = "begin" ] + +Commit(c) == /\ clState[c] = "write-check-done" + /\ clState' = [ clState EXCEPT ![c] = "committed" ] + /\ storage' = [ storage EXCEPT ![c] = "written" ] + +WVNext == \E c \in CLIENTS: \/ Precheck(c) + \/ WriteBlank(c) + \/ ConflictCheck(c) + \/ RollBack(c) + \/ Commit(c) + +WVSpec == WVInit /\ [][WVNext]_<< storage, clState >> + +THEOREM WVSpec => [](WVConsistency /\ WVTypeOk) + +============================================================================= +\* Modification History +\* Last modified Sat Jun 29 14:21:06 CST 2024 by Hillium +\* Created Sat Jun 29 10:41:34 CST 2024 by Hillium From 8c78df03f7e9156074f89782f2050ead57192448 Mon Sep 17 00:00:00 2001 From: hillium Date: Mon, 14 Oct 2024 16:48:47 +0800 Subject: [PATCH 2/5] added crash and RWLock. --- PutAndVerify/MC.cfg | 12 +++++-- PutAndVerify/MC.tla | 18 +++++++--- PutAndVerify/README.md | 6 ++++ PutAndVerify/WriteAndVerify.tla | 64 +++++++++++++++++++++++---------- 4 files changed, 75 insertions(+), 25 deletions(-) diff --git a/PutAndVerify/MC.cfg b/PutAndVerify/MC.cfg index f031352..b741d5f 100755 --- a/PutAndVerify/MC.cfg +++ b/PutAndVerify/MC.cfg @@ -4,9 +4,15 @@ Alice = Alice Bob = Bob \* MV CONSTANT definitions CONSTANT -CLIENTS <- const_171964209906974000 +CLIENTS <- const_172889209848054000 \* SYMMETRY definition -SYMMETRY symm_171964209906975000 +SYMMETRY symm_172889209848055000 +\* CONSTANT definitions +CONSTANT +WITH_CRASHING <- const_172889209848056000 +\* CONSTANT definitions +CONSTANT +WITH_RO <- const_172889209848057000 \* SPECIFICATION definition SPECIFICATION WVSpec @@ -14,4 +20,4 @@ WVSpec INVARIANT WVConsistency WVTypeOk -\* Generated on Sat Jun 29 14:21:39 CST 2024 \ No newline at end of file +\* Generated on Mon Oct 14 15:48:18 CST 2024 \ No newline at end of file diff --git a/PutAndVerify/MC.tla b/PutAndVerify/MC.tla index ccd5c00..0a46963 100755 --- a/PutAndVerify/MC.tla +++ b/PutAndVerify/MC.tla @@ -7,15 +7,25 @@ Alice, Bob ---- \* MV CONSTANT definitions CLIENTS -const_171964209906974000 == +const_172889209848054000 == {Alice, Bob} ---- \* SYMMETRY definition -symm_171964209906975000 == -Permutations(const_171964209906974000) +symm_172889209848055000 == +Permutations(const_172889209848054000) +---- + +\* CONSTANT definitions @modelParameterConstants:1WITH_CRASHING +const_172889209848056000 == +FALSE +---- + +\* CONSTANT definitions @modelParameterConstants:2WITH_RO +const_172889209848057000 == +FALSE ---- ============================================================================= \* Modification History -\* Created Sat Jun 29 14:21:39 CST 2024 by Hillium +\* Created Mon Oct 14 15:48:18 CST 2024 by Hillium diff --git a/PutAndVerify/README.md b/PutAndVerify/README.md index b7d7c53..0c27de1 100644 --- a/PutAndVerify/README.md +++ b/PutAndVerify/README.md @@ -2,3 +2,9 @@ This algorithm allows you write to a file exactly-once in a object storage supports `PUT` and `LIST` and the two operations have strong consistency. + +The model parameters: + +- `CLIENTS`: The particants of the algorithm. +- `WITH_CRASHING`: Allow any of particants crash after sending a write message before receiving a response. +- `WITH_RO`: Allow "read-only" clients to particate. The algorithm then becomes a `RWLock` implementation: *many of "read-only" clients commit* or *exactly one of "read-write" client commits*. \ No newline at end of file diff --git a/PutAndVerify/WriteAndVerify.tla b/PutAndVerify/WriteAndVerify.tla index a3f932f..661986c 100755 --- a/PutAndVerify/WriteAndVerify.tla +++ b/PutAndVerify/WriteAndVerify.tla @@ -1,65 +1,93 @@ --------------------------- MODULE WriteAndVerify --------------------------- -CONSTANT CLIENTS +CONSTANT CLIENTS, WITH_RO, WITH_CRASHING -VARIABLE storage, clState +VARIABLE storage, clState, clFavor -WVTypeOk == /\ storage \in [ CLIENTS -> { "none", "empty", "written" } ] +Vars == << storage, clState, clFavor >> + +WVTypeOk == /\ storage \in [ CLIENTS -> { "none", "empty", "written", "written-ro", "empty-ro" } ] /\ clState \in [ CLIENTS -> { "begin", "precheck-done", "blank-written", - "write-check-done", "committed", "aborted" } ] + "write-check-done", "committed", "aborted", "crashed" } ] + /\ clFavor \in [ CLIENTS -> { "read-write", "read-only" } ] WVInit == /\ storage = [ cli \in CLIENTS |-> "none" ] /\ clState = [ cli \in CLIENTS |-> "begin" ] + /\ clFavor = [ cli \in CLIENTS |-> "read-write" ] (* Only one execution can be committed. *) (* Once committed, the file has been written. *) WVConsistency == /\ \A i, j \in CLIENTS : - (* If i != j, clState[i] and clState[j] cannot be both committed. *) - i /= j /\ clState[i] = "committed" => ~clState[j] = "committed" - /\ \A i, j \in CLIENTS : - i /= j /\ storage[i] = "written" => ~storage[j] = "written" - /\ \A i \in CLIENTS : clState[i] = "committed" <=> storage[i] = "written" + i /= j /\ storage[i] = "written" => ~storage[j] \in { "written", "written-ro" } (* "Verify" condition: storage only contains our file or nothing. *) -Check(c) == /\ \A f \in CLIENTS : f = c \/ storage[f] = "none" +Check(c) == /\ clFavor[c] = "read-write" => + \A f \in CLIENTS : f /= c => storage[f] = "none" + /\ clFavor[c] = "read-only" => + (* No conflicting write. *) + \A f \in CLIENTS : f /= c => ~storage[f] \in { "empty", "written" } Precheck(c) == /\ clState[c] = "begin" /\ IF Check(c) THEN clState' = [ clState EXCEPT ![c] = "precheck-done" ] ELSE clState' = [ clState EXCEPT ![c] = "aborted" ] - /\ UNCHANGED << storage >> + /\ UNCHANGED << storage, clFavor >> + +IsRO(c) == clFavor[c] = "read-only" -WriteBlank(c) == /\ clState[c] = "precheck-done" - /\ storage' = [ storage EXCEPT ![c] = "empty" ] +DoWriteBlank(c) == /\ clState[c] = "precheck-done" + /\ storage' = [ storage EXCEPT ![c] = IF IsRO(c) THEN "empty-ro" ELSE "empty" ] + +WriteBlank(c) == /\ DoWriteBlank(c) /\ clState' = [ clState EXCEPT ![c] = "blank-written" ] + /\ UNCHANGED << clFavor >> + ConflictCheck(c) == /\ clState[c] = "blank-written" /\ IF Check(c) THEN clState' = [ clState EXCEPT ![c] = "write-check-done" ] ELSE clState' = [ clState EXCEPT ![c] = "aborted" ] - /\ UNCHANGED << storage >> + /\ UNCHANGED << storage, clFavor >> (* Delete the file when aborted. *) RollBack(c) == /\ clState[c] = "aborted" /\ storage[c] /= "none" /\ storage' = [ storage EXCEPT ![c] = "none" ] /\ clState' = [ clState EXCEPT ![c] = "begin" ] + /\ UNCHANGED << clFavor >> -Commit(c) == /\ clState[c] = "write-check-done" +DoCommit(c) == /\ clState[c] = "write-check-done" + /\ storage' = [ storage EXCEPT ![c] = IF IsRO(c) THEN "written-ro" ELSE "written" ] + +Commit(c) == /\ DoCommit(c) /\ clState' = [ clState EXCEPT ![c] = "committed" ] - /\ storage' = [ storage EXCEPT ![c] = "written" ] + /\ UNCHANGED << clFavor >> +BeRO(c) == /\ clState[c] = "begin" + /\ clFavor[c] = "read-write" + /\ clFavor' = [ clFavor EXCEPT ![c] = "read-only" ] + /\ UNCHANGED << clState, storage >> + +WrittenAndCrash(c) == /\ clState[c] = "precheck-done" \/ clState[c] = "write-check-done" + /\ clState' = [ clState EXCEPT ![c] = "crashed" ] + /\ DoWriteBlank(c) \/ DoCommit(c) + /\ UNCHANGED << clFavor >> + + WVNext == \E c \in CLIENTS: \/ Precheck(c) \/ WriteBlank(c) \/ ConflictCheck(c) \/ RollBack(c) \/ Commit(c) + \/ WITH_CRASHING /\ WrittenAndCrash(c) + \/ WITH_RO /\ BeRO(c) + -WVSpec == WVInit /\ [][WVNext]_<< storage, clState >> +WVSpec == WVInit /\ [][WVNext]_Vars THEOREM WVSpec => [](WVConsistency /\ WVTypeOk) ============================================================================= \* Modification History -\* Last modified Sat Jun 29 14:21:06 CST 2024 by Hillium +\* Last modified Mon Oct 14 15:38:01 CST 2024 by Hillium \* Created Sat Jun 29 10:41:34 CST 2024 by Hillium From c634bbc018ea4182a87eb0b12c7c409e82d5f743 Mon Sep 17 00:00:00 2001 From: hillium Date: Mon, 14 Oct 2024 16:58:00 +0800 Subject: [PATCH 3/5] fix typo --- PutAndVerify/README.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/PutAndVerify/README.md b/PutAndVerify/README.md index 0c27de1..a12262e 100644 --- a/PutAndVerify/README.md +++ b/PutAndVerify/README.md @@ -3,8 +3,8 @@ This algorithm allows you write to a file exactly-once in a object storage supports `PUT` and `LIST` and the two operations have strong consistency. -The model parameters: +The model constants: -- `CLIENTS`: The particants of the algorithm. -- `WITH_CRASHING`: Allow any of particants crash after sending a write message before receiving a response. +- `CLIENTS`: The participants of the algorithm. +- `WITH_CRASHING`: Allow any of participants crash after sending a write message before receiving a response. - `WITH_RO`: Allow "read-only" clients to particate. The algorithm then becomes a `RWLock` implementation: *many of "read-only" clients commit* or *exactly one of "read-write" client commits*. \ No newline at end of file From d32dd40895de041df217cbbcce084265591fe857 Mon Sep 17 00:00:00 2001 From: hillium Date: Mon, 14 Oct 2024 23:11:55 +0800 Subject: [PATCH 4/5] fix typo --- PutAndVerify/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/PutAndVerify/README.md b/PutAndVerify/README.md index a12262e..2db2ef3 100644 --- a/PutAndVerify/README.md +++ b/PutAndVerify/README.md @@ -7,4 +7,4 @@ The model constants: - `CLIENTS`: The participants of the algorithm. - `WITH_CRASHING`: Allow any of participants crash after sending a write message before receiving a response. -- `WITH_RO`: Allow "read-only" clients to particate. The algorithm then becomes a `RWLock` implementation: *many of "read-only" clients commit* or *exactly one of "read-write" client commits*. \ No newline at end of file +- `WITH_RO`: Allow "read-only" clients to participate. The algorithm then becomes a `RWLock` implementation: *many of "read-only" clients commit* or *exactly one of "read-write" client commits*. \ No newline at end of file From 163ec841fd845b0aa415047ed6fa7e31f69d85ed Mon Sep 17 00:00:00 2001 From: Hillium Date: Wed, 18 Dec 2024 14:03:34 +0800 Subject: [PATCH 5/5] address comments Signed-off-by: Hillium --- PutAndVerify/MC.cfg | 2 +- PutAndVerify/MC.tla | 7 +- PutAndVerify/WriteAndVerify.tla | 185 ++++++++++++++++---------------- 3 files changed, 97 insertions(+), 97 deletions(-) diff --git a/PutAndVerify/MC.cfg b/PutAndVerify/MC.cfg index b741d5f..3e9d5cb 100755 --- a/PutAndVerify/MC.cfg +++ b/PutAndVerify/MC.cfg @@ -20,4 +20,4 @@ WVSpec INVARIANT WVConsistency WVTypeOk -\* Generated on Mon Oct 14 15:48:18 CST 2024 \ No newline at end of file +\* Generated on Mon Oct 14 15:48:18 CST 2024 diff --git a/PutAndVerify/MC.tla b/PutAndVerify/MC.tla index 0a46963..0540603 100755 --- a/PutAndVerify/MC.tla +++ b/PutAndVerify/MC.tla @@ -26,6 +26,7 @@ const_172889209848057000 == FALSE ---- -============================================================================= -\* Modification History -\* Created Mon Oct 14 15:48:18 CST 2024 by Hillium +============================================================================= +\* Modification History +\* Created Mon Oct 14 15:48:18 CST 2024 by Hillium + diff --git a/PutAndVerify/WriteAndVerify.tla b/PutAndVerify/WriteAndVerify.tla index 661986c..aa8e068 100755 --- a/PutAndVerify/WriteAndVerify.tla +++ b/PutAndVerify/WriteAndVerify.tla @@ -1,93 +1,92 @@ ---------------------------- MODULE WriteAndVerify --------------------------- - -CONSTANT CLIENTS, WITH_RO, WITH_CRASHING - -VARIABLE storage, clState, clFavor - -Vars == << storage, clState, clFavor >> - -WVTypeOk == /\ storage \in [ CLIENTS -> { "none", "empty", "written", "written-ro", "empty-ro" } ] - /\ clState \in [ CLIENTS -> { "begin", "precheck-done", "blank-written", - "write-check-done", "committed", "aborted", "crashed" } ] - /\ clFavor \in [ CLIENTS -> { "read-write", "read-only" } ] - -WVInit == /\ storage = [ cli \in CLIENTS |-> "none" ] - /\ clState = [ cli \in CLIENTS |-> "begin" ] - /\ clFavor = [ cli \in CLIENTS |-> "read-write" ] - -(* Only one execution can be committed. *) -(* Once committed, the file has been written. *) -WVConsistency == /\ \A i, j \in CLIENTS : - i /= j /\ storage[i] = "written" => ~storage[j] \in { "written", "written-ro" } - -(* "Verify" condition: storage only contains our file or nothing. *) -Check(c) == /\ clFavor[c] = "read-write" => - \A f \in CLIENTS : f /= c => storage[f] = "none" - /\ clFavor[c] = "read-only" => - (* No conflicting write. *) - \A f \in CLIENTS : f /= c => ~storage[f] \in { "empty", "written" } - -Precheck(c) == /\ clState[c] = "begin" - /\ IF Check(c) - THEN clState' = [ clState EXCEPT ![c] = "precheck-done" ] - ELSE clState' = [ clState EXCEPT ![c] = "aborted" ] - /\ UNCHANGED << storage, clFavor >> - -IsRO(c) == clFavor[c] = "read-only" - -DoWriteBlank(c) == /\ clState[c] = "precheck-done" - /\ storage' = [ storage EXCEPT ![c] = IF IsRO(c) THEN "empty-ro" ELSE "empty" ] - -WriteBlank(c) == /\ DoWriteBlank(c) - /\ clState' = [ clState EXCEPT ![c] = "blank-written" ] - /\ UNCHANGED << clFavor >> - - -ConflictCheck(c) == /\ clState[c] = "blank-written" - /\ IF Check(c) - THEN clState' = [ clState EXCEPT ![c] = "write-check-done" ] - ELSE clState' = [ clState EXCEPT ![c] = "aborted" ] - /\ UNCHANGED << storage, clFavor >> - -(* Delete the file when aborted. *) -RollBack(c) == /\ clState[c] = "aborted" - /\ storage[c] /= "none" - /\ storage' = [ storage EXCEPT ![c] = "none" ] - /\ clState' = [ clState EXCEPT ![c] = "begin" ] - /\ UNCHANGED << clFavor >> - -DoCommit(c) == /\ clState[c] = "write-check-done" - /\ storage' = [ storage EXCEPT ![c] = IF IsRO(c) THEN "written-ro" ELSE "written" ] - -Commit(c) == /\ DoCommit(c) - /\ clState' = [ clState EXCEPT ![c] = "committed" ] - /\ UNCHANGED << clFavor >> - -BeRO(c) == /\ clState[c] = "begin" - /\ clFavor[c] = "read-write" - /\ clFavor' = [ clFavor EXCEPT ![c] = "read-only" ] - /\ UNCHANGED << clState, storage >> - -WrittenAndCrash(c) == /\ clState[c] = "precheck-done" \/ clState[c] = "write-check-done" - /\ clState' = [ clState EXCEPT ![c] = "crashed" ] - /\ DoWriteBlank(c) \/ DoCommit(c) - /\ UNCHANGED << clFavor >> - - -WVNext == \E c \in CLIENTS: \/ Precheck(c) - \/ WriteBlank(c) - \/ ConflictCheck(c) - \/ RollBack(c) - \/ Commit(c) - \/ WITH_CRASHING /\ WrittenAndCrash(c) - \/ WITH_RO /\ BeRO(c) - - -WVSpec == WVInit /\ [][WVNext]_Vars - -THEOREM WVSpec => [](WVConsistency /\ WVTypeOk) - -============================================================================= -\* Modification History -\* Last modified Mon Oct 14 15:38:01 CST 2024 by Hillium -\* Created Sat Jun 29 10:41:34 CST 2024 by Hillium +--------------------------- MODULE WriteAndVerify --------------------------- + +CONSTANT CLIENTS, WITH_RO, WITH_CRASHING + +VARIABLE storage, clState, clFavor + +Vars == << storage, clState, clFavor >> + +WVTypeOk == /\ storage \in [ CLIENTS -> { "none", "empty", "written", "written-ro", "empty-ro" } ] + /\ clState \in [ CLIENTS -> { "begin", "precheck-done", "blank-written", + "write-check-done", "committed", "aborted", "crashed" } ] + /\ clFavor \in [ CLIENTS -> { "read-write", "read-only" } ] + +WVInit == /\ storage = [ cli \in CLIENTS |-> "none" ] + /\ clState = [ cli \in CLIENTS |-> "begin" ] + /\ clFavor = [ cli \in CLIENTS |-> "read-write" ] + +(* Only one execution can be committed. *) +(* Once committed, the file has been written. *) +WVConsistency == /\ \A i, j \in CLIENTS : + i /= j /\ storage[i] = "written" => ~storage[j] \in { "written", "written-ro" } + +(* "Verify" condition: storage only contains our file or nothing. *) +Check(c) == /\ clFavor[c] = "read-write" => + \A f \in CLIENTS : f /= c => storage[f] = "none" + /\ clFavor[c] = "read-only" => + (* No conflicting write. *) + \A f \in CLIENTS : f /= c => ~storage[f] \in { "empty", "written" } + +Precheck(c) == /\ clState[c] = "begin" + /\ IF Check(c) + THEN clState' = [ clState EXCEPT ![c] = "precheck-done" ] + ELSE clState' = [ clState EXCEPT ![c] = "aborted" ] + /\ UNCHANGED << storage, clFavor >> + +IsRO(c) == clFavor[c] = "read-only" + +DoWriteBlank(c) == /\ clState[c] = "precheck-done" + /\ storage' = [ storage EXCEPT ![c] = IF IsRO(c) THEN "empty-ro" ELSE "empty" ] + +WriteBlank(c) == /\ DoWriteBlank(c) + /\ clState' = [ clState EXCEPT ![c] = "blank-written" ] + /\ UNCHANGED << clFavor >> + + +ConflictCheck(c) == /\ clState[c] = "blank-written" + /\ IF Check(c) + THEN clState' = [ clState EXCEPT ![c] = "write-check-done" ] + ELSE clState' = [ clState EXCEPT ![c] = "aborted" ] + /\ UNCHANGED << storage, clFavor >> + +(* Delete the file when aborted. *) +RollBack(c) == /\ clState[c] = "aborted" + /\ storage[c] /= "none" + /\ storage' = [ storage EXCEPT ![c] = "none" ] + /\ clState' = [ clState EXCEPT ![c] = "begin" ] + /\ UNCHANGED << clFavor >> + +DoCommit(c) == /\ clState[c] = "write-check-done" + /\ storage' = [ storage EXCEPT ![c] = IF IsRO(c) THEN "written-ro" ELSE "written" ] + +Commit(c) == /\ DoCommit(c) + /\ clState' = [ clState EXCEPT ![c] = "committed" ] + /\ UNCHANGED << clFavor >> + +BeRO(c) == /\ clState[c] = "begin" + /\ clFavor[c] = "read-write" + /\ clFavor' = [ clFavor EXCEPT ![c] = "read-only" ] + /\ UNCHANGED << clState, storage >> + +WrittenAndCrash(c) == /\ clState' = [ clState EXCEPT ![c] = "crashed" ] + /\ DoWriteBlank(c) \/ DoCommit(c) + /\ UNCHANGED << clFavor >> + + +WVNext == \E c \in CLIENTS: \/ Precheck(c) + \/ WriteBlank(c) + \/ ConflictCheck(c) + \/ RollBack(c) + \/ Commit(c) + \/ WITH_CRASHING /\ WrittenAndCrash(c) + \/ WITH_RO /\ BeRO(c) + + +WVSpec == WVInit /\ [][WVNext]_Vars + +THEOREM WVSpec => [](WVConsistency /\ WVTypeOk) + +============================================================================= +\* Modification History +\* Last modified Wed Dec 18 14:00:06 CST 2024 by Hillium +\* Created Sat Jun 29 10:41:34 CST 2024 by Hillium