symbol(X) :- delta(_,X,_).
alphabet(A) :- setof(X,symbol(X),A).
state(X) :- delta(X,_,_).
state(X) :- delta(_,_,X).
states(Q) :- setof(X,state(X),Q).
mark([R,S]) :- states(Q), length(Q,Nstates), test_mark([R,S],0,Nstates).
notmark([R,S]) :- state(R), state(S), R < S, not mark([R,S]).
test_mark([R,S],_,_) :- final_state(R), not final_state(S).
test_mark([R,S],_,_) :- final_state(S), not final_state(R).
test_mark([R,S],N,Nstates) :- 
  N < Nstates, 
  delta(R,X,P), 
  delta(S,X,Q), 
  M is N+1, 
  test_mark([P,Q],M,Nstates).
print_start([X|_]) :- start_state(S), member(S,X), 
  write(start_state), write('('), write(X),
                  write(')'), write('.'), nl.
print_start([X|L]) :- start_state(S), not member(S,X), print_start(L).
write_final(X) :- write(final_state),write('('), write(X), write(')'), write('.'), nl.
intersect([],_,[]).
intersect([X|L],S1,[X|S]) :- member(X,S1), intersect(L,S1,S).
intersect([X|L],S1,S) :- not member(X,S1), intersect(L,S1,S).
print_final([],_).
print_final([X|L],F) :- intersect(X,F,G), G \== [], write_final(X), print_final(L,F).
print_final([X|L],F) :- intersect(X,F,G), G == [], print_final(L,F).
print_trans(_,_,[]).
print_trans(A,NewQ,[X|Q]) :- process_state(X,A,NewQ), print_trans(A,NewQ,Q).
process_state(_,[],_).
process_state([P|L],[A|M],NewQ) :- 
  delta(P,A,Q), 
  find_state(Q,NewQ,Q1), 
  print_delta([P|L],A,Q1),
  process_state([P|L],M,NewQ).
find_state(Q,[X|_],X) :- member(Q,X).
find_state(Q,[X|L],Y) :- not member(Q,X), find_state(Q,L,Y).
print_delta(P,A,Q) :- write(delta), write('('), write(P), write(','),
write(A), write(','), write(Q), write(')'), write('.'), nl.
minimize :- 
  states([X|L]), alphabet(A),
  setof(NewQ,equivalences([X],L,[[X]],NewQ),[Q]),
  print_start(Q),
  setof(Z,final_state(Z),F),
  print_trans(A,Q,Q),
  print_final(Q,F).
equivalences(_,[],Q,Q) :- !.
equivalences(P,[X|L],Qtemp,Q) :- 
  oldClass(X,P,Qtemp,Qtemp1), Qtemp \== Qtemp1, !, equivalences([X|P],L,Qtemp1,Q). 
equivalences(P,[X|L],Qtemp,Q) :- 
  oldClass(X,P,Qtemp,Qtemp1), Qtemp == Qtemp1, !, equivalences([X|P],L,[[X]|Qtemp],Q). 
oldClass(X,[],Q,[[X]|Q]).
oldClass(X,[Y|_],Q,NewQ) :- X \== Y, not mark([X,Y]), updateQ(X,Y,Q,NewQ).
oldClass(X,[Y|L],Q,NewQ) :- X \== Y, mark([X,Y]), oldClass(X,L,Q,NewQ).
updateQ(X,Y,[Z|L],[[X|Z]|L]) :- member(Y,Z). 
updateQ(X,Y,[Z|L],[Z|NewQ]) :- not member(Y,Z), updateQ(X,Y,L,NewQ). 
