%
%  Peterson's algorithm for mutual exclusion
%  Create a state transition diagram.
%

%
%  num is used to generate state numbers.
%  state is used to cache previously created states.
%
:- dynamic num/1, state/6.

%
%  The transitions, next1 for process 1, next2 for process 2.
%  A state consists of:
%    (IP of process 1, IP of process 2, C1, C2, Last, N),
%  where N is the number of a state, used for printing
%  and for indicating that a state is the same as a previous one.
%
next1(state(set1,   P2, _,  C2,    _, N),
      state(test1,  P2,  1, C2,    1, N)).
next1(state(test1,  P2, C1,  0, Last, N),
      state(reset1, P2, C1,  0, Last, N)).
next1(state(test1,  P2, C1, C2,    2, N),
      state(reset1, P2, C1, C2,    2, N)).
next1(state(reset1, P2, _,  C2, Last, N),
      state(set1,   P2,  0, C2, Last, N)).
                                                             
next2(state(P1, set2,   C1,  _,    _, N),
      state(P1, test2,  C1,  1,    2, N)).
next2(state(P1, test2,   0, C2, Last, N),
      state(P1, reset2,  0, C2, Last, N)).
next2(state(P1, test2,  C1, C2,    1, N),
      state(P1, reset2, C1, C2,    1, N)).
next2(state(P1, reset2, C1,  _, Last, N),
      state(P1, set2,   C1,  0, Last, N)).

run :-
  retractall(num(_)),                      % Clear databases.
  retractall(state(_,_,_,_,_,_)),
  assert(num(1)),                          % Initialize state number.
  Current = state(set1, set2, 0, 0, 1, 1), % Cache initial state.
  assert(Current),
  write('Init   '),
  write_state(Current),
  move(Current, 0).

%
%  move(S, Indent)
%    Move from S to next state.
%    Indent is counter for output.
%
move(S, Indent) :-
  Indent1 is Indent + 2,
  arg(6, S, N),                % Get state number.
  write_from(N, 1, Indent1),   % Write N -> P1.
  move1(S, next1, Indent1),    % Move by executing instruction from P1.
  write_from(N, 2, Indent1),   % Write N -> P2.
  move1(S, next2, Indent1).    % Move by executing instruction from P2.

%
%  move1(S, Next, Indent)
%   Next is next1 or next2.
%   Get appropriate next state from S (if any).
%
move1(S, Next, Indent) :- 
  call(Next, S, S1), !,
  new_state(S1, Indent).
move1(_, _, _) :- 
  write('No transition'), nl.

%
%  new_state(S, Indent)
%    If the new state S is already cached, write its number.
%    Otherwise, generate a new state number,
%      replace it in S, cache it and write out.
%
new_state(state(P1, P2, C1, C2, L, _), _) :-
  state(P1, P2, C1, C2, L, N), !,
  write('Same as state '), w(N), nl.

new_state(S, Indent) :-
  retract(num(Num)), Num1 is Num+1, assert(num(Num1)),
  setarg(6, S, Num1),
  assert(S),
  write_state(S),
  move(S, Indent).

%
%  write_state(S) - write the state.
%
write_state(state(P1, P2, C1, C2, Last, N)) :-
  write(N), write('. ('),
  write_st(P1, S1), write(S1), write(', '),
  write_st(P2, S2), write(S2), 
  write(', C1='),   write(C1), 
  write(', C2='), write(C2),
  write(', Last='), write(Last), write(')'), nl.

%
%  write_st(IP, String) -
%    String is the statement corresponding to IP.
%
write_st(set1,   'C1:=1').
write_st(reset1, 'C1:=0').
write_st(set2,   'C2:=1').
write_st(reset2, 'C2:=0').
write_st(last-1, 'Last:=1').
write_st(last-2, 'Last:=2').
write_st(test1,  'C2=0vL<>1').
write_st(test2,  'C1=0vL<>2').

%
%  write_from(N, P, Indent) - write: State N -> Process P.
%
write_from(N, P, Indent) :-
  N1 is N + 1,
  w(N), write('->P'), write(P), 
  tab(Indent), 
  sp(N1).

%
%  sp(N) - write extra space for one-digit number. 
%  w(N)  - write N right-justified in two columns.
%
sp(N) :- N < 10, !, write(' ').
sp(_).

w(N) :- sp(N), write(N).