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

Jump to bottom

Finite Monotonic #153

Draft
wants to merge 7 commits into
base: master
Choose a base branch
from
Draft

Finite Monotonic #153

wants to merge 7 commits into from
+175 −1

Commits on Oct 17, 2024

  1. Turn Convergence from a state predicate that is true or false of th… 

    …e initial states into a liveness property.

Signed-off-by: Markus Alexander Kuppe <[email protected]>
    @lemmy
    lemmy committed Oct 17, 2024
    Configuration menu
    Copy the full SHA
    8034c04 View commit details
    Browse the repository at this point in the history

  2. Add a fairness constraint (not machine-closed) that asserts there are… 

    … only finitely many Increment actions. A sufficient but weaker fairness constraint would be one that guarantees a sufficient number of uninterrupted Gossip steps.

Signed-off-by: Markus Alexander Kuppe <[email protected]>
    @lemmy
    lemmy committed Oct 17, 2024
    Configuration menu
    Copy the full SHA
    7c7576b View commit details
    Browse the repository at this point in the history

  3. Add script and model spec to explore diferent fairness constraints wi… 

    …th and without the `GarbageCollect` action, a state constraint or a conjunct to disable `Increment`, and different bounds for the divergence.

Signed-off-by: Markus Alexander Kuppe <[email protected]>
    @lemmy
    lemmy committed Oct 17, 2024
    Configuration menu
    Copy the full SHA
    3debf30 View commit details
    Browse the repository at this point in the history

Commits on Oct 18, 2024

  1. Add TRUE, i.e., no fairness as a possible fairness constraint. 

    Signed-off-by: Markus Alexander Kuppe <[email protected]>
    @lemmy
    lemmy committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    8e9dc07 View commit details
    Browse the repository at this point in the history

  2. 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 <[email protected]>
    @lemmy
    lemmy committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    f3763ac View commit details
    Browse the repository at this point in the history

  3. Assert the shape of the counterexamples under all configuration. Log … 

    …to a CSV file is violated.

Depends on pending PR tlaplus/tlaplus#1042

Signed-off-by: Markus Alexander Kuppe <[email protected]>
    @lemmy
    lemmy committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    45443ef View commit details
    Browse the repository at this point in the history

  4. Ensure that the exit/return value of nested TLC runs is either 

    a successful run with no counterexample, a run that detected
a liveness violation, or a postcondition violation.

Signed-off-by: Markus Alexander Kuppe <[email protected]>
    @lemmy
    lemmy committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    d8bdb00 View commit details
    Browse the repository at this point in the history