Segmentation Fault in pnml2lts-mc

[jacopol]

erk1.pnml.txt
Dear LTSmin Support Team,
I hope this email finds you well. I am writing to report an issue that I encountered while using the pnml2lts-mc tool from the LTSmin 3.0.2 package. The tool was executed with the command "./pnml2lts-mc erk1.pnml --labels," and it produced detailed output, unfortunately, it terminated with a segmentation fault.
Below is a summary of the output:

As suggested, I am reporting this issue to seek assistance in understanding the root cause and finding a resolution. I have included all relevant information preceding the segmentation fault. Please find additional details below:
• Package: LTSmin 3.0.2
To assist you in reproducing the issue, I have attached the PNML file (erk1.pnml) used for the analysis.
I appreciate your prompt attention to this matter. If you require any further information or clarification, please do not hesitate to contact me.
Thank you for your assistance.
Best regards,

Sawsen Khilfa
3rd year Phd Student at Sup'Com

[jacopol]

Hi, that doesn’t look good, we’ll have to look into this.

At the moment, I can just confirm that I see the same behavior on Ubuntu.
Using the symbolic tool seems to work fine though, so maybe this could be your workaround?

pnml2lts-sym erk1.pnml –labels

[jacopol]

Follow-up problem when using LTL model checking: pnml2lts-mc --ltl 'action=="r1" -> (action=="r2" U action=="r3")' erk1.pnml
leads to:

$ pnml2lts-mc --ltl 'action=="r1" -> (action=="r2" U action=="r3")' erk1.pnml
pnml2lts-mc( 0/ 8): Loading model from erk1.pnml
pnml2lts-mc( 0/ 8): Edge label is id
pnml2lts-mc( 0/ 8): Petri net has 11 places, 11 transitions and 34 arcs
pnml2lts-mc( 0/ 8): Petri net ERK-PT-000001 analyzed
pnml2lts-mc( 0/ 8): There are safe places
pnml2lts-mc( 0/ 8): Loading Petri net took 0.010 real 0.000 user 0.050 sys
pnml2lts-mc( 2/ 8): LTL layer: formula: action=="r1" -> (action=="r2" U action=="r3")
pnml2lts-mc( 2/ 8): "action=="r1" -> (action=="r2" U action=="r3")" is not a file, parsing as formula...
pnml2lts-mc( 2/ 8): Using LTSmin LTL semantics
pnml2lts-mc( 0/ 8): Weak Buchi automaton detected, adding non-accepting as progress label.
*** segmentation fault ***

Please send information on how to reproduce this problem to:
         ltsmin-support@lists.utwente.nl
along with all output preceding this message.
In addition, include the following information:
Package: ltsmin 3.0.2
Stack trace:
  0: pnml2lts-mc() [0x44b5b8]
  1: pnml2lts-mc() [0x44b646]
  2: /lib/x86_64-linux-gnu/libpthread.so.0(+0x14420) [0x7f5236eab420]
  3: pnml2lts-mc() [0x42df93]
  4: pnml2lts-mc() [0x42e03f]
  5: pnml2lts-mc() [0x4525ca]
  6: pnml2lts-mc() [0x4167e0]
  7: pnml2lts-mc() [0x466b92]
  8: /lib/x86_64-linux-gnu/libpthread.so.0(+0x8609) [0x7f5236e9f609]
  9: /lib/x86_64-linux-gnu/libc.so.6(clone+0x43) [0x7f5236c75133]

[jacopol]

A quick work around is to use the sequential tool:

$ pnml2lts-seq --ltl 'action=="r1" -> (action=="r2" U action=="r3")' erk1.pnml
pnml2lts-seq: Loading model from erk1.pnml
pnml2lts-seq: Edge label is id
pnml2lts-seq: Petri net has 11 places, 11 transitions and 34 arcs
pnml2lts-seq: Petri net ERK-PT-000001 analyzed
pnml2lts-seq: There are safe places
pnml2lts-seq: Loading Petri net took 0.000 real 0.000 user 0.000 sys
pnml2lts-seq: LTL layer: formula: action=="r1" -> (action=="r2" U action=="r3")
pnml2lts-seq: "action=="r1" -> (action=="r2" U action=="r3")" is not a file, parsing as formula...
pnml2lts-seq: Using LTSmin LTL semantics
pnml2lts-seq: buchi has 3 states
pnml2lts-seq: Weak Buchi automaton detected, adding non-accepting as progress label.
pnml2lts-seq: There are 13 state labels and 1 edge labels
pnml2lts-seq: State length is 12, there are 11 groups
pnml2lts-seq: Running scc search strategy
pnml2lts-seq: Using a tree for state storage
pnml2lts-seq: Accepting cycle FOUND!
pnml2lts-seq: exiting now

[jacopol]

To get a concrete counter example, use:

pnml2lts-seq --ltl 'action=="r1" -> (action=="r2" U action=="r3")' erk1.pnml --trace error.gcf
ltsmin-printtrace error.gcf