%%% Representation of multiparty session type contexts as mCRL2 processes
%%%
%%% Copyright 2018 Alceste Scalas <alceste.scalas @ imperial.ac.uk>
%%% Released under the MIT License: https://opensource.org/licenses/MIT

%%% Sessions
sort Session;
cons s: Nat -> Session;

var x, y: Nat;
eqn s(x) == s(y) = x == y;

%%% Roles
sort Role;
cons r: Nat -> Role;

var x, y: Nat;
eqn r(x) == r(y) = x == y;

%%% Message labels
sort Message;
cons m: Nat -> Message;

var x, y: Nat;
eqn m(x) == m(y) = x == y;

%%% Payload types
sort Payload;
cons p: Nat -> Payload;

var x, y: Nat;
eqn p(x) == p(y) = x == y;

% Commonly-used payload types
map pEnd, pBool, pInt, pString, pUnit: Payload;
eqn pEnd    = p(0);
    pBool   = p(1);
    pInt    = p(2);
    pString = p(3);
    pUnit   = p(4);

%%% Actions
act o: Session # Role # Role # Message # Payload; % Output from 1st to 2nd role
    i: Session # Role # Role # Message # Payload; % Input from 1st role by 2nd
    t: Session # Role # Role # Message # Payload; % Communication: 1st to 2nd

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Beginning of autogenerated specification %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%