The Model checker generated empty states which did not meet expectations. I wrote a simple TLA specfication, https://github.com/ybbh/tla_state. When I used the model checker to check it, it generated empty initial states.
Model checker should generate non-empty initial states.
Model checker generated empty initial states.
- git clone [email protected]:ybbh/tla_state.git
- Toolbox: File -> Open Spec -> Add New Spec -> open state.tla
- Toolbox: models -> New Model -> filling Temporal formula with Spec -> setting constants NODE_ID by {"n1", "n2"}
- Toolbox: Run TLA on the model
- Toolbox: The model checker result generated empty initial states
-
When I changed the constants NODE_ID by {"n1"}, it generated correct result.
-
The initial states would be OK if I uncomment this line in state.tla.
__WhyWeNeedThis == S2
Possible when producing the initial state, the toolbox threw some unknown exceptions.
- TLC version: 2.15, 2.16
- version: 1.8.0.202303090234, 1.7.1.202012311918
- Operating System: Windows 10