From 2ce145745a3c20c5493ee06db9876eb33936d57e Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Sat, 14 Oct 2017 15:41:18 +0200 Subject: [PATCH] parameters from rewards are now also collected in wellformedness analysis --- src/storm/analysis/GraphConditions.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/storm/analysis/GraphConditions.cpp b/src/storm/analysis/GraphConditions.cpp index be8073bf7..663bf2b52 100644 --- a/src/storm/analysis/GraphConditions.cpp +++ b/src/storm/analysis/GraphConditions.cpp @@ -35,6 +35,8 @@ namespace storm { void ConstraintCollector::wellformedRequiresNonNegativeEntries(std::vector const& vec) { for(auto const& entry : vec) { if (!storm::utility::isConstant(entry)) { + auto const& transitionVars = entry.gatherVariables(); + variableSet.insert(transitionVars.begin(), transitionVars.end()); if (entry.denominator().isConstant()) { if (entry.denominatorAsNumber() > 0) { wellformedConstraintSet.emplace(entry.nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ);