search

mCRL2org / mCRL2

The Git repository for the mCRL2 toolset.
https://mcrl2.org/
Boost Software License 1.0
88 stars 36 forks source link

ltsview crashes on tictactoe.fsm #1431

Open jgroote opened 7 years ago

jgroote commented 7 years ago

Issue migrated from trac ticket # 1430

component: Core: Parse Library | priority: major

2017-09-06 14:47:27: @jgroote created the issue

In the enclosed file tictactoe.mcrl2 when applying the following commands ltsview crashes. Note that if a .lts file is generated no crash takes place on tictactoe.lts. If the .fsm file is translated to a .lts file no crash occurs.

mcrl22lps -v tictactoe.mcrl2 tictactoe.lps lps2lts -v -rjittyc tictactoe.lps tictactoe.fsm ltsview tictactoe.fsm

The tictactoe file stems directly from the example directory.

jgroote commented 7 years ago

2017-09-06 14:48:29: @jgroote uploaded file tictactoe.mcrl2 (1.3 KiB)

jgroote commented 7 years ago

2017-09-06 16:17:09: @tneele commented

I cannot reproduce this problem on Ubuntu 17.04. Can you maybe attach the fsm file as well?

jgroote commented 7 years ago

2017-09-07 17:53:49: anonymous commented

The .fsm file is has the following size and is too big to be uploaded:

1331642 Sep 6 14:31 tictactoe.fsm

jgroote commented 7 years ago

2017-09-08 12:03:14: @jgroote commented

This appears to be a problem that is specific for MacOsX. OS: OsX 10.12.6. Qt 5.7.

jgroote commented 7 years ago

2017-09-09 17:38:21: anonymous changed owner from jfg to wieger

jgroote commented 7 years ago

2017-09-09 17:38:21: anonymous changed component from ltsview to Core: Parse Library

jgroote commented 7 years ago

2017-09-09 17:38:21: anonymous commented

Further analysis shows that the problem is caused by the .fsm parser. At line 86 of parse_parameter the input consists of a domain of over 5000 elements (namely all potential positions of of the pieces in tic-tac-toe). The size of the input string is 793221 characters long. Apparently, this is too much to swallow for Boost's regexp with the relatively small stack that processes have on the mac.

As this is not untypical .fsm input, and the structure of the input is very simple, it is advisable to replace this algorithm by one that can deal with a smaller stack, probably, by splitting the input string first into the appropriate subdomains.

Note that this input is not problematic in tools that do not use Qt, such as ltsinfo. Apparently the stack of such tools is bigger on MacOsX.