Minimal mCRL2 examples fail

[zwergziege]

I'm currently toying with LTSmin and mCRL2. When running some small examples I encountered crashes of lps2lts-seq when running the following example:

act a;
proc P = a . P;

init P;

This works:

act a;
proc P(x: Bool) =
    a . P(x) +
    a . P(!x);

init P(true);

And this also

act a, b;
proc P = a . b . P;

init P;

Here is the stack trace

lps2lts-seq: mCRL2 language module initialized
lps2lts-seq: Loading model from tmp/out.lps
lps2lts-seq: mCRL2 rewriter: jitty
lps2lts-seq: Writing output to ./tmp/out.dir
lps2lts-seq: keeping true
lps2lts-seq: keeping action_labels
*** 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: ./LTSmin/bin/lps2lts-seq(HREprintStack+0x18) [0x6617d8]
  1: ./LTSmin/bin/lps2lts-seq() [0x661866]
  2: /lib/x86_64-linux-gnu/libc.so.6(+0x42520) [0x7ebef2642520]
  3: ./LTSmin/bin/lps2lts-seq() [0x5a3557]
  4: ./LTSmin/bin/lps2lts-seq(TreeDBScreate+0x17e) [0x5ac1fe]
  5: ./LTSmin/bin/lps2lts-seq(main+0x11bb) [0x54fdfb]
  6: /lib/x86_64-linux-gnu/libc.so.6(+0x29d90) [0x7ebef2629d90]
  7: /lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x80) [0x7ebef2629e40]
  8: ./LTSmin/bin/lps2lts-seq() [0x55569f]

This could of course also be a bug in the mCRL2 toolkit, of which I'm using 201808.0.7c1932b005 (Release). If this is the case and the bug has already been fixed, consider this a feature request to support a newer version of mCRL2 ;)

[mlaveaux]

One of the developers of mCRL2 here. I don't know about this specific issue, because that is a quite old version of the mCRL2 toolset. However, we have a Dockerfile in our repository for a specific ltsmin commit from the master branch that works using the latest release of the mCRL2 toolset, being 202507. This Dockerfile should give some hint of how to build ltsmin yourself if that is desired.

Another way would be to use Docker directly. Unfortunately, I inadvertently broke this Dockerfile when upgrading it to fedora 42, but if you check out our release-202507 branch, change the first line of the Dockerfile back to fedora:40 and then run docker build -f scripts/docker/ltsmin/Dockerfile . from the base directory then it should work.

If you need help setting it up feel free to reach out.

[jacopol]

Thanks Maurice, makes sense to try this in your Dockerfile. I also started a Docker for LTSmin some time ago, but it is not yet finished and it doesn't contain mcrl2 yet.