%----------------------------------------------------------------------------
%     ASCII Protocol Diagram
%----------------------------------------------------------------------------

% The main function is showp(S), where
% S is a list of send([A,B,M]) and recv([A,B,M]) terms.
% A is the sender, B is the receiver, M is the message content.

% The display looks best on ground strands. groundp(S,T) can
% be used to turn variables into atoms.

% showp uses built-in SWI term_to_atom and atom_length
% groundp uses built-in SWI gensym, reset_gensym

leftcol('  |').

% shaft is the length of an arrow (less head).
% Increase it to accommodate longer messages.

shaft(36).

% make_arrow(direction,msg,side)

make_arrow(right,M,left) :-
  make_msg(M,' '),
  leftcol(L),write(L),
  shaft(S),
  dashes(S),write('>|'),
  blanks(S),writeln(' |').

make_arrow(left,M,left) :-
  make_msg(M,' '),
  leftcol(L),write(L),
  write('<'),
  shaft(S),dashes(S),
  write('|'),
  blanks(S),
  writeln(' |').

make_arrow(left,M,right) :-
  make_msg(' ',M),
  leftcol(L),write(L),
  shaft(S),
  blanks(S),write(' |'),
  write('<'),dashes(S),
  writeln('|').

make_arrow(right,M,right) :-
  make_msg(' ',M),
  leftcol(L),write(L),
  shaft(S),
  blanks(S),write(' |'),
  dashes(S),writeln('>|').

make_msg(M1,M2) :-  
  leftcol(L),write(L),
  shaft(S),
  place_msg(M1,S,E),
  write('|'),
  S2 is S - E,
  place_msg(M2,S2,_),
  writeln('|').

place_msg(M,S,Ep) :-	% assumes M is an atom, show_msg does this
  atom_length(M,N),
  BN is (S - N + 1)//2,
  line_of(BN,' '),
  write(M),
  AN is S + 1 - BN - N,
  line_of(AN,' '),
  E is N - S - 1,
  posbound(E,Ep).

dashes(N) :- line_of(N,'-').
blanks(N) :- line_of(N,' ').

line_of(1,C) :- !,write(C).
line_of(N,_) :- N < 1,!.
line_of(N,C) :-
  line_of(1,C),
  N1 is N-1,
  line_of(N1,C).

term_length(T,N) :-
  term_to_atom(T,A),
  atom_length(A,N).

posbound(N,0) :- N < 0,!.
posbound(N,N).

make_party(left,A) :-
  term_length(A,N),
  M is 3-(N + 1)//2,
  posbound(M,MP),
  line_of(MP,' '),
  write(A),
  shaft(S),
  M1 is S - N - MP + 4,
  line_of(M1,' '),
  write('|'),
  blanks(S),writeln(' |').

make_party(right,A) :-
  term_length(A,N),
  leftcol(L),write(L),
  shaft(S),
  blanks(S),write(' |'),
  M is S + 1 - N//2,
  line_of(M,' '),
  writeln(A).

% P is a list of send([A,B,M]) and recv([A,B,M]) terms

showp(P) :- 
  showp(P,null,null).

showp([],_LR,_RR).

showp([send([e,e,M])|P],LR,_) :- !,  % e -> e: M
  make_party(right,e),
  show_msg(right,M,right),
  showp(P,LR,e).

showp([recv([e,e,M])|P],LR,_) :- !, 
  make_party(right,e),
  show_msg(right,M,right),
  showp(P,LR,e).

showp([recv([e,B,M])|P],null,null) :- !, % initially
  make_party(left,B),
  show_msg(left,M,left),
  showp(P,B,null).

showp([recv([A,B,M])|P],A,B) :- !, % A -> B: M
  show_msg(right,M,right),
  showp(P,A,B).

showp([recv([A,B,M])|P],B,A) :- !, 
  show_msg(left,M,left),
  showp(P,B,A).

showp([recv([A,B,M])|P],_,B) :- !, % new A -> B: M
  make_party(left,A),
  show_msg(right,M,right),
  showp(P,A,B).

showp([recv([A,B,M])|P],B,_) :- !, 
  make_party(right,A),
  show_msg(left,M,left),
  showp(P,B,A).

showp([recv([A,B,M])|P],A,_) :- !, % A -> new B: M
  make_party(right,B),
  show_msg(right,M,right),
  showp(P,A,B).

showp([recv([A,B,M])|P],_,A) :- !, 
  make_party(left,B),
  show_msg(left,M,left),
  showp(P,B,A).

showp([recv([A,B,M])|P],_,_) :- !, % new A -> new B: M
  make_party(left,A),
  make_party(right,B),
  show_msg(right,M,right),
  showp(P,A,B).

showp([send([A,B,M])|P],A,B) :- !, % A -> B: M
  show_msg(right,M,left),
  showp(P,A,B).

showp([send([A,B,M])|P],A,_) :- !, % A -> new B: M
  make_party(right,B),
  show_msg(right,M,left),
  showp(P,A,B).

showp([send([A,B,M])|P],_,A) :- !, 
  make_party(left,B),
  show_msg(left,M,right),
  showp(P,B,A).

showp([send([A,B,M])|P],_,B) :- !, % new A -> B: M
  make_party(left,A),
  show_msg(right,M,left),
  showp(P,A,B).

showp([send([A,B,M])|P],B,_) :- !, 
  make_party(right,A),
  show_msg(left,M,right),
  showp(P,B,A).

showp([send([A,B,M])|P],_,_) :- !, % new A -> new B: M
  make_party(left,A),
  make_party(right,B),
  show_msg(right,M,left),
  showp(P,A,B).

showp([M|P],A,B) :-
  nl,write(M),writeln(' not in form send/recv([A,B,M])'),
  showp(P,A,B). 

show_msg(D,M,E) :-
  term_to_atom(M,Ma),
  make_arrow(D,Ma,E).

groundp(P,Q) :- reset_gensym,groundp1(P,Q).

groundp1(P,P) :- atomic(P),!.
groundp1(P,Q) :- var(P),!,
  gensym(v_,Q),
  P=Q.
groundp1([X|A],[Y|B]) :- !,
  groundp1(X,Y),groundp1(A,B).
groundp1(F,G) :- 
  F =.. A,
  groundp1(A,B),
  G =.. B.

% showb displays bundles.

showb([]).
showb([T|B]) :-
	groundp(T,T1),
	showp(T1),
	showb(B).

% sample protocol traces

prot1([
  recv([a,b,[a,na]*kb]),
  recv([b,a,[na,nb]*ka]),
  recv([a,b,[nb]*kb])
]).

prot2(A,B,X,N,Nb,[
  send([A,X,[A,N]*pk(X)]),
  recv([A,B,[A,N]*pk(B)]),
  send([B,A,[N,Nb]*pk(A)]),
  recv([X,A,[N,Nb]*pk(A)]),
  send([A,X,[Nb]*pk(X)]),
  recv([A,B,[Nb]*pk(B)])
]).

prot3([
  recv([attester,guest,reallyveryextremelylongmessagebutoneatom]),
  recv([guest,attester,yetanotherreallyverylongmessagebutoneatom1]),
  recv([attester,appraiser,anothermessage]),
  recv([appraiser,enforcer,anothermessage1])
]).