search

utwente-fmt / ltsmin

The LTSmin model checking toolset
http://ltsmin.utwente.nl
BSD 3-Clause "New" or "Revised" License
52 stars 30 forks source link

pnml2lts-mc writing a trace goes wrong #137

Closed jacopol closed 6 years ago

jacopol commented 7 years ago

(on weleveld, ltsmin-3.0.git/next from July 13/2017) (this run went wrong, but there also correct runs; race condition?) problem109.pnml is from RERS2017. problem109_7.ltl: ( (!(action == "c14_t4") W (action == "c13_t3")) )

Command line: pnml2lts-mc problem109.pnml --ltl=LTL/problem109_7.ltl --strategy=cndfs --edge-label=name --trace=POR/problem109_7.gcf --por --ratio=3 pnml2lts-mc( 0/64): Loading model from problem109.pnml pnml2lts-mc( 0/64): Edge label is name pnml2lts-mc( 0/64): Petri net has 236 places, 246 transitions and 596 arcs pnml2lts-mc( 0/64): Petri net problem109.dot analyzed pnml2lts-mc(19/64): No maybe-coenabled matrix found. Turning off NESs from NDS+MC. pnml2lts-mc(19/64): LTL layer: formula: LTL/problem109_7.ltl pnml2lts-mc(19/64): buchi has 2 states pnml2lts-mc( 0/64): There are safe places pnml2lts-mc( 0/64): Loading Petri net took 0.640 real 24.460 user 2.320 sys pnml2lts-mc( 0/64): Initializing POR dependencies: labels 236, guards 236 pnml2lts-mc( 0/64): Weak Buchi automaton detected, adding non-accepting as progress label. pnml2lts-mc( 0/64): Forcing use of the an ignoring proviso (cndfs) pnml2lts-mc( 0/64): There are 238 state labels and 1 edge labels pnml2lts-mc( 0/64): State length is 237, there are 249 groups pnml2lts-mc( 0/64): Running cndfs using 64 cores pnml2lts-mc( 0/64): Using a tree table with 2^33 elements pnml2lts-mc( 0/64): Successor permutation: dynamic pnml2lts-mc( 0/64): Visible groups: 2 / 249, labels: 0 / 238 pnml2lts-mc( 0/64): POR cycle proviso: cndfs (ltl) pnml2lts-mc( 0/64): Global bits: 2, count bits: 2, local bits: 0 pnml2lts-mc(42/64): [Blue] ~48 levels ~6400 states ~9152 transitions pnml2lts-mc( 0/64):
pnml2lts-mc( 0/64): Accepting cycle FOUND at depth 71! pnml2lts-mc( 0/64):
pnml2lts-mc( 0/64): Writing trace to POR/problem109_7.gcf pnml2lts-mc( 0/64), error : no matching transition found for 37 Exit [255]

Meijuh commented 7 years ago

@alaarman can you look into this?

alaarman commented 7 years ago

@Meijuh PNML still crashes with some bus error. You said you had some fix so that it also works on OSX? I cannot find your reply about it.

alaarman commented 7 years ago

@Meijuh ?

Meijuh commented 7 years ago

Yes it is in the utwente-fmt next branch, fixed with 22744b9a3a62cb2eca30dbd917649c981928d82e and 7b3a6348cf97631671d47150eb908898afe8697b.

alaarman commented 6 years ago

The combination with POR and action-based LTL is disabled in LTSmin 3.0 (it was not supported). I cannot reproduce this without POR (no counter example is found). Please rereport if you can.