Markus Alexander Kuppe comments

Results 409 comments of


                                            Markus Alexander Kuppe

Generating initial states fails for qspinlock spec that's part of the Linux kernel

Looking at a trace of that spec makes me curious—does Spectacle support ALIASES?

Generating initial states fails for qspinlock spec that's part of the Linux kernel

```tla Next == (\E self \in ProcSet: \/ spin_lock(self) \/ spin_unlock(self) \/ spin_trylock(self) \/ spin_lock_slowpath(self)) \/ (\E self \in THREADS: thread(self)) ``` Given the (PlusCal-generated) next-state relation above, this action...

Latest pre-release does not work on non-recent Linux (e.g. Codespace default) due to GLIBC version

IMO it is a good practice to support the last two LTS releases of [Debian](https://wiki.debian.org/LTS) and [Ubuntu](https://wiki.ubuntu.com/Releases).

Verify proofs in examples/ directory as part of PR workflow

I don't have an opinion, except that some examples are perhaps too basic for the example repo?!

Verify proofs in examples/ directory as part of PR workflow

`GraphTheorem` could be aligned with a moved next to https://github.com/tlaplus/CommunityModules/blob/master/modules/Graphs.tla, like `FiniteSetExtTheorem` is next to `FiniteSetExt` in the CommunityModules?

TLAPS proves `~(x = TRUE) <=> (x = FALSE)` in released versions

Bisecting between a963bd37372d8ca0ba627687d80d4116447971aa and 8facb9aace60be675a110db98956bfd7222fa34f (HEAD) identifies 3f0847802bab27c4e57c3da11841a88d4ae07709 as the fix. This commit is the tip of @adef-inr new SMT encoding, confirming Stephan's hypothesis in #135. I confirmed that the...

TLAPS proves `~(x = TRUE) <=> (x = FALSE)` in released versions

IMO this is a severe bug that warrants a new release.

Make SimpleEventually proof a bit less simple.

> See individual comments. In particular, this uncovers a big problem with the old SMT backend. Please take another look at this PR. I will open an issue for the...

Make SimpleEventually proof a bit less simple.

Confirmed to be rejected by `HEAD@main` on a Codespace (Linux): ```shell @lemmy ➜ /workspaces/tlapm/examples (mku-LessSimpleEventually) $ tlapm --version 102637f-dirty @lemmy ➜ /workspaces/tlapm/examples (mku-LessSimpleEventually) $ tlapm SimpleEventually.tla (* created new ".tlacache/TLAPS.tlaps/TLAPS.thy"...

Make SimpleEventually proof a bit less simple.

Stephan's [proposed proof ](https://github.com/tlaplus/tlapm/pull/135/commits/c64d9522fac9e99a72f447ca3ce57e35effdc53a)already rejected by `HEAD@main`: ```shell @lemmy ➜ /workspaces/tlapm/examples (mku-LessSimpleEventually) $ tlapm SimpleEventually.tla (* created new ".tlacache/TLAPS.tlaps/TLAPS.thy" *) (* fingerprints written in ".tlacache/TLAPS.tlaps/fingerprints" *) File "/usr/local/lib/tlapm/stdlib/TLAPS.tla", line 1,...