ltsmin
ltsmin copied to clipboard
pnml2lts-mc guesses wrong ratio
LTSmin chooses --ratio=2 on default, and produces an error with the following command (this happens on caserta; on westervlier the command is going fine).
pnml2lts-mc --threads=64 --por --ltl=LTL/problem101_1.ltl --edge-label=name problem101.pnml pnml2lts-mc --threads=64 --por --ltl=LTL/problem101_1.ltl --edge-label=name --ratio=3 problem101.pnml still produces an error. Finally, pnml2lts-mc --threads=64 --por --ltl=LTL/problem101_1.ltl --edge-label=name --ratio=4 problem101.pnml works. This is inconvenient, and it is different on different machines, so hard to write correct scripts. Rather than raising an error, LTSmin should figure out the correct ratio automatically. End users are not aware of --ratio.
Of course, if the users specifies a wrong --ratio manually, the tool should produce an error indeed.
Command line: pnml2lts-mc --threads=64 --por --ltl=LTL/problem101_1.ltl --edge-label=name problem101.pnml pnml2lts-mc( 0/64): Loading model from problem101.pnml pnml2lts-mc( 0/64): Edge label is name pnml2lts-mc( 0/64): Petri net has 47 places, 45 transitions and 110 arcs pnml2lts-mc( 0/64): Petri net problem101.dot analyzed pnml2lts-mc( 5/64): No maybe-coenabled matrix found. Turning off NESs from NDS+MC. pnml2lts-mc( 5/64): LTL layer: formula: LTL/problem101_1.ltl pnml2lts-mc( 5/64): buchi has 3 states pnml2lts-mc( 0/64): There are safe places pnml2lts-mc( 0/64): Loading Petri net took 0.320 real 16.520 user 0.030 sys pnml2lts-mc( 0/64): Initializing POR dependencies: labels 47, guards 47 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), file treedbs-ll.c, line 492: assertion "satellite_bits + 2 * (size-ratio) <= 64" failed: Tree table size and satellite bits (4) too large or ratio too low (2). Exit [255]