added proper check for undefined constants when building explicit JANI models in non-parametric mode

Former-commit-id: 95c0bfc003 [formerly 3708bf3b69]
Former-commit-id: e5bbd290f3

src/builder/DdJaniModelBuilder.cpp

@@ -418,7 +418,7 @@ namespace storm {
             
             // Iterate over all assignments (boolean and integer) and build the DD for it.
             std::set<storm::expressions::Variable> assignedVariables;
-            for (auto const& assignment : destination.getNonTransientAssignments()) {
+            for (auto const& assignment : destination.getAssignments().getNonTransientAssignments()) {
                 // Record the variable as being written.
                 STORM_LOG_TRACE("Assigning to variable " << variables.variableToRowMetaVariableMap->at(assignment.getExpressionVariable()).getName());
                 assignedVariables.insert(assignment.getExpressionVariable());

src/generator/JaniNextStateGenerator.cpp

@@ -22,11 +22,15 @@ namespace storm {
         }
         
         template<typename ValueType, typename StateType>
-        JaniNextStateGenerator<ValueType, StateType>::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator<ValueType, StateType>(model.getExpressionManager(), VariableInformation(model), options), model(model), rewardVariables(), hasStateActionRewards(false) {
+        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.hasDefaultComposition(), 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(!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.
+            this->checkValid();
+            this->variableInformation = VariableInformation(model);
+            
             if (this->options.isBuildAllRewardModelsSet()) {
                 for (auto const& variable : model.getGlobalVariables()) {
                     if (variable.isTransient()) {
@@ -203,8 +207,8 @@ namespace storm {
         CompressedState JaniNextStateGenerator<ValueType, StateType>::applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& destination) {
             CompressedState newState(state);
             
-            auto assignmentIt = destination.getNonTransientAssignments().begin();
-            auto assignmentIte = destination.getNonTransientAssignments().end();
+            auto assignmentIt = destination.getAssignments().getNonTransientAssignments().begin();
+            auto assignmentIte = destination.getAssignments().getNonTransientAssignments().end();
             
             // Iterate over all boolean assignments and carry them out.
             auto boolIt = this->variableInformation.booleanVariables.begin();
@@ -642,6 +646,36 @@ namespace storm {
             }
         }
         
+        template<typename ValueType, typename StateType>
+        void JaniNextStateGenerator<ValueType, StateType>::checkValid() const {
+            // If the program still contains undefined constants and we are not in a parametric setting, assemble an appropriate error message.
+#ifdef STORM_HAVE_CARL
+            if (!std::is_same<ValueType, storm::RationalFunction>::value && model.hasUndefinedConstants()) {
+#else
+            if (model.hasUndefinedConstants()) {
+#endif
+                std::vector<std::reference_wrapper<storm::jani::Constant const>> undefinedConstants = model.getUndefinedConstants();
+                std::stringstream stream;
+                bool printComma = false;
+                for (auto const& constant : undefinedConstants) {
+                    if (printComma) {
+                        stream << ", ";
+                    } else {
+                        printComma = true;
+                    }
+                    stream << constant.get().getName() << " (" << constant.get().getType() << ")";
+                }
+                stream << ".";
+                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str());
+            }
+                
+#ifdef STORM_HAVE_CARL
+            else if (std::is_same<ValueType, storm::RationalFunction>::value && !model.undefinedConstantsAreGraphPreserving()) {
+                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The input model contains undefined constants that influence the graph structure of the underlying model, which is not allowed.");
+            }
+#endif
+        }
+        
         template class JaniNextStateGenerator<double>;
 
 #ifdef STORM_HAVE_CARL

src/generator/JaniNextStateGenerator.h

@@ -100,6 +100,11 @@ namespace storm {
              */
             void buildRewardModelInformation();
             
+            /*!
+             * Checks the underlying model for validity for this next-state generator.
+             */
+            void checkValid() const;
+            
             /// The model used for the generation of next states.
             storm::jani::Model model;
             
@@ -114,4 +119,4 @@ namespace storm {
         };
         
     }
-}
+}

src/generator/PrismNextStateGenerator.cpp

@@ -27,7 +27,7 @@ namespace storm {
             STORM_LOG_THROW(!this->program.specifiesSystemComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions.");
                         
             // Only after checking validity of the program, we initialize the variable information.
-            this->checkValid(program);
+            this->checkValid();
             this->variableInformation = VariableInformation(program);
             
             if (this->options.isBuildAllRewardModelsSet()) {
@@ -75,7 +75,7 @@ namespace storm {
         }
 
         template<typename ValueType, typename StateType>
-        void PrismNextStateGenerator<ValueType, StateType>::checkValid(storm::prism::Program const& program) {
+        void PrismNextStateGenerator<ValueType, StateType>::checkValid() const {
             // If the program still contains undefined constants and we are not in a parametric setting, assemble an appropriate error message.
 #ifdef STORM_HAVE_CARL
             if (!std::is_same<ValueType, storm::RationalFunction>::value && program.hasUndefinedConstants()) {
@@ -98,7 +98,7 @@ namespace storm {
             }
 
 #ifdef STORM_HAVE_CARL
-            else if (std::is_same<ValueType, storm::RationalFunction>::value && !program.hasUndefinedConstantsOnlyInUpdateProbabilitiesAndRewards()) {
+            else if (std::is_same<ValueType, storm::RationalFunction>::value && !program.undefinedConstantsAreGraphPreserving()) {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The program contains undefined constants that appear in some places other than update probabilities and reward value expressions, which is not admitted.");
             }
 #endif

src/generator/PrismNextStateGenerator.h

@@ -27,9 +27,9 @@ namespace storm {
             
             virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}, std::vector<StateType> const& deadlockStateIndices = {}) override;
 
-            static void checkValid(storm::prism::Program const& program);
-
         private:
+            void checkValid() const;
+
             /*!
              * A delegate constructor that is used to preprocess the program before the constructor of the superclass is
              * being called. The last argument is only present to distinguish the signature of this constructor from the
@@ -93,4 +93,4 @@ namespace storm {
     }
 }
 
-#endif /* STORM_GENERATOR_PRISMNEXTSTATEGENERATOR_H_ */
+#endif /* STORM_GENERATOR_PRISMNEXTSTATEGENERATOR_H_ */

src/storage/jani/Automaton.cpp

@@ -400,5 +400,27 @@ namespace storm {
             return result;
         }
 
+        bool Automaton::containsVariablesOnlyInProbabilitiesOrTransientAssignments(std::set<storm::expressions::Variable> const& variables) const {
+            // Check initial states restriction expression.
+            if (this->hasInitialStatesRestriction()) {
+                if (this->getInitialStatesRestriction().containsVariable(variables)) {
+                    return false;
+                }
+            }
+            
+            // Check global variable definitions.
+            if (this->getVariables().containsVariablesInBoundExpressionsOrInitialValues(variables)) {
+                return false;
+            }
+            
+            // Check edges.
+            for (auto const& edge : edges) {
+                if (edge.usesVariablesInNonTransientAssignments(variables)) {
+                    return false;
+                }
+            }
+            
+            return true;
+        }
     }
-}
+}

src/storage/jani/Automaton.h

@@ -298,7 +298,13 @@ namespace storm {
              * Retrieves the action indices appearing at some edge of the automaton.
              */
             std::set<uint64_t> getUsedActionIndices() const;
-                        
+            
+            /*!
+             * Checks whether the provided variables only appear in the probability expressions or the expressions being
+             * assigned in transient assignments.
+             */
+            bool containsVariablesOnlyInProbabilitiesOrTransientAssignments(std::set<storm::expressions::Variable> const& variables) const;
+            
         private:
             /// The name of the automaton.
             std::string name;

src/storage/jani/Edge.cpp

@@ -88,7 +88,7 @@ namespace storm {
             if (!destinations.empty()) {
                 auto const& destination = *destinations.begin();
                 
-                for (auto const& assignment : destination.getTransientAssignments()) {
+                for (auto const& assignment : destination.getAssignments().getTransientAssignments()) {
                     // Check if we can lift the assignment to the edge.
                     bool canBeLifted = true;
                     for (auto const& destination : destinations) {
@@ -112,5 +112,16 @@ namespace storm {
         boost::container::flat_set<storm::expressions::Variable> const& Edge::getWrittenGlobalVariables() const {
             return writtenGlobalVariables;
         }
+        
+        bool Edge::usesVariablesInNonTransientAssignments(std::set<storm::expressions::Variable> const& variables) const {
+            for (auto const& destination : destinations) {
+                for (auto const& assignment : destination.getAssignments().getNonTransientAssignments()) {
+                    if (assignment.getAssignedExpression().containsVariable(variables)) {
+                        return true;
+                    }
+                }
+            }
+            return false;
+        }
     }
-}
+}

src/storage/jani/Edge.h

@@ -101,6 +101,11 @@ namespace storm {
              */
             void liftTransientDestinationAssignments();
             
+            /*!
+             * Checks whether the provided variables appear on the right-hand side of non-transient assignments.
+             */
+            bool usesVariablesInNonTransientAssignments(std::set<storm::expressions::Variable> const& variables) const;
+            
         private:
             /// The index of the source location.
             uint64_t sourceLocationIndex;
@@ -127,4 +132,4 @@ namespace storm {
         };
         
     }
-}
+}

src/storage/jani/EdgeDestination.cpp

@@ -26,16 +26,8 @@ namespace storm {
             this->probability = probability;
         }
         
-        storm::jani::detail::ConstAssignments EdgeDestination::getAssignments() const {
-            return assignments.getAllAssignments();
-        }
-
-        storm::jani::detail::ConstAssignments EdgeDestination::getTransientAssignments() const {
-            return assignments.getTransientAssignments();
-        }
-        
-        storm::jani::detail::ConstAssignments EdgeDestination::getNonTransientAssignments() const {
-            return assignments.getNonTransientAssignments();
+        OrderedAssignments const& EdgeDestination::getAssignments() const {
+            return assignments;
         }
         
         void EdgeDestination::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
@@ -52,4 +44,4 @@ namespace storm {
         }
         
     }
-}
+}

src/storage/jani/EdgeDestination.h

@@ -39,18 +39,8 @@ namespace storm {
             /*!
              * Retrieves the assignments to make when choosing this destination.
              */
-            storm::jani::detail::ConstAssignments getAssignments() const;
+            OrderedAssignments const& getAssignments() const;
             
-            /*!
-             * Retrieves the transient assignments to make when choosing this destination.
-             */
-            storm::jani::detail::ConstAssignments getTransientAssignments() const;
-
-            /*!
-             * Retrieves the non-transient assignments to make when choosing this destination.
-             */
-            storm::jani::detail::ConstAssignments getNonTransientAssignments() const;
-
             /*!
              * Substitutes all variables in all expressions according to the given substitution.
              */
@@ -72,4 +62,4 @@ namespace storm {
         };
         
     }
-}
+}

src/storage/jani/Model.cpp

@@ -463,5 +463,47 @@ namespace storm {
             return true;
         }
         
+        bool Model::undefinedConstantsAreGraphPreserving() const {
+            if (!this->hasUndefinedConstants()) {
+                return true;
+            }
+
+            // Gather the variables of all undefined constants.
+            std::set<storm::expressions::Variable> undefinedConstantVariables;
+            for (auto const& constant : this->getConstants()) {
+                if (!constant.isDefined()) {
+                    undefinedConstantVariables.insert(constant.getExpressionVariable());
+                }
+            }
+            
+            // Start by checking the defining expressions of all defined constants. If it contains a currently undefined
+            // constant, we need to mark the target constant as undefined as well.
+            for (auto const& constant : this->getConstants()) {
+                if (constant.isDefined()) {
+                    if (constant.getExpression().containsVariable(undefinedConstantVariables)) {
+                        undefinedConstantVariables.insert(constant.getExpressionVariable());
+                    }
+                }
+            }
+
+            // Check global variable definitions.
+            if (this->getGlobalVariables().containsVariablesInBoundExpressionsOrInitialValues(undefinedConstantVariables)) {
+                return false;
+            }
+            
+            // Check the automata.
+            for (auto const& automaton : this->getAutomata()) {
+                if (!automaton.containsVariablesOnlyInProbabilitiesOrTransientAssignments(undefinedConstantVariables)) {
+                    return false;
+                }
+            }
+            
+            // Check initial states restriction.
+            if (initialStatesRestriction.containsVariable(undefinedConstantVariables)) {
+                return false;
+            }
+            return true;
+        }
+        
     }
-}
+}

src/storage/jani/Model.h

@@ -326,6 +326,13 @@ namespace storm {
              */
             bool checkValidity(bool logdbg = true) const;
             
+            /*!
+             * Checks that undefined constants (parameters) of the model preserve the graph of the underlying model.
+             * That is, undefined constants may only appear in the probability expressions of edge destinations as well
+             * as on the right-hand sides of transient assignments.
+             */
+            bool undefinedConstantsAreGraphPreserving() const;
+            
         private:
             /// The model name.
             std::string name;

src/storage/jani/VariableSet.cpp

@@ -178,5 +178,29 @@ namespace storm {
             return result;
         }
         
+        bool VariableSet::containsVariablesInBoundExpressionsOrInitialValues(std::set<storm::expressions::Variable> const& variables) const {
+            for (auto const& booleanVariable : this->getBooleanVariables()) {
+                if (booleanVariable.hasInitExpression()) {
+                    if (booleanVariable.getInitExpression().containsVariable(variables)) {
+                        return true;
+                    }
+                }
+            }
+            for (auto const& integerVariable : this->getBoundedIntegerVariables()) {
+                if (integerVariable.hasInitExpression()) {
+                    if (integerVariable.getInitExpression().containsVariable(variables)) {
+                        return true;
+                    }
+                }
+                if (integerVariable.getLowerBound().containsVariable(variables)) {
+                    return true;
+                }
+                if (integerVariable.getUpperBound().containsVariable(variables)) {
+                    return true;
+                }
+            }
+            return false;
+        }
+        
     }
 }

src/storage/jani/VariableSet.h

@@ -173,6 +173,12 @@ namespace storm {
              */
             std::vector<std::shared_ptr<Variable const>> getTransientVariables() const;
             
+            /*!
+             * Checks whether any of the provided variables appears in bound expressions or initial values of the
+             * variables contained in this variable set.
+             */
+            bool containsVariablesInBoundExpressionsOrInitialValues(std::set<storm::expressions::Variable> const& variables) const;
+            
         private:
             /// The vector of all variables.
             std::vector<std::shared_ptr<Variable>> variables;

src/storage/prism/Program.cpp

@@ -200,7 +200,7 @@ namespace storm {
             return false;
         }
         
-        bool Program::hasUndefinedConstantsOnlyInUpdateProbabilitiesAndRewards() const {
+        bool Program::undefinedConstantsAreGraphPreserving() const {
             if (!this->hasUndefinedConstants()) {
                 return true;
             }
@@ -212,10 +212,7 @@ namespace storm {
                     undefinedConstantVariables.insert(constant.getExpressionVariable());
                 }
             }
-            
-            // Now it remains to check that the intersection of the variables used in the program with the undefined
-            // constants' variables is empty (except for the update probabilities).
-            
+                        
             // Start by checking the defining expressions of all defined constants. If it contains a currently undefined
             // constant, we need to mark the target constant as undefined as well.
             for (auto const& constant : this->getConstants()) {
@@ -226,7 +223,7 @@ namespace storm {
                 }
             }
             
-            // Now check initial value expressions of global variables.
+            // Now check initial value and range expressions of global variables.
             for (auto const& booleanVariable : this->getGlobalBooleanVariables()) {
                 if (booleanVariable.hasInitialValue()) {
                     if (booleanVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {

src/storage/prism/Program.h

@@ -94,13 +94,13 @@ namespace storm {
             bool hasUndefinedConstants() const;
 
             /*!
-             * Retrieves whether there are undefined constants appearing in any place other than the update probabilities
-             * of the commands and the reward expressions. This is to be used for parametric model checking where the
-             * parameters are only allowed to govern the probabilities, not the underlying graph of the model.
+             * Checks that undefined constants (parameters) of the model preserve the graph of the underlying model.
+             * That is, undefined constants may only appear in the probability expressions of updates as well as in the
+             * values in reward models.
              *
-             * @return True iff all undefined constants of the model only appear in update probabilities.
+             * @return True iff the undefined constants are graph-preserving. 
              */
-            bool hasUndefinedConstantsOnlyInUpdateProbabilitiesAndRewards() const;
+            bool undefinedConstantsAreGraphPreserving() const;
             
             /*!
              * Retrieves the undefined constants in the program.