Markus Alexander Kuppe
Markus Alexander Kuppe
The no maintenance of no tags is certainly appealing but does it work for other (non-technical) tags such as ```[beginner|intermediate|advanced]```?
There is no additional metadata yet. I was just wondering if we can envision a tagging scheme that works for all metadata (let it be technical s.a. ```[tla|pcal|tlaps|``` or non-tech...
I'm reluctant to change the directory layout because others might rely on the current layout. E.g. Apalache runs benchmarks based on the examples and likely has scripts setup for that.
@konnov Does https://github.com/konnov/apalache depend on the directory structure of the TLA+ examples?
"wheel" might be missing from setup.py (https://stackoverflow.com/a/44862371/6291195)?
@fhackett Just in case you're not aware of work that appears related: * https://youtu.be/TP3SY0EUV2A?t=991 * http://www.vldb.org/pvldb/vol13/p1346-davis.pdf * https://youtu.be/itcj9j2yWQo By the way, have you considered targeting other programming languages than Go...
> * the "eXtreme Modelling in practice" paper mentions they had trouble with the trace checking I'm suggesting here. Certainly, if one does not happen to be generating a large...
@muenchnerkindl Would it be useful to include TLAPS in the `@supportedBy` annotation? For example, annotate operators for which we have lemmas? We could revert `@supportedBy` into `@unsupportedBy` to make it...
Although copy&paste usually works for TLA+ definitions and thus doesn't create an additional dependency, this is not true for Java module overrides. Since one of the main value propositions of...
Another idea: Instead of bundling CM with tla2tools.jar, tla2tools.jar could have a command to automatically fetch (a particular) version of CM from the web.