pnml2lts-mc DFSFIFO fails to compute counterexample

pnml2lts-mc automatically deduces that DFSFIFO can be used (although I didn't ask for it). It finds the accepting cycle, but it fails to create the counterexample and exits with exit code [255] (error). I don't know why. It should produce a counterexample and exit with [1]

It seems that DFSFIFO counterexample generation is not yet mature, so LTSmin shouldn't automatically switch to DFSFIFO, should it?

Command line: pnml2lts-mc problem101.pnml --edge-label=name --ltl=LTL/problem101_5.ltl --trace=101_5.gcf pnml2lts-mc( 0/48): Loading model from problem101.pnml pnml2lts-mc( 0/48): Edge label is name pnml2lts-mc( 0/48): Petri net has 47 places, 45 transitions and 110 arcs pnml2lts-mc( 0/48): Petri net problem101.dot analyzed pnml2lts-mc( 0/48): There are safe places pnml2lts-mc(27/48): LTL layer: formula: LTL/problem101_5.ltl pnml2lts-mc( 0/48): Loading Petri net took 1.360 real 58.560 user 0.080 sys pnml2lts-mc(27/48): buchi has 3 states pnml2lts-mc( 0/48): Weak Buchi automaton detected, adding non-accepting as progress label. pnml2lts-mc( 0/48): DFS-FIFO for weak LTL, using special progress label 48 pnml2lts-mc( 0/48): There are 49 state labels and 1 edge labels pnml2lts-mc( 0/48): State length is 48, there are 51 groups pnml2lts-mc( 0/48): Running dfsfifo using 48 cores pnml2lts-mc( 0/48): Using a tree table with 2^31 elements pnml2lts-mc( 0/48): Successor permutation: rr pnml2lts-mc( 0/48): Global bits: 2, count bits: 0, local bits: 0 pnml2lts-mc(40/48):
pnml2lts-mc(40/48): Non-progress cycle FOUND at depth 13! pnml2lts-mc(40/48):
pnml2lts-mc(40/48), error : Trace length 10x longer than initially found trace. Giving up. Exit [255]

The model can be found at http://www.rers-challenge.org/2017/problems/Parallel/ParallelRERS2017_version2.zip The formula was: ( []((action == "c1_t3") -> [](!(action == "c3_t2"))) )

utwente-fmt / ltsmin

pnml2lts-mc DFSFIFO fails to compute counterexample #131