Menu
▾
▴
[Scstudio-commits] SF.net SVN: scstudio:[405] trunk
|
From: <koc...@us...> - 2009-10-05 10:04:55
|
Revision: 405
http://scstudio.svn.sourceforge.net/scstudio/?rev=405&view=rev
Author: kocianon
Date: 2009-10-05 10:04:45 +0000 (Mon, 05 Oct 2009)
Log Message:
-----------
organization of time algorithms
Modified Paths:
--------------
trunk/src/check/time/CMakeLists.txt
trunk/src/check/time/time_consistency.cpp
trunk/src/check/time/time_consistency.h
trunk/src/check/time/time_pseudocode.h
trunk/src/data/msc.h
trunk/tests/bmsc_tightening_test.cpp
trunk/tests/incon_test.cpp
trunk/tests/tighten_msc_test.cpp
Added Paths:
-----------
trunk/src/check/time/tightening.cpp
trunk/src/check/time/tightening.h
trunk/src/check/time/time_pseudocode.cpp
Removed Paths:
-------------
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
Modified: trunk/src/check/time/CMakeLists.txt
===================================================================
--- trunk/src/check/time/CMakeLists.txt 2009-10-04 14:47:38 UTC (rev 404)
+++ trunk/src/check/time/CMakeLists.txt 2009-10-05 10:04:45 UTC (rev 405)
@@ -1,16 +1,14 @@
ADD_LIBRARY(sctime SHARED
export.h
module.cpp
+ time_pseudocode.cpp
+ time_pseudocode.h
time_consistency.cpp
time_consistency.h
- bmsc_tightening.h
- hmsc_all_paths.cpp
- hmsc_all_paths.h
- hmsc_tighten.h
- hmsc_tighten.cpp
- time_pseudocode.h
- constrain_check.h
- constrain_check.cpp
+ tightening.cpp
+ tightening.h
+ constrain_check.cpp
+ constrain_check.h
)
TARGET_LINK_LIBRARIES(sctime
Deleted: trunk/src/check/time/bmsc_tightening.h
===================================================================
--- trunk/src/check/time/bmsc_tightening.h 2009-10-04 14:47:38 UTC (rev 404)
+++ trunk/src/check/time/bmsc_tightening.h 2009-10-05 10:04:45 UTC (rev 405)
@@ -1,349 +0,0 @@
-#ifndef _TIME_TIGHTENING_H_
-#define _TIME_TIGHTENING_H_
-#include "time_consistency.h"
-#include "check/pseudocode/utils.h"
-
-typedef std::pair<Event*,Event*> EventPair;
-typedef std::list<EventPair> EventPairsList;
-typedef std::pair<MscTimeIntervalSetD,IntervalSetMatrix> ConstMatrixPair;
-typedef boost::intrusive_ptr<BMscMatrixConverter*> BMscMatrixConverterPtr;
-
-/**
- * \brief tightens bMSC
- */
-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);
- }
-
- bool 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();
- }
- /**
- * \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++)
- {
- 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;
- }
- /**
- * \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;
- }
-
- }
- if(is_maximal)
- {
- maximals.push_back(*it);
- }
- }
- return maximals;
- }
-
- /**
- * \brief tightens interval and matrix according to each other
- * \return pair - changed interval and matrix
- */
- ConstMatrixPair max_tightener(
- IntervalSetMatrix t_matrix,
- MscTimeIntervalSetD interval
- )
- {
-
- MscTimeIntervalSetD max_intrset;
- MscTimeIntervalSetD evts_intrset;
- max_intrset.insert(MscTimeIntervalD(0,0));
-
- EventPairsList pairs;
-
- 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++)
- {
- 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));
- */
- }
- }
-
- // 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++)
- {
- 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;
- EventPList::iterator it_max_events;
- MscTimeIntervalSetD path_union;
-
- 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))
- );
- }
- }
-
- 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);
- }
-
- 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++)
- {
- suffix_interval=MscTimeIntervalSetD::components_max(
- t_matrix(get_number(*it_succ),get_number(*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);
-
- } // 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 (!MatrixFunc::is_equal(old_matrix,current_matrix));
-
- return pair; // tighten interval, bmsc matrix
- }
-
-}; // class TightenBMsc
-
-
-#endif // _TIME_TIGHTENING_H_
Deleted: trunk/src/check/time/hmsc_all_paths.cpp
===================================================================
--- trunk/src/check/time/hmsc_all_paths.cpp 2009-10-04 14:47:38 UTC (rev 404)
+++ trunk/src/check/time/hmsc_all_paths.cpp 2009-10-05 10:04:45 UTC (rev 405)
@@ -1,66 +0,0 @@
-#include "check/time/hmsc_all_paths.h"
-
-HMscAllPaths AllPaths::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 AllPaths::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;
-}
Deleted: trunk/src/check/time/hmsc_all_paths.h
===================================================================
--- trunk/src/check/time/hmsc_all_paths.h 2009-10-04 14:47:38 UTC (rev 404)
+++ trunk/src/check/time/hmsc_all_paths.h 2009-10-05 10:04:45 UTC (rev 405)
@@ -1,63 +0,0 @@
-#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();
-
- void all_paths(HMscNodePtr, std::list<HMscNodePtr>, bool);
-
-};
-#endif
Deleted: trunk/src/check/time/hmsc_tighten.cpp
===================================================================
--- trunk/src/check/time/hmsc_tighten.cpp 2009-10-04 14:47:38 UTC (rev 404)
+++ trunk/src/check/time/hmsc_tighten.cpp 2009-10-05 10:04:45 UTC (rev 405)
@@ -1 +0,0 @@
-#include "check/time/hmsc_tighten.h"
Deleted: trunk/src/check/time/hmsc_tighten.h
===================================================================
--- trunk/src/check/time/hmsc_tighten.h 2009-10-04 14:47:38 UTC (rev 404)
+++ trunk/src/check/time/hmsc_tighten.h 2009-10-05 10:04:45 UTC (rev 405)
@@ -1,296 +0,0 @@
-#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_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
- {
- 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(size_t 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(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++)
- {
- 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/tightening.cpp
===================================================================
--- trunk/src/check/time/tightening.cpp (rev 0)
+++ trunk/src/check/time/tightening.cpp 2009-10-05 10:04:45 UTC (rev 405)
@@ -0,0 +1,136 @@
+#include "tightening.h"
+
+void MscSolveTCSP::forward(IntervalMatrix matrix,int i, int j)
+{
+ int new_j;
+ int new_i;
+ DEBUG_(i,j);
+ if((matrix.size1()==(unsigned)(i+1)) && (matrix.size1()==(unsigned)(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((unsigned)(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++)
+ {
+ IntervalMatrixFunc::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)=MscTimeIntervalSetD();
+ m_to_go_matrix(i,j)=MscTimeIntervalSetD();
+ }
+ }
+}
+
+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());
+
+ }
+ }
+ DEBUG(m_solve_matrix);
+ forward(matrix,0,-1);
+
+ return m_result_matrix;
+}
+
+//////////////////////////////////////////////////////////////////
Added: trunk/src/check/time/tightening.h
===================================================================
--- trunk/src/check/time/tightening.h (rev 0)
+++ trunk/src/check/time/tightening.h 2009-10-05 10:04:45 UTC (rev 405)
@@ -0,0 +1,712 @@
+/*
+ * 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) 2009
+ *
+ * $Id:
+ */
+
+#ifndef _TIGHTENING_H_
+#define _TIGHTENING_H_
+
+#include "time_consistency.h"
+#include "time_pseudocode.h"
+#include "check/pseudocode/msc_duplicators.h"
+#include "data/transformer.h"
+/*
+class SCTIME_EXPORT GreatTighter:public Transformer, public BMscTransformer
+{
+ virtual ~Transformer() {}
+
+ //! Human readable name of the transformation.
+ virtual std::string get_name()
+ {
+ return std::string("Great 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.
+ virtual PreconditionList get_preconditions(MscPtr msc) const = 0;
+
+ virtual BMscPtr transform(BMscPtr bmsc)
+{
+
+
+}
+
+
+};
+*/
+
+class SCTIME_EXPORT 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);
+};
+
+
+typedef std::pair<Event*,Event*> EventPair;
+typedef std::list<EventPair> EventPairsList;
+typedef std::pair<MscTimeIntervalSetD,IntervalSetMatrix> ConstMatrixPair;
+typedef boost::intrusive_ptr<BMscIntervalMatrixConverter*> BMscIntervalMatrixConverterPtr;
+
+/**
+ * \brief tightens bMSC
+ */
+class TightenBMsc
+{
+private:
+ BMscPtr m_bmsc;
+ BMscIntervalMatrixConverter m_converter;
+ IntervalSetMatrix m_matrix;
+
+ EventPList m_mins;
+ EventPList 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);
+ }
+
+ EventPVector get_events()
+ {
+ return m_converter.get_events();
+ }
+
+public:
+
+ 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++)
+ {
+ 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;
+ }
+ /**
+ * \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;
+ }
+
+ }
+ if (is_maximal)
+ {
+ maximals.push_back(*it);
+ }
+ }
+ return maximals;
+ }
+
+ /**
+ * \brief tightens interval and matrix according to each other
+ * \return pair - changed interval and matrix
+ */
+ ConstMatrixPair max_tightener(
+ IntervalSetMatrix t_matrix,
+ MscTimeIntervalSetD interval
+ )
+ {
+
+ MscTimeIntervalSetD max_intrset;
+ MscTimeIntervalSetD evts_intrset;
+ max_intrset.insert(MscTimeIntervalD(0,0));
+
+ EventPairsList pairs;
+
+ 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++)
+ {
+ 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));
+ */
+ }
+ }
+
+ // 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++)
+ {
+ 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;
+ EventPList::iterator it_max_events;
+ MscTimeIntervalSetD path_union;
+
+ 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))
+ );
+ }
+ }
+
+ 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);
+ }
+
+ 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++)
+ {
+ suffix_interval=MscTimeIntervalSetD::components_max(
+ t_matrix(get_number(*it_succ),get_number(*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);
+
+ } // 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:
+// 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_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
+ {
+ 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 (size_t 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;
+
+ 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++)
+ {
+ 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;
+ }
+
+};
+
+#endif //_TIGHTENING_H_
\ No newline at end of file
Modified: trunk/src/check/time/time_consistency.cpp
===================================================================
--- trunk/src/check/time/time_consistency.cpp 2009-10-04 14:47:38 UTC (rev 404)
+++ trunk/src/check/time/time_consistency.cpp 2009-10-05 10:04:45 UTC (rev 405)
@@ -1,4 +1,4 @@
-#include "check/time/time_consistency.h"
+#include "time_consistency.h"
const IntervalMatrix FloydWarshall::tight(const IntervalMatrix& matrix)
throw(MscTimeInconsistencyException)
@@ -21,7 +21,7 @@
}
}
return copy;
-}
+}
bool FloydWarshall::check_consistency(const IntervalMatrix& matrix)
@@ -45,268 +45,5 @@
return true;
}
/////////////////////////////////////////////////////////////////
-void MscSolveTCSP::forward(IntervalMatrix matrix,int i, int j)
-{
- int new_j;
- int new_i;
- DEBUG_(i,j);
- if((matrix.size1()==(unsigned)(i+1)) && (matrix.size1()==(unsigned)(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((unsigned)(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)=MscTimeIntervalSetD();
- m_to_go_matrix(i,j)=MscTimeIntervalSetD();
- }
- }
-}
-
-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(m_closure_initiator.get_visual_closure((*it)->get_event_a())[
- m_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()));
- }
- }
- }
-}
-///////////////////////////////////////////////////////////////////////
-
Modified: trunk/src/check/time/time_consistency.h
===================================================================
--- trunk/src/check/time/time_consistency.h 2009-10-04 14:47:38 UTC (rev 404)
+++ trunk/src/check/time/time_consistency.h 2009-10-05 10:04:45 UTC (rev 405)
@@ -1,10 +1,27 @@
+/*
+ * 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) 2009 Ondrej Kocian <koc...@ma...>
+ *
+ * $Id:
+ */
+
#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 "check/time/export.h"
+
+#include "time_pseudocode.h"
+
+
#include <limits>
#include <set>
#include <list>
@@ -12,6 +29,7 @@
#include <string>
#include <exception>
+
#ifdef _DEBUG
#include<iostream>
#define DEBUG(x) std::cerr << "DB: " << __FILE__ << ":" << __LINE__ << " " \
@@ -25,101 +43,11 @@
#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> MscTimeIntervalSetD;
-typedef boost::numeric::ublas::matrix<MscTimeIntervalD> IntervalMatrix;
-typedef boost::numeric::ublas::matrix<MscTimeIntervalSetD> 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:
- //! 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)
- {
- if(x>=matrix.size1()||y>=matrix.size2())
- throw matrix.size1();
- matrix(x,y) = c;
- matrix(y,x) = MscTimeIntervalD::interval_inverse(c);
- }
-
- //! 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_invers...
[truncated message content] |
