From 675b7bb207ff3e5a88f1aa537bdf5d12795971b7 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 19 Sep 2016 15:13:23 +0200
Subject: [PATCH] added proper check for undefined constants when building
explicit JANI models in non-parametric mode
Former-commit-id: 95c0bfc003c7be054ccf95aa0aebe5806837360a [formerly 3708bf3b691ae9f9b4f3ae80cd2f3c33109e79ab]
Former-commit-id: e5bbd290f3412126ff39783ea478bf6708cd1947
---
src/builder/DdJaniModelBuilder.cpp | 2 +-
src/generator/JaniNextStateGenerator.cpp | 40 +++++++++++++++++++--
src/generator/JaniNextStateGenerator.h | 7 +++-
src/generator/PrismNextStateGenerator.cpp | 6 ++--
src/generator/PrismNextStateGenerator.h | 6 ++--
src/storage/jani/Automaton.cpp | 24 ++++++++++++-
src/storage/jani/Automaton.h | 8 ++++-
src/storage/jani/Edge.cpp | 15 ++++++--
src/storage/jani/Edge.h | 7 +++-
src/storage/jani/EdgeDestination.cpp | 14 ++------
src/storage/jani/EdgeDestination.h | 14 ++------
src/storage/jani/Model.cpp | 44 ++++++++++++++++++++++-
src/storage/jani/Model.h | 7 ++++
src/storage/jani/VariableSet.cpp | 24 +++++++++++++
src/storage/jani/VariableSet.h | 6 ++++
src/storage/prism/Program.cpp | 9 ++---
src/storage/prism/Program.h | 10 +++---
17 files changed, 192 insertions(+), 51 deletions(-)
diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp
index 1cdf43e15..b1cafceb2 100644
--- a/src/builder/DdJaniModelBuilder.cpp
+++ b/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());
diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp
index b3f8f6561..384a37a33 100644
--- a/src/generator/JaniNextStateGenerator.cpp
+++ b/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
diff --git a/src/generator/JaniNextStateGenerator.h b/src/generator/JaniNextStateGenerator.h
index d0b5707a6..edd345b9d 100644
--- a/src/generator/JaniNextStateGenerator.h
+++ b/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 {
};
}
-}
\ No newline at end of file
+}
diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp
index 94d7a0f0a..73e3d245e 100644
--- a/src/generator/PrismNextStateGenerator.cpp
+++ b/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
diff --git a/src/generator/PrismNextStateGenerator.h b/src/generator/PrismNextStateGenerator.h
index d2004b9d3..dcf2e3f73 100644
--- a/src/generator/PrismNextStateGenerator.h
+++ b/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_ */
\ No newline at end of file
+#endif /* STORM_GENERATOR_PRISMNEXTSTATEGENERATOR_H_ */
diff --git a/src/storage/jani/Automaton.cpp b/src/storage/jani/Automaton.cpp
index d3c68cd39..95165f991 100644
--- a/src/storage/jani/Automaton.cpp
+++ b/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;
+ }
}
-}
\ No newline at end of file
+}
diff --git a/src/storage/jani/Automaton.h b/src/storage/jani/Automaton.h
index 9df752612..8b07ad062 100644
--- a/src/storage/jani/Automaton.h
+++ b/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;
diff --git a/src/storage/jani/Edge.cpp b/src/storage/jani/Edge.cpp
index 0a06f50a8..2d5def222 100644
--- a/src/storage/jani/Edge.cpp
+++ b/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;
+ }
}
-}
\ No newline at end of file
+}
diff --git a/src/storage/jani/Edge.h b/src/storage/jani/Edge.h
index 6ce6ef127..66019e04a 100644
--- a/src/storage/jani/Edge.h
+++ b/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 {
};
}
-}
\ No newline at end of file
+}
diff --git a/src/storage/jani/EdgeDestination.cpp b/src/storage/jani/EdgeDestination.cpp
index c20a5d520..f1a1987e6 100644
--- a/src/storage/jani/EdgeDestination.cpp
+++ b/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 {
}
}
-}
\ No newline at end of file
+}
diff --git a/src/storage/jani/EdgeDestination.h b/src/storage/jani/EdgeDestination.h
index a7e3fb672..962fdec6b 100644
--- a/src/storage/jani/EdgeDestination.h
+++ b/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 {
};
}
-}
\ No newline at end of file
+}
diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp
index 5f6d3e6eb..a436abbd6 100644
--- a/src/storage/jani/Model.cpp
+++ b/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;
+ }
+
}
-}
\ No newline at end of file
+}
diff --git a/src/storage/jani/Model.h b/src/storage/jani/Model.h
index d955bb0e7..b239c7f52 100644
--- a/src/storage/jani/Model.h
+++ b/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;
diff --git a/src/storage/jani/VariableSet.cpp b/src/storage/jani/VariableSet.cpp
index 4caae4269..137c3603d 100644
--- a/src/storage/jani/VariableSet.cpp
+++ b/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;
+ }
+
}
}
diff --git a/src/storage/jani/VariableSet.h b/src/storage/jani/VariableSet.h
index 78275de0b..db8d0de6a 100644
--- a/src/storage/jani/VariableSet.h
+++ b/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;
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index 126f53c4e..f187ecc08 100644
--- a/src/storage/prism/Program.cpp
+++ b/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)) {
diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h
index bc17072e1..9e4617913 100644
--- a/src/storage/prism/Program.h
+++ b/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.