utwente-fmt / ltsmin

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

Segmentation Fault in pnml2lts-mc #215

Open jacopol opened 9 months ago

jacopol commented 9 months ago

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:

image

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 commented 9 months ago

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 commented 9 months ago

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 commented 9 months ago

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 commented 9 months ago

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