move license to LICENSE file

[model-checker.git] / scanalysis.cc

diff --git a/scanalysis.cc b/scanalysis.cc
index 83a82275098d3a6b6e9ebd2b7f03cb1999cec27e..ff7854a87e8a31aec8e3ae105d403ad0b3559c66 100644 (file)
--- a/scanalysis.cc
+++ b/scanalysis.cc
@@ -65,10 +65,35 @@ ModelAction * SCAnalysis::getNextAction() {
                        act=first;
                }
        }
+       if (act==NULL)
+               return act;
+       //print cycles in a nice way to avoid confusion
+       //make sure thread starts appear after the create
+       if (act->is_thread_start()) {
+               ModelAction *createact=model->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;
+                       }
+               }
+       }
+
+       //make sure that joins appear after the thread is finished
+       if (act->is_thread_join()) {
+               int jointhread=id_to_int(act->get_thread_operand()->get_id());
+               action_list_t *threadlist=&(*threadlists)[jointhread];
+               if (!threadlist->empty()) {
+                       act=threadlist->front();
+               }
+       }
+
        return act;
 }
 
-action_list_t * SCAnalysis::generateSC(action_list_t *list) {  
+action_list_t * SCAnalysis::generateSC(action_list_t *list) {
        action_list_t *sclist=new action_list_t();
        while (true) {
                ModelAction * act=getNextAction();
@@ -123,7 +148,7 @@ bool SCAnalysis::updateConstraints(ModelAction *act) {
                                changed=true;
                                break;
                        }
-               }               
+               }
        }
        return changed;
 }
@@ -134,7 +159,7 @@ bool SCAnalysis::processRead(ModelAction *read, ClockVector *cv) {
        /* Merge in the clock vector from the write */
        const ModelAction *write=read->get_reads_from();
        ClockVector *writecv=cvmap->get(write);
-       changed|= ( writecv == NULL || merge(cv, read, writecv) && (*read < *write));
+       changed |= writecv == NULL || (merge(cv, read, writecv) && (*read < *write));
 
        for(int i=0;i<=maxthreads;i++) {
                thread_id_t tid=int_to_id(i);
@@ -153,14 +178,14 @@ bool SCAnalysis::processRead(ModelAction *read, ClockVector *cv) {
                        ClockVector *write2cv = cvmap->get(write2);
                        if (write2cv == NULL)
                                continue;
-                       
+
                        /* write -sc-> write2 &&
                                 write -rf-> R =>
                                 R -sc-> write2 */
                        if (write2cv->synchronized_since(write)) {
                                changed |= merge(write2cv, write2, cv);
                        }
-               
+
                        //looking for earliest write2 in iteration to satisfy this
                        /* write2 -sc-> R &&
                                 write -rf-> R =>
@@ -203,12 +228,6 @@ void SCAnalysis::computeCV(action_list_t *list) {
                                ClockVector *finishcv = cvmap->get(finish);
                                changed |= (finishcv == NULL) || merge(cv, act, finishcv);
                        }
-                       if (act->is_thread_join()) {
-                               Thread *joinedthr = act->get_thread_operand();
-                               ModelAction *finish = model->get_last_action(joinedthr->get_id());
-                               ClockVector *finishcv = cvmap->get(finish);
-                               changed |= (finishcv == NULL) || cv->merge(finishcv);
-                       }
                        if (act->is_read()) {
                                changed|=processRead(act, cv);
                        }