Menu
▾
▴
[Scstudio-commits] SF.net SVN: scstudio:[117] trunk
|
From: <ba...@us...> - 2008-11-16 20:19:40
|
Revision: 117
http://scstudio.svn.sourceforge.net/scstudio/?rev=117&view=rev
Author: babicaj
Date: 2008-11-16 20:19:35 +0000 (Sun, 16 Nov 2008)
Log Message:
-----------
fifo_checker_test and deadlock_checker_test are able to be to compiled and run, livelock_checker_test is comming soon -- tomorrow :)
Modified Paths:
--------------
trunk/CMakeLists.txt
trunk/Makefile
trunk/src/check/CMakeLists.txt
trunk/src/check/acyclic_checker.h
trunk/src/check/deadlock_checker.cpp
trunk/src/check/deadlock_checker.h
trunk/src/check/dfs_bmsc_graph_traverser.cpp
trunk/src/check/dfs_bmsc_graph_traverser.h
trunk/src/check/dfs_events_traverser.cpp
trunk/src/check/dfs_hmsc_traverser.cpp
trunk/src/check/dfs_hmsc_traverser.h
trunk/src/check/dfsb_hmsc_traverser.cpp
trunk/src/check/dfsb_hmsc_traverser.h
trunk/src/check/fifo_checker.cpp
trunk/src/check/fifo_checker.h
trunk/src/data/msc.cpp
trunk/src/data/msc.h
trunk/tests/CMakeLists.txt
trunk/tests/deadlock_checker_test.cpp
trunk/tests/fifo_checker_test.cpp
Modified: trunk/CMakeLists.txt
===================================================================
--- trunk/CMakeLists.txt 2008-11-12 17:12:14 UTC (rev 116)
+++ trunk/CMakeLists.txt 2008-11-16 20:19:35 UTC (rev 117)
@@ -1,6 +1,6 @@
# Process this file with cmake to produce a Makefile.
# cmake .
-# cmake . -DCMAKE_BUILD_TYPE=Debug -DCMAKE_INSTALL_PREFIX=/usr/local
+#cmake . -DCMAKE_BUILD_TYPE=Debug -DCMAKE_INSTALL_PREFIX=/usr/local
PROJECT(scstudio C CXX)
#SET(CMAKE_VERBOSE_MAKEFILE ON)
@@ -10,7 +10,7 @@
INCLUDE_DIRECTORIES(src)
ADD_SUBDIRECTORY(src .)
-#ADD_SUBDIRECTORY(tests .)
+ADD_SUBDIRECTORY(tests .)
# $Id: CMakeLists.txt,v 1.7 2008/11/06 15:16:29 gotthardp Exp $
Modified: trunk/Makefile
===================================================================
--- trunk/Makefile 2008-11-12 17:12:14 UTC (rev 116)
+++ trunk/Makefile 2008-11-16 20:19:35 UTC (rev 117)
@@ -67,6 +67,16 @@
rebuild_cache/fast: rebuild_cache
.PHONY : rebuild_cache/fast
+# Special rule for the target test
+test:
+ @$(CMAKE_COMMAND) -E cmake_echo_color --switch=$(COLOR) --cyan "Running tests..."
+ /usr/bin/ctest.exe --force-new-ctest-process $(ARGS)
+.PHONY : test
+
+# Special rule for the target test
+test/fast: test
+.PHONY : test/fast
+
# The main all target
all: cmake_check_build_system
$(CMAKE_COMMAND) -E cmake_progress_start /cygdrive/d/projekty/scstudio/CMakeFiles /cygdrive/d/projekty/scstudio/CMakeFiles/progress.make
@@ -98,14 +108,81 @@
$(CMAKE_COMMAND) -H$(CMAKE_SOURCE_DIR) -B$(CMAKE_BINARY_DIR) --check-build-system CMakeFiles/Makefile.cmake 1
.PHONY : depend
+# Convenience name for target.
+CMakeFiles/deadlock_checker_test.dir/rule:
+ $(MAKE) -f CMakeFiles/Makefile2 CMakeFiles/deadlock_checker_test.dir/rule
+.PHONY : CMakeFiles/deadlock_checker_test.dir/rule
+
+# Convenience name for target.
+deadlock_checker_test: CMakeFiles/deadlock_checker_test.dir/rule
+.PHONY : deadlock_checker_test
+
+# fast build rule for target.
+deadlock_checker_test/fast:
+ $(MAKE) -f CMakeFiles/deadlock_checker_test.dir/build.make CMakeFiles/deadlock_checker_test.dir/build
+.PHONY : deadlock_checker_test/fast
+
+# Convenience name for target.
+CMakeFiles/fifo_checker_test.dir/rule:
+ $(MAKE) -f CMakeFiles/Makefile2 CMakeFiles/fifo_checker_test.dir/rule
+.PHONY : CMakeFiles/fifo_checker_test.dir/rule
+
+# Convenience name for target.
+fifo_checker_test: CMakeFiles/fifo_checker_test.dir/rule
+.PHONY : fifo_checker_test
+
+# fast build rule for target.
+fifo_checker_test/fast:
+ $(MAKE) -f CMakeFiles/fifo_checker_test.dir/build.make CMakeFiles/fifo_checker_test.dir/build
+.PHONY : fifo_checker_test/fast
+
+# target to build an object file
+deadlock_checker_test.o:
+ $(MAKE) -f CMakeFiles/deadlock_checker_test.dir/build.make CMakeFiles/deadlock_checker_test.dir/deadlock_checker_test.o
+.PHONY : deadlock_checker_test.o
+
+# target to preprocess a source file
+deadlock_checker_test.i:
+ $(MAKE) -f CMakeFiles/deadlock_checker_test.dir/build.make CMakeFiles/deadlock_checker_test.dir/deadlock_checker_test.i
+.PHONY : deadlock_checker_test.i
+
+# target to generate assembly for a file
+deadlock_checker_test.s:
+ $(MAKE) -f CMakeFiles/deadlock_checker_test.dir/build.make CMakeFiles/deadlock_checker_test.dir/deadlock_checker_test.s
+.PHONY : deadlock_checker_test.s
+
+# target to build an object file
+fifo_checker_test.o:
+ $(MAKE) -f CMakeFiles/fifo_checker_test.dir/build.make CMakeFiles/fifo_checker_test.dir/fifo_checker_test.o
+.PHONY : fifo_checker_test.o
+
+# target to preprocess a source file
+fifo_checker_test.i:
+ $(MAKE) -f CMakeFiles/fifo_checker_test.dir/build.make CMakeFiles/fifo_checker_test.dir/fifo_checker_test.i
+.PHONY : fifo_checker_test.i
+
+# target to generate assembly for a file
+fifo_checker_test.s:
+ $(MAKE) -f CMakeFiles/fifo_checker_test.dir/build.make CMakeFiles/fifo_checker_test.dir/fifo_checker_test.s
+.PHONY : fifo_checker_test.s
+
# Help Target
help:
@echo "The following are some of the valid targets for this Makefile:"
@echo "... all (the default if no target is provided)"
@echo "... clean"
@echo "... depend"
+ @echo "... deadlock_checker_test"
@echo "... edit_cache"
+ @echo "... fifo_checker_test"
@echo "... rebuild_cache"
+ @echo "... test"
+ @echo "... deadlock_checker_test.o"
+ @echo "... deadlock_checker_test.i"
+ @echo "... deadlock_checker_test.s"
+ @echo "... fifo_checker_test.o"
+ @echo "... fifo_checker_test.i"
+ @echo "... fifo_checker_test.s"
.PHONY : help
Modified: trunk/src/check/CMakeLists.txt
===================================================================
--- trunk/src/check/CMakeLists.txt 2008-11-12 17:12:14 UTC (rev 116)
+++ trunk/src/check/CMakeLists.txt 2008-11-16 20:19:35 UTC (rev 117)
@@ -2,18 +2,19 @@
#ADD_LIBRARY(dfs_area_traverser STATIC dfs_area_traverser.cpp)
ADD_LIBRARY(dfs_events_traverser STATIC dfs_events_traverser.cpp)
ADD_LIBRARY(dfs_hmsc_traverser STATIC dfs_hmsc_traverser.cpp)
+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)
+#ADD_LIBRARY(causal_closure_initiator STATIC causal_closure_initiator.cpp)
ADD_LIBRARY(visual_closure_initiator STATIC visual_closure_initiator.cpp)
#checkers
#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(fifo_checker STATIC fifo_checker.cpp)
#ADD_LIBRARY(livelock_checker STATIC livelock_checker.cpp)
#ADD_LIBRARY(race_checker STATIC race_checker.cpp)
Modified: trunk/src/check/acyclic_checker.h
===================================================================
--- trunk/src/check/acyclic_checker.h 2008-11-12 17:12:14 UTC (rev 116)
+++ trunk/src/check/acyclic_checker.h 2008-11-16 20:19:35 UTC (rev 117)
@@ -59,7 +59,7 @@
};
-class AcyclicChecker: public BMscChecker
+class AcyclicChecker: public Checker, public BMscChecker
{
protected:
Modified: trunk/src/check/deadlock_checker.cpp
===================================================================
--- trunk/src/check/deadlock_checker.cpp 2008-11-12 17:12:14 UTC (rev 116)
+++ trunk/src/check/deadlock_checker.cpp 2008-11-16 20:19:35 UTC (rev 117)
@@ -39,9 +39,9 @@
const std::string& depth_attribute):
m_current_depth(0),
m_deadlock_free_attribute(deadlock_free_attribute),
- m_depth_attribute(depth_attribute),
- m_marker(this)
+ m_depth_attribute(depth_attribute)
{
+ m_marker = DeadlockFreeMarker(this);
m_marker_traverser.add_white_node_found_listener(&m_marker);
}
@@ -80,10 +80,10 @@
void DeadlockListener::on_node_finished(HMscNode* node)
{
- if (dynamic_cast<ReferenceNode*> (node))
+ if (dynamic_cast<ReferenceNode*> (node) ||
+ dynamic_cast<StartNode*> (node))
{
- bool& deadlock_free = get_deadlock_free(node);
- if (!deadlock_free)
+ if (!get_deadlock_free(node))
{
throw DeadlockException();
}
Modified: trunk/src/check/deadlock_checker.h
===================================================================
--- trunk/src/check/deadlock_checker.h 2008-11-12 17:12:14 UTC (rev 116)
+++ trunk/src/check/deadlock_checker.h 2008-11-16 20:19:35 UTC (rev 117)
@@ -24,6 +24,7 @@
#include "data/msc.h"
#include "data/counted_ptr.h"
#include "check/dfs_hmsc_traverser.h"
+#include "check/dfsb_hmsc_traverser.h"
class DeadlockChecker;
class DeadlockListener;
@@ -48,7 +49,7 @@
public:
- DeadlockFreeMarker(DeadlockListener* dl);
+ DeadlockFreeMarker(DeadlockListener* dl=NULL);
void on_white_node_found(HMscNode* n);
@@ -78,12 +79,12 @@
HMscNodePList m_modified;
- size_t& get_depth(HMscNode* node);
-
DFSBHMscTraverser m_marker_traverser;
DeadlockFreeMarker m_marker;
+ size_t& get_depth(HMscNode* node);
+
public:
DeadlockListener(
Modified: trunk/src/check/dfs_bmsc_graph_traverser.cpp
===================================================================
--- trunk/src/check/dfs_bmsc_graph_traverser.cpp 2008-11-12 17:12:14 UTC (rev 116)
+++ trunk/src/check/dfs_bmsc_graph_traverser.cpp 2008-11-16 20:19:35 UTC (rev 117)
@@ -83,7 +83,7 @@
ReferenceNode* ref_node = dynamic_cast<ReferenceNode*>(node);
if(ref_node!=NULL)
{
- return traverse_node(ref_node);
+ return traverse_reference_node(ref_node);
}
else
{
@@ -111,7 +111,7 @@
}
}
-bool DFSBMscGraphTraverser::traverse_node(ReferenceNode* ref_node)
+bool DFSBMscGraphTraverser::traverse_reference_node(ReferenceNode* ref_node)
{
HMscPtr hmsc = ref_node->get_hmsc();
bool inner = true;
@@ -121,7 +121,7 @@
//as it is referenced
push_top_attributes();
//node's successors aren't traversed if end node wasn't found in hmsc
- inner = traverse_successors(hmsc->get_start().get());
+ inner = traverse_node(hmsc->get_start().get());
//this line ensures (yet another one) that HMsc will traversed as many times
//as it is referenced
cleanup_top_attributes();
@@ -138,7 +138,7 @@
{
const NodeRelationPtr& rel = *relation;
m_reached_elements.back().push_back(rel.get());
- end_found = traverse_node((HMscNode*)rel->get_successor()) || end_found;
+ end_found = traverse_node(dynamic_cast<HMscNode*>(rel->get_successor())) || end_found;
m_reached_elements.back().pop_back();
}
return end_found;
Modified: trunk/src/check/dfs_bmsc_graph_traverser.h
===================================================================
--- trunk/src/check/dfs_bmsc_graph_traverser.h 2008-11-12 17:12:14 UTC (rev 116)
+++ trunk/src/check/dfs_bmsc_graph_traverser.h 2008-11-16 20:19:35 UTC (rev 117)
@@ -415,7 +415,7 @@
*/
virtual bool is_processed(HMscNode* node);
- virtual bool traverse_node(ReferenceNode* node);
+ virtual bool traverse_reference_node(ReferenceNode* node);
/**
* Color attribute's name
Modified: trunk/src/check/dfs_events_traverser.cpp
===================================================================
--- trunk/src/check/dfs_events_traverser.cpp 2008-11-12 17:12:14 UTC (rev 116)
+++ trunk/src/check/dfs_events_traverser.cpp 2008-11-16 20:19:35 UTC (rev 117)
@@ -39,6 +39,7 @@
void DFSEventsTraverser::traverse_area(EventArea* area)
{
+ if(!area) return;
StrictOrderArea* strict = dynamic_cast<StrictOrderArea*>(area);
if(strict)
{
@@ -65,9 +66,9 @@
void DFSEventsTraverser::traverse_strict_event(StrictEvent* event)
{
+ m_reached_elements.push_back(event);
if(!is_processed(event))
{
- m_reached_elements.push_back(event);
traverse_matching_event(event);
if(event->get_successor().get())
traverse_strict_event(event->get_successor().get());
Modified: trunk/src/check/dfs_hmsc_traverser.cpp
===================================================================
--- trunk/src/check/dfs_hmsc_traverser.cpp 2008-11-12 17:12:14 UTC (rev 116)
+++ trunk/src/check/dfs_hmsc_traverser.cpp 2008-11-16 20:19:35 UTC (rev 117)
@@ -18,13 +18,13 @@
#include "check/dfs_hmsc_traverser.h"
-bool DFSHMscTraverser::traverse_node(ReferenceNode* ref_node)
+bool DFSHMscTraverser::traverse_reference_node(ReferenceNode* ref_node)
{
HMscPtr hmsc = ref_node->get_hmsc();
if(hmsc.get()!=NULL)
{
m_reached_elements.push_back(MscElementPList());
- traverse_successors(hmsc->get_start().get());
+ traverse_node(hmsc->get_start().get());
m_reached_elements.pop_back();
}
Modified: trunk/src/check/dfs_hmsc_traverser.h
===================================================================
--- trunk/src/check/dfs_hmsc_traverser.h 2008-11-12 17:12:14 UTC (rev 116)
+++ trunk/src/check/dfs_hmsc_traverser.h 2008-11-16 20:19:35 UTC (rev 117)
@@ -36,7 +36,7 @@
protected:
- bool traverse_node(ReferenceNode* node);
+ bool traverse_reference_node(ReferenceNode* node);
public:
Modified: trunk/src/check/dfsb_hmsc_traverser.cpp
===================================================================
--- trunk/src/check/dfsb_hmsc_traverser.cpp 2008-11-12 17:12:14 UTC (rev 116)
+++ trunk/src/check/dfsb_hmsc_traverser.cpp 2008-11-16 20:19:35 UTC (rev 117)
@@ -18,17 +18,17 @@
#include <stack>
-#include "check/dfs_bmsc_graph_traverser.h"
+#include "check/dfsb_hmsc_traverser.h"
-DFSBMscGraphTraverser::~DFSBMscGraphTraverser()
+DFSBHMscTraverser::~DFSBHMscTraverser()
{
cleanup_traversing_attributes();
}
-void DFSBMscGraphTraverser::traverse(HMscPtr hmsc)
+void DFSBHMscTraverser::traverse(HMscPtr hmsc)
{
HMscNodePtrSet::const_iterator n;
- const HMscNodePtrSet& nodes;
+ const HMscNodePtrSet& nodes = hmsc->get_nodes();
for(n=nodes.begin();n!=nodes.end();n++)
{
if(dynamic_cast<EndNode*>((*n).get()))
@@ -39,18 +39,18 @@
cleanup_traversing_attributes();
}
-void DFSBMscGraphTraverser::traverse(HMscNode* node)
+void DFSBHMscTraverser::traverse(HMscNode* node)
{
traverse_node(node);
cleanup_traversing_attributes();
}
-bool DFSBMscGraphTraverser::traverse_node(HMscNode* node)
+bool DFSBHMscTraverser::traverse_node(HMscNode* node)
{
m_reached_elements.push_back(node);
if(is_processed(node))
{
- return;
+ return false;
}
white_node_found(node);
SuccessorNode* succ = dynamic_cast<SuccessorNode*>(node);
@@ -59,22 +59,23 @@
traverse_predecessors(succ);
}
node_finished(node);
+ return false;
}
-void DFSBMscGraphTraverser::traverse_predecessors(SuccessorNode* predecessor)
+void DFSBHMscTraverser::traverse_predecessors(SuccessorNode* succ)
{
NodeRelationPtrSet::const_iterator relation;
- for(relation=predecessor->get_predecessors().begin();
- relation!=predecessor->get_predecessors().end();relation++)
+ for(relation=succ->get_predecessors().begin();
+ relation!=succ->get_predecessors().end();relation++)
{
const NodeRelationPtr& rel = *relation;
m_reached_elements.push_back(rel.get());
- traverse_node((HMscNode*)rel->get_predecessor());
+ traverse_node(dynamic_cast<HMscNode*>(rel->get_predecessor()));
m_reached_elements.pop_back();
}
}
-bool DFSBMscGraphTraverser::is_processed(HMscNode* node)
+bool DFSBHMscTraverser::is_processed(HMscNode* node)
{
Color c = get_color(node);
if(c==BLACK)
@@ -90,36 +91,37 @@
return false;
}
-void DFSBMscGraphTraverser::cleanup_traversing_attributes()
+void DFSBHMscTraverser::cleanup_traversing_attributes()
{
- for(HMscNode* n=m_colored_nodes.begin();n!=m_colored_nodes.end();n++)
+ HMscNodePList::const_iterator n;
+ for(n=m_colored_nodes.begin();n!=m_colored_nodes.end();n++)
(*n)->remove_attribute<Color>(m_color_attribute);
m_colored_nodes.erase(m_colored_nodes.begin(),m_colored_nodes.end());
- m_reached_elements.erase(m_reached_nodes.begin(),m_reached_nodes.end());
+ m_reached_elements.erase(m_reached_elements.begin(),m_reached_elements.end());
}
-void DFSBMscGraphTraverser::white_node_found(HMscNode* n)
+void DFSBHMscTraverser::white_node_found(HMscNode* n)
{
- super.white_node_found(n);
+ DFSListenersContainer::white_node_found(n);
set_color(n,GRAY);
}
-void DFSBMscGraphTraverser::gray_node_found(HMscNode* n)
+void DFSBHMscTraverser::gray_node_found(HMscNode* n)
{
- super.gray_node_found(n);
+ DFSListenersContainer::gray_node_found(n);
m_reached_elements.pop_back();
}
-void DFSBMscGraphTraverser::black_node_found(HMscNode* n)
+void DFSBHMscTraverser::black_node_found(HMscNode* n)
{
- super.black_node_found(n);
+ DFSListenersContainer::black_node_found(n);
m_reached_elements.pop_back();
}
-void DFSBMscGraphTraverser::node_finished(HMscNode* n)
+void DFSBHMscTraverser::node_finished(HMscNode* n)
{
- super.node_finished(n);
- m_reached_elements.back().pop_back();
+ DFSListenersContainer::node_finished(n);
+ m_reached_elements.pop_back();
set_color(n,BLACK);
}
Modified: trunk/src/check/dfsb_hmsc_traverser.h
===================================================================
--- trunk/src/check/dfsb_hmsc_traverser.h 2008-11-12 17:12:14 UTC (rev 116)
+++ trunk/src/check/dfsb_hmsc_traverser.h 2008-11-16 20:19:35 UTC (rev 117)
@@ -76,7 +76,7 @@
/**
* Holds nodes with set color attribute
*/
- HMscNodePListList m_colored_nodes;
+ HMscNodePList m_colored_nodes;
/**
* Holds currently reached HMscElements.
@@ -89,9 +89,9 @@
virtual bool traverse_node(HMscNode* node);
/**
- * Traverses successors
+ * Traverses predecessors of succ
*/
- virtual bool traverse_predecessors(SuccessorNode* predecessor);
+ virtual void traverse_predecessors(SuccessorNode* succ);
/**
* Returns true iff node is already processed false otherwise
@@ -120,6 +120,14 @@
{
return n->get_attribute<Color>(m_color_attribute,WHITE);
}
+
+ void white_node_found(HMscNode* n);
+
+ void gray_node_found(HMscNode* n);
+
+ void black_node_found(HMscNode* n);
+
+ void node_finished(HMscNode* n);
};
Modified: trunk/src/check/fifo_checker.cpp
===================================================================
--- trunk/src/check/fifo_checker.cpp 2008-11-12 17:12:14 UTC (rev 116)
+++ trunk/src/check/fifo_checker.cpp 2008-11-16 20:19:35 UTC (rev 117)
@@ -25,7 +25,7 @@
BMsc* FifoChecker::create_counter_example(Event* receive_1, Event* receive_2)
{
BMsc* bmsc = new BMsc(receive_1->get_instance()->get_bmsc());
- InstancePtr send_instance(new Instance(bmsc,receive_1->get_matching_event()->get_instance()));
+/* InstancePtr send_instance(new Instance(bmsc,receive_1->get_matching_event()->get_instance()));
InstancePtr receive_instance(new Instance(bmsc,receive_1->get_instance()));
bmsc->add_instance(send_instance);
bmsc->add_instance(receive_instance);
@@ -44,7 +44,7 @@
send_area->set_first(send1);
send1->set_successor(send2);
send_area->set_first(receive2);
- receive2->set_successor(receive1);
+ receive2->set_successor(receive1);*/
return bmsc;
}
Modified: trunk/src/check/fifo_checker.h
===================================================================
--- trunk/src/check/fifo_checker.h 2008-11-12 17:12:14 UTC (rev 116)
+++ trunk/src/check/fifo_checker.h 2008-11-16 20:19:35 UTC (rev 117)
@@ -58,8 +58,7 @@
{
BoolVector& e1_closure = initiator.get_visual_closure(e1);
size_t e2_index = initiator.get_topology_index(e2);
- if(!e1_closure[e2_index]) return false;
- return true;
+ return e1_closure[e2_index];
}
public:
Modified: trunk/src/data/msc.cpp
===================================================================
--- trunk/src/data/msc.cpp 2008-11-12 17:12:14 UTC (rev 116)
+++ trunk/src/data/msc.cpp 2008-11-16 20:19:35 UTC (rev 117)
@@ -21,11 +21,12 @@
#include "data/msc.h"
-void SuccessorNode::add_predecessor(NodeRelationPtr& n)
+NodeRelationPtr SuccessorNode::add_predecessor(PredecessorNode* pred)
{
- n->set_successor(this);
+ NodeRelationPtr n(new NodeRelation(pred,this));
m_predecessors.insert(n);
- n->get_predecessor()->m_successors.insert(n);
+ pred->m_successors.insert(n);
+ return n;
}
void SuccessorNode::remove_predecessor(NodeRelationPtr& n)
@@ -34,11 +35,12 @@
n->get_predecessor()->m_successors.erase(n);
}
-void PredecessorNode::add_successor(NodeRelationPtr& n)
+NodeRelationPtr PredecessorNode::add_successor(SuccessorNode* succ)
{
- n->set_predecessor(this);
+ NodeRelationPtr n(new NodeRelation(this,succ));
m_successors.insert(n);
- n->get_successor()->m_predecessors.insert(n);
+ succ->m_predecessors.insert(n);
+ return n;
}
void PredecessorNode::remove_successor(NodeRelationPtr& n)
@@ -56,23 +58,15 @@
return m_owner->find_ptr(this);
}
-inline StrictOrderArea* StrictEvent::get_strict_order_area()
+/*inline StrictOrderArea* StrictEvent::get_strict_order_area()
{
return dynamic_cast<StrictOrderArea*>(m_area);
-}
+}*/
CoregionArea::~CoregionArea()
{
}
-void CoregionArea::add_event(CoregionEventPtr e)
-{
- //TODO: check whether it is possible to insert e
- m_events.insert(e);
- add_minimal_event(e.get());
- add_maximal_event(e.get());
-}
-
CoregionEvent::~CoregionEvent()
{
@@ -112,3 +106,23 @@
{
return m_receive_event->get_instance();
}
+
+void BMsc::add_instance(InstancePtr& i)
+{
+ m_instances.push_back(i);
+ i->set_bmsc(this);
+}
+
+void Instance::add_area(EventAreaPtr& area)
+{
+ if(!is_empty())
+ {
+ m_last->set_next(area);
+ }
+ else
+ {
+ m_first = area;
+ }
+ m_last = area;
+ area->set_instance(this);
+}
Modified: trunk/src/data/msc.h
===================================================================
--- trunk/src/data/msc.h 2008-11-12 17:12:14 UTC (rev 116)
+++ trunk/src/data/msc.h 2008-11-16 20:19:35 UTC (rev 117)
@@ -130,8 +130,6 @@
m_marked = marked;
}
- virtual ~MscElement();
-
public:
/**
@@ -260,6 +258,11 @@
{
m_marked = marked;
}
+
+ virtual ~MscElement()
+ {
+
+ }
};
template <class T>
@@ -309,6 +312,11 @@
{
m_original = e;
}
+
+ virtual ~MscElementTmpl()
+ {
+
+ }
};
/**
@@ -324,22 +332,20 @@
*/
std::string m_label;
- Msc(Msc* original=NULL):MscElementTmpl<Msc>(original)
+ Msc(const std::string& label=""):m_label(label)
{
-
}
- /**
- * Initializes m_label.
- */
- Msc(const std::string& label)
+ Msc(Msc* original):MscElementTmpl<Msc>(original)
{
- m_label = label;
}
public:
- virtual ~Msc();
+ virtual ~Msc()
+ {
+
+ }
/**
* Getter for m_label
@@ -376,12 +382,10 @@
BMsc(const std::string& label=""):Msc(label)
{
}
-
- /**
- * Creates BMsc referencing original version of BMsc.
- */
- BMsc(BMsc* original=NULL):Msc(original)
+
+ BMsc(BMsc* original):Msc(original)
{
+
}
virtual ~BMsc()
@@ -392,10 +396,7 @@
/**
* Adds instance.
*/
- void add_instance(InstancePtr& i)
- {
- m_instances.push_back(i);
- }
+ void add_instance(InstancePtr& i);
/**
* Getter for m_instances.
@@ -461,7 +462,9 @@
HMscNodePtr my_ptr();
- virtual ~HMscNode();
+ virtual ~HMscNode()
+ {
+ }
};
@@ -477,12 +480,11 @@
public:
- NodeRelation(SuccessorNode* successor, PredecessorNode* predecessor,
- const PolyLine& line):MscElementTmpl<NodeRelation>()
+ NodeRelation(PredecessorNode* predecessor,SuccessorNode* successor)
+ :MscElementTmpl<NodeRelation>()
{
m_successor = successor;
m_predecessor = predecessor;
- m_line = line;
}
SuccessorNode* get_successor()
@@ -537,7 +539,7 @@
return m_predecessors;
}
- void add_predecessor(NodeRelationPtr& n);
+ NodeRelationPtr add_predecessor(PredecessorNode* pred);
void remove_predecessor(NodeRelationPtr& n);
@@ -582,7 +584,7 @@
/**
* Adds successor.
*/
- void add_successor(NodeRelationPtr& n);
+ NodeRelationPtr add_successor(SuccessorNode* succ);
/**
* Removes successor.
@@ -610,8 +612,6 @@
{
public:
- EndNode()
- {}
EndNode(EndNode* original=NULL):HMscNode(original),SuccessorNode()
{}
@@ -663,28 +663,23 @@
public:
- /**
- * Initializes mandatory m_start
- */
+ HMsc(const std::string& label=""):Msc(label)
+ {
+ // Creating start for new HMsc, setting its original and owner
+ m_start = new StartNode();
+ m_start->set_owner(this);
+ }
+
HMsc(HMsc* original):Msc(original)
{
// Creating start for new HMsc, setting its original and owner
m_start = new StartNode(original->get_start().get());
m_start->set_owner(this);
}
-
- /**
- * Initializes m_label
- */
- HMsc(const std::string& label):Msc(label)
+
+ virtual ~HMsc()
{
- m_start = new StartNode;
- m_start->set_owner(this);
}
- /**
- * Removes all nodes inside
- */
- virtual ~HMsc();
/**
* Getter for m_start.
@@ -831,6 +826,8 @@
*/
class Instance:public MscElementTmpl<Instance>
{
+
+protected:
/**
* Label of instance -- name of concrete instance
@@ -853,6 +850,11 @@
EventAreaPtr m_first;
/**
+ * EventAreas which occure at instance as first one.
+ */
+ EventAreaPtr m_last;
+
+ /**
* BMsc whic this instance belongs to
*
* @warning counted_ptr mustn't be used because of possible cyclic dependency
@@ -866,24 +868,13 @@
public:
/**
- * @param msc - BMsc which Instance will occure in
* @param label - label of instance
*/
- Instance(BMsc* msc, const std::string& label)
+ Instance(const std::string& label, const std::string& kind="", Instance* original=NULL):
+ MscElementTmpl<Instance>(original),m_label(label),m_kind(kind)
{
- m_bmsc = msc;
- m_label = label;
}
- /**
- * @param msc - BMsc which Instance will occure in
- * @param original - original Instance, used when creating counter example
- */
- Instance(BMsc* msc, Instance* original):MscElementTmpl<Instance>(original)
- {
- m_bmsc = msc;
- }
-
virtual ~Instance()
{
@@ -912,23 +903,45 @@
return m_label;
}
+ void set_last(EventAreaPtr a)
+ {
+ m_last = a;
+ }
+
+ EventAreaPtr get_last()
+ {
+ return m_last;
+ }
+
/**
* Getter for m_bmsc
*/
- BMsc* get_bmsc()
+ BMsc* get_bmsc() const
{
return m_bmsc;
}
- Size get_height()
+ void set_bmsc(BMsc* bmsc)
{
+ m_bmsc = bmsc;
+ }
+
+ Size get_height() const
+ {
return m_height;
}
- void set_height(Size height)
+ void set_height(const Size& height)
{
m_height = height;
}
+
+ void add_area(EventAreaPtr& area);
+
+ bool is_empty()
+ {
+ return !m_last.get();
+ }
};
@@ -967,6 +980,11 @@
{
return m_label;
}
+
+ void set_label(const std::string& label)
+ {
+ m_label = label;
+ }
};
@@ -994,8 +1012,8 @@
* @param receiver - receiving event
* @param label - label of message
*/
- CompleteMessage(const std::string& label):
- MscMessage(label),m_send_event(NULL),m_receive_event(NULL)
+ CompleteMessage(Event* sender, Event* receiver, const std::string& label=""):
+ MscMessage(label),m_send_event(sender),m_receive_event(receiver)
{
}
@@ -1099,6 +1117,13 @@
typedef counted_ptr<IncompleteMessage> IncompleteMessagePtr;
+typedef enum
+{
+ BEFORE,
+ AFTER
+}
+EventPosition;
+
/**
* \brief Event which occurs in EventArea.
*/
@@ -1149,6 +1174,11 @@
}
}
}
+
+ void set_message(MscMessagePtr& message)
+ {
+ m_message = message;
+ }
/**
* Getter for m_message.
@@ -1285,6 +1315,34 @@
}
}
}
+
+ CompleteMessagePtr send_message(
+ Event* receive_event, const std::string& message_label="")
+ {
+ if(!receive_event) return CompleteMessagePtr();
+ MscMessagePtr message(new CompleteMessage(this,receive_event,message_label));
+ set_message(message);
+ receive_event->set_message(message);
+ return message;
+ }
+
+ IncompleteMessagePtr lose_message(
+ const std::string& message_label="", const std::string& instance_label="")
+ {
+ MscMessagePtr message(
+ new IncompleteMessage(LOST,message_label,instance_label));
+ set_message(message);
+ return message;
+ }
+
+ IncompleteMessagePtr find_message(
+ const std::string& message_label="", const std::string& instance_label="")
+ {
+ MscMessagePtr message(
+ new IncompleteMessage(FOUND,message_label,instance_label));
+ set_message(message);
+ return message;
+ }
};
@@ -1324,11 +1382,16 @@
m_area = area;
}
- Instance* get_instance()
+ Instance* get_instance() const
{
return m_area->get_instance();
}
+ EventArea* get_general_area()
+ {
+ return m_area;
+ }
+
};
/**
@@ -1406,11 +1469,6 @@
{
return m_successor==NULL;
}
-
- /**
- * Returns overcasted m_area
- */
- StrictOrderArea* get_strict_order_area();
};
class CoregionEventRelation:public MscElementTmpl<CoregionEventRelation>
@@ -1426,7 +1484,7 @@
public:
CoregionEventRelation(CoregionEvent* predecessor, CoregionEvent* successor,
- const PolyLine& line = NULL):MscElementTmpl<CoregionEventRelation>()
+ const PolyLine& line = PolyLine()):MscElementTmpl<CoregionEventRelation>()
{
m_predecessor = predecessor;
m_successor = successor;
@@ -1572,22 +1630,14 @@
*/
Instance* m_instance;
- EventArea()
- {
- m_previous = NULL;
- }
-
/**
* @param instance - Instance which this EventArea will occure at
*/
- EventArea(Instance* instance)
+ EventArea(EventArea* original):MscElementTmpl<EventArea>(original),
+ m_previous(NULL),m_instance(NULL),m_next()
{
- m_previous = NULL;
- m_instance = instance;
}
-
-
public:
virtual ~EventArea(){}
@@ -1611,10 +1661,15 @@
/**
* Getter for m_instance
*/
- Instance* get_instance()
+ Instance* get_instance() const
{
return m_instance;
}
+
+ void set_instance(Instance* instance)
+ {
+ m_instance = instance;
+ }
/**
* Getter for m_previous
@@ -1646,6 +1701,11 @@
{
m_height=height;
}
+
+ /**
+ * Adds event into this area. The added event is returned.
+ */
+ virtual EventPtr add_event()=0;
};
/**
@@ -1670,7 +1730,7 @@
public:
- StrictOrderArea():EventArea()
+ StrictOrderArea(StrictOrderArea* original=NULL):EventArea(original)
{
}
@@ -1681,14 +1741,6 @@
}
/**
- * See EventArea constructor for details
- */
- StrictOrderArea(Instance* instance):EventArea(instance)
- {
-
- }
-
- /**
* Getter for m_first.
*/
StrictEventPtr get_first()
@@ -1735,12 +1787,30 @@
m_last->set_successor(last);
m_last = last;
}
+ last->set_area(this);
}
bool is_empty()
{
return m_first.get()==NULL;
}
+
+ EventPtr add_event()
+ {
+ StrictEventPtr strict(new StrictEvent());
+ set_last(strict);
+ return strict;
+ }
+
+// StrictEventPtr add_strict_event(StrictEventPtr e=StrictEventPtr())
+// {
+// if(!e.get())
+// {
+// e = new StrictEvent();
+// }
+// set_last(e);
+// return e;
+// }
};
/**
@@ -1778,7 +1848,7 @@
/**
* See EventArea constructor for details
*/
- CoregionArea(Instance* instance):EventArea(instance)
+ CoregionArea(CoregionArea* original=NULL):EventArea(original)
{
}
@@ -1858,8 +1928,21 @@
return m_events;
}
- void add_event(CoregionEventPtr e);
+ EventPtr add_event()
+ {
+ CoregionEventPtr c(new CoregionEvent());
+ add_event(c);
+ return c;
+ }
+ CoregionEventPtr add_event(CoregionEventPtr e)
+ {
+ m_events.insert(e);
+ add_maximal_event(e.get());
+ e->set_area(this);
+ return e;
+ }
+
};
#endif /* _MSC_H */
Modified: trunk/tests/CMakeLists.txt
===================================================================
--- trunk/tests/CMakeLists.txt 2008-11-12 17:12:14 UTC (rev 116)
+++ trunk/tests/CMakeLists.txt 2008-11-16 20:19:35 UTC (rev 117)
@@ -1,6 +1,12 @@
ENABLE_TESTING()
ADD_EXECUTABLE(deadlock_checker_test deadlock_checker_test.cpp)
+TARGET_LINK_LIBRARIES(
+deadlock_checker_test
+msc deadlock_checker
+dfsb_hmsc_traverser
+dfs_bmsc_graph_traverser
+dfs_hmsc_traverser)
ADD_TEST(deadlock_checker deadlock_checker_test)
ADD_EXECUTABLE(fifo_checker_test fifo_checker_test.cpp)
Modified: trunk/tests/deadlock_checker_test.cpp
===================================================================
--- trunk/tests/deadlock_checker_test.cpp 2008-11-12 17:12:14 UTC (rev 116)
+++ trunk/tests/deadlock_checker_test.cpp 2008-11-16 20:19:35 UTC (rev 117)
@@ -1,93 +1,53 @@
#include "data/msc.h"
-#include "dot_writer.h"
#include "check/deadlock_checker.h"
#include <string>
+#include <iostream>
int main() {
- /**
- * Test of deadlock
- * o node
- * (o) endnode node
- * s start node
- * o
- * h1: h2:
- *
- * s s
- * | |
- * p1 n1
- * / \ ...
- * p2 p3 |
- * \ n4
- * p4
- */
+ std::cout << "Test of deadlock: " << 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 " << 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);
- 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());
- //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;
DeadlockCheckerPtr dead = DeadlockChecker::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 = dead->check(h1,chm);
- if(path_h1.get()){
- std::cerr << "*** There is deadlock in h1, path:" << std::endl;
- writer.print(path_h1,path_name);
+ if(path_h1.get())
+ {
+ std::cerr << "OK: h1 contains deadlock" << std::endl;
+ return 0;
}
- else
- std::cerr << "*** h1 is deadlock free" << std::endl;
-
- return 0;
+ std::cerr << "ERROR: h1 doesn't contain deadlock" << std::endl;
+ return 1;
}
Modified: trunk/tests/fifo_checker_test.cpp
===================================================================
--- trunk/tests/fifo_checker_test.cpp 2008-11-12 17:12:14 UTC (rev 116)
+++ trunk/tests/fifo_checker_test.cpp 2008-11-16 20:19:35 UTC (rev 117)
@@ -100,55 +100,26 @@
std::cout << "e2 O<----a------O e4" << std::endl;
std::cout << " | | " << std::endl;
- /*
- * New BMsc
- */
- BMscPtr myBmsc(new BMsc);
-
- /*
- * New Instances
- */
- InstancePtr i1(new Instance(myBmsc.get(), "p1"));
+ BMscPtr myBmsc(new BMsc());
+
+ InstancePtr i1(new Instance("p1"));
myBmsc->add_instance(i1);
- InstancePtr i2(new Instance(myBmsc.get(), "p2"));
+ InstancePtr i2(new Instance("p2"));
myBmsc->add_instance(i2);
-
- /*
- * New StrictOrderAreaPtr
- */
- StrictOrderAreaPtr soa1(new StrictOrderArea(i1.get()));
-
- /*
- * New events
- */
- MscMessagePtr a1(new MscMessage(i1.get(), i2.get(), "a"));
- MscMessagePtr a2(new MscMessage(i2.get(), i1.get(), "a"));
- StrictEventPtr e1(new StrictEvent(soa1.get(), a1));
- StrictEventPtr e2(new StrictEvent(soa1.get(), a2));
-
- /**
- * set fisrt area on instance
- * set first event on area
- * set successor of first event
- */
- i1->set_first(soa1);
- soa1->set_first(e1);
- e1->set_successor(e2);
-
-
- /**
- * next strict area
- * next events and their ralations
- */
- StrictOrderAreaPtr soa2(new StrictOrderArea(i2.get()));
-
- StrictEventPtr e3(new StrictEvent(soa2.get(), e1.get()));
- StrictEventPtr e4(new StrictEvent(soa2.get(), e2.get()));
-
- i2->set_first(soa2);
- soa2->set_first(e3);
- e3->set_successor(e4);
+ EventAreaPtr a1(new StrictOrderArea());
+ i1->add_area(a1);
+ EventAreaPtr a2(new StrictOrderArea());
+ i2->add_area(a2);
+
+ EventPtr e1 = a1->add_event();
+ EventPtr e2 = a1->add_event();
+ EventPtr e3 = a2->add_event();
+ EventPtr e4 = a2->add_event();
+
+ e1->send_message(e3.get(),"a");
+ e4->send_message(e2.get(),"a");
+
check(myBmsc,true,true);
}
@@ -161,51 +132,25 @@
std::cout << " | | " << std::endl;
BMscPtr myBmsc(new BMsc);
-
- /*
- * New Instances
- */
- InstancePtr i1(new Instance(myBmsc.get(), "p1"));
+
+ InstancePtr i1(new Instance("p1"));
myBmsc->add_instance(i1);
- InstancePtr i2(new Instance(myBmsc.get(), "p2"));
+ InstancePtr i2(new Instance("p2"));
myBmsc->add_instance(i2);
-
- /*
- * New StrictOrderAreaPtr
- */
- StrictOrderAreaPtr soa1(new StrictOrderArea(i1.get()));
-
- /*
- * New events
- */
- MscMessagePtr a1(new MscMessage(i1.get(), i2.get(), "a"));
- MscMessagePtr a2(new MscMessage(i1.get(), i2.get(), "a"));
- StrictEventPtr e1(new StrictEvent(soa1.get(), a1));
- StrictEventPtr e2(new StrictEvent(soa1.get(), a2));
-
- /**
- * set fisrt area on instance
- * set first event on area
- * set successor of first event
- */
- i1->set_first(soa1);
- soa1->set_first(e1);
- e1->set_successor(e2);
-
-
- /**
- * next strict area
- * next events and their ralations
- */
- StrictOrderAreaPtr soa2(new StrictOrderArea(i2.get()));
-
- StrictEventPtr e3(new StrictEvent(soa2.get(), e1.get()));
- StrictEventPtr e4(new StrictEvent(soa2.get(), e2.get()));
-
- i2->set_first(soa2);
- soa2->set_first(e3);
- e3->set_successor(e4);
-
+
+ EventAreaPtr a1(new StrictOrderArea());
+ i1->add_area(a1);
+ EventAreaPtr a2(new StrictOrderArea());
+ i2->add_area(a2);
+
+ EventPtr e1 = a1->add_event();
+ EventPtr e2 = a1->add_event();
+ EventPtr e3 = a2->add_event();
+ EventPtr e4 = a2->add_event();
+
+ e1->send_message(e3.get(),"a");
+ e2->send_message(e4.get(),"a");
+
check(myBmsc,true,true);
}
@@ -219,56 +164,27 @@
std::cout << " | / \\ | " << std::endl;
std::cout << "e2 O --a->O e4" << std::endl;
std::cout << " | | " << std::endl;
-
- /*
- * New BMsc
- */
+
BMscPtr myBmsc(new BMsc);
-
- /*
- * New Instances
- */
- InstancePtr i1(new Instance(myBmsc.get(), "p1"));
+
+ InstancePtr i1(new Instance("p1"));
myBmsc->add_instance(i1);
- InstancePtr i2(new Instance(myBmsc.get(), "p2"));
+ InstancePtr i2(new Instance("p2"));
myBmsc->add_instance(i2);
-
- /*
- * New StrictOrderAreaPtr
- */
- StrictOrderAreaPtr soa1(new StrictOrderArea(i1.get()));
-
- /*
- * New events
- */
- MscMessagePtr a1(new MscMessage(i1.get(), i2.get(), "a"));
- MscMessagePtr a2(new MscMessage(i1.get(), i2.get(), "a"));
- StrictEventPtr e1(new StrictEvent(soa1.get(), a1));
- StrictEventPtr e2(new StrictEvent(soa1.get(), a2));
-
- /**
- * set fisrt area on instance
- * set first event on area
- * set successor of first event
- */
- i1->set_first(soa1);
- soa1->set_first(e1);
- e1->set_successor(e2);
-
-
- /**
- * next strict area
- * next events and their ralations
- */
- StrictOrderAreaPtr soa2(new StrictOrderArea(i2.get())); //ako by sa to robilo s instance
-
- StrictEventPtr e3(new StrictEvent(soa2.get(), e2.get()));
- StrictEventPtr e4(new StrictEvent(soa2.get(), e1.get()));
-
- i2->set_first(soa2); //neprejde cez compilator neviem ako tam mam zavolat referenciu zmenil som msc.h
- soa2->set_first(e3);
- e3->set_successor(e4);
+ EventAreaPtr s1(new StrictOrderArea());
+ i1->add_area(s1);
+ EventAreaPtr s2(new StrictOrderArea());
+ i2->add_area(s2);
+
+ EventPtr e1 = s1->add_event();
+ EventPtr e2 = s1->add_event();
+ EventPtr e3 = s2->add_event();
+ EventPtr e4 = s2->add_event();
+
+ e1->send_message(e4.get(),"a");
+ e2->send_message(e3.get(),"a");
+
check(myBmsc,false,false);
}
@@ -283,39 +199,27 @@
std::cout << "| | | | " << std::endl;
std::cout << "<coregion> <coregion> " << std::endl;
std::cout << " | | " << std::endl;
-
- /*
- * New BMsc
- */
+
BMscPtr myBmsc(new BMsc);
-
- /*
- * New Instances
- */
- InstancePtr i1(new Instance(myBmsc.get(), "p1"));
+
+ InstancePtr i1(new Instance("p1"));
myBmsc->add_instance(i1);
- InstancePtr i2(new Instance(myBmsc.get(), "p2"));
+ InstancePtr i2(new Instance("p2"));
myBmsc->add_instance(i2);
-
- /*
- * New CoregionAreaPtr
- */
- CoregionAreaPtr ca1(new CoregionArea(i1.get()));
- CoregionAreaPtr ca2(new CoregionArea(i2.get()));
-
- MscMessagePtr a1(new MscMessage(i1.get(), i2.get(), "a"));
- MscMessagePtr a2(new MscMessage(i1.get(), i2.get(), "a"));
- CoregionEvent* e1 = new CoregionEvent(ca1.get(), a1);
- CoregionEvent* e2 = new CoregionEvent(ca1.get(), a2);
- CoregionEvent* e3 = new CoregionEvent(ca2.get(), e1);
- CoregionEvent* e4 = new CoregionEvent(ca2.get(), e2);
-
- i1->set_first(ca1);
- i2->set_first(ca2);
- ca1->add_minimal_event(e1);
- ca1->add_minimal_event(e2);
- ca2->add_minimal_event(e3);
- ca2->add_minimal_event(e4);
+
+ EventAreaPtr ca1(new CoregionArea());
+ i1->add_area(ca1);
+ EventAreaPtr ca2(new CoregionArea());
+ i1->add_area(ca2);
+
+ EventPtr e1 = ca1->add_event();
+ EventPtr e2 = ca1->add_event();
+ EventPtr e3 = ca2->add_event();
+ EventPtr e4 = ca2->add_event();
+
+ e1->send_message(e3.get(),"a");
+ e2->send_message(e4.get(),"a");
+
check(myBmsc,false,false);
}
@@ -330,40 +234,27 @@
std::cout << "| | | " << std::endl;
std::cout << "<coregion> | " << std::endl;
std::cout << " | | " << std::endl;
-
- /*
- * New BMsc
- */
+
BMscPtr myBmsc(new BMsc);
-
- /*
- * New Instances
- */
- InstancePtr i1(new Instance(myBmsc.get(), "p1"));
+
+ InstancePtr i1(new Instance("p1"));
myBmsc->add_instance(i1);
- InstancePtr i2(new Instance(myBmsc.get(), "p2"));
+ InstancePtr i2(new Instance("p2"));
myBmsc->add_instance(i2);
-
- /*
- * New CoregionAreaPtr
- */
- CoregionAreaPtr ca1(new CoregionArea(i1.get()));
- StrictOrderAreaPtr soa1(new StrictOrderArea(i2.get()));
-
- MscMessagePtr a1(new MscMessage(i1.get(), i2.get(), "a"));
- MscMessagePtr a2(new MscMessage(i1.get(), i2.get(), "a"));
- CoregionEvent* e1 = new CoregionEvent(ca1.get(), a1);
- CoregionEvent* e2 = new CoregionEvent(ca1.get(), a2);
- StrictEventPtr e3(new StrictEvent(soa1.get(), e1));
- StrictEventPtr e4(new StrictEvent(soa1.get(), e2));
- i1->set_first(ca1);
- i2->set_first(soa1);
- ca1->add_minimal_event(e1);
- ca1->add_minimal_event(e2);
- soa1->set_first(e3);
- e3->set_successor(e4);
+ EventAreaPtr c(new CoregionArea());
+ i1->add_area(c);
+ EventAreaPtr s(new StrictOrderArea());
+ i2->add_area(s);
+ EventPtr e1 = c->add_event();
+ EventPtr e2 = c->add_event();
+ EventPtr e3 = s->add_event();
+ EventPtr e4 = s->add_event();
+
+ e1->send_message(e3.get(),"a");
+ e2->send_message(e4.get(),"a");
+
check(myBmsc,false,false);
}
@@ -378,34 +269,27 @@
std::cout << "| | | " << std::endl;
std::cout << "<coregion> | " << std::endl;
std::cout << " | | " << std::endl;
+
BMscPtr myBmsc(new BMsc);
- /*
- * New Instances
- */
- InstancePtr i1(new Instance(myBmsc.get(), "p1"));
+
+ InstancePtr i1(new Instance("p1"));
myBmsc->add_instance(i1);
- InstancePtr i2(new Instance(myBmsc.get(), "p2"));
+ InstancePtr i2(new Instance("p2"));
myBmsc->add_instance(i2);
- /*
- * New CoregionAreaPtr
- */
- CoregionAreaPtr ca1(new CoregionArea(i1.get()));
- StrictOrderAreaPtr soa1(new StrictOrderArea(i2.get()));
-
- MscMessagePtr a1(new MscMessage(i2.get(), i1.get(), "a"));
- MscMessagePtr a2(new MscMessage(i2.get(), i1.get(), "a"));
- CoregionEvent* e1 = new CoregionEvent(ca1.get(), a1);
- CoregionEvent* e2 = new CoregionEvent(ca1.get(), a2);
- StrictEventPtr e3(new StrictEvent(soa1.get(), e1));
- StrictEventPtr e4(new StrictEvent(soa1.get(), e2));
- i1->set_first(ca1);
- i2->set_first(soa1);
- ca1->add_minimal_event(e1);
- ca1->add_minimal_event(e2);
- soa1->set_first(e3);
- e3->set_successor(e4);
+ EventAreaPtr ca1(new CoregionArea());
+ i1->add_area(ca1);
+ EventAreaPtr soa1(new StrictOrderArea());
+ i2->add_area(soa1);
+ EventPtr e1 = ca1->add_event();
+ EventPtr e2 = ca1->add_event();
+ EventPtr e3 = soa1->add_event();
+ EventPtr e4 = soa1->add_event();
+
+ e3->send_message(e1.get(),"a");
+ e4->send_message(e2.get(),"a");
+
check(myBmsc,false,false);
}
@@ -422,33 +306,25 @@
std::cout << " | | " << std::endl;
BMscPtr myBmsc(new BMsc);
- /*
- * New Instances
- */
- InstancePtr i1(new Instance(myBmsc.get(), "p1"));
+
+ InstancePtr i1(new Instance("p1"));
myBmsc->add_instance(i1);
- InstancePtr i2(new Instance(myBmsc.get(), "p2"));
+ InstancePtr i2(new Instance("p2"));
myBmsc->add_instance(i2);
- /*
- * New CoregionAreaPtr
- */
- CoregionAreaPtr ca1(new CoregionArea(i1.get()));
- StrictOrderAreaPtr soa1(new StrictOrderArea(i2.get()));
-
- MscMessagePtr a1(new MscMessage(i2.get(), i1.get(), "a"));
- MscMessagePtr a2(new MscMessage(i1.get(), i2.get(), "a"));
- CoregionEvent* e1 = new CoregionEvent(ca1.get(), a1);
- CoregionEvent* e2 = new CoregionEvent(ca1.get(), a2);
- StrictEventPtr e3(new StrictEvent(soa1.get(), e1));
- StrictEventPtr e4(new StrictEvent(soa1.get(), e2));
- i1->set_first(ca1);
- i2->set_first(soa1);
- ca1->add_minimal_event(e1);
- ca1->add_minimal_event(e2);
- soa1->set_first(e3);
- e3->set_successor(e4);
+ EventAreaPtr ca1(new CoregionArea());
+ i1->add_area(ca1);
+ EventAreaPtr soa1(new StrictOrderArea());
+ i2->add_area(soa1);
+ EventPtr e1 = ca1->add_event();
+ EventPtr e2 = ca1->add_event();
+ EventPtr e3 = soa1->add_event();
+ EventPtr e4 = soa1->add_event();
+
+ e3->send_message(e1.get(),"a");
+ e2->send_message(e4.get(),"a");
+
check(myBmsc,true,true);
}
@@ -459,55 +335,27 @@
std::cout << " | | " << std::endl;
std::cout << "e2 O<----a------O e4" << std::endl;
std::cout << " | | " << std::endl;
-
- /*
- * New BMsc
- */
+
BMscPtr myBmsc(new BMsc);
-
- /*
- * New Instances
- */
- InstancePtr i1(new Instance(myBmsc.get(), "p1"));
+
+ InstancePtr i1(new Instance("p1"));
myBmsc->add_instance(i1);
- InstancePtr i2(new Instance(myBmsc.get(), "p2"));
+ InstancePtr i2(new Instance("p2"));
myBmsc->add_instance(i2);
-
- /*
- * New StrictOrderAreaPtr
- */
- StrictOrderAreaPtr soa1(new StrictOrderArea(i1.get()));
-
- /*
- * New events
- */
- MscMessagePtr b1(new MscMessage(i1.get(), i2.get(), "b"));
- MscMessagePtr a1(new MscMessage(i2.get(), i1.get(), "a"));
- StrictEventPtr e1(new StrictEvent(soa1.get(), b1));
- StrictEventPtr e2(new StrictEvent(soa1.get(), a1));
-
- /**
- * set fisrt area on instance
- * set first event on area
- * set successor of first event
- */
- i1->set_first(soa1);
- soa1->set_first(e1);
- e1->set_successor(e2);
-
-
- /**
- * next strict area
- * next events and their ralations
- */
- StrictOrderAreaPtr soa2(new StrictOrderArea(i2.get()));
-
- StrictEventPtr e3(new StrictEvent(soa2.get(), e1.get()));
- StrictEventPtr e4(new StrictEvent(soa2.get(), e2.get()));
-
- i2->set_first(soa2);
- soa2->set_first(e3);
- e3->set_successor(e4);
+
+ EventAreaPtr s1(new CoregionArea());
+ i1->add_area(s1);
+ EventAreaPtr s2(new StrictOrderArea());
+ i2->add_area(s2);
+
+ EventPtr e1 = s1->add_event();
+ EventPtr e2 = s1->add_event();
+ EventPtr e3 = s2->add_event();
+ EventPtr e4 = s2->add_event();
+
+ e1->send_message(e3.get(),"b");
+ e4->send_message(e2.get(),"a");
+
check(myBmsc,true,true);
}
@@ -520,50 +368,25 @@
std::cout << " | | " << std::endl;
BMscPtr myBmsc(new BMsc);
-
- /*
- * New Instances
- */
- InstancePtr i1(new Instance(myBmsc.get(), "p1"));
+
+ InstancePtr i1(new Instance("p1"));
myBmsc->add_instance(i1);
- InstancePtr i2(new Instance(myBmsc.get(), "p2"));
+ InstancePtr i2(new Instance("p2"));
myBmsc->add_instance(i2);
-
- /*
- * New StrictOrderAreaPtr
- */
- StrictOrderAreaPtr soa1(new StrictOrderArea(i1.get()));
-
- /*
- * New events
- */
- MscMessagePtr a1(new MscMessage(i1.get(), i2.get(), "a"));
- MscMessagePtr b1(new MscMessage(i1.get(), i2.get(), "b"));
- StrictEventPtr e1(new StrictEvent(soa1.get(), a1));
- StrictEventPtr e2(new StrictEvent(soa1.get(), b1));
-
- /**
- * set fisrt area on instance
- * set first event on area
- * set successor of first event
- */
- i1->set_first(soa1);
- soa1->set_first(e1);
- e1->set_successor(e2);
-
-
- /**
- * next strict area
- * next events and their ralations
- */
- StrictOrderAreaPtr soa2(new StrictOrderArea(i2.get()));
-
- StrictEventPtr e3(new StrictEvent(soa2.get(), e1.get()));
- StrictEventPtr e4(new StrictEvent(soa2.get(), e2.get()));
-
- i2->set_first(soa2);
- soa2->set_first(e3);
- e3->set_successor(e4);
+
+ EventAreaPtr s1(new StrictOrderArea());
+ i1->add_area(s1);
+ EventAreaPtr s2(new StrictOrderArea());
+ i2->add_area(s2);
+
+ EventPtr e1 = s1->add_event();
+ EventPtr e2 = s1->add_event();
+ EventPtr e3 = s2->add_event();
+ EventPtr e4 = s2->add_event();
+
+ e1->send_message(e3.get(),"a");
+ e2->send_message(e4.get(),"b");
+
check(myBmsc,true,true);
}
@@ -578,54 +401,26 @@
std::cout << "e2 O --b->O e4" << std::endl;
std::cout << " | | " << std::endl;
- /*
- * New BMsc
- */
BMscPtr myBmsc(new BMsc);
-
- /*
- * New Instances
- */
- InstancePtr i1(new Instance(myBmsc.get(), "p1"));
+
+ InstancePtr i1(new Instance("p1"));
myBmsc->add_instance(i1);
- InstancePtr i2(new Instance(myBmsc.get(), "p2"));
+ InstancePtr i2(new Instance("p2"));
myBmsc->add_instance(i2);
-
- /*
- * New StrictOrderAreaPtr
- */
- StrictOrderAreaPtr soa1(new StrictOrderArea(i1.get()));
-
- /*
- * New events
- */
- MscMessagePtr a1(new MscMessage(i1.get(), i2.get(), "a"));
- MscMessagePtr b1(new MscMessage(i1.get(), i2.get(), "b"));
- StrictEventPtr e1(new StrictEvent(soa1.get(), a1));
- StrictEventPtr e2(new StrictEvent(soa1.get(), b1));
-
- /**
- * set fisrt area on instance
- * set first event on area
- * set successor of first event
- */
- i1->set_first(soa1);
- soa1->set_first(e1);
- e1->set_successor(e2);
-
-
- /**
- * next strict area
- * next events and their ralations
- */
- StrictOrderAreaPtr soa2(new StrictOrderArea(i2.get())); //ako by sa to robilo s instance
-
- StrictEventPtr e3(new StrictEvent(soa2.get(), e2.get()));
- StrictEventPtr e4(new StrictEvent(soa2.get(), e1.get()));
-
- i2->set_first(soa2); //neprejde cez compilator neviem ako tam mam zavolat referenciu zmenil som msc.h
- soa2->set_first(e3);
- e3->set_successor(e4);
+
+ EventAreaPtr a1(new StrictOrderArea());
+ i1->add_area(a1);
+ EventAreaPtr a2(new StrictOrderArea());
+ i2->add_area(a2);
+
+ EventPtr e1 = a1->add_event();
+ EventPtr e2 = a1->add_event();
+ EventPtr e3 = a2->add_event();
+ EventPtr e4 = a2->add_event();
+
+ e2->send_message(e3.get(),"a");
+ e1->send_message(e4.get(),"b");
+
check(myBmsc,false,true);
}
@@ -641,39 +436,26 @@
std::cout << "<coregion> <coregion> " << std::endl;
std::cout << " | | " << std::endl;
- /*
- * New BMsc
- */
BMscPtr myBmsc(new BMsc);
-
- /*
- * New Instances
- */
- InstancePtr i1(new Instance(myBmsc.get(), "p1"));
+
+ InstancePtr i1(new Instance("p1"));
myBmsc->add_instance(i1);
- InstancePtr i2(new Instance(myBmsc.get(), "p2"));
+ InstancePtr i2(new Instance("p2"));
myBmsc->add_instance(i2);
-
- /*
- * New CoregionAreaPtr
- */
- CoregionAreaPtr ca1(new CoregionArea(i1.get()));
- CoregionAreaPtr ca2(new CoregionArea(i2.get()));
-
- MscMessagePtr a1(new MscMessage(i1.get(), i2.get(), "a"));
- MscMessagePtr b1(new MscMessage(i1.get(), i2.get(), "b"));
- CoregionEvent* e1 = new CoregionEvent(ca1.get(), a1);
- CoregionEvent* e2 = new CoregionEvent(ca1.get(), b1);
- CoregionEvent* e3 = new CoregionEvent(ca2.get(), e1);
- CoregionEvent* e4 = new CoregionEvent(ca2.get(), e2);
- i1->set_first(ca1);
- i2->set_first(ca2);
- ca1->add_minimal_event(e1);
- ca1->add_minimal_event(e2);
- ca2->add_minimal_event(e3);
- ca2->add_minimal_event(e4);
+ EventAreaPtr a1(new CoregionArea());
+ i1->add_area(a1);
+ EventAreaPtr a2(new CoregionArea());
+ i2->add_area(a2);
+ EventPtr e1 = a1->add_event();
+ EventPtr e2 = a1->add_event();
+ EventPtr e3 = a2->add_event();
+ EventPtr e4 = a2->add_event();
+
+ e1->send_message(e3.get(),"a");
+ e2->send_message(e4.get(),"b");
+
check(myBmsc,false,true);
}
@@ -689,39 +471,26 @@
std::cout << "<coregion> | " << std::endl;
std::cout << " | | " << std::endl;
- /*
- * New BMsc
- */
BMscPtr myBmsc(new BMsc);
-
- /*
- * New Instances
- */
- InstancePtr i1(new Instance(myBmsc.get(), "p1"));
+
+ InstancePtr i1(new Instance("p1"));
myBmsc->add_instance(i1);
- InstancePtr i2(new Instance(myBmsc.get(), "p2"));
+ InstancePtr i2(new Instance("p2"));
myBmsc->add_instance(i2);
-
- /*
- * New CoregionAreaPtr
- */
- CoregionAreaPtr ca1(new CoregionArea(i1.get()));
- StrictOrderAreaPtr soa1(new StrictOrderArea(i2.get()));
-
- MscMessagePtr a1(new MscMessage(i1.get(), i2.get(), "a"));
- MscMessagePtr b1(new MscMessage(i1.get(), i2.get(), "b"));
- CoregionEvent* e1 = new CoregionEvent(ca1.get(), a1);
- CoregionEvent* e2 = new CoregionEvent(ca1.get(), b1);
- StrictEventPtr e3(new StrictEvent(soa1.get(), e1));
- StrictEventPtr e4(new StrictEvent(soa1.get(), e2));
- i1->set_first(ca1);
- i2->set_first(soa1);
- ca1->add_minimal_event(e1);
- ca1->add_minimal_event(e2);
- soa1->set_first(e3);
- e3->set_successor(e4);
+ EventAreaPtr a1(new CoregionArea());
+ i1->add_area(a1);
+ EventAreaPtr a2(new StrictOrderArea());
+ i2->add_area(a2);
+ EventPtr e1 = a1->add_event();
+ EventPtr e2 = a1->add_event();
+ EventPtr e3 = a2->add_event();
+ EventPtr e4 = a2->add_event();
+
+ e1->send_message(e3.get(),"a");
+ e2->send_message(e4.get(),"b");
+
check(myBmsc,false,true);
}
@@ -737,34 +506,27 @@
std::cout << "| | | " << std::endl;
std::cout << "<coregion> | " << std::endl;
std::cout << " | | " << std::endl;
+
BMscPtr myBmsc(new BMsc);
- /*
- * New Instances
- */
- InstancePtr i1(new Instance(myBmsc.get(), "p1"));
+
+ InstancePtr i1(new Instance("p1"));
myBmsc->add_instance(i1);
- InstancePtr i2(new Instance(myBmsc.get(), "p2"));
+ InstancePtr i2(new Instance("p2"));
myBmsc->add_instance(i2);
- /*
- * New CoregionAreaPtr
- */
- CoregionAreaPtr ca1(new CoregionArea(i1.get()));
- StrictOrderAreaPtr soa1(new StrictOrderArea(i2.get()));
-
- MscMessagePtr a1(new MscMessage(i2.get(), i1.get(), "a"));
- MscMessagePtr b1(new MscMessage(i2.get(), i1.get(), "b"));
- CoregionEvent* e1 = new CoregionEvent(ca1.get(), a1);
- CoregionEvent* e2 = new CoregionEvent(ca1.get(), b1);
- StrictEventPtr e3(new StrictEvent(soa1.get(), e1));
- StrictEventPtr e4(new StrictEvent(soa1.get(), e2));
- i1->set_first(ca1);
- i2->set_first(soa1);
- ca1->add_minimal_event(e1);
- ca1->add_minimal_event(e2);
- soa1->set_first(e3);
- e3->set_successor(e4);
+ EventAreaPtr a1(new CoregionArea());
+ i1->add_area(a1);
+ EventAreaPtr a2(new StrictOrderArea());
+ i2->add_area(a2);
+ EventPtr e1 = a1->add_event();
+ EventPtr e2 = a1->add_event();
+ EventPtr e3 = a2->add_event();
+ EventPtr e4 = a2->add_event();
+
+ e3->send_message(e1.get(),"a");
+ e4->send_message(e2.get(),"b");
+
check(myBmsc,false,true);
}
@@ -781,33 +543,25 @@
std::cout << " | | " << std::endl;
BMscPtr myBmsc(new BMsc);
- /*
- * New Instances
- */
- InstancePtr i1(new Instance(myBmsc.get(), "p1"));
+
+ InstancePtr i1(new Instance("p1"));
myBmsc->add_instance(i1);
- InstancePtr i2(new Instance(myBmsc.get(), "p2"));
+ InstancePtr i2(new Instance("p2"));
myBmsc->add_instance(i2);
- /*
- * New CoregionAreaPtr
- */
- CoregionAreaPtr ca1(new CoregionArea(i1.get()));
- StrictOrderAreaPtr soa1(new StrictOrderArea(i2.get()));
-
- MscMessagePtr a1(new MscMessage(i2.get(), i1.get(), "a"));
- MscMessagePtr b1(new MscMessage(i1.get(), i2.get(), "b"));
- CoregionEvent* e1 = new CoregionEvent(ca1.get(), a1);
- CoregionEvent* e2 = new CoregionEvent(ca1.get(), b1);
- StrictEventPtr e3(new StrictEvent(soa1.get(), e1));
- StrictEventPtr e4(new StrictEvent(soa1.get(), e2));
- i1->set_first(ca1);
- i2->set_first(soa1);
- ca1->add_minimal_event(e1);
- ca1->add_minimal_event(e2);
- soa1->set_first(e3);
- e3->set_successor(e4);
+ EventAreaPtr a1(new CoregionArea());
+ i1->add_area(a1);
+ EventAreaPtr a2(new StrictOrderArea());
+ i2->add_area(a2);
+ EventPtr e1 = a1->add_event();
+ EventPtr e2 = a1->add_event();
+ EventPtr e3 = a2->add_event();
+ EventPtr e4 = a2->add_event();
+
+ e3->send_message(e1.get(),"a");
+ e2->send_message(e4.get(),"b");
+
check(myBmsc,true,true);
}
@@ -825,43 +579,29 @@
std::cout << "<coregion> <coregion> " << std::endl;
std::cout << " | | " << std::endl;
- /*
- * New BMsc
- */
BMscPtr myBmsc(new BMsc);
-
- /*
- * New Instances
- */
- InstancePtr i1(new Instance(myBmsc.get(), "p1"));
+
+ InstancePtr i1(new Instance("p1"));
myBmsc->add_instance(i1);
- InstancePtr i2(new Instance(myBmsc.get(), "p2"));
+ InstancePtr i2(new Instance("p2"));
myBmsc->add_instance...
[truncated message content] |
