implemented lifting edge-destination assignments to edges as a JANI preprocessing step

Former-commit-id: 2aea0d3eb7 [formerly 6e16d3336d]
Former-commit-id: 04843c9749

src/adapters/DereferenceIteratorAdapter.h

@@ -37,6 +37,14 @@ namespace storm {
                 return boost::make_transform_iterator(it, Dereferencer<value_type>());
             }
             
+            bool empty() const {
+                return it == ite;
+            }
+            
+            std::size_t size() const {
+                return std::distance(it, ite);
+            }
+            
         private:
             input_iterator it;
             input_iterator ite;

src/builder/DdJaniModelBuilder.cpp

@@ -1749,6 +1749,8 @@ namespace storm {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Model still contains these undefined constants: " << boost::join(strings, ", ") << ".");
             }
             
+            STORM_LOG_THROW(!model.hasTransientEdgeDestinationAssignments(), storm::exceptions::WrongFormatException, "The symbolic JANI model builder currently does not support transient edge destination assignments.");
+            
             // Determine the actions that will appear in the parallel composition.
             storm::jani::CompositionInformationVisitor visitor(model, model.getSystemComposition());
             storm::jani::CompositionInformation actionInformation = visitor.getInformation();

src/generator/JaniNextStateGenerator.cpp

@@ -25,6 +25,7 @@ namespace storm {
         JaniNextStateGenerator<ValueType, StateType>::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator<ValueType, StateType>(model.getExpressionManager(), options), model(model), rewardVariables(), hasStateActionRewards(false) {
             STORM_LOG_THROW(model.hasStandardComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions.");
             STORM_LOG_THROW(!model.hasNonGlobalTransientVariable(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support automata-local transient variables.");
+            STORM_LOG_THROW(!model.hasTransientEdgeDestinationAssignments(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support transient edge destination assignments.");
             STORM_LOG_THROW(!this->options.isBuildChoiceLabelsSet(), storm::exceptions::InvalidSettingsException, "JANI next-state generator cannot generate choice labels.");
             
             // Only after checking validity of the program, we initialize the variable information.

src/storage/SymbolicModelDescription.cpp

@@ -71,7 +71,12 @@ namespace storm {
         SymbolicModelDescription SymbolicModelDescription::preprocess(std::string const& constantDefinitionString) const {
             if (this->isJaniModel()) {
                 std::map<storm::expressions::Variable, storm::expressions::Expression> substitution = storm::utility::jani::parseConstantDefinitionString(this->asJaniModel(), constantDefinitionString);
-                return SymbolicModelDescription(this->asJaniModel().defineUndefinedConstants(substitution).substituteConstants());
+                storm::jani::Model preparedModel = this->asJaniModel().defineUndefinedConstants(substitution).substituteConstants();
+                if (preparedModel.hasTransientEdgeDestinationAssignments()) {
+                    STORM_LOG_WARN("JANI model has transient edge-destinations assignments, which are currently not supported. Trying to lift these assignments to edges rather than destinations.");
+                    preparedModel.liftTransientEdgeDestinationAssignments();
+                }
+                return SymbolicModelDescription(preparedModel);
             } else if (this->isPrismProgram()) {
                 std::map<storm::expressions::Variable, storm::expressions::Expression> substitution = storm::utility::prism::parseConstantDefinitionString(this->asPrismProgram(), constantDefinitionString);
                 return SymbolicModelDescription(this->asPrismProgram().defineUndefinedConstants(substitution).substituteConstants());

src/storage/jani/Automaton.cpp

@@ -439,5 +439,20 @@ namespace storm {
                 edge.pushAssignmentsToDestinations();
             }
         }
+        
+        bool Automaton::hasTransientEdgeDestinationAssignments() const {
+            for (auto const& edge : this->getEdges()) {
+                if (edge.hasTransientEdgeDestinationAssignments()) {
+                    return true;
+                }
+            }
+            return false;
+        }
+        
+        void Automaton::liftTransientEdgeDestinationAssignments() {
+            for (auto& edge : this->getEdges()) {
+                edge.liftTransientDestinationAssignments();
+            }
+        }
     }
 }

src/storage/jani/Automaton.h

@@ -317,6 +317,16 @@ namespace storm {
             
             void pushEdgeAssignmentsToDestinations();
             
+            /*!
+             * Retrieves whether there is any transient edge destination assignment in the automaton.
+             */
+            bool hasTransientEdgeDestinationAssignments() const;
+            
+            /*!
+             * Lifts the common edge destination assignments to edge assignments.
+             */
+            void liftTransientEdgeDestinationAssignments();
+            
         private:
             /// The name of the automaton.
             std::string name;

src/storage/jani/Edge.cpp

@@ -137,5 +137,14 @@ namespace storm {
             }
             return false;
         }
+        
+        bool Edge::hasTransientEdgeDestinationAssignments() const {
+            for (auto const& destination : this->getDestinations()) {
+                if (destination.hasTransientAssignment()) {
+                    return true;
+                }
+            }
+            return false;
+        }
     }
 }

src/storage/jani/Edge.h

@@ -116,6 +116,11 @@ namespace storm {
              */
             bool usesVariablesInNonTransientAssignments(std::set<storm::expressions::Variable> const& variables) const;
             
+            /*!
+             * Retrieves whether there is any transient edge destination assignment in the edge.
+             */
+            bool hasTransientEdgeDestinationAssignments() const;
+            
         private:
             /// The index of the source location.
             uint64_t sourceLocationIndex;

src/storage/jani/EdgeDestination.cpp

@@ -51,5 +51,9 @@ namespace storm {
             return assignments.remove(assignment);
         }
         
+        bool EdgeDestination::hasTransientAssignment() const {
+            return !assignments.getTransientAssignments().empty();
+        }
+        
     }
 }

src/storage/jani/EdgeDestination.h

@@ -53,6 +53,11 @@ namespace storm {
             bool hasAssignment(Assignment const& assignment) const;
             bool removeAssignment(Assignment const& assignment);
             
+            /*!
+             * Retrieves whether this destination has transient assignments.
+             */
+            bool hasTransientAssignment() const;
+            
         private:
             // The index of the destination location.
             uint64_t locationIndex;

src/storage/jani/Model.cpp

@@ -520,5 +520,20 @@ namespace storm {
                 automaton.pushEdgeAssignmentsToDestinations();
             }
         }
+        
+        void Model::liftTransientEdgeDestinationAssignments() {
+            for (auto& automaton : this->getAutomata()) {
+                automaton.liftTransientEdgeDestinationAssignments();
+            }
+        }
+        
+        bool Model::hasTransientEdgeDestinationAssignments() const {
+            for (auto const& automaton : this->getAutomata()) {
+                if (automaton.hasTransientEdgeDestinationAssignments()) {
+                    return true;
+                }
+            }
+            return false;
+        }
     }
 }

src/storage/jani/Model.h

@@ -17,8 +17,6 @@ namespace storm {
         
         class Exporter;
         
-        
-        
         class Model {
         public:
             friend class Exporter;
@@ -335,6 +333,16 @@ namespace storm {
              */
             bool undefinedConstantsAreGraphPreserving() const;
             
+            /*!
+             * Lifts the common edge destination assignments to edge assignments.
+             */
+            void liftTransientEdgeDestinationAssignments();
+            
+            /*!
+             * Retrieves whether there is any transient edge destination assignment in the model.
+             */
+            bool hasTransientEdgeDestinationAssignments() const;
+            
             void makeStandardJaniCompliant();
             
             /// The name of the silent action.