Menu
▾
▴
[Scstudio-commits] SF.net SVN: scstudio:[1826] branches/conditions
|
From: <ob...@us...> - 2013-05-27 04:00:34
|
Revision: 1826
http://sourceforge.net/p/scstudio/code/1826
Author: obouda
Date: 2013-05-27 04:00:30 +0000 (Mon, 27 May 2013)
Log Message:
-----------
computing condition effect
Modified Paths:
--------------
branches/conditions/src/check/time/hmsc_all_paths.cpp
branches/conditions/src/data/msc/BMsc.cpp
branches/conditions/src/data/msc/BMsc.h
branches/conditions/src/data/msc/Condition.cpp
branches/conditions/src/data/msc/Condition.h
branches/conditions/tests/time/time_race/CMakeLists.txt
branches/conditions/tests/time/time_race/race_cond_pos3.mpr
Added Paths:
-----------
branches/conditions/tests/time/time_race/race_cond_neg2.mpr
branches/conditions/tests/time/time_race/race_cond_neg2.mpr.result
branches/conditions/tests/time/time_race/race_cond_neg2.vsd
Modified: branches/conditions/src/check/time/hmsc_all_paths.cpp
===================================================================
--- branches/conditions/src/check/time/hmsc_all_paths.cpp 2013-05-27 02:25:44 UTC (rev 1825)
+++ branches/conditions/src/check/time/hmsc_all_paths.cpp 2013-05-27 04:00:30 UTC (rev 1826)
@@ -63,6 +63,7 @@
}
// update the system state
+ // ...from condition nodes
ConditionNodePtr cond = boost::dynamic_pointer_cast<ConditionNode>(node);
if (cond != NULL)
{
@@ -81,6 +82,20 @@
; // 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();
Modified: branches/conditions/src/data/msc/BMsc.cpp
===================================================================
--- branches/conditions/src/data/msc/BMsc.cpp 2013-05-27 02:25:44 UTC (rev 1825)
+++ branches/conditions/src/data/msc/BMsc.cpp 2013-05-27 04:00:30 UTC (rev 1826)
@@ -17,6 +17,7 @@
*/
#include "data/msc.h"
+#include "data/dfs_events_traverser.h"
void BMsc::add_instance(InstancePtr& i)
{
@@ -35,3 +36,36 @@
else it++;
}
+std::pair<SystemState, SystemState> BMsc::get_condition_effect()
+{
+ struct ConditionEffectListener : WhiteEventFoundListener
+ {
+ SystemState set_vars;
+ SystemState unset_vars;
+ void on_white_event_found(Event* e)
+ {
+ ConditionEvent* ce = dynamic_cast<ConditionEvent*>(e);
+ if (ce != NULL && ce->get_condition() != NULL)
+ {
+ ConditionPtr cond = ce->get_condition();
+ std::pair<SystemState, SystemState> effect = cond->get_condition_effect();
+ for (SystemState::const_iterator i = effect.first.begin(); i != effect.first.end(); ++i)
+ {
+ set_vars.insert(*i);
+ unset_vars.erase(*i);
+ }
+ for (SystemState::const_iterator i = effect.second.begin(); i != effect.second.end(); ++i)
+ {
+ unset_vars.insert(*i);
+ set_vars.erase(*i);
+ }
+ }
+ }
+ };
+
+ DFSEventsTraverser traverser;
+ ConditionEffectListener cel;
+ traverser.add_white_event_found_listener(&cel);
+ traverser.traverse(BMscPtr(this));
+ return make_pair(cel.set_vars, cel.unset_vars);
+}
Modified: branches/conditions/src/data/msc/BMsc.h
===================================================================
--- branches/conditions/src/data/msc/BMsc.h 2013-05-27 02:25:44 UTC (rev 1825)
+++ branches/conditions/src/data/msc/BMsc.h 2013-05-27 04:00:30 UTC (rev 1826)
@@ -19,6 +19,8 @@
#ifndef _BMSC_H
#define _BMSC_H
+#include <utility>
+
/**
* \brief Represents Basic MSC.
*/
@@ -63,6 +65,13 @@
* Removes all the instances with a specified name.
*/
void remove_instances(const std::wstring &label);
+
+ /**
+ * Computes the condition effect of this BMSC.
+ * In the first element of the pair, a set of condition variable names which get set by this BMSC is returned.
+ * In the second element of the pair, a set of condition variable names which get unset by this BMSC is returned.
+ */
+ std::pair<SystemState, SystemState> get_condition_effect();
};
#endif // #ifndef _BMSC_H
Modified: branches/conditions/src/data/msc/Condition.cpp
===================================================================
--- branches/conditions/src/data/msc/Condition.cpp 2013-05-27 02:25:44 UTC (rev 1825)
+++ branches/conditions/src/data/msc/Condition.cpp 2013-05-27 04:00:30 UTC (rev 1826)
@@ -32,3 +32,31 @@
m_event = event;
}
}
+
+std::pair<SystemState, SystemState> Condition::get_condition_effect() const
+{
+ SystemState set_vars;
+ SystemState unset_vars;
+
+ // a tiny hack; both Condition and ConditionNode should use a common code, in a way different from this one...
+ ConditionNode node;
+ std::string lbl;
+ for (std::wstring::const_iterator i = m_text.begin(); i != m_text.end(); ++i)
+ lbl += (char)*i;
+ node.assign_label(lbl);
+ switch (node.get_type())
+ {
+ case ConditionNode::SETTING:
+ for (std::vector<std::string>::const_iterator i = node.get_names().begin(); i != node.get_names().end(); ++i)
+ set_vars.insert(*i);
+ break;
+ case ConditionNode::UNSETTING:
+ for (std::vector<std::string>::const_iterator i = node.get_names().begin(); i != node.get_names().end(); ++i)
+ unset_vars.insert(*i);
+ break;
+ default:
+ ; // other condition types have no effect on the system state
+ }
+
+ return make_pair(set_vars, unset_vars);
+}
Modified: branches/conditions/src/data/msc/Condition.h
===================================================================
--- branches/conditions/src/data/msc/Condition.h 2013-05-27 02:25:44 UTC (rev 1825)
+++ branches/conditions/src/data/msc/Condition.h 2013-05-27 04:00:30 UTC (rev 1826)
@@ -19,6 +19,8 @@
#ifndef _CONDITION_H
#define _CONDITION_H
+#include <utility>
+
/**
* \brief Condition on an instance in Basic MSC.
* TODO: support multiple instances bound to a single condition
@@ -56,6 +58,13 @@
{
return m_text;
}
+
+ /**
+ * Computes the condition effect of this condition.
+ * In the first element of the pair, a set of condition variable names which get set by this condition is returned.
+ * In the second element of the pair, a set of condition variable names which get unset by this condition is returned.
+ */
+ std::pair<SystemState, SystemState> get_condition_effect() const;
void glue_event(ConditionEvent* event);
Modified: branches/conditions/tests/time/time_race/CMakeLists.txt
===================================================================
--- branches/conditions/tests/time/time_race/CMakeLists.txt 2013-05-27 02:25:44 UTC (rev 1825)
+++ branches/conditions/tests/time/time_race/CMakeLists.txt 2013-05-27 04:00:30 UTC (rev 1826)
@@ -43,3 +43,4 @@
ADD_CHECKER_TEST(sctime "Time Race" race_cond_pos3.mpr 1)
ADD_CHECKER_TEST(sctime "Time Race" race_cond_neg1.mpr 0)
+ADD_CHECKER_TEST(sctime "Time Race" race_cond_neg2.mpr 0)
Added: branches/conditions/tests/time/time_race/race_cond_neg2.mpr
===================================================================
--- branches/conditions/tests/time/time_race/race_cond_neg2.mpr (rev 0)
+++ branches/conditions/tests/time/time_race/race_cond_neg2.mpr 2013-05-27 04:00:30 UTC (rev 1826)
@@ -0,0 +1,38 @@
+mscdocument impl_example3b.vsd;
+msc Page_1;
+initial connect L0, L1;
+L0: reference A connect L2;
+L1: condition Y connect L2;
+L2: connect L3, L4;
+L3: final;
+L4: condition when X connect L5;
+L5: reference B connect L6;
+L6: final;
+endmsc;
+msc A;
+inst p;
+inst q;
+inst r;
+p: instance;
+out m,0 to q;
+condition X shared;
+endinstance;
+q: instance;
+in m,0 from p;
+endinstance;
+r: instance;
+endinstance;
+endmsc;
+msc B;
+inst p;
+inst q;
+inst r;
+p: instance;
+endinstance;
+q: instance;
+in m,0 from r;
+endinstance;
+r: instance;
+out m,0 to q;
+endinstance;
+endmsc;
Property changes on: branches/conditions/tests/time/time_race/race_cond_neg2.mpr
___________________________________________________________________
Added: svn:executable
## -0,0 +1 ##
+*
\ No newline at end of property
Added: branches/conditions/tests/time/time_race/race_cond_neg2.mpr.result
===================================================================
--- branches/conditions/tests/time/time_race/race_cond_neg2.mpr.result (rev 0)
+++ branches/conditions/tests/time/time_race/race_cond_neg2.mpr.result 2013-05-27 04:00:30 UTC (rev 1826)
@@ -0,0 +1,28 @@
+Time Race violated
+OK: race_cond_neg2 violated Time Race, should be violated
+mscdocument counter_example;
+msc Page_1;
+initial connect L0;
+/* MARKED */
+L0: reference _1_A connect L1;
+L1: connect L2;
+L2: final;
+endmsc;
+msc _1_A;
+inst p;
+inst q;
+inst r;
+p: instance;
+/* MARKED */
+/* MARKED */
+out m,0 to q;
+/* MARKED */
+condition X shared;
+endinstance;
+q: instance;
+/* MARKED */
+in m,0 from p;
+endinstance;
+r: instance;
+endinstance;
+endmsc;
Added: branches/conditions/tests/time/time_race/race_cond_neg2.vsd
===================================================================
(Binary files differ)
Index: branches/conditions/tests/time/time_race/race_cond_neg2.vsd
===================================================================
--- branches/conditions/tests/time/time_race/race_cond_neg2.vsd 2013-05-27 02:25:44 UTC (rev 1825)
+++ branches/conditions/tests/time/time_race/race_cond_neg2.vsd 2013-05-27 04:00:30 UTC (rev 1826)
Property changes on: branches/conditions/tests/time/time_race/race_cond_neg2.vsd
___________________________________________________________________
Added: svn:executable
## -0,0 +1 ##
+*
\ No newline at end of property
Added: svn:mime-type
## -0,0 +1 ##
+application/msword
\ No newline at end of property
Modified: branches/conditions/tests/time/time_race/race_cond_pos3.mpr
===================================================================
--- branches/conditions/tests/time/time_race/race_cond_pos3.mpr 2013-05-27 02:25:44 UTC (rev 1825)
+++ branches/conditions/tests/time/time_race/race_cond_pos3.mpr 2013-05-27 04:00:30 UTC (rev 1826)
@@ -1,4 +1,4 @@
-mscdocument impl_example4.vsd;
+mscdocument race_cond_pos3.vsd;
msc Page_1;
initial connect L0, L1;
L0: reference A connect L2;
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|