Menu
▾
▴
[Scstudio-commits] SF.net SVN: scstudio:[214] trunk
|
From: <va...@us...> - 2009-04-06 15:33:06
|
Revision: 214
http://scstudio.svn.sourceforge.net/scstudio/?rev=214&view=rev
Author: vacek
Date: 2009-04-06 15:32:54 +0000 (Mon, 06 Apr 2009)
Log Message:
-----------
First functional version of UniversalBoundednessChecker.
Modified Paths:
--------------
trunk/src/check/boundedness/universal_boundedness_checker.cpp
trunk/src/check/boundedness/universal_boundedness_checker.h
trunk/src/check/pseudocode/msc_duplicators.h
trunk/tests/universal_boundedness_checker_test.cpp
Modified: trunk/src/check/boundedness/universal_boundedness_checker.cpp
===================================================================
--- trunk/src/check/boundedness/universal_boundedness_checker.cpp 2009-03-31 16:50:47 UTC (rev 213)
+++ trunk/src/check/boundedness/universal_boundedness_checker.cpp 2009-04-06 15:32:54 UTC (rev 214)
@@ -21,6 +21,9 @@
UniversalBoundednessCheckerPtr UniversalBoundednessChecker::m_instance;
+const std::string UniversalBoundednessChecker::com_graph_attribute = "cograt";
+const std::string UniversalBoundednessChecker::vertex_number_attribute = "venuat";
+
void FindFirstNodeListener::on_white_node_found(HMscNode *n)
{
ReferenceNode* refnode = dynamic_cast<ReferenceNode*>(n);
@@ -75,6 +78,62 @@
{
m_where_to_add->add_node(n);
}
+
+void AssignListener::on_white_node_found(HMscNode *n)
+{
+ CommunicationGraph comgraph;
+ ReferenceNode* refnode;
+ refnode = dynamic_cast<ReferenceNode*>(n);
+ if(refnode)
+ {
+ comgraph.create_from_bmsc(refnode->get_bmsc());
+ refnode->set_attribute<CommunicationGraph>(UniversalBoundednessChecker::com_graph_attribute, comgraph);
+ }
+ n->set_attribute(UniversalBoundednessChecker::vertex_number_attribute, m_node_number++);
+}
+
+void CleanupListener::on_white_node_found(HMscNode *n)
+{
+ n->remove_attribute<CommunicationGraph>(UniversalBoundednessChecker::com_graph_attribute);
+ n->remove_attribute<unsigned>(UniversalBoundednessChecker::vertex_number_attribute);
+}
+
+
+void CycleListener::on_white_node_found(HMscNode *n)
+{
+ if(!dynamic_cast<ReferenceNode*>(n))
+ return;
+
+ TarjanCycles cycle_finder(m_vertex_count);
+ MscElementPListList cycle_list;
+ cycle_list = cycle_finder.circuit_enumeration(n);
+ CommunicationGraph cycle_graph;
+ MscElementPListList::const_iterator cycles;
+ MscElementPList::const_iterator items;
+
+
+ ReferenceNode *current_node;
+ for(cycles = cycle_list.begin(); cycles != cycle_list.end(); cycles++)
+ {
+ for(items = cycles->begin(); items != cycles->end(); items++)
+ {
+ current_node = dynamic_cast<ReferenceNode*>(*items);
+
+ if(current_node == NULL)
+ {
+ continue;
+ }
+
+ if(items == cycles->begin())
+ cycle_graph = current_node->get_attribute(UniversalBoundednessChecker::com_graph_attribute, cycle_graph);
+ else cycle_graph.merge(current_node->get_attribute(UniversalBoundednessChecker::com_graph_attribute, cycle_graph));
+
+ }
+ if(!cycle_graph.is_strongly_connected())
+ throw UnboundedCycleException();
+ }
+
+}
HMscPtr UniversalBoundednessChecker::create_duplicate_counter_example(const MscElementPListList& path)
{
HMscPathDuplicator duplicator;
@@ -102,12 +161,34 @@
return p;
}
+HMscPtr UniversalBoundednessChecker::create_counter_example(const MscElementPList& to_cycle, const MscElementPList& cycle)
+{
+ HMscPtr p;
+ HMscFlatPathDuplicator duplicator;
+ MscElementPList::const_iterator iter;
+ MscElementPList path;
+ for(iter = to_cycle.begin(); iter!=to_cycle.end(); iter++)
+ path.push_back(*iter);
+ for(iter = cycle.begin(); iter!=cycle.end(); iter++)
+ path.push_back(*iter);
+
+ p = duplicator.duplicate_path(path);
+
+ MscElementPList::const_iterator h;
+ for(h=path.begin();h!=path.end();h++)
+ {
+ duplicator.get_copy(*h)->set_marked(true);
+ }
+
+ return p;
+}
+
HMscPtr UniversalBoundednessChecker::check(HMscPtr hmsc, ChannelMapperPtr chm)
{
DFSHMscTraverser name_traverser, first_node_traverser;
NameChecker n_ch;
FindFirstNodeListener ffnl;
- HMscPtr p = NULL;
+ HMscPtr p(NULL);
MscElementPListList path_to_first;
name_traverser.add_white_node_found_listener(&n_ch);
first_node_traverser.add_white_node_found_listener(&ffnl);
@@ -128,16 +209,147 @@
catch(DuplicateNamesException)
{
p = create_duplicate_counter_example(name_traverser.get_reached_elements());
+ name_traverser.cleanup_traversing_attributes();
+ return p;
}
catch(InconsistentNamesException)
{
p = create_inconsistent_counter_example(name_traverser.get_reached_elements(), path_to_first);
+ name_traverser.cleanup_traversing_attributes();
+ return p;
}
- return p;
+
+ /* Here the main part of the checker begins */
+ BMscGraphDuplicator graph_duplicator;
+ HMscPtr transformed = graph_duplicator.duplicate_hmsc(hmsc);
+ DFSHMscTraverser msc_traverser;
+ AssignListener assigner;
+ CleanupListener cleaner;
+
+ //First, communication graphs and numbers are assigned to all the vertices.
+ msc_traverser.add_white_node_found_listener(&assigner);
+ msc_traverser.traverse(transformed);
+ //Notice that the checking traverser takes the number of vertices as a parameter.
+ CycleListener cycles(assigner.get_vertex_count());
+ msc_traverser.remove_all_listeners();
+
+
+ //This is the part performing the actual checking procedure.
+ msc_traverser.add_white_node_found_listener(&cycles);
+ try
+ {
+ msc_traverser.traverse(transformed);
+ }
+ catch(UnboundedCycleException)
+ {
+
+ p = create_counter_example(msc_traverser.get_reached_elements().back(), cycles.get_cycle());
+
+ msc_traverser.cleanup_traversing_attributes();
+ }
+ msc_traverser.remove_all_listeners();
+
+ //Finally, dynamic attributes are removed.
+ msc_traverser.add_white_node_found_listener(&cleaner);
+ msc_traverser.traverse(transformed);
+
+ return p;
}
void UniversalBoundednessChecker::cleanup_attributes()
{
}
+MscElementPListList TarjanCycles::circuit_enumeration(HMscNode *n)
+{
+ m_point_stack.clear();
+ m_marked_stack.clear();
+ m_mark.clear();
+ m_result.clear();
+ m_current_path.clear();
+ m_s = n->get_attribute(UniversalBoundednessChecker::vertex_number_attribute, 0);
+ m_mark.resize(m_vertex_count, false);
+
+ backtrack(n);
+
+
+
+ return m_result;
+}
+
+bool TarjanCycles::backtrack(HMscNode *n)
+{
+ bool f = false, g = false, some_f = false;
+ //The default value 0 is never to be used - the attribute is set for sure.
+ unsigned v = n->get_attribute(UniversalBoundednessChecker::vertex_number_attribute, 0);
+ unsigned j, w;
+
+ m_point_stack.push_back(v);
+ m_current_path.push_back(n); //!!
+ m_mark[v] = true;
+ m_marked_stack.push_back(v);
+ PredecessorNode* predecessor = dynamic_cast<PredecessorNode*>(n);
+ NodeRelationPtrSet::const_iterator relation;
+
+ //for all successors
+ if(predecessor)
+ {
+ for(relation=predecessor->get_successors().begin();
+ relation!=predecessor->get_successors().end();relation++)
+ {
+ const NodeRelationPtr& rel = *relation;
+
+ some_f = some_f || f;
+ f = false;
+ w = dynamic_cast<HMscNode*>(rel->get_successor())->get_attribute(UniversalBoundednessChecker::vertex_number_attribute, 0);
+
+ if(w < m_s)
+ continue;
+
+ if(w == m_s)
+ {
+ m_current_path.push_back(rel.get());
+ m_result.push_back(m_current_path);
+ m_current_path.pop_back();
+ f = true;
+ }
+ else if(!m_mark[w])
+ {
+ m_current_path.push_back(rel.get());
+ g = backtrack(dynamic_cast<HMscNode*>(rel->get_successor()));
+ m_current_path.pop_back();
+ f = f || g;
+ }
+
+ if(f == true)
+ {
+ j = m_marked_stack.size() - 1;
+ while(m_marked_stack[j] != v && j >=0)
+ {
+ m_mark[m_marked_stack[j]] = false;
+ m_marked_stack.pop_back();
+ j--;
+ }
+ if(j >= 0)
+ {
+ m_marked_stack.pop_back();
+ m_mark[v] = false;
+ }
+ }
+ }
+ }
+ if(!m_marked_stack.empty())
+ {
+ if(m_marked_stack.back()==v)
+ {
+ m_mark[v] = false;
+ m_marked_stack.pop_back();
+ }
+ }
+
+ m_point_stack.pop_back();
+ m_current_path.pop_back();
+ return some_f;
+}
+
// $Id$
Modified: trunk/src/check/boundedness/universal_boundedness_checker.h
===================================================================
--- trunk/src/check/boundedness/universal_boundedness_checker.h 2009-03-31 16:50:47 UTC (rev 213)
+++ trunk/src/check/boundedness/universal_boundedness_checker.h 2009-04-06 15:32:54 UTC (rev 214)
@@ -18,17 +18,38 @@
#include <vector>
#include <map>
+#include <iostream>
#include "data/checker.h"
#include "data/msc.h"
#include "check/boundedness/export.h"
#include "data/dfs_hmsc_traverser.h"
#include "data/dfs_bmsc_graph_traverser.h"
#include "check/pseudocode/communication_graph.h"
+#include "check/pseudocode/msc_duplicators.h"
class UniversalBoundednessChecker;
+
typedef boost::shared_ptr<UniversalBoundednessChecker> UniversalBoundednessCheckerPtr;
+class TarjanCycles
+{
+public:
+ MscElementPListList circuit_enumeration(HMscNode *n);
+ TarjanCycles(unsigned vertex_count)
+ :m_vertex_count(vertex_count)
+ {}
+private:
+ unsigned m_s; //the value of the root of the backtracking tree
+ MscElementPListList m_result; //needs to be shared among procedures
+ std::vector<unsigned> m_point_stack;
+ std::vector<unsigned> m_marked_stack;
+ MscElementPList m_current_path;
+ std::vector<bool> m_mark;
+ bool backtrack(HMscNode *n);
+ unsigned m_vertex_count;
+};
+
class InconsistentNamesException: public std::exception
{
public:
@@ -52,13 +73,58 @@
class FirstNodeFoundException: public std::exception
{
public:
-
const char* what()
{
return "First node found.";
}
};
+class UnboundedCycleException: public std::exception
+{
+public:
+ const char* what()
+ {
+ return "An unbounded cycle has been found.";
+ }
+};
+
+class AssignListener: public WhiteNodeFoundListener
+{
+public:
+ void on_white_node_found(HMscNode *n);
+ AssignListener()
+ :m_node_number(0)
+ {}
+ unsigned get_vertex_count(void)
+ {
+ return m_node_number;
+ }
+private:
+ unsigned m_node_number;
+};
+
+class CycleListener: public WhiteNodeFoundListener
+{
+public:
+ void on_white_node_found(HMscNode *n);
+ CycleListener(unsigned vertex_count)
+ :m_vertex_count(vertex_count)
+ {}
+ const MscElementPList get_cycle()
+ {
+ return m_unbounded_cycle;
+ }
+private:
+ unsigned m_vertex_count;
+ MscElementPList m_unbounded_cycle;
+};
+
+class CleanupListener: public WhiteNodeFoundListener
+{
+public:
+ void on_white_node_found(HMscNode *n);
+};
+
class FindFirstNodeListener: public WhiteNodeFoundListener
{
public:
@@ -73,6 +139,9 @@
public:
void on_white_node_found(HMscNode *n);
+ NameChecker()
+ :m_first_node(true)
+ {}
};
@@ -96,16 +165,20 @@
*/
static UniversalBoundednessCheckerPtr m_instance;
- std::map<std::string, HMscNode> m_test;
-
HMscPtr create_duplicate_counter_example(const MscElementPListList& path);
HMscPtr create_inconsistent_counter_example(const MscElementPListList& path1, const MscElementPListList& path2);
+ HMscPtr create_counter_example(const MscElementPList& to_cycle, const MscElementPList& cycle);
+
+
public:
UniversalBoundednessChecker(){};
+ static const std::string com_graph_attribute;
+ static const std::string vertex_number_attribute;
+
/**
* Human readable description of this check.
*/
@@ -131,7 +204,6 @@
return true;
}
- ~UniversalBoundednessChecker(){}
static UniversalBoundednessCheckerPtr instance()
{
Modified: trunk/src/check/pseudocode/msc_duplicators.h
===================================================================
--- trunk/src/check/pseudocode/msc_duplicators.h 2009-03-31 16:50:47 UTC (rev 213)
+++ trunk/src/check/pseudocode/msc_duplicators.h 2009-04-06 15:32:54 UTC (rev 214)
@@ -15,7 +15,8 @@
*
* $Id$
*/
-
+#ifndef _MSC_DUPLICATORS_H
+#define _MSC_DUPLICATORS_H
#include "data/msc.h"
#include "data/dfs_area_traverser.h"
#include "data/dfs_bmsc_graph_traverser.h"
@@ -210,7 +211,7 @@
*
* 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
+ * which don't occur in HMsc to be duplicated are removed. EndNodes
* of the same kind are transformed into ConnectionNodes referencing original
* EndNodes.
*/
@@ -230,7 +231,7 @@
/**
* \brief Duplicates path in HMsc.
*
- * The path is supposed to be generated by traversers -- similar srtucture.
+ * The path is supposed to be generated by traversers -- similar structure.
*/
class SCPSEUDOCODE_EXPORT HMscPathDuplicator:public Duplicator
{
@@ -256,4 +257,6 @@
HMscPtr duplicate_path(const MscElementPList& path, bool persist_original=true);
};
+#endif /* _MSC_DUPLICATORS_H */
+
// $Id$
Modified: trunk/tests/universal_boundedness_checker_test.cpp
===================================================================
--- trunk/tests/universal_boundedness_checker_test.cpp 2009-03-31 16:50:47 UTC (rev 213)
+++ trunk/tests/universal_boundedness_checker_test.cpp 2009-04-06 15:32:54 UTC (rev 214)
@@ -11,7 +11,7 @@
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
* Lesser General Public License for more details.
*
- * Copyright (c) 2009 V\xE1clav Vacek <va...@ic...>
+ * Copyright (c) 2009 V\xE1clav Vacek <va...@ic...>
*
* $Id$
*/
@@ -44,7 +44,7 @@
if(hmsc.get())
{
result = true;
- std::cout << "OK: HMsc is supposed not to be universally bounded and it isnt't."
+ std::cout << "OK: HMsc is supposed not to be universally bounded and it isn't."
<< std::endl;
}
else
@@ -54,15 +54,17 @@
<< std::endl;
}
std::cout << std::endl;
+
return result;
}
bool check(HMscPtr hmsc,const bool is_bounded)
{
UniversalBoundednessCheckerPtr checker = UniversalBoundednessChecker::instance();
+
SRChannelMapperPtr srm = SRChannelMapper::instance();
- return print_result(checker->check(hmsc,srm),is_bounded);
+ return print_result(checker->check(hmsc,srm),is_bounded);
}
bool HMscA() {
@@ -112,12 +114,18 @@
}
bool HMscB() {
- std::cout << "Checking this bmsc in a cycle:" << std::endl;
+ std::cout << "Checking these bmscs in a cycle:" << std::endl;
std::cout << " p1 p2 " << std::endl;
std::cout << " | | " << std::endl;
std::cout << "e1 O-----a----->O e2" << std::endl;
std::cout << " | | " << std::endl;
std::cout << " | | " << std::endl;
+ std::cout << std::endl;
+ std::cout << " p1 p2 " << std::endl;
+ std::cout << " | | " << std::endl;
+ std::cout << "e3 O<----a------O e4" << std::endl;
+ std::cout << " | | " << std::endl;
+ std::cout << " | | " << std::endl;
BMscPtr bmsc2(new BMsc());
@@ -137,24 +145,95 @@
CompleteMessagePtr m1 = new CompleteMessage("a");
m1->glue_events(e1, e2);
- HMscPtr hmsc2(new HMsc("HMsc1"));
+ //////////////
+ BMscPtr bmsc3(new BMsc());
+
+ InstancePtr i3(new Instance("p1"));
+ bmsc3->add_instance(i3);
+ InstancePtr i4(new Instance("p2"));
+ bmsc3->add_instance(i4);
+
+ EventAreaPtr a3(new StrictOrderArea());
+ i3->add_area(a3);
+ EventAreaPtr a4(new StrictOrderArea());
+ i4->add_area(a4);
+
+ EventPtr e3 = a3->add_event();
+ EventPtr e4 = a4->add_event();
+
+ CompleteMessagePtr m2 = new CompleteMessage("a");
+ m2->glue_events(e4, e3);
+
+ HMscPtr hmsc2(new HMsc("HMsc2"));
StartNodePtr start1 = new StartNode();
hmsc2->set_start(start1);
ReferenceNodePtr r1_1(new ReferenceNode());
+ ReferenceNodePtr r1_2(new ReferenceNode());
EndNodePtr end1(new EndNode());
hmsc2->add_node(r1_1);
+ hmsc2->add_node(r1_2);
hmsc2->add_node(end1);
start1->add_successor(r1_1.get());
+ r1_1->add_successor(r1_2.get());
+ r1_2->add_successor(end1.get());
+ r1_2->add_successor(r1_1.get());
+ r1_1->set_msc(bmsc2);
+ r1_2->set_msc(bmsc3);
+
+ return check(hmsc2,true);
+}
+
+bool HMscC() {
+ std::cout << "Checking this bmsc in a cycle:" << std::endl;
+ std::cout << " p1 p2 " << std::endl;
+ std::cout << " | | " << std::endl;
+ std::cout << "e1 O-----a----->O e2" << std::endl;
+ std::cout << " | | " << std::endl;
+ std::cout << " | | " << std::endl;
+
+ BMscPtr bmsc1(new BMsc());
+
+ InstancePtr i1(new Instance("p1"));
+ bmsc1->add_instance(i1);
+ InstancePtr i2(new Instance("p2"));
+ bmsc1->add_instance(i2);
+
+ EventAreaPtr a1(new StrictOrderArea());
+ i1->add_area(a1);
+ EventAreaPtr a2(new StrictOrderArea());
+ i2->add_area(a2);
+
+ EventPtr e1 = a1->add_event();
+ EventPtr e2 = a2->add_event();
+
+ CompleteMessagePtr m1 = new CompleteMessage("a");
+ m1->glue_events(e1, e2);
+
+
+ HMscPtr hmsc1(new HMsc("HMsc1"));
+ StartNodePtr start1 = new StartNode();
+ hmsc1->set_start(start1);
+ ReferenceNodePtr r1_1(new ReferenceNode());
+ EndNodePtr end1(new EndNode());
+ hmsc1->add_node(r1_1);
+ hmsc1->add_node(end1);
+ start1->add_successor(r1_1.get());
r1_1->add_successor(end1.get());
r1_1->add_successor(r1_1.get());
- r1_1->set_msc(bmsc2);
+ r1_1->set_msc(bmsc1);
- return check(hmsc2,false);
+ return check(hmsc1,false);
}
int main(int argc, char** argv) {
+
RETURN_IF_FAILED(HMscA());
+
RETURN_IF_FAILED(HMscB());
+
+ RETURN_IF_FAILED(HMscC());
+
+ ;
/*CommunicationGraph tester;
std::vector<std::vector<unsigned> > test_graph, test_graph_matrix;
const int g_s = 6;
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
