Menu
▾
▴
[Scstudio-commits] SF.net SVN: scstudio:[602] trunk
|
From: <koc...@us...> - 2010-02-20 11:38:17
|
Revision: 602
http://scstudio.svn.sourceforge.net/scstudio/?rev=602&view=rev
Author: kocianon
Date: 2010-02-20 11:38:10 +0000 (Sat, 20 Feb 2010)
Log Message:
-----------
BMcsIntervalMatrix fix
Modified Paths:
--------------
trunk/src/check/pseudocode/utils.h
trunk/src/check/time/tightening.cpp
trunk/src/check/time/time_consistency.cpp
trunk/src/check/time/time_consistency.h
trunk/src/check/time/time_pseudocode.cpp
trunk/src/check/time/time_pseudocode.h
trunk/src/data/session_attribute.cpp
trunk/src/data/time.cpp
trunk/tests/tighten_msc_test.cpp
Modified: trunk/src/check/pseudocode/utils.h
===================================================================
--- trunk/src/check/pseudocode/utils.h 2010-02-19 19:30:12 UTC (rev 601)
+++ trunk/src/check/pseudocode/utils.h 2010-02-20 11:38:10 UTC (rev 602)
@@ -143,6 +143,12 @@
return m_closure_initiator.get_visual_closure(a)[m_closure_initiator.get_topology_index(b)];
}
+ const EventPVector get_topology()
+ {
+ EventPVector topology(m_topology_listener.get_topology().size());
+ topology.assign(m_topology_listener.get_topology().begin(),m_topology_listener.get_topology().end());
+ return topology;
+ }
};
template<class MscElementContainer,class AttributeType>
Modified: trunk/src/check/time/tightening.cpp
===================================================================
--- trunk/src/check/time/tightening.cpp 2010-02-19 19:30:12 UTC (rev 601)
+++ trunk/src/check/time/tightening.cpp 2010-02-20 11:38:10 UTC (rev 602)
@@ -133,6 +133,7 @@
BMscPtr BMscTighter::transform(BMscPtr bmsc)
{
BMscIntervalSetMatrix matrix(bmsc);
+ matrix.build_up();
MscSolveTCSP solve;
MscSolveTCSPReport report = solve.solveTCSP(matrix);
matrix = report.m_matrix_result;
Modified: trunk/src/check/time/time_consistency.cpp
===================================================================
--- trunk/src/check/time/time_consistency.cpp 2010-02-19 19:30:12 UTC (rev 601)
+++ trunk/src/check/time/time_consistency.cpp 2010-02-20 11:38:10 UTC (rev 602)
@@ -28,8 +28,7 @@
{
for(unsigned j=0; j < matrix.size1(); j++)
{
- copy(i,j) = MscTimeIntervalD::interval_intersection(copy(i,j), \
- copy(i,k)+copy(k,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));
@@ -135,6 +134,7 @@
DEBUG(to_tight);
//tight
IntervalMatrix tmp = m_tightener->tight(to_tight);
+ DEBUG(tmp);
// remember both
m_report->csp_mtxs.push_back(to_tight);
m_report->csp_tighten_mtxs.push_back(tmp);
@@ -151,12 +151,16 @@
m_report= &report;
m_size = matrix.size1();
-
- IntervalMatrix m;
- init_simple_matrix(m);
-
- // start whole process
- insert_interval(m,0,0);
+
+ if(m_size>0)
+ {
+ IntervalMatrix m;
+ init_simple_matrix(m);
+ // start whole process
+
+ insert_interval(m,0,0);
+ }
+
return report;
}
Modified: trunk/src/check/time/time_consistency.h
===================================================================
--- trunk/src/check/time/time_consistency.h 2010-02-19 19:30:12 UTC (rev 601)
+++ trunk/src/check/time/time_consistency.h 2010-02-20 11:38:10 UTC (rev 602)
@@ -218,9 +218,10 @@
virtual std::list<BMscPtr> check(BMscPtr bmsc, ChannelMapperPtr mapper)
{
BMscIntervalSetMatrix matrix(bmsc);
+ matrix.build_up();
MscSolveTCSP solve;
MscSolveTCSPReport report = solve.solveTCSP(matrix);
- std::list<BMscPtr> res_list;
+ std::list<BMscPtr> res_list;
// there was at least one matrix found -> consistent
if(report.csp_mtxs.size()!=0)
Modified: trunk/src/check/time/time_pseudocode.cpp
===================================================================
--- trunk/src/check/time/time_pseudocode.cpp 2010-02-19 19:30:12 UTC (rev 601)
+++ trunk/src/check/time/time_pseudocode.cpp 2010-02-20 11:38:10 UTC (rev 602)
@@ -21,95 +21,49 @@
void BMscIntervalSetMatrix::build_up_matrix()
{
- IntervalSetMatrix::resize(m_events.size());
- for (unsigned i=0;i<m_events.size();i++)
+ m_builded = true;
+ IntervalSetMatrix::resize(m_size);
+ for (unsigned i=0;i<m_size;i++)
{
- for (unsigned j=0;j<m_events.size();j++)
+ for (unsigned j=0;j<m_size;j++)
{
if (j==i)
{
- operator()(i,j)=MscTimeIntervalSetD();
- operator()(i,j).insert(MscTimeIntervalD(0,0));
+ operator()(i,j) = MscTimeIntervalD(0,0);
}
else
{
- operator()(i,j) =MscTimeIntervalSetD();
- operator()(i,j).insert(MscTimeIntervalD(-D::infinity(),D::infinity()));
+ operator()(i,j)= 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++)
+
+ std::map<std::pair<unsigned,unsigned>, MscTimeIntervalSetD>::const_iterator it;
+ for(it=m_position_to_interval.begin();it!=m_position_to_interval.end();it++)
{
- EventPSet set = EventFirstSuccessors::get(*e_v);
- for (e_m=set.begin();e_m!=set.end();e_m++)
- {
- operator()(*e_v,*e_m) = MscTimeIntervalSetD();
- operator()(*e_v,*e_m).insert(MscTimeIntervalD(0,D::infinity()));
-
- operator()(*e_m,*e_v) = MscTimeIntervalSetD();
- operator()(*e_m,*e_v).insert(MscTimeIntervalD(-D::infinity(),0));
- }
-
- TimeRelationEventPtrList::const_iterator it;
- TimeRelationEventPtrList relations = (*e_v)->get_time_relations();
-
- for (it=relations.begin();it!=relations.end();it++)
- {
- m_time_rel_set.insert(*it);
- EventP a = (*it)->get_event_a();
- EventP b = (*it)->get_event_b();
- if (m_event_topology.is_leq(a,b))
- {
- fill(a,b,(*it)->get_interval_set());
- }
- else
- {
- fill(b,a,(*it)->get_interval_set());
- }
- }
+ fill((it->first).first,(it->first).second,it->second);
}
+ m_matrix_original = *this;
}
BMscPtr BMscIntervalSetMatrix::get_modified_bmsc()
{
- // duplicate bmsc
- BMscPtr copy_bmsc;
- BMscDuplicator duplicator;
- copy_bmsc = duplicator.duplicate_bmsc(m_original_bmsc);
+ // duplicate bmsc
+ BMscPtr copy_bmsc;
+ BMscDuplicator duplicator;
+ copy_bmsc = duplicator.duplicate_bmsc(m_bmsc_original);
- // go through all relations and set copy new values
- std::set<TimeRelationEventPtr>::iterator it;
- for(it=m_time_rel_set.begin();it!=m_time_rel_set.end();it++)
- {
- EventP a = (*it)->get_event_a();
- EventP b = (*it)->get_event_b();
-
-// time relation is empty -> remove
- if(operator()(a,b).is_empty())
- {
- a->remove_time_relation(*it);
- b->remove_time_relation(*it);
- continue;
- }
-
- TimeRelationEvent* relation_copy;
- relation_copy = static_cast<TimeRelationEvent*>(duplicator.get_copy(it->get()));
- // set new value to time relation
- if (m_event_topology.is_leq(a,b))
- {
- relation_copy->set_interval_set(operator()(a,b));
- }
- else
- {
- relation_copy->set_interval_set(operator()(b,a));
- }
- }
- return copy_bmsc;
+ // go through all relations and set copy new values
+ std::map<TimeRelation*, std::pair<unsigned,unsigned> >::const_iterator it;
+ for(it=m_rel_to_position.begin();it!=m_rel_to_position.end();it++)
+ {
+ if(duplicator.get_copy(it->first))
+ ((TimeRelation*)duplicator.get_copy(it->first))->set_interval_set(operator()(it->second.first,it->second.second));
+ else
+ (it->first)->set_interval_set(operator()(it->second.first,it->second.second));
}
+ return copy_bmsc;
+}
// $Id$
Modified: trunk/src/check/time/time_pseudocode.h
===================================================================
--- trunk/src/check/time/time_pseudocode.h 2010-02-19 19:30:12 UTC (rev 601)
+++ trunk/src/check/time/time_pseudocode.h 2010-02-20 11:38:10 UTC (rev 602)
@@ -120,15 +120,22 @@
class BMscIntervalSetMatrix: public IntervalSetMatrix
{
private:
- BMscPtr m_original_bmsc;
- IntervalSetMatrix m_original_matrix;
+ BMscPtr m_bmsc_original;
+
+ bool m_builded;
+ unsigned m_size;
+
+ IntervalSetMatrix m_matrix_original;
+
+ std::map<std::pair<unsigned,unsigned>, MscTimeIntervalSetD> m_position_to_interval;
+
+ std::map<TimeRelation*, std::pair<unsigned,unsigned> > m_rel_to_position;
+ std::map<EventP,unsigned> m_event_to_number; //! the number of event in the matrix
- AllReachableEventPVector m_events; //! Vector of all events: event=matrix[number]
- std::map<EventP,unsigned> m_event_number; //! the number of event in the matrix
- EventTopologyHandler m_event_topology;
- //! set of all time relations,creates in build_up_matrix() function
- std::set<TimeRelationEventPtr> m_time_rel_set;
+ EventPVector m_events; //! Vector of all events: event=matrix[number]
+
+
//! initialization of visual closure
void build_up_matrix();
@@ -137,26 +144,54 @@
{
}
- /**
- * \brief Apply changes from the matrix to the bmsc copy
- */
-
public:
BMscIntervalSetMatrix(BMscPtr bmsc):
- m_original_bmsc(bmsc)
- ,m_events(bmsc)
- ,m_event_topology(bmsc)
+ m_bmsc_original(bmsc)
+ ,m_builded(false)
{
- std::vector<EventP>::iterator it;
- unsigned i;
-
- // set numbers to events and their succs
- for (it=m_events.begin(),i=0;it!=m_events.end();it++,i++)
+ EventTopologyHandler event_topology(m_bmsc_original);
+ m_events = event_topology.get_topology();
+
+ unsigned i; // column and row in matrix
+
+ // for all events in bmsc do:
+ EventPVector::const_iterator e_v;
+ EventPSet::const_iterator e_m;
+ for (e_v=m_events.begin(),i=0;e_v!=m_events.end();e_v++,i++)
{
- m_event_number[*it]=i;
+ m_event_to_number[*e_v]=i; // assign number to the event
}
- build_up_matrix();
- m_original_matrix = *this;
+
+ for (e_v=m_events.begin();e_v!=m_events.end();e_v++)
+ {
+ EventPSet set = EventFirstSuccessors::get(*e_v); // assigned to successors (0,inf) int
+ for (e_m=set.begin();e_m!=set.end();e_m++)
+ {
+ operator()(*e_v,*e_m)=MscTimeIntervalD(0,D::infinity());
+ }
+ }
+
+ for (e_v=m_events.begin();e_v!=m_events.end();e_v++)
+ {
+
+ TimeRelationEventPtrList::const_iterator it;
+ TimeRelationEventPtrList relations = (*e_v)->get_time_relations();
+
+ for (it=relations.begin();it!=relations.end();it++)
+ {
+ EventP a = (*it)->get_event_a();
+ EventP b = (*it)->get_event_b();
+ if (event_topology.is_leq(a,b)) // a<=b
+ {
+ // add time relation to the map
+ m_rel_to_position[it->get()]=std::make_pair(get_number(a),get_number(b));
+ if(m_position_to_interval.find(std::make_pair(get_number(a),get_number(b)))==m_position_to_interval.end())
+ operator()(a,b) = (*it)->get_interval_set();
+ else
+ operator()(a,b) = MscTimeIntervalSetD::set_intersection((*it)->get_interval_set(),operator()(a,b));
+ }
+ }
+ }
}
/*
BMscIntervalSetMatrix(const BMscIntervalSetMatrix& matrix):
@@ -174,22 +209,22 @@
//! return number of event in matrix
unsigned get_number(EventP e)
{
- return m_event_number[e];
+ return m_event_to_number[e];
}
+ //! if matrix was builded -> return reference from matrix, else return reference from map
MscTimeIntervalSetD& operator()(EventP a,EventP b)
{
- return operator()(get_number(a),get_number(b));
+ if(m_builded)
+ return operator()(get_number(a),get_number(b));
+ else
+ return m_position_to_interval[std::make_pair<unsigned,unsigned>(get_number(a),get_number(b))];
}
- MscTimeIntervalSetD& operator()(EventP a)
- {
- return operator()(get_number(a),get_number(a));
- }
BMscIntervalSetMatrix& operator=(const BMscIntervalSetMatrix& matrix)
{
- if(m_original_bmsc!=matrix.m_original_bmsc)
+ if(m_bmsc_original!=matrix.m_bmsc_original)
throw std::invalid_argument("BMscs dont match!");
IntervalSetMatrix::operator=(matrix);
return *this;
@@ -200,13 +235,16 @@
IntervalSetMatrix::operator=(matrix);
return *this;
}
-
-
- //! return all reachable events in bmsc
- const EventPVector get_events()
+ //! return all events in matrix
+ const EventPVector get_events() const
{
return m_events;
}
+
+ const unsigned get_size() const
+ {
+ return m_events.size();
+ }
//! Takes (modificated) matrix of bmsc and changes bmsc
BMscPtr get_modified_bmsc();
@@ -214,7 +252,7 @@
//! return original bmsc (assigned to the matrix)
BMscPtr get_original_bmsc() const
{
- return m_original_bmsc;
+ return m_bmsc_original;
}
~BMscIntervalSetMatrix()
@@ -231,9 +269,22 @@
//! puts IntervalSet in to the matrix to the position of events x,y
void fill(EventP x,EventP y,const MscTimeIntervalSetD& c)
{
+ fill(get_number(x),get_number(y),c);
+ }
+
+ void fill(unsigned x,unsigned y,const MscTimeIntervalSetD& c)
+ {
operator()(x,y)=c;
operator()(y,x)= MscTimeIntervalSetD::interval_inverse(c);
}
+
+ void build_up()
+ {
+ if(m_builded)
+ throw std::runtime_error("Matrix was already builded");
+ m_size = m_events.size();
+ build_up_matrix();
+ }
}; // end of class BMscMatrixConverter
Modified: trunk/src/data/session_attribute.cpp
===================================================================
--- trunk/src/data/session_attribute.cpp 2010-02-19 19:30:12 UTC (rev 601)
+++ trunk/src/data/session_attribute.cpp 2010-02-20 11:38:10 UTC (rev 602)
@@ -13,7 +13,7 @@
*
* Copyright (c) 2009 Ondrej Kocian <koc...@ma...>
*
- * $Id:$
+ * $Id$
*/
#include "data/session_attribute.h"
@@ -37,4 +37,4 @@
cancel_attribute();
}
-// $Id:$
+// $Id$
Modified: trunk/src/data/time.cpp
===================================================================
--- trunk/src/data/time.cpp 2010-02-19 19:30:12 UTC (rev 601)
+++ trunk/src/data/time.cpp 2010-02-20 11:38:10 UTC (rev 602)
@@ -52,8 +52,7 @@
}
template <>
-MscIntervalCouple<double>::MscIntervalCouple(const std::string& number, \
-const bool& closed):
+MscIntervalCouple<double>::MscIntervalCouple(const std::string& number, const bool& closed):
m_closed(closed)
,m_value(0)
{
Modified: trunk/tests/tighten_msc_test.cpp
===================================================================
--- trunk/tests/tighten_msc_test.cpp 2010-02-19 19:30:12 UTC (rev 601)
+++ trunk/tests/tighten_msc_test.cpp 2010-02-20 11:38:10 UTC (rev 602)
@@ -19,6 +19,7 @@
#include <iostream>
#include "check/time/tightening.h"
#include "data/Z120/z120.h"
+#include <list>
int main(int argc, char** argv) {
@@ -41,7 +42,7 @@
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");
@@ -53,7 +54,7 @@
MscTimeIntervalD in7(0,0);
MscTimeIntervalD in8(30,40);
MscTimeIntervalD in9(60,D::infinity());//TODO: infi
- MscTimeIntervalD in10(20,30);
+ MscTimeIntervalD in10(20,30);
MscTimeIntervalD in11(40,50);
MscTimeIntervalD in12(60,120);
MscTimeIntervalD in13(20,70);
@@ -122,11 +123,29 @@
TightenBMsc tighten(bmsc);
std::cerr << "tighten passed " << std::endl;
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);
+ // z120.save_msc(std::cout,L"original",bmsc);
+ // z120.save_msc(std::cout,L"result",result);
+ std::vector<MscPtr> mscs = z120.load_msc("cons_neg_1.mpr");
+ std::cout << mscs.size() << std::endl;
+ BMscPtr b = boost::dynamic_pointer_cast<BMsc>(mscs[0]);
+ z120.save_msc(std::cout,L"result",b);
+ ChannelMapperPtr m;
+ ConsistencyChecker checker;
+ std::list<BMscPtr> re = checker.check(b,m);
+ std::cout << re.size() << std::endl;
+
+ if(re.size() > 0){
+ std::cout << "vysledek" << std::endl;
+ z120.save_msc(std::cout,L"result",re.back());
+ }
+ else
+ std::cout << "neni" << std::endl;
+
// 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)
//
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
