From 2e0463c2310d538298915b7f51bdf603863e0fec Mon Sep 17 00:00:00 2001 From: Ernst Moritz Hahn Date: Thu, 8 Jan 2015 17:17:42 +0000 Subject: [PATCH] corrected choice of order in which states were eliminated. The previous approach lead to states always being eliminated in ascending state number order. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9513 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/param/StateEliminator.java | 26 +++++++++++++++++++++----- 1 file changed, 21 insertions(+), 5 deletions(-) diff --git a/prism/src/param/StateEliminator.java b/prism/src/param/StateEliminator.java index 6802d52e..76dfb93d 100644 --- a/prism/src/param/StateEliminator.java +++ b/prism/src/param/StateEliminator.java @@ -31,6 +31,7 @@ import java.util.Arrays; import java.util.BitSet; import java.util.Collections; import java.util.HashSet; +import java.util.List; import java.util.ListIterator; /** @@ -225,7 +226,7 @@ final class StateEliminator { } int[] states = new int[pmc.getNumStates()]; - + List statesList = new ArrayList(); switch (eliminationOrder) { case ARBITRARY: for (int state = 0; state < pmc.getNumStates(); state++) { @@ -237,20 +238,35 @@ final class StateEliminator { break; case FORWARD_REVERSED: states = collectStatesForward(); - Collections.reverse(Arrays.asList(states)); + for (int state = 0; state < pmc.getNumStates(); state++) { + statesList.add(states[state]); + } + Collections.reverse(statesList); + for (int state = 0; state < pmc.getNumStates(); state++) { + states[state] = statesList.get(state); + } break; case BACKWARD: states = collectStatesBackward(); break; case BACKWARD_REVERSED: states = collectStatesBackward(); - Collections.reverse(Arrays.asList(states)); + for (int state = 0; state < pmc.getNumStates(); state++) { + statesList.add(states[state]); + } + Collections.reverse(statesList); + for (int state = 0; state < pmc.getNumStates(); state++) { + states[state] = statesList.get(state); + } break; case RANDOM: for (int state = 0; state < pmc.getNumStates(); state++) { - states[state] = state; + statesList.add(state); + } + Collections.shuffle(statesList); + for (int state = 0; state < pmc.getNumStates(); state++) { + states[state] = statesList.get(state); } - Collections.shuffle(Arrays.asList(states)); break; default: throw new RuntimeException("unknown state elimination order");