Error: tree leafs table full! Change -s/--ratio

[yanntm]

I've run into this issue for some larger models;

I don't know what value I should put for --ratio since the default 2 is not good, I don't understand the help text very well. Shoudl I try a a higher value (3 ?) or a lower one (>1 ? < 1 ?)

Moreover, the fact that the tool runs out of memory is not correctly captured/reported. The tool happily returns 0, instead of failing. Since the 0 return value is semantic (no counter example found), this is not normal, we should get 255 or something as return code.

I think that it failed to explore some permutations due to out of mem, and deduced that it had finished exploring all perms, which is not true.

In other words, https://github.com/utwente-fmt/ltsmin/blob/ba6db313e99d5f92922f3a83ae8a4f831d369dc9/src/pins2lts-mc/parallel/permute.c#L198

needs to conclude with Abort, not just a warning.

Trace below, obtained for Referendum-COL-0050-ReachabilityDeadlock from the MCC, where it is not finding the deadlock, and concluding there is none (NB: expected response : there is a deadlock OR Fail):

INFO: Standard error output from running tool CommandLine [args=[/home/ythierry/test/ITS-Tools-pnmcc/lts_install_dir/bin/pins2lts-mc, ./gal.so, --threads=1, --when, -d], workingDir=/home/ythierry/test/ITS-Tools-pnmcc/INPUTS/31830]
pins2lts-mc, 0.000: Registering PINS so language module
pins2lts-mc, 0.000: Loading model from ./gal.so
pins2lts-mc, 0.000: library has no initializer
pins2lts-mc, 0.000: loading model GAL
pins2lts-mc, 0.001: completed loading model GAL
pins2lts-mc, 0.001: There are 102 state labels and 1 edge labels
pins2lts-mc, 0.001: State length is 151, there are 101 groups
pins2lts-mc, 0.001: Running bfs using 1 core (sequential)
pins2lts-mc, 0.001: Using a non-indexing tree table with 2^27 elements
pins2lts-mc, 0.001: Successor permutation: none
pins2lts-mc, 0.001: Global bits: 0, count bits: 0, local bits: 0
pins2lts-mc, 0.424: 4 levels 1000 states 96109 transitions
pins2lts-mc, 0.636: 4 levels 2000 states 192109 transitions
pins2lts-mc, 0.941: 4 levels 4000 states 384109 transitions
pins2lts-mc, 1.560: 5 levels 8000 states 762113 transitions
pins2lts-mc, 2.650: 5 levels 16000 states 1514113 transitions
pins2lts-mc, 4.426: 5 levels 32000 states 3018113 transitions
pins2lts-mc, 7.753: 5 levels 64000 states 6026113 transitions
pins2lts-mc, 14.378: 5 levels 128000 states 12042113 transitions
pins2lts-mc, 27.664: 6 levels 256000 states 23885717 transitions
pins2lts-mc, 54.754: 6 levels 512000 states 47437717 transitions
pins2lts-mc, 113.024: 6 levels 1024000 states 94541717 transitions
pins2lts-mc, 227.712: 6 levels 2048000 states 188749717 transitions
pins2lts-mc, 239.826: Error: tree leafs table full! Change -s/--ratio.
pins2lts-mc, 239.863:  
pins2lts-mc, 239.863:  
pins2lts-mc, 239.863: Explored 2066447 states 190446841 transitions, fanout: 92.161
pins2lts-mc, 239.863: Total exploration time 239.860 sec (239.860 sec minimum, 239.860 sec on average)
pins2lts-mc, 239.863: States per second: 8615, Transitions per second: 793992
pins2lts-mc, 239.863:  
pins2lts-mc, 239.863: Queue width: 8B, total height: 50941943, memory: 388.66MB
pins2lts-mc, 239.863: Tree memory: 660.4MB, 13.1 B/state, compr.: 2.2%
pins2lts-mc, 239.863: Tree fill ratio (roots/leafs): 39.0%/99.0%
pins2lts-mc, 239.863: Stored 101 string chucks using 0MB
pins2lts-mc, 239.863: Total memory used for chunk indexing: 0MB
pins2lts-mc, 239.863: Est. total memory use: 1049.1MB (~1412.7MB paged-in)
Exit code :0

[alaarman]

See also #135

[alaarman]

Thanks for the report, Yann. Your assessment is correct.

There is a related bug report, where I added your email:

https://github.com/utwente-fmt/ltsmin/issues/135

I’ll look into it.

Best,

Alfons

From: Yann Thierry-Mieg notifications@github.com Reply-To: utwente-fmt/ltsmin reply@reply.github.com Date: Friday, 8 December 2017 at 15:34 To: utwente-fmt/ltsmin ltsmin@noreply.github.com Cc: Subscribed subscribed@noreply.github.com Subject: [utwente-fmt/ltsmin] Error: tree leafs table full! Change -s/--ratio (#145)

I've run into this issue for some larger models;

I don't know what value I should put for --ratio since the default 2 is not good, I don't understand the help text very well. Shoudl I try a a higher value (3 ?) or a lower one (>1 ? < 1 ?)

Moreover, the fact that the tool runs out of memory is not correctly captured/reported. The tool happily returns 0, instead of failing. Since the 0 return value is semantic (no counter example found), this is not normal, we should get 255 or something as return code.

I think that it failed to explore some permutations due to out of mem, and deduced that it had finished exploring all perms, which is not true.

In other words, https://github.com/utwente-fmt/ltsmin/blob/ba6db313e99d5f92922f3a83ae8a4f831d369dc9/src/pins2lts-mc/parallel/permute.c#L198

needs to conclude with Abort, not just a warning.

Trace below, obtained for Referendum-COL-0050-ReachabilityDeadlock from the MCC, where it is not finding the deadlock, and concluding there is none (NB: expected response : there is a deadlock OR Fail): INFO: Standard error output from running tool CommandLine [args=[/home/ythierry/test/ITS-Tools-pnmcc/lts_install_dir/bin/pins2lts-mc, ./gal.so, --threads=1, --when, -d], workingDir=/home/ythierry/test/ITS-Tools-pnmcc/INPUTS/31830] pins2lts-mc, 0.000: Registering PINS so language module pins2lts-mc, 0.000: Loading model from ./gal.so pins2lts-mc, 0.000: library has no initializer pins2lts-mc, 0.000: loading model GAL pins2lts-mc, 0.001: completed loading model GAL pins2lts-mc, 0.001: There are 102 state labels and 1 edge labels pins2lts-mc, 0.001: State length is 151, there are 101 groups pins2lts-mc, 0.001: Running bfs using 1 core (sequential) pins2lts-mc, 0.001: Using a non-indexing tree table with 2^27 elements pins2lts-mc, 0.001: Successor permutation: none pins2lts-mc, 0.001: Global bits: 0, count bits: 0, local bits: 0 pins2lts-mc, 0.424: 4 levels 1000 states 96109 transitions pins2lts-mc, 0.636: 4 levels 2000 states 192109 transitions pins2lts-mc, 0.941: 4 levels 4000 states 384109 transitions pins2lts-mc, 1.560: 5 levels 8000 states 762113 transitions pins2lts-mc, 2.650: 5 levels 16000 states 1514113 transitions pins2lts-mc, 4.426: 5 levels 32000 states 3018113 transitions pins2lts-mc, 7.753: 5 levels 64000 states 6026113 transitions pins2lts-mc, 14.378: 5 levels 128000 states 12042113 transitions pins2lts-mc, 27.664: 6 levels 256000 states 23885717 transitions pins2lts-mc, 54.754: 6 levels 512000 states 47437717 transitions pins2lts-mc, 113.024: 6 levels 1024000 states 94541717 transitions pins2lts-mc, 227.712: 6 levels 2048000 states 188749717 transitions pins2lts-mc, 239.826: Error: tree leafs table full! Change -s/--ratio. pins2lts-mc, 239.863:  pins2lts-mc, 239.863:  pins2lts-mc, 239.863: Explored 2066447 states 190446841 transitions, fanout: 92.161 pins2lts-mc, 239.863: Total exploration time 239.860 sec (239.860 sec minimum, 239.860 sec on average) pins2lts-mc, 239.863: States per second: 8615, Transitions per second: 793992 pins2lts-mc, 239.863:  pins2lts-mc, 239.863: Queue width: 8B, total height: 50941943, memory: 388.66MB pins2lts-mc, 239.863: Tree memory: 660.4MB, 13.1 B/state, compr.: 2.2% pins2lts-mc, 239.863: Tree fill ratio (roots/leafs): 39.0%/99.0% pins2lts-mc, 239.863: Stored 101 string chucks using 0MB pins2lts-mc, 239.863: Total memory used for chunk indexing: 0MB pins2lts-mc, 239.863: Est. total memory use: 1049.1MB (~1412.7MB paged-in) Exit code :0 — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or mute the thread.

[yanntm]

ok Thanks Alfons, I'll try 3 or 4 as ratio, then, hoping that's ok for my models

and wait for a patch for the incorrect result issue.

[yanntm]

ok, rather than wait for a patch,

since you seem to agree with diagnosis and treatment,

I built a PR 👍

[Meijuh]

I am closing this issue, because in my opinion it is a duplicate of #135.

[alaarman]

It's not a duplicate

[alaarman]

Fixed in 52e853f

[yanntm]

Awesome thanks Alfons, I'll test this version and remove my patch.