alaarman
commented
6 years ago fixed in 7f8601079350fc1d5290379b84f7723c09817e6c
Closed jacopol closed 6 years ago
alaarman
commented
6 years ago fixed in 7f8601079350fc1d5290379b84f7723c09817e6c
The following run fails and I suspect that this is due to a race condition in adding edge labels in the action-label-table. The problem is only triggered on some runs, so may be not obvious to reproduce.
1) this error is spurious, actually this action label does exist in the model 2) there is an assertion violation, that might be related and could point to the source of the problem.
The model problem104.pnml can be found at http://www.rers-challenge.org/2017/problems/Parallel/ParallelRERS2017_version2.zip
The formulas are transformed to LTS syntax: problem104_18.ltl: ( (((action == "c3_t0") -> (!(action == "c1_t5") U (action == "c6_t2__c7_t7"))) W ((action == "c3_t6") || (action == "c7_t3"))) )
Command line: pnml2lts-mc problem104.pnml --ltl=LTL/problem104_18.ltl --strategy =cndfs --edge-label=name --trace=LTL/problem104_18.gcf pnml2lts-mc( 0/16): Loading model from problem104.pnml pnml2lts-mc( 0/16): Edge label is name pnml2lts-mc( 0/16): Petri net has 114 places, 122 transitions and 282 arcs pnml2lts-mc( 0/16): Petri net problem104.dot analyzed pnml2lts-mc( 1/16): LTL layer: formula: LTL/problem104_18.ltl pnml2lts-mc( 1/16): buchi has 3 states pnml2lts-mc( 8/16), file set-ll.c, line 117: assertion "slab->cur_len != SIZE_MAX" failed: Failed to pass length via static. pnml2lts-mc( 1/16), error : There is no group that can produce edge '"c3_t0"'