Fix bug that prevents graph generation from compiling.

[model-checker.git] / scanalysis.cc

diff --git a/scanalysis.cc b/scanalysis.cc
index 75aed1aa80ed994985fee2b67ff69e83b37a67cb..d4102fe8b6a20148ff30ae5a83cdaf506f2753df 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();
                        if (badrfset.contains(act))
                                model_print("BRF ");
                        act->print();

-                       cvmap.get(act)->print();

                        if (badrfset.contains(act)) {
                        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());
                        }
                }
                hash = hash ^ (hash << 3) ^ ((*it)->hash());


@@ -82,7 +81,7 @@ ModelAction * SCAnalysis::getNextAction() {
                        continue;
                ModelAction *first = threadlist->front();
                if (act==NULL) {
                        continue;
                ModelAction *first = threadlist->front();
                if (act==NULL) {

-                       act=first;
+                       act = first;

                        continue;
                }
                ClockVector *cv = cvmap.get(act);
                        continue;
                }
                ClockVector *cv = cvmap.get(act);


@@ -93,7 +92,6 @@ ModelAction * SCAnalysis::getNextAction() {
        if (act == NULL)
                return act;
 
        if (act == NULL)
                return act;
 

-

        /* Find the model action with the earliest sequence number in case of a cycle.
         */
 
        /* 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();
                if (threadlist->empty())
                        continue;
                ModelAction *first = threadlist->front();

-               ClockVector *cv = cvmap.get(act);

                ClockVector *cvfirst = cvmap.get(first);
                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;

                }
        }
 
                }
        }
 


@@ -136,7 +145,10 @@ action_list_t * SCAnalysis::generateSC(action_list_t *list) {
                //add ordering constraints from this choice
                if (updateConstraints(act)) {
                        //propagate changes if we have them
                //add ordering constraints from this choice
                if (updateConstraints(act)) {
                        //propagate changes if we have them

+                       bool oc=cyclic;

                        computeCV(list);
                        computeCV(list);

+                       if (!oc && cyclic)
+                               model_print("XXXXXXXXXXXXXX\n");

                }
                //add action to end
                sclist->push_back(act);
                }
                //add action to end
                sclist->push_back(act);