utwente-fmt / ltsmin

The LTSmin model checking toolset
http://ltsmin.utwente.nl
BSD 3-Clause "New" or "Revised" License
52 stars 30 forks source link

Renault strategy sometimes triggers assertion #148

Closed Meijuh closed 6 years ago

Meijuh commented 6 years ago

Running the command: dve2lts-mc --threads=2 -n --strategy=renault examples/anderson.1.prop4.dve sometimes triggers the following assertion:

dve2lts-mc: Precompiled divine module initialized
dve2lts-mc( 0/ 2): Loading model from /home/jeroen/Documents/gitprojects/ltsmin/build/testsuite/../../src/testsuite/../examples/anderson.1.prop4.dve
dve2lts-mc( 0/ 2): There are 20 state labels and 0 edge labels
dve2lts-mc( 0/ 2): State length is 8, there are 39 groups
dve2lts-mc( 0/ 2): Running renault using 2 cores
dve2lts-mc( 0/ 2): Using a tree table with 2^28 elements
dve2lts-mc( 0/ 2): Successor permutation: dynamic
dve2lts-mc( 0/ 2): Global bits: 0, count bits: 0, local bits: 2
dve2lts-mc( 0/ 2): ~699 levels ~10000 states ~16466 transitions
dve2lts-mc( 0/ 2): ~1354 levels ~20000 states ~32454 transitions
dve2lts-mc( 0/ 2): ~1385 levels ~40000 states ~86708 transitions
dve2lts-mc( 0/ 2): ~1385 levels ~80000 states ~194748 transitions
dve2lts-mc( 0/ 2), file ../../../src/src/mc-lib/renault-unionfind.c, line 227: assertion "r_uf_is_dead (uf, state)" failed: state should be dead
dve2lts-mc( 0/ 2): Could not remove /tmp/ltsmin-Cbz7iY. 

This happens on osx and Linux.

Meijuh commented 6 years ago

For know I made this a known issue in v3.0.0: https://github.com/utwente-fmt/ltsmin/commit/397586d1a4e068f669d4210f2244b14a3a68c93e.

alaarman commented 6 years ago

Fixed in 26a00ab