Menu
▾
▴
[Scstudio-commits] SF.net SVN: scstudio:[119] trunk
|
From: <ba...@us...> - 2008-11-17 19:46:28
|
Revision: 119
http://scstudio.svn.sourceforge.net/scstudio/?rev=119&view=rev
Author: babicaj
Date: 2008-11-17 19:46:26 +0000 (Mon, 17 Nov 2008)
Log Message:
-----------
livelock_checker_test should be able to be compiled, memory leaks found in regress tests should be removed, new dfs_refnode_hmsc_traverser was added - see comments in header file for details, fifo_checker_test was modified to comply with tests
Modified Paths:
--------------
trunk/src/check/CMakeLists.txt
trunk/src/check/dfs_bmsc_graph_traverser.cpp
trunk/src/check/dfs_bmsc_graph_traverser.h
trunk/src/check/livelock_checker.cpp
trunk/src/check/livelock_checker.h
trunk/src/check/refnode_finder.cpp
trunk/src/check/refnode_finder.h
trunk/src/check/visual_closure_initiator.cpp
trunk/src/check/visual_closure_initiator.h
trunk/tests/CMakeLists.txt
trunk/tests/fifo_checker_test.cpp
trunk/tests/livelock_checker_test.cpp
Added Paths:
-----------
trunk/src/check/dfs_refnode_hmsc_traverser.cpp
trunk/src/check/dfs_refnode_hmsc_traverser.h
Modified: trunk/src/check/CMakeLists.txt
===================================================================
--- trunk/src/check/CMakeLists.txt 2008-11-16 21:58:38 UTC (rev 118)
+++ trunk/src/check/CMakeLists.txt 2008-11-17 19:46:26 UTC (rev 119)
@@ -5,7 +5,7 @@
ADD_LIBRARY(dfsb_hmsc_traverser STATIC dfsb_hmsc_traverser.cpp)
ADD_LIBRARY(dfs_instance_events_traverser STATIC dfs_instance_events_traverser.cpp)
ADD_LIBRARY(dfs_bmsc_graph_traverser STATIC dfs_bmsc_graph_traverser.cpp)
-#ADD_LIBRARY(refnode_finder STATIC refnode_finder.cpp)
+ADD_LIBRARY(refnode_finder STATIC refnode_finder.cpp)
#order relation
#ADD_LIBRARY(causal_closure_initiator STATIC causal_closure_initiator.cpp)
@@ -15,7 +15,7 @@
#ADD_LIBRARY(acyclic_checker STATIC acyclic_checker.cpp)
ADD_LIBRARY(deadlock_checker STATIC deadlock_checker.cpp)
ADD_LIBRARY(fifo_checker STATIC fifo_checker.cpp)
-#ADD_LIBRARY(livelock_checker STATIC livelock_checker.cpp)
+ADD_LIBRARY(livelock_checker STATIC livelock_checker.cpp)
#ADD_LIBRARY(race_checker STATIC race_checker.cpp)
#other
Modified: trunk/src/check/dfs_bmsc_graph_traverser.cpp
===================================================================
--- trunk/src/check/dfs_bmsc_graph_traverser.cpp 2008-11-16 21:58:38 UTC (rev 118)
+++ trunk/src/check/dfs_bmsc_graph_traverser.cpp 2008-11-17 19:46:26 UTC (rev 119)
@@ -209,3 +209,14 @@
m_reached_elements.push_back(MscElementPList());
}
+Color DFSBMscGraphTraverser::get_color(HMscNode* n)
+{
+ bool just_set;
+ Color c = n->get_attribute<Color>(m_color_attribute,WHITE,just_set);
+ if(just_set)
+ {
+ m_colored_nodes.back().push_back(n);
+ }
+ return c;
+}
+
Modified: trunk/src/check/dfs_bmsc_graph_traverser.h
===================================================================
--- trunk/src/check/dfs_bmsc_graph_traverser.h 2008-11-16 21:58:38 UTC (rev 118)
+++ trunk/src/check/dfs_bmsc_graph_traverser.h 2008-11-17 19:46:26 UTC (rev 119)
@@ -435,10 +435,7 @@
*
* If attribute isn't set it is set to default value WHITE.
*/
- Color get_color(HMscNode* n)
- {
- return n->get_attribute<Color>(m_color_attribute,WHITE);
- }
+ Color get_color(HMscNode* n);
virtual void push_top_attributes();
Added: trunk/src/check/dfs_refnode_hmsc_traverser.cpp
===================================================================
--- trunk/src/check/dfs_refnode_hmsc_traverser.cpp (rev 0)
+++ trunk/src/check/dfs_refnode_hmsc_traverser.cpp 2008-11-17 19:46:26 UTC (rev 119)
@@ -0,0 +1,34 @@
+/*
+ * scstudio - Sequence Chart Studio
+ * http://scstudio.sourceforge.net
+ *
+ * This library is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU Lesser General Public
+ * License version 2.1, as published by the Free Software Foundation.
+ *
+ * This library is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+ * Lesser General Public License for more details.
+ *
+ * Copyright (c) 2008 Jindra Babica <ba...@ma...>
+ *
+ * $Id: dfs_hmsc_traverser.h 117 2008-11-16 20:19:35Z babicaj $
+ */
+
+#include "dfs_refnode_hmsc_traverser.h"
+
+bool DFSRefNodeHMscTraverser::traverse_successors(PredecessorNode* predecessor)
+{
+ bool end_found = false;
+ HMscNodePListPtr successors = m_finder.find_successors(dynamic_cast<HMscNode*>(predecessor));
+ m_finder.cleanup_traversing_attributes();
+ //TODO: m_reached_elements should contain path to succ
+ HMscNodePList::const_iterator succ;
+ for(succ=successors->begin();succ!=successors->end();succ++)
+ {
+ end_found = traverse_node(*succ) || end_found;
+ }
+ return end_found;
+}
+
Added: trunk/src/check/dfs_refnode_hmsc_traverser.h
===================================================================
--- trunk/src/check/dfs_refnode_hmsc_traverser.h (rev 0)
+++ trunk/src/check/dfs_refnode_hmsc_traverser.h 2008-11-17 19:46:26 UTC (rev 119)
@@ -0,0 +1,61 @@
+/*
+ * scstudio - Sequence Chart Studio
+ * http://scstudio.sourceforge.net
+ *
+ * This library is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU Lesser General Public
+ * License version 2.1, as published by the Free Software Foundation.
+ *
+ * This library is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+ * Lesser General Public License for more details.
+ *
+ * Copyright (c) 2008 Jindra Babica <ba...@ma...>
+ *
+ * $Id: dfs_hmsc_traverser.h 117 2008-11-16 20:19:35Z babicaj $
+ */
+
+#ifndef _DFS_REFNODE_HMSC_TRAVERSER_H
+#define _DFS_REFNODE_HMSC_TRAVERSER_H
+
+#include "check/dfs_bmsc_graph_traverser.h"
+#include "check/refnode_finder.h"
+
+
+/**
+ * Traverses nodes in HMsc and referenced HMsc in depth first
+ * search manner like DFSBMscGraphTraverser. Unlike DFSBMscGraphTraverser
+ * this traverser handles ConnectionNodes like it would be
+ * only edge of graph. I.e. user of this traverser and connected
+ * listeners to this traverser can suppose that HMsc is graph
+ * consisting of StartNodes, EndNodes and ReferenceNodes.
+ * Moreover this traverser traverses each HMsc only one time.
+ */
+class DFSRefNodeHMscTraverser:
+ public DFSBMscGraphTraverser,public WhiteNodeFoundListener,
+ public GrayNodeFoundListener,public BlackNodeFoundListener,
+ public NodeFinishedListener
+{
+
+protected:
+
+ bool traverse_successors(PredecessorNode* predecessor);
+ ReferenceNodeFinder m_finder;
+
+public:
+
+ DFSRefNodeHMscTraverser(
+ const std::string& color_attribute = "DFSRNHMT_color"):
+ DFSBMscGraphTraverser(color_attribute)
+ {
+
+ }
+
+ void cleanup_traversing_attributes();
+
+};
+
+
+#endif /* _DFS_REFNODE_HMSC_TRAVERSER_H */
+
Modified: trunk/src/check/livelock_checker.cpp
===================================================================
--- trunk/src/check/livelock_checker.cpp 2008-11-16 21:58:38 UTC (rev 118)
+++ trunk/src/check/livelock_checker.cpp 2008-11-17 19:46:26 UTC (rev 119)
@@ -18,95 +18,117 @@
#include "check/livelock_checker.h"
-const std::string LivelockListener::m_reachable_attribute = "livelock_reachable";
+const std::string ATTRIBUTE_REACHABLE = "LL_reachable";
+
LivelockCheckerPtr LivelockChecker::m_instance;
-void LivelockListener::mark_reachable(InnerNode* node){
- set_reachable(node);
- const InnerNodePSet& pre = node->get_predecessors();
+LivelockReachableMarker::LivelockReachableMarker(LivelockListener* ll):
+ m_ll(ll)
+{
+}
- InnerNodePSet::const_iterator it;
- for(it = pre.begin(); it != pre.end(); it++)
+void LivelockReachableMarker::on_white_node_found(HMscNode* n)
+{
+ bool& reachable = m_ll->get_reachable(n);
+ reachable = true;
+}
+
+LivelockListener::LivelockListener()
+{
+ m_marker = LivelockReachableMarker(this);
+ m_traverser = DFSBHMscTraverser("LL_color");
+ m_traverser.add_white_node_found_listener(&m_marker);
+}
+
+void LivelockListener::mark_reachable(HMscNode* node)
+{
+ m_traverser.traverse(node);
+}
+
+void LivelockListener::cleanup_attributes(){
+ while(!m_marked_elements.empty())
{
- if(!get_reachable(node))
- mark_reachable(*it);
+ HMscNode* p = m_marked_elements.back();
+ p->remove_attribute<bool>(ATTRIBUTE_REACHABLE);
+ m_marked_elements.pop_back();
}
}
-void LivelockListener::find_refnode(InnerNode* n){
- InnerNodePListList path = m_traverser.get_reached_nodes();
- InnerNodePListList::reverse_iterator hmsc_it;
- InnerNodePList::reverse_iterator node_rit;
-
- hmsc_it = path.rbegin();
+void LivelockListener::on_white_node_found(HMscNode* node)
+{
+ if(dynamic_cast<EndNode*>(node))
+ {
+ mark_reachable(node);
+ }
+}
- for(node_rit=hmsc_it->rbegin(); *node_rit!=n; ++node_rit){
- ReferenceNode* ref = dynamic_cast<ReferenceNode*>(*node_rit);
- if(ref!=NULL)
- {
- throw LivelockException();
- }
+void LivelockListener::on_gray_node_found(HMscNode* n)
+{
+ if(dynamic_cast<ReferenceNode*>(n) && !get_reachable(n)){
+ throw LivelockException();
}
}
+LivelockListener::~LivelockListener()
+{
+ cleanup_attributes();
+}
-
-HMscPtr LivelockChecker::create_counter_example(const InnerNodePListList& path)
+bool& LivelockListener::get_reachable(HMscNode* node)
{
- InnerNodePListList::const_iterator hmscs_it;
- HMscPtr result;
- for(hmscs_it=path.begin();hmscs_it!=path.end();hmscs_it++)
+ bool just_set;
+ return node->get_attribute<bool>(ATTRIBUTE_REACHABLE,false,just_set);
+ if(just_set)
{
- 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->get_start()->add_successor(last_node);
- if(!result.get())
- result = current_hmsc;
- }
- else
- {
- last_node->add_successor(*nodes_it);
- last_node = *nodes_it;
- }
- }
+ m_marked_elements.push_back(node);
}
- return result;
}
HMscPtr LivelockChecker::check(HMscPtr hmsc, ChannelMapperPtr chm)
{
HMscPtr p;
- DFSHMscTraverser traverser;
+ DFSHMscTraverser traverser("LC_color");
LivelockListener listener;
- listener.set_traverser(traverser);
traverser.add_white_node_found_listener(&listener);
- traverser.traverse(hmsc);
- traverser.remove_white_node_found_listeners();
-
traverser.add_gray_node_found_listener(&listener);
try
{
- traverser.traverse(hmsc);
+ traverser.traverse(hmsc);
}
catch(LivelockException& e)
{
- p = create_counter_example(traverser.get_reached_nodes());
- traverser.cleanup_traversing_attributes();
+ p = create_counter_example(traverser.get_reached_elements());
}
-
return p;
}
+
+LivelockChecker::LivelockChecker()
+{
+}
+
+HMscPtr LivelockChecker::create_counter_example(const MscElementPListList& path)
+{
+ HMscPtr e = HMscPtr(new HMsc("Erroneous path"));
+ return e;
+}
+
+LivelockCheckerPtr LivelockChecker::instance()
+{
+ if(!m_instance.get())
+ m_instance = new LivelockChecker();
+ return m_instance;
+}
+
+bool LivelockChecker::is_supported(ChannelMapperPtr chm)
+{
+ return true;
+}
+
+LivelockChecker::~LivelockChecker()
+{
+};
+void LivelockChecker::cleanup_attributes()
+{
+};
-
-
Modified: trunk/src/check/livelock_checker.h
===================================================================
--- trunk/src/check/livelock_checker.h 2008-11-16 21:58:38 UTC (rev 118)
+++ trunk/src/check/livelock_checker.h 2008-11-17 19:46:26 UTC (rev 119)
@@ -20,6 +20,7 @@
#include "data/msc.h"
#include "data/counted_ptr.h"
#include "check/dfs_hmsc_traverser.h"
+#include "check/dfsb_hmsc_traverser.h"
#include <string>
#include <stack>
@@ -46,84 +47,44 @@
}
};
-class LivelockListener:public WhiteRefNodeFoundListener, public GrayRefNodeFoundListener
+class LivelockReachableMarker:public WhiteNodeFoundListener
{
+
+ LivelockListener* m_ll;
+
+public:
+
+ LivelockReachableMarker(LivelockListener* ll=NULL);
+
+ void on_white_node_found(HMscNode* n);
+
+};
+
+class LivelockListener:public WhiteNodeFoundListener, public GrayNodeFoundListener
+{
private:
- // stack of InnerNodes with reachable element to be clean up
- InnerNodePStack m_reachable_elements;
- // actual traverser
- DFSHMscTraverser m_traverser;
- /**
- * recursive function, marking node as reachable and calling itself on node's predecessors
- * \param node to be mark
- */
- void mark_reachable(InnerNode* node);
+ HMscNodePList m_marked_elements;
- bool get_reachable(InnerNode* node)
- {
- return node->get_attribute<bool>(m_reachable_attribute,false);
- }
-
- void set_reachable(InnerNode* node)
- {
- node->set_attribute<bool>(m_reachable_attribute,true);
- m_reachable_elements.push(node);
- }
+ LivelockReachableMarker m_marker;
- void cleanup_attribute(){
- while(!m_reachable_elements.empty())
- {
- InnerNode* p = m_reachable_elements.top();
- p->remove_attribute<bool>(m_reachable_attribute);
- m_reachable_elements.pop();
- }
- }
- // goes throw the path trying to find reference node in the cyrcle
- void find_refnode(InnerNode* n);
+ DFSBHMscTraverser m_traverser;
+
+ void mark_reachable(HMscNode* node);
+
+ void cleanup_attributes();
-protected:
- static const std::string m_reachable_attribute;
public:
- void check(HMscPtr hmsc);
- void set_traverser(DFSHMscTraverser traverser)
- {
- m_traverser = traverser;
- }
+ LivelockListener();
- void on_white_node_found(InnerNode* node)
- {
- if(node->is_end_node() && !get_reachable(node))
- {
- mark_reachable(node);
- }
- }
+ ~LivelockListener();
- void on_white_node_found(ReferenceNode* node){}
+ void on_white_node_found(HMscNode* node);
- virtual void on_gray_node_found(InnerNode* n)
- {
- if(!get_reachable(n)){
- // if its false, attribute has been set, so its pushed for clean up
- m_reachable_elements.push(n);
- ReferenceNode* ref = dynamic_cast<ReferenceNode*>(n);
- if(ref!=NULL)
- {
- throw LivelockException();
- }
- else find_refnode(n);
- }
- }
+ virtual void on_gray_node_found(HMscNode* n);
- void on_gray_node_found(ReferenceNode* node)
- {
- }
-
- ~LivelockListener()
- {
- cleanup_attribute();
- }
+ bool& get_reachable(HMscNode* node);
};
@@ -140,27 +101,20 @@
*/
static LivelockCheckerPtr m_instance;
- LivelockChecker(){};
- HMscPtr create_counter_example(const InnerNodePListList& path);
+ LivelockChecker();
+ HMscPtr create_counter_example(const MscElementPListList& path);
public:
- static LivelockCheckerPtr instance()
- {
- if(!m_instance.get())
- m_instance = new LivelockChecker();
- return m_instance;
- }
+
+ static LivelockCheckerPtr instance();
- bool is_supported(ChannelMapperPtr chm)
- {
- return true;
- }
+ bool is_supported(ChannelMapperPtr chm);
- ~LivelockChecker(){};
+ ~LivelockChecker();
HMscPtr check(HMscPtr h, ChannelMapperPtr chm);
- void cleanup_attributes(){};
+ void cleanup_attributes();
};
Modified: trunk/src/check/refnode_finder.cpp
===================================================================
--- trunk/src/check/refnode_finder.cpp 2008-11-16 21:58:38 UTC (rev 118)
+++ trunk/src/check/refnode_finder.cpp 2008-11-17 19:46:26 UTC (rev 119)
@@ -41,3 +41,13 @@
//return value is no more needed
return true;
}
+
+HMscNodePListPtr ReferenceNodeFinder::find_successors(HMscNode* node)
+{
+ HMscNodePListPtr successors(new HMscNodePList);
+ ReferenceNodeFinderListener l(successors.get());
+ add_white_node_found_listener(&l);
+ traverse_node(node);
+ remove_white_node_found_listeners();
+ return successors;
+}
Modified: trunk/src/check/refnode_finder.h
===================================================================
--- trunk/src/check/refnode_finder.h 2008-11-16 21:58:38 UTC (rev 118)
+++ trunk/src/check/refnode_finder.h 2008-11-17 19:46:26 UTC (rev 119)
@@ -19,8 +19,51 @@
#ifndef _REFNODE_FINDER_H
#define _REFNODE_FINDER_H
+#include <list>
#include "check/dfs_bmsc_graph_traverser.h"
+typedef std::list<HMscNode*> HMscNodePList;
+typedef counted_ptr<HMscNodePList> HMscNodePListPtr;
+
+class ReferenceNodeFinderListener:
+ public WhiteNodeFoundListener,public GrayNodeFoundListener
+{
+
+ HMscNodePList* m_successors;
+ bool m_first;
+
+ void insert_successor(HMscNode* n)
+ {
+ //Don not insert the first one node and ConnectionNode
+ //The first one is strarting node of traversing
+ if(!dynamic_cast<ConnectionNode*>(n) && !m_first)
+ {
+ m_successors->push_back(n);
+ }
+ m_first = false;
+ }
+
+public:
+
+ ReferenceNodeFinderListener(HMscNodePList* successors):
+ WhiteNodeFoundListener(),GrayNodeFoundListener(),
+ m_successors(successors),m_first(true)
+ {
+ }
+
+ void on_white_node_found(HMscNode* n)
+ {
+ insert_successor(n);
+ }
+
+ //HMscNode can be accessible from itself
+ void on_gray_node_found(HMscNode* n)
+ {
+ insert_successor(n);
+ }
+
+};
+
/**
* \brief See method traverse(HMscNode* node) for purpose.
*/
@@ -34,9 +77,20 @@
{
}
+
+ /**
+ * \brief Finds successors of node which aren't ConnectionNodes.
+ *
+ * Note that it is neccessary to call cleanup_traversing_attributes()
+ * in case you want to reuse this traverser while traversing HMsc.
+ */
+ HMscNodePListPtr find_successors(HMscNode* node);
protected:
+ /**
+ * \brief Traverses from node to nearest StartNode,EndNodes or ReferenceNodes.
+ */
bool traverse_node(HMscNode* node);
};
Modified: trunk/src/check/visual_closure_initiator.cpp
===================================================================
--- trunk/src/check/visual_closure_initiator.cpp 2008-11-16 21:58:38 UTC (rev 118)
+++ trunk/src/check/visual_closure_initiator.cpp 2008-11-17 19:46:26 UTC (rev 119)
@@ -86,6 +86,7 @@
event_closure.resize(event_topology.size(),false);
set_topology_index(event,i);
closure[i] = &event_closure;
+ m_modified_events.push_back(event);
}
//compute visual closures of events' ordering
make_closure(closure,event_topology);
@@ -140,3 +141,13 @@
}
}
}
+
+size_t VisualClosureInitiator::get_topology_index(Event* e)
+{
+ return e->get_attribute<size_t>(m_topology_index_attribute,0);
+}
+
+void VisualClosureInitiator::set_topology_index(Event* e,size_t i)
+{
+ e->set_attribute<size_t>(m_topology_index_attribute,i);
+}
Modified: trunk/src/check/visual_closure_initiator.h
===================================================================
--- trunk/src/check/visual_closure_initiator.h 2008-11-16 21:58:38 UTC (rev 118)
+++ trunk/src/check/visual_closure_initiator.h 2008-11-17 19:46:26 UTC (rev 119)
@@ -133,18 +133,12 @@
/**
* Getter of topology index attribute of e.
*/
- size_t get_topology_index(Event* e)
- {
- return e->get_attribute<size_t>(m_topology_index_attribute,0);
- }
+ size_t get_topology_index(Event* e);
/**
* Setter of topology index attribute of e.
*/
- void set_topology_index(Event* e,size_t i)
- {
- e->set_attribute<size_t>(m_topology_index_attribute,i);
- }
+ void set_topology_index(Event* e,size_t i);
/**
* Cleans up set attributes.
Modified: trunk/tests/CMakeLists.txt
===================================================================
--- trunk/tests/CMakeLists.txt 2008-11-16 21:58:38 UTC (rev 118)
+++ trunk/tests/CMakeLists.txt 2008-11-17 19:46:26 UTC (rev 119)
@@ -17,13 +17,14 @@
visual_closure_initiator)
ADD_TEST(fifo_checker fifo_checker_test)
-#ADD_EXECUTABLE(livelock_checker_test livelock_checker_test.cpp)
-#TARGET_LINK_LIBRARIES(
-#livelock_checker_test
-#livelock_checker
-#msc
-#dfs_hmsc_traverser
-#dfs_msc_graph_traverser)
+ADD_EXECUTABLE(livelock_checker_test livelock_checker_test.cpp)
+TARGET_LINK_LIBRARIES(
+livelock_checker_test
+livelock_checker
+msc
+dfs_bmsc_graph_traverser
+dfs_hmsc_traverser
+dfsb_hmsc_traverser)
ADD_TEST(livelock_checker_checker livelock_checker_test)
# $Id: CMakeLists.txt,v 1.1 2008/10/28 21:13:20 gotthardp Exp $
Modified: trunk/tests/fifo_checker_test.cpp
===================================================================
--- trunk/tests/fifo_checker_test.cpp 2008-11-16 21:58:38 UTC (rev 118)
+++ trunk/tests/fifo_checker_test.cpp 2008-11-17 19:46:26 UTC (rev 119)
@@ -21,77 +21,93 @@
#include <iostream>
-void BMscA();
-void BMscB();
-void BMscC();
-void BMscD();
-void BMscE();
-void BMscF();
-void BMscG();
-void BMscH(); //BMscA
-void BMscI(); //BMscB
-void BMscJ(); //BMscC
-void BMscK(); //BMscD
-void BMscL(); //BMscE
-void BMscM(); //BMscF
-void BMscN(); //BMscG
-void BMscO(); //BMscK
-void BMscP(); //BMscL
-void BMscR(); //BMscM
+bool BMscA();
+bool BMscB();
+bool BMscC();
+bool BMscD();
+bool BMscE();
+bool BMscF();
+bool BMscG();
+bool BMscH(); //BMscA
+bool BMscI(); //BMscB
+bool BMscJ(); //BMscC
+bool BMscK(); //BMscD
+bool BMscL(); //BMscE
+bool BMscM(); //BMscF
+bool BMscN(); //BMscG
+bool BMscO(); //BMscK
+bool BMscP(); //BMscL
+bool BMscR(); //BMscM
+#define RETURN_IF_FAILED(res) if(!(res)) return 1;
+
/*
*
*/
int main(int argc, char** argv) {
- BMscA();
- BMscB();
- BMscC();
- BMscD();
- BMscE();
- BMscF();
- BMscG();
- BMscH();
- BMscI();
- BMscJ();
- BMscK();
- BMscL();
- BMscM();
- BMscN();
- BMscO();
- BMscP();
- BMscR();
+ RETURN_IF_FAILED(BMscA());
+ RETURN_IF_FAILED(BMscB());
+ RETURN_IF_FAILED(BMscC());
+ RETURN_IF_FAILED(BMscD());
+ RETURN_IF_FAILED(BMscE());
+ RETURN_IF_FAILED(BMscF());
+ RETURN_IF_FAILED(BMscG());
+ RETURN_IF_FAILED(BMscH());
+ RETURN_IF_FAILED(BMscI());
+ RETURN_IF_FAILED(BMscJ());
+ RETURN_IF_FAILED(BMscK());
+ RETURN_IF_FAILED(BMscL());
+ RETURN_IF_FAILED(BMscM());
+ RETURN_IF_FAILED(BMscN());
+ RETURN_IF_FAILED(BMscO());
+ RETURN_IF_FAILED(BMscP());
+ RETURN_IF_FAILED(BMscR());
return 0;
}
-void print_result(const BMscPtr bmsc,const bool is_fifo,const std::string& mapper_name)
+bool print_result(const BMscPtr bmsc,const bool is_fifo,const std::string& mapper_name)
{
+ bool result;
if(is_fifo)
if(bmsc.get())
+ {
+ result =false;
std::cout << "ERROR: BMsc is supposed to satisfy fifo for " << mapper_name
<< " channels but it doesn't satisfy it" << std::endl;
+ }
else
+ {
+ result = true;
std::cout << "OK: BMsc is supposed to satisfy fifo for " << mapper_name
<< " channels and it does so" << std::endl;
+ }
else
if(bmsc.get())
+ {
+ result = true;
std::cout << "OK: BMsc is supposed not to satisfy fifo for " << mapper_name
<< " channels and it doesn't so" << std::endl;
+ }
else
+ {
+ result =false;
std::cout << "ERROR: BMsc is supposed not to satisfy fifo for " << mapper_name
<< " channels but it satisfies it" << std::endl;
+ }
std::cout << std::endl;
+ return result;
}
-void check(BMscPtr bmsc,const bool is_sr_fifo,const bool is_srl_fifo)
+bool check(BMscPtr bmsc,const bool is_sr_fifo,const bool is_srl_fifo)
{
FifoCheckerPtr checker = FifoChecker::instance();
SRChannelMapperPtr srm = SRChannelMapper::instance();
SRLChannelMapperPtr srlm = SRLChannelMapper::instance();
- print_result(checker->check(bmsc,srm),is_sr_fifo,"sender-receiver");
- print_result(checker->check(bmsc,srlm),is_srl_fifo,"sender-receiver-label");
+ return (print_result(checker->check(bmsc,srm),is_sr_fifo,"sender-receiver") &&
+ print_result(checker->check(bmsc,srlm),is_srl_fifo,"sender-receiver-label"));
}
-void BMscA() {
+bool BMscA() {
std::cout << "Checking:" << std::endl;
std::cout << " p1 p2 " << std::endl;
std::cout << " | | " << std::endl;
@@ -120,10 +136,10 @@
e1->send_message(e3.get(),"a");
e4->send_message(e2.get(),"a");
- check(myBmsc,true,true);
+ return check(myBmsc,true,true);
}
-void BMscB() {
+bool BMscB() {
std::cout << "Checking:" << std::endl;
std::cout << " | | " << std::endl;
std::cout << "e1 O-----a----->O e3" << std::endl;
@@ -151,10 +167,10 @@
e1->send_message(e3.get(),"a");
e2->send_message(e4.get(),"a");
- check(myBmsc,true,true);
+ return check(myBmsc,true,true);
}
-void BMscC() {
+bool BMscC() {
std::cout << "Checking:" << std::endl;
std::cout << " | | " << std::endl;
std::cout << "e1 O --a->O e3" << std::endl;
@@ -185,10 +201,10 @@
e1->send_message(e4.get(),"a");
e2->send_message(e3.get(),"a");
- check(myBmsc,false,false);
+ return check(myBmsc,false,false);
}
-void BMscD() {
+bool BMscD() {
std::cout << "Checking:" << std::endl;
std::cout << " | | " << std::endl;
std::cout << "<coregion> <coregion> " << std::endl;
@@ -220,10 +236,10 @@
e1->send_message(e3.get(),"a");
e2->send_message(e4.get(),"a");
- check(myBmsc,false,false);
+ return check(myBmsc,false,false);
}
-void BMscE() {
+bool BMscE() {
std::cout << "Checking:" << std::endl;
std::cout << " | | " << std::endl;
std::cout << "<coregion> | " << std::endl;
@@ -255,10 +271,10 @@
e1->send_message(e3.get(),"a");
e2->send_message(e4.get(),"a");
- check(myBmsc,false,false);
+ return check(myBmsc,false,false);
}
-void BMscF() {
+bool BMscF() {
std::cout << "Checking:" << std::endl;
std::cout << " | | " << std::endl;
std::cout << "<coregion> | " << std::endl;
@@ -290,10 +306,10 @@
e3->send_message(e1.get(),"a");
e4->send_message(e2.get(),"a");
- check(myBmsc,false,false);
+ return check(myBmsc,false,false);
}
-void BMscG() {
+bool BMscG() {
std::cout << "Checking:" << std::endl;
std::cout << " | | " << std::endl;
std::cout << "<coregion> | " << std::endl;
@@ -325,10 +341,10 @@
e3->send_message(e1.get(),"a");
e2->send_message(e4.get(),"a");
- check(myBmsc,true,true);
+ return check(myBmsc,true,true);
}
-void BMscH() {
+bool BMscH() {
std::cout << "Checking:" << std::endl;
std::cout << " | | " << std::endl;
std::cout << "e1 O-----b----->O e3" << std::endl;
@@ -356,10 +372,10 @@
e1->send_message(e3.get(),"b");
e4->send_message(e2.get(),"a");
- check(myBmsc,true,true);
+ return check(myBmsc,true,true);
}
-void BMscI() {
+bool BMscI() {
std::cout << "Checking:" << std::endl;
std::cout << " | | " << std::endl;
std::cout << "e1 O-----a----->O e3" << std::endl;
@@ -387,10 +403,10 @@
e1->send_message(e3.get(),"a");
e2->send_message(e4.get(),"b");
- check(myBmsc,true,true);
+ return check(myBmsc,true,true);
}
-void BMscJ() {
+bool BMscJ() {
std::cout << "Checking:" << std::endl;
std::cout << " | | " << std::endl;
std::cout << "e1 O --a->O e3" << std::endl;
@@ -421,10 +437,10 @@
e2->send_message(e3.get(),"a");
e1->send_message(e4.get(),"b");
- check(myBmsc,false,true);
+ return check(myBmsc,false,true);
}
-void BMscK() {
+bool BMscK() {
std::cout << "Checking:" << std::endl;
std::cout << " | | " << std::endl;
std::cout << "<coregion> <coregion> " << std::endl;
@@ -456,10 +472,10 @@
e1->send_message(e3.get(),"a");
e2->send_message(e4.get(),"b");
- check(myBmsc,false,true);
+ return check(myBmsc,false,true);
}
-void BMscL() {
+bool BMscL() {
std::cout << "Checking:" << std::endl;
std::cout << " | | " << std::endl;
std::cout << "<coregion> | " << std::endl;
@@ -491,11 +507,11 @@
e1->send_message(e3.get(),"a");
e2->send_message(e4.get(),"b");
- check(myBmsc,false,true);
+ return check(myBmsc,false,true);
}
-void BMscM() {
+bool BMscM() {
std::cout << "Checking:" << std::endl;
std::cout << " | | " << std::endl;
std::cout << "<coregion> | " << std::endl;
@@ -527,10 +543,10 @@
e3->send_message(e1.get(),"a");
e4->send_message(e2.get(),"b");
- check(myBmsc,false,true);
+ return check(myBmsc,false,true);
}
-void BMscN() {
+bool BMscN() {
std::cout << "Checking:" << std::endl;
std::cout << " | | " << std::endl;
std::cout << "<coregion> | " << std::endl;
@@ -562,10 +578,10 @@
e3->send_message(e1.get(),"a");
e2->send_message(e4.get(),"b");
- check(myBmsc,true,true);
+ return check(myBmsc,true,true);
}
-void BMscO() {
+bool BMscO() {
std::cout << "Checking:" << std::endl;
std::cout << " | | " << std::endl;
std::cout << "<coregion> <coregion> " << std::endl;
@@ -602,10 +618,10 @@
e2->send_message(e4.get(),"b");
e5->send_message(e6.get(),"a");
- check(myBmsc,false,false);
+ return check(myBmsc,false,false);
}
-void BMscP() {
+bool BMscP() {
std::cout << "Checking:" << std::endl;
std::cout << " | | " << std::endl;
std::cout << "<coregion> | " << std::endl;
@@ -642,10 +658,10 @@
e2->send_message(e4.get(),"b");
e5->send_message(e6.get(),"a");
- check(myBmsc,false,false);
+ return check(myBmsc,false,false);
}
-void BMscR() {
+bool BMscR() {
std::cout << "Checking:" << std::endl;
std::cout << " | | " << std::endl;
std::cout << "<coregion> | " << std::endl;
@@ -682,5 +698,5 @@
e4->send_message(e2.get(),"b");
e6->send_message(e5.get(),"a");
- check(myBmsc,false,false);
+ return check(myBmsc,false,false);
}
Modified: trunk/tests/livelock_checker_test.cpp
===================================================================
--- trunk/tests/livelock_checker_test.cpp 2008-11-16 21:58:38 UTC (rev 118)
+++ trunk/tests/livelock_checker_test.cpp 2008-11-17 19:46:26 UTC (rev 119)
@@ -1,93 +1,56 @@
#include "data/msc.h"
-#include "dot_writer.h"
#include "check/livelock_checker.h"
#include <string>
+#include <iostream>
int main() {
- /**
- * Test of livelock - pretty same like deadlock, isnt it? :)
- * o node
- * (o) endnode node
- * s start node
- * o
- * h1: h2:
- *
- * s s
- * | |
- * p1 n1
- * / \ ...
- * p2 p |
- * \ n4
- * p4
- */
+ std::cout << "Test of livelock: " << std::endl;
+ std::cout << "h1: h2: " << std::endl;
+ std::cout << " start start " << std::endl;
+ std::cout << " | | " << std::endl;
+ std::cout << " p1 n1 " << std::endl;
+ std::cout << " / \\ / | " << std::endl;
+ std::cout << " p2 p3(h2) n2--n3 " << std::endl;
+ std::cout << " | \\ " << std::endl;
+ std::cout << " | p4 " << std::endl;
+ std::cout << " | / " << std::endl;
+ std::cout << " end " << std::endl;
- // Creating HMsc
HMscPtr h1(new HMsc("h1"));
HMscPtr h2(new HMsc("h2"));
- //Creating end node
- EndNodePtr end(new EndNode);
+ EndNodePtr end1(new EndNode);h1->add_node(end1);
+ ReferenceNodePtr p1(new ReferenceNode());h1->add_node(p1);
+ ReferenceNodePtr p2(new ReferenceNode());h1->add_node(p2);
+ ReferenceNodePtr p3(new ReferenceNode());h1->add_node(p3);
+ ReferenceNodePtr p4(new ReferenceNode());h1->add_node(p4);
- //Creating nodes of HMsc
- ReferenceNode* p1 = new ReferenceNode();
- ReferenceNode* p2 = new ReferenceNode();
- ReferenceNode* p3 = new ReferenceNode();
- ReferenceNode* p4 = new ReferenceNode();
+ ReferenceNodePtr n1(new ReferenceNode());h1->add_node(n1);
+ ReferenceNodePtr n2(new ReferenceNode());h1->add_node(n2);
+ ReferenceNodePtr n3(new ReferenceNode());h1->add_node(n3);
- ReferenceNode* n1 = new ReferenceNode();
- ReferenceNode* n2 = new ReferenceNode();
- ReferenceNode* n3 = new ReferenceNode();
- ReferenceNode* n4 = new ReferenceNode();
+ h1->get_start()->add_successor(p1.get());
+ p1->add_successor(p2.get());
+ p1->add_successor(p3.get());
+ p3->add_successor(p4.get());
+ p2->add_successor(end1.get());
+ p4->add_successor(end1.get());
+ p3->set_msc(h2);
- // Setting labels to node of HMsc, temporary
- p1->set_label("p1");
- p2->set_label("p2");
- p3->set_label("p3");
- p4->set_label("p4");
-
- n1->set_label("n1");
- n2->set_label("n2");
- n3->set_label("n3");
- n4->set_label("n4");
+ h2->get_start()->add_successor(n1.get());
+ n1->add_successor(n2.get());
+ n2->add_successor(n3.get());
+ n3->add_successor(n1.get());
- //Adding nodes to start node
- h1->get_start()->add_successor(p1);
- h2->get_start()->add_successor(n1);
-
- //Adding successors
- p1->add_successor(p2);
- p1->add_successor(p3);
- p2->add_successor(p2);
- p3->add_successor(p4);
- n1->add_successor(n2);
- n2->add_successor(n3);
- n3->add_successor(n4);
- n4->add_successor(n2);
-
- // Setting end node
- p4->set_end(end);
- p2->set_end(end);
- //n2->set_end(end);
- //n4->set_end(end);
- // Setting contant of hmsc node
- p3->set_msc(h2);
-
ChannelMapperPtr chm;
LivelockCheckerPtr live = LivelockChecker::instance();
- DotWriter writer;
-
- std::string name = "h1";
- std::cerr << "*** HMsc to be tested:" << std::endl;
- writer.print(h1,name);
-
- std::string path_name = "path_h1";
+
HMscPtr path_h1 = live->check(h1,chm);
- if(path_h1.get()){
- std::cerr << "*** There is livelock in h1, path:" << std::endl;
- writer.print(path_h1,path_name);
+ if(path_h1.get())
+ {
+ std::cerr << "OK: h1 contains livelock" << std::endl;
+ return 0;
}
- else
- std::cerr << "*** h1 is livelock free" << std::endl;
-
- return 0;
+ std::cerr << "ERROR: h1 doesn't contain livelock" << std::endl;
+ return 1;
}
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
