LTL non deterministic behavior.

[yanntm]

Hi LTSmin team,

So, I've come up with this example that is a bit miserable : sometimes yes, sometimes no.

I progressively dropped flags like : --threads=8 and -p (POR) without getting deterministic results.

So,
Correct answer is : product is non empty; there are counter examples.

Sometimes, LTSmin (pns2lts-mc more precisely) agrees and finds it : trace

Sometimes not : trace1.txt trace2.txt

trace1 :
...
pins2lts-mc-linux64, 24.535: Empty product with LTL!
pins2lts-mc-linux64, 24.535:
pins2lts-mc-linux64, 24.538:
pins2lts-mc-linux64, 24.538: Explored 88320 states 255795 transitions, fanout: 2.896
pins2lts-mc-linux64, 24.542: Total exploration time 22.570 sec (22.570 sec minimum, 22.570 sec on average)
pins2lts-mc-linux64, 24.545: States per second: 3913, Transitions per second: 11333
pins2lts-mc-linux64, 24.545:
pins2lts-mc-linux64, 24.546: State space has 88320 states, 1038 are accepting

trace2 :
...
pins2lts-mc-linux64, 22.995: Empty product with LTL!
pins2lts-mc-linux64, 22.995:
pins2lts-mc-linux64, 22.998:
pins2lts-mc-linux64, 22.998: Explored 88320 states 255795 transitions, fanout: 2.896
pins2lts-mc-linux64, 23.002: Total exploration time 22.500 sec (22.500 sec minimum, 22.500 sec on average)
pins2lts-mc-linux64, 23.004: States per second: 3925, Transitions per second: 11369
pins2lts-mc-linux64, 23.006:
pins2lts-mc-linux64, 23.006: State space has 88320 states, 987 are accepting

So, it's not tagging the same states as accepting ?
1038 are accepting vs 987 are accepting
in these two (supposedly exhaustive) runs.

In other cases it finds a trace almost immediately (trace3):
pins2lts-mc-linux64, 0.021: Accepting cycle FOUND at depth 83!
pins2lts-mc-linux64, 0.021:
pins2lts-mc-linux64, 0.021:
pins2lts-mc-linux64, 0.021: Explored 787 states 1672 transitions, fanout: 2.125
pins2lts-mc-linux64, 0.021: Total exploration time 0.010 sec (0.010 sec minimum, 0.010 sec on average)
pins2lts-mc-linux64, 0.021: States per second: 78700, Transitions per second: 167200
pins2lts-mc-linux64, 0.021:
pins2lts-mc-linux64, 0.021: State space has 990 states, 17 are accepting

I attach the traces and input files.

I build the inputs to LTSMin with :
Running compilation step : 'gcc' '-c' '-I./include/' '-I.' '-std=c99' '-fPIC' '-O0' 'model.c'
Compilation finished in 168 ms.
Running link step : 'gcc' '-shared' '-o' 'gal.so' 'model.o'
Link finished in 16 ms.
Running LTSmin : 'pins2lts-mc-linux64' './gal.so' '--threads=8' '-p' '--pins-guards' '--when' '--hoa' './aut.hoa' '--buchi-type=spotba'

---

Fortunately, pins2lts-seq does not find empty products, so I'm reverting my calls to use "seq" rather than mc.

The example is not super small, but not huge either.

I'm only worried its my fault in some way, this is indeed the HOA format input I coded with help from Alfons a while back.

traces.zip

[jacopol]

Hi Yann, it looks pretty weird indeed, but I had no time to study it. Would the result of adding --threads=1 be deterministic? (that would mean it is really a concurrency bug).
Also, out of curiosity, on which hardware did you run this? In particular, is it a CPU with a weak(er) memory model?