Menu
▾
▴
[Scstudio-commits] SF.net SVN: scstudio:[181] trunk
|
From: <ba...@us...> - 2009-01-31 23:08:43
|
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.
|
