Bug fix for spsc-queue test

diff --combined model.cc
index 1e425b2ece627b877e5b33dd2d7bfde60d65b47e,078a1ce75849ebc48334958a7842b22dd6c958d1..ea8f268ff270fa8d59674570103699c1eb36eb03
--- 1/model.cc
--- 2/model.cc
+++ b/model.cc
@@@ -346,13 -346,13 +346,13 @@@ uint64_t ModelChecker::switch_to_master
  
  void ModelChecker::continueRunExecution(Thread *old) 
  {
- /*
+ 
        if (params.traceminsize != 0 &&
                        execution->get_curr_seq_num() > checkfree) {
                checkfree += params.checkthreshold;
                execution->collectActions();
        }
- */
+ 
        thread_chosen = false;
        curr_thread_num = 1;
        Thread *thr = getNextThread();
@@@ -368,13 -368,13 +368,13 @@@
  
  void ModelChecker::startRunExecution(ucontext_t *old) 
  {
- /*
+ 
        if (params.traceminsize != 0 &&
                        execution->get_curr_seq_num() > checkfree) {
                checkfree += params.checkthreshold;
                execution->collectActions();
        }
- */
+ 
        thread_chosen = false;
        curr_thread_num = 1;
        Thread *thr = getNextThread();
@@@ -406,7 -406,7 +406,7 @@@ Thread* ModelChecker::getNextThread(
                        scheduler->sleep(thr);
                }
  
- //            chooseThread(act, thr);
+       chooseThread(act, thr);
        }
        return nextThread;
  }
@@@ -423,7 -423,6 +423,7 @@@ void ModelChecker::finishRunExecution(T
  void ModelChecker::finishRunExecution(ucontext_t *old) 
  {
        scheduler->set_current_thread(NULL);
 +      break_execution = true;
  }
  
  void ModelChecker::consumeAction()
@@@ -491,7 -490,7 +491,7 @@@ uint64_t ModelChecker::switch_thread(Mo
        if (act && execution->is_enabled(old) && !execution->check_action_enabled(act)) {
                scheduler->sleep(old);
        }
- //    chooseThread(act, old);
+       chooseThread(act, old);
  
        curr_thread_num++;
        Thread* next = getNextThread();
@@@ -545,17 -544,13 +545,17 @@@ void ModelChecker::handleChosenThread(T
  
  void ModelChecker::handleChosenThread(ucontext_t *old)
  {
 -      if (execution->has_asserted())
 +      if (execution->has_asserted()) {
                finishRunExecution(old);
 +              return;
 +      }
        if (!chosen_thread)
                chosen_thread = get_next_thread();
 -      if (!chosen_thread || chosen_thread->is_model_thread())
 +      if (!chosen_thread || chosen_thread->is_model_thread()) {
                finishRunExecution(old);
- /*    if (chosen_thread->just_woken_up()) {
 +              return;
 +      }
+       if (chosen_thread->just_woken_up()) {
                chosen_thread->set_wakeup_state(false);
                chosen_thread->set_pending(NULL);
                chosen_thread = NULL;
@@@ -564,9 -559,9 +564,7 @@@
                        finishRunExecution(old);
                else
                        startRunExecution(old); 
-       } */
 -      } else
--
--      {
++      } else {
                /* Consume the next action for a Thread */
                consumeAction();
  
@@@ -609,11 -604,7 +607,11 @@@ void ModelChecker::run(
        checkfree = params.checkthreshold;
        for(int exec = 0;exec < params.maxexecutions;exec++) {
                chosen_thread = init_thread;
 +              break_execution = false;
                do {
 +                      if (break_execution)
 +                              break;
 +
                        thread_chosen = false;
                        curr_thread_num = 1;
                        startRunExecution(&system_context);