-
- Downloads
[Bugfix] Stop NoSuchElementException during distributed modelchecking.
TLCIterator#getLast does not return the last element when the largest fingerprint that is *not* on disk fails to be in the last non-null bucket. This case however, is perfectly valid. Its likelyhood is increased when checkpointing is enabled. Then the buckets are flushed in shorter intervals causing a higher chance that the last bucket has only on-disk fingerprints in it when getLast() is called.
Showing
- tlatools/src/tlc2/tool/fp/DiskFPSet.java 7 additions, 1 deletiontlatools/src/tlc2/tool/fp/DiskFPSet.java
- tlatools/src/tlc2/tool/fp/MSBDiskFPSet.java 20 additions, 10 deletionstlatools/src/tlc2/tool/fp/MSBDiskFPSet.java
- tlatools/test/tlc2/tool/fp/DummyFPSetConfiguration.java 4 additions, 0 deletionstlatools/test/tlc2/tool/fp/DummyFPSetConfiguration.java
- tlatools/test/tlc2/tool/fp/MSBDiskFPSetTest2.java 67 additions, 1 deletiontlatools/test/tlc2/tool/fp/MSBDiskFPSetTest2.java
Loading
Please register or sign in to comment