
% ----------------------------------------------------------------------

/*
	TOY CCS
	Simple CCS with no value passing, choice or relabeling.
*/

% ----------------------------------------------------------------------

% Meta-ops:
:- op(1000,fx,run).
:- op(900,xfx,==>).	% action
:- op(900,xfx,===>).	% actions till stop

% Ops:
:- op(700,xfy,&).	% concurrent composition
:- op(600,xfy,?).	% input
:- op(600,xfy,!).	% output

% ----------------------------------------------------------------------

run(P)				:-	print(P), nl, P ===> _ .

P ===> End			:-	act(P,Comm,R),
						print('	'), print(Comm), nl,
						print('=> '), print(R), nl,
					R ===> End.

P ===> P			:-	dead(P).

% ----------------------------------------------------------------------

Process ==> NewProcess		:-	act(Process, _, NewProcess).

% ----------------------------------------------------------------------

act(P1&Q1, Comm, P2&Q2)			:-	out(P1,Comm,P2),
						in(Q1,Comm,Q2).

act(P1&Q1, Comm, P2&Q2)			:-	in(P1,Comm,P2),
						out(Q1,Comm,Q2).

act(P&Process, Comm, P&NewProcess)	:-	act(Process, Comm, NewProcess) .

act(Process&P, Comm, NewProcess&P)	:-	act(Process, Comm, NewProcess) .

% ----------------------------------------------------------------------

dead(P)					:-	act(P,_,_), !, fail.
dead(_).

% ----------------------------------------------------------------------

out(Channel!Process, Channel, Process).

out(P & Q, Comm, P & R)		:- out(Q, Comm, R).
out(P & Q, Comm, R & Q)		:- out(P, Comm, R).

% ----------------------------------------------------------------------

in(Channel?Process, Channel, Process).

in(P & Q, Comm, P & R)		:- in(Q, Comm, R).
in(P & Q, Comm, R & Q)		:- in(P, Comm, R).

% ----------------------------------------------------------------------


test :- run
	p!a!b!v!nil & p!b!a!v!nil & p?v?p?v?nil & a?a?a?a?nil & b?b?b?b?nil.



