Too large state spaces generated for mCRL2 models with global variables

[jkeiren]

mCRL2 models generated by mcrl22lps may introduce global variables. When generating the LTS using lps2lts-* tools, these models result in a state space that is larger than strictly needed.

The underlying reason for this is that, in the initial state, a poor choice is made for the global variables, such that, later in the state space generation process, the initial state is not revisited. In stead, a strongly bisimilar copy of the initial state is reached.

To reproduce:

$ mcrl22lps abp.mcrl2 abp.lps
$ lps2lts-seq abp.lps
(...)
lps2lts-seq: state space 46 levels, 143 states 174 transitions
$ lps2lts -v abp.lps
(...)
done with state space generation (20 levels, 74 states and 92 transitions)

When the LPS is generated without global variables, the state space is as expected, so this can be used as a workaround as follows:

$ mcrl22lps -f abp.mcrl2 abp.lps
$ lps2lts-seq abp.lps
(...)
lps2lts-seq: state space 20 levels, 74 states 92 transitions
$ lps2lts -v abp.lps
(...)
done with state space generation (20 levels, 74 states and 92 transitions)

The problem also appears with other tools such as lps2lts-sym.