mCRL2org/mCRL2

Pretty printing an LPS creates an invalid mCRL2 specification whenever there is an action is named P

mlaveaux opened this issue · 0 comments

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