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

[<xr...@us...>]

Revision: 1910
          http://sourceforge.net/p/scstudio/code/1910
Author:   xrehak
Date:     2016-01-12 15:44:55 +0000 (Tue, 12 Jan 2016)
Log Message:
-----------
local actions repaired in local-choice ... more testing needed!
and in race and time-race (the problem was in causal closure initiator).

Modified Paths:
--------------
    trunk/src/check/localchoice/local_choice_checker.cpp
    trunk/src/check/pseudocode/causal_closure_initiator.cpp
    trunk/src/check/race/race_checker.cpp

Modified: trunk/src/check/localchoice/local_choice_checker.cpp
===================================================================
--- trunk/src/check/localchoice/local_choice_checker.cpp	2016-01-12 15:39:52 UTC (rev 1909)
+++ trunk/src/check/localchoice/local_choice_checker.cpp	2016-01-12 15:44:55 UTC (rev 1910)
@@ -81,6 +81,7 @@
       {
         if(e->is_minimal())
         {
+          // Local Actions are not allowed in a coregions
           MessageEvent* me = dynamic_cast<MessageEvent*>(e);
           if(me != NULL && me->is_send())
             m_mep = true;
@@ -99,11 +100,16 @@
         MessageEvent* me = dynamic_cast<MessageEvent*>(e);
         if(me != NULL && me->is_send())
           m_mep = true;
+
+        LocalActionEvent* la = dynamic_cast<LocalActionEvent*>(e);
+        if(la != NULL)
+          m_mep = true;
       }
     }
   }
   m_idle = false;  //any event found -> instance is not idle
 }
+
 void IterationListener::on_white_node_found(HMscNode *n)
 {
   if(!dynamic_cast<ReferenceNode*>(n) && !dynamic_cast<StartNode*>(n))

Modified: trunk/src/check/pseudocode/causal_closure_initiator.cpp
===================================================================
--- trunk/src/check/pseudocode/causal_closure_initiator.cpp	2016-01-12 15:39:52 UTC (rev 1909)
+++ trunk/src/check/pseudocode/causal_closure_initiator.cpp	2016-01-12 15:44:55 UTC (rev 1910)
@@ -63,11 +63,13 @@
     {
       Event* j_event = events[j];
       MessageEvent* j_msg_event = dynamic_cast<MessageEvent*>(j_event);
+      LocalActionEvent* j_la_event = dynamic_cast<LocalActionEvent*>(j_event);
       
       if(i_event->get_instance()==j_event->get_instance() && 
-        j_msg_event != NULL && !j_msg_event->is_receive() && i_visual_closure[j])
+        ( j_la_event != NULL || ( j_msg_event != NULL && !j_msg_event->is_receive() )) &&
+        i_visual_closure[j])
       {
-        //i_event and j_event are from the same instance, j_event is send event and
+        //i_event and j_event are from the same instance, j_event is send or local action event and
         //i_event < j_event
         i_causal_closure[j] = true;
       }

Modified: trunk/src/check/race/race_checker.cpp
===================================================================
--- trunk/src/check/race/race_checker.cpp	2016-01-12 15:39:52 UTC (rev 1909)
+++ trunk/src/check/race/race_checker.cpp	2016-01-12 15:44:55 UTC (rev 1910)
@@ -272,12 +272,14 @@
   BMscDuplicator duplicator;
   BMscPtr original = e1->get_instance()->get_bmsc();
   
-  // NOTE: race should only occur with message events; just for sure...
+  e1->set_marked();
+  e2->set_marked();
+
+  // NOTE: race should occur with message events and local actions
+  // if it is a message:
   MessageEvent* me1 = dynamic_cast<MessageEvent*>(e1);
   MessageEvent* me2 = dynamic_cast<MessageEvent*>(e2);
 
-  e1->set_marked();
-  e2->set_marked();
   if (me1 != NULL) me1->get_message().get()->set_marked();
   if (me2 != NULL) me2->get_message().get()->set_marked();
 

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