search

mCRL2org / mCRL2

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

lps2lts produces invalid .aut file when using bithashing #1026

Closed jgroote closed 12 years ago

jgroote commented 12 years ago

Issue migrated from trac ticket # 1024

component: lps2lts | priority: minor | resolution: fixed

2012-06-04 11:51:24: scranen@win.tue.nl created the issue

When using bithashing, the state indices in generated .aut files are incorrect. E.g., when generating a random trace using the following command:

$ lps2lts --todo-max=1 -b test.lps test.aut

Viewing the resulting .aut file gives the following error:

$ ltsgraph-qt test.aut 
[11:46:50 error]   cannot parse AUT input (invalid transition at line 2; state index (47267995) higher than maximum (5) given by header).
jgroote commented 12 years ago

2012-06-04 14:29:24: mcrl2@ruudkoolen.nl changed status from new to accepted

jgroote commented 12 years ago

2012-06-04 14:29:24: mcrl2@ruudkoolen.nl changed owner from jfg to s051072

jgroote commented 12 years ago

2012-06-07 11:57:48: mcrl2@ruudkoolen.nl changed status from accepted to assigned

jgroote commented 12 years ago

2012-06-07 11:57:48: mcrl2@ruudkoolen.nl commented

According to the Aldebaran standard, lps2lts produces correct output; the assumption when parsing .aut files that state numbers are smaller than the number of states is incorrect. Fixing this in lps2lts is impossible, as this requires too much memory.

jgroote commented 12 years ago

2012-06-25 20:01:25: @jkeiren

jgroote commented 12 years ago

2012-08-17 14:33:28: @jkeiren changed owner from s051072 to jfg

jgroote commented 12 years ago

2012-09-09 23:06:28: @jgroote changed status from assigned to closed

jgroote commented 12 years ago

2012-09-09 23:06:28: @jgroote set resolution to fixed

jgroote commented 12 years ago

2012-09-09 23:06:28: @jgroote commented

Log: Resolves bug #1024.

A .aut file with non consecutive state numbers is now read. This means that a file written using bit hashing can now be read.

The rational test has been adapted. The ltsconvert tests should not be run, because lps2lts does not work. This does not work with -rjittyp. As lps2lts does not work not .aut, .fsm and .lts files are generated. This means ltsinfo, ltsconvert and the ltscompare tests can not be run. For reasons that I do not understand the ltscompare tests are still running on my machine.

Modified: trunk/libraries/lts/source/liblts_aut.cpp trunk/scripts/MCRL2TestTargets.cmake