Pretty printing an LPS creates an invalid mCRL2 specification whenever there is an action is named P
mlaveaux opened this issue · 0 comments
mlaveaux commented
The following mCRL2 specification:
act P;
init P.delta;
generates the following pretty printed linear process, which is invalid due to the double declaration of P as both an action and a process:
act P;
proc P(s1: Pos) =
(s1 == 2) ->
P .
P(s1 = 1)
+ delta;
init P(2);
This the following commands fail:
mcrl22lps why.mcrl2 | lpspp | mcrl22lps
declaration of both process and action P