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 hangs on TRUE formulas #130

Closed jacopol closed 6 years ago

jacopol commented 7 years ago

pnml2lts-mc correctly detects that the Büchi automata is empty, so the formula must be equivalent to TRUE. However, then pnml2lts-mc doesn't exit with the proper code [0], but just hangs until the timeout kicks in.

Command line: pnml2lts-mc problem110.pnml --ltl=LTL/problem110_12.ltl --edge-lab el=name --trace=LTL/problem110_12.gcf pnml2lts-mc( 0/48): Loading model from problem110.pnml pnml2lts-mc( 0/48): Edge label is name pnml2lts-mc( 0/48): Petri net has 200 places, 4315 transitions and 17252 arcs pnml2lts-mc( 0/48): Petri net problem110.dot analyzed pnml2lts-mc( 0/48): There are safe places pnml2lts-mc( 0/48): Loading Petri net took 4.980 real 13.190 user 27.130 sys pnml2lts-mc( 6/48): LTL layer: formula: LTL/problem110_12.ltl pnml2lts-mc( 6/48): Empty buchi automaton. pnml2lts-mc( 6/48): The property is TRUE. Killed [24]

The pnml model can be found at http://www.rers-challenge.org/2017/problems/Parallel/ParallelRERS2017_version2.zip

The property was: LTL/problem110_12.ltl: ( (!(action == "a32_SIGHUP") W (action == "a32_SIGHUP")) )

(version: ltsmin "3.0" github/next d.d. 12 juli 2017, run on westervlier)

alaarman commented 6 years ago

Fixed in 56ad59698d30a24e949edc6430d74201f02fca80