Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Finite Monotonic #153

Draft
wants to merge 7 commits into
base: master
Choose a base branch
from
+175 −1
Draft

Finite Monotonic #153

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
8034c04
Turn `Convergence` from a state predicate that is true or false of th…
lemmy Oct 17, 2024
7c7576b
Add a fairness constraint (not machine-closed) that asserts there are…
lemmy Oct 17, 2024
3debf30
Add script and model spec to explore diferent fairness constraints wi…
lemmy Oct 17, 2024
8e9dc07
Add TRUE, i.e., no fairness as a possible fairness constraint.
lemmy Oct 18, 2024
f3763ac
Do not switch between `GarbageCollect` and no `GarbageCollect` conjoi…
lemmy Oct 18, 2024
45443ef
Assert the shape of the counterexamples under all configuration. Log …
lemmy Oct 18, 2024
d8bdb00
Ensure that the exit/return value of nested TLC runs is either
lemmy Oct 18, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Do not switch between GarbageCollect and no GarbageCollect conjoi… 
…ned to `Next.` Instead, toggle between `GarbageCollect` conjoined to `Next` and `GarbageCollect` as a separate VIEW.

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
  • Loading branch information
@lemmy
lemmy committed Oct 18, 2024
commit f3763ac2152487c5d008c70f65ddd065295e75ac
1 change: 1 addition & 0 deletions specifications/FiniteMonotonic/MCCRDT.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,3 +16,4 @@ PROPERTIES

CONSTRAINTS StateConstraint
CONSTANTS Increment <- MCIncrement
VIEW View
14 changes: 13 additions & 1 deletion specifications/FiniteMonotonic/MCCRDT.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,8 +20,9 @@ ASSUME F \in 0..7

------

SetMin(s) == CHOOSE e \in s : \A o \in s : e <= o

GarbageCollect ==
LET SetMin(s) == CHOOSE e \in s : \A o \in s : e <= o IN
LET Transpose == SetMin({counter[n][o] : n, o \in Node}) IN
counter' = [
n \in Node |-> [
Expand All @@ -31,6 +32,17 @@ GarbageCollect ==

------

View ==
IF GB THEN vars ELSE
LET Transpose == SetMin({counter[n][o] : n, o \in Node}) IN
[
n \in Node |-> [
o \in Node |-> counter[n][o] - Transpose
]
]

------

S == INSTANCE CRDT

MCIncrement(n) ==
Expand Down