Kukovec
Kukovec
Currently the section ``` TLA+ Language Manual for Engineers -> The standard operators of TLA+ -> Bags ``` is blank. Since we now support the community modules, we need to...
Following a Slack troubleshooting session, it seems to be a QoL barrier for first-time users, since Apalache reports test failures if one simply runs `make` on a freshly cloned repository,...
As `tla-types` is now a typechecker-only module, and passes live on their own, we should rewire dependencies in `build.sbt` to reflect the new dependency graph.
When encountering two syntactically-equal and type-equal `Gen`-initializations, apalache appears to cache the RHS, making it impossible to generate different values for two variables initializaed this way. For the attached module,...
We should revisit all use cases of the scope-safe builder outside of tests, and eveluate whether we need scope-safety-by-construction, or whether it makes more sense to used the cheaper unsafe...