if (badrfset.contains(act))
model_print("BRF ");
act->print();
- cvmap.get(act)->print();
if (badrfset.contains(act)) {
- model_print("DESIRED %u \n",badrfset.get(act)->get_seq_number());
+ model_print("Desired Rf: %u \n",badrfset.get(act)->get_seq_number());
}
}
hash = hash ^ (hash << 3) ^ ((*it)->hash());
continue;
ModelAction *first = threadlist->front();
if (act==NULL) {
- act=first;
+ act = first;
continue;
}
ClockVector *cv = cvmap.get(act);
if (act == NULL)
return act;
-
/* Find the model action with the earliest sequence number in case of a cycle.
*/
if (threadlist->empty())
continue;
ModelAction *first = threadlist->front();
- ClockVector *cv = cvmap.get(act);
ClockVector *cvfirst = cvmap.get(first);
- if (first->get_seq_number()<act->get_seq_number()&&
- (cv->synchronized_since(first)||!cvfirst->synchronized_since(act))) {
- act=first;
+ if (first->get_seq_number()<act->get_seq_number()) {
+ bool candidate=true;
+ for (int j = 0; j <= maxthreads; j++) {
+ action_list_t *threadlist2 = &threadlists[j];
+ if (threadlist2->empty())
+ continue;
+ ModelAction *check = threadlist2->front();
+ if ((check!=first) &&
+ cvfirst->synchronized_since(check)) {
+ candidate=false;
+ break;
+ }
+ }
+ if (candidate)
+ act=first;
}
}