Markus Alexander Kuppe
Markus Alexander Kuppe
`PowSetT` has only limited support of *finite* sets according to its documentation: https://github.com/apalache-mc/apalache/blob/d2b5cc26f1ff0e6211b61b92bb2db5dd9625feca/tlair/src/main/scala/at/forsyte/apalache/tla/bmcmt/types/package.scala#L139-L153
> > Rewriting `A \subseteq B` as `A \in SUBSET B` (see diff below) triggers the same bug. > > I'd suggest the opposite: add a case in Keramelizer, analogous...
> [...] However, it doesn't handle more complex scenarios such as: > > ```tla > ------------------------- MODULE APASubRec ------------------------------ > EXTENDS Integers > > VARIABLE > \* @type: { p:...
> > I wonder though why we end up in PowSetCtorRule with Nat in the first place. > > @Kukovec @konnov shouldn't we check for that somewhere? > > The...
@thpani This PR implements the functionality you recommended in your comment https://github.com/apalache-mc/apalache/issues/2948#issuecomment-2307161449.
Thanks for merging.
FWIW: TLC could also use the JVM that is [bundled](https://github.com/tlaplus/tlapm/issues/181) as part of TLAPS.
@muenchnerkindl Do you expect AI (LLMs) to play a role in this project?
The TLA+ tools—specifically SANY—do not support a concept equivalent to a "class path" or "library path" as found in other ecosystems, which could be used to automatically locate TLA+ modules....
It makes a lot of sense to expand this menu to include all TLA+ modules available on the search paths. Ideally, clicking on a module would open it in a...