From 32dc38b48f23870b58a52b88d7be6823093e0779 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sun, 29 May 2016 18:47:06 +0200
Subject: [PATCH] some more steps towards symbolic builder for JANI models

Former-commit-id: 98cd8f61c15e4d00a8581699618a86a275857de7
---
 src/builder/DdJaniModelBuilder.cpp      | 29 +++++++++++++++++++++++++
 src/builder/DdJaniModelBuilder.h        |  6 ++++-
 src/storage/jani/CompositionVisitor.cpp | 27 -----------------------
 src/storage/jani/CompositionVisitor.h   |  7 +++---
 src/storage/jani/Model.cpp              | 22 ++++++++++++++++++-
 src/storage/jani/Model.h                | 15 +++++++++++++
 6 files changed, 73 insertions(+), 33 deletions(-)
 delete mode 100644 src/storage/jani/CompositionVisitor.cpp

diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp
index c9744d90c..623ad0187 100644
--- a/src/builder/DdJaniModelBuilder.cpp
+++ b/src/builder/DdJaniModelBuilder.cpp
@@ -119,6 +119,35 @@ namespace storm {
             this->model = this->model->substituteConstants();
         }
         
+        /*!
+         * This structure represents a subcomponent of a composition.
+         */
+        template<storm::dd::DdType Type, typename ValueType>
+        struct AutomatonDd {
+
+        };
+        
+        template <storm::dd::DdType Type, typename ValueType>
+        std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> DdJaniModelBuilder<Type, ValueType>::translate() {
+            auto system = this->model->getSystemComposition().accept(*this, boost::any());
+        }
+        
+        template <storm::dd::DdType Type, typename ValueType>
+        boost::any DdJaniModelBuilder<Type, ValueType>::visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) {
+            
+        }
+        
+        template <storm::dd::DdType Type, typename ValueType>
+        boost::any DdJaniModelBuilder<Type, ValueType>::visit(storm::jani::RenameComposition const& composition, boost::any const& data) {
+            
+        }
+        
+        template <storm::dd::DdType Type, typename ValueType>
+        boost::any DdJaniModelBuilder<Type, ValueType>::visit(storm::jani::ParallelComposition const& composition, boost::any const& data) {
+            
+        }
+
+        
         template class DdJaniModelBuilder<storm::dd::DdType::CUDD, double>;
         template class DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>;
     }
diff --git a/src/builder/DdJaniModelBuilder.h b/src/builder/DdJaniModelBuilder.h
index 983b7cd99..a3f07a21c 100644
--- a/src/builder/DdJaniModelBuilder.h
+++ b/src/builder/DdJaniModelBuilder.h
@@ -19,7 +19,7 @@ namespace storm {
     namespace builder {
         
         template <storm::dd::DdType Type, typename ValueType = double>
-        class DdJaniModelBuilder {
+        class DdJaniModelBuilder : public storm::jani::CompositionVisitor {
         public:            
             struct Options {
                 /*!
@@ -109,6 +109,10 @@ namespace storm {
              */
             storm::jani::Model const& getTranslatedModel() const;
             
+            virtual boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override;
+            virtual boost::any visit(storm::jani::RenameComposition const& composition, boost::any const& data) override;
+            virtual boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override;
+            
         private:
             /// The model to translate.
             boost::optional<storm::jani::Model> model;
diff --git a/src/storage/jani/CompositionVisitor.cpp b/src/storage/jani/CompositionVisitor.cpp
deleted file mode 100644
index 78a95ad0c..000000000
--- a/src/storage/jani/CompositionVisitor.cpp
+++ /dev/null
@@ -1,27 +0,0 @@
-#include "src/storage/jani/CompositionVisitor.h"
-
-#include "src/storage/jani/AutomatonComposition.h"
-#include "src/storage/jani/RenameComposition.h"
-#include "src/storage/jani/ParallelComposition.h"
-
-namespace storm {
-    namespace jani {
-        
-        boost::any CompositionVisitor::visit(AutomatonComposition const& composition, boost::any const& data) {
-            return data;
-        }
-        
-        boost::any CompositionVisitor::visit(RenameComposition const& composition, boost::any const& data) {
-            return composition.getSubcomposition().accept(*this, data);
-        }
-        
-        boost::any CompositionVisitor::visit(ParallelComposition const& composition, boost::any const& data) {
-            return join(composition.getLeftSubcomposition().accept(*this, data), composition.getRightSubcomposition().accept(*this, data));
-        }
-        
-        boost::any CompositionVisitor::join(boost::any const& first, boost::any const& second) {
-            return first;
-        }
-        
-    }
-}
diff --git a/src/storage/jani/CompositionVisitor.h b/src/storage/jani/CompositionVisitor.h
index 94d9bf5f5..fdf155d96 100644
--- a/src/storage/jani/CompositionVisitor.h
+++ b/src/storage/jani/CompositionVisitor.h
@@ -11,10 +11,9 @@ namespace storm {
         
         class CompositionVisitor {
         public:
-            virtual boost::any visit(AutomatonComposition const& composition, boost::any const& data);
-            virtual boost::any visit(RenameComposition const& composition, boost::any const& data);
-            virtual boost::any visit(ParallelComposition const& composition, boost::any const& data);
-            virtual boost::any join(boost::any const& first, boost::any const& second);
+            virtual boost::any visit(AutomatonComposition const& composition, boost::any const& data) = 0;
+            virtual boost::any visit(RenameComposition const& composition, boost::any const& data) = 0;
+            virtual boost::any visit(ParallelComposition const& composition, boost::any const& data) = 0;
         };
         
     }
diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp
index 5ef53fe88..ec0066ed4 100644
--- a/src/storage/jani/Model.cpp
+++ b/src/storage/jani/Model.cpp
@@ -61,7 +61,7 @@ namespace storm {
         
         uint64_t Model::getActionIndex(std::string const& name) const {
             auto it = actionToIndex.find(name);
-            STORM_LOG_THROW(it != actionToIndex.end(), storm::exceptions::WrongFormatException, "Unable to retrieve index of unknown action '" << name << "'.");
+            STORM_LOG_THROW(it != actionToIndex.end(), storm::exceptions::InvalidOperationException, "Unable to retrieve index of unknown action '" << name << "'.");
             return it->second;
         }
         
@@ -135,6 +135,18 @@ namespace storm {
             return automata;
         }
         
+        Automaton& Model::getAutomaton(std::string const& name) {
+            auto it = automatonToIndex.find(name);
+            STORM_LOG_THROW(it != automatonToIndex.end(), storm::exceptions::InvalidOperationException, "Unable to retrieve unknown automaton '" << name << "'.");
+            return automata[it->second];
+        }
+        
+        Automaton const& Model::getAutomaton(std::string const& name) const {
+            auto it = automatonToIndex.find(name);
+            STORM_LOG_THROW(it != automatonToIndex.end(), storm::exceptions::InvalidOperationException, "Unable to retrieve unknown automaton '" << name << "'.");
+            return automata[it->second];
+        }
+        
         std::shared_ptr<Composition> Model::getStandardSystemComposition() const {
             std::set<std::string> fullSynchronizationAlphabet = getActionNames(false);
             
@@ -160,6 +172,14 @@ namespace storm {
             return result;
         }
         
+        std::string const& Model::getSilentActionName() const {
+            return actions[silentActionIndex].getName();
+        }
+        
+        uint64_t Model::getSilentActionIndex() const {
+            return silentActionIndex;
+        }
+        
         Model Model::defineUndefinedConstants(std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) const {
             Model result(*this);
             
diff --git a/src/storage/jani/Model.h b/src/storage/jani/Model.h
index b1e5e3f9a..e719f6d96 100644
--- a/src/storage/jani/Model.h
+++ b/src/storage/jani/Model.h
@@ -147,6 +147,16 @@ namespace storm {
              */
             std::vector<Automaton> const& getAutomata() const;
 
+            /*!
+             * Retrieves the automaton with the given name.
+             */
+            Automaton& getAutomaton(std::string const& name);
+
+            /*!
+             * Retrieves the automaton with the given name.
+             */
+            Automaton const& getAutomaton(std::string const& name) const;
+
             /*!
              * Sets the system composition expression of the JANI model.
              */
@@ -172,6 +182,11 @@ namespace storm {
              */
             std::string const& getSilentActionName() const;
             
+            /*!
+             * Retrieves the index of the silent action.
+             */
+            uint64_t getSilentActionIndex() const;
+            
             /*!
              * Defines the undefined constants of the model by the given expressions. The original model is not modified,
              * but instead a new model is created.