Skip to content

Commit

Permalink
Refactor reduction algorithm
Browse files Browse the repository at this point in the history 
This refactoring doesn't seem to improve performance, though it does
simplify the algorithm for maintaining incremental information.
  • Loading branch information
@DavePearce
DavePearce committed Nov 22, 2015
1 parent fa8f9f7 commit 3fc38a7
Showing 1 changed file with 101 additions and 93 deletions.
194 changes: 101 additions & 93 deletions src/wyrw/util/Reductions.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,14 +32,15 @@ public static void reduce(Automaton automaton, int maxSteps, ReductionRule... re
}

/**
* Simple helper method for reducing an automaton.
* Simple helper method for reducing an automaton.
*
* @param automaton
*/
public static void reduceOver(Automaton automaton, int start, int maxSteps, ReductionRule[] reductions,
Comparator<Rewrite.Activation> comparator) {
// Now, attempt to reduce as much as possible
boolean[] reachable = new boolean[automaton.nStates()*2];
Incrementaliser inc = new Incrementaliser(automaton);

boolean changed = true;
while (changed && maxSteps-- > 0) {
changed = false;
Expand All @@ -51,19 +52,7 @@ public static void reduceOver(Automaton automaton, int start, int maxSteps, Redu
int target = activation.apply(automaton);
if (target != Automaton.K_VOID && from != target) {
// Rewrite applied
//automaton.compact(0);
// Update reachability status for nodes affected by this
// activation. This is because such states could cause
// an infinite loop of re-activations. More specifically, where
// we activate on a state and rewrite it, but then it remains
// and so we repeat.
reachable = initReachable(automaton, reachable);

// Compact all states above the pivot to eliminate unreachable
// states and prevent the automaton from growing continually.
// This is possible because automton.rewrite() can introduce
// null states into the automaton.
compact(automaton, pivot, reachable);
inc.rewrite(from, target);
//
changed = true;
break;
Expand All @@ -72,8 +61,6 @@ public static void reduceOver(Automaton automaton, int start, int maxSteps, Redu
}
}
}

compact(automaton, 0, reachable);
}

private static AbstractActivation[] probe(Automaton automaton, int start, ReductionRule[] reductions,
Expand All @@ -98,38 +85,110 @@ private static AbstractActivation[] probe(Automaton automaton, int start, Reduct
return array;
}


private void compact(Automaton automaton, int pivot) {
private static final class Incrementaliser {
private final Automaton automaton;
private boolean[] reachable;
private int[] binding;

}


/**
* Update the reachability information associated with the automaton after
* some change has occurred. This information is currently recomputed from
* scratch, though in principle it could be updated incrementally.
*/
private static boolean[] initReachable(Automaton automaton,
boolean[] reachable) {
/**
* Initialise the incrementaliser with a given automaton, which is
* presumed to be both compacted and minimised.
*
* @param automaton
*/
public Incrementaliser(Automaton automaton) {
this.automaton = automaton;
this.reachable = new boolean[automaton.nStates()*2];
this.binding = new int[automaton.nStates()*2];
}

/**
* Responsible for updating the data after a successful rewrite has been
* applied to the automaton.
*
* @param from
* @param to
*/
public void rewrite(int from, int to) {
update();
compact(0);
}

// TODO: update reachability information incrementally
/**
* Update the reachability information associated with the automaton
* after some change has occurred. This information is currently
* recomputed from scratch, though in principle it could be updated
* incrementally.
*/
private void update() {

if (reachable.length < automaton.nStates()) {
reachable = new boolean[automaton.nStates() * 2];
} else {
Arrays.fill(reachable, false);
}
// first, visit all nodes
for (int i = 0; i != automaton.nRoots(); ++i) {
int root = automaton.getRoot(i);
if (root >= 0) {
findReachable(automaton, reachable, root);
// TODO: update reachability information incrementally

if (reachable.length < automaton.nStates()) {
reachable = new boolean[automaton.nStates() * 2];
binding = new int[automaton.nStates() * 2];
} else {
Arrays.fill(reachable, false);
}
// first, visit all nodes
for (int i = 0; i != automaton.nRoots(); ++i) {
int root = automaton.getRoot(i);
if (root >= 0) {
findReachable(automaton, reachable, root);
}
}
}


private void compact(int pivot) {
int nStates = automaton.nStates();
int nRoots = automaton.nRoots();

// First, initialise binding for all states upto start state. This
// ensure that they are subsequently mapped to themselves.
for (int i = 0; i < nStates; ++i) {
binding[i] = i;
}

// Second, go through and eliminate all unreachable states and compact
// the automaton down, whilst updating reachable one oneStepUndo
// information accordingly.
int j = pivot;

for (int i = pivot; i < nStates; ++i) {
if (reachable[i]) {
Automaton.State ith = automaton.get(i);
binding[i] = j;
reachable[i] = false;
reachable[j] = true;
automaton.set(j++, ith);
}
}

return reachable;
if (j < nStates) {
// Ok, some compaction actually occurred; therefore follow through
// and update all states accordingly.
nStates = j;
automaton.resize(nStates); // will nullify all deleted states

// Update mapping and oneStepUndo for *all* states
for (int i = 0; i != nStates; ++i) {
Automaton.State state = automaton.get(i);
if(state != null) {
state.remap(binding);
}
}

// Update mapping for all roots
for (int i = 0; i != nRoots; ++i) {
int root = automaton.getRoot(i);
if (root >= 0) {
automaton.setRoot(i, binding[root]);
}
}
}
}
}

/**
* Visit all states reachable from a given starting state in the given
* automaton. In doing this, states which are visited are marked and,
Expand Down Expand Up @@ -170,55 +229,4 @@ public static void findReachable(Automaton automaton, boolean[] reachable,
}
}
}

private static void compact(Automaton automaton, int pivot,
boolean[] reachable) {
int nStates = automaton.nStates();
int nRoots = automaton.nRoots();
int[] binding = new int[nStates];

// First, initialise binding for all states upto start state. This
// ensure that they are subsequently mapped to themselves.
for (int i = 0; i < nStates; ++i) {
binding[i] = i;
}

// Second, go through and eliminate all unreachable states and compact
// the automaton down, whilst updating reachable one oneStepUndo
// information accordingly.
int j = pivot;

for (int i = pivot; i < nStates; ++i) {
if (reachable[i]) {
Automaton.State ith = automaton.get(i);
binding[i] = j;
reachable[i] = false;
reachable[j] = true;
automaton.set(j++, ith);
}
}

if (j < nStates) {
// Ok, some compaction actually occurred; therefore follow through
// and update all states accordingly.
nStates = j;
automaton.resize(nStates); // will nullify all deleted states

// Update mapping and oneStepUndo for *all* states
for (int i = 0; i != nStates; ++i) {
Automaton.State state = automaton.get(i);
if(state != null) {
state.remap(binding);
}
}

// Update mapping for all roots
for (int i = 0; i != nRoots; ++i) {
int root = automaton.getRoot(i);
if (root >= 0) {
automaton.setRoot(i, binding[root]);
}
}
}
}
}

0 comments on commit 3fc38a7

Please sign in to comment.