From f3ff3b06318cae93db4d682e6451ddbca4760328 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Tue, 22 Mar 2016 16:39:28 +0100 Subject: Use vector instead of set to add/remove states Deterministic adding/removing of states. --- lib/Core/Executor.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'lib/Core/Executor.h') diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 99f5921b..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 addedStates; + std::vector 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 removedStates; + std::vector removedStates; /// When non-empty the Executor is running in "seed" mode. The /// states in this map will be executed in an arbitrary order -- cgit 1.4.1