utwente-fmt / ltsmin

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

mcrl2 and state-labels #166

Open jacopol opened 5 years ago

jacopol commented 5 years ago

LTSmin adds guard information as state labels to the LTS, which is fine for internal use. However, these state labels are also exported to ETF (debatable) and GCF (wrong). This blocks generation of aut-files. I.e.: the following is currently not working:

lps2lts-mc abp.lps abp.aut

The work-around is:

lps2lts-mc --procs=1 abp.lps abp.gcf ltsmin-convert --rdwr --filter=action_labels abp.gcf abp.aut

(see the next issue for --procs=1, but I'm keeping these issues separate)