Menu
▾
▴
[Scstudio-commits] SF.net SVN: scstudio:[939] trunk
|
From: <lko...@us...> - 2010-09-16 12:17:51
|
Revision: 939
http://scstudio.svn.sourceforge.net/scstudio/?rev=939&view=rev
Author: lkorenciak
Date: 2010-09-16 12:17:44 +0000 (Thu, 16 Sep 2010)
Log Message:
-----------
added returning of counterexamples when time consistency check is not satisfied + some minor fixes/changes in few other algorithms
Modified Paths:
--------------
trunk/src/check/liveness/deadlock_checker.cpp
trunk/src/check/time/find_block.cpp
trunk/src/check/time/find_block.h
trunk/src/check/time/tightening.h
trunk/src/check/time/time_consistency.h
trunk/src/data/time.h
trunk/tests/time/consistency/CMakeLists.txt
Modified: trunk/src/check/liveness/deadlock_checker.cpp
===================================================================
--- trunk/src/check/liveness/deadlock_checker.cpp 2010-09-16 12:14:08 UTC (rev 938)
+++ trunk/src/check/liveness/deadlock_checker.cpp 2010-09-16 12:17:44 UTC (rev 939)
@@ -44,7 +44,6 @@
{
HMscPathDuplicator duplicator;
HMscPtr example = duplicator.duplicate_path(path);
- MscElementPListList::const_iterator h;
MscElement* last = path.back().back();
duplicator.get_copy(last)->set_marked(true);
return example;
Modified: trunk/src/check/time/find_block.cpp
===================================================================
--- trunk/src/check/time/find_block.cpp 2010-09-16 12:14:08 UTC (rev 938)
+++ trunk/src/check/time/find_block.cpp 2010-09-16 12:17:44 UTC (rev 939)
@@ -69,7 +69,7 @@
}
}
}
- Block block= Block(trav->m_counter_of_blocks, n, n, 0, m_traverser.get_reached_elements());
+ Block block= Block(trav->m_counter_of_blocks, n, n, 0, m_traverser->get_reached_elements());
trav->m_list_of_blocks.push_back(block);
trav->m_last_block=trav->m_counter_of_blocks;
trav->m_open_constraints.insert(node_constraints.begin(), node_constraints.end());
Modified: trunk/src/check/time/find_block.h
===================================================================
--- trunk/src/check/time/find_block.h 2010-09-16 12:14:08 UTC (rev 938)
+++ trunk/src/check/time/find_block.h 2010-09-16 12:17:44 UTC (rev 939)
@@ -33,16 +33,16 @@
//complete virtual methods from WNFlistener and NFlistener
class SCTIME_EXPORT MyTraverse:public WhiteNodeFoundListener, public NodeFinishedListener
{
- DFSBMscGraphTraverser m_traverser;
+ DFSBMscGraphTraverser* m_traverser;
public:
TraverseAndMarkBlocks* trav;
- MyTraverse(DFSBMscGraphTraverser traverser)
+ MyTraverse(DFSBMscGraphTraverser* traverser)
{
m_traverser = traverser;
trav = NULL;
}
- MyTraverse(TraverseAndMarkBlocks* t,DFSBMscGraphTraverser traverser)
+ MyTraverse(TraverseAndMarkBlocks* t,DFSBMscGraphTraverser* traverser)
{
m_traverser = traverser;
trav=t;
@@ -71,6 +71,9 @@
:m_number(n),m_begin(begin),m_end(end),m_if_end(if_end)
{
m_path_to_block.clear();
+ std::cout<<"size of path (list of lists) we got: "<<list.size()<<" size of the first list: "<<std::endl;
+ if(list.size() == 0) std::cout<<"is empty"<<std::endl;
+ else std::cout<<list.back().size()<<std::endl;
for(MscElementPListList::iterator it = list.begin();it!=list.end();it++)
m_path_to_block.push_back(MscElementPList(it->begin(),it->end()));
}
@@ -140,7 +143,7 @@
//BMscGraphDuplicator* duplicator= new BMscGraphDuplicator();
//m_msc=duplicator->duplicate_hmsc(m_msc);
DFSBMscGraphTraverser traverser_block;
- MyTraverse my_trav(this,traverser_block);
+ MyTraverse my_trav(this,&traverser_block);
traverser_block.add_white_node_found_listener(&my_trav);
traverser_block.add_node_finished_listener(&my_trav);
traverser_block.traverse(m_msc);
Modified: trunk/src/check/time/tightening.h
===================================================================
--- trunk/src/check/time/tightening.h 2010-09-16 12:14:08 UTC (rev 938)
+++ trunk/src/check/time/tightening.h 2010-09-16 12:17:44 UTC (rev 939)
@@ -34,88 +34,88 @@
#include <utility>
/**
- * \brief tightens BMsc
+ * \brief
*/
-class AllCombination: public std::vector<std::pair<EventP,EventP> >
-{
-private:
- std::list<std::vector<std::pair<EventP,EventP> > > lists;
+// class AllCombination: public std::vector<std::pair<EventP,EventP> >
+// {
+// private:
+// std::list<std::vector<std::pair<EventP,EventP> > > lists;
+//
+// std::vector<std::vector<std::pair<EventP,EventP> > >* v_lists;
+// std::vector<size_type>* iterators;
+// bool ini;
+//
+// void set_value(size_t to)
+// {
+// for(size_t i= 0; i<= to;i++)
+// {
+// at(i)=((*v_lists)[i])[(*iterators)[i]];
+// }
+//
+// }
+//
+// bool move_next(size_t i)
+// {
+// if(i>=v_lists->size())
+// {
+// return false;
+// }
+//
+// (*iterators)[i]++;
+//
+// if((*iterators)[i]>=(*v_lists)[i].size())
+// {
+// (*iterators)[i]=0;
+// return move_next(++i);
+// }
+// set_value(i);
+// return true;
+// }
+//
+// public:
+// AllCombination():v_lists(NULL),iterators(NULL),ini(false)
+// {
+//
+// }
+//
+// ~AllCombination()
+// {
+// if(ini)
+// {
+// delete v_lists;
+// delete iterators;
+// }
+// }
+//
+// void add_list(std::vector<std::pair<EventP,EventP> > floor)
+// {
+// lists.push_back(floor);
+// }
+//
+// void init()
+// {
+// if(lists.size() == 0)
+// return ;
+// if(ini)
+// throw std::runtime_error("Already allocated!");
+// else
+// ini = true;
+//
+// v_lists = new std::vector<std::vector<std::pair<EventP,EventP> > >(lists.begin(),lists.end());
+// resize(lists.size());
+// iterators = new std::vector<size_type>(lists.size(),0);
+// set_value(lists.size()-1);
+// }
+//
+// bool move_next()
+// {
+// return move_next(0);
+// }
+//
+// };
- std::vector<std::vector<std::pair<EventP,EventP> > >* v_lists;
- std::vector<size_type>* iterators;
- bool ini;
- void set_value(size_t to)
- {
- for(size_t i= 0; i<= to;i++)
- {
- at(i)=((*v_lists)[i])[(*iterators)[i]];
- }
-
- }
-
- bool move_next(size_t i)
- {
- if(i>=v_lists->size())
- {
- return false;
- }
-
- (*iterators)[i]++;
-
- if((*iterators)[i]>=(*v_lists)[i].size())
- {
- (*iterators)[i]=0;
- return move_next(++i);
- }
- set_value(i);
- return true;
- }
-
-public:
- AllCombination():v_lists(NULL),iterators(NULL),ini(false)
- {
-
- }
-
- ~AllCombination()
- {
- if(ini)
- {
- delete v_lists;
- delete iterators;
- }
- }
-
- void add_list(std::vector<std::pair<EventP,EventP> > floor)
- {
- lists.push_back(floor);
- }
-
- void init()
- {
- if(lists.size() == 0)
- return ;
- if(ini)
- throw std::runtime_error("Already allocated!");
- else
- ini = true;
-
- v_lists = new std::vector<std::vector<std::pair<EventP,EventP> > >(lists.begin(),lists.end());
- resize(lists.size());
- iterators = new std::vector<size_type>(lists.size(),0);
- set_value(lists.size()-1);
- }
-
- bool move_next()
- {
- return move_next(0);
- }
-
-};
-
-
class TightenBMsc
{
@@ -225,7 +225,6 @@
-// std::stack<EventP> events_to_delete;
SRChannelMapperPtr srm = SRChannelMapper::instance();
BMscIntervalSetMatrix b_matrix(bmsc,m_causal,srm); // TODO: channelmapper
@@ -250,7 +249,6 @@
{
a = new StrictEvent();
b_matrix.add_event(a);
-// events_to_delete.push(a);
rel_to_event[top] = a;
MinimalEventPList min(in);
@@ -261,7 +259,7 @@
b_matrix.fill(a,copy,MscTimeIntervalD(0,D::infinity()));
floor.push_back(std::make_pair<EventP,EventP>(a,copy));
}
- combination.add_list(floor);
+ if(!min.empty()) combination.add_list(floor);
}
// open/close relations
@@ -299,7 +297,6 @@
{
a = new StrictEvent();
b_matrix.add_event(a);
-// events_to_delete.push(a);
rel_to_event[bottom] = a;
MaximalEventPList max(in);
std::vector<std::pair<EventP,EventP> > floor;
@@ -309,7 +306,7 @@
b_matrix.fill(copy,a,MscTimeIntervalD(0,D::infinity()));
floor.push_back(std::make_pair<EventP,EventP>(copy,a));
}
- combination.add_list(floor);
+ if(!max.empty()) combination.add_list(floor);
}
// open/close relations
@@ -354,15 +351,7 @@
MscSolveTCSP solve;
MscSolveTCSPReport report = solve.solveTCSP(b_matrix);
if(report.csp_mtxs.size()==0){ // inconsistent
-
- class InconsistencyException: public std::exception
- {
- virtual const char* what() const throw()
- {
- return "inconsistent BMSC, but should not be inconsistent";
- }
- } myex;
- throw myex;//TODO do something when inconsistent (e.g.exception). For consistency check this should return something reasonable
+ throw std::runtime_error("Inconsistent path, but should be consistent due to preconditions.");
}
return std::make_pair<BMscIntervalSetMatrix,IntervalSetMatrix>(b_matrix,report.m_matrix_result);
}
@@ -397,13 +386,7 @@
} while(combination.move_next());
-// while(!events_to_delete.empty()){
-// EventP p= events_to_delete.top();
-// events_to_delete.pop();
-// delete p;
-// }
-
return std::make_pair<BMscIntervalSetMatrix,IntervalSetMatrix>(b_matrix,result);
}
Modified: trunk/src/check/time/time_consistency.h
===================================================================
--- trunk/src/check/time/time_consistency.h 2010-09-16 12:14:08 UTC (rev 938)
+++ trunk/src/check/time/time_consistency.h 2010-09-16 12:17:44 UTC (rev 939)
@@ -20,8 +20,8 @@
#define TIME_H_CON
#include "time_pseudocode.h"
+//#include "tightening.h"
-
#include <limits>
#include <set>
#include <list>
@@ -29,6 +29,19 @@
#include <string>
#include <exception>
+
+#include "check/pseudocode/msc_duplicators.h"
+#include "hmsc_all_paths.h"
+#include "hmsc_block_paths.h"
+#include "traverse_erase.h"
+#include "data/dfs_hmsc_traverser.h"
+
+#include <iostream>
+
+#include "data/Z120/z120.h"
+#include <utility>
+
+
// #define _DEBUG
#ifdef _DEBUG
#include<iostream>
@@ -43,8 +56,19 @@
#define DEBUG_(x,y)
#endif
+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;
+struct MscSolveTCSPReport;
+class MscSolveTCSP;
+
+
+///////////////////////////////////////////////////////////////
+
class MscTimeInconsistencyException;
@@ -132,11 +156,6 @@
{}
}; // end of FloydWarshall
-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 BMscTighter;
@@ -222,11 +241,728 @@
};
-class SCTIME_EXPORT ConsistencyChecker: public Checker, public BMscChecker
+
+///////////////////////////////////////////////////////////////////
+
+class TemporaryStrictEvent: public StrictEvent
{
+ ReferenceNode* m_ref_node;
+ bool m_is_top;
+
public:
+ TemporaryStrictEvent(ReferenceNode* ref_node,bool is_top)
+ {
+ m_ref_node = ref_node;
+ m_is_top = is_top;
+ }
+
+ ReferenceNode* get_ref_node()
+ {
+ return m_ref_node;
+ }
+
+ bool is_top()
+ {
+ return m_is_top;
+ }
+};
+class TimeRelationRefNodeCycle: public WhiteNodeFoundListener, public GrayNodeFoundListener, public NodeFinishedListener
+{
+ std::map<TimeRelationRefNode*,MscElementPListList> m_open_relations;
+ std::map<TimeRelationRefNode*,MscElementPListList> m_cycle_relations;
+ DFSHMscTraverser* m_hmsc_traverser;
+
+public:
+ TimeRelationRefNodeCycle(DFSHMscTraverser* hmsc_traverser)
+ {
+ m_hmsc_traverser = hmsc_traverser;
+ }
+
+ ~TimeRelationRefNodeCycle()
+ {
+ }
+
+ //checks each of time relation events connected to node from parameter and if it is not in open_relations it adds it there,
+ //if it is open_relations it deletes the relation from there
+
+ void on_white_node_found(HMscNode* node)
+ {
+ std::cout<<"white node found, m_reached_elements size: "<< m_hmsc_traverser->get_reached_elements().size() <<std::endl;
+ ReferenceNode* ref_node = dynamic_cast<ReferenceNode*>(node);
+ if(!ref_node) { std::cout<<"white node finished"<<std::endl; return; }
+
+ TimeRelationRefNodePtrSet set = ref_node->get_time_relations_top();
+ TimeRelationRefNodePtrSet::iterator it;
+ std::map<TimeRelationRefNode*,MscElementPListList>::iterator it2;
+ for(it = set.begin();it!= set.end();it++)
+ {
+ it2 = m_open_relations.find(it->get());
+ if(it2 == m_open_relations.end())
+ {
+ it2 = m_cycle_relations.find(it->get());
+ if(it2 == m_cycle_relations.end())
+ {
+ std::cout<<"no relation found"<<std::endl;
+ MscElementPListList list;
+ m_open_relations.insert(std::make_pair<TimeRelationRefNode*,MscElementPListList>( it->get(),list));
+ }
+ else
+ {
+ std::cout<<"relation found in m_cycl relations, updating path"<<std::endl;
+ it2->second = m_hmsc_traverser->get_reached_elements(); //este sa da odobrat a vlozit znova
+ std::cout<<"update OK"<<std::endl;
+ }
+ }
+ else
+ {
+ std::cout<<"relation found"<<std::endl;
+ m_open_relations.erase(it2);
+ }
+ }
+
+ std::cout<<"top done, doing bottom"<<std::endl;
+
+ set = ref_node->get_time_relations_bottom();
+ for(it = set.begin();it!= set.end();it++)
+ {
+ it2 = m_open_relations.find(it->get());
+ if(it2 == m_open_relations.end())
+ {
+ it2 = m_cycle_relations.find(it->get());
+ if(it2 == m_cycle_relations.end())
+ {
+ std::cout<<"no relation found"<<std::endl;
+ MscElementPListList list;
+ m_open_relations.insert(std::make_pair<TimeRelationRefNode*,MscElementPListList>( it->get(),list));
+ }
+ else
+ {
+ std::cout<<"relation found in m_cycl relations, updating path"<<std::endl;
+ it2->second = m_hmsc_traverser->get_reached_elements(); //este sa da odobrat a vlozit znova
+ std::cout<<"update OK, list size which is added: "<<it2->second.size() << " suppose to be: "<<m_hmsc_traverser->get_reached_elements().size() << std::endl;
+ }
+ }
+ else
+ {
+ std::cout<<"relation found: "<<it->get()->get_interval_set()<<std::endl;
+ m_open_relations.erase(it2);
+ }
+ }
+ std::cout<<"white node finished"<<std::endl;
+ }
+
+ void on_gray_node_found(HMscNode* node)
+ {
+ std::cout<<"FFFFFFFFFFFFFFFFFFFFFFgray node found"<<std::endl;
+ for(std::map<TimeRelationRefNode*,MscElementPListList>::iterator it2=m_open_relations.begin();it2 != m_open_relations.end();it2++)
+ {
+ m_cycle_relations.insert(std::make_pair<TimeRelationRefNode*,MscElementPListList>( it2->first,it2->second)); //????
+ m_open_relations.erase(it2);
+ }
+ std::cout<<"gray node finished"<<std::endl;
+ }
+
+ void on_node_finished(HMscNode* node)
+ {
+ std::cout<<"on node finished"<<std::endl;
+
+ ReferenceNode* ref_node = dynamic_cast<ReferenceNode*>(node);
+ if(!ref_node) {std::cout<<"on node finished done"<<std::endl; return;}
+ TimeRelationRefNodePtrSet set = ref_node->get_time_relations_bottom();
+
+ TimeRelationRefNodePtrSet::iterator it;
+ std::map<TimeRelationRefNode*,MscElementPListList>::iterator it2;
+ for(it = set.begin();it!= set.end();it++)
+ {
+ it2 = m_open_relations.find(it->get());
+ if(it2 == m_open_relations.end())
+ {
+ it2 = m_cycle_relations.find(it->get());
+ if(it2 == m_cycle_relations.end())
+ {
+ m_open_relations.insert(std::make_pair<TimeRelationRefNode*,MscElementPListList>( it->get(),m_hmsc_traverser->get_reached_elements()));
+ }
+ else
+ {
+ //do nothing
+ }
+ }
+ else
+ {
+ m_open_relations.erase(it2);
+ }
+ }
+
+ set = ref_node->get_time_relations_top();
+ for(it = set.begin();it!= set.end();it++)
+ {
+ it2 = m_open_relations.find(it->get());
+ if(it2 == m_open_relations.end())
+ {
+ it2 = m_cycle_relations.find(it->get());
+ if(it2 == m_cycle_relations.end())
+ {
+ m_open_relations.insert(std::make_pair<TimeRelationRefNode*,MscElementPListList>( it->get(),m_hmsc_traverser->get_reached_elements()));
+ }
+ else
+ {
+ //do nothing
+ }
+ }
+ else
+ {
+ m_open_relations.erase(it2);
+ }
+ }
+ std::cout<<"on node finished done"<<std::endl;
+ }
+
+
+ std::map<TimeRelationRefNode*,MscElementPListList> get_cycle_relations()
+ {
+ return m_cycle_relations;
+ }
+
+};
+
+
+class AllCombination: public std::vector<std::pair<EventP,EventP> >
+{
+private:
+ std::list<std::vector<std::pair<EventP,EventP> > > lists;
+
+ std::vector<std::vector<std::pair<EventP,EventP> > >* v_lists;
+ std::vector<size_type>* iterators;
+ bool ini;
+
+ void set_value(size_t to)
+ {
+ for(size_t i= 0; i<= to;i++)
+ {
+ at(i)=((*v_lists)[i])[(*iterators)[i]];
+ }
+
+ }
+
+ bool move_next(size_t i)
+ {
+ if(i>=v_lists->size())
+ {
+ return false;
+ }
+
+ (*iterators)[i]++;
+
+ if((*iterators)[i]>=(*v_lists)[i].size())
+ {
+ (*iterators)[i]=0;
+ return move_next(++i);
+ }
+ set_value(i);
+ return true;
+ }
+
+public:
+ AllCombination():v_lists(NULL),iterators(NULL),ini(false)
+ {
+
+ }
+
+ ~AllCombination()
+ {
+ if(ini)
+ {
+ delete v_lists;
+ delete iterators;
+ }
+ }
+
+ void add_list(std::vector<std::pair<EventP,EventP> > floor)
+ {
+ lists.push_back(floor);
+ }
+
+ void init()
+ {
+ if(lists.size() == 0)
+ return ;
+ if(ini)
+ throw std::runtime_error("Already allocated!");
+ else
+ ini = true;
+
+ v_lists = new std::vector<std::vector<std::pair<EventP,EventP> > >(lists.begin(),lists.end());
+ resize(lists.size());
+ iterators = new std::vector<size_type>(lists.size(),0);
+ set_value(lists.size()-1);
+ }
+
+ bool move_next()
+ {
+ return move_next(0);
+ }
+
+};
+
+
+
+
+class SCTIME_EXPORT HMscConsistencyChecker: public PathFoundListener
+{
+
+ private:
+ bool m_causal;
+ std::list<Block>::iterator m_iter;
+ std::list<HMscPtr> m_final_result;
+public:
+ HMscConsistencyChecker():m_causal(false)
+ {
+
+ }
+
+ ~HMscConsistencyChecker()
+ {
+ }
+
+ virtual std::list<HMscPtr> check(HMscPtr hmsc, ChannelMapperPtr mapper)
+ {
+ //check whether the relations spanning across cycle contain infinity
+
+ std::cout<<"starting check"<<std::endl;
+ DFSHMscTraverser hmsc_traverser;
+ TimeRelationRefNodeCycle cycle_relations_finder(&hmsc_traverser);
+ hmsc_traverser.add_white_node_found_listener(&cycle_relations_finder);
+ hmsc_traverser.add_gray_node_found_listener(&cycle_relations_finder);
+ hmsc_traverser.add_node_finished_listener(&cycle_relations_finder);
+ hmsc_traverser.traverse(hmsc);
+
+ std::cout<<"traversed hmsc, marking relations"<<std::endl;
+
+ std::map<TimeRelationRefNode*,MscElementPListList> cycle_relations = cycle_relations_finder.get_cycle_relations();
+ std::cout<<"number of found cycle relations: "<<cycle_relations.size()<<std::endl;
+ std::map<TimeRelationRefNode*,MscElementPListList>::iterator it;
+ for(it = cycle_relations.begin();it != cycle_relations.end();it++)
+ {
+ std::cout<<"candidate for inconsistency"<<std::endl;
+ MscTimeIntervalD inter = (it->first)->get_interval_set().get_set().back(); //we assume that inteval sets are ordered (infty is last)
+ std::cout<<"checking infinity"<<std::endl;
+ if(!inter.is_upper_bound_infinity()) //check whether the interval set of time realtion contains infinity //the extension of time interval is needed
+ {
+ std::cout<<"found inconsistency"<<std::endl;
+ HMscPathDuplicator duplicator2;
+ (it->second);
+// std::cout<<"getting list: "<< std::endl;
+ MscElementPListList list3 = (it->second);
+// std::cout<<"list size: "<<std::endl;
+ HMscPtr ce_hmsc = duplicator2.duplicate_path(list3);
+// std::cout<<"duplicated, marking: "<< it->first<< " what is "<< inter <<std::endl;
+ //TODO update duplicator do duplicate also time relations, then use: duplicator2.get_copy(it->first)->set_marked();
+ TimeRelationRefNodePtr rel(new TimeRelationRefNode(inter));
+// std::cout<<"relation created"<<std::endl;
+ rel->glue_ref_nodes(it->first->is_bottom_node_a(),
+ dynamic_cast<ReferenceNode*>(duplicator2.get_copy(it->first->get_ref_node_a())),
+ it->first->is_bottom_node_b(),
+ dynamic_cast<ReferenceNode*>(duplicator2.get_copy(it->first->get_ref_node_b())));
+// std::cout<<"relation glued"<<std::endl;
+ rel->set_marked();
+ m_final_result.push_back(ce_hmsc);
+// std::cout<<"counterexample created. number of counterexmaples: "<< m_final_result.size()<<std::endl;
+ }
+ }
+
+ std::cout<<"relations marked, duplicating hmsc, finding blocks and running check on each path in block"<<std::endl;
+
+ HMscDuplicator duplicator;
+ HMscPtr result = duplicator.duplicate(hmsc);
+
+//maybe I can get rid of one duplication- TODO check the algorithm whether it will be correct
+
+ BMscGraphDuplicator graph_dup;
+ HMscPtr bmsc_graph = graph_dup.duplicate_hmsc(result);
+
+
+ TraverseAndMarkBlocks block_marker;
+ block_marker.travers_and_mark_blocks(bmsc_graph);
+
+
+// AllPathsAllBlocks block_to_path(block_marker.m_list_of_blocks,bmsc_graph);
+// block_to_path.set_listener(this);
+// block_to_path.all_paths_all_blocks();
+ int i=0;
+ for (m_iter = block_marker.m_list_of_blocks.begin(); m_iter != block_marker.m_list_of_blocks.end(); m_iter++) //iterate blocks
+ {
+ i++;
+// std::cout << "Cesty v " << i << " bloku" << std::endl;
+ HMscNodePtrSet m_last;
+ m_last.insert(m_iter->get_end());
+ AllPaths allpaths = AllPaths(bmsc_graph, m_iter->get_begin(), m_last, 1);
+
+ allpaths.add_path_found_listener(this);
+ allpaths.traverse();
+ m_last.clear();
+ }
+ std::cout<<"almost at the end. size of final_result: "<<m_final_result.size()<<std::endl;
+ return m_final_result;
+ }
+
+
+/**
+* \brief Tightens BMscGraph path and returns BMscIntervalSetMatrix with original constraints and IntervalSetMatrix with tightened constraints.
+*/
+ virtual void on_path_found(std::list<MscElement*>& path)
+ {
+ std::list<HMscPtr> counter_examples;
+ HMscFlatPathToBMscDuplicator duplicator;
+ BMscPtr bmsc = duplicator.duplicate_path(path);
+
+ SRChannelMapperPtr srm = SRChannelMapper::instance();
+ BMscIntervalSetMatrix b_matrix(bmsc,m_causal,srm); // TODO: channelmapper
+
+ std::map<BMsc*,int> bmsc_to_count;
+ std::map<const TimeRelationRefNodePtrSet*,EventP> rel_to_event;
+ std::set<TimeRelationRefNode*> open_rel;
+
+ Event* a;
+ AllCombination combination;
+ for(std::list<MscElement*>::iterator it=path.begin();it!=path.end();it++)
+ {
+ ReferenceNode* ref = dynamic_cast<ReferenceNode*>(*it);
+ if(ref==NULL)
+ continue;
+ BMscPtr in = ref->get_bmsc();
+ bmsc_to_count[in.get()]++; // @Warning initial integer number = 0?
+ TimeRelationRefNodePtrSet* top = &(ref->get_time_relations_top());
+ TimeRelationRefNodePtrSet* bottom = &(ref->get_time_relations_bottom());
+
+
+ if(top->size()>0)
+ {
+ a = new TemporaryStrictEvent(ref,true);
+ b_matrix.add_event(a);
+ rel_to_event[top] = a;
+
+ MinimalEventPList min(in);
+ std::vector<std::pair<EventP,EventP> > floor;
+ for(MinimalEventPList::iterator m=min.begin();m!=min.end();m++)
+ {
+ Event* copy = dynamic_cast<Event*>(duplicator.get_copy_with_occurence(*m,bmsc_to_count[in.get()]));
+ b_matrix.fill(a,copy,MscTimeIntervalD(0,D::infinity()));
+ floor.push_back(std::make_pair<EventP,EventP>(a,copy));
+ }
+ if(!min.empty()) combination.add_list(floor);
+
+ }
+ // open/close relations
+ for(TimeRelationRefNodePtrSet::const_iterator it=top->begin();it!=top->end();it++)
+ {
+ if(open_rel.find(it->get()) != open_rel.end())
+ {//time relation is open -> close it
+ const TimeRelationRefNodePtrSet* other;
+ //find the correct time relation (for getting previously created
+ // node to which the processed time relation (it*) should be connected)
+ if(ref==(*it)->get_ref_node_a()&&(*it)->is_top_node_a())
+ {
+ if((*it)->is_top_node_b())
+ other = &((*it)->get_ref_node_b()->get_time_relations_top());
+ else
+ other = &((*it)->get_ref_node_b()->get_time_relations_bottom());
+ }
+ else
+ {
+ if((*it)->is_top_node_a())
+ other = &((*it)->get_ref_node_a()->get_time_relations_top());
+ else
+ other = &((*it)->get_ref_node_a()->get_time_relations_bottom());
+ }
+ //fill the time relation to the matrix (node a was found later)
+ b_matrix.fill(rel_to_event[other],a,(*it)->get_interval_set());
+ b_matrix.tied_rel_to_cell(*it,rel_to_event[other],a);
+ }
+ else //time relation has not been opened yet -> open it
+ open_rel.insert((*it).get());
+
+ }
+
+ if(bottom->size()>0)
+ {
+ a = new TemporaryStrictEvent(ref,false);
+ b_matrix.add_event(a);
+ rel_to_event[bottom] = a;
+ MaximalEventPList max(in);
+ std::vector<std::pair<EventP,EventP> > floor;
+ for(MaximalEventPList::iterator m=max.begin();m!=max.end();m++)
+ {
+ Event* copy = dynamic_cast<Event*>(duplicator.get_copy_with_occurence(*m,bmsc_to_count[in.get()]));
+ b_matrix.fill(copy,a,MscTimeIntervalD(0,D::infinity()));
+ floor.push_back(std::make_pair<EventP,EventP>(copy,a));
+ }
+ if(!max.empty()) combination.add_list(floor);
+ }
+
+ // open/close relations
+ for(TimeRelationRefNodePtrSet::iterator it=bottom->begin();it!=bottom->end();it++)
+ {
+ if(open_rel.find(it->get()) != open_rel.end())
+ { //time relation is open -> close it
+ const TimeRelationRefNodePtrSet* other;
+ //find the correct time relation (for getting previously created
+ // node to which the processed time relation (it*) should be connected)
+ if(ref==(*it)->get_ref_node_a()&&(*it)->is_bottom_node_a())
+ {
+ if((*it)->is_top_node_b())
+ other = &((*it)->get_ref_node_b()->get_time_relations_top());
+ else
+ other = &((*it)->get_ref_node_b()->get_time_relations_bottom());
+ }
+ else
+ {
+ if((*it)->is_top_node_a())
+ other = &((*it)->get_ref_node_a()->get_time_relations_top());
+ else
+ other = &((*it)->get_ref_node_a()->get_time_relations_bottom());
+ }
+ //fill the time relation to the matrix (node a was found later)
+ b_matrix.fill(rel_to_event[other],a,(*it)->get_interval_set());
+ b_matrix.tied_rel_to_cell(*it,rel_to_event[other],a);
+ }
+ else //time relation has not been opened yet -> open it
+ open_rel.insert((*it).get());
+ }
+ }
+ b_matrix.build_up();
+
+
+ IntervalSetMatrix result;
+ result.resize(b_matrix.size());
+
+ combination.init();
+ if(combination.size()==0){
+ //tighten the matrix
+ MscSolveTCSP solve;
+ MscSolveTCSPReport report = solve.solveTCSP(b_matrix);
+ if(report.csp_mtxs.size()==0) // inconsistent
+ {
+ std::cout<<"report.inconsis_mtxs.size() == "<<report.inconsis_mtxs.size()<<std::endl;
+ m_final_result.push_back(make_counterexample(b_matrix,&report, path));
+ }
+ return ;
+ }
+
+ do
+ {
+ // push there [0,0] interval
+ for(unsigned i=0;i<combination.size();i++)
+ {
+ b_matrix.fill(combination[i].first,combination[i].second,MscTimeIntervalD(0,0));
+ }
+ MscSolveTCSP solve;
+ if(b_matrix.get_rel_empty_set().size()!=0) // inconsistent
+ throw std::runtime_error("inconsistent matrix - found empty time interval in matrix.");
+ MscSolveTCSPReport report = solve.solveTCSP(b_matrix);
+ if(report.csp_mtxs.size()!=0) // inconsistent => fill the values to result matrix
+ {
+ IntervalSetMatrix new_result = report.m_matrix_result;
+
+ for(unsigned i=0;i<new_result.size();i++)
+ for(unsigned j=0;j<new_result.size();j++)
+ result(i,j) = MscTimeIntervalSetD::set_union(result(i,j),new_result(i,j));
+ }
+ else
+ {
+ std::cout<<"report.inconsis_mtxs.size() == "<<report.inconsis_mtxs.size()<<std::endl;
+ counter_examples.push_back(make_counterexample(b_matrix,&report, path));
+ }
+
+
+ //return back previous values
+ for(unsigned i=0;i<combination.size();i++)
+ {
+ b_matrix.fill(combination[i].first,combination[i].second,MscTimeIntervalD(0,D::infinity()));
+ }
+
+ } while(combination.move_next());
+
+ if(result(0,0).get_set().empty())
+ m_final_result.insert(m_final_result.end(),counter_examples.begin(),counter_examples.end());
+
+ return ;
+ }
+
+//TODO nekopiruje sa dobre report, asi budem
+ HMscPtr make_counterexample(BMscIntervalSetMatrix b_matrix, MscSolveTCSPReport* report,std::list<MscElement*> path)
+ {
+ HMscPtr example;
+ std::cout<<"1 "<<std::endl;
+ MscElementPListList path_list = m_iter->get_path_to_block();
+ std::cout<<"1,5"<<std::endl;
+ if(path_list.size() > 1){
+ throw std::runtime_error("Found hierarchical path. Expected flat path.");
+ }
+ std::cout<<"1,7 size of path_list: "<< path_list.size()<< " size of path_list.back(): "<<std::endl;
+ std::cout << path_list.back().size()<<std::endl;
+ //concatenate paths and then duplicate
+ path.insert(path.begin(),path_list.back().begin(),path_list.back().end());
+/* MscElementPList::iterator it;
+ for(it=path_list.back().end();it!=path_list.back().begin();it--)
+ {
+ path.push_front(*it);
+ }*/
+
+ std::cout<<"XXXXXXXXXXXXXX 2"<<std::endl;
+ //set the last time constraint marked
+ MscTimeIntervalSetD last_interval;
+ TimeRelationEventPtrList rel_list;
+ TimeRelationEventPtr new_rel;
+ EventPVector events = b_matrix.get_events();
+ std::cout<<"report->inconsis_mtxs.size() == "<<report->inconsis_mtxs.size()<<std::endl;
+ for(unsigned int i = 0; i < report->inconsis_mtxs.size(); i++)
+ {
+ // mark the inconsistent time relation
+ last_interval = report->inconsis_mtxs[i](report->inconsis_indxs[i].first, report->inconsis_indxs[i].second);
+ HMscFlatPathDuplicator duplicator;
+ example = duplicator.duplicate_path(path);
+
+// m_final_result.push_back(example);
+ std::cout<<"2,5"<<std::endl;
+ Event* copy = events[report->inconsis_indxs[i].first];
+ std::cout<<"2,7. original of copy: "<<copy->get_original()<< std::endl;
+ if(copy->get_original()) //if we are taking care of event which did not previosly occur in the path, it does not have original
+ while(copy->get_original()->get_original()!=NULL)
+ {
+ copy = copy->get_original();
+ }
+
+ std::cout<<"3"<<std::endl;
+
+ EventP event_a = dynamic_cast<Event*>(duplicator.get_copy(copy));
+ std::cout<<"3,5"<<std::endl;
+ copy = events[report->inconsis_indxs[i].second];
+ if(copy->get_original())//if we are taking care of event which did not previosly occur in the path, it does not have original
+ while(copy->get_original()->get_original()!=NULL)
+ {
+ copy = copy->get_original();
+ }
+
+ EventP event_b = dynamic_cast<Event*>(duplicator.get_copy(copy));
+
+ std::cout<<"4"<<std::endl;
+
+ if(event_a && event_b && event_a->get_instance()->get_bmsc() == event_b->get_instance()->get_bmsc())
+ {
+ rel_list = TimeRelationsFunc::get(event_a,event_b);
+ DEBUG(rel_list.size());
+ switch(rel_list.size())
+ {
+ case 0:
+ {
+ new_rel = new TimeRelationEvent(last_interval);
+ new_rel->glue_events(event_a,event_b);
+ new_rel->set_marked();
+ break;
+ }
+ case 1:
+ rel_list.begin()->get()->set_marked();
+ break;
+ default:
+ throw std::runtime_error("More than one time relation between two events");
+ }
+ continue;
+ }
+ else
+ {
+ if(event_a)
+ {
+ event_a->set_marked();
+ }
+
+ if(event_b)
+ {
+ event_b->set_marked();
+ }
+ }
+
+ //marking of the hmsc nodes where are events causing inconsistency
+ MscElementPList::const_iterator elem;
+ ReferenceNode* ref;
+ TimeRelationRefNodePtrSet set;
+ TimeRelationRefNodePtrSet::iterator it;
+
+ if(event_a)
+ {
+ for(elem=path.begin();elem!=path.end();elem++)
+ {
+ ReferenceNode* r = dynamic_cast<ReferenceNode*>(*elem);
+ if(r && (r->get_bmsc().get() == event_a->get_instance()->get_bmsc()))
+ {
+ duplicator.get_copy(r)->set_marked();
+ }
+ }
+ }
+ else
+ {
+ event_a = events[report->inconsis_indxs[i].first];
+ TemporaryStrictEvent* t_s_event_a = dynamic_cast<TemporaryStrictEvent*>(event_a);
+
+ //marking the reference node
+ ref = t_s_event_a->get_ref_node();
+ duplicator.get_copy(ref)->set_marked();
+ //marking of all time realtions from the correct boundary of reference node
+ if(t_s_event_a->is_top())
+ set = ref->get_time_relations_top();
+ else
+ set = ref->get_time_relations_bottom();
+
+ for(it = set.begin();it != set.end();it++)
+ it->get()->set_marked();
+ }
+
+ if(event_b)
+ {
+ for(elem=path.begin();elem!=path.end();elem++)
+ {
+ ReferenceNode* r = dynamic_cast<ReferenceNode*>(*elem);
+ if(r && (r->get_bmsc().get() == event_b->get_instance()->get_bmsc()))
+ {
+ duplicator.get_copy(r)->set_marked();
+ }
+ }
+ }
+ else
+ {
+ event_b = events[report->inconsis_indxs[i].second];
+ TemporaryStrictEvent* t_s_event_b = dynamic_cast<TemporaryStrictEvent*>(event_b);
+ //marking the reference node
+ ref = t_s_event_b->get_ref_node();
+ duplicator.get_copy(ref)->set_marked();
+ //marking of all time realtions from the correct boundary of reference node
+ if(t_s_event_b->is_top())
+ set = ref->get_time_relations_top();
+ else
+ set = ref->get_time_relations_bottom();
+
+ for(it = set.begin();it != set.end();it++)
+ it->get()->set_marked();
+ }
+ }
+
+ return example;
+ }
+
+ void set_causal()
+ {
+ m_causal = true;
+ }
+};
+
+//////////////////////////////////////////////////////////////////////////////////
+
+class SCTIME_EXPORT ConsistencyChecker: public Checker, public BMscChecker, public HMscChecker
+{
+public:
+
+
virtual std::wstring get_property_name() const
{
return L"Time Consistent";
@@ -249,6 +985,14 @@
return precon_list;
}
+ virtual std::list<HMscPtr> check(HMscPtr hmsc, ChannelMapperPtr mapper)
+ {
+ HMscConsistencyChecker hmsc_checker;
+ std::list<HMscPtr> resultsXXX = hmsc_checker.check(hmsc,mapper);
+ std::cout<<"got some results: "<< resultsXXX.size()<<std::endl;
+ return resultsXXX;
+ }
+
virtual std::list<BMscPtr> check(BMscPtr bmsc, ChannelMapperPtr mapper)
{
std::list<BMscPtr> res_list;
Modified: trunk/src/data/time.h
===================================================================
--- trunk/src/data/time.h 2010-09-16 12:14:08 UTC (rev 938)
+++ trunk/src/data/time.h 2010-09-16 12:17:44 UTC (rev 939)
@@ -852,9 +852,18 @@
}
/**
- * \brief intersection of two interval
+ * \brief checks whether the upper bound of time interval is infinity
+ * @returns true if the upper bound of time interval is infinity, false otherwise
+ */
+ bool is_upper_bound_infinity()
+ {
+ return m_end.get_value() == std::numeric_limits<T>::infinity();
+ }
+
+/**
+ * \brief intersection of two intervals
* @returns intersection of two intervals
- * @warning returned interval does have to be valid, is_valid() may return false, CHECK FOR VALIDITY
+ * @warning returned interval has to be valid, is_valid() may return false, CHECK FOR VALIDITY
*/
Modified: trunk/tests/time/consistency/CMakeLists.txt
===================================================================
--- trunk/tests/time/consistency/CMakeLists.txt 2010-09-16 12:14:08 UTC (rev 938)
+++ trunk/tests/time/consistency/CMakeLists.txt 2010-09-16 12:17:44 UTC (rev 939)
@@ -1,3 +1,19 @@
+ADD_CHECKER_TEST(sctime "Time Consistent" cons_pos_1.mpr 1)
+ADD_CHECKER_TEST(sctime "Time Consistent" cons_pos_2.mpr 1)
+ADD_CHECKER_TEST(sctime "Time Consistent" cons_pos_3.mpr 1)
+ADD_CHECKER_TEST(sctime "Time Consistent" cons_pos_4.mpr 1)
+ADD_CHECKER_TEST(sctime "Time Consistent" cons_pos_5.mpr 1)
+ADD_CHECKER_TEST(sctime "Time Consistent" cons_pos_6.mpr 1)
+ADD_CHECKER_TEST(sctime "Time Consistent" cons_pos_7.mpr 1)
+ADD_CHECKER_TEST(sctime "Time Consistent" cons_pos_8.mpr 1)
+ADD_CHECKER_TEST(sctime "Time Consistent" cons_pos_9.mpr 1)
+ADD_CHECKER_TEST(sctime "Time Consistent" cons_pos_10.mpr 1)
+ADD_CHECKER_TEST(sctime "Time Consistent" cons_pos_11.mpr 1)
+ADD_CHECKER_TEST(sctime "Time Consistent" cons_pos_12.mpr 1)
+ADD_CHECKER_TEST(sctime "Time Consistent" cons_pos_13.mpr 1)
+ADD_CHECKER_TEST(sctime "Time Consistent" cons_pos_14.mpr 1)
+ADD_CHECKER_TEST(sctime "Time Consistent" cons_pos_15.mpr 1)
+
ADD_CHECKER_TEST(sctime "Time Consistent" cons_neg_1.mpr 0)
ADD_CHECKER_TEST(sctime "Time Consistent" cons_neg_2.mpr 0)
ADD_CHECKER_TEST(sctime "Time Consistent" cons_neg_3.mpr 0)
@@ -12,4 +28,26 @@
ADD_CHECKER_TEST(sctime "Time Consistent" cons_neg_13.mpr 0)
ADD_CHECKER_TEST(sctime "Time Consistent" cons_neg_15.mpr 0)
ADD_CHECKER_TEST(sctime "Time Consistent" cons_neg_16.mpr 0)
+ADD_CHECKER_TEST(sctime "Time Consistent" cons_neg_17.mpr 0)
+# ADD_CHECKER_TEST(sctime "Time Consistent" cons_neg_18.mpr 0)
+# ADD_CHECKER_TEST(sctime "Time Consistent" cons_neg_19.mpr 0)
+# ADD_CHECKER_TEST(sctime "Time Consistent" cons_neg_20.mpr 0)
+# ADD_CHECKER_TEST(sctime "Time Consistent" cons_neg_21.mpr 0)
+# ADD_CHECKER_TEST(sctime "Time Consistent" cons_neg_22.mpr 0)
+ADD_CHECKER_TEST(sctime "Time Consistent" cons_neg_23.mpr 0)
+# ADD_CHECKER_TEST(sctime "Time Consistent" cons_neg_24.mpr 0)
+# ADD_CHECKER_TEST(sctime "Time Consistent" cons_neg_25.mpr 0)
+# ADD_CHECKER_TEST(sctime "Time Consistent" cons_neg_26.mpr 0)
+# ADD_CHECKER_TEST(sctime "Time Consistent" cons_neg_27.mpr 0)
+ADD_CHECKER_TEST(sctime "Time Consistent" cons_neg_28.mpr 0)
+ADD_CHECKER_TEST(sctime "Time Consistent" cons_neg_29.mpr 0)
+ADD_CHECKER_TEST(sctime "Time Consistent" cons_neg_30.mpr 0)
+ADD_CHECKER_TEST(sctime "Time Consistent" cons_neg_31.mpr 0)
+ADD_CHECKER_TEST(sctime "Time Consistent" cons_neg_32.mpr 0)
+ADD_CHECKER_TEST(sctime "Time Consistent" cons_neg_33.mpr 0)
+ADD_CHECKER_TEST(sctime "Time Consistent" cons_neg_34.mpr 0)
ADD_CHECKER_TEST(sctime "Time Consistent" cons_neg_35.mpr 0)
+ADD_CHECKER_TEST(sctime "Time Consistent" cons_neg_36.mpr 0)
+ADD_CHECKER_TEST(sctime "Time Consistent" cons_neg_37.mpr 0)
+ADD_CHECKER_TEST(sctime "Time Consistent" cons_neg_38.mpr 0)
+ADD_CHECKER_TEST(sctime "Time Consistent" cons_neg_39.mpr 0)
\ No newline at end of file
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
