* when exploring a new execution ordering), in which case we defer to the
* scheduler.
*
- * @param curr The current ModelAction. This action might guide the choice of
- * next thread.
+ * @param curr Optional: The current ModelAction. Only used if non-NULL and it
+ * might guide the choice of next thread (i.e., THREAD_CREATE should be
+ * followed by THREAD_START, or ATOMIC_RMWR followed by ATOMIC_{RMW,RMWC})
* @return The next chosen thread to run, if any exist. Or else if no threads
* remain to be executed, return NULL.
*/
return true;
}
-ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
+ModelAction * ModelChecker::get_last_conflict(ModelAction *act) const
{
switch (act->get_type()) {
case ATOMIC_FENCE:
};
} while (next_execution());
+ model_print("******* Model-checking complete: *******\n");
print_stats();
}