%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% End of autogenerated specification %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%% Initial mCRL2 process for verifying a multiparty session type contexts,
%%% using the definitions in mpst-preamble.mcrl2.
%%%
%%% NOTE: the following requires the "context" process to be defined
init allow({i, o, t}, comm( {i|o->t},
  context
));