Menu
▾
▴
[Scstudio-commits] SF.net SVN: scstudio:[256] trunk
|
From: <koc...@us...> - 2009-07-05 16:44:43
|
Revision: 256
http://scstudio.svn.sourceforge.net/scstudio/?rev=256&view=rev
Author: kocianon
Date: 2009-07-05 16:44:41 +0000 (Sun, 05 Jul 2009)
Log Message:
-----------
adding time algorithms for hmsc and bmsc
Modified Paths:
--------------
trunk/src/check/CMakeLists.txt
trunk/src/check/pseudocode/msc_duplicators.cpp
trunk/src/check/pseudocode/msc_duplicators.h
trunk/src/data/CMakeLists.txt
trunk/src/data/msc.cpp
trunk/src/data/msc.h
trunk/src/data/time.cpp
trunk/src/data/time.h
trunk/tests/CMakeLists.txt
trunk/tests/interval_set_test.cpp
Added Paths:
-----------
trunk/src/check/time/
trunk/src/check/time/CMakeLists.txt
trunk/src/check/time/bmsc_tightening.h
trunk/src/check/time/hmsc_all_paths.cpp
trunk/src/check/time/hmsc_all_paths.h
trunk/src/check/time/hmsc_tighten.cpp
trunk/src/check/time/hmsc_tighten.h
trunk/src/check/time/time_consistency.cpp
trunk/src/check/time/time_consistency.h
trunk/tests/bmsc_matrix_converter_test.cpp
trunk/tests/bmsc_tightening_test.cpp
trunk/tests/hmsc_all_paths_test.cpp
trunk/tests/incon_test.cpp
trunk/tests/max_tightener_test.cpp
trunk/tests/tighten_msc_test.cpp
Property Changed:
----------------
trunk/src/data/
Modified: trunk/src/check/CMakeLists.txt
===================================================================
--- trunk/src/check/CMakeLists.txt 2009-06-21 21:12:06 UTC (rev 255)
+++ trunk/src/check/CMakeLists.txt 2009-07-05 16:44:41 UTC (rev 256)
@@ -6,5 +6,6 @@
ADD_SUBDIRECTORY(race)
ADD_SUBDIRECTORY(boundedness)
ADD_SUBDIRECTORY(structure)
+ADD_SUBDIRECTORY(time)
# $Id$
Modified: trunk/src/check/pseudocode/msc_duplicators.cpp
===================================================================
--- trunk/src/check/pseudocode/msc_duplicators.cpp 2009-06-21 21:12:06 UTC (rev 255)
+++ trunk/src/check/pseudocode/msc_duplicators.cpp 2009-07-05 16:44:41 UTC (rev 256)
@@ -82,7 +82,9 @@
traverser.traverse(bmsc);
traverser.remove_all_listeners();
MessagesCreatorListener messages_creator(this);
+ TimeRelationCreatorListener time_creator(this);
traverser.add_white_event_found_listener(&messages_creator);
+ traverser.add_white_event_found_listener(&time_creator);
traverser.traverse(bmsc);
for(instances = bmsc->get_instances().begin();
@@ -247,6 +249,32 @@
////////////////////////////////////////////////////////////////////////
+TimeRelationCreatorListener::TimeRelationCreatorListener(BMscDuplicator* duplicator):
+m_duplicator(duplicator)
+{
+
+}
+
+void TimeRelationCreatorListener::on_white_event_found(Event* e)
+{
+ TimeRelationEventPtrList relations = e->get_time_relations();
+ TimeRelationEventPtrList::iterator it;
+ for(it=relations.begin();it!=relations.end();it++)
+ {
+ if((*it)->get_event_a()!=e)
+ continue;
+
+ Event* a_copy = m_duplicator->get_event_copy((*it)->get_event_a());
+ Event* b_copy = m_duplicator->get_event_copy((*it)->get_event_b());
+ TimeRelationEventPtr relation=TimeRelationEvent::create(a_copy,b_copy,(*it)->get_interval_set(),(*it).get());
+ m_duplicator->set_copy((*it).get(),relation.get());
+
+ }
+
+}
+
+////////////////////////////////////////////////////////////////////////
+
GraphCreatorListener::GraphCreatorListener(BMscGraphDuplicator* duplicator, DFSBMscGraphTraverser* traverser,HMsc* hmsc):
m_duplicator(duplicator),m_traverser(traverser),m_hmsc(hmsc)
{
Modified: trunk/src/check/pseudocode/msc_duplicators.h
===================================================================
--- trunk/src/check/pseudocode/msc_duplicators.h 2009-06-21 21:12:06 UTC (rev 255)
+++ trunk/src/check/pseudocode/msc_duplicators.h 2009-07-05 16:44:41 UTC (rev 256)
@@ -97,6 +97,20 @@
};
+class TimeRelationCreatorListener:public WhiteEventFoundListener
+{
+protected:
+
+ BMscDuplicator* m_duplicator;
+
+public:
+
+ TimeRelationCreatorListener(BMscDuplicator* duplicator);
+
+ void on_white_event_found(Event* e);
+
+};
+
/**
* \brief Duplicates BMsc
*
Added: trunk/src/check/time/CMakeLists.txt
===================================================================
--- trunk/src/check/time/CMakeLists.txt (rev 0)
+++ trunk/src/check/time/CMakeLists.txt 2009-07-05 16:44:41 UTC (rev 256)
@@ -0,0 +1,15 @@
+ADD_LIBRARY(sctimeconsistency SHARED
+ time_consistency.cpp
+ time_consistency.h
+ bmsc_tightening.h
+ hmsc_all_paths.cpp
+ hmsc_all_paths.h
+ hmsc_tighten.h
+ hmsc_tighten.cpp
+)
+
+TARGET_LINK_LIBRARIES(sctimeconsistency
+ scmsc
+ sctime
+)
+
Added: trunk/src/check/time/bmsc_tightening.h
===================================================================
--- trunk/src/check/time/bmsc_tightening.h (rev 0)
+++ trunk/src/check/time/bmsc_tightening.h 2009-07-05 16:44:41 UTC (rev 256)
@@ -0,0 +1,259 @@
+#ifndef _TIME_TIGHTENING_H_
+#define _TIME_TIGHTENING_H_
+#include "time_consistency.h"
+
+typedef std::pair<Event*,Event*> EventPair;
+typedef std::list<EventPair> EventPairsList;
+typedef std::pair<MscTimeIntervalSetD,IntervalSetMatrix> ConstMatrixPair;
+typedef boost::intrusive_ptr<BmscMatrixConverter*> BmscMatrixConverterPtr;
+
+class TightenBMsc
+{
+private:
+ BmscMatrixConverter m_converter;
+ BMscPtr m_bmsc;
+ IntervalSetMatrix m_matrix;
+
+ EventPList m_mins;
+ EventPList m_maxs;
+
+ int get_number(Event* e)
+ {
+ return m_converter.get_number(e);
+ }
+
+ int is_leq(Event* e,Event* f)
+ {
+ return m_converter.is_leq(e,f);
+ }
+
+ EventPVector get_events()
+ {
+ return m_converter.get_events();
+ }
+
+public:
+
+ TightenBMsc(BMscPtr bmsc):m_bmsc(bmsc)
+ {
+ m_matrix = m_converter.compute_matrix(bmsc);
+ m_mins = find_minimal_events();
+ m_maxs = find_maximal_events();
+ }
+
+ 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++)
+ {
+ bool is_minimal = true;
+ for(it_b=events.begin();it_b!=events.end();it_b++)
+ {
+ if(it_b != it && is_leq(*it_b,*it))
+ {
+ is_minimal =false;
+ break;
+ }
+
+ }
+ if(is_minimal)
+ {
+ minimals.push_back(*it);
+ }
+ }
+ return minimals;
+ }
+
+ 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;
+ }
+
+ }
+ if(is_maximal)
+ {
+ maximals.push_back(*it);
+ }
+ }
+ return maximals;
+ }
+
+ ConstMatrixPair max_tightener(
+ IntervalSetMatrix t_matrix,
+ MscTimeIntervalSetD i
+ )
+ {
+ MscTimeIntervalSetD z;
+ z.insert(MscTimeIntervalD(0,0));
+
+ EventPairsList pairs;
+
+ EventPList::iterator it_min;
+ EventPList::iterator it_max;
+
+ for(it_min=m_mins.begin();it_min!=m_mins.end();it_min++)
+ {
+ for(it_max=m_maxs.begin();it_max!=m_maxs.end();it_max++)
+ {
+ z = MscTimeIntervalSetD::components_max(z,
+ t_matrix(get_number(*it_min),get_number(*it_max)));
+ if(!MscTimeIntervalSetD::set_intersection(i,
+ t_matrix(get_number(*it_min),get_number(*it_max))).is_empty())
+ pairs.push_back(std::make_pair(*it_min,*it_max));
+ }
+ }
+
+ //TODO check WeaklyCommConnected
+ 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(z,t_matrix);
+ }
+
+ static MscTimeIntervalSetD tight(BMscPtr bmsc,MscTimeIntervalSetD i)
+ {
+ TightenBMsc tightening(bmsc);
+ ConstMatrixPair pair = tightening.tighten_msc(i);
+ tightening.modificate(pair.second);
+ return pair.first;
+ }
+
+ void modificate(IntervalSetMatrix matrix)
+ {
+ m_converter.modificate(matrix);
+ }
+
+
+
+ ConstMatrixPair tighten_msc(MscTimeIntervalSetD i)
+ {
+
+ MscSolveTCSP solve;
+ IntervalSetMatrix s;
+ IntervalSetMatrix t;
+ ConstMatrixPair pair;
+
+ t = m_matrix;
+
+ do {
+ s = t;
+ t = solve.solve(t); // TODO complete
+ pair = max_tightener(t,i);
+ i = MscTimeIntervalSetD::set_intersection(i,pair.first);
+
+ } while (!MatrixFunc::is_equal(s,t));
+
+ pair.first = i;
+ return pair;
+ }
+
+}; // class TightenBMsc
+
+
+#endif // _TIME_TIGHTENING_H_
Added: trunk/src/check/time/hmsc_all_paths.cpp
===================================================================
--- trunk/src/check/time/hmsc_all_paths.cpp (rev 0)
+++ trunk/src/check/time/hmsc_all_paths.cpp 2009-07-05 16:44:41 UTC (rev 256)
@@ -0,0 +1,2 @@
+#include "check/time/hmsc_all_paths.h"
+
Added: trunk/src/check/time/hmsc_all_paths.h
===================================================================
--- trunk/src/check/time/hmsc_all_paths.h (rev 0)
+++ trunk/src/check/time/hmsc_all_paths.h 2009-07-05 16:44:41 UTC (rev 256)
@@ -0,0 +1,119 @@
+#ifndef _AllPaths_
+#define _AllPaths_
+
+#include "check/time/time_consistency.h"
+
+
+typedef std::pair<std::list<HMscNodePtr>,bool> HMscPath;
+typedef std::pair<std::list<HMscPath>,bool> HMscAllPaths;
+class AllPaths
+{
+private:
+ HMscNodePtrSet m_nodes_set;
+ std::string m_number;
+ bool m_contains_cycle_globally;
+ TimeRelationRefNodePtr m_relation;
+ HMscPtr m_hmsc;
+ std::list<HMscPath> m_paths;
+public:
+ AllPaths(HMscPtr hmsc, TimeRelationRefNodePtr relation,
+ const std::string& number="AllPathAlg"):m_hmsc(hmsc),m_relation(relation),m_number(number)
+ {
+
+ }
+
+ ~AllPaths()
+ {
+ cleanup_attributes();
+ }
+
+ void set_number(HMscNodePtr e,int number)
+ {
+ return e->set_attribute<int>(m_number,number);
+ }
+
+ int get_number(HMscNodePtr e)
+ {
+ return e->get_attribute<int>(m_number,0);
+ }
+
+ void cleanup_attributes()
+ {
+ HMscNodePtrSet::iterator node;
+ for(node=m_nodes_set.begin();node!=m_nodes_set.end();node++)
+ (*node)->remove_attribute<int>(m_number);
+ }
+
+
+ static HMscAllPaths get_all_paths(HMscPtr hmsc, TimeRelationRefNodePtr relation)
+ {
+ AllPaths allpaths(hmsc,relation);
+ return allpaths.get_set_of_paths();
+ }
+
+ HMscAllPaths get_set_of_paths()
+ {
+
+ m_paths.clear();
+ m_contains_cycle_globally=false;
+ bool contains_cycle_locally = false;
+ std::list<HMscNodePtr> path_prefix;
+ m_nodes_set = m_hmsc->get_nodes();
+
+ HMscNodePtrSet::iterator it;
+ for(it=m_nodes_set.begin();it!=m_nodes_set.end();it++)
+ set_number(*it,0);
+
+ // TODO check origin of relation
+ all_paths(m_relation->get_ref_node_a(),path_prefix,contains_cycle_locally);
+
+ return std::make_pair(m_paths,m_contains_cycle_globally);
+ }
+
+
+ void all_paths(HMscNodePtr node, std::list<HMscNodePtr> path_prefix, bool contains_cycle_locally)
+ {
+
+ path_prefix.push_back(node);
+ if(node == m_relation->get_ref_node_b())
+ {
+ m_paths.push_back(std::make_pair(path_prefix,contains_cycle_locally));
+ }
+
+ set_number(node,get_number(node)+1);
+ PredecessorNode * pre;
+ pre = dynamic_cast<PredecessorNode*>(node.get());
+
+ if(pre == NULL)
+ {
+ path_prefix.pop_back();
+ set_number(node, 0);
+ return;
+ }
+
+
+ NodeRelationPtrSet set_succ = pre->get_successors();
+ NodeRelationPtrSet::const_iterator rel;
+ for(rel=set_succ.begin(); rel!=set_succ.end();rel++)
+ {
+ const NodeRelationPtr& node_relation = *rel;
+ HMscNodePtr new_node(dynamic_cast<HMscNode*>(node_relation.get()->get_successor()));
+ if(get_number(new_node)<=1)
+ {
+ bool contains_cycle_locally_new = contains_cycle_locally;
+ if(get_number(new_node)==1)
+ {
+ contains_cycle_locally_new = true;
+ m_contains_cycle_globally = true;
+ }
+ all_paths(new_node,path_prefix, contains_cycle_locally_new);
+
+ }
+
+ }
+ path_prefix.pop_back();
+ set_number(node, get_number(node)-1);
+ return;
+ }
+};
+#endif
Added: trunk/src/check/time/hmsc_tighten.cpp
===================================================================
--- trunk/src/check/time/hmsc_tighten.cpp (rev 0)
+++ trunk/src/check/time/hmsc_tighten.cpp 2009-07-05 16:44:41 UTC (rev 256)
@@ -0,0 +1 @@
+#include "check/time/hmsc_tighten.h"
Added: trunk/src/check/time/hmsc_tighten.h
===================================================================
--- trunk/src/check/time/hmsc_tighten.h (rev 0)
+++ trunk/src/check/time/hmsc_tighten.h 2009-07-05 16:44:41 UTC (rev 256)
@@ -0,0 +1,296 @@
+#include "check/time/time_consistency.h"
+#include "check/pseudocode/msc_duplicators.h"
+#include "check/time/hmsc_all_paths.h"
+#include "check/time/bmsc_tightening.h"
+
+//typedef std::pair<std::list<HMscNodePtr>,bool> HMscPath;
+//typedef std::pair<std::list<HMscPath>,bool> HMscAllPaths;
+typedef std::list<HMscNodePtr> HMscNodePtrList;
+
+class TightenSetOfPaths
+{
+private:
+// std::set<BMscPtr> m_bmsc_on_path_set;
+// std::set<BMscPtr> m_bmsc_all_set;
+ std::set<BMscPtr> m_bmsc_copy1;
+ std::set<BMscPtr> m_bmsc_copy2;
+
+ std::list<BMscPtr> m_msc_list;
+ std::list<TimeRelationRefNodePtr> m_constr;
+ IntervalSetMatrix m_t;
+ BMscPtr m_msc;
+ MscTimeIntervalSetD i_prime_prime;
+public:
+// HMscAllPaths
+/*
+ BMscPtr return_inner_bmsc(HmscNodePtr node)
+ {
+
+ }
+*/
+ MscTimeIntervalSetD tighten(HMscAllPaths paths, MscTimeIntervalSetD i, HMscPtr hmsc)
+ {
+
+
+ //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());
+ BMscPtr bmsc_ptr = ref_node->get_bmsc();
+ m_bmsc_copy1.insert(bmsc_duplicator_1.duplicate_bmsc(bmsc_ptr)); //in case that on paths are reference nodes only
+ }
+ }
+
+ 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++)
+ {
+
+ if(!(*it).second)
+ {
+ m_msc_list.clear();
+ m_constr.clear();
+ HMscNodePtrList::iterator n_path;
+ HMscNodePtrList::iterator n_path_previous;
+ 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_relation_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
+ {
+ has_constraint = true;
+ break;
+ }
+
+ }
+ if(has_constraint)
+ {
+ m_constr.push_back(*it_c);
+ m_msc_list.push_back(m_msc);
+
+ 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;
+
+// m_msc = concatenate(m_msc, msc_tmp); //TODO:concatenation
+ }
+
+
+
+ }
+
+
+
+ ConstMatrixPair pair;
+ if(m_msc_list.empty())
+ {
+
+ TightenBMsc tighten_msc(m_msc);
+ pair = tighten_msc.tighten_msc(i);
+ 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
+ i_prime_prime_prime = tighten_msg_path(m_msc_list,m_constr,i);
+
+ i_prime_prime = MscTimeIntervalSetD::set_intersection(i_prime_prime,pair.first);
+ }
+
+ }
+
+
+ HMscNodePtrList::iterator path_it;
+
+ 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);
+ 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()));
+ MscTimeIntervalSetD interval_set = MscTimeIntervalSetD::set_union(relation_copy->get_interval_set(), (*tr_it)->get_interval_set());
+ relation_copy->set_interval_set(interval_set);
+
+ }
+
+ }
+
+ //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);
+ std::set<TimeRelationEventPtr>::iterator tr_it;
+ for(tr_it = constraints.begin(); tr_it != constraints.end(); tr_it++)
+ {
+
+ //TODO:upravit
+ TimeRelationEvent* relation_copy = dynamic_cast<TimeRelationEvent*>(bmsc_duplicator_2.get_copy((*tr_it).get()));
+ (*tr_it)->set_interval_set(relation_copy->get_interval_set());
+
+ }
+ }
+ }
+
+
+ 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
+ std::set<TimeRelationEventPtr> constraints;
+// constraints = get_all_constraints(*b_it);
+ std::set<TimeRelationEventPtr>::iterator tr_it2;
+
+ for(tr_it2 = constraints.begin(); tr_it2 != constraints.end(); tr_it2++)
+ {
+ TimeRelationEvent* relation_copy = dynamic_cast<TimeRelationEvent*>((*tr_it2)->get_original());
+
+ //TODO:upravit
+ relation_copy->set_interval_set((*tr_it2)->get_interval_set());
+
+ }
+
+ }
+
+return i_prime_prime;
+
+ }
+
+ MscTimeIntervalSetD tighten_msg_path(std::list<BMscPtr> list_bmsc,std::list<TimeRelationRefNodePtr> constr,MscTimeIntervalSetD interval)
+ {
+ MscTimeIntervalSetD tmp_interval(interval);
+ std::vector<MscTimeIntervalSetD> durations;
+ for(int i=0;i<list_bmsc.size();i++)
+ {
+ MscTimeIntervalSetD tmp;
+
+ tmp.insert(MscTimeIntervalD(0,D::infinity()));
+ durations.push_back(tmp);
+ }
+ MscTimeIntervalSetD s_interval;
+ do {
+ s_interval = tmp_interval;
+ std::list<BMscPtr>::iterator bmsc;
+ int i=0;
+ for(bmsc=list_bmsc.begin();bmsc!=list_bmsc.end();bmsc++,i++)
+ {
+ MscTimeIntervalSetD tmp_i=tmp_interval;
+ for(int 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(int 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(int j=0;j<list_bmsc.size();j++)
+ {
+ tmp = tmp + durations[j];
+ }
+
+ std::list<TimeRelationRefNodePtr>::iterator c_it;
+ for(c_it=constr.begin();c_it!=constr.end();c_it++)
+ {
+ MscTimeIntervalSetD uu = (*c_it)->get_interval_set();
+ tmp = uu + tmp;
+ }
+
+ tmp_interval = MscTimeIntervalSetD::set_intersection(tmp_interval,tmp);
+
+
+
+ } while(s_interval!=tmp_interval);
+
+ return tmp_interval;
+ }
+
+};
+
Added: trunk/src/check/time/time_consistency.cpp
===================================================================
--- trunk/src/check/time/time_consistency.cpp (rev 0)
+++ trunk/src/check/time/time_consistency.cpp 2009-07-05 16:44:41 UTC (rev 256)
@@ -0,0 +1,314 @@
+#include "check/time/time_consistency.h"
+
+const IntervalMatrix FloydWarshall::tight(const IntervalMatrix& matrix)
+throw(MscTimeInconsistencyException)
+{
+ IntervalMatrix copy(matrix);
+ for(unsigned k=0; k < matrix.size1(); k++)
+ {
+ for(unsigned i=0; i < matrix.size1(); i++)
+ {
+ for(unsigned j=0; j < matrix.size1(); j++)
+ {
+ copy(i,j) = MscTimeIntervalD::interval_intersection(copy(i,j), \
+ copy(i,k)+copy(k,j));
+ if(!copy(i,j).is_valid())
+ {
+ DEBUG(copy(i,j));
+ throw MscTimeInconsistencyException();
+ }
+ }
+ }
+ }
+ return copy;
+}
+
+
+bool FloydWarshall::check_consistency(const IntervalMatrix& matrix)
+{
+ IntervalMatrix copy(matrix);
+ for(unsigned k=0; k < matrix.size1(); k++)
+ {
+ for(unsigned i=0; i < matrix.size1(); i++)
+ {
+ for(unsigned j=0; j < matrix.size1(); j++)
+ {
+ copy(i,j) = MscTimeIntervalD::interval_intersection(copy(i,j), \
+ copy(i,k)+copy(k,j));
+ if(!copy(i,j).is_valid())
+ {
+ return false;
+ }
+ }
+ }
+ }
+ return true;
+}
+/////////////////////////////////////////////////////////////////
+void MscSolveTCSP::forward(IntervalMatrix matrix,int i, int j)
+{
+ int new_j;
+ int new_i;
+ DEBUG_(i,j);
+ if(matrix.size1()==i+1 && matrix.size1()== j+1)
+ {
+ IntervalMatrix tmp = tightener->tight(matrix);
+ for(unsigned g=0;g<matrix.size1();g++)
+ for(unsigned h=0;h<matrix.size2();h++)
+ m_result_matrix(g,h).insert(tmp(g,h));
+
+ go_back(matrix,i,j);
+ }
+ else
+ {
+ std::list<MscTimeIntervalD> interval_list;
+ if(j+1==matrix.size1())
+ {
+ new_i = i+1;
+ new_j = new_i;
+ }
+ else
+ {
+ new_j = j+1;
+ new_i =i;
+ }
+ IntervalList list = m_solve_matrix(new_i,new_j).get_set();
+ IntervalList::iterator it;
+ for(it=list.begin();it!=list.end();it++)
+ {
+ MatrixFunc::fill_matrix(matrix,*it,(unsigned)new_i,(unsigned)new_j);
+ if(con_checker->check_consistency(matrix))
+ m_to_go_matrix(new_i,new_j).insert(*it);
+
+ }
+ DEBUG(m_to_go_matrix);
+ IntervalList& to_go = m_to_go_matrix(new_i,new_j).get_set();
+ if(!to_go.empty())
+ {
+ DEBUG(m_to_go_matrix(new_i,new_j).get_set().size());
+ MscTimeIntervalD tmp = to_go.front();
+ to_go.pop_front();
+ DEBUG(m_to_go_matrix(new_i,new_j).get_set().size());
+ DEBUG(to_go.size());
+
+
+ matrix(new_i,new_j) = tmp;
+ matrix(new_j,new_i) = MscTimeIntervalD::interval_inverse(tmp);
+
+ forward(matrix,new_i,new_j);
+ }
+ else
+ {
+ 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);
+ }
+ }
+}
+
+void MscSolveTCSP::go_back(IntervalMatrix matrix,int i,int j)
+{
+ DEBUG_(i,j);
+ if(i==-1){
+ DEBUG(m_result_matrix);
+ return;
+ }
+ IntervalList& to_go = m_to_go_matrix(i,j).get_set();
+ if(!to_go.empty())
+ {
+ DEBUG(m_to_go_matrix(i,j).get_set().size());
+ MscTimeIntervalD tmp = to_go.front();
+ to_go.pop_front();
+ DEBUG(m_to_go_matrix(i,j).get_set().size());
+ DEBUG(to_go.size());
+
+ matrix(i,j) = tmp;
+ matrix(j,i) = MscTimeIntervalD::interval_inverse(tmp);
+ forward(matrix,i,j);
+ }
+ else
+ {
+ matrix(i,j) = MscTimeIntervalD(-D::infinity(),D::infinity());
+ matrix(j,i) = MscTimeIntervalD(-D::infinity(),D::infinity());
+ if(i==j)
+ {
+ i--;
+ j = matrix.size1()-1;
+ }
+ else
+ {
+ j--;
+ }
+ go_back(matrix,i,j);
+ }
+}
+
+void MscSolveTCSP::init(unsigned size)
+{
+ m_result_matrix.resize(size,size);
+ m_to_go_matrix.resize(size,size);
+
+ for(unsigned i=0;i<size;i++)
+ {
+ for(unsigned j=0;j<size;j++)
+ {
+ m_result_matrix(i,j)=MscTimeIntervalDSet();
+ m_to_go_matrix(i,j)=MscTimeIntervalDSet();
+ }
+ }
+}
+
+IntervalSetMatrix MscSolveTCSP::solve(const IntervalSetMatrix& m)
+{
+ init(m.size1());
+ m_solve_matrix=m;
+
+ IntervalMatrix matrix(m_solve_matrix.size1(),m_solve_matrix.size2());
+ for(unsigned i=0;i<m_solve_matrix.size1();i++)
+ {
+ for(unsigned j=0;j<m_solve_matrix.size2();j++){
+ if(i==j)
+ matrix(i,j) = MscTimeIntervalD(0,0);
+ else
+ matrix(i,j)=MscTimeIntervalD(-D::infinity(),D::infinity()); //TODO:infinity
+
+ }
+ }
+ DEBUG(m_solve_matrix);
+ forward(matrix,0,-1);
+
+ return m_result_matrix;
+}
+
+//////////////////////////////////////////////////////////////////
+
+void BmscMatrixConverter::get_first_area_events(EventArea* area,Event* e)
+{
+ if(!area)
+ return;
+
+ StrictOrderArea* strict = dynamic_cast<StrictOrderArea*>(area);
+ if(strict)
+ {
+ if(strict->is_empty())
+ get_first_area_events(strict->get_next().get(),e);
+ else
+ m_succs[e].insert(strict->get_first().get());
+ }
+ else
+ {
+ CoregionArea* coregion = dynamic_cast<CoregionArea*>(area);
+ if(coregion->is_empty())
+ get_first_area_events(coregion->get_next().get(),e);
+ else
+ {
+ const CoregionEventPSet& minimals = coregion->get_minimal_events();
+ CoregionEventPSet::const_iterator min;
+ for(min=minimals.begin(); min!=minimals.end(); min++)
+ m_succs[e].insert(*min);
+ }
+ }
+}
+
+void BmscMatrixConverter::get_strict_successors(StrictEvent *e)
+{
+ if(e->get_successor().get())
+ m_succs[e].insert(e->get_successor().get());
+ else
+ get_first_area_events(e->get_area()->get_next().get(),e);
+}
+
+
+void BmscMatrixConverter::get_coregion_successors(CoregionEvent *e)
+{
+ if(e->get_successors().size()!=0)
+ {
+ const CoregEventRelPtrSet& successors = e->get_successors();
+ CoregEventRelPtrSet::const_iterator succ;
+ for(succ=successors.begin(); succ!=successors.end(); succ++)
+ {
+ m_succs[e].insert((*succ)->get_successor());
+ }
+ }
+ else
+ get_first_area_events(e->get_area()->get_next().get(),e);
+}
+
+void BmscMatrixConverter::get_successors(Event *e)
+{
+ StrictEvent* strict = dynamic_cast<StrictEvent*>(e);
+ if(strict)
+ {
+ get_strict_successors(strict);
+ }
+ else
+ {
+ CoregionEvent* coregion = dynamic_cast<CoregionEvent*>(e);
+ get_coregion_successors(coregion);
+ }
+ // if its send event
+ if(e->is_send() && (e->get_matching_event()!= NULL))
+ {
+ m_succs[e].insert(e->get_matching_event());
+ }
+
+}
+
+void BmscMatrixConverter::build_up_matrix()
+{
+ init_visual();
+ m_matrix.resize(m_events.size(),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));
+ }
+ else
+ {
+ m_matrix(i,j)=MscTimeIntervalSetD();
+ m_matrix(i,j).insert(MscTimeIntervalD(-D::infinity(),D::infinity()));
+ }
+ }
+ }
+
+ EventPVector::iterator e_v;
+ EventPSet::iterator e_m;
+
+ for(e_v=m_events.begin();e_v!=m_events.end();e_v++)
+ {
+ EventPSet& set = m_succs[*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));
+ }
+
+ TimeRelationEventPtrList::iterator it;
+ TimeRelationEventPtrList relations = (*e_v)->get_time_relations();
+
+ for(it=relations.begin();it!=relations.end();it++)
+ {
+ if(closure_initiator.get_visual_closure((*it)->get_event_a())[
+ closure_initiator.get_topology_index((*it)->get_event_b())])
+ {
+ MatrixFunc::fill_matrix(m_matrix,(*it)->get_interval_set(), \
+ get_number((*it)->get_event_a()),get_number((*it)->get_event_b()));
+ }
+ else
+ {
+ MatrixFunc::fill_matrix(m_matrix,(*it)->get_interval_set(),\
+ get_number((*it)->get_event_b()),get_number((*it)->get_event_a()));
+ }
+ }
+ }
+}
+///////////////////////////////////////////////////////////////////////
+
+
+
Added: trunk/src/check/time/time_consistency.h
===================================================================
--- trunk/src/check/time/time_consistency.h (rev 0)
+++ trunk/src/check/time/time_consistency.h 2009-07-05 16:44:41 UTC (rev 256)
@@ -0,0 +1,328 @@
+#ifndef TIME_H_CON
+#define TIME_H_CON
+#include "data/time.h"
+#include "data/msc.h"
+#include "data/dfs_events_traverser.h"
+#include "check/pseudocode/visual_closure_initiator.h"
+#include <limits>
+#include <set>
+#include <list>
+#include <vector>
+#include <string>
+#include <exception>
+
+#ifdef _DEBUG
+#include<iostream>
+#define DEBUG(x) std::cerr << "DB: " << __FILE__ << ":" << __LINE__ << " " \
+<< __FUNCTION__ << "() " << #x << " = " << (x) << std::endl
+#define DEBUG_(x,y) std::cerr << "DB: " << __FILE__ << ":" << __LINE__ \
+<< " " << __FUNCTION__ << "() " \
+<< #x << " = " << (x) << " ; " \
+<< #y << " = " << (y) << std::endl
+#else
+#define DEBUG(x)
+#define DEBUG_(x,y)
+#endif
+
+//Boost matix
+#include <boost/numeric/ublas/matrix.hpp>
+#include <boost/numeric/ublas/io.hpp>
+
+class MatrixFunc;
+class MscTimeInconsistencyException;
+
+typedef std::numeric_limits<double> D;
+typedef MscTimeInterval<double> MscTimeIntervalD;
+typedef MscTimeIntervalSet<double> MscTimeIntervalDSet;
+
+typedef boost::numeric::ublas::matrix<MscTimeIntervalD> IntervalMatrix;
+typedef boost::numeric::ublas::matrix<MscTimeIntervalDSet> IntervalSetMatrix;
+typedef std::list<MscTimeIntervalD > IntervalList;
+typedef std::vector<Event*> EventPVector;
+typedef std::set<Event*> EventPSet;
+typedef std::map<Event*,EventPSet> EventPMap;
+
+
+
+class MatrixFunc
+{
+ public:
+ static void fill_matrix(IntervalMatrix& matrix, MscTimeIntervalD c,\
+ unsigned x,unsigned y)
+ {
+ if(x>=matrix.size1()||y>=matrix.size2())
+ throw matrix.size1();
+ matrix(x,y) = c;
+ matrix(y,x) = MscTimeIntervalD::interval_inverse(c);
+ }
+
+ 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);
+ }
+
+ 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));
+ }
+
+ static
+ bool is_equal(
+ IntervalSetMatrix lhs,
+ IntervalSetMatrix rhs)
+ {
+
+ 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;
+ }
+
+ void print_out(IntervalSetMatrix matrix)
+ {
+ 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.width(15); std::cout << std::left << matrix(i,j);
+ }
+ std::cout << std::endl;
+ }
+
+ }
+};
+
+class MscTimeInconsistencyException : public std::exception
+{
+
+public:
+ const char* what()
+ {
+ return "Time Inconsistency";
+ }
+
+};
+
+
+class MscIntervalTightener
+{
+public:
+ virtual const IntervalMatrix tight(const IntervalMatrix&)
+ throw(MscTimeInconsistencyException)=0;
+
+};
+
+class MscIntervalConsistencyCheck
+{
+public:
+ virtual bool check_consistency(const IntervalMatrix&)=0;
+};
+
+
+class FloydWarshall:
+public MscIntervalTightener,
+public MscIntervalConsistencyCheck
+{
+public:
+ FloydWarshall()
+ {}
+
+ const IntervalMatrix tight(const IntervalMatrix&)
+ throw(MscTimeInconsistencyException);
+
+ bool check_consistency(const IntervalMatrix&);
+
+ ~FloydWarshall()
+ {}
+};
+
+class MscSolveTCSP
+{
+private:
+ MscIntervalTightener* tightener;
+ MscIntervalConsistencyCheck* con_checker;
+ IntervalSetMatrix m_solve_matrix;
+ IntervalSetMatrix m_result_matrix;
+ IntervalSetMatrix m_to_go_matrix;
+
+ void forward(IntervalMatrix matrix,int i, int j);
+ void go_back(IntervalMatrix matrix,int i,int j);
+
+ void init(unsigned size);
+
+public:
+ MscSolveTCSP():
+ tightener(new FloydWarshall()),
+ con_checker(new FloydWarshall())
+ {
+ }
+
+ IntervalSetMatrix solve(const IntervalSetMatrix& m);
+};
+
+class BmscMatrixConverter:public WhiteEventFoundListener
+{
+private:
+ // Vector of all events - event <-- matrix number
+ EventPVector m_events;
+ // Map of event and its first successors
+ EventPMap m_succs;
+ // main matrix of Interval Sets
+ IntervalSetMatrix m_matrix;
+ // keeping number of colum/row of event in matrix, event --> matrix
+ std::string m_number;
+
+ VisualClosureInitiator closure_initiator;
+ TopologicalOrderListener topology_listener;
+ DFSEventsTraverser traverser;
+ // bmsc to be converted to matrix
+ BMscPtr m_bmsc;
+
+ void get_first_area_events(EventArea*,Event*);
+
+ void get_strict_successors(StrictEvent*);
+
+ void get_coregion_successors(CoregionEvent*);
+
+ void get_successors(Event *e);
+
+ void pick_up_events()
+ {
+ traverser.add_white_event_found_listener(this);
+ traverser.traverse(m_bmsc);
+ traverser.remove_white_event_found_listeners();
+ }
+
+ void init_visual()
+ {
+
+ traverser.add_event_finished_listener(&topology_listener);
+ traverser.traverse(m_bmsc);
+ EventPVector topology(topology_listener.get_topology().size());
+ topology.assign(
+ topology_listener.get_topology().begin(),
+ topology_listener.get_topology().end()
+ );
+ closure_initiator.initialize(topology);
+ }
+
+ 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:
+
+ int get_number(Event* e)
+ {
+ return e->get_attribute<int>(m_number,-1);
+ }
+
+ const EventPVector get_events()
+ {
+ return m_events;
+ }
+
+ void modificate(IntervalSetMatrix matrix)
+ {
+ for(int i;i<m_events.size();i++)
+ {
+ m_events[i]->clear_time_relations();
+ }
+
+ for(int i;i<matrix.size1();i++)
+ {
+ for(int j;j<matrix.size1();j++)
+ {
+ if((matrix(i,j).get_set().begin())->get_begin_value()<0)
+ continue;
+ TimeRelationEvent::create(m_events[i],m_events[j],matrix(i,j));
+
+ }
+ }
+
+ }
+
+
+ BmscMatrixConverter(const std::string number="bmsc_matrix_converter_number")
+ :m_number(number)
+ {
+ std::cerr << "uuuuu" << std::endl;
+ }
+
+ bool is_leq(Event* a,Event *b)
+ {
+ BoolVector::iterator it;
+ BoolVector vector = closure_initiator.get_visual_closure(a);
+
+ if(closure_initiator.get_visual_closure(a)[
+ closure_initiator.get_topology_index(b)]){
+
+ return true;
+ }
+ else
+ return false;
+ }
+
+ void on_white_event_found(Event* e)
+ {
+ m_events.push_back(e);
+ set_number(e,m_events.size()-1);
+ get_successors(e);
+ }
+
+ IntervalSetMatrix compute_matrix(BMscPtr bmsc)
+ {
+ m_bmsc = bmsc;
+ pick_up_events();
+ build_up_matrix();
+ return m_matrix;
+ }
+
+ IntervalSetMatrix get_matrix()
+ {
+ return m_matrix;
+ }
+
+ ~BmscMatrixConverter()
+ {
+ cleanup_attributes();
+ }
+
+
+}; // end of class BmscMatrixConverter
+
+#endif
Property changes on: trunk/src/data
___________________________________________________________________
Modified: svn:ignore
- CMakeFiles
cmake_install.cmake
CTestTestfile.cmake
*.dir
Makefile
*.vcproj
+ CMakeFiles
cmake_install.cmake
CTestTestfile.cmake
*.dir
Makefile
*.vcproj
.time.h.swp
Modified: trunk/src/data/CMakeLists.txt
===================================================================
--- trunk/src/data/CMakeLists.txt 2009-06-21 21:12:06 UTC (rev 255)
+++ trunk/src/data/CMakeLists.txt 2009-07-05 16:44:41 UTC (rev 256)
@@ -1,3 +1,8 @@
+ADD_LIBRARY(sctime SHARED
+ time.cpp
+ time.h
+)
+
ADD_LIBRARY(scmsc SHARED
export.h
msc_types.cpp
@@ -24,11 +29,13 @@
dfs_instance_events_traverser.h
dfs_bmsc_graph_traverser.cpp
dfs_bmsc_graph_traverser.h
- time.cpp
- time.h
hmsc_reference_checker.h
)
+TARGET_LINK_LIBRARIES(scmsc
+ sctime
+)
+
# build import-export formatters
ADD_SUBDIRECTORY(engmann)
ADD_SUBDIRECTORY(Z120)
Modified: trunk/src/data/msc.cpp
===================================================================
--- trunk/src/data/msc.cpp 2009-06-21 21:12:06 UTC (rev 255)
+++ trunk/src/data/msc.cpp 2009-07-05 16:44:41 UTC (rev 256)
@@ -316,8 +316,9 @@
/////////////////////////////////////////////////////////////////////////////
#ifdef _TIME_H_
-TimeRelation::TimeRelation(const MscTimeIntervalSetD& set):
-m_interval_set(set)
+TimeRelation::TimeRelation(MscTimeIntervalSetD set,TimeRelation* original=NULL):
+m_interval_set(set),MscElementTmpl<TimeRelation>(original)
+
{
}
Modified: trunk/src/data/msc.h
===================================================================
--- trunk/src/data/msc.h 2009-06-21 21:12:06 UTC (rev 255)
+++ trunk/src/data/msc.h 2009-07-05 16:44:41 UTC (rev 256)
@@ -122,6 +122,7 @@
#ifdef _TIME_H_
typedef boost::intrusive_ptr<TimeRelationEvent> TimeRelationEventPtr;
+typedef std::list<TimeRelationEventPtr> TimeRelationEventPtrList;
typedef boost::intrusive_ptr<TimeRelationRefNode> TimeRelationRefNodePtr;
typedef std::set<TimeRelationRefNodePtr> TimeRelationRefNodePtrSet;
typedef MscTimeIntervalSet<double> MscTimeIntervalSetD;
@@ -929,6 +930,16 @@
m_time_relation_set_bottom.erase(m_time_relation_set_bottom.find(relation));
}
+ TimeRelationRefNodePtrSet get_time_relation_top()
+ {
+ return m_time_relation_set_top;
+ }
+
+ TimeRelationRefNodePtrSet get_time_relation_bottom()
+ {
+ return m_time_relation_set_bottom;
+ }
+
#endif
};
@@ -1400,7 +1411,7 @@
#ifdef _TIME_H_
- TimeRelationEventPtr m_time_relation;
+ TimeRelationEventPtrList m_time_relations;
#endif
/**
@@ -1445,15 +1456,27 @@
}
#ifdef _TIME_H_
- void set_time_relation(const TimeRelationEventPtr& relation)
+ void add_time_relation(TimeRelationEventPtr relation)
{
- m_time_relation=relation;
+ m_time_relations.push_back(relation);
}
- TimeRelationEventPtr set_time_relation()
+ void set_time_relations(const TimeRelationEventPtrList& list)
{
- return m_time_relation;
+ m_time_relations=list;
}
+
+ TimeRelationEventPtrList& get_time_relations()
+ {
+ return m_time_relations;
+ }
+
+ void clear_time_relations()
+ {
+ m_time_relations.clear();
+ }
+
+
#endif
/**
@@ -1482,8 +1505,8 @@
{
if(is_matched())
{
- CompleteMessage* complete = get_complete();
- return (is_send()?complete->get_receive_event():complete->get_send_event());
+ CompleteMessage* complete = get_complete();
+ return (is_send()?complete->get_receive_event():complete->get_send_event());
}
return NULL;
}
@@ -2228,19 +2251,19 @@
#ifdef _TIME_H_
class SCMSC_EXPORT TimeRelation:public MscElementTmpl<TimeRelation>
{
-private:
+protected:
std::wstring m_label;
MscTimeIntervalSet<double> m_interval_set;
public:
- TimeRelation(const MscTimeIntervalSetD&);
+ TimeRelation(MscTimeIntervalSetD,TimeRelation*);
TimeRelation(const std::wstring& label=L"");
TimeRelation(const std::wstring&,const MscTimeIntervalSetD);
TimeRelation(TimeRelation*);
- const MscTimeIntervalSet<double>& get_interval_set();
+ const MscTimeIntervalSetD& get_interval_set();
void set_interval_set(const MscTimeIntervalSetD&);
@@ -2256,31 +2279,50 @@
public:
- TimeRelationEvent(Event* a,Event* b,MscTimeIntervalSetD set):
- TimeRelation(set),m_event_origin(a),m_event(b)
+ TimeRelationEvent(Event* a,Event* b,MscTimeIntervalSetD set,TimeRelationEvent* original=NULL):
+ TimeRelation(set,original),m_event_origin(a),m_event(b)
{
-
}
- TimeRelationEvent(TimeRelationEvent* original):
- TimeRelation(original)
+
+ Event* get_event_a()
{
- if(original)
- {
- m_event_origin = original->m_event_origin;
- m_event = original->m_event;
- }
+ return m_event_origin;
}
+ Event* get_event_b()
+ {
+ return m_event;
+ }
+
+
~TimeRelationEvent()
{
}
- void setOrigin(Event* origin)
+ void set_a(Event* a)
{
- m_event_origin = origin;
+ m_event_origin = a;
}
+ void set_b(Event* b)
+ {
+ m_event = b;
+ }
+
+ void set_set(MscTimeIntervalSetD set)
+ {
+ m_interval_set = set;
+ }
+
+ static TimeRelationEventPtr create(Event* a,Event* b,MscTimeIntervalSetD set,TimeRelationEvent* original=NULL)
+ {
+ TimeRelationEventPtr new_relation = new TimeRelationEvent(a,b,set,original);
+ a->add_time_relation(new_relation);
+ b->add_time_relation(new_relation);
+ return new_relation;
+ }
+
};
class SCMSC_EXPORT TimeRelationRefNode:public TimeRelation
@@ -2291,26 +2333,42 @@
public:
- TimeRelationRefNode(ReferenceNode* a,ReferenceNode* b,MscTimeIntervalSet<double> set):
- TimeRelation(set),m_node_origin(a),m_node(b)
+ TimeRelationRefNode(ReferenceNode* a,ReferenceNode* b,MscTimeIntervalSet<double> set,TimeRelationRefNode* original=NULL):
+ TimeRelation(set,original),m_node_origin(a),m_node(b)
{
}
- TimeRelationRefNode(TimeRelationRefNode* original):
- TimeRelation(original)
+ ReferenceNode* get_ref_node_a()
{
- if(original)
- {
- m_node_origin = original->m_node_origin;
- m_node = original->m_node;
+ return m_node_origin;
+ }
- }
+ ReferenceNode* get_ref_node_b()
+ {
+ return m_node;
}
-
+
~TimeRelationRefNode()
{
}
+ static TimeRelationRefNodePtr create(bool bottom_a,ReferenceNode* a,
+ ReferenceNode* b,bool bottom_b,MscTimeIntervalSetD set)
+ {
+ TimeRelationRefNodePtr new_relation = new TimeRelationRefNode(a,b,set);
+ if(bottom_a)
+ a->add_time_relation_bottom(new_relation);
+ else
+ a->add_time_relation_top(new_relation);
+
+ if(bottom_b)
+ b->add_time_relation_bottom(new_relation);
+ else
+ b->add_time_relation_top(new_relation);
+
+ return new_relation;
+ }
+
};
#endif
Modified: trunk/src/data/time.cpp
===================================================================
--- trunk/src/data/time.cpp 2009-06-21 21:12:06 UTC (rev 255)
+++ trunk/src/data/time.cpp 2009-07-05 16:44:41 UTC (rev 256)
@@ -68,65 +68,6 @@
m_value = tmp;
}
-inline bool isNotIn(const char& znak,const std::string& set = "[](),")
-{
- return set.find(znak)==std::string::npos;
-}
-
-inline bool clean(char znak)
-{
- return isdigit(znak)==0&&isNotIn(znak);
-}
-
-template<class T>
-MscTimeInterval<T>::MscTimeInterval(const std::string& interval)
-throw(MscIntervalStringConversionError)
-{
- std::string tmp(interval);
- bool b_closed = true;
- bool e_closed = true;
-
- // remove all unsuitable characters; letting just numbers,commas,brackets
- tmp.erase(remove_if(tmp.begin(),tmp.end(),clean),tmp.end());
-
- // detect starting bracket
- if(isNotIn(tmp[0],std::string("([")))
- throw MscIntervalStringConversionError("No starting bracket [ or (\n");
- if(tmp[0]=='(')
- b_closed = false;
- // erase it
- tmp.erase(tmp.begin());
-
- //detect ending bracket
- if(isNotIn(tmp[tmp.length()-1],")]"))
- throw MscIntervalStringConversionError("No ending bracket ) or ]\n");
- if(tmp[tmp.length()-1]==')')
- e_closed = false;
- // erase it
- tmp.erase(tmp.end()-1);
-
-
- std::string b(tmp);
- std::string e(tmp);
-
- size_t comma_pos= tmp.find(',');
- if(comma_pos!=std::string::npos)
- {
- e = std::string(tmp.substr(comma_pos+1));
- tmp.erase(comma_pos); // erase all from comma including comma
- b = std::string(tmp);
- }
-
- MscIntervalCouple<T> begin(b,b_closed);
- MscIntervalCouple<T> end(e,e_closed);
-
- m_begin = begin;
- m_end = end;
-}
-template class MscTimeInterval<double>;
-template class MscTimeInterval<DecScaled>;
-
-
//template MscTimeInterval<double>::MscTimeInterval();
//template MscTimeInterval<DecScaled>::MscTimeInterval();
// $Id$
Modified: trunk/src/data/time.h
===================================================================
--- trunk/src/data/time.h 2009-06-21 21:12:06 UTC (rev 255)
+++ trunk/src/data/time.h 2009-07-05 16:44:41 UTC (rev 256)
@@ -62,6 +62,17 @@
return t;
}
+// string to number helping functions
+inline bool isNotIn(const char& znak,const std::string& set = "[](),")
+{
+ return set.find(znak)==std::string::npos;
+}
+
+inline bool clean(char znak)
+{
+ return isdigit(znak)==0&&isNotIn(znak);
+}
+
class MscIntervalCoupleUncomparable:public std::exception
{
public:
@@ -477,9 +488,51 @@
{
}
- MscTimeInterval(const std::string& interval) throw(MscIntervalStringConversionError);
+ MscTimeInterval(const std::string& interval)
+ throw(MscIntervalStringConversionError)
+ {
+ std::string tmp(interval);
+ bool b_closed = true;
+ bool e_closed = true;
+ // remove all unsuitable characters; letting just numbers,commas,brackets
+ tmp.erase(remove_if(tmp.begin(),tmp.end(),clean),tmp.end());
+
+ // detect starting bracket
+ if(isNotIn(tmp[0],std::string("([")))
+ throw MscIntervalStringConversionError("No starting bracket [ or (\n");
+ if(tmp[0]=='(')
+ b_closed = false;
+ // erase it
+ tmp.erase(tmp.begin());
+
+ //detect ending bracket
+ if(isNotIn(tmp[tmp.length()-1],")]"))
+ throw MscIntervalStringConversionError("No ending bracket ) or ]\n");
+ if(tmp[tmp.length()-1]==')')
+ e_closed = false;
+ // erase it
+ tmp.erase(tmp.end()-1);
+
+ std::string b(tmp);
+ std::string e(tmp);
+
+ size_t comma_pos= tmp.find(',');
+ if(comma_pos!=std::string::npos)
+ {
+ e = std::string(tmp.substr(comma_pos+1));
+ tmp.erase(comma_pos); // erase all from comma including comma
+ b = std::string(tmp);
+ }
+
+ MscIntervalCouple<T> begin(b,b_closed);
+ MscIntervalCouple<T> end(e,e_closed);
+
+ m_begin = begin;
+ m_end = end;
+ }
+
MscIntervalCouple<T> get_begin() const
{
return m_begin;
@@ -633,9 +686,16 @@
* @warning returned interval does have to be valid, is_valid() may return false, CHECK FOR VALIDITY
*/
-static MscTimeInterval interval_intersection(MscTimeInterval& left,
- MscTimeInterval& right)
+
+static MscTimeInterval interval_inverse(MscTimeInterval& inter)
{
+ return MscTimeInterval(inter.get_end_closed(),-inter.get_end_value(), \
+ -inter.get_begin_value(), inter.get_begin_closed());
+}
+
+static MscTimeInterval interval_intersection(MscTimeInterval left,
+ MscTimeInterval right)
+{
MscIntervalCouple<T> begin;
try
{
@@ -906,7 +966,7 @@
return tmp;
}
- const MscTimeIntervalSet<T> operator+(MscTimeIntervalSet<T>& set)
+ const MscTimeIntervalSet operator+(MscTimeIntervalSet& set)
{
MscTimeIntervalSet<T> new_set;
@@ -923,7 +983,7 @@
return new_set;
}
- const MscTimeIntervalSet<T> operator-(MscTimeIntervalSet<T>& set)
+ MscTimeIntervalSet operator-(MscTimeIntervalSet set)
{
MscTimeIntervalSet<T> new_set;
@@ -940,7 +1000,7 @@
return new_set;
}
- const MscTimeIntervalSet<T>& operator=(const MscTimeIntervalSet<T>& set)
+ const MscTimeIntervalSet& operator=(const MscTimeIntervalSet& set)
{
if(this==&set)
return *this;
@@ -955,14 +1015,30 @@
return set.m_set==this->m_set;
}
+ const bool operator!=(const MscTimeIntervalSet& set)
+ {
+ if(this==&set)
+ return false;
+ return set.m_set!=this->m_set;
+ }
+
void clear(){
m_set.clear();
}
+ IntervalList& get_set()
+ {
+ return m_set;
+ }
- static MscTimeIntervalSet<T> set_union(MscTimeIntervalSet<T> left,
- MscTimeIntervalSet<T> right)
+ bool is_empty()
{
+ return m_set.empty();
+ }
+
+ static MscTimeIntervalSet<T> set_union(MscTimeIntervalSet left,
+ MscTimeIntervalSet right)
+ {
MscTimeIntervalSet<T> new_set;
new_set.m_set = left.m_set;
for(typename IntervalList::iterator it = right.m_set.begin();
@@ -973,8 +1049,8 @@
return new_set;
}
- static MscTimeIntervalSet<T> set_intersection(MscTimeIntervalSet<T> left,
- MscTimeIntervalSet<T> right)
+ static MscTimeIntervalSet<T> set_intersection(MscTimeIntervalSet left,
+ MscTimeIntervalSet right)
{
MscTimeIntervalSet<T> new_set;
for(typename IntervalList::iterator it = left.m_set.begin();
@@ -987,13 +1063,15 @@
tmp = MscTimeInterval<T>::interval_intersection(*it,*it2);
if(tmp.is_valid())
new_set.insert(tmp);
+ else
+ std::cerr<< "not valid " << tmp << std::endl;
}
}
return new_set;
}
- static MscTimeIntervalSet<T> components_max(MscTimeIntervalSet<T> left,
- MscTimeIntervalSet<T> right)
+ static MscTimeIntervalSet<T> components_max(MscTimeIntervalSet left,
+ MscTimeIntervalSet right)
{
MscTimeIntervalSet<T> new_set;
for(typename IntervalList::iterator it = left.m_set.begin();
@@ -1011,6 +1089,19 @@
return new_set;
}
+ static MscTimeIntervalSet interval_inverse(MscTimeIntervalSet inter)
+ {
+ MscTimeIntervalSet<T> new_set;
+ for(typename IntervalList::iterator it = inter.m_set.begin();
+ it != inter.m_set.end(); it++)
+ {
+ new_set.insert(MscTimeInterval<T>::interval_inverse(*it));
+ }
+
+ return new_set;
+ }
+
+
friend std::ostream&
operator<<(std::ostream& os, const MscTimeIntervalSet<T> interval)
{
Modified: trunk/tests/CMakeLists.txt
===================================================================
--- trunk/tests/CMakeLists.txt 2009-06-21 21:12:06 UTC (rev 255)
+++ trunk/tests/CMakeLists.txt 2009-07-05 16:44:41 UTC (rev 256)
@@ -102,6 +102,7 @@
ADD_CHECKER_TEST(scorder "FIFO" z120_test00.mpr 1)
ADD_CHECKER_TEST(scorder "Acyclic" z120_test00.mpr 1)
ADD_CHECKER_TEST(scrace "Race Free" z120_test00.mpr 0)
+
ENDIF(ANTLR_FOUND)
ADD_EXECUTABLE(decimal_test
@@ -117,11 +118,81 @@
ADD_EXECUTABLE(interval_string
interval_string.cpp
)
+TARGET_LINK_LIBRARIES(interval_string
+ sctime
+)
-
ADD_TEST(decimal_test ${EXECUTABLE_OUTPUT_PATH}/decimal_test)
ADD_TEST(interval_test ${EXECUTABLE_OUTPUT_PATH}/interval_test)
ADD_TEST(interval_set_test ${EXECUTABLE_OUTPUT_PATH}/interval_set_test)
ADD_TEST(interval_string ${EXECUTABLE_OUTPUT_PATH}/interval_string)
+ADD_EXECUTABLE(bmsc_matrix_converter_test
+ bmsc_matrix_converter_test.cpp
+)
+
+TARGET_LINK_LIBRARIES(bmsc_matrix_converter_test
+ scmsc
+ sctimeconsistency
+ scpseudocode
+)
+
+ADD_EXECUTABLE(incon_test
+ incon_test.cpp
+)
+
+TARGET_LINK_LIBRARIES(incon_test
+ scmsc
+ sctimeconsistency
+ scpseudocode
+)
+
+ADD_EXECUTABLE(tighten_msc_test
+ tighten_msc_test.cpp
+)
+
+TARGET_LINK_LIBRARIES(tighten_msc_test
+ scmsc
+ sctimeconsistency
+
+ scpseudocode
+)
+
+ADD_EXECUTABLE(bmsc_tightening_test
+ bmsc_tightening_test.cpp
+)
+
+TARGET_LINK_LIBRARIES(bmsc_tightening_test
+ scmsc
+ sctimeconsistency
+ scpseudocode
+)
+
+
+#
+#ADD_EXECUTABLE(max_tightener_test
+# max_tightener_test.cpp
+#)
+
+#TARGET_LINK_LIBRARIES(max_tightener_test
+# scmsc
+# sctime
+# scpseudocode
+#)
+
+
+#ADD_EXECUTABLE(hmsc_all_paths_test
+# hmsc_all_paths_test.cpp
+#)
+
+#TARGET_LINK_LIBRARIES(hmsc_all_paths_test
+# scmsc
+# sctime
+# scpseudocode
+#)
+
+#ADD_EXECUTABLE(hmsc_tighten
+# hmsc_all_paths_test.cpp
+#)
+
# $Id$
Added: trunk/tests/bmsc_matrix_converter_test.cpp
===================================================================
--- trunk/tests/bmsc_matrix_converter_test.cpp (rev 0)
+++ trunk/tests/bmsc_matrix_converter_test.cpp 2009-07-05 16:44:41 UTC (rev 256)
@@ -0,0 +1,100 @@
+/*
+ * 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: race_checker_test.cpp 243 2009-05-03 19:05:14Z gotthardp $
+ */
+
+#include <iostream>
+
+#include "data/msc.h"
+#include "check/time/time_consistency.h"
+
+int main() {
+
+ BMscPtr bmsc(new BMsc(L"BMsc"));
+ InstancePtr instance1(new Instance(L"1"));
+ InstancePtr instance2(new Instance(L"2"));
+ InstancePtr instance3(new Instance(L"3"));
+ bmsc->add_instance(instance1);
+ bmsc->add_instance(instance2);
+ bmsc->add_instance(instance3);
+ StrictOrderAreaPtr strict1(new StrictOrderArea());
+ StrictOrderAreaPtr strict2(new StrictOrderArea());
+ StrictOrderAreaPtr strict3(new StrictOrderArea());
+ instance1->add_area(strict1);
+ instance2->add_area(strict2);
+ instance3->add_area(strict3);
+ EventPtr e0 = strict1->add_event();
+ EventPtr e1 = strict3->add_event();
+ EventPtr e2 = strict2->add_event();
+ EventPtr e3 = strict2->add_event();
+ EventPtr e4 = strict1->add_event();
+ EventPtr e5 = strict3->add_event();
+
+ CompleteMessagePtr m1 = new CompleteMessage(L"hi1");
+ m1->glue_events(e0, e1);
+ CompleteMessagePtr m2 = new CompleteMessage(L"hi2");
+ m2->glue_events(e5, e2);
+ CompleteMessagePtr m3 = new CompleteMessage(L"hi3");
+ m3->glue_events(e3, e4);
+
+ MscTimeIntervalD in6(10,20);
+ MscTimeIntervalD in7(0,0);
+ MscTimeIntervalD in8(30,40);
+ MscTimeIntervalD in9(60,D::infinity());
+ MscTimeIntervalD in10(20,30);
+ MscTimeIntervalD in11(40,50);
+ MscTimeIntervalD in12(60,70);
+ MscTimeIntervalD in13(20,70);
+
+
+
+ MscTimeIntervalDSet ins1;
+ MscTimeIntervalDSet ins2;
+ MscTimeIntervalDSet ins3;
+ MscTimeIntervalDSet ins4;
+ MscTimeIntervalDSet ins5;
+ MscTimeIntervalDSet ins6;
+ MscTimeIntervalDSet ins7;
+ MscTimeIntervalDSet ins8;
+
+ ins1.insert(in6);
+
+ ins2.insert(in8);
+ ins2.insert(in9);
+
+ ins3.insert(in6);
+
+ ins4.insert(in10);
+ ins4.insert(in11);
+
+ ins5.insert(in12);
+
+ ins6.insert(in7);
+ TimeRelationEvent::create(e0.get(),e1.get(),ins1);
+ TimeRelationEvent::create(e1.get(),e5.get(),ins6);
+ TimeRelationEvent::create(e5.get(),e2.get(),ins2);
+ TimeRelationEvent::create(e3.get(),e2.get(),ins1);
+ TimeRelationEvent::create(e3.get(),e4.get(),ins4);
+
+ TimeRelationEvent::create(e0.get(),e4.get(),ins5);
+
+ BmscMatrixConverter conv;
+ conv.compute_matrix(bmsc);
+ std::cerr << conv.get_matrix() << std::endl;
+ return 0;
+}
+
+// $Id: race_checker_test.cpp 243 2009-05-03 19:05:14Z gotthardp $
Added: trunk/tests/bmsc_tightening_test.cpp
===================================================================
--- trunk/tests/bmsc_tig...
[truncated message content] |
