- //print cycles in a nice way to avoid confusion
- //make sure thread starts appear after the create
- if (act->is_thread_start()) {
- ModelAction *createact = execution->get_thread(act)->get_creation();
- if (createact) {
- action_list_t *threadlist = &threadlists[id_to_int(createact->get_tid())];
- if (!threadlist->empty()) {
- ModelAction *first = threadlist->front();
- if (first->get_seq_number() <= createact->get_seq_number())
- act = first;
+
+ /* Find the model action with the earliest sequence number in case of a cycle.
+ */
+
+ for (int i = 0; i <= maxthreads; i++) {
+ action_list_t *threadlist = &threadlists[i];
+ if (threadlist->empty())
+ continue;
+ ModelAction *first = threadlist->front();
+ ClockVector *cvfirst = cvmap.get(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;
+ }