Menu
▾
▴
[Scstudio-commits] SF.net SVN: scstudio:[123] trunk
|
From: <got...@us...> - 2008-11-28 23:40:01
|
Revision: 123
http://scstudio.svn.sourceforge.net/scstudio/?rev=123&view=rev
Author: gotthardp
Date: 2008-11-28 23:39:47 +0000 (Fri, 28 Nov 2008)
Log Message:
-----------
Directory structure reorganized.
Modified Paths:
--------------
trunk/CMakeLists.txt
trunk/README
trunk/src/CMakeLists.txt
trunk/src/check/CMakeLists.txt
trunk/src/data/CMakeLists.txt
trunk/src/data/Z120/Z120.cpp
trunk/src/data/Z120/Z120.h
trunk/src/data/counted_ptr.h
trunk/src/data/msc.cpp
trunk/src/data/msc.h
trunk/src/data/msc_modifications.h
trunk/src/data/msc_visual.h
trunk/tests/CMakeLists.txt
trunk/tests/acyclic_checker_test.cpp
trunk/tests/deadlock_checker_test.cpp
trunk/tests/dot_writer.h
trunk/tests/fifo_checker_test.cpp
trunk/tests/livelock_checker_test.cpp
Added Paths:
-----------
trunk/src/check/liveness/
trunk/src/check/liveness/CMakeLists.txt
trunk/src/check/liveness/deadlock_checker.cpp
trunk/src/check/liveness/deadlock_checker.h
trunk/src/check/liveness/livelock_checker.cpp
trunk/src/check/liveness/livelock_checker.h
trunk/src/check/order/
trunk/src/check/order/CMakeLists.txt
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/
trunk/src/check/pseudocode/CMakeLists.txt
trunk/src/check/pseudocode/causal_closure_initiator.cpp
trunk/src/check/pseudocode/causal_closure_initiator.h
trunk/src/check/pseudocode/msc_duplicators.cpp
trunk/src/check/pseudocode/msc_duplicators.h
trunk/src/check/pseudocode/refnode_finder.cpp
trunk/src/check/pseudocode/refnode_finder.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/
trunk/src/check/race/CMakeLists.txt
trunk/src/check/race/bmsc_race_checker.cpp
trunk/src/check/race/bmsc_race_checker.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/data/checker.h
trunk/src/data/dfs_area_traverser.cpp
trunk/src/data/dfs_area_traverser.h
trunk/src/data/dfs_bmsc_graph_traverser.cpp
trunk/src/data/dfs_bmsc_graph_traverser.h
trunk/src/data/dfs_events_traverser.cpp
trunk/src/data/dfs_events_traverser.h
trunk/src/data/dfs_hmsc_traverser.cpp
trunk/src/data/dfs_hmsc_traverser.h
trunk/src/data/dfs_inner_hmsc_traverser.cpp
trunk/src/data/dfs_inner_hmsc_traverser.h
trunk/src/data/dfs_instance_events_traverser.cpp
trunk/src/data/dfs_instance_events_traverser.h
trunk/src/data/dfs_refnode_hmsc_traverser.cpp
trunk/src/data/dfs_refnode_hmsc_traverser.h
trunk/src/data/dfsb_hmsc_traverser.cpp
trunk/src/data/dfsb_hmsc_traverser.h
Removed Paths:
-------------
trunk/src/check/acyclic_checker.cpp
trunk/src/check/acyclic_checker.h
trunk/src/check/bmsc_race_checker.cpp
trunk/src/check/bmsc_race_checker.h
trunk/src/check/causal_closure_initiator.cpp
trunk/src/check/causal_closure_initiator.h
trunk/src/check/checker.h
trunk/src/check/deadlock_checker.cpp
trunk/src/check/deadlock_checker.h
trunk/src/check/dfs_area_traverser.cpp
trunk/src/check/dfs_area_traverser.h
trunk/src/check/dfs_bmsc_graph_traverser.cpp
trunk/src/check/dfs_bmsc_graph_traverser.h
trunk/src/check/dfs_events_traverser.cpp
trunk/src/check/dfs_events_traverser.h
trunk/src/check/dfs_hmsc_traverser.cpp
trunk/src/check/dfs_hmsc_traverser.h
trunk/src/check/dfs_inner_hmsc_traverser.cpp
trunk/src/check/dfs_inner_hmsc_traverser.h
trunk/src/check/dfs_instance_events_traverser.cpp
trunk/src/check/dfs_instance_events_traverser.h
trunk/src/check/dfs_refnode_hmsc_traverser.cpp
trunk/src/check/dfs_refnode_hmsc_traverser.h
trunk/src/check/dfsb_hmsc_traverser.cpp
trunk/src/check/dfsb_hmsc_traverser.h
trunk/src/check/fifo_checker.cpp
trunk/src/check/fifo_checker.h
trunk/src/check/footprint.cpp
trunk/src/check/footprint.h
trunk/src/check/livelock_checker.cpp
trunk/src/check/livelock_checker.h
trunk/src/check/msc_duplicators.cpp
trunk/src/check/msc_duplicators.h
trunk/src/check/race_checker.cpp
trunk/src/check/race_checker.h
trunk/src/check/refnode_finder.cpp
trunk/src/check/refnode_finder.h
trunk/src/check/utils.h
trunk/src/check/visual_closure_initiator.cpp
trunk/src/check/visual_closure_initiator.h
Property Changed:
----------------
trunk/CMakeLists.txt
trunk/src/CMakeLists.txt
trunk/src/check/CMakeLists.txt
trunk/src/data/CMakeLists.txt
trunk/src/data/Z120/CMakeLists.txt
trunk/src/data/Z120/Z120.cpp
trunk/src/data/Z120/Z120.h
trunk/src/data/Z120/main.cpp
trunk/src/data/msc_modifications.h
trunk/tests/CMakeLists.txt
trunk/tests/acyclic_checker_test.cpp
trunk/tests/deadlock_checker_test.cpp
trunk/tests/dot_writer.h
trunk/tests/fifo_checker_test.cpp
trunk/tests/livelock_checker_test.cpp
Modified: trunk/CMakeLists.txt
===================================================================
--- trunk/CMakeLists.txt 2008-11-28 20:26:06 UTC (rev 122)
+++ trunk/CMakeLists.txt 2008-11-28 23:39:47 UTC (rev 123)
@@ -9,8 +9,8 @@
INCLUDE(${CMAKE_ROOT}/Modules/Dart.cmake)
INCLUDE_DIRECTORIES(src)
-ADD_SUBDIRECTORY(src .)
-ADD_SUBDIRECTORY(tests .)
+ADD_SUBDIRECTORY(src)
+ADD_SUBDIRECTORY(tests)
-# $Id: CMakeLists.txt,v 1.7 2008/11/06 15:16:29 gotthardp Exp $
+# $Id$
Property changes on: trunk/CMakeLists.txt
___________________________________________________________________
Added: svn:keywords
+ Id
Added: svn:eol-style
+ native
Modified: trunk/README
===================================================================
--- trunk/README 2008-11-28 20:26:06 UTC (rev 122)
+++ trunk/README 2008-11-28 23:39:47 UTC (rev 123)
@@ -16,6 +16,7 @@
view/ Applications.
visio/ Microsoft Visio plug-in.
test/ Console application for tests under Unix/Linux.
+ tests/ Automated regression tests.
To get the latest sources
svn co https://scstudio.svn.sourceforge.net/svnroot/scstudio/trunk scstudio
Modified: trunk/src/CMakeLists.txt
===================================================================
--- trunk/src/CMakeLists.txt 2008-11-28 20:26:06 UTC (rev 122)
+++ trunk/src/CMakeLists.txt 2008-11-28 23:39:47 UTC (rev 123)
@@ -1,3 +1,4 @@
ADD_SUBDIRECTORY(data)
ADD_SUBDIRECTORY(check)
+# $Id$
Property changes on: trunk/src/CMakeLists.txt
___________________________________________________________________
Added: svn:keywords
+ Id
Added: svn:eol-style
+ native
Modified: trunk/src/check/CMakeLists.txt
===================================================================
--- trunk/src/check/CMakeLists.txt 2008-11-28 20:26:06 UTC (rev 122)
+++ trunk/src/check/CMakeLists.txt 2008-11-28 23:39:47 UTC (rev 123)
@@ -1,22 +1,8 @@
-#traversers
-#ADD_LIBRARY(dfs_area_traverser STATIC dfs_area_traverser.cpp)
-ADD_LIBRARY(dfs_events_traverser STATIC dfs_events_traverser.cpp)
-ADD_LIBRARY(dfs_hmsc_traverser STATIC dfs_hmsc_traverser.cpp)
-ADD_LIBRARY(dfsb_hmsc_traverser STATIC dfsb_hmsc_traverser.cpp)
-ADD_LIBRARY(dfs_instance_events_traverser STATIC dfs_instance_events_traverser.cpp)
-ADD_LIBRARY(dfs_bmsc_graph_traverser STATIC dfs_bmsc_graph_traverser.cpp)
-ADD_LIBRARY(refnode_finder STATIC refnode_finder.cpp)
+ADD_SUBDIRECTORY(pseudocode)
-#order relation
-#ADD_LIBRARY(causal_closure_initiator STATIC causal_closure_initiator.cpp)
-ADD_LIBRARY(visual_closure_initiator STATIC visual_closure_initiator.cpp)
+# plug-ins
+ADD_SUBDIRECTORY(liveness)
+ADD_SUBDIRECTORY(order)
+# ADD_SUBDIRECTORY(race)
-#checkers
-#ADD_LIBRARY(acyclic_checker STATIC acyclic_checker.cpp)
-ADD_LIBRARY(deadlock_checker STATIC deadlock_checker.cpp)
-ADD_LIBRARY(fifo_checker STATIC fifo_checker.cpp)
-ADD_LIBRARY(livelock_checker STATIC livelock_checker.cpp)
-#ADD_LIBRARY(race_checker STATIC race_checker.cpp)
-
-#other
-#ADD_LIBRARY(footprint STATIC footprint.cpp)
+# $Id$
Property changes on: trunk/src/check/CMakeLists.txt
___________________________________________________________________
Added: svn:keywords
+ Id
Deleted: trunk/src/check/acyclic_checker.cpp
===================================================================
--- trunk/src/check/acyclic_checker.cpp 2008-11-28 20:26:06 UTC (rev 122)
+++ trunk/src/check/acyclic_checker.cpp 2008-11-28 23:39:47 UTC (rev 123)
@@ -1,53 +0,0 @@
-/*
- * scstudio - Sequence Chart Studio
- * http://scstudio.sourceforge.net
- *
- * This library is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public
- * License version 2.1, as published by the Free Software Foundation.
- *
- * This library is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * Copyright (c) 2008 Jindra Babica <ba...@ma...>
- *
- * $Id$
- */
-
-#include "check/acyclic_checker.h"
-
-AcyclicCheckerPtr AcyclicChecker::m_instance;
-
-BMsc* AcyclicChecker::create_counter_example(const EventPList& path)
-{
- BMsc* bmsc = new BMsc(path.front()->get_instance()->get_bmsc());
- //TODO: construction of counter example
- return bmsc;
-}
-
-BMscPtr AcyclicChecker::check(BMscPtr bmsc, ChannelMapperPtr chm)
-{
- AcyclicCheckerListener listener;
- DFSEventsTraverser traverser;
- traverser.add_white_event_found_listener(&listener);
- traverser.add_gray_event_found_listener(&listener);
- traverser.add_event_finished_listener(&listener);
- BMscPtr result;
- try
- {
- traverser.traverse(bmsc);
- }
- catch(CycleDetectedException& cde)
- {
- result = create_counter_example(listener.get_path());
- traverser.cleanup_traversing_attributes();
- }
- return result;
-}
-
-void AcyclicChecker::cleanup_attributes()
-{
-
-}
Deleted: trunk/src/check/acyclic_checker.h
===================================================================
--- trunk/src/check/acyclic_checker.h 2008-11-28 20:26:06 UTC (rev 122)
+++ trunk/src/check/acyclic_checker.h 2008-11-28 23:39:47 UTC (rev 123)
@@ -1,110 +0,0 @@
-/*
- * scstudio - Sequence Chart Studio
- * http://scstudio.sourceforge.net
- *
- * This library is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public
- * License version 2.1, as published by the Free Software Foundation.
- *
- * This library is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * Copyright (c) 2008 Jindra Babica <ba...@ma...>
- *
- * $Id$
- */
-
-#include "check/checker.h"
-#include "data/msc.h"
-#include "check/dfs_events_traverser.h"
-
-class AcyclicChecker;
-
-typedef counted_ptr<AcyclicChecker> AcyclicCheckerPtr;
-
-class AcyclicCheckerListener:
-public WhiteEventFoundListener,
-public GrayEventFoundListener,
-public EventFinishedListener
-{
-
-protected:
-
- EventPList m_path;
-
-public:
-
- void on_white_event_found(Event* e)
- {
- m_path.push_back(e);
- }
-
- void on_gray_event_found(Event* e)
- {
- m_path.push_back(e);
- throw CycleDetectedException();
- }
-
- void on_event_finished(Event* e)
- {
- m_path.pop_back();
- }
-
- const EventPList& get_path()
- {
- return m_path;
- }
-
-};
-
-class AcyclicChecker: public Checker, public BMscChecker
-{
-
-protected:
-
- /**
- * Common instance.
- */
- static AcyclicCheckerPtr m_instance;
-
- BMsc* create_counter_example(const EventPList& path);
-
- AcyclicChecker()
- {
- }
-
-public:
-
- ~AcyclicChecker()
- {
- }
-
- /**
- * Checks whether bmsc has acyclic events' dependecy
- */
- BMscPtr check(BMscPtr bmsc, ChannelMapperPtr chm);
-
- /**
- * Cleans up no more needed attributes.
- */
- void cleanup_attributes();
-
- /**
- * Supports all mappers
- */
- bool is_supported(ChannelMapperPtr chm)
- {
- return true;
- }
-
- static AcyclicCheckerPtr instance()
- {
- if(!m_instance.get())
- m_instance = new AcyclicChecker();
- return m_instance;
- }
-
- };
-
Deleted: trunk/src/check/bmsc_race_checker.cpp
===================================================================
--- trunk/src/check/bmsc_race_checker.cpp 2008-11-28 20:26:06 UTC (rev 122)
+++ trunk/src/check/bmsc_race_checker.cpp 2008-11-28 23:39:47 UTC (rev 123)
@@ -1,172 +0,0 @@
-/*
- * scstudio - Sequence Chart Studio
- * http://scstudio.sourceforge.net
- *
- * This library is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public
- * License version 2.1, as published by the Free Software Foundation.
- *
- * This library is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * Copyright (c) 2008 Jindra Babica <ba...@ma...>
- *
- * $Id$
- */
-
-#include "check/bmsc_race_checker.h"
-
-void MinimalEventsInitiator::on_white_node_found(ReferenceNode* node)
-{
- BMscPtr b = node->get_bmsc();
- const InstancePtrList& instances = b->get_instances();
- //compute minimal Events of Instances
- EventPList minimal_events;
- InstancePtrList::const_iterator i;
- for(i=instances.begin();i!=instances.end();i++)
- {
- EventPList* events = DFSInstanceEventsTraverser::topology_order(*i);
- EventPList::const_iterator e1 = events->begin();
- while(e1!=events->end())
- {
- EventPList::const_iterator e2 = events->begin();
- while(e2!=events->end())
- {
- if(e1!=e2)
- {
- Event* e = *e2;
- BoolVector& e2_causal = m_caus_initiator->get_causal_closure(*e2);
- size_t e1_index = m_vis_initiator->get_topology_index(*e1);
- //e2<<e1 => e1 isn't minimal
- if(e2_causal[e1_index]) break;
- }
- e2++;
- }
- //'while loop' hasn't found any Event e2 to be less than e1
- if(e2==events.end())
- minimal_events.push_back(*e1);
- e1++;
- }
- delete events;
- }
- /*
- For the minimal_events find Instances containing less Events.
- Note that if there exists any less Event e1 at Instance i, e1 must be grater
- or equal to some Event e2 in minimal_events, therefore we will use only
- minimal_events to seek.
- */
- EventPList::const_iterator e;
- ExtremeEvents& extreme_events = get_minimal_events(b.get());
- for(e=minimal_events.begin();e!=minimal_events.end();e++)
- {
- EventDependentInstances e_instances(*e,m_instance_marker.get_count());
- size_t e_index = m_vis_initiator->get_topology_index(*e);
- EventPList::const_iterator f;
- for(f=minimal_events.begin();f!=minimal_events.end();f++)
- {
- //if f is less than e then Instance of f must be inserted
- BoolVector& closure = m_caus_initiator->get_causal_closure(*f);
- if(closure[e_index])
- e_instances.set_dependent(
- m_instance_marker->get_id((*f)->get_instance()));
- }
- extreme_events.add_extreme_event(e_instances);
- }
- m_modified_bmscs.push_back(b.get());
-}
-
-BMsc* BMscRaceChecker::create_counter_example(Event* e1, Event* e2)
-{
- BMsc* bmsc = new BMsc(e1->get_instance()->get_bmsc());
- InstancePtr common_instance = new Instance(bmsc,e1->get_instance());
- bmsc->add_instance(common_instance);
- BoolVector& e2_causal = m_causal_initiator.get_causal_closure(e2);
- size_t e1_index = m_visual_initiator.get_topology_index(e1);
- MscMessagePtr e1_message;
- if(e1->is_send())
- e1_message = new MscMessage(
- common_instance.get(),NULL,e1->get_message().get());
- else
- e1_message = new MscMessage(
- NULL,common_instance.get(),e1->get_message().get());
- MscMessagePtr e2_message;
- if(e2->is_send())
- e2_message = new MscMessage(
- common_instance.get(),NULL,e2->get_message().get());
- else
- e2_message = new MscMessage(
- NULL,common_instance.get(),e2->get_message().get());
- //e2 << e1
- if(e2_causal[e1_index])
- {
- StrictOrderAreaPtr common_strict = new StrictOrderArea(
- common_instance.get());
- StrictEventPtr e1_strict = new StrictEvent(common_strict.get(),e1_message,e1);
- StrictEventPtr e2_strict = new StrictEvent(common_strict.get(),e2_message,e2);
- common_strict->set_first(e1_strict);
- e1_strict->set_successor(e2_strict);
- common_instance->set_first(common_strict);
- }
- //e2 || e1
- else
- {
- CoregionAreaPtr common_coregion = new CoregionArea(common_instance.get());
- CoregionEvent* e1_coregion = new CoregionEvent(
- common_coregion.get(),e1_message,e1);
- CoregionEvent* e2_coregion = new CoregionEvent(
- common_coregion.get(),e2_message,e2);
- common_coregion->add_minimal_event(e1_coregion);
- common_coregion->add_minimal_event(e2_coregion);
- common_instance->set_first(common_coregion);
- }
- return bmsc;
-}
-
-BMscPtr BMscRaceChecker::check(BMscPtr bmsc, ChannelMapperPtr mapper)
-{
- DFSEventsTraverser traverser;
- TopologicalOrderListener topology_listener;
- traverser.add_event_finished_listener(this);
- traverser.traverse(bmsc);
- EventPVector topology(
- topology_listener.get_topology().begin(),
- topology_listener.get_topology().end()
- );
- m_visual_initiator.initialize(topology);
- m_causal_initiator.initialize(topology,m_visual_initiator,mapper);
- OrderCheckerListener order_checker_listener(&m_visual_initiator);
- DFSInstanceEventsTraverser instance_traverser;
- for(size_t i = 0; i < topology.size(); i++)
- {
- //in this block checkout whether there is any Event in race with topology[i]
- order_checker_listener.reset(
- topology[i],
- &m_visual_initiator.get_visual_closure(topology[i]),
- &m_causal_initiator.get_causal_closure(topology[i]));
- try
- {
- instance_traverser.traverse(topology[i]->get_instance());
- instance_traverser.cleanup_traversing_attributes();
- }
- catch(EventRaceException& e)
- {
- instance_traverser.cleanup_traversing_attributes();
- return create_counter_example(topology[i],e->get_event());
- }
- }
- return BMscPtr();
-}
-
-void BMscRaceChecker::cleanup_attributes()
-{
- m_visual_initiator.cleanup_attributes();
- m_causal_initiator.cleanup_attributes();
- while(!m_modified_instaces.empty())
- {
- Instance* i = m_modified_instaces.front();
- m_modified_instaces.pop_front();
- i->remove_attribute<EventPList>(m_instance_events_attribute);
- }
-}
Deleted: trunk/src/check/bmsc_race_checker.h
===================================================================
--- trunk/src/check/bmsc_race_checker.h 2008-11-28 20:26:06 UTC (rev 122)
+++ trunk/src/check/bmsc_race_checker.h 2008-11-28 23:39:47 UTC (rev 123)
@@ -1,74 +0,0 @@
-/*
- * scstudio - Sequence Chart Studio
- * http://scstudio.sourceforge.net
- *
- * This library is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public
- * License version 2.1, as published by the Free Software Foundation.
- *
- * This library is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * Copyright (c) 2008 Jindra Babica <ba...@ma...>
- *
- * $Id$
- */
-
-#ifndef _BMSC_RACE_CHECKER_H
-#define _BMSC_RACE_CHECKER_H
-
-#include "data/msc.h"
-#include "check/dfs_events_traverser.h"
-#include "check/visual_closure_initiator.h"
-#include "check/causal_closure_initiator.h"
-
-typedef std::list<Instance*> InstancePList;
-
-class BMscRaceChecker:
-public BMscChecker,
-public TopologicalOrderListener
-{
-
-protected:
-
- VisualClosureInitiator m_visual_initiator;
-
- CausalClosureInitiator m_causal_initiator;
-
- static const std::string m_instance_events_attribute;
-
- InstancePList m_modified_instaces;
-
- EventPList& get_instance_events(Instance* i)
- {
- static EventPList empty;
- return i->get_attribute<EventPList>(m_instance_events_attribute,empty);
- }
-
- /**
- * It was found that e1<e2 but not e1<<e2
- */
- BMsc* create_counter_example(Event* e1, Event* e2);
-
-public:
-
- BMscRaceChecker()
- {
-
- }
-
- BMscPtr check(BMscPtr bmsc, ChannelMapperPtr mapper);
-
- virtual void on_event_finished(Event* event)
- {
- TopologicalOrderListener::on_event_finished(event);
- //used to compare only ordering of events at the same instance
- get_instance_events(event->get_instance()).push_front(event);
- }
-
- void cleanup_attributes();
-
-};
-#endif /* _BMSC_RACE_CHECKER_H */
Deleted: trunk/src/check/causal_closure_initiator.cpp
===================================================================
--- trunk/src/check/causal_closure_initiator.cpp 2008-11-28 20:26:06 UTC (rev 122)
+++ trunk/src/check/causal_closure_initiator.cpp 2008-11-28 23:39:47 UTC (rev 123)
@@ -1,106 +0,0 @@
-/*
- * scstudio - Sequence Chart Studio
- * http://scstudio.sourceforge.net
- *
- * This library is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public
- * License version 2.1, as published by the Free Software Foundation.
- *
- * This library is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * Copyright (c) 2008 Jindra Babica <ba...@ma...>
- *
- * $Id$
- */
-
-#include <stack>
-
-#include "check/causal_closure_initiator.h"
-
-void CausalClosureInitiator::cleanup_attributes()
-{
- while(!m_modified_events.empty())
- {
- Event* e = m_modified_events.top();
- e->remove_attribute<BoolVector>(m_causal_closure_attribute);
- m_modified_events.pop();
- }
-}
-
-void CausalClosureInitiator::initialize(const EventPVector& events,
- VisualClosureInitiator& visual_closure_init, ChannelMapperPtr mapper)
-{
- //initialize matrix
- size_t events_count = events.size();
- EventPList::const_iterator i;
- //closure[x][y]==true <=> x << y
- std::vector<BoolVector*> closure(events_count);
- for(size_t i=0;i<events_count;i++)
- {
- Event* i_event = events[i];
- BoolVector& causal_closure = get_causal_closure(i_event);
- causal_closure.resize(events_count,false);
- closure[i] = &causal_closure;
- m_modified_events.push(i_event);
- //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;
- }
- for(size_t i=0;i<events_count;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++)
- {
- Event* j_event = events[j];
- //i_event and j_event are from the same instance, j_event is send event and
- //i_event < j_event
- if(i_event->get_instance()==j_event->get_instance() &&
- j_event->is_send() && i_visual_closure[j])
- {
- i_causal_closure[j] = true;
- }
- //i_event and j_event are send events of the same channel and i_event<j_event
- else if(i_event->is_send() && i_event->is_matched() &&
- j_event->is_matched() && mapper->same_channel(i_event,j_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;
- }
- }
- }
- square_closure(closure);
-}
-
-void CausalClosureInitiator::square_closure(std::vector<BoolVector*>& closure)
-{
- size_t events_count = closure.size();
- bool changed = false;
- do
- {
- for(size_t i=0; i<events_count; i++)
- for(size_t j=0; j<events_count; j++)
- if(!(*closure[i])[j] && multiply(closure,i,j))
- (*closure[i])[j] = changed = true;
- }
- while(changed);
-}
-
-bool CausalClosureInitiator::multiply(std::vector<BoolVector*>& closure, size_t row, size_t column)
-{
- for(size_t index=0;index<closure.size();index++)
- {
- if((*closure[row])[index] && (*closure[index])[column])
- return true;
- }
- return false;
-}
Deleted: trunk/src/check/causal_closure_initiator.h
===================================================================
--- trunk/src/check/causal_closure_initiator.h 2008-11-28 20:26:06 UTC (rev 122)
+++ trunk/src/check/causal_closure_initiator.h 2008-11-28 23:39:47 UTC (rev 123)
@@ -1,103 +0,0 @@
-/*
- * scstudio - Sequence Chart Studio
- * http://scstudio.sourceforge.net
- *
- * This library is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public
- * License version 2.1, as published by the Free Software Foundation.
- *
- * This library is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * Copyright (c) 2008 Jindra Babica <ba...@ma...>
- *
- * $Id$
- */
-
-#ifndef _CAUSAL_CLOSURE_INITIATOR_H
-#define _CAUSAL_CLOSURE_INITIATOR_H
-
-#include <stack>
-#include <vector>
-
-#include "data/msc.h"
-#include "check/dfs_instance_events_traverser.h"
-#include "check/visual_closure_initiator.h"
-
-typedef std::stack<Event*> EventPStack;
-
-class CausalClosureInitiator
-{
-
-protected:
-
- /**
- * Used for cleaning up attributes.
- */
- EventPStack m_modified_events;
-
- /**
- * Name of causal closure attribute.
- */
- std::string m_causal_closure_attribute;
-
- /**
- * Logically multiply closure by itself.
- */
- void square_closure(std::vector<BoolVector*>& closure);
-
- /**
- * Logical multiplication of row and column (indeces) of square matrix closure.
- */
- bool multiply(std::vector<BoolVector*>& closure, size_t row, size_t column);
-
-public:
-
- /**
- * Sets explicit names of attributes
- */
- CausalClosureInitiator(
- const std::string& causal_closure_attribute = "causal_closure")
- {
- m_causal_closure_attribute = causal_closure_attribute;
- }
-
-
- /**
- * Cleans up set attributes.
- */
- ~CausalClosureInitiator()
- {
- cleanup_attributes();
- }
-
- /**
- * Getter of causal closure attribute of e.
- */
- BoolVector& get_causal_closure(Event* e)
- {
- static BoolVector empty(1,false);
- return e->get_attribute<BoolVector>(m_causal_closure_attribute,empty);
- }
-
- /**
- * Computes causal closure.
- *
- * A visual_closure_init must be initialized - initialize method must be
- * called before.
- *
- * @param events - topologically sorted events used for visual_closure_init's initialization
- * @param visual_closure_init - initialized VisualClosureInitiator
- */
- void initialize(const EventPVector& events,
- VisualClosureInitiator& visual_closure_init, ChannelMapperPtr mapper);
-
- /**
- * Cleans up set attributes.
- */
- void cleanup_attributes();
-
-};
-#endif /* _CAUSAL_CLOSURE_INITIATOR_H */
Deleted: trunk/src/check/checker.h
===================================================================
--- trunk/src/check/checker.h 2008-11-28 20:26:06 UTC (rev 122)
+++ trunk/src/check/checker.h 2008-11-28 23:39:47 UTC (rev 123)
@@ -1,389 +0,0 @@
-/*
-* scstudio - Sequence Chart Studio
-* http://scstudio.sourceforge.net
-*
-* This library is free software; you can redistribute it and/or
-* modify it under the terms of the GNU Lesser General Public
-* License version 2.1, as published by the Free Software Foundation.
-*
-* This library is distributed in the hope that it will be useful,
-* but WITHOUT ANY WARRANTY; without even the implied warranty of
-* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
-* Lesser General Public License for more details.
-*
-* Copyright (c) 2008 Jindra Babica <ba...@ma...>
-*
-* $Id$
-*/
-
-#ifndef _CHECKER_H
-#define _CHECKER_H
-
-#include <exception>
-#include <map>
-
-#include "data/msc.h"
-#include "data/counted_ptr.h"
-
-class ChannelMapper;
-class Checker;
-class HMscChecker;
-class BMscChecker;
-
-typedef counted_ptr<ChannelMapper> ChannelMapperPtr;
-typedef counted_ptr<Checker> CheckerPtr;
-typedef counted_ptr<HMscChecker> HMscCheckerPtr;
-typedef counted_ptr<BMscChecker> BMscCheckerPtr;
-
-/**
- * Basic abstract class for all checking algorithms.
- */
-class Checker
-{
-
-public:
-
- /**
- * Removes no more needed attributes.
- *
- * Descendat of this class should remove attributes of MscElements that are no
- * more needed. This method should be called after finish of algorithm.
- */
- virtual void cleanup_attributes()=0;
-
- /**
- * Checks whether Checker supports given ChannelMapper.
- *
- * Deafult behaviour is false for all mappers, but it is neccessary to check
- * out this behaviour in individual checkers.
- */
- virtual bool is_supported(ChannelMapperPtr chm)=0;
-
- virtual ~Checker()
- {
-
- }
-};
-
-/**
-* Basic abstract class for checking algorithms of HMsc.
-*/
-class HMscChecker
-{
-
-protected:
-
- /**
- * Hidden constructor.
- */
- HMscChecker()
- {
- }
-
-public:
-
- ~HMscChecker()
- {
- }
-
- /**
- * Checks HMsc against specific property.
- *
- * Returns MscPathPtr with violating example if there is any in hmsc
- * otherwise HMscPathPtr is undefined.
- * @param hmsc - HMsc to be checked
- * @param mapper - ChannelMapper which is chosen as delivery semantic
- */
- virtual HMscPtr check(HMscPtr hmsc, ChannelMapperPtr mapper)=0;
-};
-
-/**
-* Basic abstract class for checking algorithms of BMsc.
-*/
-class BMscChecker
-{
-
-protected:
-
- /**
- * Singleton instance.
- */
- static BMscCheckerPtr m_checker;
-
-public:
-
- /**
- * Checks BMsc against specific property.
- *
- * Returns BMscPtr with violating example if there is any in bmsc otherwise
- * BMscPtr is undefined.
- * @param bmsc - BMsc to be checked
- * @param mapper - ChannelMapper which is chosen as delivery semantic
- */
- virtual BMscPtr check(BMscPtr bmsc, ChannelMapperPtr mapper)=0;
-};
-
-/**
- * Abstract class whose purpose is to decide whether two Messages belongs to the
- * same channel or not and assign to a message ID of channel which the message
- * belongs to. This class shortly defines delivery semantic.
- */
-class ChannelMapper
-{
-
-public:
-
- virtual ~ChannelMapper()
- {
-
- }
-
- /**
- * Returns true if e1's message belongs to the same channel as e2's message.
- */
- virtual bool same_channel(const Event* e1, const Event* e2) const=0;
-
- /**
- * Returns index of channel which event's message belongs into.
- *
- * @warning event must have set message
- */
- virtual size_t channel(const Event* event)=0;
-
- /**
- * Returns number of different channels mapped by this channel mapper
- */
- virtual size_t get_channel_count()=0;
-
- /**
- * Returns copy of this channel mapper without registered channels.
- *
- * Usefull if you need to have the same functionality of the original mapper,
- * but you don't want to work with all registered events by the original one.
- * This approach may increase efficiency in some cases.
- */
- virtual ChannelMapperPtr copy()=0;
-};
-
-/**
- * Basic implementation of ChannelMapper.
- */
-template<typename MessagePart>
-class GeneralMapper:public ChannelMapper
-{
-
-public:
-
- typedef std::map<MessagePart,size_t> ChannelMap;
-
-protected:
-
- /**
- * Common instance of GeneralMapper.
- */
- static counted_ptr<GeneralMapper<MessagePart> > m_instance;
-
- /**
- * Holds identificators of channels represented by MessagePart of MscMessage.
- */
- std::map<MessagePart,size_t> m_channels;
-
- /**
- * Use GeneralMapper::instance() to obtain instance of GeneralMapper
- */
- GeneralMapper(){};
-
-public:
-
- /**
- * Returns true if m1 belongs to the same channel as m2.
- */
- bool same_channel(const Event* e1, const Event* e2) const
- {
- return MessagePart::same_channel(e1,e2);
- }
-
- /**
- * Returns index of channel which event's message belongs into.
- */
- size_t channel(const Event* event)
- {
- MessagePart part(event);
- typename ChannelMap::iterator i = m_channels.find(part);
- if(i==m_channels.end())
- {
- size_t id = m_channels.size();
- m_channels[part] = id;
- return id;
- }
- return i->second;
- }
-
- /**
- * Returns common instance of ChannelMapper
- */
- static counted_ptr<GeneralMapper<MessagePart> > instance()
- {
- if(m_instance.get()==NULL)
- {
- counted_ptr<GeneralMapper<MessagePart> > p(new GeneralMapper<MessagePart>());
- m_instance = p;
- }
- return m_instance;
- }
-
- /**
- * Returns number of channel registered by this channel mapper
- */
- size_t get_channel_count()
- {
- return m_channels.size();
- }
-
- /**
- * Returns copy of this channel mapper without registered channels.
- *
- * Usefull if you need to have the same functionality of the original mapper,
- * but you don't want to work with all registered events by the original one.
- */
- ChannelMapperPtr copy()
- {
- return ChannelMapperPtr(new GeneralMapper<MessagePart>());
- }
-
-};
-
-/**
- * Used in GeneralMapper template to decide whether two messages belongs to the
- * same channel (delivery semantic).
- *
- * For decision send and receive instances' labels are used.
- *
- * To see delivery semantic of this class see operator<() and same_channel()
- * methods of this class.
- */
-class SRMessagePart
-{
-
- std::string m_sender;
-
- std::string m_receiver;
-
-public:
-
- SRMessagePart(const Event* e)
- {
- m_sender = e->get_sender_label();
- m_receiver = e->get_receiver_label();
- }
-
- /**
- * Used in std::map as comparision function
- */
- bool operator<(const SRMessagePart& mp) const
- {
- int s = m_sender.compare(mp.m_sender);
- int r = m_receiver.compare(mp.m_receiver);
- return s<0 || s+r<0;
- }
-
- /**
- * Channels of message m1 and m2 are same if and only if m1 has got same
- * sender and receiver as m2.
- */
- static bool same_channel(const Event* e1, const Event* e2)
- {
- if((e1->is_send() && e2->is_send()) || (e1->is_receive() && e2->is_receive()))
- {
- return e1->get_sender_label()==e2->get_sender_label() &&
- e2->get_receiver_label()==e2->get_receiver_label();
- }
- return false;
- }
-};
-
-/**
- * Used in GeneralMapper template to decide whether two messages belongs to the
- * same channel (delivery semantic).
- *
- * For decision send and receive instances' labels and message label are used.
- *
- * To see delivery semantic of this class see operator<() and same_channel()
- * methods of this class.
- */
-class SRLMessagePart {
-
- std::string m_sender;
-
- std::string m_receiver;
-
- std::string m_label;
-
-public:
-
- SRLMessagePart(const Event* e)
- {
- m_sender = e->get_sender_label();
- m_receiver = e->get_receiver_label();
- m_label = e->get_message()->get_label();
- }
-
- bool operator<(const SRLMessagePart& mp) const
- {
- int s = m_sender.compare(mp.m_sender);
- int r = m_receiver.compare(mp.m_receiver);
- int l = m_label.compare(mp.m_label);
- return s<0 || (s==0 && (r<0 || (r==0 && l<0)));
- }
-
- /**
- * Channels of message of e1 and e2 are same if and only if e1 has got same
- * sender, receiver and label as e2.
- */
- static bool same_channel(const Event* e1,const Event* e2)
- {
- return e1->get_sender_label()==e2->get_sender_label() &&
- e1->get_receiver_label()==e2->get_receiver_label() &&
- e1->get_message()->get_label()==e2->get_message()->get_label();
- }
-};
-
-typedef GeneralMapper<SRMessagePart> SRChannelMapper;
-typedef GeneralMapper<SRLMessagePart> SRLChannelMapper;
-
-typedef counted_ptr<SRChannelMapper> SRChannelMapperPtr;
-typedef counted_ptr<SRLChannelMapper> SRLChannelMapperPtr;
-
-template <class T>
-counted_ptr<GeneralMapper<T> > GeneralMapper<T>::m_instance;
-
-enum Color
-{
- WHITE,
- GRAY,
- BLACK
-};
-
-/**
- * Trohwn when acyclic relation is required and cycle was found.
- */
-class CycleDetectedException:public std::exception
-{
- virtual const char* what() const throw()
- {
- return "Acyclic graph expected but there was found cycle";
- }
-};
-
-/**
- * Thrown when unsupported channel mapper acquired.
- */
-class UnsupportedMapperException:public std::exception
-{
- virtual const char* what() const throw()
- {
- return "Unsupported channel mapper";
- }
-};
-#endif /* _CHECKER_H */
-
Deleted: trunk/src/check/deadlock_checker.cpp
===================================================================
--- trunk/src/check/deadlock_checker.cpp 2008-11-28 20:26:06 UTC (rev 122)
+++ trunk/src/check/deadlock_checker.cpp 2008-11-28 23:39:47 UTC (rev 123)
@@ -1,184 +0,0 @@
-/*
- * scstudio - Sequence Chart Studio
- * http://scstudio.sourceforge.net
- *
- * This library is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public
- * License version 2.1, as published by the Free Software Foundation.
- *
- * This library is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * Copyright (c) 2008 Jindra Babica <ba...@ma...>
- *
- * $Id$
- */
-
-#include "dfsb_hmsc_traverser.h"
-
-
-#include "check/deadlock_checker.h"
-
-DeadlockCheckerPtr DeadlockChecker::m_instance;
-
-DeadlockFreeMarker::DeadlockFreeMarker(DeadlockListener* dl):m_dl(dl)
-{
-
-}
-
-void DeadlockFreeMarker::on_white_node_found(HMscNode* n)
-{
- bool& deadlock_free = m_dl->get_deadlock_free(n);
- deadlock_free = true;
-}
-
-DeadlockListener::DeadlockListener(
- const std::string& deadlock_free_attribute,
- const std::string& depth_attribute):
- m_current_depth(0),
- m_deadlock_free_attribute(deadlock_free_attribute),
- m_depth_attribute(depth_attribute)
- {
- m_marker = DeadlockFreeMarker(this);
- m_marker_traverser.add_white_node_found_listener(&m_marker);
- }
-
-bool& DeadlockListener::get_deadlock_free(HMscNode* node)
-{
- bool status;
- bool& deadlock_free = node->get_attribute<bool>(m_deadlock_free_attribute,false,status);
- if(status)
- {
- m_modified.push_back(node);
- }
- return deadlock_free;
-}
-
-size_t& DeadlockListener::get_depth(HMscNode* node)
-{
- return node->get_attribute<size_t>(m_depth_attribute,0);
-}
-
-void DeadlockListener::on_white_node_found(HMscNode* node)
-{
- //set depth attribute
- m_current_depth++;
- get_depth(node) = m_current_depth;
- if (dynamic_cast<ReferenceNode*> (node))
- {
- m_depths.push(m_current_depth);
- }
- //set deadlock free attribute
- bool& deadlock_free = get_deadlock_free(node);
- if (dynamic_cast<EndNode*>(node))
- {
- mark_deadlock_free(node);
- }
-}
-
-void DeadlockListener::on_node_finished(HMscNode* node)
-{
- if (dynamic_cast<ReferenceNode*> (node) ||
- dynamic_cast<StartNode*> (node))
- {
- if (!get_deadlock_free(node))
- {
- throw DeadlockException();
- }
- //this node is no more on traversing stack
- m_depths.pop();
- }
- m_current_depth--;
-}
-
-void DeadlockListener::on_gray_node_found(HMscNode* node)
-{
- //m_depths can be empty
- if (!m_depths.empty())
- {
- //depth of node is surely set (in on_white_node_found())
- size_t node_depth = get_depth(node);
- size_t top_reference_depth = m_depths.top();
- //there is some ReferenceNode on path from node to previous white HMscNode
- if (top_reference_depth >= m_current_depth)
- {
- mark_deadlock_free(node);
- }
- }
-}
-
-void DeadlockListener::mark_deadlock_free(HMscNode* node)
-{
- m_marker_traverser.traverse(node);
-}
-
-void DeadlockListener::cleanup_attributes()
-{
- while (!m_modified.empty())
- {
- m_modified.back()->remove_attribute<bool>(m_deadlock_free_attribute);
- m_modified.back()->remove_attribute<size_t>(m_depth_attribute);
- m_modified.pop_back();
- }
-}
-
-HMscPtr DeadlockChecker::create_counter_example(const MscElementPListList& path)
-{
-// InnerNodePListList::const_iterator hmscs_it;
-// HMscPtr result;
-// for (hmscs_it = path.begin(); hmscs_it != path.end(); hmscs_it++)
-// {
-// HMscPtr current_hmsc;
-// InnerNode* last_node = NULL;
-// InnerNodePList::const_iterator nodes_it;
-// for (nodes_it = hmscs_it->begin(); nodes_it != hmscs_it->end(); nodes_it++)
-// {
-// if (last_node == NULL)
-// {
-// if (dynamic_cast<ReferenceNode*> (*nodes_it) != NULL)
-// last_node = new ReferenceNode((ReferenceNode*) * nodes_it);
-// else
-// last_node = new ConnectionNode((ConnectionNode*) * nodes_it);
-// current_hmsc = new HMsc((*nodes_it)->get_owner());
-// current_hmsc->get_start()->add_successor(last_node);
-// if (!result.get())
-// result = current_hmsc;
-// }
-// else
-// {
-// last_node->add_successor(*nodes_it);
-// last_node = *nodes_it;
-// }
-// }
-// }
-// return result;
- HMscPtr example = new HMsc("counter example");
- return example;
-}
-
-HMscPtr DeadlockChecker::check(HMscPtr hmsc, ChannelMapperPtr chm)
-{
- //this will be used do show eventual counterexample
- HMscPtr p;
- DeadlockListener listener;
- DFSHMscTraverser traverser;
- traverser.add_white_node_found_listener(&listener);
- traverser.add_gray_node_found_listener(&listener);
- traverser.add_node_finished_listener(&listener);
- try
- {
- traverser.traverse(hmsc);
- }
- catch (DeadlockException)
- {
- p = create_counter_example(traverser.get_reached_elements());
- traverser.cleanup_traversing_attributes();
- }
- return p;
-}
-
-void DeadlockChecker::cleanup_attributes()
-{
-}
Deleted: trunk/src/check/deadlock_checker.h
===================================================================
--- trunk/src/check/deadlock_checker.h 2008-11-28 20:26:06 UTC (rev 122)
+++ trunk/src/check/deadlock_checker.h 2008-11-28 23:39:47 UTC (rev 123)
@@ -1,156 +0,0 @@
-/*
- * scstudio - Sequence Chart Studio
- * http://scstudio.sourceforge.net
- *
- * This library is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public
- * License version 2.1, as published by the Free Software Foundation.
- *
- * This library is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * Copyright (c) 2008 Jindra Babica <ba...@ma...>
- *
- * $Id$
- */
-
-#include <string>
-#include <stack>
-#include <exception>
-
-#include "check/checker.h"
-#include "data/msc.h"
-#include "data/counted_ptr.h"
-#include "check/dfs_hmsc_traverser.h"
-#include "check/dfsb_hmsc_traverser.h"
-
-class DeadlockChecker;
-class DeadlockListener;
-
-typedef counted_ptr<DeadlockChecker> DeadlockCheckerPtr;
-
-class DeadlockException:public std::exception
-{
-
-public:
-
- const char* what()
- {
- return "There was found deadlock in HMsc";
- }
-};
-
-class DeadlockFreeMarker:public WhiteNodeFoundListener
-{
-
- DeadlockListener* m_dl;
-
-public:
-
- DeadlockFreeMarker(DeadlockListener* dl=NULL);
-
- void on_white_node_found(HMscNode* n);
-
-};
-
-class DeadlockListener:
-public WhiteNodeFoundListener,
-public GrayNodeFoundListener,
-public NodeFinishedListener
-{
-
-protected:
-
- /**
- * Depth of last found white HMscNode in Depth First Search tree
- */
- size_t m_current_depth;
-
- /**
- * Depths of founded ReferenceNodes
- */
- std::stack<size_t> m_depths;
-
- std::string m_deadlock_free_attribute;
-
- std::string m_depth_attribute;
-
- HMscNodePList m_modified;
-
- DFSBHMscTraverser m_marker_traverser;
-
- DeadlockFreeMarker m_marker;
-
- size_t& get_depth(HMscNode* node);
-
-public:
-
- DeadlockListener(
- const std::string& deadlock_free_attribute ="dl:deadlock_free",
- const std::string& depth_attribute ="dl:depth");
-
- void on_white_node_found(HMscNode* node);
-
- void on_node_finished(HMscNode* node);
-
- void on_gray_node_found(HMscNode* node);
-
- void mark_deadlock_free(HMscNode* node);
-
- void cleanup_attributes();
-
- bool& get_deadlock_free(HMscNode* node);
-
- ~DeadlockListener()
- {
- cleanup_attributes();
- }
-};
-
-class DeadlockChecker: public Checker, public HMscChecker
-{
-
-protected:
-
- /**
- * Common instance.
- */
- static DeadlockCheckerPtr m_instance;
-
- DeadlockChecker(){};
-
- HMscPtr create_counter_example(const MscElementPListList& path);
-
-public:
-
- /**
- * Checks whether hmsc satisfy deadlock free property.
- */
- HMscPtr check(HMscPtr hmsc, ChannelMapperPtr chm);
-
- /**
- * Cleans up no more needed attributes.
- */
- void cleanup_attributes();
-
- /**
- * Supports all mappers
- */
- bool is_supported(ChannelMapperPtr chm)
- {
- return true;
- }
-
- ~DeadlockChecker(){}
-
- static DeadlockCheckerPtr instance()
- {
- if(!m_instance.get())
- m_instance = new DeadlockChecker();
- return m_instance;
- }
-
- };
-
Deleted: trunk/src/check/dfs_area_traverser.cpp
===================================================================
--- trunk/src/check/dfs_area_traverser.cpp 2008-11-28 20:26:06 UTC (rev 122)
+++ trunk/src/check/dfs_area_traverser.cpp 2008-11-28 23:39:47 UTC (rev 123)
@@ -1,89 +0,0 @@
-/*
- * scstudio - Sequence Chart Studio
- * http://scstudio.sourceforge.net
- *
- * This library is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public
- * License version 2.1, as published by the Free Software Foundation.
- *
- * This library is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * Copyright (c) 2008 Jindra Babica <ba...@ma...>
- *
- * $Id$
- */
-
-#include "check/dfs_area_traverser.h"
-
-DFSAreaTraverser::DFSAreaTraverser(const std::string& color):
-DFSEventsTraverser(color)
-{
-
-}
-
-void DFSAreaTraverser::traverse_area(EventArea* area)
-{
- if(!area) return;
- StrictOrderArea* strict = dynamic_cast<StrictOrderArea*>(area);
- if(strict)
- {
- if(!strict->is_empty())
- traverse_strict_event(strict->get_first().get());
- }
- else
- {
- CoregionArea* coregion = dynamic_cast<CoregionArea*>(area);
- const CoregionEventPSet& minimals = coregion->get_minimal_events();
- CoregionEventPSet::const_iterator min;
- for(min=minimals.begin(); min!=minimals.end(); min++)
- traverse_coregion_event(*min);
- }
-}
-
-void DFSAreaTraverser::traverse(BMscPtr bmsc)
-{
- InstancePtrList::const_iterator instance;
- const InstancePtrList& instances = bmsc->get_instances();
- for(instance=instances.begin(); instance!=instances.end(); instance++)
- {
- EventArea* area = (*instance)->get_first().get();
- while(area)
- {
- traverse_area(area);
- area = area->get_next().get();
- }
- }
- cleanup_traversing_attributes();
-}
-
-void DFSAreaTraverser::traverse_coregion_event(CoregionEvent* event)
-{
- m_reached_elements.push_back(event);
- if(!is_processed(event))
- {
- const CoregEventRelPtrSet& successors = event->get_successors();
- CoregEventRelPtrSet::const_iterator successor;
- for(successor=successors.begin(); successor!=successors.end(); successor++)
- {
- m_reached_elements.push_back((*successor).get());
- traverse_coregion_event((*successor)->get_successor());
- m_reached_elements.pop_back();
- }
- event_finished(event);
- }
-}
-
-void DFSAreaTraverser::traverse_strict_event(StrictEvent* event)
-{
- m_reached_elements.push_back(event);
- if(!is_processed(event))
- {
- if(event->get_successor().get())
- traverse_strict_event(event->get_successor().get());
- event_finished(event);
- }
-}
-
Deleted: trunk/src/check/dfs_area_traverser.h
===================================================================
--- trunk/src/check/dfs_area_traverser.h 2008-11-28 20:26:06 UTC (rev 122)
+++ trunk/src/check/dfs_area_traverser.h 2008-11-28 23:39:47 UTC (rev 123)
@@ -1,55 +0,0 @@
-/*
- * scstudio - Sequence Chart Studio
- * http://scstudio.sourceforge.net
- *
- * This library is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public
- * License version 2.1, as published by the Free Software Foundation.
- *
- * This library is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * Copyright (c) 2008 Jindra Babica <ba...@ma...>
- *
- * $Id$
- */
-
-#ifndef _DFS_AREA_TRAVERSER_H
-#define _DFS_AREA_TRAVERSER_H
-
-#include "check/dfs_instance_events_traverser.h"
-
-/**
- * Processes EventAreas' events in sequence and do not follow matching events
- * during traversing.
- *
- * Single EventAreas are traversed in depth first search manner.
- */
-class DFSAreaTraverser:public DFSEventsTraverser
-{
-
-public:
-
- DFSAreaTraverser(const std::string& color="color");
-
- void traverse(BMscPtr bmsc);
-
-protected:
-
- void traverse_area(EventArea* area);
-
- /**
- * Doesn't continue in traversing next EventArea in case of event hasn't got
- * any successors.
- */
- void traverse_coregion_event(CoregionEvent* event);
-
- void traverse_strict_event(StrictEvent* event);
-
-};
-
-
-#endif /* _DFS_AREA_TRAVERSER_H */
-
Deleted: trunk/src/check/dfs_bmsc_graph_traverser.cpp
===================================================================
--- trunk/src/check/dfs_bmsc_graph_traverser.cpp 2008-11-28 20:26:06 UTC (rev 122)
+++ trunk/src/check/dfs_bmsc_graph_traverser.cpp 2008-11-28 23:39:47 UTC (rev 123)
@@ -1,222 +0,0 @@
-/*
- * scstudio - Sequence Chart Studio
- * http://scstudio.sourceforge.net
- *
- * This library is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public
- * License version 2.1, as published by the Free Software Foundation.
- *
- * This library is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * Copyright (c) 2008 Jindra Babica <ba...@ma...>
- *
- * $Id$
- */
-
-#include <stack>
-
-#include "check/dfs_bmsc_graph_traverser.h"
-
-void DFSListenersContainer::white_node_found(HMscNode* n)
-{
- WhiteNodeFoundListenerPList::iterator l;
- for(l=m_white_node_found_listeners.begin();l!=m_white_node_found_listeners.end();l++)
- (*l)->on_white_node_found(n);
-}
-
-void DFSListenersContainer::gray_node_found(HMscNode* n)
-{
- GrayNodeFoundListenerPList::iterator l;
- for(l=m_gray_node_found_listeners.begin();l!=m_gray_node_found_listeners.end();l++)
- (*l)->on_gray_node_found(n);
-}
-
-void DFSListenersContainer::black_node_found(HMscNode* n)
-{
- BlackNodeFoundListenerPList::iterator l;
- for(l=m_black_node_found_listeners.begin();l!=m_black_node_found_listeners.end();l++)
- (*l)->on_black_node_found(n);
-}
-
-void DFSListenersContainer::node_finished(HMscNode* n)
-{
- NodeFinishedListenerPList::iterator l;
- for(l=m_node_finished_listeners.begin();l!=m_node_finished_listeners.end();l++)
- (*l)->on_node_finished(n);
-}
-
-DFSListenersContainer::~DFSListenersContainer()
-{
-
-}
-
-DFSBMscGraphTraverser::~DFSBMscGraphTraverser()
-{
- cleanup_traversing_attributes();
-}
-
-void DFSBMscGraphTraverser::traverse(HMscPtr hmsc)
-{
- push_top_attributes();
- traverse_node(hmsc->get_start().get());
- cleanup_traversing_attributes();
-}
-
-void DFSBMscGraphTraverser::traverse(HMscNode* node)
-{
- push_top_attributes();
- traverse_node(node);
- cleanup_traversing_attributes();
-}
-
-bool DFSBMscGraphTraverser::traverse_node(HMscNode* node)
-{
- m_reached_elements.back().push_back(node);
- if(is_processed(node))
- {
- return false;
- }
- white_node_found(node);
- ReferenceNode* ref_node = dynamic_cast<ReferenceNode*>(node);
- bool ending_successors;
- if(ref_node!=NULL)
- {
- ending_successors = traverse_reference_node(ref_node);
- }
- else
- {
- ConnectionNode* conn_node = dynamic_cast<ConnectionNode*>(node);
- if(conn_node)
- {
- ending_successors = traverse_successors(conn_node);
- }
- else
- {
- StartNode* start_node = dynamic_cast<StartNode*>(node);
- if(start_node)
- {
- ending_successors = traverse_successors(start_node);
- }
- else
- {
- //node is supposed to be EndNode
- ending_successors = true;
- }
- }
- }
- node_finished(node);
- return ending_successors;
-}
-
-bool DFSBMscGraphTraverser::traverse_reference_node(ReferenceNode* ref_node)
-{
- HMscPtr hmsc = ref_node->get_hmsc();
- bool inner = true;
- if(hmsc.get()!=NULL)
- {
- //this line ensures (yet another one) that HMsc will be traversed as many times
- //as it is referenced
- push_top_attributes();
- //node's successors aren't traversed if end node wasn't found in hmsc
- inner = traverse_node(hmsc->get_start().get());
- //this line ensures (yet another one) that HMsc will traversed as many times
- //as it is referenced
- cleanup_top_attributes();
- }
- return inner && traverse_successors(ref_node);
-}
-
-bool DFSBMscGraphTraverser::traverse_successors(PredecessorNode* predecessor)
-{
- bool end_found = false;
- NodeRelationPtrSet::const_iterator relation;
- for(relation=predecessor->get_successors().begin();
- relation!=predecessor->get_successors().end();relation++)
- {
- const NodeRelationPtr& rel = *relation;
- m_reached_elements.back().push_back(rel.get());
- end_found = traverse_node(dynamic_cast<HMscNode*>(rel->get_successor())) || end_found;
- m_reached_elements.back().pop_back();
- }
- return end_found;
-}
-
-bool DFSBMscGraphTraverser::is_processed(HMscNode* node)
-{
- Color c = get_color(node);
- if(c==BLACK)
- {
- black_node_found(node);
- return true;
- }
- if(c==GRAY)
- {
- gray_node_found(node);
- return true;
- }
- return false;
-}
-
-void DFSBMscGraphTraverser::cleanup_traversing_attributes()
-{
- while(!m_colored_nodes.empty())
- {
- cleanup_top_attributes();
- }
-}
-
-void DFSBMscGraphTraverser::white_node_found(HMscNode* n)
-{
- DFSListenersContainer::white_node_found(n);
- set_color(n,GRAY);
-}
-
-void DFSBMscGraphTraverser::gray_node_found(HMscNode* n)
-{
- DFSListenersContainer::gray_node_found(n);
- m_reached_elements.back().pop_back();
-}
-
-void DFSBMscGraphTraverser::black_node_found(HMscNode* n)
-{
- DFSListenersContainer::black_node_found(n);
- m_reached_elements.back().pop_back();
-}
-
-void DFSBMscGraphTraverser::node_finished(HMscNode* n)
-{
- DFSListenersContainer::node_finished(n);
- m_reached_elements.back().pop_back();
- set_color(n,BLACK);
-}
-
-void DFSBMscGraphTraverser::cleanup_top_attributes()
-{
- HMscNodePList& top = m_colored_nodes.back();
- HMscNodePList::iterator event;
- for(event=top.begin();event!=top.end();event++)
- (*event)->remove_attribute<Color>(m_color_attribute);
- m_colored_nodes.pop_back();
- m_reached_elements.pop_back();
-}
-
-void DFSBMscGraphTraverser::push_top_attributes()
-{
- m_colored_nodes.push_back(HMscNodePList());
- m_reached_elements.push_back(MscElementPList());
-}
-
-Color DFSBMscGraphTraverser::get_color(HMscNode* n)
-{
- bool just_set;
- Color c = n->get_attribute<Color>(m_color_attribute,WHITE,just_set);
- if(just_set)
- {
- m_colored_nodes.back().push_back(n);
- }
- return c;
-}
-
Deleted: trunk/src/check/dfs_bmsc_graph_traverser.h
===================================================================
--- trunk/src/check/dfs_bmsc_graph_traverser.h 2008-11-28 20:26:06 UTC (rev 122)
+++ trunk/src/check/dfs_bmsc_graph_traverser.h 2008-11-28 23:39:47 UTC (rev 123)
@@ -1,465 +0,0 @@
-/*
- * scstudio - Sequence Chart Studio
- * http://scstudio.sourceforge.net
- *
- * This library is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public
- * License version 2.1, as published by the Free Software Foundation.
- *
- * This library is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * Copyright (c) 2008 Jindra Babica <ba...@ma...>
- *
- * $Id$
- */
-
-#ifndef _DFS_MSC_GRAPH_TRAVERSER_H
-#define _DFS_MSC_GRAPH_TRAVERSER_H
-
-#include<stack>
-
-#include "data/msc.h"
-#include "check/checker.h"
-
-typedef std::list<HMscNode*> HMscNodePList;
-typedef std::list<HMscNodePList> HMscNodePListList;
-typedef std::list<MscElement*> MscElementPList;
-typedef std::list<MscElementPList> MscElementPListList;
-
-
-/**
- * Listener of founded white HMscNode
- */
-class WhiteNodeFoundListener
-{
-public:
-
- virtual ~WhiteNodeFoundListener()
- {
-
- }
-
- virtual void on_white_node_found(HMscNode* n)=0;
-};
-
-/**
- * Listener of founded gray HMscNode
- */
-class GrayNodeFoundListener
-{
-public:
-
- virtual ~GrayNodeFoundListener()
- {
-
- }
-
- virtual void on_gray_node_found(HMscNode* n)=0;
-};
-
-/**
- * Listener of founded black HMscNode
- */
-class BlackNodeFoundListener
-{
-public:
-
- virtual ~BlackNodeFoundListener()
- {
-
- }
-
- virtual void on_black_node_found(HMscNode* n)=0;
-};
-
-/**
- * Listener of finished HMscNode
- */
-class NodeFinishedListener
-{
-public:
-
- virtual ~NodeFinishedListener()
- {
-
- }
-
- virtual void on_node_finished(HMscNode* node)=0;
-};
-
-/**
- * Auxiliary listener of founded white HMscNode.
- *
- * Extend this listener to process only ReferenceNodes during traversing.
- */
-class WhiteRefNodeFoundListener:public WhiteNodeFoundListener
-{
-public:
-
- virtual ~WhiteRefNodeFoundListener()
- {
-
- }
-
- virtual void on_white_node_found(HMscNode* n){
- ReferenceNode* ref = dynamic_cast<ReferenceNode*>(n);
- if(ref!=NULL)
- {
- on_white_node_found(ref);
- }
- }
-
- virtual void on_white_node_found(ReferenceNode* n)=0;
-};
-
-/**
- * Auxiliary listener of founded gray HMscNode.
- *
- * Extend this listener to process only ReferenceNodes during traversing.
- */
-class GrayRefNodeFoundListener:public GrayNodeFoundListener
-{
-public:
-
- virtual ~GrayRefNodeFoundListener()
- {
-
- }
-
- virtual void on_gray_node_found(HMscNode* n){
- Ref...
[truncated message content] |