Menu
▾
▴
[Scstudio-commits] SF.net SVN: scstudio:[870] trunk
|
From: <lko...@us...> - 2010-09-03 14:13:06
|
Revision: 870
http://scstudio.svn.sourceforge.net/scstudio/?rev=870&view=rev
Author: lkorenciak
Date: 2010-09-03 14:12:59 +0000 (Fri, 03 Sep 2010)
Log Message:
-----------
fixed few bugs
Modified Paths:
--------------
trunk/src/check/time/tightening.h
trunk/src/check/time/time_pseudocode.h
trunk/src/check/time/time_trace_race.h
trunk/src/data/msc.h
Added Paths:
-----------
trunk/tests/time/CMakeFiles/
Modified: trunk/src/check/time/tightening.h
===================================================================
--- trunk/src/check/time/tightening.h 2010-09-03 13:37:25 UTC (rev 869)
+++ trunk/src/check/time/tightening.h 2010-09-03 14:12:59 UTC (rev 870)
@@ -267,11 +267,13 @@
for(TimeRelationRefNodePtrSet::const_iterator it=top->begin();it!=top->end();it++)
{
if(open_rel.find(it->get()) != open_rel.end())
- {
+ {//time relation is open -> close it
const TimeRelationRefNodePtrSet* other;
+ //find the correct time relation (for getting previously created
+ // node to which the processed time relation (it*) should be connected)
if(ref==(*it)->get_ref_node_a()&&(*it)->is_top_node_a())
{
- if((*it)->is_top_node_b())
+ if((*it)->is_top_node_b())
other = &((*it)->get_ref_node_b()->get_time_relations_top());
else
other = &((*it)->get_ref_node_b()->get_time_relations_bottom());
@@ -283,10 +285,11 @@
else
other = &((*it)->get_ref_node_a()->get_time_relations_bottom());
}
- b_matrix.fill(a,rel_to_event[other],(*it)->get_interval_set());
- b_matrix.tied_rel_to_cell(*it,a, rel_to_event[other]);
+ //fill the time relation to the matrix (node a was found later)
+ b_matrix.fill(rel_to_event[other],a,(*it)->get_interval_set());
+ b_matrix.tied_rel_to_cell(*it,rel_to_event[other],a);
}
- else
+ else //time relation has not been opened yet -> open it
open_rel.insert((*it).get());
}
@@ -301,7 +304,7 @@
std::vector<std::pair<EventP,EventP> > floor(max.size());
for(MaximalEventPList::iterator m=max.begin();m!=max.end();m++)
{
- Event* copy = dynamic_cast<Event*>(duplicator.get_copy_with_occurence(*m,bmsc_to_count[in.get()]));
+ Event* copy = dynamic_cast<Event*>(duplicator.get_copy_with_occurence(*m,bmsc_to_count[in.get()]));
b_matrix.fill(copy,a,MscTimeIntervalD(0,D::infinity()));
floor.push_back(std::make_pair<EventP,EventP>(copy,a));
}
@@ -312,8 +315,10 @@
for(TimeRelationRefNodePtrSet::iterator it=bottom->begin();it!=bottom->end();it++)
{
if(open_rel.find(it->get()) != open_rel.end())
- {
+ { //time relation is open -> close it
const TimeRelationRefNodePtrSet* other;
+ //find the correct time relation (for getting previously created
+ // node to which the processed time relation (it*) should be connected)
if(ref==(*it)->get_ref_node_a()&&(*it)->is_bottom_node_a())
{
if((*it)->is_top_node_b())
@@ -328,10 +333,11 @@
else
other = &((*it)->get_ref_node_a()->get_time_relations_bottom());
}
+ //fill the time relation to the matrix (node a was found later)
b_matrix.fill(rel_to_event[other],a,(*it)->get_interval_set());
b_matrix.tied_rel_to_cell(*it,rel_to_event[other],a);
}
- else
+ else //time relation has not been opened yet -> open it
open_rel.insert((*it).get());
}
}
Modified: trunk/src/check/time/time_pseudocode.h
===================================================================
--- trunk/src/check/time/time_pseudocode.h 2010-09-03 13:37:25 UTC (rev 869)
+++ trunk/src/check/time/time_pseudocode.h 2010-09-03 14:12:59 UTC (rev 870)
@@ -225,7 +225,7 @@
using IntervalSetMatrix::operator();
- //! return number of event in matrix
+ //! return position of the event in the matrix
const unsigned get_number(EventP e)
{
return m_event_to_number[e];
Modified: trunk/src/check/time/time_trace_race.h
===================================================================
--- trunk/src/check/time/time_trace_race.h 2010-09-03 13:37:25 UTC (rev 869)
+++ trunk/src/check/time/time_trace_race.h 2010-09-03 14:12:59 UTC (rev 870)
@@ -23,6 +23,7 @@
#include "data/dfs_hmsc_traverser.h"
#include "data/dfs_hmsc_flat_traverser.h"
#include "data/dfs_events_traverser.h"
+#include "data/Z120/z120.h"
#include "check/pseudocode/utils.h"
#include "check/time/export.h"
@@ -74,7 +75,6 @@
public:
void on_path_found(MscElementPList& path){
-
//code for testing:
// std::cout << "new path:" << std::endl;
//
@@ -93,7 +93,16 @@
HMscTighter tighter; //TODO ONDRA?? preco causal nemozem nastavit rovno???
(tighter).set_causal();
std::pair<BMscIntervalSetMatrix,IntervalSetMatrix> pair = (tighter).tighten_BMscGraph_path(path);
+
+//code for testing:
+/* Z120 z120;
+ BMscPtr bmsc_copy_2;
+ HMscFlatPathToBMscDuplicator duplicator2;
+ bmsc_copy_2 = duplicator2.duplicate_path(path);
+ z120.save_msc(std::cout,L"duplicated_path",bmsc_copy_2);*/
+
+
//check time race
// get matrix after tightening
BMscIntervalSetMatrix causal_matrix = pair.first;
@@ -107,26 +116,28 @@
EventTopologyHandler handler(causal_matrix.get_original_bmsc());
// EventTopologyHandler handler = *causal_matrix.get_m_event_topology_handler(); //TODO why this is not possible? ask Ondra!!!
-
for (e_before=events.begin();e_before!=events.end();e_before++)
{
for (e_after=events.begin();e_after!=events.end();e_after++)
{
if (handler.visual_is_leq(*e_before,*e_after))
{
-
//check whether intersection (-infty,0) and constraint corresponding to e_before and e_after is empty
if(!MscTimeIntervalSetD::set_intersection(MscTimeIntervalD(0,-D::infinity(),0,0),
matrix_result.operator()(causal_matrix.get_number(*e_before),
- causal_matrix.get_number(*e_after))).is_empty()
- && ((*e_before)->get_instance() == (*e_after)->get_instance())
+ causal_matrix.get_number(*e_after))).is_empty()){
+ Instance* instance1 = (*e_before)->get_instance();
+ Instance* instance2 = (*e_after)->get_instance();
+ if(instance1 && instance2
+ && instance1 == instance2
) //races are only on the same instance
{
+
//time race found
//duplicate hmsc
Event* event_original1 = *e_before;
Event* event_original2 = *e_after;
-
+
while(event_original1->get_original()!=NULL)
{
event_original1 = event_original1->get_original();
@@ -162,7 +173,7 @@
//throw exception with counterexample HMSC
throw TimeRaceInHMscException(hmsc);
- }
+ }}
}
}
}
Modified: trunk/src/data/msc.h
===================================================================
--- trunk/src/data/msc.h 2010-09-03 13:37:25 UTC (rev 869)
+++ trunk/src/data/msc.h 2010-09-03 14:12:59 UTC (rev 870)
@@ -1825,6 +1825,7 @@
EventTmpl(Event* original=NULL)
:Event(original)
{
+ m_area = NULL;
}
public:
@@ -1844,7 +1845,8 @@
Instance* get_instance() const
{
- return m_area->get_instance();
+ if(m_area) return m_area->get_instance();
+ else return NULL;
}
EventArea* get_general_area() const
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
