Markus Alexander Kuppe
Markus Alexander Kuppe
The current fix is too narrow: ```tla ---- MODULE M ---- EXTENDS Integers VARIABLE \* @type: Int; x Init == x = 0 Next == x' \in 0..42 \* No...
Btw. it would be nice if `--config=SomeConfigFile.cfg` could be `--config SomeConfigFile.cfg` to make the shell's tab-completion work.
Ditching cinit and rewriting `CONSTANT N` to `N == 4` works fine.
@konnov It seems I don't understand the semantics of [`ConstInit`](https://github.com/konnov/apalache/blob/master/docs/manual.md#53-constinit-predicate-). I assumed that `Initializing CONSTANTS with the provided operator` in Apalache's output prior to the exception says that `CONSTANT N`...
`CONSTANT N` has to be initialized in a config (`MC.cfg`), but configs are a clutch. It's much more convenient to have no `MC.cfg` and define (several) `ConstInit` in `MC.tla`.
The TLA+ definition of `TakeSet` could be added to https://github.com/tlaplus/CommunityModules/blob/57e173e41930ae4c8a3301d6a0f078717cc8d470/modules/FiniteSetsExt.tla#L43-L57
What is missing before this PR can be merged? I'm happy to take this on.
This appears to be a `classpath` issue. With Java: Options set to `-classpath CommunityModules.jar`, evaluation fails whereas it succeeds with a full qualified path `-classpath /home/markus/blockingqueue/CommunityModules.jar`. Fails: ``` /usr/lib/jvm/java-11-openjdk-amd64//bin/java -classpath...
@klinvill Thanks; I will report back on the ergonomics.
3. seems to be most in line with how the Toolbox handles its `F11` shortcut.