I expect that we should never have a totally-empty NodeStack. It is designed
such that there is a stub 'empty' node that represents the choices at the start
of the program, when the first userprogram thread is 'created' (note: there is
no corresponding ModelAction for this first creation).
ModelAction * NodeStack::explore_action(ModelAction *act)
{
DBG();
- if (node_list.empty()) {
- node_list.push_back(new Node(act));
- iter = node_list.begin();
- } else if (get_head()->has_been_explored(act->get_tid())) {
+
+ ASSERT(!node_list.empty());
+
+ if (get_head()->has_been_explored(act->get_tid())) {
/* Discard duplicate ModelAction */
delete act;
iter++;