Menu
▾
▴
[Scstudio-commits] SF.net SVN: scstudio:[1864] trunk
|
From: <xb...@us...> - 2013-10-11 09:27:09
|
Revision: 1864
http://sourceforge.net/p/scstudio/code/1864
Author: xborza
Date: 2013-10-11 09:27:00 +0000 (Fri, 11 Oct 2013)
Log Message:
-----------
/trunk merged with with ondra/conditions branch
Modified Paths:
--------------
trunk/doc/help/CMakeLists.txt
trunk/doc/help/frontend/automatic_drawing.body.htm
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.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/time/constraint_syntax.cpp
trunk/src/check/time/hmsc_all_paths.cpp
trunk/src/check/time/hmsc_all_paths.h
trunk/src/check/time/module.cpp
trunk/src/check/time/pcap_time.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/z120.h
trunk/src/data/Z120/z120_save.cpp
trunk/src/data/beautify/layout_optimizer.cpp
trunk/src/data/beautify/time_transformer.cpp
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/Condition.h
trunk/src/data/msc/ConditionNode.cpp
trunk/src/data/msc/ConditionNode.h
trunk/src/data/msc/CoregionArea.cpp
trunk/src/data/msc/CoregionArea.h
trunk/src/data/msc/CoregionEventRelation.h
trunk/src/data/msc/Event.cpp
trunk/src/data/msc/Event.h
trunk/src/data/msc/EventArea.cpp
trunk/src/data/msc/EventArea.h
trunk/src/data/msc/EventTmpl.h
trunk/src/data/msc/Instance.cpp
trunk/src/data/msc/Instance.h
trunk/src/data/msc/LocalAction.h
trunk/src/data/msc/MessageEvent.cpp
trunk/src/data/msc/MessageEvent.h
trunk/src/data/msc/MscMessage.h
trunk/src/data/msc/StrictOrderArea.cpp
trunk/src/data/msc/StrictOrderArea.h
trunk/src/data/msc/time/TimeRelationEvent.cpp
trunk/src/data/msc/time/TimeRelationEvent.h
trunk/src/data/msc.h
trunk/src/data/msc_types.h
trunk/src/data/mscgen/MscgenContext.cpp
trunk/src/data/pcap/pcap_handler.cpp
trunk/src/data/pcap/pcap_handler.h
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/membership_additional.cpp
trunk/src/membership/membership_additional.h
trunk/src/membership/membership_alg.cpp
trunk/src/membership/membership_base.h
trunk/src/membership/membership_time.cpp
trunk/src/montecarlo/montecarlo.cpp
trunk/src/montecarlo/montecarlo.h
trunk/src/view/visio/addon/extract.cpp
trunk/src/view/visio/addon/extract.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_position_test/exporttex_position_test.cpp
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/time/time_race/CMakeLists.txt
trunk/tests/universal_boundedness_checker_test.cpp
Added Paths:
-----------
trunk/src/data/msc/Condition.cpp
trunk/src/data/msc/ConditionEvent.h
trunk/src/data/msc/LocalAction.cpp
trunk/src/data/msc/LocalActionEvent.h
trunk/tests/time/time_race/race_cond_neg1.mpr
trunk/tests/time/time_race/race_cond_neg1.mpr.result
trunk/tests/time/time_race/race_cond_neg1.vsd
trunk/tests/time/time_race/race_cond_neg2.mpr
trunk/tests/time/time_race/race_cond_neg2.mpr.result
trunk/tests/time/time_race/race_cond_neg2.vsd
trunk/tests/time/time_race/race_cond_pos1.mpr
trunk/tests/time/time_race/race_cond_pos1.vsd
trunk/tests/time/time_race/race_cond_pos2.mpr
trunk/tests/time/time_race/race_cond_pos2.vsd
trunk/tests/time/time_race/race_cond_pos3.mpr
trunk/tests/time/time_race/race_cond_pos3.vsd
Removed Paths:
-------------
trunk/src/data/msc/MscMessage.cpp
Property Changed:
----------------
trunk/doc/help/frontend/
trunk/src/data/msc/EventArea.cpp
trunk/src/data/msc/MessageEvent.h
trunk/src/data/msc/StrictOrderArea.cpp
Modified: trunk/doc/help/CMakeLists.txt
===================================================================
--- trunk/doc/help/CMakeLists.txt 2013-09-26 12:48:24 UTC (rev 1863)
+++ trunk/doc/help/CMakeLists.txt 2013-10-11 09:27:00 UTC (rev 1864)
@@ -18,7 +18,6 @@
fifo/fifo.html
frontend/automatic_drawing.html
frontend/flip_message_direction.html
- frontend/message_jumping.html
frontend/message_numbering.html
frontend/settings.html
frontend/shape_selection.html
Index: trunk/doc/help/frontend
===================================================================
--- trunk/doc/help/frontend 2013-09-26 12:48:24 UTC (rev 1863)
+++ trunk/doc/help/frontend 2013-10-11 09:27:00 UTC (rev 1864)
Property changes on: trunk/doc/help/frontend
___________________________________________________________________
Added: svn:global-ignores
## -0,0 +1 ##
+message_jumping.body.htm
Modified: trunk/doc/help/frontend/automatic_drawing.body.htm
===================================================================
--- trunk/doc/help/frontend/automatic_drawing.body.htm 2013-09-26 12:48:24 UTC (rev 1863)
+++ trunk/doc/help/frontend/automatic_drawing.body.htm 2013-10-11 09:27:00 UTC (rev 1864)
@@ -75,11 +75,15 @@
</p>
<ul>
<li>
- if there are no instances selected, all instances on the page are taken (there have to be at least 2 instances on the page);
+ if there are no instances selected, all instances on the page are taken;
</li>
<li>
- otherwise, all selected instances (at least 2) are taken into account.
+ if there is exactly one instance selected, then SCStudio waits for
+ another instance to be selected;
</li>
+ <li>
+ otherwise, all selected instances are taken into account.
+ </li>
</ul>
From all of these instances, the leftmost and the rightmost instances are
recognized as the first and last instance in the message sequence. (During
Modified: trunk/src/check/localchoice/local_choice_checker.cpp
===================================================================
--- trunk/src/check/localchoice/local_choice_checker.cpp 2013-09-26 12:48:24 UTC (rev 1863)
+++ trunk/src/check/localchoice/local_choice_checker.cpp 2013-10-11 09:27:00 UTC (rev 1864)
@@ -67,7 +67,7 @@
current_node->set_attribute(LocalChoiceChecker::lc_nip_attribute, nip);
}
-void BMscInitListener::on_white_event_found(MessageEvent *e)
+void BMscInitListener::on_white_event_found(Event *e)
{
if(m_first) //Still looking for a possibly first event in the instance
{
@@ -81,7 +81,8 @@
{
if(e->is_minimal())
{
- if(e->is_send())
+ MessageEvent* me = dynamic_cast<MessageEvent*>(e);
+ if(me != NULL && me->is_send())
m_mep = true;
}
else //the event is not minimal
@@ -95,7 +96,8 @@
m_first = false;
if(m_first_coregion == NULL)
{
- if(e->is_send())
+ MessageEvent* me = dynamic_cast<MessageEvent*>(e);
+ if(me != NULL && me->is_send())
m_mep = true;
}
}
Modified: trunk/src/check/localchoice/local_choice_checker.h
===================================================================
--- trunk/src/check/localchoice/local_choice_checker.h 2013-09-26 12:48:24 UTC (rev 1863)
+++ trunk/src/check/localchoice/local_choice_checker.h 2013-10-11 09:27:00 UTC (rev 1864)
@@ -105,7 +105,7 @@
bool m_mep;
CoregionArea *m_first_coregion;
public:
- void on_white_event_found(MessageEvent *e);
+ void on_white_event_found(Event *e);
BMscInitListener(void)
:m_idle(true),m_first(true),m_mep(false), m_first_coregion(NULL)
{}
Modified: trunk/src/check/order/acyclic_checker.cpp
===================================================================
--- trunk/src/check/order/acyclic_checker.cpp 2013-09-26 12:48:24 UTC (rev 1863)
+++ trunk/src/check/order/acyclic_checker.cpp 2013-10-11 09:27:00 UTC (rev 1864)
@@ -57,8 +57,8 @@
BMscDuplicator duplicator;
for(it = bmsc->get_instances().begin(); it != bmsc->get_instances().end(); it++)
{
- const MessageEventPList min_events = (*it)->get_minimal_events();
- for (MessageEventPList::const_iterator i = min_events.begin(); i != min_events.end(); ++i)
+ const EventPList min_events = (*it)->get_minimal_events();
+ for (EventPList::const_iterator i = min_events.begin(); i != min_events.end(); ++i)
{
ConnectionNode* node = (*i)->get_attribute<ConnectionNode*>("ACC_node", NULL);
start->add_successor(node);
@@ -80,7 +80,7 @@
cono = dynamic_cast<ConnectionNode*>((*eit));
if(cono)
{
- MessageEventP e = cono->get_attribute<MessageEventP>("ACC_event", NULL);
+ EventP e = cono->get_attribute<EventP>("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-09-26 12:48:24 UTC (rev 1863)
+++ trunk/src/check/order/acyclic_checker.h 2013-10-11 09:27:00 UTC (rev 1864)
@@ -49,7 +49,7 @@
AssignHMscListener(HMsc *hmsc)
:m_hmsc(hmsc)
{}
- void on_white_event_found(MessageEvent *e)
+ void on_white_event_found(Event *e)
{
ConnectionNode *node = new ConnectionNode();
m_hmsc->add_node(node);
@@ -75,7 +75,7 @@
class InstanceSuccessors: public EventSuccessorListener
{
public:
- void on_event_successor(MessageEvent *event, MessageEvent *successor)
+ void on_event_successor(Event *event, Event *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(MessageEvent *e)
+ void on_white_event_found(Event *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<MessageEvent*>("ACC_event");
+ node->remove_attribute<Event*>("ACC_event");
e->remove_attribute<ConnectionNode*>("ACC_node");
}
};
Modified: trunk/src/check/order/fifo_checker.cpp
===================================================================
--- trunk/src/check/order/fifo_checker.cpp 2013-09-26 12:48:24 UTC (rev 1863)
+++ trunk/src/check/order/fifo_checker.cpp 2013-10-11 09:27:00 UTC (rev 1864)
@@ -40,6 +40,7 @@
{
//event is surely complete
MessageEvent* copy = duplicator.get_event_copy(events[i]);
+ assert(copy->get_complete_message() != NULL); // better way of saying something is sure
copy->get_complete_message()->set_marked(MARKED);
}
return new_bmsc;
@@ -53,8 +54,7 @@
DFSEventsTraverser traverser;
traverser.add_event_finished_listener(&topology_listener);
traverser.traverse(bmsc);
- MessageEventPVector topology(topology_listener.get_topology().size());
- topology.assign(
+ EventPVector topology(
topology_listener.get_topology().begin(),
topology_listener.get_topology().end()
);
@@ -65,13 +65,16 @@
BoolVector& closure_e = closure_initiator.get_visual_closure(topology[e]);
for(size_t f=0; f<topology.size(); f++)
{
- if(topology[e]->is_receive() && topology[f]->is_receive() &&
- topology[e]->is_matched() && topology[f]->is_matched() &&
- mapper->same_channel(topology[e],topology[f]) && closure_e[f] &&
- !closure_initiator.get_visual_closure(topology[e]->get_matching_event())[
- closure_initiator.get_topology_index(topology[f]->get_matching_event())])
+ MessageEventP me = dynamic_cast<MessageEventP>(topology[e]);
+ MessageEventP mf = dynamic_cast<MessageEventP>(topology[f]);
+
+ if(me != NULL && mf != NULL &&
+ me->is_receive() && mf->is_receive() &&
+ me->is_matched() && mf->is_matched() &&
+ mapper->same_channel(me, mf) && closure_e[f] &&
+ !closure_initiator.get_visual_closure(me->get_matching_event())[closure_initiator.get_topology_index(mf->get_matching_event())])
{
- result.push_back(create_counter_example(bmsc,topology[e],topology[f]));
+ result.push_back(create_counter_example(bmsc, me, mf));
}
}
}
@@ -83,7 +86,7 @@
{
while(!m_modified_events.empty())
{
- MessageEvent* e = m_modified_events.top();
+ Event* 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-09-26 12:48:24 UTC (rev 1863)
+++ trunk/src/check/order/fifo_checker.h 2013-10-11 09:27:00 UTC (rev 1864)
@@ -55,7 +55,7 @@
/**
* Events with modified dynamic attributes
*/
- MessageEventPStack m_modified_events;
+ EventPStack m_modified_events;
BMscPtr create_counter_example(BMscPtr& bmsc, MessageEvent* receive1, MessageEvent* receive2);
@@ -65,7 +65,7 @@
* An e1 is supposed to be before e2. If this holds true is returned, false
* otherwise.
*/
- bool consistent_order(VisualClosureInitiator& initiator, MessageEvent* e1, MessageEvent* e2)
+ bool consistent_order(VisualClosureInitiator& initiator, Event* e1, Event* e2)
{
BoolVector& e1_closure = initiator.get_visual_closure(e1);
size_t e2_index = initiator.get_topology_index(e2);
@@ -130,7 +130,7 @@
/**
* Setter of channel id attribute of message.
*/
- void set_channel_id(MessageEvent* e, size_t id)
+ void set_channel_id(Event* e, size_t id)
{
e->set_attribute<size_t>(channel_id_attribute,id);
}
@@ -138,7 +138,7 @@
/**
* Getter of channel id attribute of m.
*/
- size_t get_channel_id(MessageEvent* e)
+ size_t get_channel_id(Event* e)
{
return e->get_attribute<size_t>(channel_id_attribute,0);
}
@@ -148,9 +148,10 @@
*
* MessageEvent should be checked if it is receive event and has matching event.
*/
- static bool should_be_checked(MessageEvent* e)
+ static bool should_be_checked(Event* e)
{
- return e->is_receive() && e->is_matched();
+ MessageEvent* me = dynamic_cast<MessageEvent*>(e);
+ return (me != NULL && me->is_receive() && me->is_matched());
}
};
Modified: trunk/src/check/pseudocode/causal_closure_initiator.cpp
===================================================================
--- trunk/src/check/pseudocode/causal_closure_initiator.cpp 2013-09-26 12:48:24 UTC (rev 1863)
+++ trunk/src/check/pseudocode/causal_closure_initiator.cpp 2013-10-11 09:27:00 UTC (rev 1864)
@@ -24,23 +24,22 @@
{
while(!m_modified_events.empty())
{
- MessageEvent* e = m_modified_events.top();
+ Event* e = m_modified_events.top();
e->remove_attribute<BoolVector>(m_causal_closure_attribute);
m_modified_events.pop();
}
}
-void CausalClosureInitiator::initialize(const MessageEventPVector& events,
+void CausalClosureInitiator::initialize(const EventPVector& events,
VisualClosureInitiator& visual_closure_init, ChannelMapperPtr mapper)
{
//initialize matrix
size_t events_count = events.size();
- 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++)
{
- MessageEvent* i_event = events[i];
+ Event* i_event = events[i];
BoolVector& causal_closure = get_causal_closure(i_event);
causal_closure.resize(events_count,false);
closure[i] = &causal_closure;
@@ -48,33 +47,40 @@
//for any event e: e << e
causal_closure[i] = true;
//send event << receive matching event
- if(i_event->is_send() && i_event->is_matched())
- causal_closure[visual_closure_init.get_topology_index(
- i_event->get_matching_event())] = true;
+ MessageEvent* i_msg_event = dynamic_cast<MessageEvent*>(i_event);
+ if(i_msg_event != NULL && i_msg_event->is_send() && i_msg_event->is_matched())
+ {
+ size_t topo_index = visual_closure_init.get_topology_index(i_msg_event->get_matching_event());
+ causal_closure[topo_index] = true;
+ }
}
for(size_t i=0;i<events_count;i++)
{
- MessageEvent* i_event = events[i];
+ Event* 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++)
{
- 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
+ Event* j_event = events[j];
+ MessageEvent* j_msg_event = dynamic_cast<MessageEvent*>(j_event);
+
if(i_event->get_instance()==j_event->get_instance() &&
- !j_event->is_receive() && i_visual_closure[j])
+ j_msg_event != NULL && !j_msg_event->is_receive() && i_visual_closure[j])
{
+ //i_event and j_event are from the same instance, j_event is send event and
+ //i_event < j_event
i_causal_closure[j] = true;
}
- //i_event and j_event are send events of the same channel and i_event<j_event
- if(i_event->is_send() && i_event->is_matched() &&
- j_event->is_send() && j_event->is_matched() &&
- mapper->same_channel(i_event,j_event) && i_visual_closure[j])
+
+ MessageEvent* i_msg_event = dynamic_cast<MessageEvent*>(i_event);
+ if(i_msg_event != NULL && j_msg_event != NULL &&
+ i_msg_event->is_send() && i_msg_event->is_matched() &&
+ j_msg_event->is_send() && j_msg_event->is_matched() &&
+ mapper->same_channel(i_msg_event,j_msg_event) && i_visual_closure[j])
{
- get_causal_closure(i_event->get_matching_event())[
- visual_closure_init.get_topology_index(j_event->get_matching_event())
- ] = true;
+ //i_event and j_event are send events of the same channel and i_event<j_event
+ size_t topo_index = visual_closure_init.get_topology_index(j_msg_event->get_matching_event());
+ get_causal_closure(i_msg_event->get_matching_event())[topo_index] = true;
}
}
}
Modified: trunk/src/check/pseudocode/causal_closure_initiator.h
===================================================================
--- trunk/src/check/pseudocode/causal_closure_initiator.h 2013-09-26 12:48:24 UTC (rev 1863)
+++ trunk/src/check/pseudocode/causal_closure_initiator.h 2013-10-11 09:27:00 UTC (rev 1864)
@@ -35,7 +35,7 @@
/**
* Used for cleaning up attributes.
*/
- MessageEventPStack m_modified_events;
+ EventPStack m_modified_events;
/**
* Name of causal closure attribute.
@@ -75,7 +75,7 @@
/**
* Getter of causal closure attribute of e.
*/
- BoolVector& get_causal_closure(MessageEvent* e)
+ BoolVector& get_causal_closure(Event* e)
{
static BoolVector empty(1,false);
return e->get_attribute<BoolVector>(m_causal_closure_attribute,empty);
@@ -90,7 +90,7 @@
* @param events - topologically sorted events used for visual_closure_init's initialization
* @param visual_closure_init - initialized VisualClosureInitiator
*/
- void initialize(const MessageEventPVector& events,
+ void initialize(const EventPVector& events,
VisualClosureInitiator& visual_closure_init, ChannelMapperPtr mapper);
/**
Modified: trunk/src/check/pseudocode/communication_graph.cpp
===================================================================
--- trunk/src/check/pseudocode/communication_graph.cpp 2013-09-26 12:48:24 UTC (rev 1863)
+++ trunk/src/check/pseudocode/communication_graph.cpp 2013-10-11 09:27:00 UTC (rev 1864)
@@ -20,17 +20,16 @@
const std::string CommunicationGraph::lexical_order_attribute = "lexical_order";
-void CommunicationGraphListener::on_white_event_found(MessageEvent *e)
+void CommunicationGraphListener::on_white_event_found(Event *e)
{
unsigned from, to;
bool status;
-
- if(e->is_send())
+ MessageEvent* me = dynamic_cast<MessageEvent*>(e);
+
+ if(me != NULL && me->is_send() && me->is_matched())
{
- if(!e->is_matched())
- return;
- from = e->get_instance()->get_attribute(m_index_attribute, 0, status);
- to = e->get_matching_event()->get_instance()->get_attribute(m_index_attribute, 0, status);
+ from = me->get_instance()->get_attribute(m_index_attribute, 0, status);
+ to = me->get_matching_event()->get_instance()->get_attribute(m_index_attribute, 0, status);
m_graph.at(from).at(to) += 1;
}
}
Modified: trunk/src/check/pseudocode/communication_graph.h
===================================================================
--- trunk/src/check/pseudocode/communication_graph.h 2013-09-26 12:48:24 UTC (rev 1863)
+++ trunk/src/check/pseudocode/communication_graph.h 2013-10-11 09:27:00 UTC (rev 1864)
@@ -88,7 +88,7 @@
Graph& m_graph;
std::string m_index_attribute;
public:
- void on_white_event_found(MessageEvent *e);
+ void on_white_event_found(Event *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-09-26 12:48:24 UTC (rev 1863)
+++ trunk/src/check/pseudocode/msc_duplicators.cpp 2013-10-11 09:27:00 UTC (rev 1864)
@@ -105,12 +105,6 @@
return new_bmsc;
}
-MessageEvent* BMscDuplicator::get_event_copy(MessageEvent* e)
-{
- MscElement* elem = get_copy(e);
- return dynamic_cast<MessageEvent*>(elem);
-}
-
BMscDuplicator::~BMscDuplicator()
{
}
@@ -369,7 +363,7 @@
}
-void EventsCreatorListener::on_white_event_found(MessageEvent* e)
+void EventsCreatorListener::on_white_event_found(Event* e)
{
if(m_last_instance!=e->get_instance())
{
@@ -395,14 +389,14 @@
m_last_area = e->get_area();
}
- MessageEventPtr new_e = new MessageEvent(e);
+ EventPtr new_e = e->clone();
m_duplicator->set_copy(e,new_e.get());
m_last_new_area->add_event(new_e);
create_successor(e);
}
-MessageEvent* EventsCreatorListener::get_preceding_event()
+Event* EventsCreatorListener::get_preceding_event()
{
const MscElementPList& elements = m_traverser->get_reached_elements();
if(elements.size()>1)
@@ -413,31 +407,31 @@
if(dynamic_cast<CoregionEventRelation*>(*i))
{
i--;
- return dynamic_cast<MessageEvent*>(*i);
+ return dynamic_cast<Event*>(*i);
}
}
return NULL;
}
-void EventsCreatorListener::on_gray_event_found(MessageEvent* e)
+void EventsCreatorListener::on_gray_event_found(Event* e)
{
create_successor(e);
}
-void EventsCreatorListener::on_black_event_found(MessageEvent* e)
+void EventsCreatorListener::on_black_event_found(Event* e)
{
create_successor(e);
}
-void EventsCreatorListener::create_successor(MessageEvent* e)
+void EventsCreatorListener::create_successor(Event* e)
{
- MessageEvent* coreg_new = m_duplicator->get_event_copy(e);
+ Event* coreg_new = m_duplicator->get_event_copy(e);
if(coreg_new->in_coregion_area())
{
- MessageEvent* preceding = get_preceding_event();
+ Event* preceding = get_preceding_event();
if(preceding)
{
- MessageEvent* preceding_new = m_duplicator->get_event_copy(preceding);
+ Event* 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);
}
@@ -452,25 +446,29 @@
}
-void MessagesCreatorListener::on_white_event_found(MessageEvent* e)
+void MessagesCreatorListener::on_white_event_found(Event* e)
{
- MessageEvent* event_copy = m_duplicator->get_event_copy(e);
- if(e->is_matched())
+ MessageEvent* me = dynamic_cast<MessageEvent*>(e);
+ if (me == NULL)
+ return; // events of other types ignored
+
+ MessageEvent* event_copy = m_duplicator->get_event_copy(me);
+ if(me->is_matched())
{
- if(e->is_send())
+ if(me->is_send())
{
- 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());
+ MessageEvent* matching_copy = m_duplicator->get_event_copy(me->get_matching_event());
+ MscMessagePtr complete = new CompleteMessage(event_copy,matching_copy,me->get_complete_message().get());
event_copy->set_message(complete);
matching_copy->set_message(complete);
- m_duplicator->set_copy(e->get_message().get(),complete.get());
+ m_duplicator->set_copy(me->get_message().get(),complete.get());
}
}
else
{
- MscMessagePtr incomplete = new IncompleteMessage(e->get_incomplete_message().get());
+ MscMessagePtr incomplete = new IncompleteMessage(me->get_incomplete_message().get());
event_copy->set_message(incomplete);
- m_duplicator->set_copy(e->get_message().get(),incomplete.get());
+ m_duplicator->set_copy(me->get_message().get(),incomplete.get());
}
}
@@ -482,7 +480,7 @@
}
-void TimeRelationCreatorListener::on_white_event_found(MessageEvent* e)
+void TimeRelationCreatorListener::on_white_event_found(Event* e)
{
TimeRelationEventPtrList relations = e->get_time_relations();
TimeRelationEventPtrList::iterator it;
@@ -491,16 +489,15 @@
if((*it)->get_event_a()!=e)
continue;
- 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());
+ Event* a_copy = m_duplicator->get_event_copy((*it)->get_event_a());
+ Event* 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());
if((it->get())->get_marked() == MARKED)
relation->set_marked();
}
-
}
////////////////////////////////////////////////////////////////////////
Modified: trunk/src/check/pseudocode/msc_duplicators.h
===================================================================
--- trunk/src/check/pseudocode/msc_duplicators.h 2013-09-26 12:48:24 UTC (rev 1863)
+++ trunk/src/check/pseudocode/msc_duplicators.h 2013-10-11 09:27:00 UTC (rev 1864)
@@ -42,6 +42,7 @@
virtual ~Duplicator();
+ // TODO: make this (and possibly others) a template method returning the same type it accepts, so that dynamic casts are not necessary
MscElement*& get_copy(MscElement* e);
SuccessorNode* get_copy(SuccessorNode* s)
@@ -118,17 +119,17 @@
DFSAreaTraverser* m_traverser;
- void create_successor(MessageEvent* e);
+ void create_successor(Event* e);
- MessageEvent* get_preceding_event();
+ Event* get_preceding_event();
public:
EventsCreatorListener(BMscDuplicator* duplicator, DFSAreaTraverser* traverser, BMsc* bmsc);
- void on_white_event_found(MessageEvent* e);
- void on_gray_event_found(MessageEvent* e);
- void on_black_event_found(MessageEvent* e);
+ void on_white_event_found(Event* e);
+ void on_gray_event_found(Event* e);
+ void on_black_event_found(Event* e);
};
@@ -142,7 +143,7 @@
MessagesCreatorListener(BMscDuplicator* duplicator);
- void on_white_event_found(MessageEvent* e);
+ void on_white_event_found(Event* e);
};
@@ -157,7 +158,7 @@
TimeRelationCreatorListener(BMscDuplicator* duplicator);
- void on_white_event_found(MessageEvent* e);
+ void on_white_event_found(Event* e);
};
@@ -180,13 +181,19 @@
~BMscDuplicator();
- MessageEvent* get_event_copy(MessageEvent* e);
+ template <typename EventType>
+ EventType* get_event_copy(EventType* e)
+ {
+ MscElement* elem = get_copy(e);
+ EventType* copy = dynamic_cast<EventType*>(elem);
+ assert(copy != NULL);
+ return copy;
+ }
};
/**
* \brief HMscDuplicator creates exact copy of HMsc
*/
-
class SCPSEUDOCODE_EXPORT HMscDuplicator:
public Duplicator
{
@@ -447,12 +454,12 @@
~HMscFlatPathToBMscDuplicator();
BMscPtr duplicate_path(const MscElementPList& path);
+
+ // TODO: make this a template method returning the same type it accepts, so that dynamic casts are not necessary
MscElement* get_copy_with_occurence(MscElement* element, int occurence);
+ // TODO: make this a template method returning the same type it accepts, so that dynamic casts are not necessary
MscElement* get_copy_by_ref_node(MscElement* element, ReferenceNode* ref);
-
-
-
};
Modified: trunk/src/check/pseudocode/utils.h
===================================================================
--- trunk/src/check/pseudocode/utils.h 2013-09-26 12:48:24 UTC (rev 1863)
+++ trunk/src/check/pseudocode/utils.h 2013-10-11 09:27:00 UTC (rev 1864)
@@ -37,16 +37,19 @@
/**
* \brief Returns event's next first successors
* if event is a send one, returns also its match event
- * TODO: move the functionality to MessageEvent
+ * TODO: move the functionality to Event, or MessageEvent, respectivelly (which would override it)
*/
class SCPSEUDOCODE_EXPORT EventFirstSuccessors
{
public:
- static MessageEventPSet get(MessageEvent* e)
+ static EventPSet get(const EventP e)
{
- MessageEventPSet events = e->get_instance()->get_successor_events(e);
- if(e->is_send() && e->get_matching_event())
- events.insert(e->get_matching_event());
+ EventPSet events = e->get_instance()->get_successor_events(e);
+
+ MessageEventP me = dynamic_cast<MessageEventP>(e);
+ if (me != NULL && me->is_send() && me->get_matching_event())
+ events.insert(me->get_matching_event());
+
return events;
}
}; // EventFirstSuccessors
@@ -82,31 +85,21 @@
class TopologyOrderListener:public EventFinishedListener
{
- MessageEventPList* m_topology;
+ EventPList* m_topology;
public:
- TopologyOrderListener(MessageEventPList* topology)
+ TopologyOrderListener(EventPList* topology)
{
m_topology = topology;
}
- void on_event_finished(MessageEvent* e)
+ void on_event_finished(Event* e)
{
m_topology->push_front(e);
}
};
-class EventRecognizer
-{
-public:
-
- static bool is_matched_receive(MessageEvent* e)
- {
- return e->is_matched() && e->is_receive();
- }
-};
-
/**
* \brief Handles visual closure on bmsc
* Init DFSEventsTraverser, TopologicalOrderListener
@@ -117,7 +110,7 @@
{
private:
BMscPtr m_bmsc;
- MessageEventPList m_event_topology;
+ EventPList m_event_topology;
ChannelMapperPtr m_mapper;
VisualClosureInitiator* m_p_visual_closure_initiator;
@@ -132,8 +125,10 @@
traverser.traverse(m_bmsc);
m_event_topology = topology_listener.get_topology();
- MessageEventPVector topology(topology_listener.get_topology().size());
- topology.assign(topology_listener.get_topology().begin(),topology_listener.get_topology().end());
+ EventPVector topology(
+ 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
@@ -185,7 +180,7 @@
/**
* \return true if a is less then b (a<b) or equal (a=b)
*/
- bool visual_is_leq(MessageEvent* a,MessageEvent *b)
+ bool visual_is_leq(Event* a, Event *b)
{
BoolVector vector = m_p_visual_closure_initiator->get_visual_closure(a);
@@ -195,7 +190,7 @@
/**
* \return true if a is less then b (a<b) or equal (a=b)
*/
- bool causal_is_leq(MessageEvent* a,MessageEvent *b)
+ bool causal_is_leq(Event* a, Event *b)
{
if(!m_p_causal_closure_initiator)
throw std::runtime_error("Causal closure hasnt been initialized!");
@@ -208,11 +203,9 @@
/**
* \return vector of topologically sorted events according to visual order
*/
- const MessageEventPVector get_topology()
+ const EventPVector get_topology()
{
- MessageEventPVector topology(m_event_topology.size());
- topology.assign(m_event_topology.begin(),m_event_topology.end());
- return topology;
+ return EventPVector(m_event_topology.begin(),m_event_topology.end());
}
};
@@ -316,7 +309,7 @@
* pick up all events
* (WhiteNodeFoundListener)
*/
-class AllReachableEventPVector:public std::vector<MessageEventP>, public WhiteEventFoundListener
+class AllReachableEventPVector:public std::vector<EventP>, public WhiteEventFoundListener
{
private:
DFSEventsTraverser m_traverser;
@@ -341,7 +334,7 @@
m_traverser.remove_white_event_found_listeners();
}
- void on_white_event_found(MessageEvent* e)
+ void on_white_event_found(Event* e)
{
this->push_back(e);
}
@@ -352,7 +345,7 @@
* Go through the vector of all events using AllReachableEventPVector
* and using EventTopologyHandler choose minimal events
*/
-class MinimalEventPList: public std::list<MessageEventP>
+class MinimalEventPList: public std::list<EventP>
{
private:
AllReachableEventPVector m_events;
@@ -361,8 +354,8 @@
public:
MinimalEventPList(BMscPtr bmsc):m_events(bmsc),m_event_top(bmsc)
{
- MessageEventPVector::iterator it;
- MessageEventPVector::iterator it_b;
+ EventPVector::iterator it;
+ EventPVector::iterator it_b;
for (it=m_events.begin();it!=m_events.end();it++)
{
bool is_minimal = true;
@@ -385,7 +378,7 @@
* Go through the vector of all events using AllReachableEventPVector
* and using EventTopologyHandler choose maximal events
*/
-class MaximalEventPList: public std::list<MessageEventP>
+class MaximalEventPList: public std::list<EventP>
{
private:
AllReachableEventPVector m_events;
@@ -394,8 +387,8 @@
public:
MaximalEventPList(BMscPtr bmsc):m_events(bmsc),m_event_top(bmsc)
{
- MessageEventPVector::iterator it;
- MessageEventPVector::iterator it_b;
+ EventPVector::iterator it;
+ EventPVector::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-09-26 12:48:24 UTC (rev 1863)
+++ trunk/src/check/pseudocode/visual_closure_initiator.cpp 2013-10-11 09:27:00 UTC (rev 1864)
@@ -39,8 +39,8 @@
return; // nothing to do, there is no non-empty predecessor area
}
- MessageEventPList max_events = pred_area->get_maximal_events();
- for (MessageEventPList::const_iterator it = max_events.begin(); it != max_events.end(); ++it)
+ EventPList max_events = pred_area->get_maximal_events();
+ for (EventPList::const_iterator it = max_events.begin(); it != max_events.end(); ++it)
make_closure(closure_matrix, succ_index, get_topology_index(*it));
}
@@ -51,7 +51,7 @@
void VisualClosureInitiator::cleanup_attributes()
{
- MessageEventPList::iterator e;
+ EventPList::iterator e;
for(e=m_modified_events.begin();e!=m_modified_events.end();e++)
{
(*e)->remove_attribute<size_t>(m_topology_index_attribute);
@@ -60,14 +60,14 @@
m_modified_events.erase(m_modified_events.begin(),m_modified_events.end());
}
-void VisualClosureInitiator::initialize(const MessageEventPVector& event_topology)
+void VisualClosureInitiator::initialize(const EventPVector& 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++)
{
- MessageEvent* event = event_topology[i];
+ Event* event = event_topology[i];
BoolVector& event_closure = get_visual_closure(event);
event_closure.resize(event_topology.size(),false);
set_topology_index(event,i);
@@ -75,25 +75,28 @@
m_modified_events.push_back(event);
}
//compute visual closures of events' ordering
- make_closure(closure,event_topology);
+ make_closure(closure, event_topology);
}
-void VisualClosureInitiator::make_closure(std::vector<BoolVector*>& closure, const MessageEventPVector& event_topology)
+void VisualClosureInitiator::make_closure(std::vector<BoolVector*>& closure_matrix, const EventPVector& event_topology)
{
for(size_t e=0; e<event_topology.size(); e++)
{
- (*closure[e])[e] = true;
- MessageEvent* event_e = event_topology[e];
+ (*closure_matrix[e])[e] = true;
+ Event* event_e = event_topology[e];
+
//send event is predecessor
- if(event_e->is_receive() && event_e->is_matched())
+ MessageEvent* msg_event_e = dynamic_cast<MessageEvent*>(event_e);
+ if(msg_event_e != NULL && msg_event_e->is_receive() && msg_event_e->is_matched())
{
- make_closure(closure,e,get_topology_index(event_e->get_matching_event()));
+ make_closure(closure_matrix,e,get_topology_index(msg_event_e->get_matching_event()));
}
- make_closure(closure,e,event_e);
+
+ make_closure(closure_matrix,e,event_e);
}
}
-void VisualClosureInitiator::make_closure(std::vector<BoolVector*>& closure, size_t e, MessageEvent* event_e)
+void VisualClosureInitiator::make_closure(std::vector<BoolVector*>& closure, size_t e, Event* event_e)
{
if (event_e->is_minimal())
{
@@ -102,18 +105,18 @@
}
else
{
- MessageEventPSet preds = event_e->get_predecessor_events();
- for (MessageEventPSet::const_iterator it = preds.begin(); it != preds.end(); ++it)
+ EventPSet preds = event_e->get_predecessor_events();
+ for (EventPSet::const_iterator it = preds.begin(); it != preds.end(); ++it)
make_closure(closure, e, get_topology_index(*it));
}
}
-size_t VisualClosureInitiator::get_topology_index(MessageEvent* e)
+size_t VisualClosureInitiator::get_topology_index(Event* e)
{
return e->get_attribute<size_t>(m_topology_index_attribute,0);
}
-void VisualClosureInitiator::set_topology_index(MessageEvent* e,size_t i)
+void VisualClosureInitiator::set_topology_index(Event* 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-09-26 12:48:24 UTC (rev 1863)
+++ trunk/src/check/pseudocode/visual_closure_initiator.h 2013-10-11 09:27:00 UTC (rev 1864)
@@ -37,16 +37,16 @@
protected:
- MessageEventPList m_topology;
+ EventPList m_topology;
public:
- const MessageEventPList& get_topology()
+ const EventPList& get_topology()
{
return m_topology;
}
- virtual void on_event_finished(MessageEvent* event)
+ virtual void on_event_finished(Event* event)
{
m_topology.push_front(event);
}
@@ -61,7 +61,7 @@
/**
* Events with modified attributes
*/
- MessageEventPList m_modified_events;
+ EventPList m_modified_events;
/**
* Name of topology attribute.
@@ -86,12 +86,12 @@
/**
* Completes closure_matrix for topologicaly sorted event - event_topology
*/
- void make_closure(std::vector<BoolVector*>& closure_matrix, const MessageEventPVector& event_topology);
+ void make_closure(std::vector<BoolVector*>& closure_matrix, const EventPVector& event_topology);
/**
* Completes closure_matrix for event_e with index e
*/
- void make_closure(std::vector<BoolVector*>& closure_matrix, size_t e, MessageEvent* event_e);
+ void make_closure(std::vector<BoolVector*>& closure_matrix, size_t e, Event* event_e);
public:
@@ -118,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 MessageEventPVector& event_topology);
+ void initialize(const EventPVector& event_topology);
/**
* Getter of visual closure attribute of e.
*/
- BoolVector& get_visual_closure(MessageEvent* e)
+ BoolVector& get_visual_closure(Event* e)
{
static BoolVector empty(1,false);
return e->get_attribute<BoolVector>(m_visual_closure_attribute,empty);
@@ -132,12 +132,12 @@
/**
* Getter of topology index attribute of e.
*/
- size_t get_topology_index(MessageEvent* e);
+ size_t get_topology_index(Event* e);
/**
* Setter of topology index attribute of e.
*/
- void set_topology_index(MessageEvent* e,size_t i);
+ void set_topology_index(Event* e,size_t i);
/**
* Cleans up set attributes.
Modified: trunk/src/check/race/footprint.cpp
===================================================================
--- trunk/src/check/race/footprint.cpp 2013-09-26 12:48:24 UTC (rev 1863)
+++ trunk/src/check/race/footprint.cpp 2013-10-11 09:27:00 UTC (rev 1864)
@@ -28,7 +28,7 @@
return a->operator <(*b.get());
}
-EventDependentInstances::EventDependentInstances(MessageEvent* event,size_t instances_count)
+EventDependentInstances::EventDependentInstances(Event* event,size_t instances_count)
{
m_event = event;
m_instances = BoolVector(instances_count,false);
@@ -63,7 +63,7 @@
return m_instances;
}
-MessageEvent* EventDependentInstances::get_event()
+Event* EventDependentInstances::get_event()
{
return m_event;
}
Modified: trunk/src/check/race/footprint.h
===================================================================
--- trunk/src/check/race/footprint.h 2013-09-26 12:48:24 UTC (rev 1863)
+++ trunk/src/check/race/footprint.h 2013-10-11 09:27:00 UTC (rev 1864)
@@ -54,7 +54,7 @@
/**
* Represents dependent Instances -- contain lesser/greater (depends on chosen semantic)
- * MessageEvent then the MessageEvent with specified m_event in this class.
+ * Event then the Event with specified m_event in this class.
*/
class EventDependentInstances
{
@@ -62,14 +62,14 @@
private:
/**
- * This instance of DependetInstances represents dependet instances of an MessageEvent
+ * This instance of DependetInstances represents dependent instances of an Event
* of this attribute
*/
- MessageEvent* m_event;
+ Event* m_event;
/**
* Each Instance i must have its own number. For this vector m_instances holds:
- * m_instances[i]==true iff i contains any greater/lesser MessageEvent than the MessageEvent
+ * m_instances[i]==true iff i contains any greater/lesser Event than the Event
* m_event.
*/
BoolVector m_instances;
@@ -79,7 +79,7 @@
/**
*
*/
- EventDependentInstances(MessageEvent* event,size_t instances_count);
+ EventDependentInstances(Event* event,size_t instances_count);
/**
* Used in std::set as comparision method
@@ -97,7 +97,7 @@
const BoolVector& get_instances();
- MessageEvent* get_event();
+ Event* get_event();
};
@@ -107,7 +107,7 @@
protected:
/**
- * Holds greater/lesser Instances of Events accessible under id of MessageEvent's
+ * Holds greater/lesser Instances of Events accessible under id of Event's
* Instance.
*/
EDInstancesPtrSetVector m_events_instances;
Modified: trunk/src/check/race/race_checker.cpp
===================================================================
--- trunk/src/check/race/race_checker.cpp 2013-09-26 12:48:24 UTC (rev 1863)
+++ trunk/src/check/race/race_checker.cpp 2013-10-11 09:27:00 UTC (rev 1864)
@@ -47,7 +47,7 @@
bmsc->add_instance(i);
StrictOrderAreaPtr a(new StrictOrderArea());
i->add_area(a);
- MessageEventPtr e = a->add_event();
+ MessageEventPtr e = a->add_event(new MessageEvent());
IncompleteMessagePtr m(new IncompleteMessage(LOST));
m->glue_event(e);
}
@@ -72,15 +72,15 @@
BMscPtr b = node->get_bmsc();
const InstancePtrList& instances = b->get_instances();
//compute minimal Events of Instances
- MessageEventPList minimal_events;
+ EventPList minimal_events;
InstancePtrList::const_iterator i;
for(i=instances.begin();i!=instances.end();i++)
{
- MessageEventPListPtr events = DFSInstanceEventsTraverser::topology_order((*i).get());
- MessageEventPList::const_iterator e1;
+ EventPListPtr events = DFSInstanceEventsTraverser::topology_order(i->get());
+ EventPList::const_iterator e1;
for(e1 = events->begin();e1!=events->end();e1++)
{
- MessageEventPList::const_iterator e2;
+ EventPList::const_iterator e2;
for(e2 = events->begin();e2!=events->end();e2++)
{
if(e1!=e2)
@@ -91,27 +91,26 @@
if(e2_causal[e1_index]) break;
}
}
- //'while loop' hasn't found any MessageEvent e2 to be less than e1
+ //'while loop' hasn't found any Event e2 to be less than e1
if(e2==events->end())
minimal_events.push_back(*e1);
}
}
/*
- For each MessageEvent e1 from minimal_events find Instances containing less Events
- than MessageEvent e1 in minimal_events.
- Note that if there exists any MessageEvent e2<e1 at Instance i, e2 must be grater
- or equal to some MessageEvent e3 in minimal_events, therefore we will use only
+ For each Event e1 from minimal_events find Instances containing less Events
+ than Event e1 in minimal_events.
+ Note that if there exists any Event e2<e1 at Instance i, e2 must be grater
+ or equal to some Event e3 in minimal_events, therefore we will use only
minimal_events to seek.
*/
- MessageEventPList::const_iterator e;
+ EventPList::const_iterator e;
ExtremeEvents& extreme_events = get_events(b.get());
m_modified_bmscs.push_back(b.get());
for(e=minimal_events.begin();e!=minimal_events.end();e++)
{
- EDInstancesPtr e_instances(
- new EventDependentInstances(*e,m_instance_marker->get_count()));
+ EDInstancesPtr e_instances(new EventDependentInstances(*e,m_instance_marker->get_count()));
size_t e_index = m_vis_initiator->get_topology_index(*e);
- MessageEventPList::const_iterator f;
+ EventPList::const_iterator f;
for(f=minimal_events.begin();f!=minimal_events.end();f++)
{
//if f is less than e (not equal) then Instance of f must be inserted
@@ -156,16 +155,16 @@
BMscPtr b = node->get_bmsc();
const InstancePtrList& instances = b->get_instances();
//compute maximal Events of Instances
- MessageEventPList maximal_events;
+ EventPList maximal_events;
InstancePtrList::const_iterator i;
for(i=instances.begin();i!=instances.end();i++)
{
- MessageEventPListPtr events = DFSInstanceEventsTraverser::topology_order((*i).get());
- MessageEventPList::const_iterator e1 = events->begin();
+ EventPListPtr events = DFSInstanceEventsTraverser::topology_order((*i).get());
+ EventPList::const_iterator e1 = events->begin();
while(e1!=events->end())
{
BoolVector& e1_causal = m_caus_initiator->get_causal_closure(*e1);
- MessageEventPList::const_iterator e2 = events->begin();
+ EventPList::const_iterator e2 = events->begin();
while(e2!=events->end())
{
//we are looking only for different events to be greater
@@ -177,30 +176,28 @@
}
e2++;
}
- //'while loop' hasn't found any MessageEvent e2 to be greater than e1
+ //'while loop' hasn't found any Event e2 to be greater than e1
if(e2==events->end())
maximal_events.push_back(*e1);
e1++;
}
}
/*
- * For any MessageEvent e1 from maximal_events find Instances containing any MessageEvent e2
- * such that e2<<e1 and instances containing any MessageEvent e3 such that e1<<e3.
+ * For any Event e1 from maximal_events find Instances containing any Event e2
+ * such that e2<<e1 and instances containing any Event e3 such that e1<<e3.
*/
- MessageEventPList::const_iterator e;
+ EventPList::const_iterator e;
ExtremeEvents& extreme_events_greater = get_events_greater(b.get());
ExtremeEvents& extreme_events_less = get_events_less(b.get());
m_modified_bmscs.push_back(b.get());
- MessageEventPListPtr events = DFSEventsTraverser::topology_order(b);
+ EventPListPtr events = DFSEventsTraverser::topology_order(b);
for(e=maximal_events.begin();e!=maximal_events.end();e++)
{
- EDInstancesPtr e_instances_greater(
- new EventDependentInstances(*e,m_instance_marker->get_count()));
- EDInstancesPtr e_instances_less(
- new EventDependentInstances(*e,m_instance_marker->get_count()));
+ EDInstancesPtr e_instances_greater(new EventDependentInstances(*e,m_instance_marker->get_count()));
+ EDInstancesPtr e_instances_less(new EventDependentInstances(*e,m_instance_marker->get_count()));
size_t e_index = m_vis_initiator->get_topology_index(*e);
const BoolVector& e_closure = m_caus_initiator->get_causal_closure(*e);
- MessageEventPList::const_iterator f;
+ EventPList::const_iterator f;
/*
Note that in the article only Events from MinP (used D \in MinP notation in
the article) are supposed to be checked. Nothing changes if we check all
@@ -270,26 +267,30 @@
return result;
}
-BMscPtr RaceChecker::create_counter_example(MessageEvent* e1, MessageEvent* e2)
+BMscPtr RaceChecker::create_counter_example(Event* e1, Event* e2)
{
BMscDuplicator duplicator;
BMscPtr original = e1->get_instance()->get_bmsc();
+
+ // NOTE: race should only occur with message events; just for sure...
+ MessageEvent* me1 = dynamic_cast<MessageEvent*>(e1);
+ MessageEvent* me2 = dynamic_cast<MessageEvent*>(e2);
e1->set_marked();
e2->set_marked();
- e1->get_message().get()->set_marked();
- e2->get_message().get()->set_marked();
+ if (me1 != NULL) me1->get_message().get()->set_marked();
+ if (me2 != NULL) me2->get_message().get()->set_marked();
BMscPtr copy = duplicator.duplicate_bmsc(original);
e1->set_marked(NONE);
e2->set_marked(NONE);
- e1->get_message().get()->set_marked(NONE);
- e2->get_message().get()->set_marked(NONE);
+ if (me1 != NULL) me1->get_message().get()->set_marked(NONE);
+ if (me2 != NULL) me2->get_message().get()->set_marked(NONE);
return copy;
}
-bool RaceChecker::check_events(MessageEvent* e1, MessageEvent* e2)
+bool RaceChecker::check_events(Event* e1, Event* e2)
{
//e1<e2 or they are unordered because of topology order with respect to <
BoolVector& e1_visual_order = m_visual_initiator.get_visual_closure(e1);
@@ -305,11 +306,8 @@
std::list<BMscPtr> RaceChecker::check_bmsc(BMscPtr bmsc, ChannelMapperPtr mapper)
{
- MessageEventPListPtr t = DFSEventsTraverser::topology_order(bmsc);
- MessageEventPVector topology(
- t->begin(),
- t->end()
- );
+ EventPListPtr t = DFSEventsTraverser::topology_order(bmsc);
+ EventPVector topology(t->begin(), t->end());
m_visual_initiator.initialize(topology);
m_causal_initiator.initialize(topology,m_visual_initiator,mapper);
std::list<BMscPtr> result;
@@ -610,15 +608,18 @@
EDInstancesPtrSet::const_iterator b;
for(b=bmsc_edi[i].begin();b!=bmsc_edi[i].end();b++)
{
- MessageEvent* b_event = (*b)->get_event();
- if(b_event->is_receive())
+ MessageEvent* b_event = dynamic_cast<MessageEvent*>((*b)->get_event());
+ if(b_event != NULL && b_event->is_receive())
{
const BoolVector& b_instances = (*b)->get_instances();
const EDInstancesPtrSetVector& fooprint_edi = m_footprint->get_events_instances();
EDInstancesPtrSet::const_iterator a;
for(a=fooprint_edi[i].begin();a!=fooprint_edi[i].end();a++)
{
- MessageEvent* a_event = (*a)->get_event();
+ MessageEvent* a_event = dynamic_cast<MessageEvent*>((*a)->get_event());
+ if (a_event == NULL)
+ continue;
+
if(a_event->is_receive() && !m_mapper->same_channel(a_event,b_event))
{
m_counterexamples.push_back(RaceInHMscException(f,b_event,a_event,get_reached_elements().back()));
Modified: trunk/src/check/race/race_checker.h
===================================================================
--- trunk/src/check/race/race_checker.h 2013-09-26 12:48:24 UTC (rev 1863)
+++ trunk/src/check/race/race_checker.h 2013-10-11 09:27:00 UTC (rev 1864)
@@ -89,7 +89,7 @@
* becomes members of new Footprint f2.
*
* When computing new Footprint it is neccessary to find relation between Events
- * in f1 and Events in MaxP of b in case there is some MessageEvent from f1 which belongs
+ * in f1 and Events in MaxP of b in case there is some Event from f1 which belongs
* to new f2 too. This listener prepares structure for this purpose too.
*
* Details are described in Lemma 15 of the article.
@@ -246,7 +246,7 @@
/**
* It was found that e1<e2 but not e1<<e2
*/
- BMscPtr create_counter_example(MessageEvent* e1, MessageEvent* e2);
+ BMscPtr create_counter_example(Event* e1, Event* e2);
/**
*
@@ -303,7 +303,7 @@
return true;
}
- bool check_events(MessageEvent* e1, MessageEvent* e2);
+ bool check_events(Event* e1, Event* e2);
};
class RaceInBMscException:public std::exception
Modified: trunk/src/check/time/constraint_syntax.cpp
===================================================================
--- trunk/src/check/time/constraint_syntax.cpp 2013-09-26 12:48:24 UTC (rev 1863)
+++ trunk/src/check/time/constraint_syntax.cpp 2013-10-11 09:27:00 UTC (rev 1864)
@@ -360,8 +360,8 @@
std::set<TimeRelationEventPtr>::iterator rel;
for(rel=time_relations.begin();rel!=time_relations.end();rel++)
{
- MessageEvent* a = (*rel)->get_event_a();
- MessageEvent* b = (*rel)->get_event_b();
+ Event* a = (*rel)->get_event_a();
+ Event* b = (*rel)->get_event_b();
if(!events_top.visual_is_leq(a,b)&&!events_top.visual_is_leq(b,a))
m_broken_rel.push(*rel);
}
Modified: trunk/src/check/time/hmsc_all_paths.cpp
===================================================================
--- trunk/src/check/time/hmsc_all_paths.cpp 2013-09-26 12:48:24 UTC (rev 1863)
+++ trunk/src/check/time/hmsc_all_paths.cpp 2013-10-11 09:27:00 UTC (rev 1864)
@@ -1,4 +1,5 @@
#include "hmsc_all_paths.h"
+#include <vector>
void AllPaths::traverse()
{
@@ -14,10 +15,9 @@
}
-void AllPaths::all_paths(
-HMscNodePtr node,
-MscElementPList path_prefix2
-)
+//#define MYDBG
+
+void AllPaths::all_paths(HMscNodePtr node, MscElementPList path_prefix2, SystemState system_state)
{
HMscNodePtrSet::iterator last_it;
std::list<PathFoundListener*>::iterator listener_it;
@@ -46,7 +46,7 @@
}
}
- set_number(node,get_number(node)+1); //increment occurence counter of node
+ set_number(node, get_number(node, system_state)+1, system_state); //increment occurence counter of node
//check whether node has successors
PredecessorNode * pre;
@@ -58,10 +58,44 @@
//keep poping until reference node is reached
while(!dynamic_cast<HMscNode*>(path_prefix2.back()))
path_prefix2.pop_back();
- set_number(node, 0);
+ set_number(node, 0, system_state);
return;
}
+ // update the system state
+ // ...from condition nodes
+ ConditionNodePtr cond = boost::dynamic_pointer_cast<ConditionNode>(node);
+ if (cond != NULL)
+ {
+ const std::vector<std::string> names = cond->get_names();
+ switch (cond->get_type())
+ {
+ case ConditionNode::SETTING:
+ for (std::vector<std::string>::const_iterator i = names.begin(); i != names.end(); ++i)
+ system_state.insert(*i);
+ break;
+ case ConditionNode::UNSETTING:
+ for (std::vector<std::string>::const_iterator i = names.begin(); i != names.end(); ++i)
+ system_state.erase(*i);
+ break;
+ default:
+ ; // other condition types have no effect on the system state
+ }
+ }
+ // ... and reference nodes
+ ReferenceNodePtr ref = boost::dynamic_pointer_cast<ReferenceNode>(node);
+ if (ref != NULL)
+ {
+ BMscPtr bmsc = ref->get_bmsc();
+ if (bmsc != NULL)
+ {
+ std::pair<SystemState, SystemState> cond_effect = bmsc->get_condition_effect();
+ for (SystemState::const_iterator i = cond_effect.first.begin(); i != cond_effect.first.end(); ++i)
+ system_state.insert(*i);
+ for (SystemState::const_iterator i = cond_effect.second.begin(); i != cond_effect.second.end(); ++i)
+ system_state.erase(*i);
+ }
+ }
//traverse all successors which do not occur in path_prefix more than m_occurence
NodeRelationPtrVector set_succ = pre->get_successors();
@@ -69,15 +103,31 @@
for(rel=set_succ.begin(); rel!=set_succ.end();rel++)
{
const NodeRelationPtr& node_relation = *rel;
- HMscNodePtr new_node(dynamic_cast<HMscNode*>(node_relation.get()->get_successor()));
- if(get_number(new_node)<m_occurence)
+ HMscNodePtr new_node(dynamic_cast<HMscNode*>(node_relation->get_successor()));
+ if(get_number(new_node, system_state)<m_occurence)
{
-
- path_prefix2.push_back(node_relation.get()); //update attribute
- all_paths(new_node,path_prefix2);
-
+ // check for an unsatisfied guard
+ ConditionNodePtr new_cond_node = boost::dynamic_pointer_cast<ConditionNode>(new_node);
+ if (new_cond_node != NULL)
+ {
+ if (new_cond_node->get_type() == ConditionNode::GUARDING)
+ {
+ bool satisfied = false;
+ const std::vector<std::string> names = new_cond_node->get_names();
+ for (std::vector<std::string>::const_iterator i = names.begin(); i != names.end(); ++i)
+ if (system_state.find(*i) != system_state.end())
+ {
+ satisfied = true;
+ break;
+ }
+ if (!satisfied)
+ continue;
+ }
+ }
+
+ path_prefix2.push_back(node_relation.get()); //update attribute
+ all_paths(new_node,path_prefix2, system_state);
}
-
}
//all successors have been traversed-> update attributes and finish.
@@ -85,6 +135,6 @@
//keep poping until reference node is reached
while(!dynamic_cast<HMscNode*>(path_prefix2.back()))
path_prefix2.pop_back();
- set_number(node, get_number(node)-1);
+ set_number(node, get_number(node, system_state)-1, system_state);
...
[truncated message content] |
