Reset C++ templates due to race conditions

src/main/resources/de/hhu/stups/codegenerator/CppTemplate.stg

@@ -19,7 +19,6 @@ machine(forModelChecking, imports, includedMachines, machine, structs, constants
 #include \<atomic>
 #include \<any>
 #include \<mutex>
-#include \<shared_mutex>
 #include \<future>
 #include \<boost/asio/post.hpp>
 #include \<boost/asio/thread_pool.hpp>
@@ -1123,22 +1122,21 @@ model_check_transition(machine, hasParameters, tupleType, transitionIdentifier,
 <if(hasParameters)>
 <if(isCaching)>
 <machine>::_ProjectionRead_<evalTransitions> read_<evalTransitions>_state = state._projected_state_for_<evalTransitions>();
+BSet\<<tupleType>\> <transitionIdentifier>;
 auto <transitionIdentifier>_ptr = _OpCache<evalTransitions>.find(read_<evalTransitions>_state);
 if(<transitionIdentifier>_ptr == _OpCache<evalTransitions>.end()) {
-    BSet\<<tupleType>\> <transitionIdentifier> = state.<evalTransitions>();
+    <transitionIdentifier> = state.<evalTransitions>();
     {
         std::unique_lock\<std::mutex> _ProjectionRead_<evalTransitions>_lock(_ProjectionRead_<evalTransitions>_mutex);
         _OpCache<evalTransitions>.insert({read_<evalTransitions>_state, <transitionIdentifier>});
     }
-    for(const <tupleType>& param : <transitionIdentifier>) {
-        <execTransitions>
-    }
 } else {
-    BSet\<<tupleType>\> <transitionIdentifier> = <transitionIdentifier>_ptr->second;
+    <transitionIdentifier> = <transitionIdentifier>_ptr->second;
+}
+
 for(const <tupleType>& param : <transitionIdentifier>) {
     <execTransitions>
 }
-}
 <else>
 BSet\<<tupleType>\> <transitionIdentifier> = state.<evalTransitions>();
 for(const <tupleType>& param : <transitionIdentifier>) {
@@ -1511,7 +1509,10 @@ copiedState.<operation>(<parameters; separator=", ">);
 <endif>
 copiedState.stateAccessedVia = "<operation>";
 result.insert(copiedState);
+{
+    std::unique_lock\<std::mutex> lock(mutex);
     transitions += 1;
+}
 >>
 
 model_check_transition_param_assignment(type, param, val, isLhs, oneParameter) ::= <<
@@ -1655,12 +1656,16 @@ void modelCheckMultiThreaded(boost::asio::thread_pool& workers) {
     states.insert(machine);
     unvisitedStates.push_back(machine);
 
-    std::atomic\<bool> stopThreads(false);
+    std::atomic\<bool> stopThreads;
+    stopThreads = false;
     std::atomic\<int> possibleQueueChanges;
     possibleQueueChanges = 0;
 
-    while(!unvisitedStates.empty() && !stopThreads.load()) {
-        possibleQueueChanges.fetch_add(1);
+    std::atomic\<bool> waitFlag;
+    waitFlag = true;
+
+    while(!unvisitedStates.empty() && !stopThreads) {
+        possibleQueueChanges += 1;
         <machine> state = next();
         std::packaged_task\<void()> task([&, state] {
             std::unordered_set\<<machine>, <machine>::Hash, <machine>::HashEqual> nextStates = generateNextStates(state);
@@ -1681,12 +1686,14 @@ void modelCheckMultiThreaded(boost::asio::thread_pool& workers) {
                 }
             }
 
-            possibleQueueChanges.fetch_sub(1);
             {
                 std::unique_lock\<std::mutex> lock(mutex);
-                if (!unvisitedStates.empty() || possibleQueueChanges.load() == 0) {
+                possibleQueueChanges -= 1;
+                int running = possibleQueueChanges;
+                if (!unvisitedStates.empty() || running == 0) {
                     {
                         std::unique_lock\<std::mutex> lock(waitMutex);
+                        waitFlag = false;
                         waitCV.notify_one();
                     }
                 }
@@ -1696,26 +1703,29 @@ void modelCheckMultiThreaded(boost::asio::thread_pool& workers) {
             if(invariantViolated(state)) {
                 invariantViolatedBool = true;
                 counterExampleState = state;
-                stopThreads.store(true);
+                stopThreads = true;
             }
 
             if(nextStates.empty()) {
                 deadlockDetected = true;
                 counterExampleState = state;
-                stopThreads.store(true);
+                stopThreads = true;
             }
 
         });
 
+        waitFlag = true;
         boost::asio::post(workers, std::move(task));
 
         {
             std::unique_lock\<std::mutex> lock(waitMutex);
+            if(unvisitedStates.empty() && possibleQueueChanges > 0) {
                 waitCV.wait(lock, [&] {
-                return !unvisitedStates.empty() || possibleQueueChanges == 0;
+                    return waitFlag == false;
                 });
             }
         }
+    }
     workers.join();
     printResult();
 }