several convenience additions to jani data structures

src/storm/storage/jani/Assignment.cpp

@@ -37,7 +37,7 @@ namespace storm  {
         }
         
         void Assignment::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
-            this->setAssignedExpression(this->getAssignedExpression().substitute(substitution));
+            this->setAssignedExpression(this->getAssignedExpression().substitute(substitution).simplify());
         }
         
         int64_t Assignment::getLevel() const {

src/storm/storage/jani/Assignment.h

@@ -14,7 +14,8 @@ namespace storm {
              * Creates an assignment of the given expression to the given variable.
              */
             Assignment(storm::jani::Variable const& variable, storm::expressions::Expression const& expression, uint64_t index = 0);
-            
+
+            Assignment(Assignment const&) = default;
             bool operator==(Assignment const& other) const;
             
             /*!

src/storm/storage/jani/Automaton.cpp

@@ -53,6 +53,10 @@ namespace storm {
             return variables.addVariable(variable);
         }
 
+        bool Automaton::hasVariable(std::string const& name) const {
+            return variables.hasVariable(name);
+        }
+
         VariableSet& Automaton::getVariables() {
             return variables;
         }

src/storm/storage/jani/Automaton.h

@@ -79,6 +79,8 @@ namespace storm {
              * Retrieves the variables of this automaton.
              */
             VariableSet const& getVariables() const;
+
+            bool hasVariable(std::string const& name) const;
             
             /*!
              * Retrieves all expression variables used by this automaton.

src/storm/storage/jani/JSONExporter.cpp

@@ -35,6 +35,7 @@ namespace storm {
 
 
         modernjson::json buildExpression(storm::expressions::Expression const& exp,  std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables = VariableSet(), VariableSet const& localVariables = VariableSet()) {
+            STORM_LOG_TRACE("Exporting " << exp);
             return ExpressionToJson::translate(exp,  constants, globalVariables, localVariables);
         }
 

src/storm/storage/jani/Location.cpp

@@ -10,6 +10,10 @@ namespace storm {
         Location::Location(std::string const& name, std::vector<Assignment> const& transientAssignments) : name(name), assignments(transientAssignments) {
             // Intentionally left empty.
         }
+
+        Location::Location(std::string const& name, OrderedAssignments const& assignments) : name(name), assignments(assignments) {
+            // Intentionally left empty.
+        }
         
         std::string const& Location::getName() const {
             return name;

src/storm/storage/jani/Location.h

@@ -18,7 +18,8 @@ namespace storm {
              * Creates a new location.
              */
             Location(std::string const& name, std::vector<Assignment> const& transientAssignments = {});
-            
+
+            Location(std::string const& name, OrderedAssignments const& assignments);
             /*!
              * Retrieves the name of the location.
              */

src/storm/storage/jani/Model.cpp

@@ -711,7 +711,15 @@ namespace storm {
         std::vector<Automaton> const& Model::getAutomata() const {
             return automata;
         }
-        
+
+        bool Model::hasAutomaton(std::string const& name) const {
+            return automatonToIndex.find(name) != automatonToIndex.end();
+        }
+
+        void Model::replaceAutomaton(uint64_t index, Automaton const& automaton) {
+            automata[index] = automaton;
+        }
+
         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 << "'.");

src/storm/storage/jani/Model.h

@@ -245,6 +245,19 @@ namespace storm {
              */
             std::vector<Automaton> const& getAutomata() const;
 
+            /**
+             * Replaces the automaton at index with a new automaton.
+             * @param index
+             * @param newAutomaton
+             */
+            void replaceAutomaton(uint64_t index, Automaton const& newAutomaton);
+
+            /*!
+             * Rerieves whether there exists an automaton with the given name.
+             * @param name
+             * @return
+             */
+            bool hasAutomaton(std::string const& name) const;
             /*!
              * Retrieves the automaton with the given name.
              */

src/storm/storage/jani/OrderedAssignments.cpp

@@ -16,6 +16,14 @@ namespace storm {
         OrderedAssignments::OrderedAssignments(Assignment const& assignment) {
             add(assignment);
         }
+
+        OrderedAssignments OrderedAssignments::clone() const {
+            OrderedAssignments result;
+            for (auto const& assignment : allAssignments) {
+                result.add(Assignment(*assignment));
+            }
+            return result;
+        }
         
         bool OrderedAssignments::add(Assignment const& assignment) {
             // If the element is contained in this set of assignment, nothing needs to be added.

src/storm/storage/jani/OrderedAssignments.h

@@ -140,7 +140,9 @@ namespace storm {
             bool areLinear() const;
             
             friend std::ostream& operator<<(std::ostream& stream, OrderedAssignments const& assignments);
-            
+
+            OrderedAssignments clone() const;
+
         private:
             uint64_t isReadBeforeAssignment(Variable const& var, uint64_t assignmentNumber, uint64_t start = 0) const;
             uint64_t isWrittenBeforeAssignment(Variable const& var, uint64_t assignmentNumber, uint64_t start = 0) const;