Menu
▾
▴
[Scstudio-commits] SF.net SVN: scstudio:[1724] trunk
|
From: <ob...@us...> - 2013-03-21 18:08:51
|
Revision: 1724
http://sourceforge.net/p/scstudio/code/1724
Author: obouda
Date: 2013-03-21 18:08:46 +0000 (Thu, 21 Mar 2013)
Log Message:
-----------
merged from conditions branch
Modified Paths:
--------------
trunk/README
trunk/doc/help/CMakeLists.txt
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/pseudocode/causal_closure_initiator.cpp
trunk/src/check/pseudocode/causal_closure_initiator.h
trunk/src/check/pseudocode/communication_graph.cpp
trunk/src/check/pseudocode/communication_graph.h
trunk/src/check/pseudocode/msc_duplicators.cpp
trunk/src/check/pseudocode/msc_duplicators.h
trunk/src/check/pseudocode/utils.cpp
trunk/src/check/pseudocode/utils.h
trunk/src/check/pseudocode/visual_closure_initiator.cpp
trunk/src/check/pseudocode/visual_closure_initiator.h
trunk/src/check/race/footprint.cpp
trunk/src/check/race/footprint.h
trunk/src/check/race/race_checker.cpp
trunk/src/check/race/race_checker.h
trunk/src/check/structure/name_checker.cpp
trunk/src/check/time/constraint_syntax.cpp
trunk/src/check/time/tightening.cpp
trunk/src/check/time/tightening.h
trunk/src/check/time/time_consistency.h
trunk/src/check/time/time_pseudocode.cpp
trunk/src/check/time/time_pseudocode.h
trunk/src/check/time/time_trace_race.h
trunk/src/check/time/traverse_erase.cpp
trunk/src/check/time/traverse_erase.h
trunk/src/data/CMakeLists.txt
trunk/src/data/Z120/Context.cpp
trunk/src/data/Z120/Context_Impl.h
trunk/src/data/Z120/string_list_printer.h
trunk/src/data/Z120/z120.h
trunk/src/data/Z120/z120_save.cpp
trunk/src/data/beautify/instance_sequencer.cpp
trunk/src/data/beautify/layout_optimizer.cpp
trunk/src/data/beautify/time_transformer.cpp
trunk/src/data/checker.h
trunk/src/data/dfs_area_traverser.cpp
trunk/src/data/dfs_area_traverser.h
trunk/src/data/dfs_events_traverser.cpp
trunk/src/data/dfs_events_traverser.h
trunk/src/data/dfs_instance_events_traverser.cpp
trunk/src/data/dfs_instance_events_traverser.h
trunk/src/data/engmann/engmann.cpp
trunk/src/data/exporttex/exportTex.cpp
trunk/src/data/modelchecking/divine.cpp
trunk/src/data/modelchecking/divine.h
trunk/src/data/msc/BMsc.cpp
trunk/src/data/msc/BMsc.h
trunk/src/data/msc/Comment.h
trunk/src/data/msc/Commentable.h
trunk/src/data/msc/CompleteMessage.cpp
trunk/src/data/msc/CompleteMessage.h
trunk/src/data/msc/Condition.h
trunk/src/data/msc/ConditionNode.cpp
trunk/src/data/msc/ConditionNode.h
trunk/src/data/msc/ConnectionNode.h
trunk/src/data/msc/CoregionArea.cpp
trunk/src/data/msc/CoregionArea.h
trunk/src/data/msc/CoregionEventRelation.h
trunk/src/data/msc/EndNode.h
trunk/src/data/msc/EventArea.h
trunk/src/data/msc/HMsc.cpp
trunk/src/data/msc/HMsc.h
trunk/src/data/msc/HMscNode.cpp
trunk/src/data/msc/HMscNode.h
trunk/src/data/msc/IncompleteMessage.cpp
trunk/src/data/msc/IncompleteMessage.h
trunk/src/data/msc/Instance.cpp
trunk/src/data/msc/Instance.h
trunk/src/data/msc/LocalAction.h
trunk/src/data/msc/Msc.h
trunk/src/data/msc/MscElement.h
trunk/src/data/msc/MscElementTmpl.h
trunk/src/data/msc/MscMessage.cpp
trunk/src/data/msc/MscMessage.h
trunk/src/data/msc/NodeRelation.cpp
trunk/src/data/msc/NodeRelation.h
trunk/src/data/msc/PredecessorNode.cpp
trunk/src/data/msc/PredecessorNode.h
trunk/src/data/msc/ReferenceNode.h
trunk/src/data/msc/StartNode.h
trunk/src/data/msc/StrictOrderArea.h
trunk/src/data/msc/SuccessorNode.cpp
trunk/src/data/msc/SuccessorNode.h
trunk/src/data/msc/time/AbsoluteTime.h
trunk/src/data/msc/time/TimeConstraint.cpp
trunk/src/data/msc/time/TimeConstraint.h
trunk/src/data/msc/time/TimeRelation.cpp
trunk/src/data/msc/time/TimeRelation.h
trunk/src/data/msc/time/TimeRelationEvent.cpp
trunk/src/data/msc/time/TimeRelationEvent.h
trunk/src/data/msc/time/TimeRelationRefNode.cpp
trunk/src/data/msc/time/TimeRelationRefNode.h
trunk/src/data/msc.h
trunk/src/data/mscgen/MscgenContext.cpp
trunk/src/data/mscgen/mscgen.h
trunk/src/data/mscgen/string_list_printer.h
trunk/src/data/pcap/pcap_handler.cpp
trunk/src/data/pcap/pcap_handler.h
trunk/src/data/pcap/pcap_settings.cpp
trunk/src/data/time_relevant_ordering/dfs_backward_traverser.cpp
trunk/src/data/time_relevant_ordering/dfs_backward_traverser.h
trunk/src/data/time_relevant_ordering/time_order_optimizer.cpp
trunk/src/data/time_relevant_ordering/time_order_optimizer.h
trunk/src/data/time_relevant_ordering/time_relevant_ordering.cpp
trunk/src/data/time_relevant_ordering/time_relevant_ordering.h
trunk/src/membership/diff_impl.cpp
trunk/src/membership/diff_impl.h
trunk/src/membership/membership_additional.cpp
trunk/src/membership/membership_additional.h
trunk/src/membership/membership_alg.cpp
trunk/src/membership/membership_alg.h
trunk/src/membership/membership_base.h
trunk/src/membership/membership_time.cpp
trunk/src/membership/membership_time.h
trunk/src/montecarlo/montecarlo.cpp
trunk/src/montecarlo/montecarlo.h
trunk/src/scstudio.cpp
trunk/src/view/visio/addon/enums.h
trunk/src/view/visio/addon/extract.cpp
trunk/src/view/visio/addon/extract.h
trunk/src/view/visio/addon/instancesfielddlg.cpp
trunk/src/view/visio/addon/instancesfielddlg.h
trunk/src/view/visio/addon/messagesequencedlg.cpp
trunk/src/view/visio/addon/messagesequencedlg.h
trunk/src/view/visio/addon/pageutils.cpp
trunk/src/view/visio/addon/pageutils.h
trunk/src/view/visio/addon/shapeutils.cpp
trunk/src/view/visio/addon/shapeutils.h
trunk/src/view/visio/addon/visualize.cpp
trunk/src/view/visio/addon/visualize.h
trunk/tests/acyclic_checker_test.cpp
trunk/tests/bmsc_matrix_converter_test.cpp
trunk/tests/bmsc_tightening_test.cpp
trunk/tests/constrain_check_test.cpp
trunk/tests/exporttex_test/exporttex_diff.py
trunk/tests/exporttex_test/exporttex_test.cpp
trunk/tests/exporttex_test/exporttex_test00.mpr.result
trunk/tests/exporttex_test/exporttex_test94.mpr
trunk/tests/fifo_checker_test.cpp
trunk/tests/hmsc_all_paths_test.cpp
trunk/tests/local_choice_checker_test.cpp
trunk/tests/max_tightener_test.cpp
trunk/tests/race_checker_test.cpp
trunk/tests/tighten_hmsc_test.cpp
trunk/tests/tighten_msc_test.cpp
trunk/tests/universal_boundedness_checker_test.cpp
Added Paths:
-----------
trunk/.gitignore
trunk/src/data/msc/Event.cpp
trunk/src/data/msc/Event.h
trunk/src/data/msc/EventArea.cpp
trunk/src/data/msc/EventTmpl.h
trunk/src/data/msc/MessageEvent.cpp
trunk/src/data/msc/MessageEvent.h
trunk/src/data/msc/StrictOrderArea.cpp
trunk/src/view/visio/scstudio.vs2012.sln
Removed Paths:
-------------
trunk/src/check/race/bmsc_race_checker.cpp
trunk/src/check/race/bmsc_race_checker.h
trunk/src/data/msc/CoregionEvent.cpp
trunk/src/data/msc/CoregionEvent.h
trunk/src/data/msc/Event.cpp
trunk/src/data/msc/Event.h
trunk/src/data/msc/EventTmpl.h
trunk/src/data/msc/GeneralEvent.cpp
trunk/src/data/msc/GeneralEvent.h
trunk/src/data/msc/GeneralEventTmpl.h
trunk/src/data/msc/StrictEvent.h
trunk/src/data/msc_modifications.h
Property Changed:
----------------
trunk/
trunk/third-party-sw/antlr/runtime/C/configure
trunk/third-party-sw/antlr/runtime/C/copy.sh
Index: trunk
===================================================================
--- trunk 2013-03-21 17:02:30 UTC (rev 1723)
+++ trunk 2013-03-21 18:08:46 UTC (rev 1724)
Property changes on: trunk
___________________________________________________________________
Modified: svn:mergeinfo
## -1,2 +1,3 ##
+/branches/conditions:1599-1723
/branches/internal-structure-refactoring:1540-1552
/branches/refactoring:1332-1337,1339,1341
\ No newline at end of property
Copied: trunk/.gitignore (from rev 1723, branches/conditions/.gitignore)
===================================================================
--- trunk/.gitignore (rev 0)
+++ trunk/.gitignore 2013-03-21 18:08:46 UTC (rev 1724)
@@ -0,0 +1,89 @@
+CMakeCache.txt
+DartConfiguration.tcl
+Debug/
+Release/
+Testing/
+*.vcproj
+*.vcproj.*.user
+*.cmake
+*.dir
+CMakeFiles/
+*.sln
+*.suo
+Makefile
+*.so
+doc/beautify.aux
+doc/beautify.log
+doc/beautify.out
+doc/beautify.pdf
+doc/doxygen/doxygen.config.local
+doc/find_flow/memb_alg.aux
+doc/find_flow/memb_alg.log
+doc/find_flow/memb_alg.out
+doc/find_flow/memb_alg.pdf
+doc/help/*.html
+doc/help/*/*.html
+scstudio.ncb
+src/config.h
+src/data/Z120/Z120.tokens
+src/data/Z120/Z120Lexer.c
+src/data/Z120/Z120Lexer.h
+src/data/Z120/Z120Parser.c
+src/data/Z120/Z120Parser.h
+src/data/mscgen/Mscgen.tokens
+src/data/mscgen/MscgenLexer.c
+src/data/mscgen/MscgenLexer.h
+src/data/mscgen/MscgenParser.c
+src/data/mscgen/MscgenParser.h
+src/scstudio
+src/view/visio/addon/dlldata.c
+src/view/visio/addon/eventsink.h
+src/view/visio/addon/eventsink_i.c
+src/view/visio/addon/eventsink_p.c
+src/view/visio/redistribute
+src/view/visio/setup-nsis/api.h
+src/view/visio/setup-nsis/pluginapi.h
+src/view/visio/setup-nsis/pluginapi.c
+tests/acyclic_checker_test
+tests/checker_test
+tests/deadlock_checker_test
+tests/decimal_test
+tests/diff/diff_test
+tests/engmann_test
+tests/fifo_checker_test
+tests/find_block_test
+tests/interval_set_test
+tests/interval_string
+tests/interval_test
+tests/livelock_checker_test
+tests/local_choice_checker_test
+tests/membership/membership_test
+tests/montecarlo/montecarlo_test
+tests/pcap/pcap_test
+tests/race_checker_test
+tests/tighten_hmsc_test
+tests/tighten_msc_test
+tests/tightening_tests/tighten_test
+tests/time_relevant_ordering/time_relevant_ordering
+tests/universal_boundedness_checker_test
+tests/z120_test/z120_test
+third-party-sw/boost/*.exe
+third-party-sw/boost/bin.v2/
+third-party-sw/boost/bootstrap.log
+third-party-sw/boost/project-config.jam
+third-party-sw/boost/stage/
+third-party-sw/boost/tools/build/v2/engine/bin.*/
+third-party-sw/boost/tools/build/v2/engine/bootstrap/
+third-party-sw/antlr/runtime/C/.deps/
+third-party-sw/antlr/runtime/C/.libs/
+third-party-sw/antlr/runtime/C/*.o
+third-party-sw/antlr/runtime/C/*.lo
+third-party-sw/antlr/runtime/C/config.log
+third-party-sw/antlr/runtime/C/config.status
+third-party-sw/antlr/runtime/C/libantlr3c.a
+third-party-sw/antlr/runtime/C/libantlr3c.la
+third-party-sw/antlr/runtime/C/libantlr3c.lai
+third-party-sw/antlr/runtime/C/libtool
+third-party-sw/antlr/runtime/C/stamp-h1
+third-party-sw/boost/b2
+third-party-sw/boost/bjam
Modified: trunk/README
===================================================================
--- trunk/README 2013-03-21 17:02:30 UTC (rev 1723)
+++ trunk/README 2013-03-21 18:08:46 UTC (rev 1724)
@@ -31,7 +31,7 @@
Compiling SCStudio (Linux version)
----------------------------------
-$ cd scstudio/trunk
+$ cd scstudio
$ cmake .
$ make
[$ make test]
Modified: trunk/doc/help/CMakeLists.txt
===================================================================
--- trunk/doc/help/CMakeLists.txt 2013-03-21 17:02:30 UTC (rev 1723)
+++ trunk/doc/help/CMakeLists.txt 2013-03-21 18:08:46 UTC (rev 1724)
@@ -81,4 +81,3 @@
ENDFOREACH(FILE)
# $Id$
-
Modified: trunk/src/check/localchoice/local_choice_checker.cpp
===================================================================
--- trunk/src/check/localchoice/local_choice_checker.cpp 2013-03-21 17:02:30 UTC (rev 1723)
+++ trunk/src/check/localchoice/local_choice_checker.cpp 2013-03-21 18:08:46 UTC (rev 1724)
@@ -11,12 +11,13 @@
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
* Lesser General Public License for more details.
*
- * Copyright (c) 2008 V\xE1clav Vacek <va...@ic...>
+ * Copyright (c) 2008 Vaclav Vacek <va...@ic...>
*
* $Id$
*/
#include "check/localchoice/local_choice_checker.h"
+#include "data/msc/CoregionArea.h"
LocalChoiceCheckerPtr LocalChoiceChecker::m_instance;
const std::string LocalChoiceChecker::lc_mep_attribute = "lcmep";
@@ -66,22 +67,21 @@
current_node->set_attribute(LocalChoiceChecker::lc_nip_attribute, nip);
}
-void BMscInitListener::on_white_event_found(Event *e)
+void BMscInitListener::on_white_event_found(MessageEvent *e)
{
- CoregionEventPtr cor_e;
if(m_first) //Still looking for a possibly first event in the instance
{
- cor_e = dynamic_cast<CoregionEvent*>(e);
- if(cor_e)
+ CoregionArea* coregion = dynamic_cast<CoregionArea*>(e->get_area());
+ if(coregion != NULL)
{
if(m_first_coregion == NULL)
- m_first_coregion = cor_e->get_coregion_area();
+ m_first_coregion = coregion;
- if(m_first_coregion == cor_e->get_coregion_area())
+ if(m_first_coregion == coregion)
{
- if(cor_e->is_minimal())
+ if(e->is_minimal())
{
- if(cor_e->is_send())
+ if(e->is_send())
m_mep = true;
}
else //the event is not minimal
@@ -109,9 +109,9 @@
HMscNodePListPtr successors;
HMscNodePList::iterator it;
std::set<std::wstring>::iterator str_it;
-
+
std::set<std::wstring> empty; //neutral value for get_attribute
-
+
successors = NodeFinder::successors(n, "rnf_inner"); //the string is the name of the dynamic attribute
std::set<std::wstring> &curr_nip = n->get_attribute(LocalChoiceChecker::lc_nip_attribute, empty);
Modified: trunk/src/check/localchoice/local_choice_checker.h
===================================================================
--- trunk/src/check/localchoice/local_choice_checker.h 2013-03-21 17:02:30 UTC (rev 1723)
+++ trunk/src/check/localchoice/local_choice_checker.h 2013-03-21 18:08:46 UTC (rev 1724)
@@ -11,7 +11,7 @@
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
* Lesser General Public License for more details.
*
- * Copyright (c) 2008 V\xE1clav Vacek <va...@ic...>
+ * Copyright (c) 2008 Vaclav Vacek <va...@ic...>
*
* $Id$
*/
@@ -31,7 +31,7 @@
class NonlocalNode: public std::exception
{
-public:
+public:
virtual const char* what() const throw()
{
return "A nonlocal choice node has been found.";
@@ -86,7 +86,7 @@
}
void on_white_node_found(HMscNode *n);
bool changed(void)
- {
+ {
return m_change;
}
};
@@ -105,7 +105,7 @@
bool m_mep;
CoregionArea *m_first_coregion;
public:
- void on_white_event_found(Event *e);
+ void on_white_event_found(MessageEvent *e);
BMscInitListener(void)
:m_idle(true),m_first(true),m_mep(false), m_first_coregion(NULL)
{}
@@ -117,7 +117,7 @@
m_first_coregion = NULL;
}
bool is_idle(void)
- {
+ {
return m_idle;
}
bool is_mep(void)
@@ -129,19 +129,19 @@
class SCLOCALCHOICE_EXPORT LocalChoiceChecker: public Checker, public HMscChecker
{
protected:
-
+
/**
* Common instance.
*/
static LocalChoiceCheckerPtr m_instance;
BMscGraphDuplicator m_graph_duplicator;
-
-
+
+
public:
static const std::string lc_mep_attribute;
static const std::string lc_nip_attribute;
-
+
LocalChoiceChecker(){};
/**
* Human readable name of the property being checked.
@@ -167,7 +167,7 @@
* Cleans up no more needed attributes.
*/
void cleanup_attributes();
-
+
/**
* Supports all mappers
*/
@@ -175,8 +175,8 @@
{
return true;
}
-
-
+
+
static LocalChoiceCheckerPtr instance()
{
if(!m_instance.get())
@@ -185,5 +185,5 @@
}
};
-
+
// $Id$
Modified: trunk/src/check/order/acyclic_checker.cpp
===================================================================
--- trunk/src/check/order/acyclic_checker.cpp 2013-03-21 17:02:30 UTC (rev 1723)
+++ trunk/src/check/order/acyclic_checker.cpp 2013-03-21 18:08:46 UTC (rev 1724)
@@ -57,28 +57,12 @@
BMscDuplicator duplicator;
for(it = bmsc->get_instances().begin(); it != bmsc->get_instances().end(); it++)
{
- ConnectionNode *dummy;
- EventAreaPtr eap = (*it)->get_first_area();
- while(eap)
+ const MessageEventPList min_events = (*it)->get_minimal_events();
+ for (MessageEventPList::const_iterator i = min_events.begin(); i != min_events.end(); ++i)
{
- if(eap->is_empty())
- eap = eap->get_next_area();
- else
- break;
+ ConnectionNode* node = (*i)->get_attribute<ConnectionNode*>("ACC_node", NULL);
+ start->add_successor(node);
}
- if(eap)
- {
- StrictOrderArea *seap = dynamic_cast<StrictOrderArea*>(eap.get());
- if(seap)
- start->add_successor(seap->get_first_event()->get_attribute("ACC_node", dummy));
- else
- {
- CoregionArea *ceap = dynamic_cast<CoregionArea*>(eap.get());
- CoregionEventPVector::const_iterator cit;
- for(cit = ceap->get_minimal_events().begin(); cit != ceap->get_minimal_events().end(); cit++)
- start->add_successor((*cit)->get_attribute("ACC_node", dummy));
- }
- }
}
cycle_traverser.traverse(hmsc);
std::list<BMscPtr> res;
@@ -96,8 +80,7 @@
cono = dynamic_cast<ConnectionNode*>((*eit));
if(cono)
{
- Event *e, *dummy;
- e = cono->get_attribute("ACC_event", dummy);
+ MessageEventP e = cono->get_attribute<MessageEventP>("ACC_event", NULL);
duplicator.get_copy(e)->set_marked(MARKED);
}
nore = dynamic_cast<NodeRelation*>((*eit));
Modified: trunk/src/check/order/acyclic_checker.h
===================================================================
--- trunk/src/check/order/acyclic_checker.h 2013-03-21 17:02:30 UTC (rev 1723)
+++ trunk/src/check/order/acyclic_checker.h 2013-03-21 18:08:46 UTC (rev 1724)
@@ -49,7 +49,7 @@
AssignHMscListener(HMsc *hmsc)
:m_hmsc(hmsc)
{}
- void on_white_event_found(Event *e)
+ void on_white_event_found(MessageEvent *e)
{
ConnectionNode *node = new ConnectionNode();
m_hmsc->add_node(node);
@@ -61,7 +61,7 @@
class MessageSuceessors: public SendReceivePairListener
{
public:
- void on_send_receive_pair(Event *send, Event *receive)
+ void on_send_receive_pair(MessageEvent *send, MessageEvent *receive)
{
ConnectionNode *first, *second;
first = send->get_attribute("ACC_node", second);
@@ -75,7 +75,7 @@
class InstanceSuccessors: public EventSuccessorListener
{
public:
- void on_event_successor(Event *event, Event *successor)
+ void on_event_successor(MessageEvent *event, MessageEvent *successor)
{
ConnectionNode *first, *second;
first = event->get_attribute("ACC_node", second);
@@ -87,7 +87,7 @@
class CleanHMscListener: public WhiteEventFoundListener
{
public:
- void on_white_event_found(Event *e)
+ void on_white_event_found(MessageEvent *e)
{
ConnectionNode *node, *dummy;
NodeRelation* nr;
@@ -98,7 +98,7 @@
nr->remove_attribute<MscMessage*>("ACC_message");
e->remove_attribute<NodeRelation*>("ACC_relation");
}
- node->remove_attribute<Event*>("ACC_event");
+ node->remove_attribute<MessageEvent*>("ACC_event");
e->remove_attribute<ConnectionNode*>("ACC_node");
}
};
Modified: trunk/src/check/order/fifo_checker.cpp
===================================================================
--- trunk/src/check/order/fifo_checker.cpp 2013-03-21 17:02:30 UTC (rev 1723)
+++ trunk/src/check/order/fifo_checker.cpp 2013-03-21 18:08:46 UTC (rev 1724)
@@ -31,15 +31,15 @@
return result;
}
-BMscPtr FifoChecker::create_counter_example(BMscPtr& bmsc, Event* e_1, Event* e_2)
+BMscPtr FifoChecker::create_counter_example(BMscPtr& bmsc, MessageEvent* e_1, MessageEvent* e_2)
{
BMscDuplicator duplicator;
BMscPtr new_bmsc = duplicator.duplicate_bmsc(bmsc);
- Event* events[] = {e_1,e_2};
+ MessageEvent* events[] = {e_1,e_2};
for(size_t i=0;i<2;i++)
{
//event is surely complete
- Event* copy = duplicator.get_event_copy(events[i]);
+ MessageEvent* copy = duplicator.get_event_copy(events[i]);
copy->get_complete_message()->set_marked(MARKED);
}
return new_bmsc;
@@ -53,7 +53,7 @@
DFSEventsTraverser traverser;
traverser.add_event_finished_listener(&topology_listener);
traverser.traverse(bmsc);
- EventPVector topology(topology_listener.get_topology().size());
+ MessageEventPVector topology(topology_listener.get_topology().size());
topology.assign(
topology_listener.get_topology().begin(),
topology_listener.get_topology().end()
@@ -83,7 +83,7 @@
{
while(!m_modified_events.empty())
{
- Event* e = m_modified_events.top();
+ MessageEvent* e = m_modified_events.top();
m_modified_events.pop();
e->remove_attribute<size_t>(channel_id_attribute);
}
Modified: trunk/src/check/order/fifo_checker.h
===================================================================
--- trunk/src/check/order/fifo_checker.h 2013-03-21 17:02:30 UTC (rev 1723)
+++ trunk/src/check/order/fifo_checker.h 2013-03-21 18:08:46 UTC (rev 1724)
@@ -30,7 +30,6 @@
class FifoChecker;
-typedef std::stack<Event*> EventPStack;
typedef boost::shared_ptr<FifoChecker> FifoCheckerPtr;
/** \brief Checks the FIFO property of a MSC.
@@ -56,9 +55,9 @@
/**
* Events with modified dynamic attributes
*/
- EventPStack m_modified_events;
+ MessageEventPStack m_modified_events;
- BMscPtr create_counter_example(BMscPtr& bmsc, Event* receive1, Event* receive2);
+ BMscPtr create_counter_example(BMscPtr& bmsc, MessageEvent* receive1, MessageEvent* receive2);
/**
* Checks whether e1 and e2 (from equivalent channel) are in consistent order.
@@ -66,7 +65,7 @@
* An e1 is supposed to be before e2. If this holds true is returned, false
* otherwise.
*/
- bool consistent_order(VisualClosureInitiator& initiator, Event* e1, Event* e2)
+ bool consistent_order(VisualClosureInitiator& initiator, MessageEvent* e1, MessageEvent* e2)
{
BoolVector& e1_closure = initiator.get_visual_closure(e1);
size_t e2_index = initiator.get_topology_index(e2);
@@ -131,7 +130,7 @@
/**
* Setter of channel id attribute of message.
*/
- void set_channel_id(Event* e, size_t id)
+ void set_channel_id(MessageEvent* e, size_t id)
{
e->set_attribute<size_t>(channel_id_attribute,id);
}
@@ -139,7 +138,7 @@
/**
* Getter of channel id attribute of m.
*/
- size_t get_channel_id(Event* e)
+ size_t get_channel_id(MessageEvent* e)
{
return e->get_attribute<size_t>(channel_id_attribute,0);
}
@@ -147,9 +146,9 @@
/**
* Determines whether event should be checked or not.
*
- * Event should be checked if it is receive event and has matching event.
+ * MessageEvent should be checked if it is receive event and has matching event.
*/
- static bool should_be_checked(Event* e)
+ static bool should_be_checked(MessageEvent* e)
{
return e->is_receive() && e->is_matched();
}
Modified: trunk/src/check/pseudocode/causal_closure_initiator.cpp
===================================================================
--- trunk/src/check/pseudocode/causal_closure_initiator.cpp 2013-03-21 17:02:30 UTC (rev 1723)
+++ trunk/src/check/pseudocode/causal_closure_initiator.cpp 2013-03-21 18:08:46 UTC (rev 1724)
@@ -24,23 +24,23 @@
{
while(!m_modified_events.empty())
{
- Event* e = m_modified_events.top();
+ MessageEvent* e = m_modified_events.top();
e->remove_attribute<BoolVector>(m_causal_closure_attribute);
m_modified_events.pop();
}
}
-void CausalClosureInitiator::initialize(const EventPVector& events,
+void CausalClosureInitiator::initialize(const MessageEventPVector& events,
VisualClosureInitiator& visual_closure_init, ChannelMapperPtr mapper)
{
//initialize matrix
size_t events_count = events.size();
- EventPList::const_iterator i;
+ MessageEventPList::const_iterator i;
//closure[x][y]==true <=> x << y
std::vector<BoolVector*> closure(events_count);
for(size_t i=0;i<events_count;i++)
{
- Event* i_event = events[i];
+ MessageEvent* i_event = events[i];
BoolVector& causal_closure = get_causal_closure(i_event);
causal_closure.resize(events_count,false);
closure[i] = &causal_closure;
@@ -54,12 +54,12 @@
}
for(size_t i=0;i<events_count;i++)
{
- Event* i_event = events[i];
+ MessageEvent* i_event = events[i];
BoolVector& i_causal_closure = *closure[i];
BoolVector& i_visual_closure = visual_closure_init.get_visual_closure(i_event);
for(size_t j = 0; j < events_count; j++)
{
- Event* j_event = events[j];
+ MessageEvent* j_event = events[j];
//i_event and j_event are from the same instance, j_event is send event and
//i_event < j_event
if(i_event->get_instance()==j_event->get_instance() &&
Modified: trunk/src/check/pseudocode/causal_closure_initiator.h
===================================================================
--- trunk/src/check/pseudocode/causal_closure_initiator.h 2013-03-21 17:02:30 UTC (rev 1723)
+++ trunk/src/check/pseudocode/causal_closure_initiator.h 2013-03-21 18:08:46 UTC (rev 1724)
@@ -27,8 +27,6 @@
#include "check/pseudocode/visual_closure_initiator.h"
#include "check/pseudocode/export.h"
-typedef std::stack<Event*> EventPStack;
-
class SCPSEUDOCODE_EXPORT CausalClosureInitiator
{
@@ -37,7 +35,7 @@
/**
* Used for cleaning up attributes.
*/
- EventPStack m_modified_events;
+ MessageEventPStack m_modified_events;
/**
* Name of causal closure attribute.
@@ -77,7 +75,7 @@
/**
* Getter of causal closure attribute of e.
*/
- BoolVector& get_causal_closure(Event* e)
+ BoolVector& get_causal_closure(MessageEvent* e)
{
static BoolVector empty(1,false);
return e->get_attribute<BoolVector>(m_causal_closure_attribute,empty);
@@ -92,7 +90,7 @@
* @param events - topologically sorted events used for visual_closure_init's initialization
* @param visual_closure_init - initialized VisualClosureInitiator
*/
- void initialize(const EventPVector& events,
+ void initialize(const MessageEventPVector& events,
VisualClosureInitiator& visual_closure_init, ChannelMapperPtr mapper);
/**
Modified: trunk/src/check/pseudocode/communication_graph.cpp
===================================================================
--- trunk/src/check/pseudocode/communication_graph.cpp 2013-03-21 17:02:30 UTC (rev 1723)
+++ trunk/src/check/pseudocode/communication_graph.cpp 2013-03-21 18:08:46 UTC (rev 1724)
@@ -11,7 +11,7 @@
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
* Lesser General Public License for more details.
*
- * Copyright (c) 2008 V\xE1clav Vacek <va...@ic...>
+ * Copyright (c) 2008 Vaclav Vacek <va...@ic...>
*
* $Id$
*/
@@ -20,7 +20,7 @@
const std::string CommunicationGraph::lexical_order_attribute = "lexical_order";
-void CommunicationGraphListener::on_white_event_found(Event *e)
+void CommunicationGraphListener::on_white_event_found(MessageEvent *e)
{
unsigned from, to;
bool status;
@@ -77,7 +77,7 @@
std::map<std::wstring, InstancePtr>::iterator instance_map_iterator;
const InstancePtrList& instance_list = bmsc->get_instances();
InstancePtrList::const_iterator instance_list_iterator;
-
+
for(instance_list_iterator = instance_list.begin();
instance_list_iterator != instance_list.end();
instance_list_iterator++)
@@ -92,7 +92,7 @@
instance_map_iterator->second.get()->set_attribute(lexical_order_attribute, num);
num++;
}
-
+
create_from_bmsc_with_param(bmsc, lexical_order_attribute, num);
for(instance_list_iterator = instance_list.begin();
Modified: trunk/src/check/pseudocode/communication_graph.h
===================================================================
--- trunk/src/check/pseudocode/communication_graph.h 2013-03-21 17:02:30 UTC (rev 1723)
+++ trunk/src/check/pseudocode/communication_graph.h 2013-03-21 18:08:46 UTC (rev 1724)
@@ -11,7 +11,7 @@
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
* Lesser General Public License for more details.
*
- * Copyright (c) 2008 V\xE1clav Vacek <va...@ic...>
+ * Copyright (c) 2008 Vaclav Vacek <va...@ic...>
*
* $Id$
*/
@@ -88,7 +88,7 @@
Graph& m_graph;
std::string m_index_attribute;
public:
- void on_white_event_found(Event *e);
+ void on_white_event_found(MessageEvent *e);
CommunicationGraphListener(Graph& destination, std::string index_attribute)
:m_graph(destination), m_index_attribute(index_attribute)
{}
Modified: trunk/src/check/pseudocode/msc_duplicators.cpp
===================================================================
--- trunk/src/check/pseudocode/msc_duplicators.cpp 2013-03-21 17:02:30 UTC (rev 1723)
+++ trunk/src/check/pseudocode/msc_duplicators.cpp 2013-03-21 18:08:46 UTC (rev 1724)
@@ -18,6 +18,7 @@
#include "check/pseudocode/msc_duplicators.h"
#include "data/dfs_instance_events_traverser.h"
+#include "data/msc/CoregionArea.h"
#include <map>
const std::string BMSC_DUPLICATOR_TRAVERSING_ATTR = "BDcolor";
@@ -104,10 +105,10 @@
return new_bmsc;
}
-Event* BMscDuplicator::get_event_copy(Event* e)
+MessageEvent* BMscDuplicator::get_event_copy(MessageEvent* e)
{
MscElement* elem = get_copy(e);
- return dynamic_cast<Event*>(elem);
+ return dynamic_cast<MessageEvent*>(elem);
}
BMscDuplicator::~BMscDuplicator()
@@ -368,7 +369,7 @@
}
-void EventsCreatorListener::on_white_event_found(Event* e)
+void EventsCreatorListener::on_white_event_found(MessageEvent* e)
{
if(m_last_instance!=e->get_instance())
{
@@ -377,9 +378,9 @@
m_last_instance = e->get_instance();
m_last_new_instance = new_instance.get();
}
- if(m_last_area!=e->get_general_area())
+ if(m_last_area!=e->get_area())
{
- StrictOrderArea* strict = dynamic_cast<StrictOrderArea*>(e->get_general_area());
+ StrictOrderArea* strict = dynamic_cast<StrictOrderArea*>(e->get_area());
EventAreaPtr area;
if(strict)
{
@@ -387,29 +388,21 @@
}
else
{
- area = new CoregionArea(dynamic_cast<CoregionArea*>(e->get_general_area()));
+ area = new CoregionArea(dynamic_cast<CoregionArea*>(e->get_area()));
}
m_last_new_area = area.get();
m_last_new_instance->add_area(area);
- m_last_area = e->get_general_area();
+ m_last_area = e->get_area();
}
- CoregionEvent* coreg_event = dynamic_cast<CoregionEvent*>(e);
- if(coreg_event)
- {
- CoregionEventPtr new_e = new CoregionEvent(e);
- m_duplicator->set_copy(e,new_e.get());
- dynamic_cast<CoregionArea*>(m_last_new_area)->add_event(new_e);
- }
- else
- {
- StrictEventPtr new_e = new StrictEvent(e);
- m_duplicator->set_copy(e,new_e.get());
- dynamic_cast<StrictOrderArea*>(m_last_new_area)->add_event(new_e);
- }
+
+ MessageEventPtr new_e = new MessageEvent(e);
+ m_duplicator->set_copy(e,new_e.get());
+ m_last_new_area->add_event(new_e);
+
create_successor(e);
}
-CoregionEvent* EventsCreatorListener::get_preceding_event()
+MessageEvent* EventsCreatorListener::get_preceding_event()
{
const MscElementPList& elements = m_traverser->get_reached_elements();
if(elements.size()>1)
@@ -420,33 +413,33 @@
if(dynamic_cast<CoregionEventRelation*>(*i))
{
i--;
- return dynamic_cast<CoregionEvent*>(*i);
+ return dynamic_cast<MessageEvent*>(*i);
}
}
return NULL;
}
-void EventsCreatorListener::on_gray_event_found(Event* e)
+void EventsCreatorListener::on_gray_event_found(MessageEvent* e)
{
create_successor(e);
}
-void EventsCreatorListener::on_black_event_found(Event* e)
+void EventsCreatorListener::on_black_event_found(MessageEvent* e)
{
create_successor(e);
}
-void EventsCreatorListener::create_successor(Event* e)
+void EventsCreatorListener::create_successor(MessageEvent* e)
{
- CoregionEvent* coreg_new = dynamic_cast<CoregionEvent*>(m_duplicator->get_event_copy(e));
- if(coreg_new)
+ MessageEvent* coreg_new = m_duplicator->get_event_copy(e);
+ if(coreg_new->in_coregion_area())
{
- CoregionEvent* preceding = get_preceding_event();
+ MessageEvent* preceding = get_preceding_event();
if(preceding)
{
- CoregionEvent* preceding_new = dynamic_cast<CoregionEvent*>(m_duplicator->get_event_copy(preceding));
- preceding_new->add_successor(coreg_new);
- // std::cerr << "creating coreg rel " << preceding_new << " -> " << coreg_new << std::endl;
+ MessageEvent* preceding_new = m_duplicator->get_event_copy(preceding);
+ CoregionArea* coregion = dynamic_cast<CoregionArea*>(preceding_new->get_area());
+ coregion->add_successor_rel(preceding_new, coreg_new);
}
}
}
@@ -459,14 +452,14 @@
}
-void MessagesCreatorListener::on_white_event_found(Event* e)
+void MessagesCreatorListener::on_white_event_found(MessageEvent* e)
{
- Event* event_copy = m_duplicator->get_event_copy(e);
+ MessageEvent* event_copy = m_duplicator->get_event_copy(e);
if(e->is_matched())
{
if(e->is_send())
{
- Event* matching_copy = m_duplicator->get_event_copy(e->get_matching_event());
+ MessageEvent* 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);
@@ -489,7 +482,7 @@
}
-void TimeRelationCreatorListener::on_white_event_found(Event* e)
+void TimeRelationCreatorListener::on_white_event_found(MessageEvent* e)
{
TimeRelationEventPtrList relations = e->get_time_relations();
TimeRelationEventPtrList::iterator it;
@@ -498,8 +491,8 @@
if((*it)->get_event_a()!=e)
continue;
- Event* a_copy = m_duplicator->get_event_copy((*it)->get_event_a());
- Event* b_copy = m_duplicator->get_event_copy((*it)->get_event_b());
+ MessageEvent* a_copy = m_duplicator->get_event_copy((*it)->get_event_a());
+ MessageEvent* b_copy = m_duplicator->get_event_copy((*it)->get_event_b());
TimeRelationEventPtr relation = new TimeRelationEvent((*it).get());
relation->glue_events(a_copy, b_copy);
m_duplicator->set_copy((*it).get(),relation.get());
Modified: trunk/src/check/pseudocode/msc_duplicators.h
===================================================================
--- trunk/src/check/pseudocode/msc_duplicators.h 2013-03-21 17:02:30 UTC (rev 1723)
+++ trunk/src/check/pseudocode/msc_duplicators.h 2013-03-21 18:08:46 UTC (rev 1724)
@@ -26,7 +26,6 @@
#include "check/pseudocode/export.h"
#include "check/time/time_pseudocode.h"
-typedef std::list<Event*> EventPList;
typedef std::list<ReferenceNode*> ReferenceNodePList;
typedef std::list<HMsc*> HMscPList;
typedef std::list<ConnectionNode*> ConnectionNodePList;
@@ -119,17 +118,17 @@
DFSAreaTraverser* m_traverser;
- void create_successor(Event* e);
+ void create_successor(MessageEvent* e);
- CoregionEvent* get_preceding_event();
+ MessageEvent* get_preceding_event();
public:
EventsCreatorListener(BMscDuplicator* duplicator, DFSAreaTraverser* traverser, BMsc* bmsc);
- void on_white_event_found(Event* e);
- void on_gray_event_found(Event* e);
- void on_black_event_found(Event* e);
+ void on_white_event_found(MessageEvent* e);
+ void on_gray_event_found(MessageEvent* e);
+ void on_black_event_found(MessageEvent* e);
};
@@ -143,7 +142,7 @@
MessagesCreatorListener(BMscDuplicator* duplicator);
- void on_white_event_found(Event* e);
+ void on_white_event_found(MessageEvent* e);
};
@@ -158,7 +157,7 @@
TimeRelationCreatorListener(BMscDuplicator* duplicator);
- void on_white_event_found(Event* e);
+ void on_white_event_found(MessageEvent* e);
};
@@ -181,7 +180,7 @@
~BMscDuplicator();
- Event* get_event_copy(Event* e);
+ MessageEvent* get_event_copy(MessageEvent* e);
};
/**
Modified: trunk/src/check/pseudocode/utils.cpp
===================================================================
--- trunk/src/check/pseudocode/utils.cpp 2013-03-21 17:02:30 UTC (rev 1723)
+++ trunk/src/check/pseudocode/utils.cpp 2013-03-21 18:08:46 UTC (rev 1724)
@@ -19,79 +19,6 @@
#include "check/pseudocode/utils.h"
-void EventFirstSuccessors::get_first_area_events(EventArea* area,Event* e)
-{
- if(!area)
- return;
-
- StrictOrderArea* strict = dynamic_cast<StrictOrderArea*>(area);
- if(strict)
- {
- if(strict->is_empty())
- get_first_area_events(strict->get_next_area().get(),e);
- else
- m_succs.insert(strict->get_first_event().get());
- }
- else
- {
- CoregionArea* coregion = dynamic_cast<CoregionArea*>(area);
- if(coregion->is_empty())
- get_first_area_events(coregion->get_next_area().get(),e);
- else
- {
- const CoregionEventPVector& minimals = coregion->get_minimal_events();
- CoregionEventPVector::const_iterator min;
- for(min=minimals.begin(); min!=minimals.end(); min++)
- m_succs.insert(*min);
- }
- }
-}
-
-void EventFirstSuccessors::get_strict_successors(StrictEvent *e)
-{
- if(e->get_successor().get())
- m_succs.insert(e->get_successor().get());
- else
- get_first_area_events(e->get_area()->get_next_area().get(),e);
-}
-
-
-void EventFirstSuccessors::get_coregion_successors(CoregionEvent *e)
-{
- if(e->get_successors().size()!=0)
- {
- const CoregEventRelPtrVector& successors = e->get_successors();
- CoregEventRelPtrVector::const_iterator succ;
- for(succ=successors.begin(); succ!=successors.end(); succ++)
- {
- m_succs.insert((*succ)->get_successor());
- }
- }
- else
- get_first_area_events(e->get_area()->get_next_area().get(),e);
-}
-
-void EventFirstSuccessors::get_successors(Event *e)
-{
- StrictEvent* strict = dynamic_cast<StrictEvent*>(e);
- if(strict)
- {
- get_strict_successors(strict);
- }
- else
- {
- CoregionEvent* coregion = dynamic_cast<CoregionEvent*>(e);
- get_coregion_successors(coregion);
- }
- // if its send event
- if(e->is_send() && e->get_matching_event())
- {
- m_succs.insert(e->get_matching_event());
- }
-}
-
-//////////////////////////////////////////////////////////
-
WhiteNodeMarker::WhiteNodeMarker(const std::string& mark):
m_mark(mark)
{
Modified: trunk/src/check/pseudocode/utils.h
===================================================================
--- trunk/src/check/pseudocode/utils.h 2013-03-21 17:02:30 UTC (rev 1723)
+++ trunk/src/check/pseudocode/utils.h 2013-03-21 18:08:46 UTC (rev 1724)
@@ -29,30 +29,25 @@
#include "data/node_finder.h"
#include "check/pseudocode/visual_closure_initiator.h"
#include "check/pseudocode/causal_closure_initiator.h"
+#include "data/msc.h"
typedef std::map<std::wstring,size_t> StringSizeTMap;
-typedef Event* EventP;
-typedef std::set<Event*> EventPSet;
/**
* \brief Returns event's next first successors
* if event is a send one, returns also its match event
+ * TODO: move the functionality to MessageEvent
*/
class SCPSEUDOCODE_EXPORT EventFirstSuccessors
{
-private:
- EventPSet m_succs;
- void get_first_area_events(EventArea*,Event*);
- void get_strict_successors(StrictEvent*);
- void get_coregion_successors(CoregionEvent*);
- void get_successors(Event *e);
public:
- static EventPSet get(Event* e)
+ static MessageEventPSet get(MessageEvent* e)
{
- EventFirstSuccessors first_successors;
- first_successors.get_successors(e);
- return first_successors.m_succs;
+ MessageEventPSet events = e->get_instance()->get_successor_events(e);
+ if(e->is_send() && e->get_matching_event())
+ events.insert(e->get_matching_event());
+ return events;
}
}; // EventFirstSuccessors
@@ -87,16 +82,16 @@
class TopologyOrderListener:public EventFinishedListener
{
- EventPList* m_topology;
+ MessageEventPList* m_topology;
public:
- TopologyOrderListener(EventPList* topology)
+ TopologyOrderListener(MessageEventPList* topology)
{
m_topology = topology;
}
- void on_event_finished(Event* e)
+ void on_event_finished(MessageEvent* e)
{
m_topology->push_front(e);
}
@@ -106,7 +101,7 @@
{
public:
- static bool is_matched_receive(Event* e)
+ static bool is_matched_receive(MessageEvent* e)
{
return e->is_matched() && e->is_receive();
}
@@ -122,7 +117,7 @@
{
private:
BMscPtr m_bmsc;
- EventPList m_event_topology;
+ MessageEventPList m_event_topology;
ChannelMapperPtr m_mapper;
VisualClosureInitiator* m_p_visual_closure_initiator;
@@ -137,7 +132,7 @@
traverser.traverse(m_bmsc);
m_event_topology = topology_listener.get_topology();
- EventPVector topology(topology_listener.get_topology().size());
+ MessageEventPVector topology(topology_listener.get_topology().size());
topology.assign(topology_listener.get_topology().begin(),topology_listener.get_topology().end());
m_p_visual_closure_initiator = new VisualClosureInitiator();
m_p_visual_closure_initiator->initialize(topology); //here should be topologically sorted elements
@@ -190,7 +185,7 @@
/**
* \return true if a is less then b (a<b) or equal (a=b)
*/
- bool visual_is_leq(Event* a,Event *b)
+ bool visual_is_leq(MessageEvent* a,MessageEvent *b)
{
BoolVector vector = m_p_visual_closure_initiator->get_visual_closure(a);
@@ -200,7 +195,7 @@
/**
* \return true if a is less then b (a<b) or equal (a=b)
*/
- bool causal_is_leq(Event* a,Event *b)
+ bool causal_is_leq(MessageEvent* a,MessageEvent *b)
{
if(!m_p_causal_closure_initiator)
throw std::runtime_error("Causal closure hasnt been initialized!");
@@ -213,9 +208,9 @@
/**
* \return vector of topologically sorted events according to visual order
*/
- const EventPVector get_topology()
+ const MessageEventPVector get_topology()
{
- EventPVector topology(m_event_topology.size());
+ MessageEventPVector topology(m_event_topology.size());
topology.assign(m_event_topology.begin(),m_event_topology.end());
return topology;
}
@@ -321,7 +316,7 @@
* pick up all events
* (WhiteNodeFoundListener)
*/
-class AllReachableEventPVector:public std::vector<EventP>, public WhiteEventFoundListener
+class AllReachableEventPVector:public std::vector<MessageEventP>, public WhiteEventFoundListener
{
private:
DFSEventsTraverser m_traverser;
@@ -346,7 +341,7 @@
m_traverser.remove_white_event_found_listeners();
}
- void on_white_event_found(Event* e)
+ void on_white_event_found(MessageEvent* e)
{
this->push_back(e);
}
@@ -357,7 +352,7 @@
* Go through the vector of all events using AllReachableEventPVector
* and using EventTopologyHandler choose minimal events
*/
-class MinimalEventPList: public std::list<EventP>
+class MinimalEventPList: public std::list<MessageEventP>
{
private:
AllReachableEventPVector m_events;
@@ -366,8 +361,8 @@
public:
MinimalEventPList(BMscPtr bmsc):m_events(bmsc),m_event_top(bmsc)
{
- EventPVector::iterator it;
- EventPVector::iterator it_b;
+ MessageEventPVector::iterator it;
+ MessageEventPVector::iterator it_b;
for (it=m_events.begin();it!=m_events.end();it++)
{
bool is_minimal = true;
@@ -390,7 +385,7 @@
* Go through the vector of all events using AllReachableEventPVector
* and using EventTopologyHandler choose maximal events
*/
-class MaximalEventPList: public std::list<EventP>
+class MaximalEventPList: public std::list<MessageEventP>
{
private:
AllReachableEventPVector m_events;
@@ -399,8 +394,8 @@
public:
MaximalEventPList(BMscPtr bmsc):m_events(bmsc),m_event_top(bmsc)
{
- EventPVector::iterator it;
- EventPVector::iterator it_b;
+ MessageEventPVector::iterator it;
+ MessageEventPVector::iterator it_b;
for (it=m_events.begin();it!=m_events.end();it++)
{
bool is_maximal = true;
Modified: trunk/src/check/pseudocode/visual_closure_initiator.cpp
===================================================================
--- trunk/src/check/pseudocode/visual_closure_initiator.cpp 2013-03-21 17:02:30 UTC (rev 1723)
+++ trunk/src/check/pseudocode/visual_closure_initiator.cpp 2013-03-21 18:08:46 UTC (rev 1724)
@@ -33,29 +33,15 @@
void VisualClosureInitiator::make_closure(std::vector<BoolVector*>& closure_matrix, size_t succ_index, EventArea* pred_area)
{
- if(pred_area->is_empty())
- {
- if(!pred_area->is_first_area())
- make_closure(closure_matrix,succ_index,pred_area->get_previous_area());
+ while (pred_area->is_empty()) {
+ pred_area = pred_area->get_previous_area();
+ if (pred_area == NULL)
+ return; // nothing to do, there is no non-empty predecessor area
}
- else
- {
- StrictOrderArea* strict_area = dynamic_cast<StrictOrderArea*>(pred_area);
- if(strict_area)
- {
- make_closure(closure_matrix,succ_index,get_topology_index(strict_area->get_last_event().get()));
- }
- else
- {
- CoregionArea* coregion_area = dynamic_cast<CoregionArea*>(pred_area);
- CoregionEventPVector::const_iterator max;
- const CoregionEventPVector& max_events = coregion_area->get_maximal_events();
- for(max=max_events.begin();max!=max_events.end();max++)
- {
- make_closure(closure_matrix,succ_index,get_topology_index(*max));
- }
- }
- }
+
+ MessageEventPSet max_events = pred_area->get_maximal_events();
+ for (MessageEventPSet::const_iterator it = max_events.begin(); it != max_events.end(); ++it)
+ make_closure(closure_matrix, succ_index, get_topology_index(*it));
}
VisualClosureInitiator::~VisualClosureInitiator()
@@ -65,7 +51,7 @@
void VisualClosureInitiator::cleanup_attributes()
{
- EventPList::iterator e;
+ MessageEventPList::iterator e;
for(e=m_modified_events.begin();e!=m_modified_events.end();e++)
{
(*e)->remove_attribute<size_t>(m_topology_index_attribute);
@@ -74,14 +60,14 @@
m_modified_events.erase(m_modified_events.begin(),m_modified_events.end());
}
-void VisualClosureInitiator::initialize(const EventPVector& event_topology)
+void VisualClosureInitiator::initialize(const MessageEventPVector& event_topology)
{
//initialize vectors of visual closure of events
//closure[x][y]==true <=> x<*y
std::vector<BoolVector*> closure(event_topology.size());
for(size_t i=0;i<event_topology.size();i++)
{
- Event* event = event_topology[i];
+ MessageEvent* event = event_topology[i];
BoolVector& event_closure = get_visual_closure(event);
event_closure.resize(event_topology.size(),false);
set_topology_index(event,i);
@@ -92,13 +78,12 @@
make_closure(closure,event_topology);
}
-void VisualClosureInitiator::make_closure(std::vector<BoolVector*>& closure,
- const EventPVector& event_topology)
+void VisualClosureInitiator::make_closure(std::vector<BoolVector*>& closure, const MessageEventPVector& event_topology)
{
for(size_t e=0; e<event_topology.size(); e++)
{
(*closure[e])[e] = true;
- Event* event_e = event_topology[e];
+ MessageEvent* event_e = event_topology[e];
//send event is predecessor
if(event_e->is_receive() && event_e->is_matched())
{
@@ -108,46 +93,27 @@
}
}
-void VisualClosureInitiator::make_closure(std::vector<BoolVector*>& closure,
- size_t e, Event* event_e)
+void VisualClosureInitiator::make_closure(std::vector<BoolVector*>& closure, size_t e, MessageEvent* event_e)
{
- StrictEvent* strict_event = dynamic_cast<StrictEvent*>(event_e);
- if(strict_event)
+ if (event_e->is_minimal())
{
- if(!strict_event->is_first())
- {
- //complete closure with direct predecessor
- make_closure(closure,e,get_topology_index(strict_event->get_predecessor()));
- }
- else if(strict_event->get_area()->get_previous_area())
- {
- make_closure(closure,e,strict_event->get_area()->get_previous_area());
- }
+ if (event_e->get_area()->get_previous_area() != NULL)
+ make_closure(closure, e, event_e->get_area()->get_previous_area());
}
else
{
- CoregionEvent* coregion_event = dynamic_cast<CoregionEvent*>(event_e);
- if(!coregion_event->is_minimal())
- {
- //complete closure with direct predecessors
- CoregEventRelPtrVector::const_iterator pred_rel;
- const CoregEventRelPtrVector& predecessors = coregion_event->get_predecessors();
- for(pred_rel=predecessors.begin();pred_rel!=predecessors.end();pred_rel++)
- make_closure(closure,e,get_topology_index((*pred_rel)->get_predecessor()));
- }
- else if(coregion_event->get_area()->get_previous_area())
- {
- make_closure(closure,e,coregion_event->get_area()->get_previous_area());
- }
+ MessageEventPSet preds = event_e->get_predecessor_events();
+ for (MessageEventPSet::const_iterator it = preds.begin(); it != preds.end(); ++it)
+ make_closure(closure, e, get_topology_index(*it));
}
}
-size_t VisualClosureInitiator::get_topology_index(Event* e)
+size_t VisualClosureInitiator::get_topology_index(MessageEvent* e)
{
return e->get_attribute<size_t>(m_topology_index_attribute,0);
}
-void VisualClosureInitiator::set_topology_index(Event* e,size_t i)
+void VisualClosureInitiator::set_topology_index(MessageEvent* e,size_t i)
{
e->set_attribute<size_t>(m_topology_index_attribute,i);
}
Modified: trunk/src/check/pseudocode/visual_closure_initiator.h
===================================================================
--- trunk/src/check/pseudocode/visual_closure_initiator.h 2013-03-21 17:02:30 UTC (rev 1723)
+++ trunk/src/check/pseudocode/visual_closure_initiator.h 2013-03-21 18:08:46 UTC (rev 1724)
@@ -26,8 +26,6 @@
#include "data/dfs_events_traverser.h"
#include "check/pseudocode/export.h"
-typedef std::list<Event*> EventPList;
-typedef std::vector<Event*> EventPVector;
typedef std::vector<bool> BoolVector;
typedef std::list<CoregionArea*> CoregionAreaPList;
@@ -39,16 +37,16 @@
protected:
- EventPList m_topology;
+ MessageEventPList m_topology;
public:
- const EventPList& get_topology()
+ const MessageEventPList& get_topology()
{
return m_topology;
}
- virtual void on_event_finished(Event* event)
+ virtual void on_event_finished(MessageEvent* event)
{
m_topology.push_front(event);
}
@@ -58,12 +56,12 @@
class SCPSEUDOCODE_EXPORT VisualClosureInitiator
{
-protected:
+private:
/**
* Events with modified attributes
*/
- EventPList m_modified_events;
+ MessageEventPList m_modified_events;
/**
* Name of topology attribute.
@@ -88,12 +86,12 @@
/**
* Completes closure_matrix for topologicaly sorted event - event_topology
*/
- void make_closure(std::vector<BoolVector*>& closure_matrix, const EventPVector& event_topology);
+ void make_closure(std::vector<BoolVector*>& closure_matrix, const MessageEventPVector& event_topology);
/**
* Completes closure_matrix for event_e with index e
*/
- void make_closure(std::vector<BoolVector*>& closure_matrix, size_t e, Event* event_e);
+ void make_closure(std::vector<BoolVector*>& closure_matrix, size_t e, MessageEvent* event_e);
public:
@@ -120,12 +118,12 @@
* @param event_topology - topologically sorted events of BMsc
* (i<j <=> (event_topology[i]<event_topology[j] or event_topology[i]||event_topology[j]).
*/
- void initialize(const EventPVector& event_topology);
+ void initialize(const MessageEventPVector& event_topology);
/**
* Getter of visual closure attribute of e.
*/
- BoolVector& get_visual_closure(Event* e)
+ BoolVector& get_visual_closure(MessageEvent* e)
{
static BoolVector empty(1,false);
return e->get_attribute<BoolVector>(m_visual_closure_attribute,empty);
@@ -134,12 +132,12 @@
/**
* Getter of topology index attribute of e.
*/
- size_t get_topology_index(Event* e);
+ size_t get_topology_index(MessageEvent* e);
/**
* Setter of topology index attribute of e.
*/
- void set_topology_index(Event* e,size_t i);
+ void set_topology_index(MessageEvent* e,size_t i);
/**
* Cleans up set attributes.
Deleted: trunk/src/check/race/bmsc_race_checker.cpp
===================================================================
--- trunk/src/check/race/bmsc_race_checker.cpp 2013-03-21 17:02:30 UTC (rev 1723)
+++ trunk/src/check/race/bmsc_race_checker.cpp 2013-03-21 18:08:46 UTC (rev 1724)
@@ -1,174 +0,0 @@
-/*
- * scstudio - Sequence Chart Studio
- * http://scstudio.sourceforge.net
- *
- * This library is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public
- * License version 2.1, as published by the Free Software Foundation.
- *
- * This library is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * Copyright (c) 2008 Jindra Babica <ba...@ma...>
- *
- * $Id$
- */
-
-#include "check/race/race_checker.h"
-
-void MinimalEventsInitiator::on_white_node_found(ReferenceNode* node)
-{
- BMscPtr b = node->get_bmsc();
- const InstancePtrList& instances = b->get_instances();
- //compute minimal Events of Instances
- EventPList minimal_events;
- InstancePtrList::const_iterator i;
- for(i=instances.begin();i!=instances.end();i++)
- {
- EventPList* events = DFSInstanceEventsTraverser::topology_order(*i);
- EventPList::const_iterator e1 = events->begin();
- while(e1!=events->end())
- {
- EventPList::const_iterator e2 = events->begin();
- while(e2!=events->end())
- {
- if(e1!=e2)
- {
- Event* e = *e2;
- BoolVector& e2_causal = m_caus_initiator->get_causal_closure(*e2);
- size_t e1_index = m_vis_initiator->get_topology_index(*e1);
- //e2<<e1 => e1 isn't minimal
- if(e2_causal[e1_index]) break;
- }
- e2++;
- }
- //'while loop' hasn't found any Event e2 to be less than e1
- if(e2==events.end())
- minimal_events.push_back(*e1);
- e1++;
- }
- delete events;
- }
- /*
- For the minimal_events find Instances containing less Events.
- Note that if there exists any less Event e1 at Instance i, e1 must be grater
- or equal to some Event e2 in minimal_events, therefore we will use only
- minimal_events to seek.
- */
- EventPList::const_iterator e;
- ExtremeEvents& extreme_events = get_minimal_events(b.get());
- for(e=minimal_events.begin();e!=minimal_events.end();e++)
- {
- EventDependentInstances e_instances(*e,m_instance_marker.get_count());
- size_t e_index = m_vis_initiator->get_topology_index(*e);
- EventPList::const_iterator f;
- for(f=minimal_events.begin();f!=minimal_events.end();f++)
- {
- //if f is less than e then Instance of f must be inserted
- BoolVector& closure = m_caus_initiator->get_causal_closure(*f);
- if(closure[e_index])
- e_instances.set_dependent(
- m_instance_marker->get_id((*f)->get_instance()));
- }
- extreme_events.add_extreme_event(e_instances);
- }
- m_modified_bmscs.push_back(b.get());
-}
-
-BMsc* BMscRaceChecker::create_counter_example(Event* e1, Event* e2)
-{
- BMsc* bmsc = new BMsc(e1->get_instance()->get_bmsc());
- InstancePtr common_instance = new Instance(bmsc,e1->get_instance());
- bmsc->add_instance(common_instance);
- BoolVector& e2_causal = m_causal_initiator.get_causal_closure(e2);
- size_t e1_index = m_visual_initiator.get_topology_index(e1);
- MscMessagePtr e1_message;
- if(e1->is_send())
- e1_message = new MscMessage(
- common_instance.get(),NULL,e1->get_message().get());
- else
- e1_message = new MscMessage(
- NULL,common_instance.get(),e1->get_message().get());
- MscMessagePtr e2_message;
- if(e2->is_send())
- e2_message = new MscMessage(
- common_instance.get(),NULL,e2->get_message().get());
- else
- e2_message = new MscMessage(
- NULL,common_instance.get(),e2->get_message().get());
- //e2 << e1
- if(e2_causal[e1_index])
- {
- StrictOrderAreaPtr common_strict = new StrictOrderArea(
- common_instance.get());
- StrictEventPtr e1_strict = new StrictEvent(common_strict.get(),e1_message,e1);
- StrictEventPtr e2_strict = new StrictEvent(common_strict.get(),e2_message,e2);
- common_strict->set_first(e1_strict);
- e1_strict->set_successor(e2_strict);
- common_instance->set_first(common_strict);
- }
- //e2 || e1
- else
- {
- CoregionAreaPtr common_coregion = new CoregionArea(common_instance.get());
- CoregionEvent* e1_coregion = new CoregionEvent(
- common_coregion.get(),e1_message,e1);
- CoregionEvent* e2_coregion = new CoregionEvent(
- common_coregion.get(),e2_message,e2);
- common_coregion->add_minimal_event(e1_coregion);
- common_coregion->add_minimal_event(e2_coregion);
- common_instance->set_first(common_coregion);
- }
- return bmsc;
-}
-
-BMscPtr BMscRaceChecker::check(BMscPtr bmsc, ChannelMapperPtr mapper)
-{
- DFSEventsTraverser traverser;
- TopologicalOrderListener topology_listener;
- traverser.add_event_finished_listener(this);
- traverser.traverse(bmsc);
- EventPVector topology(
- topology_listener.get_topology().begin(),
- topology_listener.get_topology().end()
- );
- m_visual_initiator.initialize(topology);
- m_causal_initiator.initialize(topology,m_visual_initiator,mapper);
- OrderCheckerListener order_checker_listener(&m_visual_initiator);
- DFSInstanceEventsTraverser instance_traverser;
- for(size_t i = 0; i < topology.size(); i++)
- {
- //in this block checkout whether there is any Event in race with topology[i]
- order_checker_listener.reset(
- topology[i],
- &m_visual_initiator.get_visual_closure(topology[i]),
- &m_causal_initiator.get_causal_closure(topology[i]));
- try
- {
- instance_traverser.traverse(topology[i]->get_instance());
- instance_traverser.cleanup_traversing_attributes();
- }
- catch(EventRaceException& e)
- {
- instance_traverser.cleanup_traversing_attributes();
- return create_counter_example(topology[i],e->get_event());
- }
- }
- return BMscPtr();
-}
-
-void BMscRaceChecker::cleanup_attributes()
-{
- m_visual_initiator.cleanup_attributes();
- m_causal_initiator.cleanup_attributes();
- while(!m_modified_instaces.empty())
- {
- Instance* i = m_modified_instaces.front();
- m_modified_instaces.pop_front();
- i->remove_attribute<EventPList>(m_instance_events_attribute);
- }
-}
-
-// $Id$
Deleted: trunk/src/check/race/bmsc_race_checker.h
===================================================================
--- trunk/src/check/race/bmsc_race_checker.h 2013-03-21 17:02:30 UTC (rev 1723)
+++ trunk/src/check/race/bmsc_race_checker.h 2013-03-21 18:08:46 UTC (rev 1724)
@@ -1,77 +0,0 @@
-/*
- * scstudio - Sequence Chart Studio
- * http://scstudio.sourceforge.net
- *
- * This library is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public
- * License version 2.1, as published by the Free Software Foundation.
- *
- * This library is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * Copyright (c) 2008 Jindra Babica <ba...@ma...>
- *
- * $Id$
- */
-
-#ifndef _BMSC_RACE_CHECKER_H
-#define _BMSC_RACE_CHECKER_H
-
-#include "data/msc.h"
-#include "data/dfs_events_traverser.h"
-#include "check/pseudocode/visual_closure_initiator.h"
-#include "check/pseudocode/causal_closure_initiator.h"
-
-typedef std::list<Instance*> InstancePList;
-
-class BMscRaceChecker:
-public BMscChecker,
-public TopologicalOrderListener
-{
-
-protected:
-
- VisualClosureInitiator m_visual_initiator;
-
- CausalClosureInitiator m_causal_initiator;
-
- static const std::string m_instance_events_attribute;
-
- InstancePList m_modified_instaces;
-
- EventPList& get_instance_events(Instance* i)
- {
- ...
[truncated message content] |
