Merge pull request #362 from MartinNowack/feat_determ_state_selection

Deterministic state addition and removing

1 files changed, 3 insertions, 2 deletions

diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 600c7b90..92edc364 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -122,12 +122,12 @@ private:
   /// instructions step. 
   /// \invariant \ref addedStates is a subset of \ref states. 
   /// \invariant \ref addedStates and \ref removedStates are disjoint.
-  std::set<ExecutionState*> addedStates;
+  std::vector<ExecutionState *> addedStates;
   /// Used to track states that have been removed during the current
   /// instructions step. 
   /// \invariant \ref removedStates is a subset of \ref states. 
   /// \invariant \ref addedStates and \ref removedStates are disjoint.
-  std::set<ExecutionState*> removedStates;
+  std::vector<ExecutionState *> removedStates;
 
   /// When non-empty the Executor is running in "seed" mode. The
   /// states in this map will be executed in an arbitrary order
@@ -412,6 +412,7 @@ private:
                      double maxInstTime);
   void checkMemoryUsage();
   void printDebugInstructions(ExecutionState &state);
+  void doDumpStates();
 
 public:
   Executor(const InterpreterOptions &opts, InterpreterHandler *ie);