-
- Downloads
Safety-checking of the behavior graph incorrectly returns lasso-shaped
and not a finite prefix counter-example. Fixes Github issue #710 https://github.com/tlaplus/tlaplus/issues/710 [Bug][TLC][Changelog]
Showing
- tlatools/org.lamport.tlatools/src/tlc2/tool/liveness/LiveCheck.java 92 additions, 5 deletions...rg.lamport.tlatools/src/tlc2/tool/liveness/LiveCheck.java
- tlatools/org.lamport.tlatools/src/tlc2/tool/liveness/Liveness.java 10 additions, 1 deletion...org.lamport.tlatools/src/tlc2/tool/liveness/Liveness.java
- tlatools/org.lamport.tlatools/src/tlc2/tool/liveness/TBGraphNode.java 14 additions, 0 deletions....lamport.tlatools/src/tlc2/tool/liveness/TBGraphNode.java
- tlatools/org.lamport.tlatools/test-model/Github710.cfg 3 additions, 0 deletionstlatools/org.lamport.tlatools/test-model/Github710.cfg
- tlatools/org.lamport.tlatools/test-model/Github710a.tla 22 additions, 0 deletionstlatools/org.lamport.tlatools/test-model/Github710a.tla
- tlatools/org.lamport.tlatools/test-model/Github710b.tla 20 additions, 0 deletionstlatools/org.lamport.tlatools/test-model/Github710b.tla
- tlatools/org.lamport.tlatools/test/tlc2/tool/liveness/CodePlexBug08AgentRingTest.java 3 additions, 26 deletions...s/test/tlc2/tool/liveness/CodePlexBug08AgentRingTest.java
- tlatools/org.lamport.tlatools/test/tlc2/tool/liveness/CodePlexBug08AgentRingTest_TTraceTest.java 3 additions, 32 deletions.../tool/liveness/CodePlexBug08AgentRingTest_TTraceTest.java
- tlatools/org.lamport.tlatools/test/tlc2/tool/liveness/Github710aTest.java 68 additions, 0 deletions...port.tlatools/test/tlc2/tool/liveness/Github710aTest.java
- tlatools/org.lamport.tlatools/test/tlc2/tool/liveness/Github710bTest.java 65 additions, 0 deletions...port.tlatools/test/tlc2/tool/liveness/Github710bTest.java
Loading
Please register or sign in to comment