[Scstudio-commits] SF.net SVN: scstudio:[1907] trunk/src/check/race

[<lko...@us...>]

Revision: 1907
          http://sourceforge.net/p/scstudio/code/1907
Author:   lkorenciak
Date:     2016-01-08 14:31:25 +0000 (Fri, 08 Jan 2016)
Log Message:
-----------
=fixing race cchecker on actions 1-st part

Modified Paths:
--------------
    trunk/src/check/race/race_checker.cpp
    trunk/src/check/race/race_checker.h

Modified: trunk/src/check/race/race_checker.cpp
===================================================================
--- trunk/src/check/race/race_checker.cpp	2015-12-14 23:57:15 UTC (rev 1906)
+++ trunk/src/check/race/race_checker.cpp	2016-01-08 14:31:25 UTC (rev 1907)
@@ -488,7 +488,10 @@
 
   //mark elements
   e.get_first()->get_complete_message()->set_marked();
-  e.get_second()->get_complete_message()->set_marked();
+  MessageEvent* me = dynamic_cast<MessageEvent*>(e.get_second());
+  if (me != NULL) {
+    me->get_complete_message()->set_marked();
+  }
   e.get_first()->set_marked();
   e.get_second()->set_marked();
 
@@ -498,7 +501,9 @@
   
   //Unmark elements in the original BMsc
   e.get_first()->get_complete_message()->set_marked(NONE);
-  e.get_second()->get_complete_message()->set_marked(NONE);
+  if (me != NULL) {
+    me->get_complete_message()->set_marked(NONE);
+  }
   e.get_first()->set_marked(NONE);
   e.get_second()->set_marked(NONE);
 
@@ -617,15 +622,32 @@
         for(a=fooprint_edi[i].begin();a!=fooprint_edi[i].end();a++)
         {
           MessageEvent* a_event = dynamic_cast<MessageEvent*>((*a)->get_event());
-          if (a_event == NULL)
+          if (a_event != NULL) {
+            if(a_event->is_receive() && !m_mapper->same_channel(a_event,b_event))
+            {
+              m_counterexamples.push_back(RaceInHMscException(f,b_event,a_event,get_reached_elements().back()));
+            }
+            else if(a_event->is_send())
+            {
+              const BoolVector& a_instances = (*a)->get_instances();
+              size_t j = 0;
+              for(; j<a_instances.size(); j++)
+              {
+                if(a_instances[j] && b_instances[j])
+                {
+                  break;
+                }
+              }
+              if(j==a_instances.size())
+              {
+                m_counterexamples.push_back(RaceInHMscException(f,b_event,a_event,get_reached_elements().back()));
+              }
+            }
             continue;
+          }
           
-          if(a_event->is_receive() && !m_mapper->same_channel(a_event,b_event))
-          {
-            m_counterexamples.push_back(RaceInHMscException(f,b_event,a_event,get_reached_elements().back()));
-          }
-          else if(a_event->is_send())
-          {
+          LocalActionEvent* la_event = dynamic_cast<LocalActionEvent*>((*a)->get_event());
+          if (la_event != NULL) {
             const BoolVector& a_instances = (*a)->get_instances();
             size_t j = 0;
             for(; j<a_instances.size(); j++)
@@ -637,8 +659,9 @@
             }
             if(j==a_instances.size())
             {
-              m_counterexamples.push_back(RaceInHMscException(f,b_event,a_event,get_reached_elements().back()));
+              m_counterexamples.push_back(RaceInHMscException(f,b_event,la_event,get_reached_elements().back()));
             }
+            continue;
           }
         }
       }
@@ -648,7 +671,7 @@
 
 ////////////////////////////////////////////////////////////////////////////////
 
-RaceInHMscException::RaceInHMscException(FootprintPtr& footprint,MessageEvent* first, MessageEvent* second,
+RaceInHMscException::RaceInHMscException(FootprintPtr& footprint,MessageEvent* first, Event* second,
                                          const MscElementPList& path_to_second):
   m_footprint(footprint),m_first(first),
    m_second(second),m_path_to_second(path_to_second)
@@ -665,7 +688,7 @@
   return m_first;
 }
 
-MessageEvent* RaceInHMscException::get_second()
+Event* RaceInHMscException::get_second()
 {
   return m_second;
 }

Modified: trunk/src/check/race/race_checker.h
===================================================================
--- trunk/src/check/race/race_checker.h	2015-12-14 23:57:15 UTC (rev 1906)
+++ trunk/src/check/race/race_checker.h	2016-01-08 14:31:25 UTC (rev 1907)
@@ -380,12 +380,12 @@
   
   FootprintPtr m_footprint;
   MessageEvent* m_first;
-  MessageEvent* m_second;
+  Event* m_second;
   MscElementPList m_path_to_second;
   
 public:
   
-  RaceInHMscException(FootprintPtr& footprint,MessageEvent* first, MessageEvent* second, 
+  RaceInHMscException(FootprintPtr& footprint,MessageEvent* first, Event* second, 
     const MscElementPList& path_to_second);
   
   ~RaceInHMscException() throw ()
@@ -395,7 +395,7 @@
 
   FootprintPtr& get_footprint();
   MessageEvent* get_first();
-  MessageEvent* get_second();
+  Event* get_second();
   MscElementPList& get_path_to_second();
 };
 

This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.