Menu
▾
▴
[Scstudio-commits] SF.net SVN: scstudio:[501] trunk
|
From: <koc...@us...> - 2009-12-02 22:45:12
|
Revision: 501
http://scstudio.svn.sourceforge.net/scstudio/?rev=501&view=rev
Author: kocianon
Date: 2009-12-02 22:45:05 +0000 (Wed, 02 Dec 2009)
Log Message:
-----------
tightening - not working but worked 5 mins ago, infinite value in interval fix (valid/invalid)
Modified Paths:
--------------
trunk/src/check/time/tightening.cpp
trunk/src/check/time/tightening.h
trunk/src/check/time/time_pseudocode.h
trunk/src/data/time.h
trunk/tests/CMakeLists.txt
trunk/tests/tighten_msc_test.cpp
Modified: trunk/src/check/time/tightening.cpp
===================================================================
--- trunk/src/check/time/tightening.cpp 2009-12-02 21:02:43 UTC (rev 500)
+++ trunk/src/check/time/tightening.cpp 2009-12-02 22:45:05 UTC (rev 501)
@@ -151,4 +151,120 @@
return m_result_matrix;
}
+
+///////////////////////////////////////////////////////////////////
+
+MscTimeIntervalSetD TightenBMsc::get_max_interval(BMscIntervalSetMatrix bmsc_matrix)
+{
+ 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 find max_intrset
+ 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=bmsc_matrix(*it_min,*it_max);
+ max_intrset = MscTimeIntervalSetD::components_max(max_intrset,evts_intrset);
+ }
+ }
+ return max_intrset;
+}
+
+ConstBMscMatrixPair TightenBMsc::tighten_msc(MscTimeIntervalSetD interval)
+{
+
+ MscSolveTCSP solve;
+ BMscIntervalSetMatrix old_matrix(m_matrix);
+ BMscIntervalSetMatrix current_matrix(m_matrix);
+
+ // pair (MscTimeIntervalSetD,IntervalSetMatrix)
+ ConstBMscMatrixPair pair(std::make_pair(interval,m_bmsc));
+ 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));
+ m_matrix = current_matrix;
+ return pair; // tighten interval, bmsc matrix
+}
+
+ConstBMscMatrixPair TightenBMsc::max_tightener(BMscIntervalSetMatrix t_matrix
+ ,MscTimeIntervalSetD interval
+ )
+{
+ MscTimeIntervalSetD max_intrset = get_max_interval(t_matrix);
+ // assign tightened interval
+ interval = MscTimeIntervalSetD::set_intersection(interval,max_intrset);
+ EventPVector::iterator it_v;
+
+ // for all a \in events
+ // for all b \in a.get_next do
+ for (it_v = m_events.begin();it_v!=m_events.end();it_v++)
+ {
+ EventPSet succs = EventFirstSuccessors::get(*it_v);
+ EventPSet::iterator it_succ;
+
+ for (it_succ=succs.begin();it_succ!=succs.end();it_succ++)
+ {
+ EventPList::iterator it_min_events;
+ 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(*it_min_events,*it_max_events));
+ }
+ }
+
+ MscTimeIntervalSetD tight_interval;
+ tight_interval = MscTimeIntervalSetD::set_union(interval,
+ MscTimeIntervalSetD::zero_max_interval(path_union,interval));
+ MscTimeIntervalSetD prefix_interval;
+ prefix_interval.insert(MscTimeIntervalD(0,0));
+
+ for (it_min_events=m_mins.begin();it_min_events!=m_mins.end();it_min_events++)
+ {
+ prefix_interval=MscTimeIntervalSetD::components_max(
+ t_matrix(*it_min_events,*it_v),prefix_interval);
+ }
+
+ MscTimeIntervalSetD suffix_interval;
+ suffix_interval.insert(MscTimeIntervalD(0,0));
+
+ for (it_max_events=m_maxs.begin();
+ it_max_events!=m_maxs.end();
+ it_max_events++)
+ {
+ suffix_interval=MscTimeIntervalSetD::components_max(
+ t_matrix(*it_succ,*it_max_events),suffix_interval);
+ }
+
+ //final tightening
+ t_matrix(*it_v,*it_succ)=MscTimeIntervalSetD::set_intersection(
+ t_matrix(*it_v,*it_succ)
+ ,tight_interval-prefix_interval-suffix_interval);
+
+ } // end for succs
+ } // end for all events
+
+ return std::make_pair(interval,t_matrix);
+}
+
// $Id$
Modified: trunk/src/check/time/tightening.h
===================================================================
--- trunk/src/check/time/tightening.h 2009-12-02 21:02:43 UTC (rev 500)
+++ trunk/src/check/time/tightening.h 2009-12-02 22:45:05 UTC (rev 501)
@@ -23,6 +23,15 @@
#include "time_pseudocode.h"
#include "check/pseudocode/msc_duplicators.h"
#include "data/transformer.h"
+
+typedef std::pair<Event*,Event*> EventPair;
+typedef std::list<EventPair> EventPairsList;
+typedef std::pair<MscTimeIntervalSetD,IntervalSetMatrix> ConstMatrixPair;
+typedef std::pair<MscTimeIntervalSetD,BMscIntervalSetMatrix> ConstBMscMatrixPair;
+typedef boost::intrusive_ptr<BMscIntervalMatrixConverter*> BMscIntervalMatrixConverterPtr;
+
+
+class TightenBMsc;
/*
class SCTIME_EXPORT GreatTighter:public Transformer, public BMscTransformer
{
@@ -50,37 +59,7 @@
};
*/
-/*
-class BMscTighter//:public Transformer, public BMscTransformer
-{
-public:
- //! Human readable name of the transformation.
- virtual std::string get_name()
- {
- return std::string("BMsc Tigher");
- }
-
- //! List of properties that must be satisfied before executing the transformation.
- typedef std::vector<PrerequisiteCheck> PreconditionList;
-
- //! Returns a list of preconditions for this transformation.
- PreconditionList get_preconditions(MscPtr msc) const
- {
- return PreconditionList();
- }
-
- BMscPtr transform(BMscPtr bmsc)
- {
- BMscPtr new_bmsc;
- return new_bmsc;
- }
-
- ~BMscTighter() {}
-};
-
-*/
-
class SCTIME_EXPORT MscSolveTCSP
{
private:
@@ -106,11 +85,8 @@
};
-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
*/
@@ -131,28 +107,10 @@
return m_event_top.is_leq(e,f);
}
- MscTimeIntervalSetD get_max_interval(BMscIntervalSetMatrix bmsc_matrix)
- {
- MscTimeIntervalSetD max_intrset;
- MscTimeIntervalSetD evts_intrset;
- max_intrset.insert(MscTimeIntervalD(0,0));
+ MscTimeIntervalSetD get_max_interval(BMscIntervalSetMatrix);
- EventPairsList pairs;
- EventPList::iterator it_min;
- EventPList::iterator it_max;
-
- // for every pair (minimal,maximal) events find max_intrset
- 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=bmsc_matrix(*it_min,*it_max);
- max_intrset = MscTimeIntervalSetD::components_max(max_intrset,evts_intrset);
- }
- }
- return max_intrset;
- }
-
+ //! tightens interval and matrix according to each other
+ ConstBMscMatrixPair max_tightener(BMscIntervalSetMatrix,MscTimeIntervalSetD);
public:
TightenBMsc(BMscPtr bmsc):m_bmsc(bmsc),m_matrix(bmsc),m_event_top(bmsc)
@@ -160,112 +118,64 @@
{
}
- static ConstMatrixPair tight(
- BMscPtr bmsc
- ,MscTimeIntervalSetD interval)
+ //! tight BMsc due to interval
+ ConstBMscMatrixPair tighten_msc(MscTimeIntervalSetD);
+
+ static ConstBMscMatrixPair tight(BMscPtr bmsc,MscTimeIntervalSetD interval)
{
TightenBMsc tightening(bmsc);
- ConstMatrixPair pair = tightening.tighten_msc(interval);
+ ConstBMscMatrixPair pair = tightening.tighten_msc(interval);
//tightening.modificate(pair.second);
return pair;
}
- //! tight BMsc due to interval
- ConstMatrixPair tighten_msc(MscTimeIntervalSetD interval)
- {
+}; // class TightenBMsc
- MscSolveTCSP solve;
- BMscIntervalSetMatrix old_matrix(m_matrix);
- BMscIntervalSetMatrix current_matrix(m_matrix);
+typedef std::list<HMscNodePtr> HMscNodePtrList;
- // pair (MscTimeIntervalSetD,IntervalSetMatrix)
- ConstMatrixPair pair;
- do
+
+class BMscTighter:public Transformer // , public BMscTransformer
+{
+
+ public:
+ //! Human readable name of the transformation.
+ virtual std::wstring get_name() const
{
- 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;
+ return L"BMsc Tigher";
}
- while (!IntervalMatrixFunc::is_equal(old_matrix,current_matrix));
- return pair; // tighten interval, bmsc matrix
- }
+ //! List of properties that must be satisfied before executing the transformation.
+ typedef std::vector<PrerequisiteCheck> PreconditionList;
- //! tightens interval and matrix according to each other
- ConstMatrixPair max_tightener(BMscIntervalSetMatrix t_matrix
- ,MscTimeIntervalSetD interval
- )
- {
- MscTimeIntervalSetD max_intrset = get_max_interval(t_matrix);
- // assign tightened interval
- interval = MscTimeIntervalSetD::set_intersection(interval,max_intrset);
- EventPVector::iterator it_v;
+ //! Returns a list of preconditions for this transformation.
+ PreconditionList get_preconditions(MscPtr msc) const
+ {
+ return PreconditionList();
+ }
- // for all a \in events
- // for all b \in a.get_next do
- for (it_v = m_events.begin();it_v!=m_events.end();it_v++)
+ MscPtr transform(MscPtr msc)
{
- EventPSet succs = EventFirstSuccessors::get(*it_v);
- EventPSet::iterator it_succ;
+ BMscPtr bmsc = dynamic_cast<BMsc*>(msc.get());
+ if(!bmsc.get())
+ return NULL;
- for (it_succ=succs.begin();it_succ!=succs.end();it_succ++)
- {
- EventPList::iterator it_min_events;
- EventPList::iterator it_max_events;
- MscTimeIntervalSetD path_union;
+ return transform(bmsc);
+ }
+
+ BMscPtr transform(BMscPtr bmsc)
+ {
+ MscTimeIntervalSetD set;
+ MscTimeIntervalD interval(-D::infinity(),D::infinity());
+ set.insert(interval);
+ TightenBMsc tightener(bmsc);
+ ConstBMscMatrixPair pair = tightener.tighten_msc(set);
+ return pair.second.get_modified_bmsc();
+ }
- 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(*it_min_events,*it_max_events));
- }
- }
+ ~BMscTighter() {}
+};
- 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(*it_min_events,*it_v),prefix_interval);
- }
-
- MscTimeIntervalSetD suffix_interval;
- suffix_interval.insert(MscTimeIntervalD(0,0));
-
- for (it_max_events=m_maxs.begin();
- it_max_events!=m_maxs.end();
- it_max_events++)
- {
- suffix_interval=MscTimeIntervalSetD::components_max(
- t_matrix(*it_succ,*it_max_events),suffix_interval);
- }
-
- //final tightening
- t_matrix(*it_v,*it_succ)=MscTimeIntervalSetD::set_intersection(
- t_matrix(*it_v,*it_succ)
- ,tight_interval-prefix_interval-suffix_interval);
-
- } // end for succs
- } // end for all events
-
- return std::make_pair(interval,t_matrix);
- }
-
-}; // class TightenBMsc
-
-typedef std::list<HMscNodePtr> HMscNodePtrList;
/*
class TightenSetOfPaths
{
Modified: trunk/src/check/time/time_pseudocode.h
===================================================================
--- trunk/src/check/time/time_pseudocode.h 2009-12-02 21:02:43 UTC (rev 500)
+++ trunk/src/check/time/time_pseudocode.h 2009-12-02 22:45:05 UTC (rev 501)
@@ -156,7 +156,7 @@
}
build_up_matrix();
}
-
+/*
BMscIntervalSetMatrix(const BMscIntervalSetMatrix& matrix):
IntervalSetMatrix(matrix)
,m_event_topology(matrix.get_original_bmsc())
@@ -165,7 +165,7 @@
m_events=matrix.m_events;
m_event_number=matrix.m_event_number;
m_time_rel_set=matrix.m_time_rel_set;
- }
+ }*/
using IntervalSetMatrix::operator();
Modified: trunk/src/data/time.h
===================================================================
--- trunk/src/data/time.h 2009-12-02 21:02:43 UTC (rev 500)
+++ trunk/src/data/time.h 2009-12-02 22:45:05 UTC (rev 501)
@@ -38,6 +38,9 @@
#pragma warning(disable: 4290)
#endif
+
+typedef std::numeric_limits<double> D;
+
/*
class MscIntervalCoupleUncomparable;
class MscIntervalCouple;
@@ -800,10 +803,22 @@
{
return false;
}
- if(m_begin==m_end)
- return m_begin.get_closed();
- else
- return true;
+ if(m_begin.get_value()==D::infinity())
+ return false;
+
+ if(m_end.get_value()==-D::infinity())
+ return false;
+
+ if(m_begin.get_value()==-D::infinity() && m_begin.get_closed())
+ return false;
+
+ if(m_end.get_value()==D::infinity() && m_end.get_closed())
+ return false;
+
+ if(m_begin==m_end && !m_begin.get_closed())
+ return false;
+
+ return true;
}
void set_empty()
Modified: trunk/tests/CMakeLists.txt
===================================================================
--- trunk/tests/CMakeLists.txt 2009-12-02 21:02:43 UTC (rev 500)
+++ trunk/tests/CMakeLists.txt 2009-12-02 22:45:05 UTC (rev 501)
@@ -168,14 +168,15 @@
# scpseudocode
# )
-#ADD_EXECUTABLE(tighten_msc_test
-# tighten_msc_test.cpp
-# )
-# TARGET_LINK_LIBRARIES(tighten_msc_test
-# scmsc
-# sctime
-# scpseudocode
-# )
+ADD_EXECUTABLE(tighten_msc_test
+ tighten_msc_test.cpp
+)
+TARGET_LINK_LIBRARIES(tighten_msc_test
+ scmsc
+ sctime
+ scpseudocode
+ scZ120
+)
#
# ADD_EXECUTABLE(bmsc_tightening_test
# bmsc_tightening_test.cpp
Modified: trunk/tests/tighten_msc_test.cpp
===================================================================
--- trunk/tests/tighten_msc_test.cpp 2009-12-02 21:02:43 UTC (rev 500)
+++ trunk/tests/tighten_msc_test.cpp 2009-12-02 22:45:05 UTC (rev 501)
@@ -18,6 +18,7 @@
#include <iostream>
#include "check/time/tightening.h"
+#include "data/Z120/z120.h"
int main(int argc, char** argv) {
@@ -69,19 +70,19 @@
MscTimeIntervalSetD ins8;
ins1.insert(in6);
-
+
ins2.insert(in8);
- ins2.insert(in9);
-
- ins3.insert(in6);
-
- ins4.insert(in10);
- ins4.insert(in11);
+ ins2.insert(in9);
+ ins3.insert(in6);
+
+ ins4.insert(in10);
+ ins4.insert(in11);
+
ins5.insert(in12);
ins6.insert(in7);
-
+
TimeRelationEventPtr rel1a = new TimeRelationEvent(ins1);
rel1a->glue_events(e0.get(),e1.get());
TimeRelationEventPtr rel6 = new TimeRelationEvent(ins6);
@@ -97,37 +98,39 @@
MscTimeIntervalSetD i;
i.insert(MscTimeIntervalD(0,80));
-
+/*
BMscIntervalMatrixConverter conv(bmsc);
std::cerr << conv.get_matrix() << std::endl;
if(conv.is_leq(e3.get(),e4.get()))
std::cerr << "ANO" << std::endl;
else
- std::cerr << "NE" << std::endl;
+ std::cerr << "NE" << std::endl;*/
// MscSolveTCSP sol;
// std::cerr << sol.solve(conv.get_matrix()) << std::endl;
// sol.solve(conv.get_matrix());
- std::cerr << "tighten passed " << std::endl;
+ // std::cerr << "tighten passed " << std::endl;
// MaxTightener tight(bmsc,&conv);
- std::cerr << "tighten passed " << std::endl;
+// std::cerr << "tighten passed " << std::endl;
// EventPList min;
// EventPList max;
// min.push_back(e0.get());
// min.push_back(e3.get());
// max.push_back(e2.get());
// max.push_back(e4.get());
-
+/*
ConstMatrixPair pair;
TightenBMsc tighten(bmsc);
std::cerr << "tighten passed " << std::endl;
- pair = tighten.tighten_msc(i);
-
-
-
+ pair = tighten.tighten_msc(i);*/
+ BMscTighter tightener;
+ BMscPtr result = tightener.transform(bmsc);
+ Z120 z120;
+ z120.save_msc(std::cout,L"original",bmsc);
+ z120.save_msc(std::cout,L"result",result);
// tight.max_tightener(min,max,sol.solve(conv.get_matrix()),i,bmsc,conv);
// std::pair<MscTimeIntervalSetD,IntervalSetMatrix> max_tightener(EventPList min, EventPList max,IntervalSetMatrix t_matrix,MscTimeIntervalSetD i,BMsc bmsc)
//
- std::cerr << pair.first << std::endl << pair.second << std::endl;
+ //std::cerr << pair.first << std::endl << pair.second << std::endl;
return 0;
}
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
