Menu
▾
▴
[Scstudio-commits] SF.net SVN: scstudio:[450] trunk
|
From: <koc...@us...> - 2009-11-04 15:11:17
|
Revision: 450
http://scstudio.svn.sourceforge.net/scstudio/?rev=450&view=rev
Author: kocianon
Date: 2009-11-04 15:11:10 +0000 (Wed, 04 Nov 2009)
Log Message:
-----------
bmsc hmsc constraints checker
Modified Paths:
--------------
trunk/src/check/liveness/deadlock_checker.h
trunk/src/check/pseudocode/utils.h
trunk/src/check/time/constrain_check.cpp
trunk/src/check/time/constrain_check.h
trunk/src/check/time/module.cpp
trunk/src/check/time/tightening.cpp
trunk/src/check/time/tightening.h
trunk/src/check/time/time_pseudocode.cpp
trunk/src/check/time/time_pseudocode.h
trunk/src/data/dfs_refnode_hmsc_traverser.cpp
trunk/src/data/dfsb_hmsc_traverser.cpp
trunk/src/data/msc.cpp
trunk/src/data/msc.h
trunk/tests/CMakeLists.txt
trunk/tests/constrain_check_test.cpp
Modified: trunk/src/check/liveness/deadlock_checker.h
===================================================================
--- trunk/src/check/liveness/deadlock_checker.h 2009-11-03 00:56:27 UTC (rev 449)
+++ trunk/src/check/liveness/deadlock_checker.h 2009-11-04 15:11:10 UTC (rev 450)
@@ -119,7 +119,7 @@
static DeadlockCheckerPtr m_instance;
HMscPtr create_counter_example(const MscElementPListList& path);
-
+
public:
DeadlockChecker(){};
Modified: trunk/src/check/pseudocode/utils.h
===================================================================
--- trunk/src/check/pseudocode/utils.h 2009-11-03 00:56:27 UTC (rev 449)
+++ trunk/src/check/pseudocode/utils.h 2009-11-04 15:11:10 UTC (rev 450)
@@ -27,15 +27,17 @@
#include "data/dfsb_hmsc_traverser.h"
#include "check/pseudocode/export.h"
#include "data/node_finder.h"
+#include "check/pseudocode/visual_closure_initiator.h"
typedef std::map<std::wstring,size_t> StringSizeTMap;
+typedef Event* EventP;
typedef std::set<Event*> EventPSet;
+
/**
* \brief Returns event's next first successors
- * if event is a send one, returns also its match event
+ * if event is a send one, returns also its match event
*/
-
class SCPSEUDOCODE_EXPORT EventFirstSuccessors
{
private:
@@ -59,40 +61,40 @@
class SCPSEUDOCODE_EXPORT InstanceIdMarker:public WhiteRefNodeFoundListener
{
private:
-
+
std::string m_instance_id_attribute;
-
+
StringSizeTMap m_identifiers;
-
+
std::list<Instance*> m_modified_instances;
-
+
void set_instance_id(Instance* i);
-
+
public:
-
+
InstanceIdMarker(const std::string& instance_id_attribute="instance_id");
-
+
virtual void on_white_node_found(ReferenceNode* node);
-
+
size_t get_instance_id(Instance* i);
-
+
void cleanup_attributes();
-
+
size_t get_count();
-
+
};
class TopologyOrderListener:public EventFinishedListener
{
EventPList* m_topology;
-
+
public:
-
+
TopologyOrderListener(EventPList* topology)
{
m_topology = topology;
}
-
+
void on_event_finished(Event* e)
{
m_topology->push_front(e);
@@ -102,13 +104,47 @@
class EventRecognizer
{
public:
-
+
static bool is_matched_receive(Event* e)
{
return e->is_matched() && e->is_receive();
}
};
+/**
+ * \brief Handles visual closure on bmsc
+ * Init DFSEventsTraverser, TopologicalOrderListener
+ * and VisualClosureInitiator. Makes easier to run is_leq method
+ * on two events.
+ */
+class EventTopologyHandler
+{
+private:
+ BMscPtr m_bmsc;
+ VisualClosureInitiator m_closure_initiator;
+ TopologicalOrderListener m_topology_listener;
+ DFSEventsTraverser m_traverser;
+public:
+ EventTopologyHandler(BMscPtr bmsc):m_bmsc(bmsc)
+ {
+ m_traverser.add_event_finished_listener(&m_topology_listener);
+ m_traverser.traverse(m_bmsc);
+ EventPVector topology(m_topology_listener.get_topology().size());
+ topology.assign(m_topology_listener.get_topology().begin(),m_topology_listener.get_topology().end());
+ m_closure_initiator.initialize(topology);
+ }
+
+ /**
+ * \return true if a is less then b (a<b) or equal (a=b)
+ */
+ bool is_leq(Event* a,Event *b)
+ {
+ BoolVector vector = m_closure_initiator.get_visual_closure(a);
+
+ return m_closure_initiator.get_visual_closure(a)[m_closure_initiator.get_topology_index(b)];
+ }
+};
+
template<class MscElementContainer,class AttributeType>
void remove_attributes(MscElementContainer& container, const std::string& name)
{
@@ -121,13 +157,13 @@
}
/**
- * /brief Eliminates from hmsc nodes which are not reachable from
+ * \brief Eliminates from hmsc nodes which are not reachable from
* end nodes of hmsc.
*/
void eliminate_noending_nodes(HMscPtr& hmsc);
/**
- * /brief Marks white nodes by boolean true
+ * \brief Marks white nodes by boolean true
*/
class SCPSEUDOCODE_EXPORT WhiteNodeMarker: public WhiteNodeFoundListener
{
@@ -151,7 +187,7 @@
};
/**
- * /brief Eliminates nodes which are not reachable from end node.
+ * \brief Eliminates nodes which are not reachable from end node.
*
* Currently supports only BMsc graph, please extend implementation if
* neccessary.
@@ -172,17 +208,16 @@
};
-/*
- * \brief Check whether the HMscNode is ending node
+/**
+ * \brief Check whether the HMscNode is ending node
* (one of the straight successors is End node)
* due to connection node theather
*
*/
-
class IsEndingNode
{
private:
-
+
public:
IsEndingNode()
{
@@ -193,7 +228,7 @@
//isnt it EndNode itself?
if((end=dynamic_cast<EndNode*>(node)))
return end;
-
+
HMscNodePListPtr succs = NodeFinder::successors(node,"IsEndingNode");
HMscNodePList::iterator it;
for(it=succs->begin();it!=succs->end();it++)
@@ -204,6 +239,108 @@
}
};
+/**
+ * \brief Vector of all reachable events in bmsc
+ * Using DFSEventsTraverser goes through the BMsc and
+ * pick up all events
+ * (WhiteNodeFoundListener)
+ */
+class AllReachableEventPVector:public std::vector<EventP>, public WhiteEventFoundListener
+{
+private:
+ DFSEventsTraverser m_traverser;
+public:
+ AllReachableEventPVector(BMscPtr bmsc)
+ {
+ m_traverser.add_white_event_found_listener(this);
+ m_traverser.traverse(bmsc);
+ m_traverser.cleanup_traversing_attributes();
+ m_traverser.remove_white_event_found_listeners();
+ }
+
+ AllReachableEventPVector()
+ {}
+
+ void set_new_bmsc(BMscPtr bmsc)
+ {
+ clear();
+ m_traverser.add_white_event_found_listener(this);
+ m_traverser.traverse(bmsc);
+ m_traverser.cleanup_traversing_attributes();
+ m_traverser.remove_white_event_found_listeners();
+ }
+
+ void on_white_event_found(Event* e)
+ {
+ this->push_back(e);
+ }
+};
+
+/**
+ * \brief List of minimal events
+ * Go through the vector of all events using AllReachableEventPVector
+ * and using EventTopologyHandler choose minimal events
+ */
+class MinimalEventPList: public std::list<EventP>
+{
+private:
+ AllReachableEventPVector m_events;
+ EventTopologyHandler m_event_top;
+
+public:
+ MinimalEventPList(BMscPtr bmsc):m_events(bmsc),m_event_top(bmsc)
+ {
+ EventPVector::iterator it;
+ EventPVector::iterator it_b;
+ for (it=m_events.begin();it!=m_events.end();it++)
+ {
+ bool is_minimal = true;
+ for (it_b=m_events.begin();it_b!=m_events.end();it_b++)
+ {
+ if (it_b != it && m_event_top.is_leq(*it_b,*it))
+ {
+ is_minimal=false;
+ break;
+ }
+ }
+ if (is_minimal)
+ push_back(*it);
+ }
+ }
+};
+
+/**
+ * \brief list of maximal events
+ * Go through the vector of all events using AllReachableEventPVector
+ * and using EventTopologyHandler choose maximal events
+ */
+class MaximalEventPList: public std::list<EventP>
+{
+private:
+ AllReachableEventPVector m_events;
+ EventTopologyHandler m_event_top;
+
+public:
+ MaximalEventPList(BMscPtr bmsc):m_events(bmsc),m_event_top(bmsc)
+ {
+ EventPVector::iterator it;
+ EventPVector::iterator it_b;
+ for (it=m_events.begin();it!=m_events.end();it++)
+ {
+ bool is_maximal = true;
+ for (it_b=m_events.begin();it_b!=m_events.end();it_b++)
+ {
+ if (it_b != it && m_event_top.is_leq(*it,*it_b))
+ {
+ is_maximal=false;
+ break;
+ }
+ }
+ if (is_maximal)
+ push_back(*it);
+ }
+ }
+};
#endif /* _UTILS_H */
// $Id$
Modified: trunk/src/check/time/constrain_check.cpp
===================================================================
--- trunk/src/check/time/constrain_check.cpp 2009-11-03 00:56:27 UTC (rev 449)
+++ trunk/src/check/time/constrain_check.cpp 2009-11-04 15:11:10 UTC (rev 450)
@@ -1,14 +1,20 @@
#include "constrain_check.h"
-#include "data/dfs_bmsc_graph_traverser.h"
+#include "data/dfs_refnode_hmsc_traverser.h"
#include "check/pseudocode/utils.h"
HMscTimeConstrainCheckerPtr HMscTimeConstrainChecker::m_instance;
HMscTimeConstrainChecker::HMscTimeConstrainChecker(
- const std::string& name):
- m_local_active_constraints(name)
+ const std::string& local
+ ,const std::string& first_find
+ ):
+ m_local_active_constraints(local),m_first_find_with(first_find)
{}
+/** updating global set of active constraints (m_active_constraints)
+ * constraints with the equal begin and end reference node are ignored
+ * @Warning WHITENODE function
+ */
void HMscTimeConstrainChecker::check_active_set(
ReferenceNode* n,
@@ -21,63 +27,64 @@
{
TimeRelationRefNodePtr constraint = *it;
+ // ignore constraints with the equal begin and end reference node
+ if(constraint->get_ref_node_a()==constraint->get_ref_node_b())
+ continue;
TimeRelationRefNodePtrSet::iterator found_constraint;
found_constraint=m_active_constraints.find(constraint);
if(found_constraint==m_active_constraints.end())
{
- if(constraint->get_ref_node_b()==n && constraint->get_ref_node_a()!=n)
- {
- throw constraint.get();
- }
-
+ set_first_find_with(constraint.get(),n);
m_active_constraints.insert(constraint);
}
else
{
- if(constraint->get_ref_node_b()==n)
- m_active_constraints.erase(found_constraint);
+// if(get_first_find_with(constraint.get()).get()==n)
+// {
+// if(constraint->get_ref_node_a()==constraint->get_ref_node_b())
+// continue; //time relation on one refnode
+// else
+// throw constraint.get(); // begin of refnode was refound?
+// // end of timerelation was found, remove it from the global set
+// }
+// else
+ m_active_constraints.erase(found_constraint);
}
}
-
}
-void HMscTimeConstrainChecker::on_white_node_found(HMscNode* n)
+void HMscTimeConstrainChecker::on_white_node_found(ReferenceNode* n)
{
-
+
add_local_active_constraints(n);
//TOP
- if(ReferenceNode* ref=dynamic_cast<ReferenceNode*>(n))
- {
TimeRelationRefNodePtrSet constraint_set;
- constraint_set = ref->get_time_relations_top();
+ constraint_set = n->get_time_relations_top();
+ check_active_set(n,constraint_set);
- check_active_set(ref,constraint_set);
-
//BOTTOM
- constraint_set = ref->get_time_relations_bottom();
+ constraint_set = n->get_time_relations_bottom();
// add_active_constraints_bottom(n);
- check_active_set(ref,constraint_set);
- }
+ check_active_set(n,constraint_set);
if(m_active_constraints.size()!=0 && IsEndingNode::check(n))
throw m_active_constraints;
}
-void HMscTimeConstrainChecker::on_gray_node_found(HMscNode* n)
+void HMscTimeConstrainChecker::on_gray_node_found(ReferenceNode* n)
{
TimeRelationRefNodePtrSet constraints_set;
constraints_set = get_local_active_constraints(n);
if(constraints_set!=m_active_constraints)
throw constraints_set;
-
}
-void HMscTimeConstrainChecker::on_black_node_found(HMscNode* n)
+void HMscTimeConstrainChecker::on_black_node_found(ReferenceNode* n)
{
TimeRelationRefNodePtrSet constraints_set;
@@ -87,16 +94,16 @@
}
-void HMscTimeConstrainChecker::on_node_finished(HMscNode* n)
+void HMscTimeConstrainChecker::on_node_finished(ReferenceNode* n)
{
- TimeRelationRefNodePtrSet constraints_set;
+ // fix global set
m_active_constraints = get_local_active_constraints(n);
}
HMscPtr HMscTimeConstrainChecker::check(HMscPtr hmsc, ChannelMapperPtr chm)
{
HMscPtr p;
- DFSBMscGraphTraverser traverser;
+ DFSRefNodeHMscTraverser traverser;
traverser.add_white_node_found_listener(this);
traverser.add_gray_node_found_listener(this);
traverser.add_black_node_found_listener(this);
@@ -107,13 +114,13 @@
}
catch (TimeRelationRefNode* relation)
{
- p = process_path(traverser.get_reached_elements());
+ //p = process_path(traverser.get_reached_elements());
//mark_time_relation(relation);
traverser.cleanup_traversing_attributes();
}
catch (TimeRelationRefNodePtrSet relations)
{
- p = process_path(traverser.get_reached_elements());
+ //p = process_path(traverser.get_reached_elements());
//mark_time_relations(relations);
traverser.cleanup_traversing_attributes();
}
@@ -121,10 +128,10 @@
return p;
}
-Checker::PreconditionList HMscTimeConstrainChecker::get_preconditions(MscPtr msc) const
-{
- Checker::PreconditionList result;
- // no preconditions
+Checker::PreconditionList HMscTimeConstrainChecker::get_preconditions(MscPtr msc) const
+{
+ Checker::PreconditionList result;
+ // no preconditions
return result;
}
Modified: trunk/src/check/time/constrain_check.h
===================================================================
--- trunk/src/check/time/constrain_check.h 2009-11-03 00:56:27 UTC (rev 449)
+++ trunk/src/check/time/constrain_check.h 2009-11-04 15:11:10 UTC (rev 450)
@@ -13,7 +13,7 @@
*
*
*
- *
+ *
*/
#include <string>
@@ -25,16 +25,19 @@
#include "data/checker.h"
#include "data/msc.h"
#include "check/pseudocode/msc_duplicators.h"
-#include "data/dfs_bmsc_graph_traverser.h"
+#include "data/dfs_refnode_hmsc_traverser.h"
+#include "check/pseudocode/utils.h"
+#include "check/time/time_pseudocode.h"
class HMscTimeConstrainChecker;
+class BMscTimeConstrainChecker;
typedef boost::shared_ptr<HMscTimeConstrainChecker> HMscTimeConstrainCheckerPtr;
/*
class ConstrainException:public std::exception
{
-
+
public:
virtual const char* what() const throw()
{
@@ -46,28 +49,29 @@
class SCTIME_EXPORT HMscTimeConstrainChecker:
public Checker
, public HMscChecker
- , public WhiteNodeFoundListener
- , public GrayNodeFoundListener
- , public BlackNodeFoundListener
- , public NodeFinishedListener
+ , public WhiteRefNodeFoundListener
+ , public GrayRefNodeFoundListener
+ , public BlackRefNodeFoundListener
+ , public RefNodeFinishedListener
{
private:
- std::string m_local_active_constraints;
- std::stack<MscElement*> to_be_clean;
- // active constraints on the path
- std::set<TimeRelationRefNodePtr> m_active_constraints;
+ std::string m_local_active_constraints; ///< attr of local set of constraints
+ std::string m_first_find_with; /// attr of TimeRelation, RefNode first find with
+ std::stack<MscElement*> to_be_clean; ///< stack of items with atribute
+ std::set<TimeRelationRefNodePtr> m_active_constraints; ///< global set of active constrains
HMscPathDuplicator m_duplicator;
-//////////// attribute handler
- // ADD
- void add_local_active_constraints(HMscNode* n)
+
+/////// BEGIN attribute handler
+ /// add global set of open time constraints to the ReferenceNode
+ void add_local_active_constraints(ReferenceNode* n)
{
n->set_attribute<TimeRelationRefNodePtrSet>(m_local_active_constraints,m_active_constraints);
to_be_clean.push(n);
}
- //GET
- TimeRelationRefNodePtrSet get_local_active_constraints(HMscNode* n)
+ /// get set of local active constraints from ReferenceNode
+ TimeRelationRefNodePtrSet get_local_active_constraints(ReferenceNode* n)
{
TimeRelationRefNodePtrSet empty;
if(!(n->is_attribute_set(m_local_active_constraints)))
@@ -76,11 +80,28 @@
return n->get_attribute<TimeRelationRefNodePtrSet>(m_local_active_constraints,empty);
}
+ ///
+ void set_first_find_with(TimeRelationRefNode* n, ReferenceNodePtr ref)
+ {
+ n->set_attribute<ReferenceNodePtr>(m_first_find_with,ref);
+ to_be_clean.push(n);
+ }
+
+ ///
+ ReferenceNodePtr get_first_find_with(TimeRelationRefNode* n)
+ {
+ ReferenceNodePtr ref;
+ if(!(n->is_attribute_set(m_first_find_with)))
+ return ref.get();
+ else
+ return n->get_attribute<ReferenceNodePtr>(m_first_find_with,ref);
+ }
//////// END attribute handler
+ ///
void check_active_set(ReferenceNode* n, TimeRelationRefNodePtrSet set);
protected:
-
+
/**
* Common instance.
*/
@@ -88,10 +109,41 @@
HMscPtr create_counter_example(const MscElementPListList& path);
+ //! Marking functions to highlight (set_marked(true)) in visio
+ void mark_time_relations(const TimeRelationRefNodePtrSet& relations)
+ {
+ TimeRelationRefNodePtrSet::const_iterator it;
+ for(it=relations.begin();it!=relations.end();it++)
+ mark_time_relation(it->get());
+ }
+
+ void mark_time_relation(TimeRelationRefNode* relation)
+ {
+ MscElement * copy;
+ copy = m_duplicator.get_copy(relation);
+ copy->set_marked(true);
+ }
+ /// making path from traverser (set_marked(true))
+ HMscPtr process_path(const MscElementPListList& path)
+ {
+ HMscPtr p;
+ p = m_duplicator.duplicate_path(path);
+
+ MscElementPListList::const_iterator h;
+ for(h=path.begin();h!=path.end();h++)
+ {
+ MscElement* last = (*h).back();
+ m_duplicator.get_copy(last)->set_marked(true);
+ }
+
+ return p;
+ }
+
public:
HMscTimeConstrainChecker(
- const std::string& name="attribute name"
+ const std::string& local="constraints checker, local constrains"
+ ,const std::string& first_find="constraints checker, first find with"
);
~HMscTimeConstrainChecker()
@@ -99,92 +151,135 @@
cleanup_attributes();
}
- /**
- * Human readable name of the property being checked.
- */
- // note: DLL in Windows cannot return pointers to static data
+ /// Human readable name of the property being checked.
virtual std::wstring get_property_name() const
- {
+ {
return L"Time Constraints";
}
- /**
- * Ralative path to a HTML file displayed as help.
- */
+ /// Ralative path to a HTML file displayed as help.
virtual std::wstring get_help_filename() const
{ return L""; }
virtual Checker::PreconditionList get_preconditions(MscPtr msc) const;
- /**
- * Checks whether hmsc satisfy deadlock free property.
- */
+ /// Checks whether hmsc satisfy deadlock free property.
HMscPtr check(HMscPtr hmsc, ChannelMapperPtr chm);
- void on_white_node_found(HMscNode*);
+ void on_white_node_found(ReferenceNode*);
- void on_gray_node_found(HMscNode*);
+ void on_gray_node_found(ReferenceNode*);
- void on_black_node_found(HMscNode*);
+ void on_black_node_found(ReferenceNode*);
- void on_node_finished(HMscNode*);
+ void on_node_finished(ReferenceNode*);
- HMscPtr process_path(const MscElementPListList& path)
+ //! Cleans up no more needed attributes.
+ void cleanup_attributes()
{
- HMscPtr p;
- p = m_duplicator.duplicate_path(path);
+ while(!to_be_clean.empty())
+ {
+ MscElement* n = to_be_clean.top();
+ n->remove_attribute<TimeRelationRefNodePtrSet>(m_local_active_constraints);
+ n->remove_attribute<ReferenceNodePtr>(m_first_find_with);
- MscElementPListList::const_iterator h;
- for(h=path.begin();h!=path.end();h++)
- {
- MscElement* last = (*h).back();
- m_duplicator.get_copy(last)->set_marked(true);
+ to_be_clean.pop();
}
+ }
- return p;
+ /// Supports all mappers
+ bool is_supported(ChannelMapperPtr chm)
+ {
+ return true;
}
- void mark_time_relations(const TimeRelationRefNodePtrSet& relations)
+ static HMscTimeConstrainCheckerPtr instance()
{
- TimeRelationRefNodePtrSet::const_iterator it;
- for(it=relations.begin();it!=relations.end();it++)
- mark_time_relation(it->get());
+ if(!m_instance.get())
+ m_instance = HMscTimeConstrainCheckerPtr(new HMscTimeConstrainChecker());
+ return m_instance;
}
- void mark_time_relation(TimeRelationRefNode* relation)
+};
+
+
+class BMscTimeConstrainChecker:public Checker,public BMscChecker
+{
+private:
+public:
+// Checker interface
+
+ /// Human readable name of the property being checked.
+ virtual std::wstring get_property_name() const
{
- MscElement * copy;
- copy = m_duplicator.get_copy(relation);
- copy->set_marked(true);
+ return L"BMsc Time Constraints Checker";
}
+ /// Ralative path to a HTML file displayed as help.
+ virtual std::wstring get_help_filename() const
+ {
+ return L"";
+ }
+
+ /// Returns a list of preconditions for the check.
+ PreconditionList get_preconditions(MscPtr msc) const
+ {
+ return PreconditionList();
+ };
+
/**
- * Cleans up no more needed attributes.
+ * Removes no more needed attributes.
+ *
+ * Descendat of this class should remove attributes of MscElements that are no
+ * more needed. This method should be called after finish of algorithm.
*/
+ virtual void cleanup_attributes()
+ {
- void cleanup_attributes()
- {
- while(!to_be_clean.empty())
- {
- MscElement* n = to_be_clean.top();
- n->remove_attribute<TimeRelationRefNodePtrSet>(m_local_active_constraints);
- to_be_clean.pop();
- }
}
/**
- * Supports all mappers
+ * Checks whether Checker supports given ChannelMapper.
+ *
+ * Deafult behaviour is false for all mappers, but it is neccessary to check
+ * out this behaviour in individual checkers.
*/
- bool is_supported(ChannelMapperPtr chm)
+ virtual bool is_supported(ChannelMapperPtr chm)
{
return true;
}
- static HMscTimeConstrainCheckerPtr instance()
+ BMscPtr check(BMscPtr bmsc, ChannelMapperPtr mapper)
{
- if(!m_instance.get())
- m_instance = HMscTimeConstrainCheckerPtr(new HMscTimeConstrainChecker());
- return m_instance;
+ EventTopologyHandler events_top(bmsc);
+ BMscAllTimeRelationPtrSet time_relations(bmsc);
+ std::stack<TimeRelationEventPtr> broken_rel;
+ std::set<TimeRelationEventPtr>::iterator rel;
+ for(rel=time_relations.begin();rel!=time_relations.end();rel++)
+ {
+ Event* a = (*rel)->get_event_a();
+ Event* b = (*rel)->get_event_b();
+ if(!events_top.is_leq(a,b)&&!events_top.is_leq(b,a))
+ broken_rel.push(*rel);
+ }
+
+ if(broken_rel.empty())
+ return NULL;
+ else
+ {
+ BMscPtr bmsc_copy;
+ BMscDuplicator duplicator;
+ bmsc_copy = duplicator.duplicate_bmsc(bmsc);
+ while(!broken_rel.empty())
+ {
+ duplicator.get_copy((broken_rel.top()).get())->set_marked(true);
+ broken_rel.pop();
+ }
+ return bmsc_copy;
+ }
}
-};
+ ~BMscTimeConstrainChecker()
+ {
+ }
+};
\ No newline at end of file
Modified: trunk/src/check/time/module.cpp
===================================================================
--- trunk/src/check/time/module.cpp 2009-11-03 00:56:27 UTC (rev 449)
+++ trunk/src/check/time/module.cpp 2009-11-04 15:11:10 UTC (rev 450)
@@ -25,7 +25,8 @@
{
Checker **result = new Checker* [2];
result[0] = new HMscTimeConstrainChecker();
- result[1] = NULL;
+ result[1] = new BMscTimeConstrainChecker();
+ result[2] = NULL;
return result;
}
Modified: trunk/src/check/time/tightening.cpp
===================================================================
--- trunk/src/check/time/tightening.cpp 2009-11-03 00:56:27 UTC (rev 449)
+++ trunk/src/check/time/tightening.cpp 2009-11-04 15:11:10 UTC (rev 450)
@@ -30,7 +30,7 @@
IntervalList::iterator it;
for(it=list.begin();it!=list.end();it++)
{
- IntervalMatrixFunc::fill_matrix(matrix,*it,(unsigned)new_i,(unsigned)new_j);
+ matrix.fill((unsigned)new_i,(unsigned)new_j,*it);
if(con_checker->check_consistency(matrix))
m_to_go_matrix(new_i,new_j).insert(*it);
@@ -55,7 +55,7 @@
{
matrix(new_i,new_j) = MscTimeIntervalD(-D::infinity(),D::infinity());
matrix(new_j,new_i) = MscTimeIntervalD(-D::infinity(),D::infinity());
- go_back(matrix,i,j);
+ go_back(matrix,i,j);
}
}
}
@@ -93,14 +93,14 @@
{
j--;
}
- go_back(matrix,i,j);
+ go_back(matrix,i,j);
}
}
void MscSolveTCSP::init(unsigned size)
{
- m_result_matrix.resize(size,size);
- m_to_go_matrix.resize(size,size);
+ m_result_matrix.resize(size);
+ m_to_go_matrix.resize(size);
for(unsigned i=0;i<size;i++)
{
@@ -116,7 +116,7 @@
{
init(m.size1());
m_solve_matrix=m;
- IntervalMatrix matrix(m_solve_matrix.size1(),m_solve_matrix.size2());
+ IntervalMatrix matrix(m_solve_matrix.size1());
for(unsigned i=0;i<m_solve_matrix.size1();i++)
{
for(unsigned j=0;j<m_solve_matrix.size2();j++){
@@ -126,7 +126,7 @@
matrix(i,j)=MscTimeIntervalD(-D::infinity(),D::infinity());
}
- }
+ }
DEBUG(m_solve_matrix);
forward(matrix,0,-1);
Modified: trunk/src/check/time/tightening.h
===================================================================
--- trunk/src/check/time/tightening.h 2009-11-03 00:56:27 UTC (rev 449)
+++ trunk/src/check/time/tightening.h 2009-11-04 15:11:10 UTC (rev 450)
@@ -48,8 +48,39 @@
};
+
*/
+class SCTIME_EXPORT BMscTighter:public Transformer, public BMscTransformer
+{
+
+public:
+ //! Human readable name of the transformation.
+ virtual std::string get_name()
+ {
+ return std::string("BMsc Tigher");
+ }
+
+ //! List of properties that must be satisfied before executing the transformation.
+ typedef std::vector<PrerequisiteCheck> PreconditionList;
+
+ //! Returns a list of preconditions for this transformation.
+ PreconditionList get_preconditions(MscPtr msc) const
+ {
+ return PreconditionList();
+ }
+
+ BMscPtr transform(BMscPtr bmsc)
+ {
+ BMscPtr new_bmsc;
+ return new_bmsc;
+ }
+
+ ~BMscTighter() {}
+};
+
+
+
class SCTIME_EXPORT MscSolveTCSP
{
private:
@@ -66,8 +97,8 @@
public:
MscSolveTCSP():
- tightener(new FloydWarshall()),
- con_checker(new FloydWarshall())
+ tightener(new FloydWarshall()),
+ con_checker(new FloydWarshall())
{
}
@@ -81,150 +112,106 @@
typedef boost::intrusive_ptr<BMscIntervalMatrixConverter*> BMscIntervalMatrixConverterPtr;
/**
- * \brief tightens bMSC
+ * \brief tightens BMsc
*/
+
class TightenBMsc
{
private:
BMscPtr m_bmsc;
- BMscIntervalMatrixConverter m_converter;
- IntervalSetMatrix m_matrix;
+ BMscIntervalSetMatrix m_matrix;
+ EventTopologyHandler m_event_top;
+ AllReachableEventPVector m_events;
- EventPList m_mins;
- EventPList m_maxs;
+ MinimalEventPList m_mins;
+ MaximalEventPList m_maxs;
- int get_number(Event* e)
- {
- return m_converter.get_number(e);
- }
-
bool is_leq(Event* e,Event* f)
{
- return m_converter.is_leq(e,f);
+ return m_event_top.is_leq(e,f);
}
- EventPVector get_events()
+ MscTimeIntervalSetD get_max_interval(BMscIntervalSetMatrix bmsc_matrix)
{
- return m_converter.get_events();
- }
+ MscTimeIntervalSetD max_intrset;
+ MscTimeIntervalSetD evts_intrset;
+ max_intrset.insert(MscTimeIntervalD(0,0));
-public:
+ EventPairsList pairs;
+ EventPList::iterator it_min;
+ EventPList::iterator it_max;
- TightenBMsc(BMscPtr bmsc):m_bmsc(bmsc),m_converter(bmsc)
- {
- m_matrix = m_converter.get_matrix();
- m_mins = find_minimal_events();
- m_maxs = find_maximal_events();
- }
- /**
- * \brief
- */
- EventPList find_minimal_events()
- {
- EventPList minimals;
- EventPVector events = get_events();
- EventPVector::iterator it;
- EventPVector::iterator it_b;
-
- for (it=events.begin();it!=events.end();it++)
+ // for every pair (minimal,maximal) events find max_intrset
+ for (it_min=m_mins.begin();it_min!=m_mins.end();it_min++)
{
- bool is_minimal = true;
- for (it_b=events.begin();it_b!=events.end();it_b++)
+ for (it_max=m_maxs.begin();it_max!=m_maxs.end();it_max++)
{
- if (it_b != it && is_leq(*it_b,*it))
- {
- is_minimal =false;
- break;
- }
-
+ evts_intrset=bmsc_matrix(*it_min,*it_max);
+ max_intrset = MscTimeIntervalSetD::components_max(max_intrset,evts_intrset);
}
- if (is_minimal)
- {
- minimals.push_back(*it);
- }
}
- return minimals;
+ return max_intrset;
}
- /**
- * \brief
- */
- EventPList find_maximal_events()
- {
- EventPList maximals;
- EventPVector events = get_events();
- EventPVector::iterator it;
- EventPVector::iterator it_b;
- for (it=events.begin();it!=events.end();it++)
- {
- bool is_maximal = true;
- for (it_b=events.begin();it_b!=events.end();it_b++)
- {
- if (it_b != it && is_leq(*it,*it_b))
- {
- is_maximal =false;
- break;
- }
+public:
- }
- if (is_maximal)
- {
- maximals.push_back(*it);
- }
- }
- return maximals;
+ TightenBMsc(BMscPtr bmsc):m_bmsc(bmsc),m_matrix(bmsc),m_event_top(bmsc)
+ ,m_events(bmsc),m_mins(bmsc),m_maxs(bmsc)
+ {
}
- /**
- * \brief tightens interval and matrix according to each other
- * \return pair - changed interval and matrix
- */
- ConstMatrixPair max_tightener(
- IntervalSetMatrix t_matrix,
- MscTimeIntervalSetD interval
- )
+ static ConstMatrixPair tight(
+ BMscPtr bmsc
+ ,MscTimeIntervalSetD interval)
{
+ TightenBMsc tightening(bmsc);
+ ConstMatrixPair pair = tightening.tighten_msc(interval);
+ //tightening.modificate(pair.second);
+ return pair;
+ }
- MscTimeIntervalSetD max_intrset;
- MscTimeIntervalSetD evts_intrset;
- max_intrset.insert(MscTimeIntervalD(0,0));
+ //! tight BMsc due to interval
+ ConstMatrixPair tighten_msc(MscTimeIntervalSetD interval)
+ {
- EventPairsList pairs;
+ MscSolveTCSP solve;
+ BMscIntervalSetMatrix old_matrix(m_matrix);
+ BMscIntervalSetMatrix current_matrix(m_matrix);
- EventPList::iterator it_min;
- EventPList::iterator it_max;
-
- // for every pair (minimal,maximal) events
- for (it_min=m_mins.begin();it_min!=m_mins.end();it_min++)
+ // pair (MscTimeIntervalSetD,IntervalSetMatrix)
+ ConstMatrixPair pair;
+ do
{
- for (it_max=m_maxs.begin();it_max!=m_maxs.end();it_max++)
- {
- evts_intrset=t_matrix(get_number(*it_min),get_number(*it_max));
- max_intrset = MscTimeIntervalSetD::components_max(
- max_intrset,
- evts_intrset
- );
-
- /*
- if(!MscTimeIntervalSetD::set_intersection(interval,
- t_matrix(get_number(*it_min),get_number(*it_max))).is_empty())
- pairs.push_back(std::make_pair(*it_min,*it_max));
- */
- }
+ old_matrix = current_matrix;
+ // tight matrix
+ current_matrix = solve.solve(current_matrix);
+ // tight both matrix and interval with respect to each other
+ pair = max_tightener(current_matrix,interval);
+ // assign tightened interval
+ interval = pair.first;
}
+ while (!IntervalMatrixFunc::is_equal(old_matrix,current_matrix));
+ return pair; // tighten interval, bmsc matrix
+ }
+
+ //! tightens interval and matrix according to each other
+ ConstMatrixPair max_tightener(BMscIntervalSetMatrix t_matrix
+ ,MscTimeIntervalSetD interval
+ )
+ {
+ MscTimeIntervalSetD max_intrset = get_max_interval(t_matrix);
// assign tightened interval
interval = MscTimeIntervalSetD::set_intersection(interval,max_intrset);
- // TODO:
- EventPVector all_events = get_events();
EventPVector::iterator it_v;
// for all a \in events
// for all b \in a.get_next do
- for (it_v = all_events.begin();it_v!=all_events.end();it_v++)
+ for (it_v = m_events.begin();it_v!=m_events.end();it_v++)
{
EventPSet succs = EventFirstSuccessors::get(*it_v);
EventPSet::iterator it_succ;
+
for (it_succ=succs.begin();it_succ!=succs.end();it_succ++)
{
EventPList::iterator it_min_events;
@@ -233,195 +220,53 @@
for (it_min_events=m_mins.begin();it_min_events!=m_mins.end();it_min_events++)
{
-
for (it_max_events=m_maxs.begin();it_max_events!=m_maxs.end();it_max_events++)
{
if (is_leq(*it_min_events,*it_v)&&is_leq(*it_succ,*it_max_events))
continue;
- path_union=MscTimeIntervalSetD::set_union(path_union,
- t_matrix(get_number(*it_min_events),get_number(*it_max_events))
- );
+ path_union=MscTimeIntervalSetD::set_union(
+ path_union,t_matrix(*it_min_events,*it_max_events));
}
}
MscTimeIntervalSetD tight_interval;
tight_interval = MscTimeIntervalSetD::set_union(interval,
MscTimeIntervalSetD::zero_max_interval(path_union,interval));
-
MscTimeIntervalSetD prefix_interval;
prefix_interval.insert(MscTimeIntervalD(0,0));
+
for (it_min_events=m_mins.begin();it_min_events!=m_mins.end();it_min_events++)
{
prefix_interval=MscTimeIntervalSetD::components_max(
- t_matrix(get_number(*it_min_events),get_number(*it_v)),prefix_interval);
+ t_matrix(*it_min_events,*it_v),prefix_interval);
}
MscTimeIntervalSetD suffix_interval;
suffix_interval.insert(MscTimeIntervalD(0,0));
- for (it_max_events=m_maxs.begin();it_max_events!=m_maxs.end();it_max_events++)
+
+ for (it_max_events=m_maxs.begin();
+ it_max_events!=m_maxs.end();
+ it_max_events++)
{
suffix_interval=MscTimeIntervalSetD::components_max(
- t_matrix(get_number(*it_succ),get_number(*it_max_events)),suffix_interval);
+ t_matrix(*it_succ,*it_max_events),suffix_interval);
}
//final tightening
- t_matrix(get_number(*it_v),get_number(*it_succ))=MscTimeIntervalSetD::set_intersection(t_matrix(get_number(*it_v),get_number(*it_succ)),tight_interval-prefix_interval-suffix_interval);
+ t_matrix(*it_v,*it_succ)=MscTimeIntervalSetD::set_intersection(
+ t_matrix(*it_v,*it_succ)
+ ,tight_interval-prefix_interval-suffix_interval);
} // end for succs
} // end for all events
- /*
- bool is_on_common_path;
- EventPSet nodes_on_common_path;
- EventPVector::iterator it_v;
- EventPVector events = get_events();
-
- for(it_v = events.begin();it_v!=events.end();it_v++)
- {
- is_on_common_path=true;
- EventPairsList::iterator it_a;
- for(it_a=pairs.begin();it_a!=pairs.end();it_a++)
- {
- if(!is_leq(it_a->first,(*it_v)) || !is_leq(*it_v,it_a->second))
- {
- is_on_common_path = false;
- break;
- }
- }
-
- if(is_on_common_path)
- {
- nodes_on_common_path.insert(*it_v);
- }
- }
-
- if(nodes_on_common_path.empty())
- return std::make_pair(z,t_matrix);
-
- Event* min_random;
- Event* max_random;
-
- EventPSet::iterator it_set;
- EventPSet::iterator it_set_b;
-
- for(it_set=nodes_on_common_path.begin();it_set!=nodes_on_common_path.end();it_set++)
- {
- bool is_minimal = true;
- for(it_set_b=nodes_on_common_path.begin();it_set_b!=nodes_on_common_path.end();it_set_b++)
- {
- if(it_set_b != it_set && is_leq(*it_set_b,*it_set))
- {
- is_minimal =false;
- break;
- }
-
- }
- if(is_minimal)
- {
- min_random = *it_set;
- break;
- }
- }
-
- for(it_set=nodes_on_common_path.begin();it_set!=nodes_on_common_path.end();it_set++)
- {
- if(*it_set == min_random || is_leq(*it_set,min_random))
- continue;
- bool is_maximal = true;
- for(it_set_b=nodes_on_common_path.begin();it_set_b!=nodes_on_common_path.end();it_set_b++)
- {
- if(it_set_b != it_set && is_leq(*it_set,*it_set_b))
- {
- is_maximal =false;
- break;
- }
-
- }
- if(is_maximal)
- {
- max_random = *it_set;
- break;
- }
- }
- MscTimeIntervalSetD from_min;
- MscTimeIntervalSetD from_max;
- from_min.insert(MscTimeIntervalD(0,0));
- from_max.insert(MscTimeIntervalD(0,0));
-
- for(it_min=m_mins.begin();it_min!=m_mins.end();it_min++)
- {
- from_min = MscTimeIntervalSetD::components_max(from_min,
- t_matrix(get_number(*it_min),get_number(min_random)));
- }
-
- for(it_max=m_maxs.begin();it_max!=m_maxs.end();it_max++)
- {
- from_max = MscTimeIntervalSetD::components_max(from_max,
- t_matrix(get_number(*it_max),get_number(max_random)));
- }
-
- t_matrix(get_number(min_random),get_number(max_random))= \
- MscTimeIntervalSetD::set_intersection(
- t_matrix(get_number(min_random),get_number(max_random)),
- ((i - from_min) - from_max));
- */
return std::make_pair(interval,t_matrix);
}
- /**
- * \brief
- */
- static MscTimeIntervalSetD tight(
- BMscPtr bmsc,
- MscTimeIntervalSetD interval)
- {
- TightenBMsc tightening(bmsc);
- ConstMatrixPair pair = tightening.tighten_msc(interval);
- tightening.modificate(pair.second);
- return pair.first;
- }
-
- void modificate(IntervalSetMatrix matrix)
- {
- m_converter.modificate(matrix);
- }
-
-
- /**
- * \brief tightens bMSC
- * \parms interval of duration of bmsc
- */
- ConstMatrixPair tighten_msc(MscTimeIntervalSetD interval)
- {
-
- MscSolveTCSP solve;
- IntervalSetMatrix old_matrix;
- IntervalSetMatrix current_matrix;
-
- // pair (MscTimeIntervalSetD,IntervalSetMatrix)
- ConstMatrixPair pair;
-
- current_matrix = m_matrix;
-
- do
- {
- old_matrix = current_matrix;
- // tight matrix
- current_matrix = solve.solve(current_matrix);
- // tight both matrix and interval with respect to each other
- pair = max_tightener(current_matrix,interval);
- // assign tightened interval
- interval = pair.first;
- }
- while(!IntervalMatrixFunc::is_equal(old_matrix,current_matrix));
-
- return pair; // tighten interval, bmsc matrix
- }
-
}; // class TightenBMsc
typedef std::list<HMscNodePtr> HMscNodePtrList;
-
+/*
class TightenSetOfPaths
{
private:
@@ -437,12 +282,7 @@
MscTimeIntervalSetD i_prime_prime;
public:
// HMscAllPaths
- /*
- BMscPtr return_inner_bmsc(HmscNodePtr node)
- {
- }
- */
MscTimeIntervalSetD tighten(
HMscAllPaths paths,
MscTimeIntervalSetD i,
@@ -454,9 +294,11 @@
//initialization of both copies
BMscDuplicator bmsc_duplicator_1;
std::list<HMscPath>::iterator it;
+
for (it=paths.first.begin();it!=paths.first.end();it++)
{
std::list<HMscNodePtr>::iterator node;
+
for (node=(*it).first.begin();node!=(*it).first.end();node++)
{
ReferenceNode* ref_node = dynamic_cast<ReferenceNode*>((*node).get());
@@ -466,22 +308,29 @@
}
BMscDuplicator bmsc_duplicator_2;
+
HMscNodePtrSet all_nodes = hmsc->get_nodes();
HMscNodePtrSet::iterator hmsc_node;
+
for (hmsc_node=all_nodes.begin();hmsc_node!=all_nodes.end();hmsc_node++)
{
ReferenceNode* ref_node = dynamic_cast<ReferenceNode*>((*hmsc_node).get());
+
if (!ref_node)
continue;
+
BMscPtr bmsc = ref_node->get_bmsc();
+
if (!bmsc)
continue;
+
m_bmsc_copy2.insert(bmsc_duplicator_2.duplicate_bmsc(bmsc));
}
// std::list<HMscPath>::iterator it;
+
for (it=paths.first.begin();it!=paths.first.end();it++)
{
@@ -494,20 +343,28 @@
n_path = it->first.begin();
ReferenceNode* ref_node = dynamic_cast<ReferenceNode*>((*n_path).get());
BMscPtr from_node = ref_node->get_bmsc();
+
if (from_node)
m_msc = from_node;
+
n_path_previous = n_path;
+
n_path++;
+
for (;n_path!=it->first.end();n_path++)
{
n_path_previous++;
ReferenceNode* ref_node = dynamic_cast<ReferenceNode*>((*n_path).get());
+
if (!ref_node)
continue;
TimeRelationRefNodePtrSet constr_set = ref_node->get_time_relations_top();
+
TimeRelationRefNodePtrSet::iterator it_c;
+
bool has_constraint = false;
+
for (it_c=constr_set.begin();it_c!=constr_set.end();it_c++)
{
if ((*it_c)->get_ref_node_b() == (*n_path_previous).get()) //Warning: we assume that nodes in time relation ref node are ordered
@@ -517,6 +374,7 @@
}
}
+
if (has_constraint)
{
m_constr.push_back(*it_c);
@@ -524,15 +382,18 @@
ReferenceNode* ref_node = dynamic_cast<ReferenceNode*>((*n_path).get());
BMscPtr from_node = ref_node->get_bmsc();
+
if (from_node)
m_msc = from_node;
}
+
else
{
BMscPtr msc_tmp;
ReferenceNode* ref_node = dynamic_cast<ReferenceNode*>((*n_path).get());
BMscPtr from_node = ref_node->get_bmsc();
+
if (from_node)
msc_tmp = from_node;
@@ -542,6 +403,7 @@
}
ConstMatrixPair pair;
+
if (m_msc_list.empty())
{
TightenBMsc tighten_msc(m_msc);
@@ -549,11 +411,12 @@
m_t = pair.second;
i_prime_prime = MscTimeIntervalSetD::set_intersection(i_prime_prime,pair.first);
}
+
else
{
m_msc_list.push_back(m_msc);
MscTimeIntervalSetD i_prime_prime_prime;
-// TightenMsgPath tighten_msg_path(m_msc_list); //TODO: MSG PATH
+// TightenMsgPath tighten_msg_path(m_msc_list); //TODO: MSG PATH
i_prime_prime_prime = tighten_msg_path(m_msc_list,m_constr,i);
i_prime_prime = MscTimeIntervalSetD::set_intersection(i_prime_prime,pair.first);
@@ -567,8 +430,9 @@
{
//TODO:write get_all_constraints
std::set<TimeRelationEventPtr> constraints;
-// constraints = get_all_constraints(*path_it);
+// constraints = get_all_constraints(*path_it);
std::set<TimeRelationEventPtr>::iterator tr_it;
+
for (tr_it = constraints.begin(); tr_it != constraints.end(); tr_it++)
{
TimeRelationEvent* relation_copy = dynamic_cast<TimeRelationEvent*>(bmsc_duplicator_1.get_copy((*tr_it).get()));
@@ -580,12 +444,14 @@
//TODO:upravit nakopirovat povodne obmedzenia naspat
// m_bmsc_all_set = m_bmsc_copy2;
+
for (path_it = it->first.begin(); path_it!= it->first.end(); path_it++)
{
//TODO:write get_all_constraints
std::set<TimeRelationEventPtr> constraints;
-// constraints = get_all_constraints(*path_it);
+// constraints = get_all_constraints(*path_it);
std::set<TimeRelationEventPtr>::iterator tr_it;
+
for (tr_it = constraints.begin(); tr_it != constraints.end(); tr_it++)
{
@@ -599,6 +465,7 @@
std::set<BMscPtr>::iterator b_it2;
+
for (b_it2 = m_bmsc_copy2.begin(); b_it2!= m_bmsc_copy2.end(); b_it2++)
{
//TODO:write get_all_constraints
@@ -629,6 +496,7 @@
{
MscTimeIntervalSetD tmp_interval(interval);
std::vector<MscTimeIntervalSetD> durations;
+
for (size_t i=0;i<list_bmsc.size();i++)
{
MscTimeIntervalSetD tmp;
@@ -638,53 +506,70 @@
}
MscTimeIntervalSetD s_interval;
+
do
{
s_interval = tmp_interval;
std::list<BMscPtr>::iterator bmsc;
unsigned int i=0;
+
for (bmsc=list_bmsc.begin();bmsc!=list_bmsc.end();bmsc++,i++)
{
MscTimeIntervalSetD tmp_i=tmp_interval;
+
for (size_t j=0;j<list_bmsc.size();j++)
{
if (i==j)
continue;
+
tmp_i = tmp_i - durations[j];
}
+
std::list<TimeRelationRefNodePtr>::iterator c_it;
+
for (c_it=constr.begin();c_it!=constr.end();c_it++)
tmp_i = tmp_i - (*c_it)->get_interval_set();
durations[i]=TightenBMsc::tight(*bmsc,MscTimeIntervalSetD::set_intersection(tmp_i,durations[i]));
}
+
MscTimeIntervalSetD interval_set;
std::list<TimeRelationRefNodePtr>::iterator c_it2;
+
for (c_it2=constr.begin();c_it2!=constr.end();c_it2++)
{
interval_set = (*c_it2)->get_interval_set();
MscTimeIntervalSetD tmp_i=tmp_interval;
+
for (size_t j=0;j<list_bmsc.size();j++)
{
tmp_i = tmp_i - durations[j];
}
+
interval_set = (*c_it2)->get_interval_set();
+
std::list<TimeRelationRefNodePtr>::iterator c_it;
+
for (c_it=constr.begin();c_it!=constr.end();c_it++)
{
interval_set = (*c_it2)->get_interval_set();
+
if (*c_it==*c_it2)
continue;
+
tmp_i = tmp_i - (*c_it)->get_interval_set();
}
+
interval_set = (*c_it2)->get_interval_set();
+
(*c_it2)->set_interval_set(MscTimeIntervalSetD::set_intersection((*c_it2)->get_interval_set(),tmp_i));
interval_set = (*c_it2)->get_interval_set();
}
MscTimeIntervalSetD tmp;
+
tmp.insert(MscTimeIntervalD(0,0));
for (size_t j=0;j<list_bmsc.size();j++)
@@ -693,6 +578,7 @@
}
std::list<TimeRelationRefNodePtr>::iterator c_it;
+
for (c_it=constr.begin();c_it!=constr.end();c_it++)
{
MscTimeIntervalSetD uu = (*c_it)->get_interval_set();
@@ -702,12 +588,13 @@
tmp_interval = MscTimeIntervalSetD::set_intersection(tmp_interval,tmp);
}
+
while (s_interval!=tmp_interval);
return tmp_interval;
}
-};
+};*/
#endif //_TIGHTENING_H_
Modified: trunk/src/check/time/time_pseudocode.cpp
===================================================================
--- trunk/src/check/time/time_pseudocode.cpp 2009-11-03 00:56:27 UTC (rev 449)
+++ trunk/src/check/time/time_pseudocode.cpp 2009-11-04 15:11:10 UTC (rev 450)
@@ -1,22 +1,21 @@
#include "time_pseudocode.h"
-void BMscIntervalMatrixConverter::build_up_matrix()
+void BMscIntervalSetMatrix::build_up_matrix()
{
- init_visual();
- m_matrix.resize(m_events.size(),m_events.size());
+ IntervalSetMatrix::resize(m_events.size());
for (unsigned i=0;i<m_events.size();i++)
{
for (unsigned j=0;j<m_events.size();j++)
{
if (j==i)
{
- m_matrix(i,j) =MscTimeIntervalSetD();
- m_matrix(i,j).insert(MscTimeIntervalD(0,0));
+ operator()(i,j)=MscTimeIntervalSetD();
+ operator()(i,j).insert(MscTimeIntervalD(0,0));
}
else
{
- m_matrix(i,j) =MscTimeIntervalSetD();
- m_matrix(i,j).insert(MscTimeIntervalD(-D::infinity(),D::infinity()));
+ operator()(i,j) =MscTimeIntervalSetD();
+ operator()(i,j).insert(MscTimeIntervalD(-D::infinity(),D::infinity()));
}
}
}
@@ -26,13 +25,14 @@
for (e_v=m_events.begin();e_v!=m_events.end();e_v++)
{
- EventPSet& set = m_succs[*e_v];
+ EventPSet set = EventFirstSuccessors::get(*e_v);
for (e_m=set.begin();e_m!=set.end();e_m++)
{
- m_matrix(get_number(*e_v),get_number(*e_m)) = MscTimeIntervalSetD();
- m_matrix(get_number(*e_v),get_number(*e_m)).insert(MscTimeIntervalD(0,D::infinity()));
- m_matrix(get_number(*e_m),get_number(*e_v)) = MscTimeIntervalSetD();
- m_matrix(get_number(*e_m),get_number(*e_v)).insert(MscTimeIntervalD(-D::infinity(),0));
+ operator()(*e_v,*e_m) = MscTimeIntervalSetD();
+ operator()(*e_v,*e_m).insert(MscTimeIntervalD(0,D::infinity()));
+
+ operator()(*e_m,*e_v) = MscTimeIntervalSetD();
+ operator()(*e_m,*e_v).insert(MscTimeIntervalD(-D::infinity(),0));
}
TimeRelationEventPtrList::iterator it;
@@ -40,33 +40,19 @@
for (it=relations.begin();it!=relations.end();it++)
{
- if (m_closure_initiator.get_visual_closure((*it)->get_event_a())[
- m_closure_initiator.get_topology_index((*it)->get_event_b())])
+ m_time_rel_set.insert(*it);
+ EventP a = (*it)->get_event_a();
+ EventP b = (*it)->get_event_b();
+ if (m_event_topology.is_leq(a,b))
{
- IntervalMatrixFunc::fill_matrix(m_matrix, (*it)->get_interval_set()
- ,get_number((*it)->get_event_a())
- ,get_number((*it)->get_event_b()));
+ fill(a,b,(*it)->get_interval_set());
}
else
{
- IntervalMatrixFunc::fill_matrix(m_matrix, (*it)->get_interval_set()
- ,get_number((*it)->get_event_b())
- ,get_number((*it)->get_event_a()));
+ fill(b,a,(*it)->get_interval_set());
}
}
}
}
-void BMscIntervalMatrixConverter::init_visual()
-{
- m_traverser.add_event_finished_listener(&m_topology_listener);
- m_traverser.traverse(m_bmsc);
- EventPVector topology(m_topology_listener.get_topology().size());
- topology.assign(
- m_topology_listener.get_topology().begin(),
- m_topology_listener.get_topology().end()
- );
- m_closure_initiator.initialize(topology);
-}
-
// $Id$
Modified: trunk/src/check/time/time_pseudocode.h
===================================================================
--- trunk/src/check/time/time_pseudocode.h 2009-11-03 00:56:27 UTC (rev 449)
+++ trunk/src/check/time/time_pseudocode.h 2009-11-04 15:11:10 UTC (rev 450)
@@ -23,11 +23,13 @@
#include "data/msc.h"
#include "data/dfs_hmsc_traverser.h"
#include "data/dfs_events_traverser.h"
-#include "check/pseudocode/visual_closure_initiator.h"
+
#include "check/pseudocode/utils.h"
#include "check/time/export.h"
+#include "check/pseudocode/msc_duplicators.h"
#include <set>
+#include <stdexcept>
//Boost matix
#include <boost/numeric/ublas/matrix.hpp>
@@ -39,19 +41,226 @@
typedef std::vector<Event*> EventPVector;
typedef std::set<Event*> EventPSet;
typedef std::map<Event*,EventPSet> EventPMap;
-typedef boost::numeric::ublas::matrix<MscTimeIntervalD> IntervalMatrix;
-typedef boost::numeric::ublas::matrix<MscTimeIntervalSetD> IntervalSetMatrix;
typedef std::numeric_limits<double> D;
+typedef boost::numeric::ublas::matrix<MscTimeIntervalD> BoostIntervalMatrix;
+typedef boost::numeric::ublas::matrix<MscTimeIntervalSetD> BoostIntervalSetMatrix;
+class HMscAllTimeRelations;
-class HMscAllTimeRelations;
class IntervalMatrixFunc;
-
class BMscIntervalMatrixConverter;
+class IntervalMatrix:public BoostIntervalMatrix
+{
+public:
+ IntervalMatrix()
+ {}
+ IntervalMatrix(unsigned size):BoostIntervalMatrix(size,size)
+ {}
+ using BoostIntervalMatrix::operator();
+ //! adding to the matrix INTERVAL c to (x,y) and its inverse to (y,x)
+ void fill(size_type x,size_type y,MscTimeIntervalD& c)
+ {
+ if (x>=size1()||y>=size2()||x>=size2()||y>=size1())
+ throw size1();
+ operator()(x,y)=c;
+ operator()(y,x)=MscTimeIntervalD::interval_inverse(c);
+ }
+};
+
+class IntervalSetMatrix:public BoostIntervalSetMatrix
+{
+public:
+ IntervalSetMatrix()
+ {}
+
+ IntervalSetMatrix(const IntervalSetMatrix& matrix):BoostIntervalSetMatrix(matrix)
+ {}
+
+ using BoostIntervalSetMatrix::operator();
+
+ //! adding to the matrix-set INTERVAL SET c to (x,y) and its inverse to (y,x)
+ void fill(size_type x,size_type y,MscTimeIntervalSetD& c)
+ {
+ if (x>=size1()||y>=size2()||x>=size2()||y>=size1())
+ throw size1();
+
+ operator()(x,y) = c;
+
+ operator()(y,x) = MscTimeIntervalSetD::interval_inverse(c);
+ }
+
+ //! adding to the matrix-set INTERVAL c to (x,y) and its inverse to (y,x)
+
+ void fill(size_type x,size_type y,MscTimeIntervalD& c)
+ {
+ if (x>=size1()||y>=size2()||x>=size2()||y>=size1())
+ throw size1();
+
+ operator()(x,y).insert(c);
+
+ operator()(y,x).insert(MscTimeIntervalD::interval_inverse(c));
+ }
+
+ void resize(size_type i)
+ {
+ BoostIntervalSetMatrix::resize(i,i);
+ }
+
+ IntervalSetMatrix& operator=(const IntervalSetMatrix& matrix)
+ {
+ BoostIntervalSetMatrix::operator=(matrix);
+ return *this;
+ }
+};
+
+class SCTIME_EXPORT BMscIntervalSetMatrix: public IntervalSetMatrix
+{
+private:
+ BMscPtr m_original_bmsc;
+ AllReachableEventPVector m_events; //! Vector of all events: event=matrix[number]
+ std::map<EventP,unsigned> m_event_number; //! the number of event in the matrix
+
+ EventTopologyHandler m_event_topology;
+ //! set of all time relations,creates in build_up_matrix() function
+ std::set<TimeRelationEventPtr> m_time_rel_set;
+
+ //! initialization of visual closure
+
+ void build_up_matrix();
+
+ void cleanup_attributes()
+ {
+ }
+
+ /**
+ * \brief Apply changes from the matrix to the bmsc copy
+ */
+
+public:
+ BMscIntervalSetMatrix(BMscPtr bmsc):
+ m_original_bmsc(bmsc)
+ ,m_events(bmsc)
+ ,m_event_topology(bmsc)
+ {
+ std::vector<EventP>::iterator it;
+ unsigned i;
+
+ // set numbers to events and their succs
+ for (it=m_events.begin(),i=0;it!=m_events.end();it++,i++)
+ {
+ m_event_number[*it]=i;
+ }
+ build_up_matrix();
+ }
+
+ BMscIntervalSetMatrix(const BMscIntervalSetMatrix& matrix):
+ IntervalSetMatrix(matrix)
+ ,m_event_topology(matrix.get_original_bmsc())
+ {
+ m_original_bmsc=matrix.m_original_bmsc;
+ m_events=matrix.m_events;
+ m_event_number=matrix.m_event_number;
+ m_time_rel_set=matrix.m_time_rel_set;
+ }
+
+ using IntervalSetMatrix::operator();
+
+ //! return number of event in matrix
+ unsigned get_number(EventP e)
+ {
+ return m_event_number[e];
+ }
+
+ MscTimeIntervalSetD& operator()(EventP a,EventP b)
+ {
+ return operator()(get_number(a),get_number(b));
+ }
+
+ MscTimeIntervalSetD& operator()(EventP a)
+ {
+ return operator()(get_number(a),get_number(a));
+ }
+
+ BMscIntervalSetMatrix& operator=(const BMscIntervalSetMatrix& matrix)
+ {
+ if(m_original_bmsc!=matrix.m_original_bmsc)
+ throw std::invalid_argument("BMscs dont match!");
+ IntervalSetMatrix::operator=(matrix);
+ return *this;
+ }
+
+ BMscIntervalSetMatrix& operator=(const IntervalSetMatrix& matrix)
+ {
+ IntervalSetMatrix::operator=(matrix);
+ return *this;
+ }
+
+
+ //! return all reachable events in bmsc
+ const EventPVector get_events()
+ {
+ return m_events;
+ }
+
+ //! Takes (modificated) matrix of bmsc and changes bmsc
+ BMscPtr get_modified_bmsc()
+ {
+ // duplicate bmsc
+ BMscPtr copy_bmsc;
+ BMscDuplicator duplicator;
+ copy_bmsc = duplicator.duplicate_bmsc(m_original_bmsc);
+
+ // go through all relations and set copy new values
+ std::set<TimeRelationEventPtr>::iterator it;
+ for(it=m_time_rel_set.begin();it!=m_time_rel_set.end();it++)
+ {
+ EventP a = (*it)->get_event_a();
+ EventP b = (*it)->get_event_b();
+ // set new value to time relation
+ if (m_event_topology.is_leq(a,b))
+ {
+ TimeRelationEvent* relation;
+ relation = static_cast<TimeRelationEvent*>(duplicator.get_copy(it->get()));
+ relation->set_interval_set(operator()(a,b));
+ }
+ else
+ {
+ (*it)->set_interval_set(operator()(b,a));
+ }
+ }
+ return copy_bmsc;
+ }
+ //! return original bmsc (assigned to the matrix)
+ BMscPtr get_original_bmsc() const
+ {
+ return m_original_bmsc;
+ }
+
+ ~BMscIntervalSetMatrix()
+ {
+ }
+/*
+ //! adding to the matrix-set INTERVAL SET c to (x,y) and its inverse to (y,x)
+ void fill(EventP x,EventP y,MscTimeIntervalD& c)
+ {
+ (*this)(x,y).insert(c);
+ (*this)(y,x).insert(MscTimeIntervalD::interval_inverse(c));
+ }
+*/
+ //! puts IntervalSet in to the matrix to the position of events x,y
+ void fill(EventP x,EventP y,const MscTimeIntervalSetD& c)
+ {
+ operator()(x,y)=c;
+ operator()(y,x)= MscTimeIntervalSetD::interval_inverse(c);
+ }
+
+}; // end of class BMscMatrixConverter
+
// pick up all time relation in HMsc
+
class HMscAllTimeRelations:public WhiteRefNodeFoundListener
{
private:
@@ -99,42 +308,30 @@
};
-class IntervalMatrixFunc
+class BMscAllTimeRelationPtrSet:public std::set<TimeRelationEventPtr>
{
+private:
public:
- //! adding to the matrix INTERVAL c to (x,y) and its inverse to (y,x)
- static
- void fill_matrix(IntervalMatrix& matrix, MscTimeIntervalD c,\
- unsigned x,unsigned y)
+ BMscAllTimeRelationPtrSet(BMscPtr bmsc)
{
- if (x>=matrix.size1()||y>=matrix.size2())
- throw matrix.size1();
- matrix(x,y) = c;
- matrix(y,x) = MscTimeIntervalD::interval_inverse(c);
+ AllReachableEventPVector all_events(bmsc);
+ std::vector<EventP>::iterator e;
+ for(e=all_events.begin();e!=all_events.end();e++)
+ {
+ TimeRelationEventPtrList time_relations;
+ std::list<TimeRelationEventPtr>::iterator rel;
+ time_relations=(*e)->get_time_relations();
+ for(rel=time_relations.begin();rel!=time_relations.end();rel++)
+ {
+ insert(*rel);
+ }
+ }
}
+};
- //! adding to the matrix-set INTERVAL SET c to (x,y) and its inverse to (y,x)
- static
- void fill_matrix(IntervalSetMatrix& matrix, MscTimeIntervalSetD c, \
- unsigned x,unsigned y)
- {
- if (x>=matrix.size1()||y>=matrix.size2())
- throw matrix.size1();
- matrix(x,y) = c;
- matrix(y,x) = MscTimeIntervalSetD::interval_inverse(c);
- }
-
- //! adding to the matrix-set INTERVAL c to (x,y) and its inverse to (y,x)
- static
- void fill_matrix(IntervalSetMatrix& matrix, MscTimeIntervalD c, \
- unsigned x,unsigned y)
- {
- if (x>=matrix.size1()||y>=matrix.size2())
- throw matrix.size1();
- matrix(x,y).insert(c);
- matrix(y,x).insert(MscTimeIntervalD::interval_inverse(c));
- }
-
+class IntervalMatrixFunc
+{
+public:
//! check whether two matrices are equal
static
bool is_equal(
@@ -144,19 +341,27 @@
if (&lhs == &rhs)
return true;
+
if (lhs.size1() != rhs.size1())
return false;
+
if (lhs.size2() != rhs.size2())
return false;
+
IntervalSetMatrix::iterator1 l(lhs.begin1());
+
IntervalSetMatrix::iterator1 r(rhs.begin1());
+
while (l != lhs.end1())
{
if (*l != *r)
return false;
+
++l;
+
++r;
}
+
return true;
}
@@ -165,138 +370,24 @@
{
std::cout << "matrix: " << matrix.size1() << "x" <<
matrix.size2() << std::endl;
+
for (unsigned i=0;i<matrix.size1();i++)
{
for (unsigned j=0;j<matrix.size2();j++)
{
std::cout << " {" << matrix(i,j) << "}";
}
+
std::cout << std::endl;
}
}
}; //end of IntervalMatrix
-class SCTIME_EXPORT BMscIntervalMatrixConverter:public WhiteEventFoundListener
-{
-private:
- BMscPtr m_bmsc;
- EventPVector m_events; //!< Vector of all events - event <-- matrix number
- EventPMap m_succs; //!< Map of event and its first successors
- IntervalSetMatrix m_matrix; //!< main matrix of Interval Sets
- std::string m_number; //!< attribute,event(m_number=number) --> matrix
- VisualClosureInitiator m_closure_initiator;
- TopologicalOrderListener m_topology_listener;
- DFSEventsTraverser m_traverser;
- //!< bmsc to be converted to the matrix
-
- void pick_up_events()
- {
- m_traverser.add_white_event_found_listener(this);
- m_traverser.traverse(m_bmsc);
- m_traverser.remove_white_event_found_listeners();
- }
-
- //! initialization of visual closure
- void init_visual();
-
- void build_up_matrix();
-
- void set_number(Event* e,int number)
- {
- return e->set_attribute<int> (m_number,number);
- }
-
- void cleanup_attributes()
- {
- EventPVector::iterator event;
- for (event=m_events.begin();event!=m_events.end();event++)
- (*event)->remove_attribute<int> (m_number);
- }
-
-public:
- BMscI...
[truncated message content] |
