System too small : padding with a zero ?

[yanntm]

Hi, I'm playing with structural reductions, I saw you were as well Alfons in NFM paper. Anyway, this model CSRepetitions-PT-02 from the MCC reduces to a single place when just looking for deadlocks.

csrepet.zip

Model attached, use

gcc -c -I$LTSMIN/include -I. -std=c99 -fPIC -O3 model.c 
gcc, -shared -o gal.so model.o
$LTSMIN/bin/pins2lts-mc ./gal.so --threads=1 -p --pins-guards --when -d
pins2lts-mc, 0.000: Registering PINS so language module
pins2lts-mc, 0.000, ** error **: Unable to open cgroup memory limit file /sys/fs/cgroup/memory/memory.limit_in_bytes: No such file or directory
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.000: completed loading model GAL
pins2lts-mc, 0.000: Initializing POR dependencies: labels 3, guards 2
pins2lts-mc, 0.000, file treedbs-ll.c, line 488: assertion "nNodes >= 2" failed: Tree vectors too small: 1

So, it's too small, but I'm not sure how to fix this from outside. Ideally, the case could have been detected before building a treedbs and patched by adding a (constant) 0 variable in slot 1 ? i.e. either decorating or modifying the PINS.

I can detect and do this when building my gal.c, but I'm not sure if it's really a clean solution. I'd prefer LTSmin to behave "normally" here I think (and sidestep the problem internally), it's better for both toolsets.

Thank you

yann

By the way, on this very simple example, I still have quite a bit of setup code. Any tips on how I could lighten it ? It's generated obviously so volume is not the first issue. I had to go for sparse matrices otherwise compilation + init time blew up to quadratic. But it could be better (bitsets encoded into the source ?). I have read, write, mayEnable/Disable, coEnab, DNA. Any other info I could compute that could be useful ? Can I improve that code performance-wise/API wise with ltsmin ? More short/long versions of the successor functions perhaps ?

[alaarman]

Should be fixed in bf909b9

The ones you have are the most important ones. NotLeftAccord could offer some better reductions with weak stubborn sets, but I never found much advantage. The transaction reduction discussed in my NFM paper also uses NLA.

About initialization, I wonder whether this is worth optimizing for in the general case. If these time are not negligible then the model checking problem is perhaps trivial? I would rather see less functions and matrices in PINS.

[yanntm]

great, thanks for the fast response, I'll try that patch asap.

Well some models are just huge in terms of e.g. 20k transitions, so going quadratic hurts, when the other tools (lola, tapaal in particular) just start a random thread and find the c-ex very fast, because indeed the problem is pretty trivial. So I think mostly sparse initialization could be nice, in some (most ?) cases. I agree it's not really the hard cases.

[alaarman]

The multi-core backend (without POR) does not need any matrices. So you could also turn them off, what's what e.g. SpinS allows you to do. POR anyway will not help for model checking problems with counter examples (i.e. trivial problems).

[yanntm]

Ok, Thanks for the advice, I guess I'll compromise and place a cutoff for the matrices I'm willing to feed to ltsmin. Above 1M entries or so, I'll try a POR free run without the matrices first.