(Possibly?) Unsound Partial Order Reduction

[sjudson]

I was testing a variant of the BEEM model checking benchmarks using dve2lts-seq and found an inconsistency: the model checking fails when run naively, but then passes when partial order reduction is added.

Specifically I am running iprotocol.6.dev using the negation of the prop3:

! ([] (<> (Consumer == "consume")))

which rewrites to

<> ([] !(Consumer == "consume"))

The relevant outputs are, first without partial order reduction:

$ divine compile -l ../examples/iprotocol.6.dve && dve2lts-seq --strategy=scc --ltl ../examples/iprotocol.prop3.tt.ltl iprotocol.6.dve2C
dve2lts-seq: Precompiled divine module initialized
dve2lts-seq: Loading model from iprotocol.6.dve2C
dve2lts-seq: LTL layer: formula: ../examples/iprotocol.prop3.tt.ltl
dve2lts-seq: Using Spin LTL semantics
dve2lts-seq: buchi has 2 states
dve2lts-seq: There are 45 state labels and 0 edge labels
dve2lts-seq: State length is 38, there are 39 groups
dve2lts-seq: Running scc search strategy
dve2lts-seq: Using a tree for state storage
dve2lts-seq: Accepting cycle FOUND!
dve2lts-seq: exiting now

and then with partial order reduction:

$ divine compile -l ../examples/iprotocol.6.dve && dve2lts-seq --por=heur --strategy=scc --proviso=stack --ltl ../examples/iprotocol.prop3.tt.ltl iprotocol.6.dve2C
dve2lts-seq: Precompiled divine module initialized
dve2lts-seq: Loading model from iprotocol.6.dve2C
dve2lts-seq: Initializing POR dependencies: labels 44, guards 44
dve2lts-seq: LTL layer: formula: ../examples/iprotocol.prop3.tt.ltl
dve2lts-seq: Using Spin LTL semantics
dve2lts-seq: buchi has 2 states
dve2lts-seq: There are 45 state labels and 0 edge labels
dve2lts-seq: State length is 38, there are 39 groups
dve2lts-seq: Running scc search strategy
dve2lts-seq: Using a tree for state storage
dve2lts-seq: Visible groups: 3 / 39, labels: 0 / 45
dve2lts-seq: POR cycle proviso: stack (ltl)
dve2lts-seq: explored 1860 levels ~100000 states ~134354 transitions
dve2lts-seq: explored 1860 levels ~200000 states ~270743 transitions
dve2lts-seq: explored 1980 levels ~400000 states ~542750 transitions
dve2lts-seq: explored 2100 levels ~800000 states ~1089019 transitions
dve2lts-seq: explored 2220 levels ~1600000 states ~2183360 transitions
dve2lts-seq: explored 2340 levels ~3200000 states ~4374173 transitions
dve2lts-seq: explored 2460 levels ~6400000 states ~8756817 transitions
dve2lts-seq: Empty product with LTL!
dve2lts-seq: state space 2460 levels, 6445773 states 8823715 transitions

Digging in a bit more, the (an?) issue seems to be this state:

(0, 1, 8, 1, 8, 0, 8, 4, 9, 8, 8, 5, 0, 8, 0, 8, 8, 0, 0, 1, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1)

That s[3] = 1 means that Consumer == "consume", and the state self loops, creating a trace that never reaches the point thatConsumer != "consume" as required.

Is this an issue with how I'm using the tool APIs, or is the partial order reduction here unsound?

EDIT: could this be relevant: What’s Wrong with On-the-Fly Partial Order Reduction?

[alaarman]

It sounds like the scc algorithm in the sequential tool does not correctly report to the cycle proviso to the PINS layer. Upon detecting this cycle it should signify arg->proviso = 1 so the POR algorithm does not reduce for that state.

I don't think Siegel's paper is relevant as I recall that they author tried LTSmin with a counterexample but the bug did not appear to be implementation.

[jacopol]

Thanks Alfons! Is there a simple fix?