ybbh / tla_state

Description

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.

Expected Behavior

Model checker should generate non-empty initial states.

Actual Behavior

Model checker generated empty initial states.

Steps to Reproduce

1. git clone [email protected]:ybbh/tla_state.git
2. Toolbox: File -> Open Spec -> Add New Spec -> open state.tla
3. Toolbox: models -> New Model -> filling Temporal formula with Spec -> setting constants NODE_ID by {"n1", "n2"}
4. Toolbox: Run TLA on the model
5. Toolbox: The model checker result generated empty initial states

Steps Taken to Fix

1. When I changed the constants NODE_ID by {"n1"}, it generated correct result.

2. The initial states would be OK if I uncomment this line in state.tla.

     __WhyWeNeedThis == S2
   

Possible Fix

Possible when producing the initial state, the toolbox threw some unknown exceptions.

Your Environment

• TLC version: 2.15, 2.16
• version: 1.8.0.202303090234, 1.7.1.202012311918
• Operating System: Windows 10