Comments (3)
fan-tom
commented on July 19, 2024
Though a workaround exists, in a big specification with lots of short-living variables, usually named the same, it is not obvious which operator we are referring here, as there is no user-defined operator with this name and there is no source location in the error message
from apalache.
shonfeder
commented on July 19, 2024
Interesting behavior here. Thank you for the report!
Maybe a good start here would be to figure out the intention behind at.forsyte.apalache.tla.imp.ModuleTranslator#workaroundMarkRecursive and whether there are any cases where we actually need it, just in case the fix here could be as simple as getting rid of that check.
from apalache.
fan-tom
commented on July 19, 2024
Comment says it is a workaround for this issue #130, which is caused by a bug in SANY, but there is no link to this SANY bug to understand whether we still need it
from apalache.
Related Issues (20)
- Unexpected exception HOT 2
- Document Apalache config format + options
- A set filter over PowSet[FinSet[Int]] is not implemented
- Wrong function sets counterexample? HOT 6
- Add warning for misplaced occurrence of `oneOf` when parsing from quint
- Raise error when an unexpanded type constant is found in quint IR output
- `parse` command adds superfluous `EXTENDS` statement HOT 2
- Use `parse` to format modules. HOT 2
- Unhandled Exception (java.util.NoSuchElementException: None.get) on empty file input HOT 4
- Crash with `funArrays` encoding HOT 2
- Typechecking crashes with `IllegalArgumentException: Unsupported expression` on unbounded quantification (e.g., `\A x: P`). HOT 8
- Operator overriding in annotations
- Include constant value assignments in ITF
- Allow specifying types in separate files
- Extend the server to be able to reply with formatted TLA+ generated from the IR HOT 1
- Pretty printing the apalache IR into TLA+ does not sanitize identifiers
- Assignments in quint `init` operators need to be unprimed HOT 2
- TLA+ pretty printer produces `[]` on empty tuples, which is invalid syntax
- Add support for Quint's `allListsUpTo`
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from apalache.