/**\
 Module "partit.c"

 Handles partitions of equivalenceclasses into finergrain (smaller)
 classes according to the sametransition criterion: two states should
 stay in the same equivalenceclass if and only if they both have
 exactly the same transitions (i.e. they both go to the same equivalence
 class on every possible alphabet symbol). For further details see
 Aho & Ullman's "Principles of Compiler design"  DFA Minimization.

 Partitioning a group of states into equivalenceclasses is done
 much more efficiently than the straightforward way by two stages:

 1. First split the group into singleton subgroups (each subgroup
 consists of a single member) and then

 2. Use R.E. Tarjan fast UnionFind algorithm to merge singleton
 groups into equivalenceclasses.
\**/
#include "auto.h"
extern state_t find ();
extern void Union ();
#ifdef DEBUG
extern void dump_state ();
#endif
/*
 static int update_partitions (group_size, member, old_groups, new_groups)
 int group_size;
 state_t member[], old_groups[], new_groups[];

 1. scans all members of 'member[]' group and checks if the UnionFind
 arrays 'old_groups[]' & 'new_groups[]' are partitioned equivalently
 with respect to the (partial) group 'member[]'.
 2. If partitions are not equivalent  updates 'old_groups[]' according
 to 'new_groups[]' (only in the states of 'member[]') and returns TRUE.
 Otherwise  no updating is done and FALSE is returned.
`*/
static int update_partitions (group_size, member, old_groups, new_groups)
int group_size;
state_t member[], old_groups[], new_groups[];
{
state_t i, state;
state_t old_rep, new_rep;
int update = FALSE;
for (i = 0; i < group_size; i++) {
state = member[i];
old_rep = find(state, old_groups);
new_rep = find(state, new_groups);
if (old_rep != new_rep) {
update = TRUE; /* at least one transition is different */
break;
}
}
if (update) {
for (i = 0; i < group_size; i++) {
state = member[i];
old_groups[state] = new_groups[state];
}
return TRUE; /* partitions updated */
} else
return FALSE; /* no updating of partitions */
}
/*
 void init_partitions (nstates, attribs, groups)
 int nstates;
 char attribs[];
 state_t groups[];

 Initialize the UnionFind array 'groups[]' with two disjoint equivalence
 groups according to the state attributes 'attribs[]' of a DFA:
 a. The accept states
 b. All states that are not accept states
`*/
void init_partitions (nstates, attribs, groups)
int nstates;
char attribs[];
state_t groups[];
{
state_t accept_rep = 0; /* representative state of acceptstates */
state_t others_rep = 0; /* representative state of other states */
state_t i;
for (i = 1; i <= nstates; i++) /* clear 'groups[]' array */
groups[i] = 0; /* i.e. make its members disjoint */
for (i = 1; i <= nstates; i++) {
if (attribs[i] == 'A') {
if (accept_rep == 0) { /* no representative yet */
accept_rep = i;
} else
Union(accept_rep, i, groups);
} else {
if (others_rep == 0) { /* no representative yet */
others_rep = i;
} else
Union(others_rep, i, groups);
}
}
}
/*
 static int same_transitions (s1, s2, mat, nab, groups)
 state_t s1, s2;
 state_t mat[MAX_STATES + 1][AB_SIZE + 1];
 int nab;
 state_t groups[];

 Return TRUE if the two states 's1' and 's2' have equivalent transitions
 according to the transitionmatrix 'mat[][]', FALSE otherwise.
 'nab' is the number of symbols in the alphabet.
 'groups[]' is the current partition of the states into equivalence
 classes.
`*/
static int same_transitions (s1, s2, mat, nab, groups)
state_t s1, s2;
state_t mat[MAX_STATES + 1][AB_SIZE + 1];
int nab;
state_t groups[];
{
state_t i, transition1, transition2;
for (i = 1; i <= nab; i++) { /* Loop over Alphabet symbols */
transition1 = mat[s1][i];
transition2 = mat[s2][i];
if (transition1 > 0) /* find the representative of transition1 */
transition1 = find(transition1, groups);
if (transition2 > 0) /* find the representative of transition2 */
transition2 = find(transition2, groups);
if (transition1 != transition2)
return FALSE;
}
return TRUE; /* All transitions of s1 & s2 were equivalent */
}
/*
 int partition (dfa, old_groups)
 automaton_t *dfa;
 state_t old_groups[];

 Partition the UnionFind array 'old_groups[]' to finergrain partitions
 according to the transitions of the initial partition.
 (i.e. if members of a group in a partition go to different groups on
 at least one input symbol  the group is partitioned such that these
 members no longer lie in the same group).
 'dfa' point to the DFA according to which partition is done.
 Return TRUE iff the initial partition was further partitioned,
 Otherwise  FALSE
`*/
int partition (dfa, old_groups)
automaton_t *dfa;
state_t old_groups[];
{
state_t member[MAX_STATES + 1]; /* singlegroup members */
state_t new_groups[MAX_STATES + 1]; /* temporary UnionFind array */
char unified[MAX_STATES + 1]; /* flags to mark unified states */
state_t rep; /* group representative */
int updated = FALSE;
int group_size, nstates = dfa>nstates;
int i, j;
for (rep = 1; rep <= nstates; rep++) {
if (old_groups[rep] >= 0) /* skip nonrepresentatives */
continue; /* and groups with cardinality 1 */
/*
 else  found a group representative:
 1. Fill 'member[]' with all members of this group
 2. Build a temporary disjoint group with these members
 in 'new_groups[]'
*/
group_size = 0;
for (i = 1; i <= nstates; i++) {
if (find(i, old_groups) == rep) { /* found a group member */
member[group_size++] = i;
new_groups[i] = 0;
unified[i] = FALSE;
}
}
/*
 For every pair of members member[i] & member[j] in the temporary
 disjoint group check iff they have the same transitions according
 To the main partition 'old_groups[]':
 If so: Unify them (in the temporary group) into one group

 Every already treated member[i] is marked by setting:

 unified[member[i]] = TRUE

 This is done for efficiency since all members that have the same
 transitions as member[i] are unified with member[i] in the Ith
 pass through the loop so there's no use in trying to check them
 further. (only those members of the disjoint group who are still
 "ununified" need to be checked among themselves).
*/
for (i = 0; i < group_size  1; i++) {
if (unified[member[i]])
continue;
unified[member[i]] = TRUE;
/*
 Since the equivalence relation is symmetric it is
 sufficient to check i & j pairs only when i < j
*/
for (j = i + 1; j < group_size; j++) {
if (unified[member[j]])
continue;
if (same_transitions(member[i], member[j], dfa>mat, dfa>nab, old_groups)) {
Union(member[i], member[j], new_groups);
unified[member[j]] = TRUE;
}
}
}
#if DEBUG > 0
dump_state (dfa, old_groups);
#endif
if (update_partitions(group_size, member, old_groups, new_groups)) {
updated = TRUE;
}
}
return (updated);
}