Merge remote-tracking branch 'private/master'

[model-checker.git] / scanalysis.cc

diff --git a/scanalysis.cc b/scanalysis.cc
index 75aed1aa80ed994985fee2b67ff69e83b37a67cb..8aa400c239223a8d90ef1119126bdd87cb163b8f 100644 (file)
--- a/scanalysis.cc
+++ b/scanalysis.cc
@@ -29,9 +29,8 @@ void SCAnalysis::print_list(action_list_t *list) {
                        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());
@@ -82,7 +81,7 @@ ModelAction * SCAnalysis::getNextAction() {
                        continue;
                ModelAction *first = threadlist->front();
                if (act==NULL) {
-                       act=first;
+                       act = first;
                        continue;
                }
                ClockVector *cv = cvmap.get(act);
@@ -93,7 +92,6 @@ ModelAction * SCAnalysis::getNextAction() {
        if (act == NULL)
                return act;
 
-
        /* Find the model action with the earliest sequence number in case of a cycle.
         */
 
@@ -102,11 +100,22 @@ ModelAction * SCAnalysis::getNextAction() {
                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;
                }
        }