added constants, added custom iterator to variable set

Former-commit-id: 8f4a1d6aec

src/storage/jani/AutomatonComposition.cpp

@@ -0,0 +1,23 @@
+#include "src/storage/jani/AutomatonComposition.h"
+
+namespace storm {
+    namespace jani {
+        
+        AutomatonComposition::AutomatonComposition(std::string const& name) : name(name) {
+            // Intentionally left empty.
+        }
+        
+        boost::any AutomatonComposition::accept(CompositionVisitor& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
+        }
+        
+        std::string const& AutomatonComposition::getAutomatonName() const {
+            return name;
+        }
+        
+        void AutomatonComposition::write(std::ostream& stream) const {
+            stream << name;
+        }
+        
+    }
+}

src/storage/jani/AutomatonComposition.h

@@ -0,0 +1,30 @@
+#pragma once
+
+#include "src/storage/jani/Composition.h"
+
+namespace storm {
+    namespace jani {
+        
+        class AutomatonComposition : public Composition {
+        public:
+            /*!
+             * Creates a reference to an automaton to be used in a composition.
+             */
+            AutomatonComposition(std::string const& name);
+            
+            /*!
+             * Retrieves the name of the automaton this composition element refers to.
+             */
+            std::string const& getAutomatonName() const;
+            
+            virtual boost::any accept(CompositionVisitor& visitor, boost::any const& data) const override;
+            
+            virtual void write(std::ostream& stream) const override;
+            
+        private:
+            // The name of the automaton this composition element refers to.
+            std::string name;
+        };
+        
+    }
+}

src/storage/jani/Composition.cpp

@@ -0,0 +1,12 @@
+#include "src/storage/jani/Composition.h"
+
+namespace storm {
+    namespace jani {
+        
+        std::ostream& operator<<(std::ostream& stream, Composition const& composition) {
+            composition.write(stream);
+            return stream;
+        }
+        
+    }
+}

src/storage/jani/Composition.h

@@ -0,0 +1,20 @@
+#pragma once
+
+#include <ostream>
+
+#include "src/storage/jani/CompositionVisitor.h"
+
+namespace storm {
+    namespace jani {
+        
+        class Composition {
+        public:
+            virtual boost::any accept(CompositionVisitor& visitor, boost::any const& data) const = 0;
+            
+            virtual void write(std::ostream& stream) const = 0;
+            
+            friend std::ostream& operator<<(std::ostream& stream, Composition const& composition);
+        };
+        
+    }
+}

src/storage/jani/CompositionVisitor.cpp

@@ -0,0 +1,27 @@
+#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;
+        }
+        
+    }
+}

src/storage/jani/CompositionVisitor.h

@@ -0,0 +1,21 @@
+#pragma once
+
+#include <boost/any.hpp>
+
+namespace storm {
+    namespace jani {
+        
+        class AutomatonComposition;
+        class RenameComposition;
+        class ParallelComposition;
+        
+        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);
+        };
+        
+    }
+}

src/storage/jani/Constant.cpp

@@ -0,0 +1,35 @@
+#include "src/storage/jani/Constant.h"
+
+namespace storm {
+    namespace jani {
+        
+        Constant::Constant(std::string const& name, boost::optional<storm::expressions::Expression> const& expression) : name(name), expression(expression) {
+            // Intentionally left empty.
+        }
+        
+        bool Constant::isDefined() const {
+            return static_cast<bool>(expression);
+        }
+        
+        void Constant::define(storm::expressions::Expression const& expression) {
+            this->expression = expression;
+        }
+        
+        storm::expressions::Type const& Constant::getType() const {
+            return variable.getType();
+        }
+        
+        bool Constant::isBooleanConstant() const {
+            return getType().isBooleanType();
+        }
+        
+        bool Constant::isIntegerConstant() const {
+            return getType().isIntegerType();
+        }
+        
+        bool Constant::isRealConstant() const {
+            return getType().isRationalType();
+        }
+        
+    }
+}

src/storage/jani/Constant.h

@@ -0,0 +1,62 @@
+#pragma once
+
+#include <string>
+
+#include <boost/optional.hpp>
+
+#include "src/storage/expressions/Variable.h"
+#include "src/storage/expressions/Expression.h"
+
+namespace storm {
+    namespace jani {
+        
+        class Constant {
+        public:
+            /*!
+             * Creates a constant.
+             */
+            Constant(std::string const& name, boost::optional<storm::expressions::Expression> const& expression = boost::none);
+            
+            /*!
+             * Retrieves whether the constant is defined in the sense that it has a defining expression.
+             */
+            bool isDefined() const;
+            
+            /*!
+             * Defines the constant with the given expression.
+             */
+            void define(storm::expressions::Expression const& expression);
+            
+            /*!
+             * Retrieves the type of the constant.
+             */
+            storm::expressions::Type const& getType() const;
+            
+            /*!
+             * Retrieves whether the constant is a boolean constant.
+             */
+            bool isBooleanConstant() const;
+            
+            /*!
+             * Retrieves whether the constant is an integer constant.
+             */
+            bool isIntegerConstant() const;
+            
+            /*!
+             * Retrieves whether the constant is a real constant.
+             */
+            bool isRealConstant() const;
+            
+        private:
+            // The name of the constant.
+            std::string name;
+            
+            // The expression variable associated with the constant.
+            storm::expressions::Variable variable;
+
+            // The expression defining the constant (if any).
+            boost::optional<storm::expressions::Expression> expression;
+        };
+        
+    }
+}

src/storage/jani/ParallelComposition.cpp

@@ -0,0 +1,33 @@
+#include "src/storage/jani/ParallelComposition.h"
+
+#include <boost/algorithm/string/join.hpp>
+
+namespace storm {
+    namespace jani {
+        
+        ParallelComposition::ParallelComposition(std::shared_ptr<Composition> const& leftSubcomposition, std::shared_ptr<Composition> const& rightSubcomposition, std::set<std::string> const& alphabet) : leftSubcomposition(leftSubcomposition), rightSubcomposition(rightSubcomposition) {
+            // Intentionally left empty.
+        }
+        
+        Composition const& ParallelComposition::getLeftSubcomposition() const {
+            return *leftSubcomposition;
+        }
+        
+        Composition const& ParallelComposition::getRightSubcomposition() const {
+            return *rightSubcomposition;
+        }
+        
+        std::set<std::string> const& ParallelComposition::getSynchronizationAlphabet() const {
+            return alphabet;
+        }
+
+        boost::any ParallelComposition::accept(CompositionVisitor& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
+        }
+        
+        void ParallelComposition::write(std::ostream& stream) const {
+            stream << this->getLeftSubcomposition() << " |[" << boost::algorithm::join(alphabet, ", ") << "]| " << this->getRightSubcomposition();
+        }
+        
+    }
+}

src/storage/jani/ParallelComposition.h

@@ -0,0 +1,49 @@
+#pragma once
+
+#include <set>
+#include <memory>
+
+#include "src/storage/jani/Composition.h"
+
+namespace storm {
+    namespace jani {
+        
+        class ParallelComposition : public Composition {
+        public:
+            /*!
+             * Creates a parallel composition of the two subcompositions.
+             */
+            ParallelComposition(std::shared_ptr<Composition> const& leftSubcomposition, std::shared_ptr<Composition> const& rightSubcomposition, std::set<std::string> const& alphabet = {});
+            
+            /*!
+             * Retrieves the left subcomposition.
+             */
+            Composition const& getLeftSubcomposition() const;
+
+            /*!
+             * Retrieves the right subcomposition.
+             */
+            Composition const& getRightSubcomposition() const;
+
+            /*!
+             * Retrieves the alphabet of actions over which to synchronize the automata.
+             */
+            std::set<std::string> const& getSynchronizationAlphabet() const;
+            
+            virtual boost::any accept(CompositionVisitor& visitor, boost::any const& data) const override;
+            
+            virtual void write(std::ostream& stream) const override;
+            
+        private:
+            // The left subcomposition.
+            std::shared_ptr<Composition> leftSubcomposition;
+            
+            // The right subcomposition.
+            std::shared_ptr<Composition> rightSubcomposition;
+            
+            // The alphabet of actions over which to synchronize.
+            std::set<std::string> alphabet;
+        };
+        
+    }
+}

src/storage/jani/RenameComposition.cpp

@@ -0,0 +1,41 @@
+#include "src/storage/jani/RenameComposition.h"
+
+#include <vector>
+#include <sstream>
+
+#include <boost/algorithm/string/join.hpp>
+
+namespace storm {
+    namespace jani {
+        
+        RenameComposition::RenameComposition(std::shared_ptr<Composition> const& subcomposition, std::map<std::string, boost::optional<std::string>> const& renaming) : subcomposition(subcomposition), renaming(renaming) {
+            // Intentionally left empty.
+        }
+        
+        Composition const& RenameComposition::getSubcomposition() const {
+            return *subcomposition;
+        }
+        
+        boost::any RenameComposition::accept(CompositionVisitor& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
+        }
+        
+        void RenameComposition::write(std::ostream& stream) const {
+            std::vector<std::string> renamingStrings;
+            
+            for (auto const& entry : renaming) {
+                std::stringstream stream;
+                stream << entry.first << " -> ";
+                if (entry.second) {
+                    stream << entry.second;
+                } else {
+                    stream << "tau";
+                }
+            }
+            
+            stream << "(" << subcomposition << ") / {" << boost::join(renamingStrings, ", ") << "}";
+        }
+
+        
+    }
+}

src/storage/jani/RenameComposition.h

@@ -0,0 +1,42 @@
+#pragma once
+
+#include <memory>
+#include <map>
+
+#include <boost/optional.hpp>
+
+#include "src/storage/jani/Composition.h"
+
+namespace storm {
+    namespace jani {
+        
+        class RenameComposition : public Composition {
+        public:
+            RenameComposition(std::shared_ptr<Composition> const& subcomposition, std::map<std::string, boost::optional<std::string>> const& renaming = {});
+            
+            /*!
+             * Retrieves the subcomposition of this rename composition.
+             */
+            Composition const& getSubcomposition() const;
+            
+            /*!
+             * Retrieves the renaming of actions. If some action name is mapped to none, this indicates the action is to
+             * be renamed to the silent action.
+             */
+            std::map<std::string, boost::optional<std::string>> const& getRenaming() const;
+            
+            virtual boost::any accept(CompositionVisitor& visitor, boost::any const& data) const override;
+            
+            virtual void write(std::ostream& stream) const override;
+            
+        private:
+            // The subcomposition.
+            std::shared_ptr<Composition> subcomposition;
+            
+            // The renaming to perform. If one cation is mapped to none, this means that the action is to be renamed to
+            // the silent action.
+            std::map<std::string, boost::optional<std::string>> renaming;
+        };
+        
+    }
+}

src/storage/jani/VariableSet.cpp

@@ -7,6 +7,73 @@
 namespace storm {
     namespace jani {
         
+        namespace detail {
+            
+            VariableSetIterator::VariableSetIterator(VariableSet const& variableSet, boost::variant<bool_iter, bint_iter, int_iter> initialIterator) : variableSet(variableSet), it(initialIterator) {
+                // Intentionally left empty.
+            }
+            
+            VariableSetIterator& VariableSetIterator::operator++() {
+                incrementIterator();
+                return *this;
+            }
+            
+            VariableSetIterator& VariableSetIterator::operator++(int) {
+                incrementIterator();
+                return *this;
+            }
+            
+            Variable const& VariableSetIterator::operator*() {
+                if (it.which() == 0) {
+                    return *boost::get<bool_iter>(it);
+                } else if (it.which() == 1) {
+                    return *boost::get<bint_iter>(it);
+                } else {
+                    return *boost::get<int_iter>(it);
+                }
+            }
+            
+            bool VariableSetIterator::operator==(VariableSetIterator const& other) const {
+                return this->it == other.it;
+            }
+            
+            bool VariableSetIterator::operator!=(VariableSetIterator const& other) const {
+                return this->it != other.it;
+            }
+            
+            void VariableSetIterator::incrementIterator() {
+                if (it.which() == 0) {
+                    bool_iter& tmp = boost::get<bool_iter>(it);
+                    if (tmp != variableSet.getBooleanVariables().end()) {
+                        ++tmp;
+                    } else {
+                        it = variableSet.getBoundedIntegerVariables().begin();
+                    }
+                } else if (it.which() == 1) {
+                    bint_iter& tmp = boost::get<bint_iter>(it);
+                    if (tmp != variableSet.getBoundedIntegerVariables().end()) {
+                        ++tmp;
+                    } else {
+                        it = variableSet.getUnboundedIntegerVariables().begin();
+                    }
+                } else {
+                    ++boost::get<int_iter>(it);
+                }
+            }
+            
+            IntegerVariables::IntegerVariables(VariableSet const& variableSet) : variableSet(variableSet) {
+                // Intentionally left empty.
+            }
+            
+            VariableSetIterator IntegerVariables::begin() const {
+                return VariableSetIterator(variableSet, variableSet.getBoundedIntegerVariables().begin());
+            }
+            
+            VariableSetIterator IntegerVariables::end() const {
+                return VariableSetIterator(variableSet, variableSet.getUnboundedIntegerVariables().end());
+            }
+        }
+        
         VariableSet::VariableSet() {
             // Intentionally left empty.
         }
@@ -23,6 +90,10 @@ namespace storm {
             return unboundedIntegerVariables;
         }
         
+        detail::IntegerVariables VariableSet::getIntegerVariables() const {
+            return detail::IntegerVariables(*this);
+        }
+        
         void VariableSet::addBooleanVariable(BooleanVariable const& variable) {
             STORM_LOG_THROW(!this->hasVariable(variable.getName()), storm::exceptions::WrongFormatException, "Cannot add variable with name '" << variable.getName() << "', because a variable with that name already exists.");
             booleanVariables.push_back(variable);
@@ -51,5 +122,13 @@ namespace storm {
             return it->second.get();
         }
         
+        detail::VariableSetIterator VariableSet::begin() const {
+            return detail::VariableSetIterator(*this, booleanVariables.begin());
+        }
+        
+        detail::VariableSetIterator VariableSet::end() const {
+            return detail::VariableSetIterator(*this, unboundedIntegerVariables.end());
+        }
+        
     }
 }

src/storage/jani/VariableSet.h

@@ -3,6 +3,8 @@
 #include <vector>
 #include <set>
 
+#include <boost/variant.hpp>
+
 #include "src/storage/jani/BooleanVariable.h"
 #include "src/storage/jani/UnboundedIntegerVariable.h"
 #include "src/storage/jani/BoundedIntegerVariable.h"
@@ -10,8 +12,66 @@
 namespace storm {
     namespace jani {
         
+        class VariableSet;
+        
+        namespace detail {
+            
+            class VariableSetIterator {
+            private:
+                typedef std::vector<BooleanVariable>::const_iterator bool_iter;
+                typedef std::vector<BoundedIntegerVariable>::const_iterator bint_iter;
+                typedef std::vector<UnboundedIntegerVariable>::const_iterator int_iter;
+                
+            public:
+                /*!
+                 * Creates an iterator over all variables.
+                 */
+                VariableSetIterator(VariableSet const& variableSet, boost::variant<bool_iter, bint_iter, int_iter> initialIterator);
+                
+                // Methods to advance the iterator.
+                VariableSetIterator& operator++();
+                VariableSetIterator& operator++(int);
+                
+                Variable const& operator*();
+
+                bool operator==(VariableSetIterator const& other) const;
+                bool operator!=(VariableSetIterator const& other) const;
+                
+            private:
+                // Moves the iterator to the next position.
+                void incrementIterator();
+                
+                // The underlying variable set.
+                VariableSet const& variableSet;
+
+                // The current iterator position.
+                boost::variant<bool_iter, bint_iter, int_iter> it;
+            };
+            
+            class IntegerVariables {
+            public:
+                IntegerVariables(VariableSet const& variableSet);
+                
+                /*!
+                 * Retrieves an iterator to all integer variables (bounded and unbounded) in the variable set.
+                 */
+                VariableSetIterator begin() const;
+
+                /*!
+                 * Retrieves the end iterator to all integer variables (bounded and unbounded) in the variable set.
+                 */
+                VariableSetIterator end() const;
+                
+            private:
+                // The underlying variable set.
+                VariableSet const& variableSet;
+            };
+        }
+        
         class VariableSet {
         public:
+            friend class detail::VariableSetIterator;
+            
             /*!
              * Creates an empty variable set.
              */
@@ -32,6 +92,11 @@ namespace storm {
              */
             std::vector<UnboundedIntegerVariable> const& getUnboundedIntegerVariables() const;
             
+            /*!
+             * Retrieves an iterable object to all integer (bounded and unbounded) variables in the variable set.
+             */
+            detail::IntegerVariables getIntegerVariables() const;
+            
             /*!
              * Adds the given boolean variable to this set.
              */
@@ -57,6 +122,16 @@ namespace storm {
              */
             Variable const& getVariable(std::string const& name) const;
             
+            /*!
+             * Retrieves an iterator to the variables in this set.
+             */
+            detail::VariableSetIterator begin() const;
+
+            /*!
+             * Retrieves the end iterator to the variables in this set.
+             */
+            detail::VariableSetIterator end() const;
+
         private:
             // The boolean variables in this set.
             std::vector<BooleanVariable> booleanVariables;