* @param tid The Thread's ID
* @return A Thread reference
*/
-Thread * ModelChecker::get_thread(thread_id_t tid)
+Thread * ModelChecker::get_thread(thread_id_t tid) const
{
return thread_map->get(id_to_int(tid));
}
* @param act The ModelAction
* @return A Thread reference
*/
-Thread * ModelChecker::get_thread(ModelAction *act)
+Thread * ModelChecker::get_thread(ModelAction *act) const
{
return get_thread(act->get_tid());
}
if (has_asserted())
return false;
- Thread * curr = thread_current();
+ Thread *curr = thread_current();
if (curr) {
if (curr->get_state() == THREAD_READY) {
ASSERT(priv->current_action);
ASSERT(false);
}
}
- Thread * next = scheduler->next_thread(priv->nextThread);
+ Thread *next = scheduler->next_thread(priv->nextThread);
/* Infeasible -> don't take any more steps */
if (!isfeasible())
return false;
- if (next)
- next->set_state(THREAD_RUNNING);
DEBUG("(%d, %d)\n", curr ? curr->get_id() : -1, next ? next->get_id() : -1);
/* next == NULL -> don't take any more steps */
if (!next)
return false;
- if ( next->get_pending() != NULL ) {
- //restart a pending action
+ next->set_state(THREAD_RUNNING);
+
+ if (next->get_pending() != NULL) {
+ /* restart a pending action */
set_current_action(next->get_pending());
next->set_pending(NULL);
next->set_state(THREAD_READY);