Thread: [Scstudio-commits] SF.net SVN: scstudio:[181] trunk (Page 2)

SourceForge Headquarters 1320 Columbia Street Suite 310 San Diego, CA 92101 +1 (858) 422-6466

Revision: 181
          http://scstudio.svn.sourceforge.net/scstudio/?rev=181&view=rev
Author:   babicaj
Date:     2009-01-31 23:08:34 +0000 (Sat, 31 Jan 2009)

Log Message:
-----------
RaceChecker,FifoChecker and duplicators refactored. RaceChecker was missing BMscChecker ancestor.

Modified Paths:
--------------
    trunk/src/check/order/fifo_checker.cpp
    trunk/src/check/pseudocode/msc_duplicators.cpp
    trunk/src/check/pseudocode/msc_duplicators.h
    trunk/src/check/race/footprint.cpp
    trunk/src/check/race/footprint.h
    trunk/src/check/race/race_checker.cpp
    trunk/src/check/race/race_checker.h
    trunk/src/data/msc.h
    trunk/tests/race_checker_test.cpp

Modified: trunk/src/check/order/fifo_checker.cpp
===================================================================

--- trunk/src/check/order/fifo_checker.cpp	2009-01-31 17:35:56 UTC (rev 180)
+++ trunk/src/check/order/fifo_checker.cpp	2009-01-31 23:08:34 UTC (rev 181)
@@ -32,16 +32,8 @@
   {
     //event is surely complete
     Event* copy = duplicator.get_event_copy(events[i]);
-    copy->set_marked(true);
     copy->get_complete_message()->set_marked(true);
-    if(copy->is_send())
-    {
-      copy->get_complete_message()->get_receive_event()->set_marked(true);
-    }
-    else
-    {
-      copy->get_complete_message()->get_send_event()->set_marked(true);
-    }
+    copy->get_complete_message()->get_receive_event()->set_marked(true);
   }
   return new_bmsc;
 }

Modified: trunk/src/check/pseudocode/msc_duplicators.cpp
===================================================================
--- trunk/src/check/pseudocode/msc_duplicators.cpp	2009-01-31 17:35:56 UTC (rev 180)
+++ trunk/src/check/pseudocode/msc_duplicators.cpp	2009-01-31 23:08:34 UTC (rev 181)
@@ -30,15 +30,21 @@
 {
 }
 
-Duplicator::~Duplicator()
+void Duplicator::cleanup_attributes()
 {
   MscElementPList::const_iterator i;
   for(i=m_modified_elements.begin();i!=m_modified_elements.end();i++)
   {
     (*i)->remove_attribute<MscElement*>(DUPLICATOR_COPY_ATTR);
   }
+  m_modified_elements.clear();
 }
 
+Duplicator::~Duplicator()
+{
+  cleanup_attributes();
+}
+
 MscElement*& Duplicator::get_copy(MscElement* e)
 {
   bool just_set;
@@ -225,8 +231,8 @@
 
 ////////////////////////////////////////////////////////////////////////
 
-GraphCreatorListener::GraphCreatorListener(HMsc* hmsc):
-m_hmsc(hmsc)
+GraphCreatorListener::GraphCreatorListener(BMscGraphDuplicator* duplicator,HMsc* hmsc):
+m_duplicator(duplicator),m_hmsc(hmsc)
 {
 }
 
@@ -290,7 +296,7 @@
     StartNode *new_node = new StartNode(n);
     m_hmsc->set_start(new_node);
     m_new_nodes.push_back(new_node);
-    set_copy(n,new_node);
+    m_duplicator->set_copy(n,new_node);
   }
 }
 
@@ -338,7 +344,7 @@
   m_hmsc->add_node(new_node);
   add_new_successor(new_node.get());
   m_new_nodes.push_back(new_node.get());
-  set_copy(old_node,new_node.get());
+  m_duplicator->set_copy(old_node,new_node.get());
 }
 
 bool GraphCreatorListener::is_root_element(HMscNode* n)
@@ -346,31 +352,19 @@
   return n->get_owner()==m_hmsc->get_original();
 }
 
-void GraphCreatorListener::set_copy(HMscNode* n, HMscNode* copy)
+PredecessorNode* GraphCreatorListener::get_predecessor()
 {
-  HMscNode*& attribute = get_copy(n);
-  attribute = copy;
+  return dynamic_cast<PredecessorNode*>(m_new_nodes.back());
 }
 
-HMscNode*& GraphCreatorListener::get_copy(HMscNode* n)
+HMscNode* GraphCreatorListener::get_node_copy(HMscNode* n)
 {
-  bool just_set;
-  HMscNode*& copy = n->get_attribute<HMscNode*>(BMSC_DUPLICATOR_COPY_ATTR,NULL,just_set);
-  if(just_set)
-  {
-    m_modified_elements.push_back(n);
-  }
-  return copy;
+  return dynamic_cast<HMscNode*>(m_duplicator->get_copy(n));
 }
 
-PredecessorNode* GraphCreatorListener::get_predecessor()
-{
-  return dynamic_cast<PredecessorNode*>(m_new_nodes.back());
-}
-
 void GraphCreatorListener::process_nonwhite_node(HMscNode* n)
 {
-  HMscNode* copy = get_copy(n);
+  HMscNode* copy = get_node_copy(n);
   add_new_successor(copy);
 }
 
@@ -478,12 +472,6 @@
 
 GraphCreatorListener::~GraphCreatorListener()
 {
-  while(!m_modified_elements.empty())
-  {
-    MscElement* e = m_modified_elements.back();
-    e->remove_attribute<HMscNode*>(BMSC_DUPLICATOR_COPY_ATTR);
-    m_modified_elements.pop_back();
-  }
   while(!m_modified_hmscs.empty())
   {
     HMsc* h = m_modified_hmscs.back();
@@ -492,13 +480,13 @@
   }
 }
 
-HMscPtr BMscGraphDuplicator::duplicate(HMscPtr& hmsc)
+HMscPtr BMscGraphDuplicator::duplicate_hmsc(HMscPtr& hmsc)
 {
   HMscPtr new_hmsc;
   if(hmsc.get())
   {
     new_hmsc = new HMsc(hmsc.get());
-    GraphCreatorListener listener(new_hmsc.get());
+    GraphCreatorListener listener(this,new_hmsc.get());
     DFSBMscGraphTraverser traverser;
     traverser.add_black_node_found_listener(&listener);
     traverser.add_gray_node_found_listener(&listener);
@@ -509,6 +497,16 @@
   return new_hmsc;
 }
 
+HMscPtr BMscGraphDuplicator::duplicate(HMscPtr& hmsc)
+{
+  BMscGraphDuplicator duplicator;
+  return duplicator.duplicate_hmsc(hmsc);
+}
+
+BMscGraphDuplicator::~BMscGraphDuplicator()
+{
+}
+
 HMscPtr HMscPathDuplicator::duplicate_path(const MscElementPListList& path)
 {
   HMscPtr root;
@@ -557,6 +555,7 @@
             if(ref_node)
             {
               ReferenceNode* new_ref = new ReferenceNode(ref_node);
+              new_ref->set_msc(ref_node->get_msc());
               new_hmsc->add_node(new_ref);
               new_rel = new_ref->add_predecessor(new_pred);
               new_pred = new_ref;

Modified: trunk/src/check/pseudocode/msc_duplicators.h
===================================================================
--- trunk/src/check/pseudocode/msc_duplicators.h	2009-01-31 17:35:56 UTC (rev 180)
+++ trunk/src/check/pseudocode/msc_duplicators.h	2009-01-31 23:08:34 UTC (rev 181)
@@ -41,6 +41,8 @@
   MscElement*& get_copy(MscElement* e);
 
   void set_copy(MscElement* original, MscElement* copy);
+
+  void cleanup_attributes();
 };
 
 class BMscDuplicator;
@@ -116,14 +118,32 @@
   Event* get_event_copy(Event* e);
 };
 
-///////////////////////////////////////////////////////////
+class BMscGraphDuplicator;
 
-class GraphCreatorListener: public WhiteNodeFoundListener,public GrayNodeFoundListener,
+/**
+ * \brief Duplicates HMsc like it would be BMsc graph.
+ *
+ * Result of this duplicator is flattened version of HMsc (BMsc graph)
+ * without unreachable HMscNodes and nodes which
+ * man isn't able to get to EndNode from.
+ *
+ * All ReferenceNodes reference only BMsc, moreover each BMsc is 
+ * referenced only one time -- each BMsc is duplicated too. Kept elements 
+ * references to its original element via attribute m_original.
+ *
+ * Original ReferenceNodes which references HMsc are transformed into 
+ * ConnectionNodes referencing the ReferenceNode by m_original. StartNodes 
+ * which don't occure in HMsc to be duplicated are removed. EndNodes
+ * of the same kind are transformed into ConnectionNodes referencing original
+ * EndNodes.
+ */
+class SCPSEUDOCODE_EXPORT GraphCreatorListener:public WhiteNodeFoundListener,public GrayNodeFoundListener,
   public BlackNodeFoundListener,public NodeFinishedListener
 {
 protected:
 
-  MscElementPList m_modified_elements;
+  BMscGraphDuplicator* m_duplicator;
+
   HMscPList m_modified_hmscs;
 
   MscElementPList m_new_nodes;
@@ -132,10 +152,6 @@
 
   bool is_root_element(HMscNode* n);
 
-  HMscNode*& get_copy(HMscNode* n);
-
-  void set_copy(HMscNode* n, HMscNode* copy);
-
   void process_new_node(HMscNode* old_node, HMscNodePtr& new_node);
 
   void process_nonwhite_node(HMscNode* n);
@@ -150,9 +166,11 @@
 
   void add_new_successor(HMscNode* new_successor);
 
+  HMscNode* get_node_copy(HMscNode* n);
+
 public:
 
-  GraphCreatorListener(HMsc* hmsc);
+  GraphCreatorListener(BMscGraphDuplicator* duplicator, HMsc* hmsc);
 
   ~GraphCreatorListener();
 
@@ -171,7 +189,6 @@
   void on_node_finished(StartNode* n);
   void on_node_finished(EndNode* n);
   void on_node_finished(ConnectionNode* n);
-
 };
 
 /**
@@ -191,13 +208,17 @@
  * of the same kind are transformed into ConnectionNodes referencing original
  * EndNodes.
  */
-class SCPSEUDOCODE_EXPORT BMscGraphDuplicator
+class SCPSEUDOCODE_EXPORT BMscGraphDuplicator:public Duplicator
 {
 
 public:
 
+  HMscPtr duplicate_hmsc(HMscPtr& hmsc);
+
   static HMscPtr duplicate(HMscPtr& hmsc);
 
+  ~BMscGraphDuplicator();
+
 };
 
 /**

Modified: trunk/src/check/race/footprint.cpp
===================================================================
--- trunk/src/check/race/footprint.cpp	2009-01-31 17:35:56 UTC (rev 180)
+++ trunk/src/check/race/footprint.cpp	2009-01-31 23:08:34 UTC (rev 181)
@@ -205,4 +205,14 @@
   return dynamic_cast<HMscNode*>(m_path.back());
 }
 
+const MscElementPList& Footprint::get_path() const
+{
+  return m_path;
+}
+
+FootprintPtr Footprint::get_previous()
+{
+    return m_previous;
+}
+
 // $Id$

Modified: trunk/src/check/race/footprint.h
===================================================================
--- trunk/src/check/race/footprint.h	2009-01-31 17:35:56 UTC (rev 180)
+++ trunk/src/check/race/footprint.h	2009-01-31 23:08:34 UTC (rev 181)
@@ -201,6 +201,10 @@
     const ExtremeEvents& max_events_greater);
   
   HMscNode* get_node();
+
+  const MscElementPList& get_path() const;
+
+  FootprintPtr get_previous();
 };
 
 #endif /* _FOOTPRINT_H */

Modified: trunk/src/check/race/race_checker.cpp
===================================================================
--- trunk/src/check/race/race_checker.cpp	2009-01-31 17:35:56 UTC (rev 180)
+++ trunk/src/check/race/race_checker.cpp	2009-01-31 23:08:34 UTC (rev 181)
@@ -20,7 +20,6 @@
 
 
 #include "check/race/race_checker.h"
-#include "check/pseudocode/msc_duplicators.h"
 
 BMscRaceCheckingListener::BMscRaceCheckingListener(RaceChecker* checker, ChannelMapperPtr mapper)
 {
@@ -35,7 +34,7 @@
   {
     BMscPtr example = m_checker->check_bmsc(b,m_mapper);
     if(example.get())
-      throw RaceInBMscException(b);
+      throw RaceInBMscException(example);
     //precompute MinP for b
   }
 }
@@ -233,8 +232,8 @@
   BMscDuplicator duplicator;
   BMscPtr original = e1->get_instance()->get_bmsc();
   BMscPtr copy = duplicator.duplicate_bmsc(original);
-  duplicator.get_copy(e1)->set_marked();
-  duplicator.get_copy(e2)->set_marked();
+  duplicator.get_event_copy(e1)->get_complete_message()->get_receive_event()->set_marked();
+  duplicator.get_event_copy(e2)->get_complete_message()->get_receive_event()->set_marked();
   duplicator.get_copy(e1->get_message().get())->set_marked();
   duplicator.get_copy(e2->get_message().get())->set_marked();
   return copy;
@@ -291,6 +290,7 @@
   m_instance_marker.cleanup_attributes();
   m_min_events_initiator.cleanup_attributes();
   m_max_events_initiator.cleanup_attributes();
+  m_graph_duplicator.cleanup_attributes();
 }
 
 void RaceChecker::prepare_hmsc(HMscPtr hmsc,ChannelMapperPtr mapper)
@@ -311,7 +311,7 @@
 HMscPtr RaceChecker::check(HMscPtr hmsc, ChannelMapperPtr mapper)
 {
   //transform hmsc into BMsc graph
-  HMscPtr transformed = BMscGraphDuplicator::duplicate(hmsc);
+  HMscPtr transformed = m_graph_duplicator.duplicate_hmsc(hmsc);
   //compute causal closure of all BMsc and check BMscs to be race free
   HMscPtr res = check_bmscs(transformed,mapper);
   if(res.get())
@@ -366,8 +366,9 @@
 HMscPtr RaceChecker::create_counter_example(const MscElementPListList& path, BMscPtr example)
 {
   HMscPathDuplicator duplicator;
+  //result contains path in already duplicated HMsc
   HMscPtr result = duplicator.duplicate_path(path);
-  //set propper msc to last element
+  //set proper msc to last element
   ReferenceNode* last_copy = dynamic_cast<ReferenceNode*>(
     duplicator.get_copy(path.back().back()));
   last_copy->set_msc(example);
@@ -376,13 +377,40 @@
   for(h=path.begin();h!=path.end();h++)
   {
     duplicator.get_copy(h->back())->set_marked(true);
+    //set proper original
+    MscElementPList::const_iterator e;
+    for(e=h->begin();e!=h->end();e++)
+    {
+      MscElement* elem = m_graph_duplicator.get_copy(*e);
+      elem->set_general_original((*e)->get_general_original());
+    }
   }
   return result;
 }
 
 HMscPtr RaceChecker::create_counter_example(RaceInHMscException& e)
 {
-  //TODO: create counter example
+  //build run in BMsc graph
+  FootprintPtr f = e.get_footprint();
+  MscElementPList path;
+  do
+  {
+    path.insert(path.begin(),f->get_path().begin(),f->get_path().end());
+    f = f->get_previous();
+  }
+  while(f);
+  //make structured path from simple path
+  MscElementPList::const_iterator elem;
+  MscElementPListList structured;
+  for(elem=path.begin();elem!=path.end();elem++)
+  {
+    if(dynamic_cast<StartNode*>(*elem))
+    {
+      MscElementPList empty;
+      structured.push_back(empty);
+    }
+    structured.back().push_back(*elem);
+  }
   return HMscPtr(new HMsc());
 }
 

Modified: trunk/src/check/race/race_checker.h
===================================================================
--- trunk/src/check/race/race_checker.h	2009-01-31 17:35:56 UTC (rev 180)
+++ trunk/src/check/race/race_checker.h	2009-01-31 23:08:34 UTC (rev 181)
@@ -29,6 +29,7 @@
 #include "check/pseudocode/refnode_finder.h"
 #include "check/race/footprint.h"
 #include "check/race/export.h"
+#include "check/pseudocode/msc_duplicators.h"
 
 class BMscRaceCheckingListener;
 class RaceInBMscException;
@@ -167,7 +168,7 @@
 
 };
 
-class SCRACE_EXPORT RaceChecker: public Checker, public HMscChecker
+class SCRACE_EXPORT RaceChecker: public Checker, public BMscChecker, public HMscChecker
 {
 
 protected:
@@ -181,6 +182,8 @@
   MinimalEventsInitiator m_min_events_initiator;
   
   MaximalEventsInitiator m_max_events_initiator;
+
+  BMscGraphDuplicator m_graph_duplicator;
   
   /**
    * Checks HMsc to have only race free BMscs

Modified: trunk/src/data/msc.h
===================================================================
--- trunk/src/data/msc.h	2009-01-31 17:35:56 UTC (rev 180)
+++ trunk/src/data/msc.h	2009-01-31 23:08:34 UTC (rev 181)
@@ -282,6 +282,19 @@
     m_marked = marked;
   }
 
+  /**
+   * \brief See MscElementTmpl for details about attribute original
+   */
+  virtual MscElement* get_general_original() const =0;
+
+  /**
+   * \brief See MscElementTmpl for details about attribute original
+   *
+   * Implementation of this method can throw bad cast exception
+   * in case original is not of appropriate type
+   */
+  virtual void set_general_original(MscElement* original)=0;
+
   virtual ~MscElement()
   {
     
@@ -343,6 +356,25 @@
   }
   
 public:
+
+  MscElement* get_general_original() const
+  {
+    return m_original.get();
+  }
+
+  void set_general_original(MscElement* original)
+  {
+    T* orig = dynamic_cast<T*>(original);
+    if(orig || !original)
+    {
+      set_original(orig);
+    }
+    else
+    {
+      throw std::bad_cast("Attribute m_original is not of desired type");
+    }
+  }
+
   /**
    * Getter for m_original.
    */

Modified: trunk/tests/race_checker_test.cpp
===================================================================
--- trunk/tests/race_checker_test.cpp	2009-01-31 17:35:56 UTC (rev 180)
+++ trunk/tests/race_checker_test.cpp	2009-01-31 23:08:34 UTC (rev 181)
@@ -302,12 +302,69 @@
   return check(hmsc1,true,true);
 }
 
+bool HMscF()
+{
+  std::cout << "HMscF:" << std::endl;
+
+  BMscPtr bmsc1(new BMsc("BMsc"));
+  InstancePtr instance1(new Instance("NAME"));
+  InstancePtr instance2(new Instance("NAME"));
+  InstancePtr instance3(new Instance("NAME"));
+  bmsc1->add_instance(instance1);
+  bmsc1->add_instance(instance2);
+  bmsc1->add_instance(instance3);
+
+  StrictOrderAreaPtr strict1(new StrictOrderArea());
+  instance1->add_area(strict1);
+
+  StrictOrderAreaPtr strict2(new StrictOrderArea());
+  instance2->add_area(strict2);
+
+  StrictOrderAreaPtr strict3(new StrictOrderArea());
+  instance3->add_area(strict3);  
+
+  EventPtr e1 = strict1->add_event();
+  EventPtr e2 = strict2->add_event();
+  CompleteMessagePtr m = new CompleteMessage("NAME");
+  m->glue_events(e1,e2);
+
+  e1 = strict2->add_event();
+  e2 = strict3->add_event();
+  m = new CompleteMessage("NAME");
+  m->glue_events(e1,e2);
+
+  e1 = strict2->add_event();
+  e2 = strict1->add_event();
+  m = new CompleteMessage("NAME");
+  m->glue_events(e1,e2);
+
+  e1 = strict3->add_event();
+  e2 = strict1->add_event();
+  m = new CompleteMessage("NAME");
+  m->glue_events(e1,e2);
+
+  HMscPtr hmsc1(new HMsc("HMsc"));
+  StartNodePtr start1 = new StartNode();
+  hmsc1->set_start(start1);
+  ReferenceNodePtr r1(new ReferenceNode());
+  EndNodePtr end1(new EndNode());
+  hmsc1->add_node(r1);
+  hmsc1->add_node(end1);
+  start1->add_successor(r1.get());
+  r1->add_successor(end1.get());
+
+  r1->set_msc(bmsc1);
+
+  return check(hmsc1,false,false);
+}
+
 int main(int argc, char** argv) {
-  //RETURN_IF_FAILED(HMscA());
+  RETURN_IF_FAILED(HMscA());
   RETURN_IF_FAILED(HMscB());
   RETURN_IF_FAILED(HMscC());
   RETURN_IF_FAILED(HMscD());
   RETURN_IF_FAILED(HMscE());
+  RETURN_IF_FAILED(HMscF());
   return 0;
 }
 


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




Thread: [Scstudio-commits] SF.net SVN: scstudio:[181] trunk (Page 2)

scstudio-commits