From: Brian Norris <banorris@uci.edu>
Date: Thu, 13 Dec 2012 02:27:27 +0000 (-0800)
Subject: model: change guaranteed condition into ASSERT()
X-Git-Tag: oopsla2013~428
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=9ab812e65ac3bdf679247f01611f21d1af8968b9;p=model-checker.git

model: change guaranteed condition into ASSERT()

This guaranteed condition should only be included as an ASSERT(). This
gives a bonus, that the code becomes a little easier to read.
---

diff --git a/model.cc b/model.cc
index 90b2c2f..059a522 100644
--- a/model.cc
+++ b/model.cc
@@ -2705,17 +2705,13 @@ bool ModelChecker::take_step() {
 
 	Thread *curr = priv->current_action ? get_thread(priv->current_action) : NULL;
 	if (curr) {
-		if (curr->get_state() == THREAD_READY) {
-			ASSERT(priv->current_action);
+		ASSERT(curr->get_state() == THREAD_READY);
 
-			priv->nextThread = check_current_action(priv->current_action);
-			priv->current_action = NULL;
+		priv->nextThread = check_current_action(priv->current_action);
+		priv->current_action = NULL;
 
-			if (curr->is_blocked() || curr->is_complete())
-				scheduler->remove_thread(curr);
-		} else {
-			ASSERT(false);
-		}
+		if (curr->is_blocked() || curr->is_complete())
+			scheduler->remove_thread(curr);
 	}
 	Thread *next = scheduler->next_thread(priv->nextThread);