Menu
▾
▴
[Scstudio-commits] SF.net SVN: scstudio:[582] trunk
|
From: <va...@us...> - 2010-02-10 20:47:07
|
Revision: 582
http://scstudio.svn.sourceforge.net/scstudio/?rev=582&view=rev
Author: vacek
Date: 2010-02-10 20:46:58 +0000 (Wed, 10 Feb 2010)
Log Message:
-----------
Halfway to multiple results of checkers - interface change. Behaviour to be done.
Modified Paths:
--------------
trunk/src/check/boundedness/universal_boundedness_checker.cpp
trunk/src/check/boundedness/universal_boundedness_checker.h
trunk/src/check/liveness/deadlock_checker.cpp
trunk/src/check/liveness/deadlock_checker.h
trunk/src/check/liveness/livelock_checker.cpp
trunk/src/check/liveness/livelock_checker.h
trunk/src/check/localchoice/local_choice_checker.cpp
trunk/src/check/localchoice/local_choice_checker.h
trunk/src/check/order/acyclic_checker.cpp
trunk/src/check/order/acyclic_checker.h
trunk/src/check/order/fifo_checker.cpp
trunk/src/check/order/fifo_checker.h
trunk/src/check/race/race_checker.cpp
trunk/src/check/race/race_checker.h
trunk/src/check/realizability/realizability_checker.cpp
trunk/src/check/realizability/realizability_checker.h
trunk/src/check/structure/name_checker.cpp
trunk/src/check/structure/name_checker.h
trunk/src/check/structure/nonrecursivity_checker.cpp
trunk/src/check/structure/nonrecursivity_checker.h
trunk/src/check/time/constraint_syntax.cpp
trunk/src/check/time/constraint_syntax.h
trunk/src/check/time/time_consistency.h
trunk/src/data/checker.h
trunk/src/data/hmsc_reference_checker.h
trunk/src/view/visio/addon/document.cpp
trunk/tests/acyclic_checker_test.cpp
trunk/tests/checker_test.cpp
trunk/tests/deadlock_checker_test.cpp
trunk/tests/fifo_checker_test.cpp
trunk/tests/livelock_checker_test.cpp
trunk/tests/local_choice_checker_test.cpp
trunk/tests/race_checker_test.cpp
trunk/tests/universal_boundedness_checker_test.cpp
Modified: trunk/src/check/boundedness/universal_boundedness_checker.cpp
===================================================================
--- trunk/src/check/boundedness/universal_boundedness_checker.cpp 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/src/check/boundedness/universal_boundedness_checker.cpp 2010-02-10 20:46:58 UTC (rev 582)
@@ -147,7 +147,7 @@
return p;
}
-HMscPtr UniversalBoundednessChecker::check(HMscPtr hmsc, ChannelMapperPtr chm)
+std::list<HMscPtr> UniversalBoundednessChecker::check(HMscPtr hmsc, ChannelMapperPtr chm)
{
DFSHMscTraverser name_traverser("UB_color");
NameCollector name_collector;
@@ -191,8 +191,9 @@
msc_traverser.add_white_node_found_listener(&cleaner);
msc_traverser.traverse(transformed);
-
- return p;
+ std::list<HMscPtr> result;
+ result.push_back(p);
+ return result;
}
void UniversalBoundednessChecker::cleanup_attributes()
Modified: trunk/src/check/boundedness/universal_boundedness_checker.h
===================================================================
--- trunk/src/check/boundedness/universal_boundedness_checker.h 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/src/check/boundedness/universal_boundedness_checker.h 2010-02-10 20:46:58 UTC (rev 582)
@@ -155,7 +155,7 @@
/**
* Checks whether hmsc satisfy universal boundedness property.
*/
- HMscPtr check(HMscPtr hmsc, ChannelMapperPtr chm);
+ std::list<HMscPtr> check(HMscPtr hmsc, ChannelMapperPtr chm);
/**
* Cleans up no more needed attributes.
Modified: trunk/src/check/liveness/deadlock_checker.cpp
===================================================================
--- trunk/src/check/liveness/deadlock_checker.cpp 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/src/check/liveness/deadlock_checker.cpp 2010-02-10 20:46:58 UTC (rev 582)
@@ -145,7 +145,7 @@
return example;
}
-HMscPtr DeadlockChecker::check(HMscPtr hmsc, ChannelMapperPtr chm)
+std::list<HMscPtr> DeadlockChecker::check(HMscPtr hmsc, ChannelMapperPtr chm)
{
//this will be used do show eventual counterexample
HMscPtr p;
@@ -163,7 +163,9 @@
p = create_counter_example(traverser.get_reached_elements());
traverser.cleanup_traversing_attributes();
}
- return p;
+ std::list<HMscPtr> result;
+ result.push_back(p);
+ return result;
}
void DeadlockChecker::cleanup_attributes()
Modified: trunk/src/check/liveness/deadlock_checker.h
===================================================================
--- trunk/src/check/liveness/deadlock_checker.h 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/src/check/liveness/deadlock_checker.h 2010-02-10 20:46:58 UTC (rev 582)
@@ -142,7 +142,7 @@
/**
* Checks whether hmsc satisfy deadlock free property.
*/
- HMscPtr check(HMscPtr hmsc, ChannelMapperPtr chm);
+ std::list<HMscPtr> check(HMscPtr hmsc, ChannelMapperPtr chm);
/**
* Cleans up no more needed attributes.
Modified: trunk/src/check/liveness/livelock_checker.cpp
===================================================================
--- trunk/src/check/liveness/livelock_checker.cpp 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/src/check/liveness/livelock_checker.cpp 2010-02-10 20:46:58 UTC (rev 582)
@@ -66,7 +66,7 @@
return result;
}
-HMscPtr LivelockChecker::check(HMscPtr hmsc, ChannelMapperPtr chm)
+std::list<HMscPtr> LivelockChecker::check(HMscPtr hmsc, ChannelMapperPtr chm)
{
HMscPtr p;
//mark nodes that path to EndNode exists from
@@ -87,7 +87,9 @@
{
p = create_counter_example(traverser.get_reached_elements());
}
- return p;
+ std::list<HMscPtr> result;
+ result.push_back(p);
+ return result;
}
LivelockChecker::LivelockChecker()
Modified: trunk/src/check/liveness/livelock_checker.h
===================================================================
--- trunk/src/check/liveness/livelock_checker.h 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/src/check/liveness/livelock_checker.h 2010-02-10 20:46:58 UTC (rev 582)
@@ -119,7 +119,7 @@
~LivelockChecker();
- HMscPtr check(HMscPtr h, ChannelMapperPtr chm);
+ std::list<HMscPtr> check(HMscPtr h, ChannelMapperPtr chm);
void cleanup_attributes();
Modified: trunk/src/check/localchoice/local_choice_checker.cpp
===================================================================
--- trunk/src/check/localchoice/local_choice_checker.cpp 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/src/check/localchoice/local_choice_checker.cpp 2010-02-10 20:46:58 UTC (rev 582)
@@ -205,7 +205,7 @@
}
-HMscPtr LocalChoiceChecker::check(HMscPtr hmsc, ChannelMapperPtr chm)
+std::list<HMscPtr> LocalChoiceChecker::check(HMscPtr hmsc, ChannelMapperPtr chm)
{
HMscPtr transformed = m_graph_duplicator.duplicate_hmsc(hmsc);
DFSRefNodeHMscTraverser ref_traverser;
@@ -241,7 +241,10 @@
ref_traverser.add_white_node_found_listener(&cl_list);
ref_traverser.traverse(transformed);
m_graph_duplicator.cleanup_attributes();
- return p;
+
+ std::list<HMscPtr> result;
+ result.push_back(p);
+ return result;
}
void LocalChoiceChecker::cleanup_attributes(void)
Modified: trunk/src/check/localchoice/local_choice_checker.h
===================================================================
--- trunk/src/check/localchoice/local_choice_checker.h 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/src/check/localchoice/local_choice_checker.h 2010-02-10 20:46:58 UTC (rev 582)
@@ -144,7 +144,7 @@
/**
* Checks whether hmsc satisfy universal boundedness property.
*/
- HMscPtr check(HMscPtr hmsc, ChannelMapperPtr chm);
+ std::list<HMscPtr> check(HMscPtr hmsc, ChannelMapperPtr chm);
/**
* Cleans up no more needed attributes.
Modified: trunk/src/check/order/acyclic_checker.cpp
===================================================================
--- trunk/src/check/order/acyclic_checker.cpp 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/src/check/order/acyclic_checker.cpp 2010-02-10 20:46:58 UTC (rev 582)
@@ -47,7 +47,7 @@
return new_bmsc;
}
-BMscPtr AcyclicChecker::check(BMscPtr bmsc, ChannelMapperPtr chm)
+std::list<BMscPtr> AcyclicChecker::check(BMscPtr bmsc, ChannelMapperPtr chm)
{
AcyclicCheckerListener listener;
DFSEventsTraverser traverser;
@@ -61,7 +61,9 @@
{
result = create_counter_example(bmsc,traverser.get_reached_elements());
}
- return result;
+ std::list<BMscPtr> res;
+ res.push_back(result);
+ return res;
}
void AcyclicChecker::cleanup_attributes()
Modified: trunk/src/check/order/acyclic_checker.h
===================================================================
--- trunk/src/check/order/acyclic_checker.h 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/src/check/order/acyclic_checker.h 2010-02-10 20:46:58 UTC (rev 582)
@@ -80,7 +80,7 @@
/**
* Checks whether bmsc has acyclic events' dependecy
*/
- BMscPtr check(BMscPtr bmsc, ChannelMapperPtr chm);
+ std::list<BMscPtr> check(BMscPtr bmsc, ChannelMapperPtr chm);
/**
* Cleans up no more needed attributes.
Modified: trunk/src/check/order/fifo_checker.cpp
===================================================================
--- trunk/src/check/order/fifo_checker.cpp 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/src/check/order/fifo_checker.cpp 2010-02-10 20:46:58 UTC (rev 582)
@@ -45,7 +45,7 @@
return new_bmsc;
}
-BMscPtr FifoChecker::check(BMscPtr bmsc, ChannelMapperPtr mapper)
+std::list<BMscPtr> FifoChecker::check(BMscPtr bmsc, ChannelMapperPtr mapper)
{
ChannelMapperPtr chm = mapper->copy();
VisualClosureInitiator closure_initiator;
@@ -73,12 +73,16 @@
{
result = create_counter_example(bmsc,topology[e],topology[f]);
cleanup_attributes();
- return result;
+ std::list<BMscPtr> res;
+ res.push_back(result);
+ return res;
}
}
}
cleanup_attributes();
- return result;
+ std::list<BMscPtr> res;
+ res.push_back(result);
+ return res;
}
void FifoChecker::cleanup_attributes()
Modified: trunk/src/check/order/fifo_checker.h
===================================================================
--- trunk/src/check/order/fifo_checker.h 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/src/check/order/fifo_checker.h 2010-02-10 20:46:58 UTC (rev 582)
@@ -114,7 +114,7 @@
/**
* Checks whether bmsc contains overtaking messages.
*/
- BMscPtr check(BMscPtr bmsc, ChannelMapperPtr mapper);
+ std::list<BMscPtr> check(BMscPtr bmsc, ChannelMapperPtr mapper);
void cleanup_attributes();
Modified: trunk/src/check/race/race_checker.cpp
===================================================================
--- trunk/src/check/race/race_checker.cpp 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/src/check/race/race_checker.cpp 2010-02-10 20:46:58 UTC (rev 582)
@@ -305,11 +305,13 @@
return result;
}
-BMscPtr RaceChecker::check(BMscPtr bmsc, ChannelMapperPtr mapper)
+std::list<BMscPtr> RaceChecker::check(BMscPtr bmsc, ChannelMapperPtr mapper)
{
BMscPtr b = check_bmsc(bmsc,mapper);
cleanup_attributes();
- return b;
+ std::list<BMscPtr> result;
+ result.push_back(b);
+ return result;
}
void RaceChecker::cleanup_attributes()
@@ -337,7 +339,7 @@
}
-HMscPtr RaceChecker::check(HMscPtr hmsc, ChannelMapperPtr mapper)
+std::list<HMscPtr> RaceChecker::check(HMscPtr hmsc, ChannelMapperPtr mapper)
{
//transform hmsc into BMsc graph
HMscPtr transformed = m_graph_duplicator.duplicate_hmsc(hmsc);
@@ -346,14 +348,18 @@
if(res.get())
{
cleanup_attributes();
- return res;
+ std::list<HMscPtr> result;
+ result.push_back(res);
+ return result;
}
//precompute possible things for race checking - e.g. MinP
prepare_hmsc(transformed,mapper);
//check hmsc to be race free
HMscPtr error = check_hmsc(transformed,mapper);
cleanup_attributes();
- return error;
+ std::list<HMscPtr> result;
+ result.push_back(error);
+ return result;
}
HMscPtr RaceChecker::check_hmsc(HMscPtr hmsc,ChannelMapperPtr mapper)
Modified: trunk/src/check/race/race_checker.h
===================================================================
--- trunk/src/check/race/race_checker.h 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/src/check/race/race_checker.h 2010-02-10 20:46:58 UTC (rev 582)
@@ -238,9 +238,9 @@
BMscPtr check_bmsc(BMscPtr bmsc, ChannelMapperPtr mapper);
- BMscPtr check(BMscPtr bmsc, ChannelMapperPtr mapper);
+ std::list<BMscPtr> check(BMscPtr bmsc, ChannelMapperPtr mapper);
- HMscPtr check(HMscPtr hmsc, ChannelMapperPtr mapper);
+ std::list<HMscPtr> check(HMscPtr hmsc, ChannelMapperPtr mapper);
void cleanup_attributes();
Modified: trunk/src/check/realizability/realizability_checker.cpp
===================================================================
--- trunk/src/check/realizability/realizability_checker.cpp 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/src/check/realizability/realizability_checker.cpp 2010-02-10 20:46:58 UTC (rev 582)
@@ -22,9 +22,11 @@
-HMscPtr RealizabilityChecker::check(HMscPtr hmsc, ChannelMapperPtr chm)
+std::list<HMscPtr> RealizabilityChecker::check(HMscPtr hmsc, ChannelMapperPtr chm)
{
- return NULL;
+ std::list<HMscPtr> result;
+ result.push_back(NULL);
+ return result;
}
Modified: trunk/src/check/realizability/realizability_checker.h
===================================================================
--- trunk/src/check/realizability/realizability_checker.h 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/src/check/realizability/realizability_checker.h 2010-02-10 20:46:58 UTC (rev 582)
@@ -59,7 +59,7 @@
/**
* Checks whether hmsc satisfy universal boundedness property.
*/
- HMscPtr check(HMscPtr hmsc, ChannelMapperPtr chm);
+ std::list<HMscPtr> check(HMscPtr hmsc, ChannelMapperPtr chm);
/**
* Cleans up no more needed attributes.
Modified: trunk/src/check/structure/name_checker.cpp
===================================================================
--- trunk/src/check/structure/name_checker.cpp 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/src/check/structure/name_checker.cpp 2010-02-10 20:46:58 UTC (rev 582)
@@ -158,7 +158,7 @@
}
-BMscPtr NameChecker::check(BMscPtr bmsc, ChannelMapperPtr chm)
+std::list<BMscPtr> NameChecker::check(BMscPtr bmsc, ChannelMapperPtr chm)
{
HMscPtr hmsc1(new HMsc(L"HMsc1"));
StartNodePtr start1 = new StartNode();
@@ -170,8 +170,9 @@
start1->add_successor(r1_1.get());
r1_1->add_successor(end1.get());
r1_1->set_msc(bmsc);
+ std::list<BMscPtr> result;
- HMscPtr r = check(hmsc1, chm);
+ HMscPtr r = check(hmsc1, chm).front();
if(r)
{
DFSHMscTraverser first_node_traverser;
@@ -183,14 +184,20 @@
}
catch(FirstNodeFoundException)
{
- return dynamic_cast<ReferenceNode*>(first_node_traverser.get_reached_elements().back().back())->get_bmsc();
+ result.push_back(dynamic_cast<ReferenceNode*>(first_node_traverser.get_reached_elements().back().back())->get_bmsc());
+ return result;
+
}
- return NULL; //just to avoid compiler warning - this line is actually not reachable
+ result.push_back(NULL);
+ return result; //just to avoid compiler warning - this line is actually not reachable
}
else
- return NULL;
+ {
+ result.push_back(NULL);
+ return result;
+ }
}
-HMscPtr NameChecker::check(HMscPtr hmsc, ChannelMapperPtr chm)
+std::list<HMscPtr> NameChecker::check(HMscPtr hmsc, ChannelMapperPtr chm)
{
DFSHMscTraverser name_traverser, first_node_traverser;
NameListener n_ch;
@@ -199,7 +206,7 @@
MscElementPListList path_to_first;
name_traverser.add_white_node_found_listener(&n_ch);
first_node_traverser.add_white_node_found_listener(&ffnl);
-
+ std::list<HMscPtr> result;
try
{
first_node_traverser.traverse(hmsc);
@@ -219,7 +226,8 @@
p = create_duplicate_counter_example(name_traverser.get_reached_elements(), err.get_name());
name_traverser.cleanup_traversing_attributes();
m_graph_duplicator.cleanup_attributes();
- return p;
+ result.push_back(p);
+ return result;
}
catch(InconsistentNamesException)
@@ -227,9 +235,10 @@
p = create_inconsistent_counter_example(name_traverser.get_reached_elements(), path_to_first);
name_traverser.cleanup_traversing_attributes();
m_graph_duplicator.cleanup_attributes();
- return p;
+ result.push_back(p);
+ return result;
}
- return NULL;
+ return result;
}
void NameChecker::cleanup_attributes()
Modified: trunk/src/check/structure/name_checker.h
===================================================================
--- trunk/src/check/structure/name_checker.h 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/src/check/structure/name_checker.h 2010-02-10 20:46:58 UTC (rev 582)
@@ -146,9 +146,9 @@
/**
* Checks whether a given hmsc contains consistent set of instances.
*/
- HMscPtr check(HMscPtr hmsc, ChannelMapperPtr chm);
+ std::list<HMscPtr> check(HMscPtr hmsc, ChannelMapperPtr chm);
- BMscPtr check(BMscPtr bmsc, ChannelMapperPtr chm);
+ std::list<BMscPtr> check(BMscPtr bmsc, ChannelMapperPtr chm);
/**
* Cleans up no more needed attributes.
Modified: trunk/src/check/structure/nonrecursivity_checker.cpp
===================================================================
--- trunk/src/check/structure/nonrecursivity_checker.cpp 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/src/check/structure/nonrecursivity_checker.cpp 2010-02-10 20:46:58 UTC (rev 582)
@@ -53,14 +53,14 @@
return example;
}
-HMscPtr NonrecursivityChecker::check(HMscPtr hmsc, ChannelMapperPtr chm)
+std::list<HMscPtr> NonrecursivityChecker::check(HMscPtr hmsc, ChannelMapperPtr chm)
{
DFSHMscTraverser recursive_traverser;
RecursivityListener rec_listener;
HMscPtr p(NULL);
recursive_traverser.add_gray_node_found_listener(&rec_listener);
+ std::list<HMscPtr> result;
-
try
{
recursive_traverser.traverse(hmsc);
@@ -69,10 +69,11 @@
{
p = create_counter_example(recursive_traverser.get_reached_elements());
recursive_traverser.cleanup_traversing_attributes();
- return p;
+ result.push_back(p);
+ return result;
}
-
- return NULL;
+ result.push_back(NULL);
+ return result;
}
void NonrecursivityChecker::cleanup_attributes()
Modified: trunk/src/check/structure/nonrecursivity_checker.h
===================================================================
--- trunk/src/check/structure/nonrecursivity_checker.h 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/src/check/structure/nonrecursivity_checker.h 2010-02-10 20:46:58 UTC (rev 582)
@@ -77,7 +77,7 @@
/**
* Checks whether a given hmsc contains consistent set of instances.
*/
- HMscPtr check(HMscPtr hmsc, ChannelMapperPtr chm);
+ std::list<HMscPtr> check(HMscPtr hmsc, ChannelMapperPtr chm);
/**
* Cleans up no more needed attributes.
Modified: trunk/src/check/time/constraint_syntax.cpp
===================================================================
--- trunk/src/check/time/constraint_syntax.cpp 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/src/check/time/constraint_syntax.cpp 2010-02-10 20:46:58 UTC (rev 582)
@@ -42,11 +42,12 @@
}
}
-HMscPtr ConstraintsChecker::check(HMscPtr hmsc, ChannelMapperPtr mapper)
+std::list<HMscPtr> ConstraintsChecker::check(HMscPtr hmsc, ChannelMapperPtr mapper)
{
+ std::list<HMscPtr> result;
// empty hmsc handler
if(!hmsc.get())
- return NULL;
+ return result;
m_changed = false;
DFSHMscFlatTraverser traverser("ConstraintsChecker");
@@ -62,19 +63,25 @@
inner_hmsc_found(m_copy,NULL);
tra.traverse(m_copy);
if(!m_changed)
- return NULL;
+ {
+ result.push_back(NULL);
+ return result;
+ }
mark();
m_tra=NULL;
- return m_copy;
+ result.push_back(m_copy);
+ return result;
}
- BMscPtr ConstraintsChecker::check(BMscPtr bmsc, ChannelMapperPtr mapper)
+ std::list<BMscPtr> ConstraintsChecker::check(BMscPtr bmsc, ChannelMapperPtr mapper)
{
+ std::list<BMscPtr> result;
BMscPtr ret;
BMscConstraintCheck checker;
ret = checker.check(bmsc);
- return ret;
+ result.push_back(ret);
+ return result;
}
void ConstraintsChecker::mark()
Modified: trunk/src/check/time/constraint_syntax.h
===================================================================
--- trunk/src/check/time/constraint_syntax.h 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/src/check/time/constraint_syntax.h 2010-02-10 20:46:58 UTC (rev 582)
@@ -73,8 +73,8 @@
ConstraintsChecker(): m_changed(false)
{}
- BMscPtr check(BMscPtr, ChannelMapperPtr);
- HMscPtr check(HMscPtr, ChannelMapperPtr);
+ std::list<BMscPtr> check(BMscPtr, ChannelMapperPtr);
+ std::list<HMscPtr> check(HMscPtr, ChannelMapperPtr);
void on_new_inner_bmsc_found(BMscPtr bmsc, ReferenceNode* refNode);
Modified: trunk/src/check/time/time_consistency.h
===================================================================
--- trunk/src/check/time/time_consistency.h 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/src/check/time/time_consistency.h 2010-02-10 20:46:58 UTC (rev 582)
@@ -215,15 +215,16 @@
return precon_list;
}
- virtual BMscPtr check(BMscPtr bmsc, ChannelMapperPtr mapper)
+ virtual std::list<BMscPtr> check(BMscPtr bmsc, ChannelMapperPtr mapper)
{
BMscIntervalSetMatrix matrix(bmsc);
MscSolveTCSP solve;
MscSolveTCSPReport report = solve.solveTCSP(matrix);
+ std::list<BMscPtr> res_list;
// there was at least one matrix found -> consistent
if(report.csp_mtxs.size()!=0)
- return NULL;
+ return res_list;
/* ok, incosistency was found, so pick the last inconsistent
@@ -265,7 +266,8 @@
throw std::runtime_error("More than one time relation between two events");
}
- return matrix.get_modified_bmsc();
+ res_list.push_back(matrix.get_modified_bmsc());
+ return res_list;
}
virtual void cleanup_attributes()
Modified: trunk/src/data/checker.h
===================================================================
--- trunk/src/data/checker.h 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/src/data/checker.h 2010-02-10 20:46:58 UTC (rev 582)
@@ -106,12 +106,12 @@
/**
* Checks HMsc against specific property.
*
- * Returns MscPathPtr with violating example if there is any in hmsc
- * otherwise HMscPathPtr is undefined.
+ * Returns a list of MscPathPtr with violating examples if there are any in hmsc
+ * otherwise the list is empty.
* @param hmsc - HMsc to be checked
* @param mapper - ChannelMapper which is chosen as delivery semantic
*/
- virtual HMscPtr check(HMscPtr hmsc, ChannelMapperPtr mapper)=0;
+ virtual std::list<HMscPtr> check(HMscPtr hmsc, ChannelMapperPtr mapper)=0;
};
/**
@@ -133,12 +133,12 @@
/**
* Checks BMsc against specific property.
*
- * Returns BMscPtr with violating example if there is any in bmsc otherwise
- * BMscPtr is undefined.
+ * Returns a list of BMscPtr with violating examples if there are any in bmsc otherwise
+ * the list is empty.
* @param bmsc - BMsc to be checked
* @param mapper - ChannelMapper which is chosen as delivery semantic
*/
- virtual BMscPtr check(BMscPtr bmsc, ChannelMapperPtr mapper)=0;
+ virtual std::list<BMscPtr> check(BMscPtr bmsc, ChannelMapperPtr mapper)=0;
};
/**
Modified: trunk/src/data/hmsc_reference_checker.h
===================================================================
--- trunk/src/data/hmsc_reference_checker.h 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/src/data/hmsc_reference_checker.h 2010-02-10 20:46:58 UTC (rev 582)
@@ -64,7 +64,7 @@
if(reference_node != NULL && reference_node->get_bmsc().get() != NULL)
{
BMscPtr bmsc = reference_node->get_bmsc();
- BMscPtr counterexample = m_checker->check(bmsc, m_mapper);
+ BMscPtr counterexample = m_checker->check(bmsc, m_mapper).front(); //Warning
if(counterexample != NULL)
throw ReferenceException(reference_node, counterexample);
}
@@ -82,7 +82,7 @@
class HMscReferenceChecker: public HMscChecker
{
public:
- HMscPtr check(HMscPtr hmsc, ChannelMapperPtr chm)
+ std::list<HMscPtr> check(HMscPtr hmsc, ChannelMapperPtr chm)
{
HMscPtr example;
@@ -104,8 +104,9 @@
reference->set_marked(true);
reference->set_msc(error.get_counterexample());
}
-
- return example;
+ std::list<HMscPtr> result;
+ result.push_back(example);
+ return result;
}
};
Modified: trunk/src/view/visio/addon/document.cpp
===================================================================
--- trunk/src/view/visio/addon/document.cpp 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/src/view/visio/addon/document.cpp 2010-02-10 20:46:58 UTC (rev 582)
@@ -756,7 +756,13 @@
try
{
- BMscPtr bresult = bmsc_checker->check(bmsc, srm);
+ std::list<BMscPtr> lresult = bmsc_checker->check(bmsc, srm);
+ BMscPtr bresult;
+ if(lresult.size() > 0)
+ bresult = lresult.back();
+ else
+ bresult = NULL;
+
// note: the explicit cast is a workaround for a bug in Visual Studio .NET
result = boost::dynamic_pointer_cast<Msc>(bresult);
result_set = true;
@@ -786,7 +792,12 @@
try
{
- HMscPtr hresult = hmsc_checker->check(hmsc, srm);
+ std::list<HMscPtr> lresult = hmsc_checker->check(hmsc, srm);
+ HMscPtr hresult;
+ if(lresult.size() > 0)
+ hresult = lresult.back();
+ else
+ hresult = NULL;
result = boost::dynamic_pointer_cast<Msc>(hresult);
result_set = true;
}
Modified: trunk/tests/acyclic_checker_test.cpp
===================================================================
--- trunk/tests/acyclic_checker_test.cpp 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/tests/acyclic_checker_test.cpp 2010-02-10 20:46:58 UTC (rev 582)
@@ -61,8 +61,8 @@
AcyclicCheckerPtr checker = AcyclicChecker::instance();
SRChannelMapperPtr srm = SRChannelMapper::instance();
SRMChannelMapperPtr srlm = SRMChannelMapper::instance();
- return (print_result(checker->check(bmsc,srm),is_sr_fifo,"sender-receiver") &&
- print_result(checker->check(bmsc,srlm),is_srl_fifo,"sender-receiver-label"));
+ return (print_result(checker->check(bmsc,srm).back(),is_sr_fifo,"sender-receiver") &&
+ print_result(checker->check(bmsc,srlm).back(),is_srl_fifo,"sender-receiver-label"));
}
bool BMscA() {
Modified: trunk/tests/checker_test.cpp
===================================================================
--- trunk/tests/checker_test.cpp 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/tests/checker_test.cpp 2010-02-10 20:46:58 UTC (rev 582)
@@ -61,7 +61,7 @@
if(bmsc_checker != NULL && bmsc != NULL
&& checker->is_supported(srm))
{
- return bmsc_checker->check(bmsc, srm);
+ return bmsc_checker->check(bmsc, srm).back();
}
HMscPtr hmsc = boost::dynamic_pointer_cast<HMsc>(msc);
@@ -69,7 +69,7 @@
if(hmsc_checker != NULL && hmsc != NULL
&& checker->is_supported(srm))
{
- return hmsc_checker->check(hmsc, srm);
+ return hmsc_checker->check(hmsc, srm).back();
}
std::cerr << "ERROR: No relevant checker for " << property << std::endl;
Modified: trunk/tests/deadlock_checker_test.cpp
===================================================================
--- trunk/tests/deadlock_checker_test.cpp 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/tests/deadlock_checker_test.cpp 2010-02-10 20:46:58 UTC (rev 582)
@@ -44,7 +44,7 @@
ChannelMapperPtr chm;
DeadlockCheckerPtr dead = DeadlockChecker::instance();
- HMscPtr path_h1 = dead->check(h1,chm);
+ HMscPtr path_h1 = dead->check(h1,chm).back();
if(path_h1.get())
{
std::cerr << "OK: h1 contains deadlock" << std::endl;
Modified: trunk/tests/fifo_checker_test.cpp
===================================================================
--- trunk/tests/fifo_checker_test.cpp 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/tests/fifo_checker_test.cpp 2010-02-10 20:46:58 UTC (rev 582)
@@ -105,8 +105,8 @@
FifoCheckerPtr checker = FifoChecker::instance();
SRChannelMapperPtr srm = SRChannelMapper::instance();
SRMChannelMapperPtr srlm = SRMChannelMapper::instance();
- return (print_result(checker->check(bmsc,srm),is_sr_fifo,"sender-receiver") &&
- print_result(checker->check(bmsc,srlm),is_srl_fifo,"sender-receiver-label"));
+ return (print_result(checker->check(bmsc,srm).back(),is_sr_fifo,"sender-receiver") &&
+ print_result(checker->check(bmsc,srlm).back(),is_srl_fifo,"sender-receiver-label"));
}
bool BMscA() {
Modified: trunk/tests/livelock_checker_test.cpp
===================================================================
--- trunk/tests/livelock_checker_test.cpp 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/tests/livelock_checker_test.cpp 2010-02-10 20:46:58 UTC (rev 582)
@@ -50,7 +50,7 @@
ChannelMapperPtr chm;
LivelockCheckerPtr live = LivelockChecker::instance();
- HMscPtr path_h1 = live->check(h1,chm);
+ HMscPtr path_h1 = live->check(h1,chm).back();
if(path_h1.get())
{
std::cerr << "OK: h1 contains livelock" << std::endl;
@@ -84,7 +84,7 @@
ChannelMapperPtr chm;
LivelockCheckerPtr live = LivelockChecker::instance();
- HMscPtr path_h1 = live->check(h1,chm);
+ HMscPtr path_h1 = live->check(h1,chm).back();
if(path_h1.get())
{
std::cerr << "ERROR: h1 contains livelock" << std::endl;
@@ -118,7 +118,7 @@
ChannelMapperPtr chm;
LivelockCheckerPtr live = LivelockChecker::instance();
- HMscPtr path_h1 = live->check(h1,chm);
+ HMscPtr path_h1 = live->check(h1,chm).back();
if(path_h1.get())
{
std::cerr << "ERROR: h1 contains livelock" << std::endl;
Modified: trunk/tests/local_choice_checker_test.cpp
===================================================================
--- trunk/tests/local_choice_checker_test.cpp 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/tests/local_choice_checker_test.cpp 2010-02-10 20:46:58 UTC (rev 582)
@@ -38,7 +38,7 @@
SRChannelMapperPtr srm = SRChannelMapper::instance();
- return print_result(checker->check(hmsc,srm),is_local_choice);
+ return print_result(checker->check(hmsc,srm).back(),is_local_choice);
}
bool HMscA() {
Modified: trunk/tests/race_checker_test.cpp
===================================================================
--- trunk/tests/race_checker_test.cpp 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/tests/race_checker_test.cpp 2010-02-10 20:46:58 UTC (rev 582)
@@ -61,8 +61,8 @@
static RaceChecker ch;
SRChannelMapperPtr srm = SRChannelMapper::instance();
SRMChannelMapperPtr srlm = SRMChannelMapper::instance();
- bool result = (print_result(ch.check(hmsc,srm),is_sr_race_free,"sender-receiver") &&
- print_result(ch.check(hmsc,srlm),is_srl_race_free,"sender-receiver-label"));
+ bool result = (print_result(ch.check(hmsc,srm).back(),is_sr_race_free,"sender-receiver") &&
+ print_result(ch.check(hmsc,srlm).back(),is_srl_race_free,"sender-receiver-label"));
return result;
}
Modified: trunk/tests/universal_boundedness_checker_test.cpp
===================================================================
--- trunk/tests/universal_boundedness_checker_test.cpp 2010-02-10 15:18:33 UTC (rev 581)
+++ trunk/tests/universal_boundedness_checker_test.cpp 2010-02-10 20:46:58 UTC (rev 582)
@@ -64,7 +64,7 @@
SRChannelMapperPtr srm = SRChannelMapper::instance();
- return print_result(checker->check(hmsc,srm),is_bounded);
+ return print_result(checker->check(hmsc,srm).back(),is_bounded);
}
bool HMscA() {
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
