Menu
▾
▴
[Scstudio-commits] SF.net SVN: scstudio:[165] trunk/src
|
From: <ba...@us...> - 2009-01-11 19:50:42
|
Revision: 165
http://scstudio.svn.sourceforge.net/scstudio/?rev=165&view=rev
Author: babicaj
Date: 2009-01-11 19:50:35 +0000 (Sun, 11 Jan 2009)
Log Message:
-----------
deadlock checker returns proper counter example
Modified Paths:
--------------
trunk/src/check/liveness/CMakeLists.txt
trunk/src/check/liveness/deadlock_checker.cpp
trunk/src/check/pseudocode/msc_duplicators.cpp
trunk/src/check/pseudocode/msc_duplicators.h
trunk/src/data/msc.cpp
trunk/src/data/msc.h
Modified: trunk/src/check/liveness/CMakeLists.txt
===================================================================
--- trunk/src/check/liveness/CMakeLists.txt 2009-01-11 17:57:54 UTC (rev 164)
+++ trunk/src/check/liveness/CMakeLists.txt 2009-01-11 19:50:35 UTC (rev 165)
@@ -9,6 +9,7 @@
TARGET_LINK_LIBRARIES(scliveness
scmsc
+ scpseudocode
)
INSTALL(TARGETS scliveness
Modified: trunk/src/check/liveness/deadlock_checker.cpp
===================================================================
--- trunk/src/check/liveness/deadlock_checker.cpp 2009-01-11 17:57:54 UTC (rev 164)
+++ trunk/src/check/liveness/deadlock_checker.cpp 2009-01-11 19:50:35 UTC (rev 165)
@@ -18,6 +18,7 @@
#include "data/dfsb_hmsc_traverser.h"
#include "check/liveness/deadlock_checker.h"
+#include "check/pseudocode/msc_duplicators.h"
DeadlockCheckerPtr DeadlockChecker::m_instance;
@@ -124,36 +125,14 @@
HMscPtr DeadlockChecker::create_counter_example(const MscElementPListList& path)
{
-// InnerNodePListList::const_iterator hmscs_it;
-// HMscPtr result;
-// for (hmscs_it = path.begin(); hmscs_it != path.end(); hmscs_it++)
-// {
-// HMscPtr current_hmsc;
-// InnerNode* last_node = NULL;
-// InnerNodePList::const_iterator nodes_it;
-// for (nodes_it = hmscs_it->begin(); nodes_it != hmscs_it->end(); nodes_it++)
-// {
-// if (last_node == NULL)
-// {
-// if (dynamic_cast<ReferenceNode*> (*nodes_it) != NULL)
-// last_node = new ReferenceNode((ReferenceNode*) * nodes_it);
-// else
-// last_node = new ConnectionNode((ConnectionNode*) * nodes_it);
-// current_hmsc = new HMsc((*nodes_it)->get_owner());
-// current_hmsc = set_start(new StartNode((*nodes_it)->get_owner()->get_start().get()));
-// current_hmsc->get_start()->add_successor(last_node);
-// if (!result.get())
-// result = current_hmsc;
-// }
-// else
-// {
-// last_node->add_successor(*nodes_it);
-// last_node = *nodes_it;
-// }
-// }
-// }
-// return result;
- HMscPtr example = new HMsc("counter example");
+ HMscPathDuplicator duplicator;
+ HMscPtr example = duplicator.duplicate_path(path);
+ MscElementPListList::const_iterator h;
+ for(h=path.begin();h!=path.end();h++)
+ {
+ MscElement* last = (*h).back();
+ duplicator.get_copy(last)->set_marked(true);
+ }
return example;
}
Modified: trunk/src/check/pseudocode/msc_duplicators.cpp
===================================================================
--- trunk/src/check/pseudocode/msc_duplicators.cpp 2009-01-11 17:57:54 UTC (rev 164)
+++ trunk/src/check/pseudocode/msc_duplicators.cpp 2009-01-11 19:50:35 UTC (rev 165)
@@ -24,7 +24,38 @@
const std::string BMSC_GRAPH_DUPLICATOR_COPY_ATTR = "BGDcopy";
const std::string BMSC_GRAPH_DUPLICATOR_REF_ATTR = "BGDreferencing";
const std::string BMSC_GRAPH_DUPLICATOR_ENDLIST_ATTR = "BGDendlist";
+const std::string DUPLICATOR_COPY_ATTR = "Dcopy";
+Duplicator::Duplicator()
+{
+}
+
+Duplicator::~Duplicator()
+{
+ MscElementPList::const_iterator i;
+ for(i=m_modified_elements.begin();i!=m_modified_elements.end();i++)
+ {
+ (*i)->remove_attribute<MscElement*>(DUPLICATOR_COPY_ATTR);
+ }
+}
+
+MscElement*& Duplicator::get_copy(MscElement* e)
+{
+ bool just_set;
+ MscElement*& copy = e->get_attribute<MscElement*>(DUPLICATOR_COPY_ATTR,NULL,just_set);
+ if(just_set)
+ {
+ m_modified_elements.push_back(e);
+ }
+ return copy;
+}
+
+void Duplicator::set_copy(MscElement* original, MscElement* copy)
+{
+ MscElement*& c = get_copy(original);
+ c = copy;
+}
+
BMscDuplicator::BMscDuplicator()
{
}
@@ -488,4 +519,92 @@
return new_hmsc;
}
+HMscPtr HMscPathDuplicator::duplicate_path(const MscElementPListList& path)
+{
+ HMscPtr root;
+ if(path.size()>0)
+ {
+ MscElementPListList::const_iterator h;
+ PredecessorNode* new_pred(NULL);
+ for(h=path.begin();h!=path.end();h++)
+ {
+ HMscPtr new_hmsc;
+ NodeRelation* old_rel(NULL);
+ MscElementPList::const_iterator e;
+ for(e=(*h).begin();e!=(*h).end();e++)
+ {
+ if(e==(*h).begin())
+ {
+ StartNode* start = dynamic_cast<StartNode*>(*e);
+ new_hmsc = new HMsc(start->get_owner());
+ if(!root.get())
+ {
+ root = new_hmsc;
+ }
+ else
+ {
+ //hmsc is surely referenced from ReferenceNode
+ ReferenceNode* ref = dynamic_cast<ReferenceNode*>(new_pred);
+ ref->set_msc(new_hmsc);
+ }
+ StartNode* new_start = new StartNode(start);
+ new_hmsc->set_start(new_start);
+ new_pred = new_start;
+ set_copy(start,new_start);
+ set_copy(start->get_owner(),new_hmsc.get());
+ }
+ else
+ {
+ NodeRelation* rel = dynamic_cast<NodeRelation*>(*e);
+ if(rel)
+ {
+ old_rel = rel;
+ }
+ else
+ {
+ ReferenceNode* ref_node = dynamic_cast<ReferenceNode*>(*e);
+ NodeRelationPtr new_rel;
+ if(ref_node)
+ {
+ ReferenceNode* new_ref = new ReferenceNode(ref_node);
+ new_hmsc->add_node(new_ref);
+ new_rel = new_ref->add_predecessor(new_pred);
+ new_pred = new_ref;
+ set_copy(ref_node,new_ref);
+ }
+ else
+ {
+ ConnectionNode* con_node = dynamic_cast<ConnectionNode*>(*e);
+ if(con_node)
+ {
+ ConnectionNode* new_con = new ConnectionNode(con_node);
+ new_hmsc->add_node(new_con);
+ new_rel = new_con->add_predecessor(new_pred);
+ new_pred = new_con;
+ set_copy(con_node,new_con);
+ }
+ else
+ {
+ EndNode* end_node = dynamic_cast<EndNode*>(*e);
+ EndNode* new_end = new EndNode(end_node);
+ new_rel = new_end->add_predecessor(new_pred);
+ new_hmsc->add_node(new_end);
+ set_copy(end_node,new_end);
+ }
+ }
+ new_rel->set_original(old_rel);
+ new_rel->set_line(old_rel->get_line());
+ set_copy(old_rel,new_rel.get());
+ }
+ }
+ }
+ }
+ }
+ return root;
+}
+
+HMscPathDuplicator::~HMscPathDuplicator()
+{
+}
+
// $Id$
Modified: trunk/src/check/pseudocode/msc_duplicators.h
===================================================================
--- trunk/src/check/pseudocode/msc_duplicators.h 2009-01-11 17:57:54 UTC (rev 164)
+++ trunk/src/check/pseudocode/msc_duplicators.h 2009-01-11 19:50:35 UTC (rev 165)
@@ -26,6 +26,23 @@
typedef std::list<HMsc*> HMscPList;
typedef std::list<ConnectionNode*> ConnectionNodePList;
+class SCPSEUDOCODE_EXPORT Duplicator
+{
+protected:
+
+ MscElementPList m_modified_elements;
+
+ Duplicator();
+
+public:
+
+ virtual ~Duplicator();
+
+ MscElement*& get_copy(MscElement* e);
+
+ void set_copy(MscElement* original, MscElement* copy);
+};
+
class BMscDuplicator;
class EventsCreatorListener:
@@ -186,4 +203,18 @@
};
+/**
+ * \brief Duplicates path in HMsc.
+ *
+ * The path is supposed to be generated by traversers -- similar srtucture.
+ */
+class SCPSEUDOCODE_EXPORT HMscPathDuplicator:public Duplicator
+{
+public:
+
+ ~HMscPathDuplicator();
+
+ HMscPtr duplicate_path(const MscElementPListList& path);
+};
+
// $Id$
Modified: trunk/src/data/msc.cpp
===================================================================
--- trunk/src/data/msc.cpp 2009-01-11 17:57:54 UTC (rev 164)
+++ trunk/src/data/msc.cpp 2009-01-11 19:50:35 UTC (rev 165)
@@ -32,6 +32,16 @@
pred->m_successors.insert(this);
}
+void NodeRelation::set_line(const PolyLine& line)
+{
+ m_line = line;
+}
+
+const PolyLine& NodeRelation::get_line()
+{
+ return m_line;
+}
+
void SuccessorNode::remove_predecessor(const NodeRelationPtr& n)
{
m_predecessors.erase(n);
@@ -71,6 +81,10 @@
HMscNode::HMscNode(HMscNode* original):MscElementTmpl<HMscNode>(original),
m_owner(NULL)
{
+ if(original)
+ {
+ m_position = original->get_position();
+ }
}
HMscNodePtr HMscNode::my_ptr()
Modified: trunk/src/data/msc.h
===================================================================
--- trunk/src/data/msc.h 2009-01-11 17:57:54 UTC (rev 164)
+++ trunk/src/data/msc.h 2009-01-11 19:50:35 UTC (rev 165)
@@ -368,6 +368,10 @@
Msc(Msc* original):MscElementTmpl<Msc>(original)
{
+ if(original)
+ {
+ m_label = original->get_label();
+ }
}
public:
@@ -532,6 +536,10 @@
* Connects to a given PredecessorNode and re-configures its back pointer.
*/
void set_predecessor(PredecessorNode* pred);
+
+ void set_line(const PolyLine& line);
+
+ const PolyLine& get_line();
};
typedef boost::intrusive_ptr<NodeRelation> NodeRelationPtr;
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
