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

--filter=action_labels #192

Open jacopol opened 3 years ago

jacopol commented 3 years ago

The option --filter is described in the manpage, but it is not clear that you can give it value "action_labels".

This option is currently necessary, since LTSmin adds the guards in a specification as state labels. These state labels also occur in the generated state space by default, blocking ltsmin-reduce. This mainly affects mcrl2 users that want to generate and minimize a state space.

Ideally, lps2lts-mc should not write the state labels that are generated internally by default.