search

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

Writing trace with ndfs sometimes failes #147

Closed Meijuh closed 6 years ago

Meijuh commented 6 years ago

Running the command dve2lts-mc --trace=a.gcf --strategy=ndfs examples/iprotocol.2.prop4.dve sometimes gives the following error: 

dve2lts-mc: Precompiled divine module initialized
dve2lts-mc( 0/ 4): Loading model from /home/jeroen/Documents/gitprojects/ltsmin/build/testsuite/../../src/testsuite/../examples/iprotocol.2.prop4.dve
dve2lts-mc( 0/ 4): There are 54 state labels and 0 edge labels
dve2lts-mc( 0/ 4): State length is 26, there are 360 groups
dve2lts-mc( 0/ 4): Running ndfs using 4 cores
dve2lts-mc( 0/ 4): Using a tree table with 2^28 elements
dve2lts-mc( 0/ 4): Successor permutation: dynamic
dve2lts-mc( 0/ 4): Global bits: 0, count bits: 0, local bits: 2
dve2lts-mc( 0/ 4): [Blue] ~250 levels ~10000 states ~6854 transitions
dve2lts-mc( 1/ 4):
dve2lts-mc( 1/ 4): Accepting cycle FOUND at depth 170!
dve2lts-mc( 1/ 4):
dve2lts-mc( 1/ 4): Writing trace to a.gcf
dve2lts-mc( 1/ 4), ** error **: no matching transition found for 165

Found using 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 39d7b3c3839965d64fcb5e363105452bf0981c89.