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:
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?
I was testing a variant of the BEEM model checking benchmarks using
dve2lts-seqand 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:which rewrites to
The relevant outputs are, first without partial order reduction:
and then with partial order reduction:
Digging in a bit more, the (an?) issue seems to be this state:
That
s[3] = 1means thatConsumer == "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?