[Scstudio-commits] SF.net SVN: scstudio:[245] trunk/src

[<got...@us...>]

Revision: 245
          http://scstudio.svn.sourceforge.net/scstudio/?rev=245&view=rev
Author:   gotthardp
Date:     2009-05-05 12:03:16 +0000 (Tue, 05 May 2009)

Log Message:
-----------
Feature request #2557089 implemented: Generic checker for BMSC in HMSC is now available. FIFO and Acyclic properties are now checked also for HMSC and Race preconditions were fixed.

Modified Paths:
--------------
    trunk/src/check/order/acyclic_checker.h
    trunk/src/check/order/fifo_checker.h
    trunk/src/check/race/race_checker.cpp
    trunk/src/data/CMakeLists.txt

Added Paths:
-----------
    trunk/src/data/hmsc_reference_checker.h

Modified: trunk/src/check/order/acyclic_checker.h
===================================================================
--- trunk/src/check/order/acyclic_checker.h	2009-05-03 19:13:46 UTC (rev 244)
+++ trunk/src/check/order/acyclic_checker.h	2009-05-05 12:03:16 UTC (rev 245)
@@ -19,6 +19,7 @@
 #include "data/checker.h"
 #include "data/msc.h"
 #include "data/dfs_events_traverser.h"
+#include "data/hmsc_reference_checker.h"
 #include "check/order/export.h"
 
 class AcyclicChecker;
@@ -38,7 +39,8 @@
   
 };
 
-class SCORDER_EXPORT AcyclicChecker: public Checker, public BMscChecker
+class SCORDER_EXPORT AcyclicChecker
+  : public Checker, public BMscChecker, public HMscReferenceChecker<AcyclicChecker>
 {
   
 protected:

Modified: trunk/src/check/order/fifo_checker.h
===================================================================
--- trunk/src/check/order/fifo_checker.h	2009-05-03 19:13:46 UTC (rev 244)
+++ trunk/src/check/order/fifo_checker.h	2009-05-05 12:03:16 UTC (rev 245)
@@ -25,6 +25,7 @@
 #include "data/msc.h"
 #include "data/checker.h"
 #include "check/pseudocode/visual_closure_initiator.h"
+#include "data/hmsc_reference_checker.h"
 #include "check/order/export.h"
 
 class FifoChecker;
@@ -32,7 +33,8 @@
 typedef std::stack<Event*> EventPStack;
 typedef boost::shared_ptr<FifoChecker> FifoCheckerPtr;
 
-class SCORDER_EXPORT FifoChecker: public Checker, public BMscChecker
+class SCORDER_EXPORT FifoChecker
+  : public Checker, public BMscChecker, public HMscReferenceChecker<FifoChecker>
 {
   
 protected:

Modified: trunk/src/check/race/race_checker.cpp
===================================================================
--- trunk/src/check/race/race_checker.cpp	2009-05-03 19:13:46 UTC (rev 244)
+++ trunk/src/check/race/race_checker.cpp	2009-05-05 12:03:16 UTC (rev 245)
@@ -251,13 +251,8 @@
     result.push_back(CheckerPrecondition(L"Livelock Free", PP_REQUIRED));
   }
 
-  // FIXME: Acylic and FIFO cannot check HMSC (bug #2557089)
-  BMscPtr bmsc = boost::dynamic_pointer_cast<BMsc>(msc);
-  if(bmsc != NULL)
-  {
-    result.push_back(CheckerPrecondition(L"Acyclic", PP_REQUIRED));
-    result.push_back(CheckerPrecondition(L"FIFO", PP_REQUIRED));
-  }
+  result.push_back(CheckerPrecondition(L"Acyclic", PP_REQUIRED));
+  result.push_back(CheckerPrecondition(L"FIFO", PP_REQUIRED));
 
   return result;
 }

Modified: trunk/src/data/CMakeLists.txt
===================================================================
--- trunk/src/data/CMakeLists.txt	2009-05-03 19:13:46 UTC (rev 244)
+++ trunk/src/data/CMakeLists.txt	2009-05-05 12:03:16 UTC (rev 245)
@@ -25,6 +25,7 @@
   dfs_bmsc_graph_traverser.cpp
   dfs_bmsc_graph_traverser.h
   time.h
+  hmsc_reference_checker.h
 )
 
 # build import-export formatters

Added: trunk/src/data/hmsc_reference_checker.h
===================================================================
--- trunk/src/data/hmsc_reference_checker.h	                        (rev 0)
+++ trunk/src/data/hmsc_reference_checker.h	2009-05-05 12:03:16 UTC (rev 245)
@@ -0,0 +1,114 @@
+/*
+ * 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) 2009 Petr Gotthard <pet...@ce...>
+ *
+ * $Id$
+ */
+
+#ifndef _HMSC_REFERENCE_CHECKER_H
+#define _HMSC_REFERENCE_CHECKER_H
+
+#include "data/checker.h"
+#include "data/dfs_hmsc_traverser.h"
+#include "check/pseudocode/msc_duplicators.h"
+
+/**
+ * Represents a property violation in a BMSC referenced from a given reference node.
+ */
+class ReferenceException
+{
+public:
+  ReferenceException(ReferenceNodePtr reference, BMscPtr counterexample)
+    : m_reference(reference), m_counterexample(counterexample)
+  { }
+
+  ReferenceNodePtr get_reference() const
+  {
+    return m_reference;
+  }
+
+  BMscPtr get_counterexample() const
+  {
+    return m_counterexample;
+  }
+
+private:
+  ReferenceNodePtr m_reference;
+  BMscPtr m_counterexample;
+};
+
+/**
+ * Walks through all references in HMSC and invokes a given checker.
+ */
+class ReferenceWalker:public WhiteNodeFoundListener
+{
+public:
+  ReferenceWalker(BMscChecker* bmsc_checker, ChannelMapperPtr mapper)
+    : m_checker(bmsc_checker), m_mapper(mapper)
+  { }
+
+  void on_white_node_found(HMscNode* node)
+  {
+    ReferenceNodePtr reference_node = dynamic_cast<ReferenceNode*>(node);
+    if(reference_node != NULL)
+    {
+      BMscPtr bmsc = reference_node->get_bmsc();
+      BMscPtr counterexample = m_checker->check(bmsc, m_mapper);
+      if(counterexample != NULL)
+        throw ReferenceException(reference_node, counterexample);
+    }
+  }
+
+private:
+  BMscChecker* m_checker;
+  ChannelMapperPtr m_mapper;
+};
+
+/**
+ * Abstract checker that verifies a property against every BMsc in HMsc.
+ */
+template <class BMSC_CHECKER>
+class HMscReferenceChecker: public HMscChecker
+{
+public:
+  HMscPtr check(HMscPtr hmsc, ChannelMapperPtr chm)
+  {
+    HMscPtr example;
+
+    DFSBMscGraphTraverser traverser;
+    // the descendant is expected to be BMscChecker
+    ReferenceWalker walker(dynamic_cast<BMSC_CHECKER*>(this), chm);
+    traverser.add_white_node_found_listener(&walker);
+    try
+    {
+      traverser.traverse(hmsc);
+    }
+    catch (ReferenceException &error)
+    {
+      HMscPathDuplicator duplicator;
+      example = duplicator.duplicate_path(traverser.get_reached_elements());
+
+      MscElementPtr element = duplicator.get_copy(error.get_reference().get());
+      ReferenceNodePtr reference = boost::dynamic_pointer_cast<ReferenceNode>(element);
+      reference->set_marked(true);
+      reference->set_msc(error.get_counterexample());
+    }
+
+    return example;
+  }
+};
+
+#endif /* _HMSC_REFERENCE_CHECKER_H */
+
+// $Id$


Property changes on: trunk/src/data/hmsc_reference_checker.h
___________________________________________________________________
Added: svn:keywords
   + Id
Added: svn:eol-style
   + native


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.