Skip to content

Comments

Check liveness#6

Draft
lemmy wants to merge 7 commits intoPirateshipOrg:mainfrom
lemmy:mku-liveness
Draft

Check liveness#6
lemmy wants to merge 7 commits intoPirateshipOrg:mainfrom
lemmy:mku-liveness

Conversation

@lemmy
Copy link
Collaborator

@lemmy lemmy commented Nov 6, 2024

No description provided.

lemmy added 7 commits November 5, 2024 18:23
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Clearly, `TRUE \notin Range(primary)` can not be implemented.

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
…mmitIndex keep forever increasing.

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Fixes Github issue PirateshipOrg#2
https://github.com/heidihoward/pirateship-tla/issues/2

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
…e-correct) Txn.

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
MonotonicReduction—is sufficient to constrain the state space and verify
essential safety and liveness properties.

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant