Markus Alexander Kuppe
Markus Alexander Kuppe
- Every tla2tools build is [published](https://github.com/tlaplus/tlaplus/blob/ad133ce159375f94071f0571f28460c705939d2a/.github/workflows/main.yml#L242-L249) to Github packages (the [1.7.0 build number](https://github.com/tlaplus/tlaplus/blob/ad133ce159375f94071f0571f28460c705939d2a/tlatools/org.lamport.tlatools/github.xml#L13) is clearly outdate) - Pulling/Installing tla2tools.jar from [Github packages](https://docs.github.com/en/packages/working-with-a-github-packages-registry/working-with-the-apache-maven-registry#installing-a-package) with maven, sbt, ... [requires authentication](https://github.com/tlaplus/tlaplus/blob/ad133ce159375f94071f0571f28460c705939d2a/.github/workflows/main.yml#L242-L249) with a...
Painful, but tla2tools.jar will from now on be published at https://oss.sonatype.org/content/repositories/snapshots/org/lamport/tla2tools/1.8.0-SNAPSHOT/
I recommend using the new snapshot dependency from Sonatype until the version of SANY with Unicode support is fully integrated into Apalache. Once this integration is complete, we can manually...
No, I didn't mean to suggest a full-scale tla2tools.jar and Toolbox release. What I had in mind was more like a monthly or quarterly code snapshot (not -SNAPSHOT) that would...
> > This looks good to me, interesting to learn that Apalache doesn't use a separate model file for constants but defines everything in one file. > > Maybe a...
> There is also [this way](https://apalache.informal.systems/docs/apalache/parameters.html#convention-over-configuration) to replace operators, but it is very Apalache-specific. Did you create the prefix convention before introducing type annotations? It appears to me that using...
> However, it seems like like a small refactor may be enough to make it Apalache compatible? Refactoring of Apalache or Voting.tla? In my opinion, TLA+ examples should not be...
TLC should have produced a warning for `V'=... /\ ... /\ UNCHANGED `.
Disabling the special handling of `SUBSET Int` in the SetMembershipSimplifier by commenting out the SUBSET [case](https://github.com/apalache-mc/apalache/blob/4f0b30ea339635547fc667bd9c3b5ec0ead27de2/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala#L63-L64) results in Apalache also reporting a bogus counterexample for `SUBSET Int`. This suggests a...
More observation: * The size of infinite sets like `Nat` is 0, which results in them being processed by the same branch that handles the empty set: https://github.com/apalache-mc/apalache/blob/4f0b30ea339635547fc667bd9c3b5ec0ead27de2/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/LazyEquality.scala#L303-L312 * `{}...