Skip to content

CIF to mCRL2: don't generate empty process

For this CIF specification:

automaton a:
  disc int[0..5] x;
  location:
    initial;
    marked x = 3;
end

CIF to mCRL2 with -v '' (and after #353 (closed) also with -a0) generates:

% Generated by CIF to mCRL2.

% Process for behavior of the CIF specification.
proc P(
    a'x': Int
) =
;

% Initialization.
init P(0);

This is an invalid mCRL2 model.