Menu
▾
▴
[Scstudio-commits] SF.net SVN: scstudio:[897] trunk
|
From: <ma...@us...> - 2010-09-08 23:01:57
|
Revision: 897
http://scstudio.svn.sourceforge.net/scstudio/?rev=897&view=rev
Author: madzin
Date: 2010-09-08 23:01:50 +0000 (Wed, 08 Sep 2010)
Log Message:
-----------
revert to non-refactoring version, repair bugs in time membership, add partial membership algorithm (not tested), add test for time membership
Modified Paths:
--------------
trunk/src/membership/CMakeLists.txt
trunk/src/membership/membership_alg.cpp
trunk/src/membership/membership_alg.h
trunk/tests/membership/CMakeLists.txt
trunk/tests/membership/membership_test.cpp
Added Paths:
-----------
trunk/tests/membership/test_bmsc29_1.mpr
trunk/tests/membership/test_bmsc29_2.mpr
trunk/tests/membership/test_bmsc30_1.mpr
trunk/tests/membership/test_bmsc30_2.mpr
trunk/tests/membership/test_bmsc31_1.mpr
trunk/tests/membership/test_hmsc29.mpr
trunk/tests/membership/test_hmsc30.mpr
trunk/tests/membership/test_hmsc31.mpr
Modified: trunk/src/membership/CMakeLists.txt
===================================================================
--- trunk/src/membership/CMakeLists.txt 2010-09-08 22:49:10 UTC (rev 896)
+++ trunk/src/membership/CMakeLists.txt 2010-09-08 23:01:50 UTC (rev 897)
@@ -3,10 +3,6 @@
module.cpp
membership_alg.cpp
membership_alg.h
- membership_time.cpp
- membership_time.h
- membership_additional.cpp
- membership_additional.h
)
TARGET_LINK_LIBRARIES(scmembership
Modified: trunk/src/membership/membership_alg.cpp
===================================================================
--- trunk/src/membership/membership_alg.cpp 2010-09-08 22:49:10 UTC (rev 896)
+++ trunk/src/membership/membership_alg.cpp 2010-09-08 23:01:50 UTC (rev 897)
@@ -2,10 +2,10 @@
//Attributy sa nemaju porovnavat jednoducho mame prefrcat celym koregionom a taktiez tym bmsc diagramom
+//TODO throw exception instead of Error: unexpected behaviour
-
/*
* scstudio - Sequence Chart Studio
* http://scstudio.sourceforge.net
@@ -23,13 +23,20 @@
*
*/
-//#include "membership/membership_alg.h"
-#include "membership/membership_time.h"
+#include "membership/membership_alg.h"
#include "check/time/time_pseudocode.h"
#include "check/time/tightening.h"
#include <limits>
#include <map>
+// map of bmsc names and configurations which were checked
+std::map<std::wstring, std::set<ConfigurationPtr> > checked;
+
+std::map<TimeRelationRefNodePtr, ConfigurationPtr> top_time_references;
+std::map<TimeRelationRefNodePtr, ConfigurationPtr> bottom_time_references;
+
+std::vector<Event*> attributed_events;
+
//save ordering of coregion events in appropriate coregion
std::map<CoregionAreaPtr, CoregionOrderingPtr> coregion_ordering;
//snapshots of context for each coregion
@@ -37,17 +44,52 @@
//checked possibilities of coregion ordering
std::map<CoregionAreaPtr, std::vector<CoregionOrderingPtr> > checked_orderings;
+//name of instances on which a user is focused on
+std::vector<std::wstring> focused_instances;
+
+//identification for receive events
+int max_id;
+
+BMscPtr global_bmsc;
+BMscIntervalSetMatrix* time_matrix;
+
InstancePtr find_instance(InstancePtrList instances, std::wstring name);
HMscPtr search_bmsc(BMscPtr bmsc, BMscPtr bmsc_f);
HMscPtr search_hmsc(HMscPtr hmsc, BMscPtr bmsc_f);
/*
+ * find name of the instance among fosuces instances
+ */
+bool contain_focused_instances(std::wstring instance)
+{
+ for(unsigned int i = 0; i < focused_instances.size(); i++)
+ {
+ if(focused_instances[i] == instance)
+ return true;
+ }
+
+ return false;
+}
+
+/*
* checks whole branch from defined node in HMSC
*/
bool check_branch(HMscNodePtr node, ConfigurationPtr b);
/*
+ * adds searched configuration to map of checked configurations
+ *
+ * configuration - state of node in searched HMSC and state of bMSC which is looked for
+ */
+void add_checked_branch(ReferenceNodePtr ref_node, ConfigurationPtr searched_conf);
+
+/*
+ * checks if instance contains any event
+ */
+bool is_empty_instance(InstancePtrList node_instances, InstancePtrList b_instances);
+
+/*
* compares strict order area from HMSC node with matching strict order area from bMSC which is looked for
*
* parameters: node_events - events of HMSC node cut
@@ -84,6 +126,21 @@
CoregionAreaPtr b_coregion, std::vector<Event*>& b_events);
/*
+ * compares two events
+ */
+bool compare_events(Event* a, Event* b);
+
+/*
+ * compares events attributes
+ */
+bool compare_events_attribute(Event* a, Event* b);
+
+/*
+ * tries to find configuration into map of seared configuration
+ */
+bool look_at_checked_conf(ReferenceNodePtr node, ConfigurationPtr b);
+
+/*
* compares one instance from HMSC node with matching instance from bMSC which is looked for
*
* parameters: node_instance - instance from HMSC node
@@ -103,6 +160,101 @@
bool check_node(ReferenceNodePtr node, enum check_type type, ConfigurationPtr old_conf);
/*
+ * in case events are send events, adds attribute to both events and to both receive event in case messages are complete
+ *
+ * parameters: node_e - event from HMSC node
+ * b_e - event from bMSC
+ */
+void set_identification(Event* node_e, Event* b_e);
+
+/*
+ * checks whether node has null pointer to reference bMSC
+ */
+bool is_node_null(ReferenceNodePtr node);
+
+/*
+ * checks whether instance contains any event
+ */
+bool is_instance_null(InstancePtr instance);
+
+/*
+ * checks whether coregion area contains any event
+ */
+bool is_cor_area_null(CoregionAreaPtr cor);
+
+/*
+ * checks whether strict order area contains any event
+ */
+bool is_strict_area_null(StrictOrderAreaPtr strict);
+
+/*
+ * checks time constraints in HMSC node
+ */
+//TODO skontrolovat co to vlastne robi, a kde kontrolujem casove obmedzenia v ramci bMSC z dajakeho HMSC nodu
+bool check_node_time(ReferenceNodePtr node, ConfigurationPtr conf);
+
+/*
+ * finds the maximum event of HMSC node and returns time interval value of matching event in bMSC
+ */
+Event* get_max_event(ReferenceNodePtr node, ConfigurationPtr conf);
+
+/*
+ * returns map where the key is instance name and the value is vector of the event identifications
+ * (in case of coregion area)
+ */
+std::map<std::wstring, std::vector<int> > get_node_last_events(ReferenceNodePtr node);
+
+/*
+ * finds the minimum event of HMSC node and returns time interval value of matching event in bMSC
+ */
+Event* get_min_event(ConfigurationPtr conf);
+
+/*
+ * compare absolut position, is the fist parameter before (more minimal) than the second
+ *
+ * return: 0 - it is not decideable
+ * 1 - the fist is before the second
+ * 2 - the second is before the first
+ */
+int compare_absolut_position(Event* first, Event* second);
+
+/*
+ * returns the last event on instance
+ */
+std::vector<Event*> get_last_instance_event(Event* start);
+
+/*
+ * returns maximal events of coregion area
+ */
+std::vector<Event*> get_last_coregion_events(CoregionArea* cor);
+
+/*
+ * compares events time relations
+ *
+ * paramterers: a - HMSC node
+ * b - bMSC node
+ */
+bool compare_events_time_relations(Event* a, Event* b);
+
+/*
+ * finds event in bMSC on instance by id
+ *
+ * parameters: label - label of instance where the event should be
+ * id - id of event which is looked for
+ */
+Event* find_event_on_instance_by_id(std::wstring label, int id, StrictEventPtr start_event = NULL);
+
+/*
+ * removes event attribute "indentification"
+ */
+void remove_events_attributes(std::vector<Event*> vec);
+
+/*
+ * return matrix of time intervals among each nodes
+ */
+BMscIntervalSetMatrix get_bmsc_matrix(BMscPtr bmsc_f);
+
+/*
* Returns precondition list of the membership algorithm
*/
Checker::PreconditionList MembershipAlg::get_preconditions(MscPtr msc) const
@@ -126,7 +278,7 @@
return NULL;
}
- set_global_bmsc(bmsc_f);
+ global_bmsc = bmsc_f;
if (hmsc != NULL)
return search_hmsc(hmsc, bmsc_f);
@@ -143,12 +295,19 @@
}
}
+MscPtr MembershipAlg::find(MscPtr msc, MscPtr bmsc, std::vector<std::wstring> instances)
+{
+ focused_instances.insert(focused_instances.begin(), instances.begin(), instances.end());
+
+ return this->find(msc, bmsc);
+}
+
/*
* Tries to find bMSC in HMSC
*/
HMscPtr search_hmsc(HMscPtr hmsc, BMscPtr bmsc_f)
{
- set_max_id(0);
+ max_id = 0;
BMscGraphDuplicator duplicator;
HMscPtr dup_hmsc;
@@ -180,7 +339,7 @@
//get time matrix
BMscIntervalSetMatrix time_matrix2 = get_bmsc_matrix(bmsc_f);
- set_time_matrix(&time_matrix2);
+ time_matrix = &time_matrix2;
//creates configuration of defined bMSC
ConfigurationPtr searched_conf = new Configuration(bmsc_f->get_instances());
@@ -209,8 +368,9 @@
bool check_branch(HMscNodePtr hmsc_node, ConfigurationPtr b)
{
//remove attributes from previous computation
- if(!get_attributed_events().empty()){
- remove_events_attributes();
+ if(!attributed_events.empty()){
+ remove_events_attributes(attributed_events);
+ attributed_events.clear();
}
//checks end node
@@ -218,7 +378,7 @@
if (end != NULL)
{
- if (b->is_null())
+ if (b->is_null(focused_instances))
return true;
else
return false;
@@ -252,7 +412,11 @@
else
{
//when deosn't exist empty path to EndNode
- if (b->is_null() && !is_node_null(node))
+// if (b->is_null() && !is_node_null(node))
+// return false;
+
+ //when deosn't exist empty path to EndNode
+ if (b->is_null(focused_instances) && !is_node_null(node))
return false;
//checks if this node with this configuration was checked
@@ -267,21 +431,24 @@
//tries to matching events between searched MSC and bMSC which is looked for
if (!check_node(node, membership, b))
{
- remove_events_attributes();
+ remove_events_attributes(attributed_events);
+ attributed_events.clear();
return false;
}
//checks time constraints for this node
if(!check_node_time(node, old_config_II))
{
- remove_events_attributes();
+ remove_events_attributes(attributed_events);
+ attributed_events.clear();
return false;
}
//checks the ordering of events (by attribute which was set at check_node(node, membership,b))
if (!check_node(node, receive_ordering, old_config_I))
{
- remove_events_attributes();
+ remove_events_attributes(attributed_events);
+ attributed_events.clear();
return false;
}
@@ -294,7 +461,8 @@
if(!b->compare(old_config_I))
return false;
- remove_events_attributes();
+ remove_events_attributes(attributed_events);
+ attributed_events.clear();
NodeRelationPtrVector successors = node->get_successors();
NodeRelationPtrVector::iterator it;
@@ -445,7 +613,6 @@
if(!node_events.empty())
node_e_a = node_events[0]->get_general_area();
else
- //may be there should be return true
return false;
CoregionAreaPtr cor = boost::dynamic_pointer_cast<CoregionArea> (node_e_a);
@@ -673,7 +840,9 @@
}
}
-//TODO it can cause segmentation fault .get()
+ if(b_e->get_successor() == NULL)
+ std::cerr << "Error: unexpected behaviour" << std::endl;
+
b_e = b_e->get_successor().get();
CoregEventRelPtrVector succ = node_e->get_successors();
@@ -823,6 +992,240 @@
}
/*
+ * Add checked branch to map of checked branches
+ */
+void add_checked_branch(ReferenceNodePtr ref_node, ConfigurationPtr conf)
+{
+ BMscPtr bmsc = ref_node->get_bmsc();
+
+ if(bmsc == NULL)
+ {
+ std::cerr << "Internal error: checked_branch" << std::endl;
+ return;
+ }
+
+ std::wstring bmsc_name = bmsc->get_label();
+ std::set<ConfigurationPtr> conf_set;
+ conf_set.insert(conf);
+
+ if(checked.find(bmsc_name) == checked.end())
+ checked.insert(std::make_pair(bmsc_name, conf_set));
+ else
+ checked.find(bmsc_name)->second.insert(conf);
+}
+
+/*
+ * Compare values in two events
+ */
+bool compare_events(Event* a, Event* b)
+{
+ if (b == NULL || a == NULL)
+ return false;
+
+ if (a->get_instance()->get_label() != b->get_instance()->get_label())
+ return false;
+
+ if (a->is_send() != b->is_send())
+ return false;
+
+ if ((a->get_complete_message() == NULL) != (b->get_complete_message() == NULL))
+ return false;
+
+ if (a->get_message()->get_label() != b->get_message()->get_label())
+ return false;
+
+ if (a->is_matched() != b->is_matched())
+ return false;
+
+ if (a->is_matched())
+ {
+ if (a->is_send())
+ {
+ if (a->get_receiver_label() != b->get_receiver_label())
+ return false;
+ }
+ else
+ {
+ if (a->get_sender_label() != b->get_sender_label())
+ return false;
+ }
+ }
+
+ return true;
+}
+
+//parameters node_e, b_e
+bool compare_events_attribute(Event* a, Event* b)
+{
+ IncompleteMessagePtr incom_a = boost::dynamic_pointer_cast<IncompleteMessage > (a->get_message());
+ IncompleteMessagePtr incom_b = boost::dynamic_pointer_cast<IncompleteMessage > (b->get_message());
+
+ switch ((incom_a != NULL) + (incom_b != NULL))
+ {
+ case 2:
+ return true;
+ break;
+
+ case 1:
+ return false;
+ break;
+
+ case 0:
+ break;
+
+ default:
+ return false;
+ }
+
+ int a_id, b_id;
+ bool a_set = true;
+
+ a_id = a->get_attribute("identification", -1, a_set);
+
+ bool b_set = true;
+
+ b_id = b->get_attribute("identification", -2, b_set);
+
+ if(focused_instances.empty() || contain_focused_instances(a->get_matching_event()->get_instance()->get_label()))
+ {
+ if (a_set || b_set || a_id != b_id)
+ return false;
+
+ return compare_events_time_relations(a,b);
+ }
+ else
+ return true;
+}
+
+bool compare_events_time_relations(Event* node_a, Event* bmsc_a)
+{
+ TimeRelationEventPtrList node_intervals = node_a->get_time_relations();
+ TimeRelationEventPtrList::iterator it;
+ int time_node_b_id;
+
+ for(it = node_intervals.begin(); it != node_intervals.end(); it++)
+ {
+ if((*it)->get_event_a() == node_a)
+ {
+ bool time_node_b_id_set = true;
+
+ time_node_b_id = (*it)->get_event_b()->get_attribute("identification", -1, time_node_b_id_set);
+
+ if(time_node_b_id_set)
+ {
+ std::cerr << "Error: Unexpected behaviour 3" << std::endl;
+ return false;
+ }
+
+ Event* bmsc_b = find_event_on_instance_by_id((*it)->get_event_b()->get_instance()->get_label(), time_node_b_id);
+
+ if(bmsc_b == NULL)
+ return false;
+
+ MscTimeIntervalSetD result, hmsc_inter, bmsc_inter;
+
+ hmsc_inter = (*it)->get_interval_set();
+ bmsc_inter = time_matrix->operator()(bmsc_a, bmsc_b);
+ result = MscTimeIntervalSetD::set_intersection(hmsc_inter, bmsc_inter);
+
+ if(result.is_empty())
+ return false;
+ else
+ if(result != bmsc_inter)
+ {
+std::cerr << "Warning: the HMSC interval do not cover whole bMSC interval" << std::endl;
+ return false;
+ }
+ }
+ }
+
+ return true;
+}
+
+Event* find_event_on_instance_by_id(std::wstring label, int id, StrictEventPtr start_event)
+{
+ EventAreaPtr first;
+
+ if(start_event == NULL)
+ {
+ InstancePtrList instances = global_bmsc->get_instances();
+ InstancePtrList::iterator it;
+ InstancePtr instance;
+
+ for(it = instances.begin(); it != instances.end(); it++)
+ {
+ if((*it)->get_label() == label)
+ {
+ instance = *it;
+ break;
+ }
+ }
+
+ first = instance->get_first();
+ }
+ else
+ {
+ first = start_event->get_general_area();
+ }
+
+ StrictOrderAreaPtr strict = boost::dynamic_pointer_cast<StrictOrderArea>(first);
+
+ StrictEventPtr str = strict->get_first();
+
+ //function finds event only in bMSC which is looked for, so coregion area is not allowed
+ if(str == NULL)
+ {
+ std::cerr << "Error: bMSC which is looked for contains coregion area" << std::endl;
+ return NULL;
+ }
+
+ int event_id;
+ bool event_set = true;
+
+ event_id = str->get_attribute("identification", -1, event_set);
+
+ if(event_set)
+ attributed_events.push_back(str.get());
+
+ StrictEventPtr old;
+
+ while(event_id != id)
+ {
+ old = str;
+ str = str->get_successor();
+
+ if(str == NULL)
+ {
+ EventAreaPtr area = old->get_general_area();
+ area = area->get_next();
+
+ strict = boost::dynamic_pointer_cast<StrictOrderArea>(area);
+
+ if(strict == NULL)
+ {
+ std::cerr << "Error: Node was not found" << std::endl;
+ return NULL;
+ }
+
+ str = strict->get_first();
+
+ if(str == NULL)
+ {
+ std::cerr << "Error: Node was not found" << std::endl;
+ return NULL;
+ }
+ }
+
+ event_id = str->get_attribute("identification", -1, event_set);
+
+ if(event_set)
+ attributed_events.push_back(str.get());
+ }
+
+ return str.get();
+}
+
+/*
* Tries finding bMSC in bMSC
*
* bmsc - where the bmsc_f is looking for
@@ -850,7 +1253,7 @@
else
{
std::cout << "Error: Unexpected behaviour 43" << std::endl;
- return false;
+ return NULL;
}
//creates end node
@@ -865,17 +1268,114 @@
else
{
std::cout << "Error: Unexpected behaviour 23" << std::endl;
- return false;
+ return NULL;
}
return search_hmsc(hmsc, bmsc_f);
}
/*
+ * Checks if the instance is empty
+ */
+bool is_empty_instance(InstancePtrList node_instances, InstancePtrList b_instances)
+{
+ InstancePtrList::iterator node_instence_it, b_instance_it;
+
+ bool in_bmsc_f;
+ EventAreaPtr event_area;
+
+ for (node_instence_it = node_instances.begin(); node_instence_it != node_instances.end(); node_instence_it++)
+ {
+ //in case the user is not focused on this instance the algorithm skip the checking of them
+ bool skip = false;
+
+ if(!focused_instances.empty())
+ {
+ skip = true;
+
+ for(unsigned int i = 0; i < focused_instances.size(); i++)
+ {
+ if(focused_instances[i] == (*node_instence_it)->get_label())
+ skip = false;
+ }
+ }
+
+ if(skip)
+ continue;
+
+ in_bmsc_f = false;
+
+ for (b_instance_it = b_instances.begin(); b_instance_it != b_instances.end(); b_instance_it++)
+ {
+ if ((*node_instence_it)->get_label() == (*b_instance_it)->get_label())
+ {
+ in_bmsc_f = true;
+ break;
+ }
+ }
+
+ if (!in_bmsc_f)
+ {
+ event_area = (*node_instence_it)->get_first();
+
+ if (event_area != NULL)
+ {
+ StrictOrderAreaPtr strict = boost::dynamic_pointer_cast<StrictOrderArea > (event_area);
+
+ if (strict == NULL)
+ {
+ CoregionAreaPtr coregion = boost::dynamic_pointer_cast<CoregionArea > (event_area);
+ if (coregion != NULL)
+ {
+ if (coregion->get_minimal_events().size() != 0)
+ return false;
+ }
+ }
+ else
+ {
+ if (strict->get_first() != NULL)
+ return false;
+ }
+ }
+ }
+ }
+
+ return true;
+}
+
+/*
+ * Checks if the node was checked with this configuration
+ */
+bool look_at_checked_conf(ReferenceNodePtr node, ConfigurationPtr b)
+{
+ std::map<std::wstring, std::set<ConfigurationPtr> >::iterator it_checked;
+ it_checked = checked.find(node->get_msc()->get_label());
+
+ if (it_checked != checked.end())
+ {
+ std::set<ConfigurationPtr>::iterator conf_it;
+
+ for (conf_it = it_checked->second.begin(); conf_it != it_checked->second.end();
+ conf_it++)
+ {
+ if (b->compare(*conf_it))
+ {
+ return false;
+ }
+ }
+ }
+
+ return true;
+}
+
+/*
* Checks instance
*/
bool check_instance(InstancePtr node_instance, enum check_type type, PositionPtr old_position)
{
+ if(!focused_instances.empty() && !contain_focused_instances(node_instance->get_label()))
+ return true;
+
std::vector<Event*> node_events, b_events;
EventAreaPtr node_area, b_area;
std::wstring name;
@@ -1058,7 +1558,7 @@
std::set<PositionPtr> positions = conf->get_positions();
std::set<PositionPtr>::iterator position_it;
- if (node_instances.size() > b_instances.size())
+ if (focused_instances.empty() && node_instances.size() > b_instances.size())
{
if (!is_empty_instance(node_instances, b_instances))
return false;
@@ -1098,3 +1598,635 @@
return true;
}
+void set_identification(Event* node_e, Event* b_e)
+{
+ if (node_e->is_send())
+ {
+ node_e->set_attribute("identification", max_id);
+ attributed_events.push_back(node_e);
+ b_e->set_attribute("identification", max_id++);
+ attributed_events.push_back(b_e);
+
+ CompleteMessagePtr node_message = node_e->get_complete_message();
+
+ if (node_message != NULL)
+ {
+ Event* event = node_message->get_receive_event();
+ event->set_attribute("identification", max_id);
+ attributed_events.push_back(event);
+ }
+
+ CompleteMessagePtr b_message = b_e->get_complete_message();
+
+ if (b_message != NULL)
+ {
+ Event* event = b_message->get_receive_event();
+ event->set_attribute("identification", max_id++);
+ attributed_events.push_back(event);
+ }
+
+ }
+}
+
+bool is_node_null(ReferenceNodePtr node)
+{
+ MscPtr msc = node->get_msc();
+
+ BMscPtr bmsc = boost::dynamic_pointer_cast<BMsc> (msc);
+
+ if(bmsc == NULL)
+ {
+ std::cerr << "Internal Error: typecast failed" << std::endl;
+ return false;
+ }
+
+ InstancePtrList instances = bmsc->get_instances();
+ InstancePtrList::iterator it;
+
+ for(it = instances.begin(); it != instances.end(); it++)
+ {
+ if(focused_instances.empty() || contain_focused_instances((*it)->get_label()))
+ {
+ if(!is_instance_null(*it))
+ return false;
+ }
+ }
+
+ return true;
+}
+
+bool is_instance_null(InstancePtr instance)
+{
+ EventAreaPtr area;
+ StrictOrderAreaPtr strict;
+ CoregionAreaPtr cor;
+
+ if(instance == NULL)
+ return true;
+
+ area = instance->get_first();
+
+ while(area != NULL)
+ {
+ strict = boost::dynamic_pointer_cast<StrictOrderArea>(area);
+
+ if(strict == NULL)
+ {
+ cor = boost::dynamic_pointer_cast<CoregionArea>(area);
+
+ if(cor != NULL)
+ if(!is_cor_area_null(cor))
+ return false;
+ }
+ else
+ if(!is_strict_area_null(strict))
+ return false;
+
+ area = area->get_next();
+ }
+
+ return true;
+}
+
+bool is_cor_area_null(CoregionAreaPtr cor)
+{
+ if(cor == NULL)
+ return true;
+
+ if(!cor->get_minimal_events().empty())
+ return false;
+
+ return true;
+}
+
+bool is_strict_area_null(StrictOrderAreaPtr strict)
+{
+ if(strict == NULL)
+ return true;
+
+ if(strict->get_first() != NULL)
+ return false;
+
+ return true;
+}
+
+bool check_node_time(ReferenceNodePtr node, ConfigurationPtr conf)
+{
+ TimeRelationRefNodePtrSet top = node->get_time_relations_top();
+ TimeRelationRefNodePtrSet bottom = node->get_time_relations_bottom();
+ TimeRelationRefNodePtrSet::iterator it;
+
+ std::vector<TimeRelationRefNodePtr> top_vec, bottom_vec, themself_vec;
+
+//top_time_references, bottom_time_references su tam ulozene uzly kde sa zacina casovy interval, a su usporiadane podla top/bottom. To znamena casovy interval na node_a je pripojeny na top/bottom.
+
+//top_vec, bottom_vec su tam ulozene intervaly kde je aktualny node pripojeny ako koniec intervalu, su usporiadane podla top/bottom.
+
+ for(it = top.begin(); it!=top.end(); it++)
+ {
+ if((*it)->get_ref_node_b() == node.get())
+ {
+ if((*it)->get_ref_node_b() == (*it)->get_ref_node_a())
+ themself_vec.push_back(*it);
+ else
+ top_vec.push_back(*it);
+ }
+ else
+ top_time_references.insert(std::make_pair(*it, conf));
+ }
+
+ for(it = bottom.begin(); it!=bottom.end(); it++)
+ {
+ if((*it)->get_ref_node_b() == node.get())
+ {
+ if((*it)->get_ref_node_b() != (*it)->get_ref_node_a())
+ bottom_vec.push_back(*it);
+ }
+ else
+ bottom_time_references.insert(std::make_pair(*it, conf));
+ }
+
+ //relation between the first and the second hmsc node
+ //min_a - top of the first hmsc node
+ //min_b - top of the second hmsc node
+ //max_a - bottom of the first hmsc node
+ //max_b - bottom of the second hmsc node
+ Event* max_a = NULL;
+ Event* max_b = NULL;
+ Event* min_a = NULL;
+ Event* min_b = NULL;
+
+ if(!themself_vec.empty())
+ {
+ if(themself_vec.size() > 1)
+ {
+ std::cerr << "Error: more time intervals between top and bottom of one reference node" << std::endl;
+ return false;
+ }
+
+ min_a = get_min_event(conf);
+ max_b = get_max_event(node, conf);
+
+ if(min_a == NULL || max_b == NULL)
+ {
+ std::cerr << "Error: unexpected behaviour" << std::endl;
+ return false;
+ }
+
+ TimeRelationRefNodePtr relation = themself_vec.front();
+
+ if(relation == NULL)
+ {
+ std::cout<<"Error: Unexpected program's behaviour"<<std::endl;
+ return false;
+ }
+
+ MscTimeIntervalSetD result, hmsc_inter, bmsc_inter;
+
+ hmsc_inter = relation->get_interval_set();
+ bmsc_inter = time_matrix->operator()(min_a, max_b);
+
+ result = MscTimeIntervalSetD::set_intersection(hmsc_inter, bmsc_inter);
+
+ if(result.is_empty())
+ return false;
+ else
+ if(result != bmsc_inter)
+ {
+std::cerr << "Warning: the HMSC interval do not cover whole bMSC interval" << std::endl;
+ return false;
+ }
+ }
+
+ if(!top_vec.empty())
+ min_b = get_min_event(conf);
+
+ if(!bottom_vec.empty())
+ max_b = get_max_event(node, conf);
+
+ std::vector<TimeRelationRefNodePtr>::iterator it_vec;
+ std::map<TimeRelationRefNodePtr, ConfigurationPtr>::iterator it_map;
+
+ if(max_b != NULL)
+ {
+ for(it_vec = bottom_vec.begin(); it_vec != bottom_vec.end(); it_vec++)
+ {
+ it_map = top_time_references.find(*it_vec);
+
+ if(it_map == top_time_references.end())
+ continue;
+
+ min_a = get_min_event(it_map->second);
+
+ MscTimeIntervalSetD result, hmsc_inter, bmsc_inter;
+
+ hmsc_inter = (*it_vec)->get_interval_set();
+ bmsc_inter = time_matrix->operator()(min_a, max_b);
+ result = MscTimeIntervalSetD::set_intersection(hmsc_inter, bmsc_inter);
+
+ if(result.is_empty())
+ return false;
+ else
+ if(result != bmsc_inter)
+ {
+std::cerr << "Warning: the HMSC interval do not cover whole bMSC interval" << std::endl;
+ return false;
+ }
+
+ }
+
+ for(it_vec = bottom_vec.begin(); it_vec != bottom_vec.end(); it_vec++)
+ {
+ it_map = bottom_time_references.find(*it_vec);
+
+ if(it_map == bottom_time_references.end())
+ continue;
+
+ max_a = get_max_event(it_map->first->get_ref_node_a(), it_map->second);
+
+ MscTimeIntervalSetD hmsc_inter = (*it_vec)->get_interval_set();
+ MscTimeIntervalSetD result, bmsc_inter_set;
+
+ bmsc_inter_set = time_matrix->operator()(max_a, max_b);
+ result = MscTimeIntervalSetD::set_intersection(hmsc_inter, bmsc_inter_set);
+
+ if(result.is_empty())
+ return false;
+ else
+ if(result != bmsc_inter_set)
+ {
+std::cerr << "Warning: the HMSC interval do not cover whole bMSC interval" << std::endl;
+ return false;
+ }
+ }
+
+ }
+
+ if(min_b != NULL)
+ {
+ for(it_vec = top_vec.begin(); it_vec != top_vec.end(); it_vec++)
+ {
+ it_map = bottom_time_references.find(*it_vec);
+
+ if(it_map == bottom_time_references.end())
+ continue;
+
+ max_a = get_max_event(it_map->first->get_ref_node_a(), it_map->second);
+
+ MscTimeIntervalSetD hmsc_inter = (*it_vec)->get_interval_set();
+ MscTimeIntervalSetD result, bmsc_inter_set;
+
+ bmsc_inter_set = time_matrix->operator()(max_a, min_b);
+ result = MscTimeIntervalSetD::set_intersection(hmsc_inter, bmsc_inter_set);
+
+ if(result.is_empty())
+ return false;
+ else
+ if(result != bmsc_inter_set)
+ {
+std::cerr << "Warning: the HMSC interval do not cover whole bMSC interval" << std::endl;
+ return false;
+ }
+ }
+
+ for(it_vec = top_vec.begin(); it_vec != top_vec.end(); it_vec++)
+ {
+ it_map = top_time_references.find(*it_vec);
+
+ if(it_map == top_time_references.end())
+ continue;
+
+ min_a = get_min_event(it_map->second);
+
+ MscTimeIntervalSetD hmsc_inter = (*it_vec)->get_interval_set();
+ MscTimeIntervalSetD result, bmsc_inter_set;
+
+ bmsc_inter_set = time_matrix->operator()(min_a, min_b);
+ result = MscTimeIntervalSetD::set_intersection(hmsc_inter, bmsc_inter_set);
+
+ if(result.is_empty())
+ return false;
+ else
+ if(result != bmsc_inter_set)
+ {
+std::cerr << "Warning: the HMSC interval do not cover whole bMSC interval" << std::endl;
+ return false;
+ }
+ }
+ }
+
+ return true;
+
+}
+
+Event* get_min_event(ConfigurationPtr conf)
+{
+ std::set<PositionPtr> positions = conf->get_positions();
+ std::set<PositionPtr>::iterator it;
+ //vector of events which could be minimal event of matching HMSC node
+ std::vector<Event*> pos_min;
+
+ for(it = positions.begin(); it != positions.end(); it++)
+ {
+ std::vector<Event*> events = (*it)->get_events();
+
+ if(events.size() == 0)
+ continue;
+
+ std::map<CoregionAreaPtr, CoregionOrderingPtr>::iterator cor_ordering_it;
+
+ if(events.size() > 1)
+ {
+ CoregionAreaPtr cor = dynamic_cast<CoregionArea*> (events.front()->get_general_area());
+
+ if(cor == NULL)
+ {
+ std::cerr << "Error: unexpected behaviour" << std::endl;
+ return NULL;
+ }
+
+ cor_ordering_it = coregion_ordering.find(cor);
+
+ if(cor_ordering_it != coregion_ordering.end())
+ {
+ pos_min.push_back(cor_ordering_it->second->getOrdering().front().get());
+ }
+ }
+ else
+ pos_min.push_back(events.front());
+ }
+
+ //set of the minimal events (in case more events, the algorithm is not able to decide the minimum one)
+ std::set<Event*> min;
+ min.insert(pos_min[0]);
+
+ //try to eliminate pos_min to one event
+ for(unsigned int i = 0; i < pos_min.size(); i++)
+ {
+ switch (compare_absolut_position((*min.begin()), pos_min[i]))
+ {
+ case 0: min.insert(pos_min[i]); break;
+ case 1: break;
+ case 2: min.clear(); min.insert(pos_min[i]); break;
+ default: std::cerr << "Error: unexpected behaviour" << std::endl;
+ }
+ }
+
+ if(min.size() != 1)
+ return NULL;
+ else
+ return *(min.begin());
+}
+
+Event* get_max_event(ReferenceNodePtr node, ConfigurationPtr conf)
+{
+ std::set<PositionPtr> positions = conf->get_positions();
+ std::set<PositionPtr>::iterator it;
+
+ std::map<std::wstring, std::vector<int> > node_last_events;
+ node_last_events = get_node_last_events(node);
+
+ //vector of posible events
+ std::vector<Event*> pos_max;
+
+ for(it = positions.begin(); it != positions.end(); it++)
+ {
+ std::vector<Event*> events = (*it)->get_events();
+
+ if(events.empty())
+ continue;
+
+ //spoliehame sa na strict order area takze tam vzdy bude iba jeden event
+ Event* e = events.front();
+ StrictEvent* s_e = dynamic_cast<StrictEvent*> (e);
+
+ //find instance in the map of node last events
+ std::map <std::wstring, std::vector<int> >::iterator node_last_it;
+ node_last_it = node_last_events.find(e->get_instance()->get_label());
+
+ if(node_last_it == node_last_events.end())
+ continue;
+
+ std::vector<int> node_events = node_last_it->second;
+
+ Event* temp;
+ for(unsigned int i = 0; i < node_events.size(); i++)
+ {
+ temp = find_event_on_instance_by_id(e->get_instance()->get_label(), node_events[i], s_e);
+
+ if(temp == NULL)
+ continue;
+
+ pos_max.push_back(temp);
+ }
+ }
+
+ //set of the maximal events (in case more events, the algorithm is not able to decide the maximum one)
+ std::set<Event*> max;
+ max.insert(pos_max[0]);
+
+ //try to eliminate pos_min to one event
+ for(unsigned int i = 0; i < pos_max.size(); i++)
+ {
+ switch (compare_absolut_position(pos_max[i], (*max.begin())))
+ {
+ case 0: max.insert(pos_max[i]); break;
+ case 1: break;
+ case 2: max.clear(); max.insert(pos_max[i]); break;
+ default: std::cerr << "Error: unexpected behaviour" << std::endl;
+ }
+ }
+
+ if(max.size() != 1)
+ return NULL;
+ else
+ return *(max.begin());
+}
+
+/*
+ * compare absolut position, is the fist parameter before (more minimal) than the second
+ *
+ * return: 0 - it is not decideable
+ * 1 - the fist is before the second
+ * 2 - the second is before the first
+ * 3 - error
+ */
+int compare_absolut_position(Event* first, Event* second)
+{
+ MscTimeIntervalSetD inter = time_matrix->operator()(first, second);
+ const IntervalList intervals = inter.get_set();
+ bool positive = false;
+ bool negative = false;
+
+ IntervalList::const_iterator it;
+
+ //in interval [0], positive and negative are not set => negative == positive => undecidable
+ for(it = intervals.begin(); it != intervals.end(); it++)
+ {
+ if(it->get_begin_value() > 0
+ || (it->get_begin_value() == 0 && !it->get_begin_closed()))
+ {
+ positive = true;
+ }
+
+ if(it->get_begin_value() < 0) negative = true;
+
+ if(it->get_end_value() > 0) positive = true;
+
+ if(it->get_end_value() < 0
+ || (it->get_end_value() == 0 && !it->get_end_closed()))
+ {
+ negative = true;
+ }
+ }
+
+ if(negative == positive)
+ return 0;
+
+ if(negative)
+ return 2;
+
+ if(positive)
+ return 1;
+
+ return 3;
+}
+
+std::map<std::wstring, std::vector<int> > get_node_last_events(ReferenceNodePtr node)
+{
+ MscPtr msc = node->get_msc();
+
+ BMscPtr bmsc = boost::dynamic_pointer_cast<BMsc>(msc);
+
+ if(bmsc == NULL)
+ std::cerr << "Error: Unexpected behaviur 35" << std::endl;
+
+ InstancePtrList instances = bmsc->get_instances();
+ InstancePtrList::iterator inst_it;
+
+ //name of instance, event identification
+ std::map<std::wstring, std::vector<int> > node_last_events;
+ EventPtr start;
+ EventArea* area;
+ StrictOrderArea* strict;
+ CoregionArea* cor;
+
+ for(inst_it = instances.begin(); inst_it != instances.end(); inst_it++)
+ {
+ area = (*inst_it)->get_first().get();
+ strict = dynamic_cast<StrictOrderArea*>(area);
+
+ if(strict != NULL)
+ {
+ start = strict->get_first();
+ std::vector<int> identifications;
+ std::vector<Event*> e_set = get_last_instance_event(start.get());
+//TODO dopracovat coregiony
+ Event* e = e_set.front();
+
+ if(e == NULL)
+ continue;
+
+ int it_id;
+ bool it_set = true;
+
+ //mozno by to chcelo prerobit na is_set_attribure aby sa tu zbytocne nedavali nove hodnoty do attributu, potom by sa mohlo zmazat remove_attribure z check node.
+ it_id = e->get_attribute("identification", -1, it_set);
+
+ if(!it_set)
+ identifications.push_back(it_id);
+
+ node_last_events.insert(std::make_pair((*inst_it)->get_label(), identifications));
+ }
+
+ cor = dynamic_cast<CoregionArea*>(area);
+
+ if(cor != NULL)
+ {
+ std::cout << "Coregion time intervals: This funcion is not currently supported." << std::endl;
+ }
+ }
+
+ return node_last_events;
+}
+
+std::vector<Event*> get_last_instance_event(Event* start)
+{
+ std::vector<Event*> result;
+
+ if(start == NULL)
+ return result;
+
+ EventArea* area = start->get_general_area();
+ EventArea* not_null_area = area;
+
+ StrictOrderArea* str;
+ CoregionArea* cor;
+
+ while(area->get_next() != NULL)
+ {
+ area = area->get_next().get();
+ str = dynamic_cast<StrictOrderArea*>(area);
+ cor = dynamic_cast<CoregionArea*>(area);
+
+ if(str == NULL)
+ {
+ if(!is_strict_area_null(str))
+ not_null_area = str;
+ }
+ else
+ if(!is_cor_area_null(cor))
+ not_null_area = cor;
+ }
+
+ str = dynamic_cast<StrictOrderArea*>(not_null_area);
+ cor = dynamic_cast<CoregionArea*>(not_null_area);
+
+ if(str != NULL)
+ {
+ result.push_back(str->get_last().get());
+ return result;
+ }
+ else
+ return get_last_coregion_events(cor);
+}
+
+std::vector<Event*> get_last_coregion_events(CoregionArea* cor)
+{
+ std::vector<Event*> result;
+
+ CoregionEventPVector vec = cor->get_maximal_events();
+ CoregionEventPVector::iterator it;
+
+ for(it = vec.begin(); it != vec.end(); it++)
+ {
+ EventPtr e = *it;
+ result.push_back(e.get());
+ }
+
+ return result;
+}
+
+void remove_events_attributes(std::vector<Event*> vec)
+{
+ std::vector<Event*>::iterator it;
+
+ for(it = vec.begin(); it != vec.end(); it++)
+ (*it)->remove_attribute<int>("identification");
+}
+
+BMscIntervalSetMatrix get_bmsc_matrix(BMscPtr bmsc_f)
+{
+ //matrix context inicialization
+ BMscIntervalSetMatrix matrix(bmsc_f);
+ //create matrix
+ matrix.build_up();
+
+ MscSolveTCSP solve;
+ //tight the matrix
+ MscSolveTCSPReport report = solve.solveTCSP(matrix);
+ //get the result of the tightening
+ matrix = report.m_matrix_result;
+
+ return matrix;
+}
Modified: trunk/src/membership/membership_alg.h
===================================================================
--- trunk/src/membership/membership_alg.h 2010-09-08 22:49:10 UTC (rev 896)
+++ trunk/src/membership/membership_alg.h 2010-09-08 23:01:50 UTC (rev 897)
@@ -23,6 +23,8 @@
#include "membership/export.h"
#include "check/pseudocode/msc_duplicators.h"
+bool contain_focused_instances(std::wstring instance);
+
class Position;
class Configuration;
class Membership;
@@ -279,14 +281,17 @@
return NULL;
}
- bool is_null()
+ bool is_null(std::vector<std::wstring> focused)
{
std::set<PositionPtr>::iterator it;
for(it = positions.begin(); it != positions.end(); it++)
{
if(!(*it)->get_events().empty())
- return false;
+ {
+ if(focused.empty() || contain_focused_instances((*it)->get_name()))
+ return false;
+ }
}
return true;
@@ -475,10 +480,7 @@
std::vector<CoregionEventPtr> a_ordering = a->getOrdering();
if(this->ordering.size() != a_ordering.size())
-{
-std::cerr << "fuck this " << this->ordering.size() << " "<< a_ordering.size() << std::endl;
exit (4); //return false;
-}
for(unsigned int i = 0; i < this->ordering.size(); i++)
{
@@ -533,6 +535,7 @@
* Checks whether hmsc satisfy universal boundedness property.
*/
virtual MscPtr find(MscPtr hmsc, MscPtr bmsc);
+ virtual MscPtr find(MscPtr hmsc, MscPtr bmsc, std::vector<std::wstring> instances);
MscPtr get_dp_msc(MscPtr msc);
Modified: trunk/tests/membership/CMakeLists.txt
===================================================================
--- trunk/tests/membership/CMakeLists.txt 2010-09-08 22:49:10 UTC (rev 896)
+++ trunk/tests/membership/CMakeLists.txt 2010-09-08 23:01:50 UTC (rev 897)
@@ -193,6 +193,26 @@
ADD_TEST(membership_test-82 ${MEMBERSHIP_TEST_EXECUTABLE} ${CMAKE_CURRENT_SOURCE_DIR}/test_bmsc28.mpr ${CMAKE_CURRENT_SOURCE_DIR}/test_bmsc28_4.mpr 0)
+#tests for new time algorithm
+ADD_TEST(membership_test-83 ${MEMBERSHIP_TEST_EXECUTABLE} ${CMAKE_CURRENT_SOURCE_DIR}/test_hmsc29.mpr ${CMAKE_CURRENT_SOURCE_DIR}/test_bmsc29_1.mpr 1)
+ADD_TEST(membership_test-84 ${MEMBERSHIP_TEST_EXECUTABLE} ${CMAKE_CURRENT_SOURCE_DIR}/test_hmsc29.mpr ${CMAKE_CURRENT_SOURCE_DIR}/test_bmsc29_2.mpr 0)
+ADD_TEST(membership_test-85 ${MEMBERSHIP_TEST_EXECUTABLE} ${CMAKE_CURRENT_SOURCE_DIR}/test_hmsc30.mpr ${CMAKE_CURRENT_SOURCE_DIR}/test_bmsc30_1.mpr 1)
+ADD_TEST(membership_test-86 ${MEMBERSHIP_TEST_EXECUTABLE} ${CMAKE_CURRENT_SOURCE_DIR}/test_hmsc30.mpr ${CMAKE_CURRENT_SOURCE_DIR}/test_bmsc30_2.mpr 0)
+
+ADD_TEST(membership_test-87 ${MEMBERSHIP_TEST_EXECUTABLE} ${CMAKE_CURRENT_SOURCE_DIR}/test_hmsc31.mpr ${CMAKE_CURRENT_SOURCE_DIR}/test_bmsc31_1.mpr 1)
+
+ADD_TEST(membership_test-88 ${MEMBERSHIP_TEST_EXECUTABLE} ${CMAKE_CURRENT_SOURCE_DIR}/time_hard_bmsc01.mpr ${CMAKE_CURRENT_SOURCE_DIR}/time_hard_bmsc_pat01.mpr 1)
+
+ADD_TEST(membership_test-89 ${MEMBERSHIP_TEST_EXECUTABLE} ${CMAKE_CURRENT_SOURCE_DIR}/time_hard_bmsc02.mpr ${CMAKE_CURRENT_SOURCE_DIR}/time_hard_bmsc_pat01.mpr 0)
+
+ADD_TEST(membership_test-90 ${MEMBERSHIP_TEST_EXECUTABLE} ${CMAKE_CURRENT_SOURCE_DIR}/time_hard_bmsc03.mpr ${CMAKE_CURRENT_SOURCE_DIR}/time_hard_bmsc_pat01.mpr 0)
+
+ADD_TEST(membership_test-91 ${MEMBERSHIP_TEST_EXECUTABLE} ${CMAKE_CURRENT_SOURCE_DIR}/time_hard_bmsc04.mpr ${CMAKE_CURRENT_SOURCE_DIR}/time_hard_bmsc_pat02.mpr 0)
+
+ADD_TEST(membership_test-92 ${MEMBERSHIP_TEST_EXECUTABLE} ${CMAKE_CURRENT_SOURCE_DIR}/time_hard_bmsc05.mpr ${CMAKE_CURRENT_SOURCE_DIR}/time_hard_bmsc_pat02.mpr 0)
+
+#coregion minimal
+ADD_TEST(membership_test-93 ${MEMBERSHIP_TEST_EXECUTABLE} ${CMAKE_CURRENT_SOURCE_DIR}/coregion_minimal.mpr ${CMAKE_CURRENT_SOURCE_DIR}/coregion_minimal_pat1.mpr 1)
Modified: trunk/tests/membership/membership_test.cpp
===================================================================
--- trunk/tests/membership/membership_test.cpp 2010-09-08 22:49:10 UTC (rev 896)
+++ trunk/tests/membership/membership_test.cpp 2010-09-08 23:01:50 UTC (rev 897)
@@ -44,10 +44,21 @@
{
if(argc < 4)
{
- std::cerr << "Usage: " << argv[0] << " <filename> <filename> <satisfied>" << std::endl;
+ std::cerr << "Usage: " << argv[0] << " <filename> <filename> <satisfied> <names of focused instances> (optional)" << std::endl;
return 1;
}
+ std::vector<std::wstring> focused_instances;
+
+ for(int i = 4; i < argc; i++)
+ {
+ std::string s = argv[i];
+ std::wstring temp(s.length(),L' ');
+ std::copy(s.begin(), s.end(), temp.begin());
+
+ focused_instances.push_back(temp);
+ }
+
Z120 z120;
StreamReportPrinter printer(std::wcerr);
@@ -90,23 +101,28 @@
BMscPtr bmsc = boost::dynamic_pointer_cast<BMsc>(msc_b[0]);
- MscPtr result = mem.find(msc[0], bmsc);
+ MscPtr result;
+ if(focused_instances.empty())
+ result = mem.find(msc[0], bmsc);
+ else
+ result = mem.find(msc[0], bmsc, focused_instances);
+
if(result == NULL)
{
-std::cout << "result was null" << std::endl;
+std::cerr << "result was null" << std::endl;
if(satisfied)
{
std::cerr << "ERROR: HMSC should contain bMSC" << std::endl;
errors = 1;
}
else
- std::cout << "OK: HMSC doesn't contain bMSC" << std::endl;
+ std::cerr << "OK: HMSC doesn't contain bMSC" << std::endl;
}
else
{
if(satisfied)
- std::cout << "OK: HMSC contains bMSC" << std::endl;
+ std::cerr << "OK: HMSC contains bMSC" << std::endl;
else
{
std::cerr << "ERROR: HMSC should not contain bMSC" << std::endl;
Added: trunk/tests/membership/test_bmsc29_1.mpr
===================================================================
--- trunk/tests/membership/test_bmsc29_1.mpr (rev 0)
+++ trunk/tests/membership/test_bmsc29_1.mpr 2010-09-08 23:01:50 UTC (rev 897)
@@ -0,0 +1,24 @@
+
+
+
+
+
+
+
+msc bmsc3;
+inst A;
+inst B;
+A: instance;
+label e1;
+in no,0 from B;
+time e0 [1];
+out ok,1 to B;
+time e1 [2,3];
+endinstance;
+B: instance;
+label e0;
+out no,0 to A;
+in ok,1 from A;
+endinstance;
+endmsc;
+
Added: trunk/tests/membership/test_bmsc29_2.mpr
===================================================================
--- trunk/tests/membership/test_bmsc29_2.mpr (rev 0)
+++ trunk/tests/membership/test_bmsc29_2.mpr 2010-09-08 23:01:50 UTC (rev 897)
@@ -0,0 +1,23 @@
+
+
+
+
+
+
+
+msc bmsc3;
+inst A;
+inst B;
+A: instance;
+label e1;
+in no,0 from B;
+time e0 [1];
+out ok,1 to B;
+endinstance;
+B: instance;
+label e0;
+out no,0 to A;
+in ok,1 from A;
+endinstance;
+endmsc;
+
Added: trunk/tests/membership/test_bmsc30_1.mpr
===================================================================
--- trunk/tests/membership/test_bmsc30_1.mpr (rev 0)
+++ trunk/tests/membership/test_bmsc30_1.mpr 2010-09-08 23:01:50 UTC (rev 897)
@@ -0,0 +1,24 @@
+
+
+
+
+
+
+
+msc bmsc3;
+inst A;
+inst B;
+A: instance;
+label e1;
+in no,0 from B;
+time e0 [1];
+out ok,1 to B;
+time e1 [2,3];
+endinstance;
+B: instance;
+label e0;
+out no,0 to A;
+in ok,1 from A;
+endinstance;
+endmsc;
+
Added: trunk/tests/membership/test_bmsc30_2.mpr
===================================================================
--- trunk/tests/membership/test_bmsc30_2.mpr (rev 0)
+++ trunk/tests/membership/test_bmsc30_2.mpr 2010-09-08 23:01:50 UTC (rev 897)
@@ -0,0 +1,23 @@
+
+
+
+
+
+
+
+msc bmsc3;
+inst A;
+inst B;
+A: instance;
+label e1;
+in no,0 from B;
+time e0 [1];
+out ok,1 to B;
+endinstance;
+B: instance;
+label e0;
+out no,0 to A;
+in ok,1 from A;
+endinstance;
+endmsc;
+
Added: trunk/tests/membership/test_bmsc31_1.mpr
===================================================================
--- trunk/tests/membership/test_bmsc31_1.mpr (rev 0)
+++ trunk/tests/membership/test_bmsc31_1.mpr 2010-09-08 23:01:50 UTC (rev 897)
@@ -0,0 +1,15 @@
+msc aaa;
+inst A;
+inst B;
+A: instance;
+label e1;
+in no,0 from B;
+out ok,1 to B;
+endinstance;
+B: instance;
+out no,0 to A;
+time e1 [3,6];
+in ok,1 from A;
+endinstance;
+endmsc;
+
Added: trunk/tests/membership/test_hmsc29.mpr
===================================================================
--- trunk/tests/membership/test_hmsc29.mpr (rev 0)
+++ trunk/tests/membership/test_hmsc29.mpr 2010-09-08 23:01:50 UTC (rev 897)
@@ -0,0 +1,22 @@
+mscdocument Ola;
+msc iha;
+initial connect L1;
+L1: reference aaa connect L2;
+L2: final;
+endmsc;
+
+msc aaa;
+inst A;
+inst B;
+A: instance;
+in no,0 from B;
+label e1;
+out ok,1 to B;
+endinstance;
+B: instance;
+out no,0 to A;
+time e1 [3,6];
+in ok,1 from A;
+endinstance;
+endmsc;
+
Added: trunk/tests/membership/test_hmsc30.mpr
===================================================================
--- trunk/tests/membership/test_hmsc30.mpr (rev 0)
+++ trunk/tests/membership/test_hmsc30.mpr 2010-09-08 23:01:50 UTC (rev 897)
@@ -0,0 +1,22 @@
+mscdocument Ola;
+msc iha;
+initial connect L1;
+L1: reference aaa connect L2;
+L2: final;
+endmsc;
+
+msc aaa;
+inst A;
+inst B;
+A: instance;
+in no,0 from B;
+out ok,1 to B;
+time e1 [-6,-3];
+endinstance;
+B: instance;
+label e1;
+out no,0 to A;
+in ok,1 from A;
+endinstance;
+endmsc;
+
Added: trunk/tests/membership/test_hmsc31.mpr
===================================================================
--- trunk/tests/membership/test_hmsc31.mpr (rev 0)
+++ trunk/tests/membership/test_hmsc31.mpr 2010-09-08 23:01:50 UTC (rev 897)
@@ -0,0 +1,22 @@
+mscdocument Ola;
+msc iha;
+initial connect L1;
+L1: reference aaa connect L2;
+L2: final;
+endmsc;
+
+msc aaa;
+inst A;
+inst B;
+A: instance;
+label e1;
+in no,0 from B;
+out ok,1 to B;
+endinstance;
+B: instance;
+out no,0 to A;
+time e1 [3,6];
+in ok,1 from A;
+endinstance;
+endmsc;
+
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
