Menu
▾
▴
[Scstudio-commits] SF.net SVN: scstudio:[175] trunk/src/check
|
From: <ba...@us...> - 2009-01-26 23:08:16
|
Revision: 175
http://scstudio.svn.sourceforge.net/scstudio/?rev=175&view=rev
Author: babicaj
Date: 2009-01-26 21:44:38 +0000 (Mon, 26 Jan 2009)
Log Message:
-----------
AcyclicChecker's counter example has marked events and messages, BMscDuplicator refactored
Modified Paths:
--------------
trunk/src/check/order/acyclic_checker.cpp
trunk/src/check/order/acyclic_checker.h
trunk/src/check/order/fifo_checker.cpp
trunk/src/check/pseudocode/msc_duplicators.cpp
trunk/src/check/pseudocode/msc_duplicators.h
Modified: trunk/src/check/order/acyclic_checker.cpp
===================================================================
--- trunk/src/check/order/acyclic_checker.cpp 2009-01-20 09:33:45 UTC (rev 174)
+++ trunk/src/check/order/acyclic_checker.cpp 2009-01-26 21:44:38 UTC (rev 175)
@@ -21,19 +21,19 @@
AcyclicCheckerPtr AcyclicChecker::m_instance;
-BMscPtr AcyclicChecker::create_counter_example(BMscPtr& bmsc, const EventPList& path)
+BMscPtr AcyclicChecker::create_counter_example(BMscPtr& bmsc, const MscElementPList& path)
{
- Event* last_event = path.back();
+ MscElement* last_event = path.back();
BMscDuplicator duplicator;
BMscPtr new_bmsc = duplicator.duplicate_bmsc(bmsc);
- EventPList::const_iterator i = path.begin();
+ MscElementPList::const_iterator i = path.begin();
while(*i != last_event)
{
i++;
}
while(i != path.end())
{
- Event* copy = duplicator.get_copy((*i));
+ MscElement* copy = duplicator.get_copy((*i));
copy->set_marked(true);
i++;
}
@@ -44,9 +44,7 @@
{
AcyclicCheckerListener listener;
DFSEventsTraverser traverser;
- traverser.add_white_event_found_listener(&listener);
traverser.add_gray_event_found_listener(&listener);
- traverser.add_event_finished_listener(&listener);
BMscPtr result;
try
{
@@ -54,8 +52,7 @@
}
catch(CycleDetectedException&)
{
- result = create_counter_example(bmsc,listener.get_path());
- traverser.cleanup_traversing_attributes();
+ result = create_counter_example(bmsc,traverser.get_reached_elements());
}
return result;
}
Modified: trunk/src/check/order/acyclic_checker.h
===================================================================
--- trunk/src/check/order/acyclic_checker.h 2009-01-20 09:33:45 UTC (rev 174)
+++ trunk/src/check/order/acyclic_checker.h 2009-01-26 21:44:38 UTC (rev 175)
@@ -26,38 +26,16 @@
typedef boost::shared_ptr<AcyclicChecker> AcyclicCheckerPtr;
class AcyclicCheckerListener:
-public WhiteEventFoundListener,
-public GrayEventFoundListener,
-public EventFinishedListener
+public GrayEventFoundListener
{
-protected:
-
- EventPList m_path;
-
public:
- void on_white_event_found(Event* e)
- {
- m_path.push_back(e);
- }
-
void on_gray_event_found(Event* e)
{
- m_path.push_back(e);
throw CycleDetectedException();
}
- void on_event_finished(Event* e)
- {
- m_path.pop_back();
- }
-
- const EventPList& get_path()
- {
- return m_path;
- }
-
};
class SCORDER_EXPORT AcyclicChecker: public Checker, public BMscChecker
@@ -70,7 +48,7 @@
*/
static AcyclicCheckerPtr m_instance;
- BMscPtr create_counter_example(BMscPtr& original, const EventPList& path);
+ BMscPtr create_counter_example(BMscPtr& original, const MscElementPList& path);
public:
Modified: trunk/src/check/order/fifo_checker.cpp
===================================================================
--- trunk/src/check/order/fifo_checker.cpp 2009-01-20 09:33:45 UTC (rev 174)
+++ trunk/src/check/order/fifo_checker.cpp 2009-01-26 21:44:38 UTC (rev 175)
@@ -31,7 +31,7 @@
for(size_t i=0;i<2;i++)
{
//event is surely complete
- Event* copy = duplicator.get_copy(events[i]);
+ Event* copy = duplicator.get_event_copy(events[i]);
copy->set_marked(true);
copy->get_complete_message()->set_marked(true);
if(copy->is_send())
Modified: trunk/src/check/pseudocode/msc_duplicators.cpp
===================================================================
--- trunk/src/check/pseudocode/msc_duplicators.cpp 2009-01-20 09:33:45 UTC (rev 174)
+++ trunk/src/check/pseudocode/msc_duplicators.cpp 2009-01-26 21:44:38 UTC (rev 175)
@@ -80,15 +80,10 @@
return new_bmsc;
}
-Event*& BMscDuplicator::get_copy(Event* e)
+Event* BMscDuplicator::get_event_copy(Event* e)
{
- bool just_set;
- Event*& copy = e->get_attribute<Event*>(BMSC_DUPLICATOR_COPY_ATTR,NULL,just_set);
- if(just_set)
- {
- m_modified_elements.push_back(e);
- }
- return copy;
+ MscElement* elem = get_copy(e);
+ return dynamic_cast<Event*>(elem);
}
BMscDuplicator::~BMscDuplicator()
@@ -147,18 +142,17 @@
m_last_new_instance->add_area(area);
m_last_area = e->get_general_area();
}
- Event*& copy = m_duplicator->get_copy(e);
CoregionEvent* coreg_event = dynamic_cast<CoregionEvent*>(e);
if(coreg_event)
{
CoregionEvent* new_e = new CoregionEvent(e);
- copy = new_e;
+ m_duplicator->set_copy(e,new_e);
dynamic_cast<CoregionArea*>(m_last_new_area)->add_event(new_e);
}
else
{
StrictEvent* new_e = new StrictEvent(e);
- copy = new_e;
+ m_duplicator->set_copy(e,new_e);
dynamic_cast<StrictOrderArea*>(m_last_new_area)->add_event(new_e);
}
create_successor(e);
@@ -193,13 +187,13 @@
void EventsCreatorListener::create_successor(Event* e)
{
- CoregionEvent* coreg_new = dynamic_cast<CoregionEvent*>(m_duplicator->get_copy(e));
+ CoregionEvent* coreg_new = dynamic_cast<CoregionEvent*>(m_duplicator->get_event_copy(e));
if(coreg_new)
{
CoregionEvent* preceding = get_preceding_event();
if(preceding)
{
- CoregionEvent* preceding_new = dynamic_cast<CoregionEvent*>(m_duplicator->get_copy(preceding));
+ CoregionEvent* preceding_new = dynamic_cast<CoregionEvent*>(m_duplicator->get_event_copy(preceding));
preceding_new->add_successor(coreg_new);
}
}
@@ -215,15 +209,16 @@
void MessagesCreatorListener::on_white_event_found(Event* e)
{
- Event* event_copy = m_duplicator->get_copy(e);
+ Event* event_copy = m_duplicator->get_event_copy(e);
if(e->is_matched())
{
if(e->is_send())
{
- Event* matching_copy = m_duplicator->get_copy(e->get_matching_event());
+ Event* matching_copy = m_duplicator->get_event_copy(e->get_matching_event());
MscMessagePtr complete = new CompleteMessage(event_copy,matching_copy,e->get_complete_message().get());
event_copy->set_message(complete);
matching_copy->set_message(complete);
+ m_duplicator->set_copy(e->get_message().get(),complete.get());
}
}
else
Modified: trunk/src/check/pseudocode/msc_duplicators.h
===================================================================
--- trunk/src/check/pseudocode/msc_duplicators.h 2009-01-20 09:33:45 UTC (rev 174)
+++ trunk/src/check/pseudocode/msc_duplicators.h 2009-01-26 21:44:38 UTC (rev 175)
@@ -100,7 +100,7 @@
* Duplicated BMsc's elemenents have set attribute original to the original
* BMsc's elements.
*/
-class SCPSEUDOCODE_EXPORT BMscDuplicator
+class SCPSEUDOCODE_EXPORT BMscDuplicator:public Duplicator
{
protected:
@@ -116,7 +116,7 @@
~BMscDuplicator();
- Event*& get_copy(Event* e);
+ Event* get_event_copy(Event* e);
};
///////////////////////////////////////////////////////////
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|