-
- Downloads
Please tell me *which* "Successor state is not completely specified by
the next-state action." Additionally, include action name which leaves the state incomplete. Fixes Github issue #118 https://github.com/tlaplus/tlaplus/issues/118 [Feature][TLC][Changelog]
Showing
- tlatools/src/tlc2/output/MP.java 9 additions, 1 deletiontlatools/src/tlc2/output/MP.java
- tlatools/src/tlc2/tool/Action.java 4 additions, 0 deletionstlatools/src/tlc2/tool/Action.java
- tlatools/src/tlc2/tool/DFIDModelChecker.java 17 additions, 1 deletiontlatools/src/tlc2/tool/DFIDModelChecker.java
- tlatools/src/tlc2/tool/ModelChecker.java 16 additions, 1 deletiontlatools/src/tlc2/tool/ModelChecker.java
- tlatools/src/tlc2/tool/TLCState.java 2 additions, 0 deletionstlatools/src/tlc2/tool/TLCState.java
- tlatools/src/tlc2/tool/TLCStateFun.java 5 additions, 0 deletionstlatools/src/tlc2/tool/TLCStateFun.java
- tlatools/src/tlc2/tool/TLCStateMut.java 21 additions, 0 deletionstlatools/src/tlc2/tool/TLCStateMut.java
- tlatools/src/tlc2/tool/TLCStateMutSource.java 21 additions, 0 deletionstlatools/src/tlc2/tool/TLCStateMutSource.java
- tlatools/test-model/IncompleteNextMultipleActions.cfg 2 additions, 0 deletionstlatools/test-model/IncompleteNextMultipleActions.cfg
- tlatools/test-model/IncompleteNextMultipleActions.tla 11 additions, 0 deletionstlatools/test-model/IncompleteNextMultipleActions.tla
- tlatools/test/tlc2/tool/IncompleteNextMultipleActionsTest.java 67 additions, 0 deletions...ols/test/tlc2/tool/IncompleteNextMultipleActionsTest.java
- tlatools/test/tlc2/tool/IncompleteNextTest.java 7 additions, 0 deletionstlatools/test/tlc2/tool/IncompleteNextTest.java
- tlatools/test/tlc2/tool/queue/DummyTLCState.java 11 additions, 0 deletionstlatools/test/tlc2/tool/queue/DummyTLCState.java
Loading
Please sign in to comment