Markus Alexander Kuppe comments

Results 409 comments of


                                            Markus Alexander Kuppe

Make SimpleEventually proof a bit less simple.

TLAPS starts to reject Stephan's [proposed proof](https://github.com/tlaplus/tlapm/pull/135/commits/c64d9522fac9e99a72f447ca3ce57e35effdc53a) as well as my [extension](https://github.com/tlaplus/tlapm/pull/135/commits/102637fd2c5c4649819cdc118864c394fda55489) with the introduction of the new SMT encoding in 3f0847802bab27c4e57c3da11841a88d4ae07709. https://github.com/tlaplus/tlapm/commit/581ebd8afbe927b2b7d31c62ccec3a3409d9d8ce is the last commit with which TLAPS...

Bogus safety violation checking if a set is a subset of Nat.

5724d0d causes Apalache to report a proper error message: `SetInRule is not implemented for type PowSet[Set(Int)] (found in {1, 2, 3, 4} ∈ SUBSET Nat)`.

Bogus safety violation checking if a set is a subset of Nat.

@thpani @konnov https://github.com/apalache-mc/apalache/commit/c69c355877ea306e38eaf53212ba779efa14318b and https://github.com/apalache-mc/apalache/commit/830caa71596caf488b7717b39ba2a4e535ddb779 cause Apalache to no longer hit this code path for the given inputs (the expressions are rewritten elsewhere). Would you like to add the safeguard...

Bogus safety violation checking if a set is a subset of Nat.

@konnov This PR does not aim to extend the encoding. Instead, it ensures that Apalache throws an error when an infinite set is encountered in a context where it isn't...

Bogus safety violation checking if a set is a subset of Nat.

This is ready for review and merging. Although commits c69c355877ea306e38eaf53212ba779efa14318b and 830caa71596caf488b7717b39ba2a4e535ddb779 prevent any of the three encodings from reporting a bogus invariant violation for expressions like `{1, 2, 3}...

Bogus safety violation checking if a set is a subset of Nat.

What should that entry be?

Bogus safety violation checking if a set is a subset of Nat.

done

tlapm ending abnormally with Invalid_argument("List.combine") in level or arity checking

Latest and greatest (6acb3cb) errors out right away: ```scala -> % ~/.opam/5.1.0/bin/tlapm --version 6acb3cb -> % ~/.opam/5.1.0/bin/tlapm --cleanfp BlockingQueueFair.tla File "./BlockingQueue.tla", line 126, characters 21-28: Error: Invalid number of arguments...

tlapm ending abnormally with Invalid_argument("List.combine") in level or arity checking

[Removing the `USE` from `BlockingQueue.tla`](https://github.com/lemmy/BlockingQueue/blob/4e227ab2eae1d2400689238dbdd4da2c30dc532e/BlockingQueue.tla#L77-L81) allows TLAPS to prove `BlockingQueueSplit.tla`. However, `BlockingQueueFair.tla` fails with a new error that mentions `EnabledWrapper`, which is not defined or declared in my workspace: ```shell...

tlapm ending abnormally with Invalid_argument("List.combine") in level or arity checking

The `EnabledWrapper` error appears to be coming from the *two* levels of refinement: BGFair refines BGSplit refines BQ. No error if the INSTANCE statement removed in BQSplit. ```diff diff --git...