%doesn't work for now -- not sure if it's a simple bug, or a problem w/theory

function M0 = minimize_dfsa(M0)
% M1 is the smallest equivalent nfsa to M0
% see str2dfsa.m for basic nfsa definitions

%this is a generalization of the the construction in Lewis and Papadimitriou, p 80

nQ = length(M0.Q);

% initialize the \equiv_0 relation
EQU = eye(nQ);
for p=1:nQ
  for q=p+1:nQ
    EQU(p,q) = (ismember(p,M0.F)==ismember(q,M0.F));
  end
end
EQU = EQU+EQU';

% compute \equiv_k for k=1:nQ
for k=1:nQ
  EQU1 = eye(nQ);
  for p=1:nQ
    for q=p+1:nQ
      b = EQU(p,q);
      if b
        for s=M0.ALF
	  P1 = nfsa_delta(M0,p,s);
          Q1 = nfsa_delta(M0,q,s);
	  b = ((isempty(P1)==isempty(Q1)));	
          for p1=P1
	    for q1=Q1
	      % natural generalization: 
 	      % all the children must be (k-1)-equivalent
 	      b = b & EQU(p1,q1);
  	      if ~b, break, end
	    end
	    if ~b, break, end
	  end
	  if ~b, break, end
        end
      end %if b
      EQU1(p,q) = b;
    end
  end
  EQU = EQU1 + EQU1';
end

% collapse equivalent states
for p=1:nQ
  for q=p+1:nQ
    if EQU(p,q)
      M0 = collapse(M0,p,q);
    end
  end
end

M0 = remove_unreachable_n(M0);
return


function M = collapse(M,p,q)
% everything that pointed to q must point to p

[pp,ss] = get_ndparents(M,q);
for j=1:length(pp)
  R = nfsa_delta(M,pp(j),ss(j));
  R = setrepl(R,q,p);
  M = set_ndelta(M,[pp(j)],[ss(j)],{R});
end

% now q is not reachable

% take q out of F if it's there
M.F = setdiff(M.F,q);
return


function set1 = setrepl(set1,p,q)
%replace all occurrences of p w/q in set1
set1(find(set1==p)) = q;
return