Menu
▾
▴
[Scstudio-commits] SF.net SVN: scstudio:[111] trunk/src
|
From: <ba...@us...> - 2008-10-05 18:05:46
|
Revision: 111
http://scstudio.svn.sourceforge.net/scstudio/?rev=111&view=rev
Author: babicaj
Date: 2008-10-05 18:03:03 +0000 (Sun, 05 Oct 2008)
Log Message:
-----------
Structure of HMsc was customized for graphical representation. Traversers of HMsc was modified in appropriate way. It is more than possible that checkers need to be modified too. Sorry for current compilation problem it will be corrected as soon as possible.
Modified Paths:
--------------
trunk/src/check/dfs_bmsc_graph_traverser.cpp
trunk/src/check/dfs_bmsc_graph_traverser.h
trunk/src/check/dfs_hmsc_traverser.cpp
trunk/src/check/dfs_hmsc_traverser.h
trunk/src/check/footprint.cpp
trunk/src/check/footprint.h
trunk/src/check/race_checker.cpp
trunk/src/check/race_checker.h
trunk/src/data/counted_ptr.h
trunk/src/data/msc.cpp
trunk/src/data/msc.h
Added Paths:
-----------
trunk/src/check/refnode_finder.cpp
trunk/src/check/refnode_finder.h
trunk/src/data/msc_visual.h
Modified: trunk/src/check/dfs_bmsc_graph_traverser.cpp
===================================================================
--- trunk/src/check/dfs_bmsc_graph_traverser.cpp 2008-10-04 22:31:47 UTC (rev 110)
+++ trunk/src/check/dfs_bmsc_graph_traverser.cpp 2008-10-05 18:03:03 UTC (rev 111)
@@ -27,67 +27,95 @@
void DFSBMscGraphTraverser::traverse(HMscPtr hmsc)
{
- m_colored_nodes.push_back(InnerNodePList());
- traverse_successors(hmsc->get_start()->get_successors());
+ push_top_attributes();
+ traverse_node(hmsc->get_start().get());
cleanup_traversing_attributes();
}
-bool DFSBMscGraphTraverser::traverse_node(InnerNode* node)
+bool DFSBMscGraphTraverser::traverse_node(HMscNode* node)
{
- Color c = get_color(node);
- if(c==BLACK)
+ if(is_processed(node))
{
- black_node_found(node);
return false;
}
- if(c==GRAY)
- {
- gray_node_found(node);
- return false;
- }
white_node_found(node);
ReferenceNode* ref_node = dynamic_cast<ReferenceNode*>(node);
if(ref_node!=NULL)
{
- HMscPtr hmsc = ref_node->get_hmsc();
- if(hmsc.get()!=NULL)
+ return traverse_node(ref_node);
+ }
+ else
+ {
+ bool ending_successors;
+ ConnectionNode* conn_node = dynamic_cast<ConnectionNode*>(node);
+ if(conn_node)
{
- m_reached_nodes.push_back(InnerNodePList());
- //this line ensures (yet another one) that HMsc will be traversed as many times
- //as it is referenced
- m_colored_nodes.push_back(InnerNodePList());
- //node's successors aren't traversed if end node wasn't found in hmsc
- return traverse_successors(hmsc->get_start()->get_successors()) &&
- (traverse_successors(node->get_successors()) || ref_node->is_end_node());
- //this line ensures (yet another one) that HMsc will traversed as many times
- //as it is referenced
- cleanup_top_attributes();
- m_reached_nodes.pop_back();
+ ending_successors = traverse_successors(conn_node);
}
+ else
+ {
+ StartNode* start_node = dynamic_cast<StartNode*>(node);
+ if(start_node)
+ {
+ ending_successors = traverse_successors(start_node);
+ }
+ else
+ {
+ //node is supposed to be EndNode
+ ending_successors = true;
+ }
+ }
+ node_finished(node);
+ return ending_successors;
}
- bool ending_successors = traverse_successors(node->get_successors());
- node_finished(node);
- return ending_successors || (ref_node!=NULL && ref_node->is_end_node());
}
-bool DFSBMscGraphTraverser::traverse_successors(const InnerNodePSet& successors)
+bool DFSBMscGraphTraverser::traverse_node(ReferenceNode* ref_node)
{
+ HMscPtr hmsc = ref_node->get_hmsc();
+ bool inner = true;
+ if(hmsc.get()!=NULL)
+ {
+ //this line ensures (yet another one) that HMsc will be traversed as many times
+ //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());
+ //this line ensures (yet another one) that HMsc will traversed as many times
+ //as it is referenced
+ cleanup_top_attributes();
+ }
+ return inner && traverse_successors(ref_node);
+}
+
+bool DFSBMscGraphTraverser::traverse_successors(PredecessorNode* predecessor)
+{
bool end_found = false;
- InnerNodePSet::const_iterator successor;
- for(successor=successors.begin();successor!=successors.end();successor++)
+ NodeRelationPtrSet::const_iterator relation;
+ for(relation=predecessor->get_successors().begin();
+ relation!=predecessor->get_successors().end();relation++)
{
- end_found = traverse_node(*successor) || end_found;
+ const NodeRelationPtr& rel = *relation;
+ m_reached_nodes.back().push_back(rel);
+ end_found = traverse_node((HMscNode*)rel->get_successor()) || end_found;
}
return end_found;
}
-void DFSBMscGraphTraverser::cleanup_top_attributes()
+bool DFSBMscGraphTraverser::is_processed(HMscNode* node)
{
- InnerNodePList& top = m_colored_nodes.back();
- InnerNodePList::iterator event;
- for(event=top.begin();event!=top.end();event++)
- (*event)->remove_attribute<Color>(m_color_attribute);
- m_colored_nodes.pop_back();
+ Color c = get_color(node);
+ if(c==BLACK)
+ {
+ black_node_found(node);
+ return true;
+ }
+ if(c==GRAY)
+ {
+ gray_node_found(node);
+ return true;
+ }
+ return false;
}
void DFSBMscGraphTraverser::cleanup_traversing_attributes()
@@ -96,16 +124,10 @@
{
cleanup_top_attributes();
}
- while(!m_reached_nodes.empty())
- {
- m_reached_nodes.pop_back();
- }
-
}
-void DFSBMscGraphTraverser::white_node_found(InnerNode* n)
+void DFSBMscGraphTraverser::white_node_found(HMscNode* n)
{
- m_reached_nodes.back().push_back(n);
WhiteNodeFoundListenerPList::iterator l;
for(l=m_white_node_found_listeners.begin();l!=m_white_node_found_listeners.end();l++)
(*l)->on_white_node_found(n);
@@ -113,21 +135,23 @@
m_colored_nodes.back().push_back(n);
}
-void DFSBMscGraphTraverser::gray_node_found(InnerNode* n)
+void DFSBMscGraphTraverser::gray_node_found(HMscNode* n)
{
GrayNodeFoundListenerPList::iterator l;
for(l=m_gray_node_found_listeners.begin();l!=m_gray_node_found_listeners.end();l++)
(*l)->on_gray_node_found(n);
+ m_reached_nodes.back().pop_back();
}
-void DFSBMscGraphTraverser::black_node_found(InnerNode* n)
+void DFSBMscGraphTraverser::black_node_found(HMscNode* n)
{
BlackNodeFoundListenerPList::iterator l;
for(l=m_black_node_found_listeners.begin();l!=m_black_node_found_listeners.end();l++)
(*l)->on_black_node_found(n);
+ m_reached_nodes.back().pop_back();
}
-void DFSBMscGraphTraverser::node_finished(InnerNode* n)
+void DFSBMscGraphTraverser::node_finished(HMscNode* n)
{
NodeFinishedListenerPList::iterator l;
for(l=m_node_finished_listeners.begin();l!=m_node_finished_listeners.end();l++)
@@ -136,3 +160,19 @@
set_color(n,BLACK);
}
+void DFSBMscGraphTraverser::cleanup_top_attributes()
+{
+ HMscNodePList& top = m_colored_nodes.back();
+ HMscNodePList::iterator event;
+ for(event=top.begin();event!=top.end();event++)
+ (*event)->remove_attribute<Color>(m_color_attribute);
+ m_colored_nodes.pop_back();
+ m_reached_nodes.pop_back();
+}
+
+void DFSBMscGraphTraverser::push_top_attributes()
+{
+ m_colored_nodes.push_back(HMscNodePList());
+ m_reached_nodes.push_back(NodeRelationPtrList());
+}
+
Modified: trunk/src/check/dfs_bmsc_graph_traverser.h
===================================================================
--- trunk/src/check/dfs_bmsc_graph_traverser.h 2008-10-04 22:31:47 UTC (rev 110)
+++ trunk/src/check/dfs_bmsc_graph_traverser.h 2008-10-05 18:03:03 UTC (rev 111)
@@ -24,11 +24,14 @@
#include "data/msc.h"
#include "check/checker.h"
-typedef std::list<InnerNode*> InnerNodePList;
-typedef std::list<InnerNodePList> InnerNodePListList;
+typedef std::list<HMscNode*> HMscNodePList;
+typedef std::list<HMscNodePList> HMscNodePListList;
+typedef std::list<NodeRelationPtr> NodeRelationPtrList;
+typedef std::list<NodeRelationPtrList> NodeRelationPtrListList;
+
/**
- * Listener of founded white InnerNode
+ * Listener of founded white HMscNode
*/
class WhiteNodeFoundListener
{
@@ -39,11 +42,11 @@
}
- virtual void on_white_node_found(InnerNode* n)=0;
+ virtual void on_white_node_found(HMscNode* n)=0;
};
/**
- * Listener of founded gray InnerNode
+ * Listener of founded gray HMscNode
*/
class GrayNodeFoundListener
{
@@ -54,11 +57,11 @@
}
- virtual void on_gray_node_found(InnerNode* n)=0;
+ virtual void on_gray_node_found(HMscNode* n)=0;
};
/**
- * Listener of founded black InnerNode
+ * Listener of founded black HMscNode
*/
class BlackNodeFoundListener
{
@@ -69,11 +72,11 @@
}
- virtual void on_black_node_found(InnerNode* n)=0;
+ virtual void on_black_node_found(HMscNode* n)=0;
};
/**
- * Listener of finished InnerNode
+ * Listener of finished HMscNode
*/
class NodeFinishedListener
{
@@ -84,11 +87,11 @@
}
- virtual void on_node_finished(InnerNode* node)=0;
+ virtual void on_node_finished(HMscNode* node)=0;
};
/**
- * Auxiliary listener of founded white InnerNode.
+ * Auxiliary listener of founded white HMscNode.
*
* Extend this listener to process only ReferenceNodes during traversing.
*/
@@ -101,7 +104,7 @@
}
- virtual void on_white_node_found(InnerNode* n){
+ virtual void on_white_node_found(HMscNode* n){
ReferenceNode* ref = dynamic_cast<ReferenceNode*>(n);
if(ref!=NULL)
{
@@ -113,7 +116,7 @@
};
/**
- * Auxiliary listener of founded gray InnerNode.
+ * Auxiliary listener of founded gray HMscNode.
*
* Extend this listener to process only ReferenceNodes during traversing.
*/
@@ -126,7 +129,7 @@
}
- virtual void on_gray_node_found(InnerNode* n){
+ virtual void on_gray_node_found(HMscNode* n){
ReferenceNode* ref = dynamic_cast<ReferenceNode*>(n);
if(ref!=NULL)
{
@@ -138,7 +141,7 @@
};
/**
- * Auxiliary listener of founded black InnerNode.
+ * Auxiliary listener of founded black HMscNode.
*
* Extend this listener to process only ReferenceNodes during traversing.
*/
@@ -151,7 +154,7 @@
}
- virtual void on_black_node_found(InnerNode* n){
+ virtual void on_black_node_found(HMscNode* n){
ReferenceNode* ref = dynamic_cast<ReferenceNode*>(n);
if(ref!=NULL)
{
@@ -163,7 +166,7 @@
};
/**
- * Auxiliary listener of finished InnerNode.
+ * Auxiliary listener of finished HMscNode.
*
* Extend this listener to process only ReferenceNodes during traversing.
*/
@@ -176,7 +179,7 @@
}
- virtual void on_node_finished(InnerNode* n){
+ virtual void on_node_finished(HMscNode* n){
ReferenceNode* ref = dynamic_cast<ReferenceNode*>(n);
if(ref!=NULL)
{
@@ -197,7 +200,7 @@
typedef std::list<BlackNodeFoundListenerP> BlackNodeFoundListenerPList;
/**
- * Traverses all accessible InnerNodes in HMsc and referenced HMsc in depth
+ * Traverses all accessible HMscNodes in HMsc and referenced HMsc in depth
* first search manner.
*
* HMsc is traversed like BMsc-graph (flattened version of HMsc - each
@@ -205,15 +208,15 @@
* many times as it is referenced. If ReferenceNode references HMsc, this HMsc
* is traversed before successors of referencing node are processed.
*
- * InnerNodes of HMsc are during traversing in different states - with different
+ * HMscNodes of HMsc are during traversing in different states - with different
* color. WHITE color means that node wasn't traversed before. GRAY nodes
* are those which have been already traversed and they are just on the stack -
* not all successors of these events were processed. BLACK nodes are those
* which have been already traversed but aren't yet on the stack - all
* successors have been processed.
*
- * Note that not all InnerNodes must be traversed by this DFSBMscGraphTraverser,
- * imagine InnerNode B which is accessible only from ReferenceNode A but A's
+ * Note that not all HMscNodes must be traversed by this DFSBMscGraphTraverser,
+ * imagine HMscNode B which is accessible only from ReferenceNode A but A's
* HMsc hasn't got any end node.
*
* @warning Non-recursive HMsc is expected.
@@ -224,7 +227,7 @@
public:
/**
- * To change default name of attribute which holds color of InnerNodes use
+ * To change default name of attribute which holds color of HMscNodes use
* color_attribute parameter.
*/
DFSBMscGraphTraverser(const std::string& color_attribute = "msc_graph_traverse_color")
@@ -312,13 +315,13 @@
}
/**
- * Returns reached InnerNodes in particular phase of traversing.
+ * Returns reached HMscNodes in particular phase of traversing.
*
- * The result corresponds to call stack on particular InnerNodes.
+ * The result corresponds to call stack on particular HMscNodes.
*
* Warning: The result is emptied when cleanup_traversing_attributes() is called
*/
- const InnerNodePListList& get_reached_nodes()
+ const NodeRelationPtrListList& get_reached_nodes()
{
return m_reached_nodes;
}
@@ -328,27 +331,34 @@
/**
* Holds nodes with set color attribute
*/
- InnerNodePListList m_colored_nodes;
+ HMscNodePListList m_colored_nodes;
/**
- * Holds currently reached InnerNodes.
+ * Holds currently reached HMscNodes.
*/
- InnerNodePListList m_reached_nodes;
+ NodeRelationPtrListList m_reached_nodes;
/**
* Cleans up traversing attributes from the top of m_colored_nodes
*/
- void cleanup_top_attributes();
+ virtual void cleanup_top_attributes();
/**
* Traverses single node
*/
- virtual bool traverse_node(InnerNode* node);
+ virtual bool traverse_node(HMscNode* node);
/**
* Traverses successors
*/
- virtual bool traverse_successors(const InnerNodePSet& successors);
+ virtual bool traverse_successors(PredecessorNode* predecessor);
+
+ /**
+ * Returns true iff node is just processed false otherwise
+ */
+ virtual bool is_processed(HMscNode* node);
+
+ virtual bool traverse_node(ReferenceNode* node);
/**
* Holds listeners
@@ -381,29 +391,29 @@
std::string m_color_attribute;
/**
- * Called when white InnerNode is found.
+ * Called when white HMscNode is found.
*/
- virtual void white_node_found(InnerNode* n);
+ virtual void white_node_found(HMscNode* n);
/**
- * Called when gray InnerNode is found.
+ * Called when gray HMscNode is found.
*/
- virtual void gray_node_found(InnerNode* n);
+ virtual void gray_node_found(HMscNode* n);
/**
- * Called when black InnerNode is found.
+ * Called when black HMscNode is found.
*/
- virtual void black_node_found(InnerNode* n);
+ virtual void black_node_found(HMscNode* n);
/**
* Called when all successors of e are processed.
*/
- virtual void node_finished(InnerNode* n);
+ virtual void node_finished(HMscNode* n);
/**
* Sets color attribute of e to c value .
*/
- void set_color(InnerNode* n, Color c)
+ void set_color(HMscNode* n, Color c)
{
n->set_attribute<Color>(m_color_attribute,c);
}
@@ -413,11 +423,14 @@
*
* If attribute isn't set it is set to default value WHITE.
*/
- Color get_color(InnerNode* n)
+ Color get_color(HMscNode* n)
{
return n->get_attribute<Color>(m_color_attribute,WHITE);
}
+ virtual void push_top_attributes();
+
+
};
Modified: trunk/src/check/dfs_hmsc_traverser.cpp
===================================================================
--- trunk/src/check/dfs_hmsc_traverser.cpp 2008-10-04 22:31:47 UTC (rev 110)
+++ trunk/src/check/dfs_hmsc_traverser.cpp 2008-10-05 18:03:03 UTC (rev 111)
@@ -18,35 +18,25 @@
#include "check/dfs_hmsc_traverser.h"
-bool DFSHMscTraverser::traverse_node(InnerNode* node)
+bool DFSHMscTraverser::traverse_node(ReferenceNode* ref_node)
{
- Color c = get_color(node);
- if(c==BLACK)
+ HMscPtr hmsc = ref_node->get_hmsc();
+ if(hmsc.get()!=NULL)
{
- black_node_found(node);
- return false;
+ m_reached_nodes.push_back(NodeRelationPtrList());
+ traverse_successors(hmsc->get_start().get());
+ m_reached_nodes.pop_back();
+
}
- if(c==GRAY)
+ return traverse_successors(ref_node);
+}
+
+void DFSHMscTraverser::cleanup_traversing_attributes()
+{
+ cleanup_top_attributes();
+ while(!m_reached_nodes.empty())
{
- gray_node_found(node);
- return false;
+ m_reached_nodes.pop_back();
}
- white_node_found(node);
- ReferenceNode* refNode = dynamic_cast<ReferenceNode*>(node);
- if(refNode!=NULL)
- {
- HMscPtr hmsc = refNode->get_hmsc();
- if(hmsc.get()!=NULL)
- {
- m_reached_nodes.push_back(InnerNodePList());
- //node's successors are traversed in all cases
- traverse_successors(hmsc->get_start()->get_successors());
- m_reached_nodes.pop_back();
- }
- }
- traverse_successors(node->get_successors());
- node_finished(node);
- //return value is no more needed
- return true;
}
Modified: trunk/src/check/dfs_hmsc_traverser.h
===================================================================
--- trunk/src/check/dfs_hmsc_traverser.h 2008-10-04 22:31:47 UTC (rev 110)
+++ trunk/src/check/dfs_hmsc_traverser.h 2008-10-05 18:03:03 UTC (rev 111)
@@ -23,11 +23,11 @@
/**
- * Traverses all ReferenceNodes in HMsc and referenced HMsc in depth
+ * Traverses all HMscNodes in HMsc and referenced HMsc in depth
* first search manner. I.e. unlike DFSBMscGraphTraverser this traverser doesn't
* care about presence of EndNodes in referenced HMsc in ReferenceNodes.
* Successors of the ReferenceNode are traversed no matter there is EndNode in
- * it's HMsc.
+ * it's HMsc. Moreover each HMsc is traversed only one time.
*
* @warning Non-recursive HMsc is expected.
*/
@@ -36,7 +36,7 @@
protected:
- bool traverse_node(InnerNode* node);
+ bool traverse_node(ReferenceNode* node);
public:
@@ -47,6 +47,8 @@
}
+ void cleanup_traversing_attributes();
+
};
Modified: trunk/src/check/footprint.cpp
===================================================================
--- trunk/src/check/footprint.cpp 2008-10-04 22:31:47 UTC (rev 110)
+++ trunk/src/check/footprint.cpp 2008-10-05 18:03:03 UTC (rev 111)
@@ -1,6 +1,207 @@
-#import "check/footprint.h"
+/*
+ * 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: bmsc_race_checker.cpp 97 2008-06-02 10:40:48Z babicaj $
+ */
+#include "check/footprint.h"
+
bool EDInstancesPtrComparator::operator()(const EDInstancesPtr& a, const EDInstancesPtr& b)
{
return a->operator <(*b.get());
-}
\ No newline at end of file
+}
+
+bool FootprintPtrComparator::operator()(const FootprintPtr& a, const FootprintPtr& b)
+{
+ return a->operator <(*b.get());
+}
+
+EventDependentInstances::EventDependentInstances(Event* event,size_t instances_count)
+{
+ m_event = event;
+ m_instances = BoolVector(instances_count,false);
+}
+
+bool EventDependentInstances::operator<(const EventDependentInstances& di) const
+{
+ return compare(di)<0;
+}
+
+int EventDependentInstances::compare(const EventDependentInstances& di) const
+{
+ if(m_event<di.m_event) return -1;
+ if(di.m_event<m_event) return 1;
+ //compare bool vector as binary number
+ for(int i=0; i<m_instances.size(); i++)
+ {
+ if(m_instances[i]!=di.m_instances[i])
+ return m_instances[i]-di.m_instances[i];
+ }
+ //otherwise this is same as di
+ return 0;
+}
+
+void EventDependentInstances::set_dependent(size_t instance)
+{
+ m_instances[instance] = true;
+}
+
+const BoolVector& EventDependentInstances::get_instances()
+{
+ return m_instances;
+}
+
+Event* EventDependentInstances::get_event()
+{
+ return m_event;
+}
+
+int ExtremeEvents::compare(
+ const EDInstancesPtrSet& first,
+ const EDInstancesPtrSet& second) const
+{
+ EDInstancesPtrSet::const_iterator first_i = first.begin();
+ EDInstancesPtrSet::const_iterator second_i = second.begin();
+ while(first_i!=first.end() && second_i!=second.end())
+ {
+ const EDInstancesPtr first_edis = *first_i;
+ const EDInstancesPtr second_edis = *second_i;
+ int comparision = first_edis->compare(*second_edis.get());
+ if(comparision!=0) return comparision;
+ first_i++;
+ second_i++;
+ }
+ return first.size()-second.size();
+}
+
+ExtremeEvents::ExtremeEvents()
+{
+
+}
+
+ExtremeEvents::ExtremeEvents(size_t instances_count)
+{
+ m_events_instances = EDInstancesPtrSetVector(instances_count);
+}
+
+bool ExtremeEvents::operator<(const ExtremeEvents& other) const
+{
+ const EDInstancesPtrSetVector& other_events = other.get_events_instances();
+ for(size_t i=0;i<m_events_instances.size();i++)
+ {
+ int comparision = compare(m_events_instances[i],other_events[i]);
+ if(comparision!=0)
+ {
+ return comparision<0;
+ }
+ }
+ //otherwise this is supposed to be same as other
+ return false;
+}
+
+void ExtremeEvents::add_extreme_event(size_t instance, EDInstancesPtr& edis)
+{
+ m_events_instances[instance].insert(edis);
+}
+
+const EDInstancesPtrSetVector& ExtremeEvents::get_events_instances() const
+{
+ return m_events_instances;
+}
+
+
+Footprint::Footprint(StartNode* start, size_t instances_count):ExtremeEvents(instances_count)
+{
+ m_path.push_back(start);
+}
+
+Footprint::Footprint(
+ FootprintPtr previous,
+ const InnerNodePList& path,
+ const ExtremeEvents& max_events_less,
+ const ExtremeEvents& max_events_greater)
+ :ExtremeEvents(previous->get_events_instances().size())
+{
+ const EDInstancesPtrSetVector& previous_events = previous->get_events_instances();
+ const EDInstancesPtrSetVector& events_less = max_events_less.get_events_instances();
+ const EDInstancesPtrSetVector& events_greater = max_events_greater.get_events_instances();
+
+ m_previous = previous;
+ m_path.insert(m_path.begin(),path.begin(),path.end());
+ size_t instances_count = previous_events.size();
+
+ for(size_t i=0; i<instances_count; i++)
+ {
+ /*
+ * If events_greater[i] contains any EDInstances these will become part
+ * of new Footprint - doesn't care about previous_events[i]
+ */
+ if(events_greater[i].size()>0)
+ {
+ m_events_instances[i] = events_greater[i];
+ }
+ else if(previous_events[i].size()>0)
+ {
+ /*
+ * Let previous_edi be a EvendDependntInstaces in previous_events[i]. Find
+ * less_edi (EventDependentInstances) from events_less and instance
+ * index j such that (less_edi.m_instances[j]==true and
+ * previous_edi.m_instances[j]==true).
+ *
+ * Let new_edi be copied previous_edi (the new_edi will be inserted into
+ * m_events_instances[i]). If there is any less_edi and index j as
+ * described in previous paragraph then new_edi.m_instances[j]==true.
+ */
+ EDInstancesPtrSet::const_iterator previous_edi;
+ for(previous_edi=previous_events[i].begin();previous_edi!=previous_events[i].end();previous_edi++)
+ {
+ EDInstancesPtr new_edi = new EventDependentInstances(**previous_edi);
+ const BoolVector& previous_edi_instances = (*previous_edi)->get_instances();
+ for(size_t j=0;j<instances_count;j++)
+ {
+ EDInstancesPtrSet::const_iterator less_edi;
+ for(less_edi=events_less[j].begin();less_edi!=events_less[j].end();less_edi++)
+ {
+ const BoolVector& less_edi_instances = (*less_edi)->get_instances();
+ size_t y=0;
+ for(;y<instances_count;y++)
+ {
+ if(previous_edi_instances[y]&&less_edi_instances[y])
+ {
+ break;
+ }
+ }
+ if(y!=instances_count)
+ {
+ break;
+ }
+ }
+ if(less_edi!=events_less[j].end())
+ {
+ new_edi->set_dependent(j);
+ break;
+ }
+ }
+ m_events_instances[i].insert(new_edi);
+ }
+ }
+ }
+}
+
+PredecessorNode* Footprint::get_node()
+{
+ return m_path.back();
+}
+
Modified: trunk/src/check/footprint.h
===================================================================
--- trunk/src/check/footprint.h 2008-10-04 22:31:47 UTC (rev 110)
+++ trunk/src/check/footprint.h 2008-10-05 18:03:03 UTC (rev 111)
@@ -1,3 +1,21 @@
+/*
+ * 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: bmsc_race_checker.cpp 97 2008-06-02 10:40:48Z babicaj $
+ */
+
#ifndef _FOOTPRINT_H
#define _FOOTPRINT_H
@@ -3,4 +21,5 @@
#include <map>
#include <set>
+#include <list>
#include "data/msc.h"
@@ -13,6 +32,8 @@
typedef std::vector<bool> BoolVector;
typedef counted_ptr<EventDependentInstances> EDInstancesPtr;
typedef counted_ptr<Footprint> FootprintPtr;
+typedef std::list<InnerNode*> InnerNodePList;
+typedef std::list<PredecessorNode*> PredecessorNodePList;
class EDInstancesPtrComparator
{
@@ -20,10 +41,17 @@
bool operator()(const EDInstancesPtr& a, const EDInstancesPtr& b);
};
+class FootprintPtrComparator
+{
+public:
+ bool operator()(const FootprintPtr& a, const FootprintPtr& b);
+};
+
typedef std::set<EDInstancesPtr,EDInstancesPtrComparator> EDInstancesPtrSet;
+typedef std::vector<EDInstancesPtrSet> EDInstancesPtrSetVector;
/**
- * Represents dependent Instances -- contain lesser/grater (depends on chosen semantic)
+ * Represents dependent Instances -- contain lesser/greater (depends on chosen semantic)
* Event then the Event with specified m_event in this class.
*/
class EventDependentInstances
@@ -39,8 +67,8 @@
/**
* Each Instance i must have its own number. For this vector m_instances holds:
- * m_instances[i]==true iff i contains any greater/lesser Event than the Event e with
- * id == m_event_id.
+ * m_instances[i]==true iff i contains any greater/lesser Event than the Event
+ * m_event.
*/
BoolVector m_instances;
@@ -49,45 +77,25 @@
/**
*
*/
- EventDependentInstances(Event* event,size_t instances_count)
- {
- m_event = event;
- m_instances = BoolVector(instances_count,false);
- }
+ EventDependentInstances(Event* event,size_t instances_count);
/**
* Used in std::set as comparision method
*
* The di is supposed to have m_instances as large as this one has.
*/
- bool operator<(const EventDependentInstances& di) const
- {
- return compare(di)<0;
- }
+ bool operator<(const EventDependentInstances& di) const;
/**
* Returns -1 for this<di, 0 for this==di and 1 for this>di
*/
- int compare(const EventDependentInstances& di) const
- {
- if(m_event<di.m_event) return -1;
- if(di.m_event<m_event) return 1;
- //compare bool vector as binary number
- for(int i=0; i<m_instances.size(); i++)
- {
- if(m_instances[i]!=di.m_instances[i])
- return m_instances[i]-di.m_instances[i];
- }
- //otherwise this is same as di
- return 0;
- }
+ int compare(const EventDependentInstances& di) const;
- void set_dependent(size_t instance)
- {
- m_instances[instance] = true;
- }
+ void set_dependent(size_t instance);
+ const BoolVector& get_instances();
+ Event* get_event();
};
@@ -100,43 +108,39 @@
* Holds greater/lesser Instances of Events accessible under id of Event's
* Instance.
*/
- EDInstancesPtrSet m_events_instances;
+ EDInstancesPtrSetVector m_events_instances;
+ /**
+ * Compares first and second like they would be a strings.
+ *
+ * Compares element by element, if any less/greater element in first is found
+ * than an element of second at the same position, first is declared to be
+ * less/greater than second.
+ *
+ * Returns x<0 if first < second, 0 if first == second, x>0 if first > second
+ */
+ int compare(
+ const EDInstancesPtrSet& first,
+ const EDInstancesPtrSet& second) const;
+
public:
- ExtremeEvents()
- {
- }
+ ExtremeEvents();
+ ExtremeEvents(size_t instances_count);
+
/**
- * Compares ExtremeEvents by items.
+ * Compares ExtremeEvents item by item.
+ *
+ * Items are supposed to be separate EDInstancesPtrSets which are elements
+ * of m_events_instances. Empty item i (empty EDInstancesPtrSet) is supposed
+ * to be less than anything else which is not empty.
*/
- bool operator<(const ExtremeEvents& extreme) const
- {
- EDInstancesPtrSet::const_iterator my_i = m_events_instances.begin();
- EDInstancesPtrSet::const_iterator extreme_i = extreme.m_events_instances.begin();
- while(my_i!=m_events_instances.end() && extreme_i!=extreme.m_events_instances.end())
- {
- const EDInstancesPtr my_edis = *my_i;
- const EDInstancesPtr extreme_edis = *extreme_i;
- int comparision = my_edis->compare(*extreme_edis.get());
- if(comparision!=0) return comparision<0;
- my_i++;
- extreme_i++;
- }
- //otherwise this is same as extreme
- return false;
- }
+ bool operator<(const ExtremeEvents& other) const;
- void add_extreme_event(EDInstancesPtr& edis)
- {
- m_events_instances.insert(edis);
- }
+ void add_extreme_event(size_t instance, EDInstancesPtr& edis);
- const EDInstancesPtrSet& get_events_instances()
- {
- return m_events_instances;
- }
+ const EDInstancesPtrSetVector& get_events_instances() const;
};
/**
@@ -152,15 +156,14 @@
private:
/**
- * Node in HMsc which built this Footprint.
+ * Path in HMsc which built this Footprint.
*
- * A path with counter example should be returned as structured path (i.e. as
- * HMsc) but keeping HMsc for all possible Footprint during computation would
- * be very memory consuming therefore only one ReferenceNode is used and
- * previous Footprint which this one originates from (see m_previous).
- * Structured path should be computed from these properties.
+ * This path must contain exactly one ReferenceNode - the last one element of
+ * the m_path or must contain only one element - StartNode (initial Footprint).
+ * All remaining members of this m_path are supposed to be
+ * ConnectionNodes.
*/
- ReferenceNode* m_node;
+ PredecessorNodePList m_path;
/**
* Previous Footprint which was this one created from.
@@ -170,30 +173,32 @@
public:
/**
- * Creates new Footprint of two concatenated BMscs.
- *
- * The first one is represented by its footprint, the second one is whole BMsc.
- * @param previous - previous Footprint which is this one creted from
- * @param bmsc_node - ReferenceNode containing BMsc
- * TODO: throw exception if bmsc_node doesn't contain BMsc
- */
- Footprint(FootprintPtr previous, ReferenceNode* bmsc_node)
- {
- m_previous = previous;
- m_node = bmsc_node;
- }
-
- /**
* Creates new initial Footprint
*
* Created Footprint doesn't reference neither ReferenceNode nor Footprint and
* is supposed to be predecessor (not neccessary direct) of the others
* Footprints.
*/
- Footprint()
- {
- }
+ Footprint(StartNode* start, size_t instances_count);
+ /**
+ * Creates new Footprint from previous Footprint and maximal events (denoted
+ * as MaxP in the article) of particular BMsc b.
+ *
+ * The new Footprint is created likewise construction of footprint (with
+ * lowercase f) in the article.
+ *
+ * @param path - members of this list are copied into m_path, see m_path property for details about neccessary properties of this list
+ * @param max_events_less - ExtremeEvents of b whose m_instances attribute is supposed to have lesser semantic.
+ * @param max_events_greater - ExtremeEvents of b whose m_instances attribute is supposed to have greater semantic.
+ */
+ Footprint(
+ FootprintPtr previous,
+ const InnerNodePList& path,
+ const ExtremeEvents& max_events_less,
+ const ExtremeEvents& max_events_greater);
+
+ PredecessorNode* get_node();
};
#endif /* _FOOTPRINT_H */
Modified: trunk/src/check/race_checker.cpp
===================================================================
--- trunk/src/check/race_checker.cpp 2008-10-04 22:31:47 UTC (rev 110)
+++ trunk/src/check/race_checker.cpp 2008-10-05 18:03:03 UTC (rev 111)
@@ -21,6 +21,13 @@
#include "check/race_checker.h"
+ExtremeEvents& MinimalEventsInitiator::get_events(BMsc* b)
+{
+ static ExtremeEvents extreme(m_instance_marker->get_count());
+ m_modified_bmscs.push_back(b);
+ return b->get_attribute<ExtremeEvents>(m_events_attribute,extreme);
+}
+
void MinimalEventsInitiator::on_white_node_found(ReferenceNode* node)
{
BMscPtr b = node->get_bmsc();
@@ -76,7 +83,8 @@
e_instances->set_dependent(
m_instance_marker->get_instance_id((*f)->get_instance()));
}
- extreme_events.add_extreme_event(e_instances);
+ extreme_events.add_extreme_event(
+ m_instance_marker->get_instance_id((*e)->get_instance()),e_instances);
}
}
@@ -89,6 +97,12 @@
}
}
+ExtremeEvents& MaximalEventsInitiator::get_events_less(BMsc* b)
+{
+ static ExtremeEvents extreme(m_instance_marker->get_count());
+ return b->get_attribute<ExtremeEvents>(m_events_less_attribute,extreme);
+}
+
void MaximalEventsInitiator::on_white_node_found(ReferenceNode* node)
{
BMscPtr b = node->get_bmsc();
@@ -123,18 +137,22 @@
delete events;
}
/*
- For any Event e1 from maximal_events find Instances containing any Event e2
- such that e2<<e1.
- */
+ * For any Event e1 from maximal_events find Instances containing any Event e2
+ * such that e2<<e1 and instances containing any Event e3 such that e1<<e3.
+ */
EventPList::const_iterator e;
- ExtremeEvents& extreme_events = get_events(b.get());
+ ExtremeEvents& extreme_events_greater = get_events_greater(b.get());
+ ExtremeEvents& extreme_events_less = get_events_less(b.get());
m_modified_bmscs.push_back(b.get());
EventPList* events = DFSEventsTraverser::topology_order((*e)->get_instance());
for(e=maximal_events.begin();e!=maximal_events.end();e++)
{
- EDInstancesPtr e_instances =
+ EDInstancesPtr e_instances_greater =
new EventDependentInstances(*e,m_instance_marker->get_count());
+ EDInstancesPtr e_instances_less =
+ new EventDependentInstances(*e,m_instance_marker->get_count());
size_t e_index = m_vis_initiator->get_topology_index(*e);
+ const BoolVector& e_closure = m_caus_initiator->get_causal_closure(*e);
EventPList::const_iterator f;
/*
Note that in the article only Events from MinP (used D \in MinP notation in
@@ -143,17 +161,35 @@
*/
for(f=events->begin();f!=events->end();f++)
{
- //if f is less than e then Instance of f must be inserted
- BoolVector& f_closure = m_caus_initiator->get_causal_closure(*f);
+ const BoolVector& f_closure = m_caus_initiator->get_causal_closure(*f);
+ size_t f_index = m_vis_initiator->get_topology_index(*f);
+ size_t f_instance_id = m_instance_marker->get_instance_id((*f)->get_instance());
+ //f is less than e
if(f_closure[e_index])
- e_instances->set_dependent(
- m_instance_marker->get_instance_id((*f)->get_instance()));
+ {
+ e_instances_greater->set_dependent(f_instance_id);
+ }
+ //e is less than f
+ if(e_closure[f_index])
+ {
+ e_instances_less->set_dependent(f_instance_id);
+ }
}
- extreme_events.add_extreme_event(e_instances);
+ extreme_events_greater.add_extreme_event(
+ m_instance_marker->get_instance_id((*e)->get_instance()),e_instances_greater);
}
delete events;
}
+void MaximalEventsInitiator::cleanup_attributes(){
+ while(!m_modified_bmscs.empty())
+ {
+ BMsc* b = m_modified_bmscs.back();
+ b->remove_attribute<ExtremeEvents>(m_events_attribute);
+ m_modified_bmscs.pop_back();
+ }
+}
+
RaceChecker::RaceChecker()
{
m_min_events_initiator = MinimalEventsInitiator(
@@ -283,12 +319,14 @@
//precompute possible things for race checking - e.g. MinP
prepare_hmsc(hmsc,mapper);
//check hmsc to be race free
- check_hmsc(hmsc);
+ return check_hmsc(hmsc,mapper);
}
-HMscPtr RaceChecker::check_hmsc(HMscPtr hmsc)
+HMscPtr RaceChecker::check_hmsc(HMscPtr hmsc,ChannelMapperPtr mapper)
{
-
+ FootprintTraverser t(hmsc.get(),mapper.get(),m_instance_marker.get_count(),
+ &m_min_events_initiator,&m_max_events_initiator);
+ t.traverse();
}
/**
@@ -311,29 +349,105 @@
return counter_example;
}
-HMscPtr RaceChecker::create_counter_example(const InnerNodePListList& path, BMscPtr example){
+HMscPtr RaceChecker::create_counter_example(const InnerNodePListList& path, BMscPtr example)
+{
//TODO: create counter example
-// ReferenceNodePList::const_iterator n;
-// HMscPtr first_hmsc;
-// HMscPtr current_hmsc;
-// ReferenceNode* last_node = NULL;
-// for(n=l.get_path().begin();n!=l.get_path().end();n++)
-// {
-// ReferenceNode* node = *n;
-// if(!current_hmsc.get() || current_hmsc->get_original()!=node->get_owner())
-// {
-// if(last_node)
-// last_node->set_end();
-// current_hmsc = new HMsc(node->get_owner());
-// ReferenceNode* new_node = new ReferenceNode(node);
-// current_hmsc->get_start()->add_successor(new_node);
-// last_node = new_node;
-// if(!first_hmsc.get())
-// first_hmsc = current_hmsc;
-// }else{
-// last_node->add_successor(new ReferenceNode(node));
-// }
-// }
-// last_node->set_msc(example);
-// return first_hmsc;
+ return HMscPtr();
}
+
+HMscPtr create_counter_example(RaceInHMscException* e)
+{
+ //TODO: create counter example
+ delete e;
+ return HMscPtr();
+}
+
+FootprintTraverser::FootprintTraverser(
+ HMsc* hmsc,
+ ChannelMapper* mapper,
+ size_t instances_count,
+ MinimalEventsInitiator* min,
+ MaximalEventsInitiator* max)
+{
+ m_min = min;
+ m_max = max;
+ m_mapper = mapper;
+ FootprintPtr initial = new Footprint(hmsc->get_start().get(),instances_count);
+ todo.insert(initial);
+}
+
+FootprintPtr FootprintTraverser::extract_todo()
+{
+ FootprintPtr first = *todo.begin();
+ todo.erase(todo.begin());
+ return first;
+}
+
+void FootprintTraverser::traverse()
+{
+ while(!todo.empty())
+ {
+ m_footprint = extract_todo();
+ done.insert(m_footprint);
+ traverse(m_footprint->get_node());
+ }
+}
+
+void FootprintTraverser::on_white_node_found(ReferenceNode* node)
+{
+ check_race(node->get_bmsc().get());
+ FootprintPtr f = new Footprint(
+ m_footprint,this->get_reached_nodes().back(),
+ m_max->get_events_less(node->get_bmsc().get()),
+ m_max->get_events_greater(node->get_bmsc().get()));
+ if(todo.find(f)!=todo.end() && done.find(f)!=done.end())
+ {
+ todo.insert(f);
+ }
+}
+
+void FootprintTraverser::check_race(BMsc* bmsc)
+{
+ ExtremeEvents& min_p = m_min->get_events(bmsc);
+ const EDInstancesPtrSetVector& bmsc_edi = min_p.get_events_instances();
+ for(size_t i=0; i<bmsc_edi.size(); i++)
+ {
+ EDInstancesPtrSet::const_iterator b;
+ for(b=bmsc_edi[i].begin();b!=bmsc_edi[i].end();b++)
+ {
+ Event* b_event = (*b)->get_event();
+ if(b_event->is_receive())
+ {
+ const BoolVector& b_instances = (*b)->get_instances();
+ const EDInstancesPtrSetVector& fooprint_edi = m_footprint->get_events_instances();
+ EDInstancesPtrSet::const_iterator a;
+ for(a=fooprint_edi[i].begin();a!=fooprint_edi[i].end();a++)
+ {
+ Event* a_event = (*a)->get_event();
+ if(a_event->is_receive() && !m_mapper->same_channel(a_event,b_event))
+ {
+ throw new RaceInHMscException(m_footprint,b_event,a_event,get_reached_nodes().back());
+ }
+ else if(a_event->is_send())
+ {
+ const BoolVector& a_instances = (*a)->get_instances();
+ size_t j = 0;
+ for(; j<a_instances.size(); j++)
+ {
+ if(a_instances[j] && b_instances[j])
+ {
+ break;
+ }
+ }
+ if(j==a_instances.size())
+ {
+ throw new RaceInHMscException(m_footprint,b_event,a_event,get_reached_nodes().back());
+ }
+ }
+ }
+ }
+ }
+ }
+}
+
+
Modified: trunk/src/check/race_checker.h
===================================================================
--- trunk/src/check/race_checker.h 2008-10-04 22:31:47 UTC (rev 110)
+++ trunk/src/check/race_checker.h 2008-10-05 18:03:03 UTC (rev 111)
@@ -1,8 +1,19 @@
-/*
- * File: hmsc_race_checker.h
- * Author: Jind?ich
+/*
+ * scstudio - Sequence Chart Studio
+ * http://scstudio.sourceforge.net
*
- * Created on 24. ÄŹĹĽËťerven 2008, 13:18
+ * 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: bmsc_race_checker.cpp 97 2008-06-02 10:40:48Z babicaj $
*/
#ifndef _HMSC_RACE_CHECKER_H
@@ -16,9 +27,11 @@
#include "check/dfs_bmsc_graph_traverser.h"
#include "check/utils.h"
#include "check/footprint.h"
+#include "check/refnode_finder.h"
class BMscRaceCheckingListener;
class RaceInBMscException;
+class RaceInHMscException;
typedef std::stack<ReferenceNode*> ReferenceNodePStack;
typedef std::list<BMsc*> BMscPList;
@@ -60,14 +73,9 @@
void on_white_node_found(ReferenceNode* node);
- ExtremeEvents& get_events(BMsc* b)
- {
- static ExtremeEvents extreme;
- m_modified_bmscs.push_back(b);
- return b->get_attribute<ExtremeEvents>(m_events_attribute,extreme);
- }
+ ExtremeEvents& get_events(BMsc* b);
- void cleanup_attributes();
+ virtual void cleanup_attributes();
};
@@ -87,22 +95,74 @@
class MaximalEventsInitiator:public MinimalEventsInitiator
{
+protected:
+
+ std::string m_events_less_attribute;
+
public:
MaximalEventsInitiator(
VisualClosureInitiator* vis_initiator=NULL,
CausalClosureInitiator* caus_initiator=NULL,
InstanceIdMarker* instance_marker=NULL,
- const std::string& events_attribute = "maximal_events"):
+ const std::string& events_greater_attribute = "maximal_events_greater",
+ const std::string& events_less_attribute = "maximal_events_less"):
MinimalEventsInitiator(
- vis_initiator,caus_initiator,instance_marker,events_attribute)
+ vis_initiator,caus_initiator,instance_marker,events_greater_attribute)
{
+ m_events_less_attribute = events_less_attribute;
}
+ ExtremeEvents& get_events_greater(BMsc* b)
+ {
+ return get_events(b);
+ }
+
+ ExtremeEvents& get_events_less(BMsc* b);
+
void on_white_node_found(ReferenceNode* node);
+ void cleanup_attributes();
+
};
+class FootprintTraverser:public WhiteRefNodeFoundListener,public ReferenceNodeFinder
+{
+private:
+
+ std::set<FootprintPtr> todo;
+ std::set<FootprintPtr> done;
+
+ ChannelMapper* m_mapper;
+ MinimalEventsInitiator* m_min;
+ MaximalEventsInitiator* m_max;
+
+ FootprintPtr m_footprint;
+
+ FootprintPtr extract_todo();
+
+ /**
+ * To understand this method see Algorithm 1 in the article
+ */
+ void check_race(BMsc* b);
+
+public:
+
+ FootprintTraverser(
+ HMsc* hmsc,
+ ChannelMapper* mapper,
+ size_t instances_count,
+ MinimalEventsInitiator* min,
+ MaximalEventsInitiator* max);
+
+ void on_white_node_found(ReferenceNode* node);
+
+ void traverse();
+
+ void traverse(PredecessorNode* node);
+
+};
+
class RaceChecker:public HMscChecker
{
@@ -129,6 +189,11 @@
BMsc* create_counter_example(Event* e1, Event* e2);
/**
+ *
+ */
+ HMscPtr create_counter_example(RaceInHMscException* e);
+
+ /**
* Precomputes neccessary things for race checking
*/
void prepare_hmsc(HMscPtr hmsc,ChannelMapperPtr mapper);
@@ -143,7 +208,7 @@
*/
HMscPtr create_counter_example(const InnerNodePListList& path, BMscPtr example);
- HMscPtr check_hmsc(HMscPtr hmsc);
+ HMscPtr check_hmsc(HMscPtr hmsc, ChannelMapperPtr mapper);
public:
@@ -292,7 +357,27 @@
};
+class RaceInHMscException:public std::exception
+{
+private:
+
+ FootprintPtr m_footprint;
+ Event* m_first;
+ Event* m_second;
+ InnerNodePList m_path_to_second;
+
+public:
+
+ RaceInHMscException(FootprintPtr footprint,Event* first, Event* second,
+ const InnerNodePList& path_to_second);
+
+ ~RaceInHMscException() throw ()
+ {
+
+ }
+};
+
#endif /* _HMSC_RACE_CHECKER_H */
Added: trunk/src/check/refnode_finder.cpp
===================================================================
--- trunk/src/check/refnode_finder.cpp (rev 0)
+++ trunk/src/check/refnode_finder.cpp 2008-10-05 18:03:03 UTC (rev 111)
@@ -0,0 +1,52 @@
+/*
+ * 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$
+ */
+
+#include "check/refnode_finder.h"
+
+bool ReferenceNodeFinder::traverse_node(HMscNode* node)
+{
+ if(is_processed(node))
+ {
+ //return value is no more needed
+ return true;
+ }
+ white_node_found(node);
+ //traverse successors only if node is not ReferenceNode
+ if(!dynamic_cast<ReferenceNode*>(node))
+ {
+ if(dynamic_cast<ConnectionNode*>(node)||
+ dynamic_cast<StartNode*>(node))
+ {
+ traverse_successors((PredecessorNode*)node);
+ }
+ //else node is supposed to be EndNode
+ }
+ node_finished(node);
+ //return value is no more needed
+ return true;
+}
+
+void ReferenceNodeFinder::traverse(HMscNode* node)
+{
+ PredecessorNode* pred = dynamic_cast<PredecessorNode*>(node);
+ if(pred){
+ push_top_attributes();
+ traverse_successors(pred);
+ cleanup_traversing_attributes();
+ }
+}
Property changes on: trunk/src/check/refnode_finder.cpp
___________________________________________________________________
Added: svn:keywords
+ Id
Added: svn:eol-style
+ native
Added: trunk/src/check/refnode_finder.h
===================================================================
--- trunk/src/check/refnode_finder.h (rev 0)
+++ trunk/src/check/refnode_finder.h 2008-10-05 18:03:03 UTC (rev 111)
@@ -0,0 +1,53 @@
+/*
+ * 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$
+ */
+
+#ifndef _REFNODE_FINDER_H
+#define _REFNODE_FINDER_H
+
+#include "check/dfs_bmsc_graph_traverser.h"
+
+/**
+ * \brief See method traverse(HMscNode* node) for purpose.
+ */
+class ReferenceNodeFinder: public DFSBMscGraphTraverser
+{
+
+public:
+
+ ReferenceNodeFinder(const std::string& color_attribute = "rnf_color")
+ :DFSBMscGraphTraverser(color_attribute)
+ {
+
+ }
+
+ /**
+ * \brief Traverses HMsc of the node until ReferenceNodes are found.
+ *
+ * This traverser continues in traversing until first ReferenceNode successors
+ * of the node are found.
+ */
+ void traverse(HMscNode* node);
+
+protected:
+
+ bool traverse_node(HMscNode* node);
+
+};
+
+#endif /* _REFNODE_FINDER_H */
+
Property changes on: trunk/src/check/refnode_finder.h
___________________________________________________________________
Added: svn:keywords
+ Id
Added: svn:eol-style
+ native
Modified: trunk/src/data/counted_ptr.h
===================================================================
--- trunk/src/data/counted_ptr.h 2008-10-04 22:31:47 UTC (rev 110)
+++ trunk/src/data/counted_ptr.h 2008-10-05 18:03:03 UTC (rev 111)
@@ -224,6 +224,12 @@
return count;
}
+
+ template<class rtype>
+ bool operator<(const counted_ptr<rtype>& right) const
+ {
+ return (m_pointer < right.m_pointer);
+ }
private:
template<class rtype>
Modified: trunk/src/data/msc.cpp
===================================================================
--- trunk/src/data/msc.cpp 2008-10-04 22:31:47 UTC (rev 110)
+++ trunk/src/data/msc.cpp 2008-10-05 18:03:03 UTC (rev 111)
@@ -21,17 +21,41 @@
#include "data/msc.h"
-Msc::~Msc()
+void SuccessorNode::add_predecessor(NodeRelationPtr& n)
{
-
+ n->set_successor(this);
+ m_predecessors.insert(n);
+ n->get_predecessor()->m_successors.insert(n);
}
-void StartNode::add_successor(InnerNode* n)
+void SuccessorNode::remove_predecessor(NodeRelationPtr& n)
{
+ m_predecessors.erase(n);
+ n->get_predecessor()->m_successors.erase(n);
+}
+
+void PredecessorNode::add_successor(NodeRelationPtr& n)
+{
+ n->set_predecessor(this);
m_successors.insert(n);
- n->set_owner(m_owner);
+ n->get_successor()->m_predecessors.insert(n);
}
+void PredecessorNode::remove_successor(NodeRelationPtr& n)
+{
+ m_successors.erase(n);
+ n->get_successor()->m_predecessors.erase(n);
+}
+
+HMscNodePtr HMscNode::my_ptr()
+{
+ if(m_owner==NULL){
+ HMscNodePtr a;
+ return a;
+ }
+ return m_owner->find_ptr(this);
+}
+
inline Instance* Event::get_instance()
{
return m_area->get_instance();
@@ -105,31 +129,3 @@
{
return dynamic_cast<CoregionArea*>(m_area);
}
-
-HMsc::~HMsc()
-{
- InnerNodePSet::const_iterator n;
- InnerNodePQueue to_delete;
- for(n=m_start->get_successors().begin();n!=m_start->get_successors().end();n++)
- {
- to_delete.push(*n);
- }
- while(!to_delete.empty())
- {
- InnerNode* node = to_delete.front();
- to_delete.pop();
- InnerNodePSet::iterator i;
- for(i=node->m_predecessors.begin();i!=node->m_predecessors.end();i++)
- {
- (*i)->m_successors.erase(node);
-
- }
- InnerNodePSet::iterator m;
- for(m=node->m_successors.begin();m!=node->m_successors.end();m++)
- {
- (*m)->m_predecessors.erase(node);
- to_delete.push(*m);
- }
- delete node;
- }
-}
Modified: trunk/src/data/msc.h
===================================================================
--- trunk/src/data/msc.h 2008-10-04 22:31:47 UTC (rev 110)
+++ trunk/src/data/msc.h 2008-10-05 18:03:03 UTC (rev 111)
@@ -27,6 +27,7 @@
#include <queue>
#include "data/counted_ptr.h"
+#include "data/msc_visual.h"
class MscElement;
class HMscNode;
@@ -45,6 +46,8 @@
class EventArea;
class StrictOrderArea;
class CoregionArea;
+class SuccessorNode;
+class PredecessorNode;
typedef counted_ptr<MscElement> MscElementPtr;
@@ -54,8 +57,12 @@
typedef counted_ptr<HMsc> HMscPtr;
+typedef counted_ptr<HMscNode> HMscNodePtr;
+typedef std::set<HMscNodePtr> HMscNodePtrSet;
+
typedef counted_ptr<ReferenceNode> ReferenceNodePtr;
typedef std::list<ReferenceNodePtr> ReferenceNodePtrList;
+
typedef std::set<InnerNode*> InnerNodePSet;
typedef std::set<ReferenceNode*> ReferenceNodePSet;
typedef std::queue<InnerNode*> InnerNodePQueue;
@@ -91,7 +98,9 @@
typedef void* AttributeP;
typedef std::map<std::string,AttributeP> AttributePMap;
+typedef std::set<HMscNodePtr> HMscNodePtrSet;
+
/**
* \brief Common basic abstract class for all elements of MSC
*/
@@ -107,25 +116,24 @@
* is left up to piece of code using these attributes
*/
AttributePMap m_attributes;
+
+ /**
+ * \brief Determines whether this element is in some way interesting for creator
+ */
+ bool m_marked;
protected:
/**
- * Abstract class shouldn't be able to be instantiated.
- */
- MscElement()
- {
- }
-
- /**
* \brief Creates MscElement referencing the original one.
*
* Used to create counter example with reference to original element which
* should be accessible from the new one.
*/
- MscElement(MscElement* original)
+ MscElement(MscElement* original=NULL, bool marked=false)
{
m_original = original;
+ m_marked = marked;
}
virtual ~MscElement()
@@ -282,6 +290,16 @@
{
m_original = e;
}
+
+ bool get_marked()
+ {
+ return m_marked;
+ }
+
+ void set_marked(bool marked)
+ {
+ m_marked = marked;
+ }
};
/**
@@ -293,14 +311,15 @@
protected:
/**
- * Label of MSC.
+ * \brief Label of MSC.
*/
std::string m_label;
-
- Msc()
+
+ Msc(Msc* original=NULL):MscElement(original)
{
+
}
-
+
/**
* Initializes m_label.
*/
@@ -352,9 +371,8 @@
/**
* Creates BMsc referencing original version of BMsc.
*/
- BMsc(BMsc* original)
+ BMsc(BMsc* original=NULL):Msc(original)
{
- m_original = original;
}
virtual ~BMsc()
@@ -382,9 +400,12 @@
/**
* \brief Base abstract class for node of HMsc
*/
-class HMscNode:public MscElement{
+class HMscNode:public MscElement
+{
std::string m_label;
+
+ Point m_position;
protected:
@@ -393,16 +414,9 @@
/**
* This is an abstract class
*/
- HMscNode(){}
-
- HMscNode(HMscNode* original):MscElement(original)
+ HMscNode(HMscNode* original=NULL):MscElement(original)
{}
- virtual ~HMscNode()
- {
-
- }
-
public:
/**
@@ -430,95 +444,194 @@
{
m_owner = owner;
}
+
+ Point& get_position()
+ {
+ return m_position;
+ }
+
+ HMscNodePtr my_ptr();
+
+ virtual ~HMscNode();
};
-/**
- * \brief End node of HMsc.
- *
- * Represents end node as specified in Z.120
- */
-class EndNode:public HMscNode
+class NodeRelation:MscElement
{
-
+protected:
+
+ PolyLine m_line;
+
+ SuccessorNode* m_successor;
+
+ PredecessorNode* m_predecessor;
+
public:
- EndNode()
- {}
-
- EndNode(EndNode* original):HMscNode(original)
- {}
-
- virtual ~EndNode()
+
+ NodeRelation(SuccessorNode* successor, PredecessorNode* predecessor,
+ const PolyLine& line)
{
-
+ m_successor = successor;
+ m_predecessor = predecessor;
+ m_line = line;
}
-
+
+ SuccessorNode* get_successor()
+ {
+ return m_successor;
+ }
+
+ PredecessorNode* get_predecessor()
+ {
+ return m_predecessor;
+ }
+
+ void set_successor(SuccessorNode* n)
+ {
+ m_successor = n;
+ }
+
+ void set_predecessor(PredecessorNode* n)
+ {
+ m_predecessor = n;
+ }
+
};
-/**
- * \brief Start node of HMsc.
- *
- * According to ITU-T standard, each HMsc has got exactly
- * one start node.
- */
-class StartNode:public HMscNode
+typedef counted_ptr<NodeRelation> NodeRelationPtr;
+typedef std::set<NodeRelationPtr> NodeRelationPtrSet;
+
+class SuccessorNode
{
-private:
+protected:
+
/**
- * Succesors of StartNode.
+ * Succesors of PredecessorNode.
*/
- InnerNodePSet m_successors;
+ NodeRelationPtrSet m_predecessors;
+ public:
+
+ SuccessorNode()
+ {
+ }
+
+ virtual ~SuccessorNode()
+ {
+ }
+
/**
- * EndNode which this StartNode is connected to,
- * undefined if there isn't any such connection.
+ * Getter for m_predecessors.
*/
- EndNodePtr m_end;
+ const NodeRelationPtrSet& get_predecessors()
+ {
+ return m_predecessors;
+ }
-public:
+ void add_predecessor(NodeRelationPtr& n);
- StartNode()
+ void remove_predecessor(NodeRelationPtr& n);
+
+ /**
+ * Returns true iff node has any successors
+ */
+ bool has_predecessors()
{
+ return m_predecessors.size()!=0;
}
- StartNode(StartNode* original):HMscNode(original)
- {}
+ friend class PredecessorNode;
+};
- virtual ~StartNode()
+class PredecessorNode
+{
+protected:
+
+ /**
+ * Succesors of PredecessorNode.
+ */
+ NodeRelationPtrSet m_successors;
+
+public:
+
+ PredecessorNode()
{
-
}
-
+
+ virtual ~PredecessorNode()
+ {
+ }
+
/**
* Getter for m_successors.
*/
- const InnerNodePSet& get_successors()
- {
+ const NodeRelationPtrSet& get_successors()
+ {
return m_successors;
}
/**
* Adds successor.
*/
- void add_successor(InnerNode* n);
+ void add_successor(NodeRelationPtr& n);
/**
* Removes successor.
*/
- void remove_successor(InnerNode* n)
+ void remove_successor(NodeRelationPtr& n);
+
+ /**
+ * Returns true iff node has any successors
+ */
+ bool has_successors()
{
- m_successors.erase(n);
+ return m_successors.size()!=0;
}
- EndNodePtr get_end()
+ friend class SuccessorNode;
+
+};
+
+/**
+ * \brief End node of HMsc.
+ *
+ * Represents end node as specified in Z.120
+ */
+class EndNode:public SuccessorNode, public HMscNode
+{
+
+public:
+ EndNode()
+ {}
+
+ EndNode(EndNode* original=NULL):HMscNode(original),SuccessorNode()
+ {}
+
+ virtual ~EndNode()
{
- return m_end;
+
}
- void set_end(EndNodePtr end)
+};
+
+/**
+ * \brief Start node of HMsc.
+ *
+ * According to ITU-T standard, each HMsc has got exactly
+ * one start node.
+ */
+class StartNode:public PredecessorNode, public HMscNode
+{
+public:
+
+ StartNode(StartNode* original=NULL):HMscNode(original),PredecessorNode()
{
- m_end = end;
}
+
+ virtual ~StartNode()
+ {
+
+ }
};
/**
@@ -533,18 +646,19 @@
* Mandatory element in HMsc, should be initialized in constructor.
*/
StartNodePtr m_start;
+
+ /**
+ * Set of all HMscNodes included in this HMsc
+ */
+ HMscNodePtrSet m_nodes;
public:
/**
* Initializes mandatory m_start
*/
-
- HMsc(HMsc* original)
+ HMsc(HMsc* original):Msc(original)
{
- // Setting original HMsc, copying label of HMsc from original
- m_original = original;
- m_label = original->get_label();
// Creating start for new HMsc, setting its original and owner
m_start = new StartNode(original->get_start().get());
m_start->set_owner(this);
@@ -566,134 +680,37 @@
/**
* Getter for m_start.
*/
- StartNodePtr get_start()
- {
- return m_start;
+ StartNodePtr get_start()
+ {
+ return m_start;
}
-
-};
-
-/**
- * \brief Abstract class representing inner node in HMsc.
- */
-class InnerNode:public HMscNode
-{
-protected:
-
- /**
- * Succesors of InnerNode.
- *
- * @warning counted_ptrs mustn't be used because of possible cyclic dependency
- */
- InnerNodePSet m_successors;
-
- /**
- * Predecessors of this InnerNode.
- *
- * @warning counted_ptrs mustn't be used because of possible cyclic dependency
- */
- InnerNodePSet m_predecessors;
-
- /**
- * EndNode which this ReferenceNode is connected to,
- * undefined if there isn't any such connection.
- */
- EndNodePtr ...
[truncated message content] |
