From 40a982430c07401dd0162185ef51dc0ce1a325e8 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Tue, 22 Aug 2017 15:46:30 +0200
Subject: [PATCH 1/6] cmake for carl: handle situation where carl version
information is missing
Older carl versions don't provide detailed version information, so we
provide an informative error message instead of cmake syntax errors during
the comparison.
---
resources/3rdparty/CMakeLists.txt | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt
index 243c0b0e5..b4f200234 100644
--- a/resources/3rdparty/CMakeLists.txt
+++ b/resources/3rdparty/CMakeLists.txt
@@ -215,6 +215,10 @@ if(USE_CARL)
else()
message(SEND_ERROR "File ${carlLOCATION} does not exist, did you build carl?")
endif()
+ if("${carl_MINORYEARVERSION}" STREQUAL "" OR "${carl_MINORMONTHVERSION}" STREQUAL "" OR "${carl_MAINTENANCEVERSION}" STREQUAL "")
+ # don't have detailed version information, probably an old version of carl
+ message(FATAL_ERROR "Carl at ${carlLOCATION} outdated, require ${CARL_MINYEAR}.${CARL_MINMONTH}.${CARL_MINPATCH}, have ${carl_VERSION}")
+ endif()
if(${carl_MINORYEARVERSION} LESS ${CARL_MINYEAR})
message(SEND_ERROR "Carl outdated, require ${CARL_MINYEAR}.${CARL_MINMONTH}.${CARL_MINPATCH}, have ${carl_VERSION}")
elseif(${carl_MINORYEARVERSION} EQUAL ${CARL_MINYEAR})
From 50ba6866ebb0dd245f8ab1686bd77d750708f67e Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Thu, 28 Sep 2017 12:14:27 +0200
Subject: [PATCH 2/6] checking solver requirements for PLA
---
...SparseDtmcParameterLiftingModelChecker.cpp | 48 +++++++++++++++++--
.../SparseDtmcParameterLiftingModelChecker.h | 8 ++--
2 files changed, 49 insertions(+), 7 deletions(-)
diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
index 119e3791d..150a9d86c 100644
--- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
+++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
@@ -6,6 +6,8 @@
#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+#include "storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h"
+#include "storm/modelchecker/prctl/helper/BaierUpperRewardBoundsComputer.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/solver/StandardMinMaxLinearEquationSolver.h"
@@ -17,6 +19,8 @@
#include "storm/exceptions/InvalidPropertyException.h"
#include "storm/exceptions/NotSupportedException.h"
#include "storm/exceptions/UnexpectedException.h"
+#include "storm/exceptions/UncheckedRequirementException.h"
+
namespace storm {
namespace modelchecker {
@@ -27,7 +31,7 @@ namespace storm {
}
template <typename SparseModelType, typename ConstantType>
- SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseDtmcParameterLiftingModelChecker(std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>>&& solverFactory) : solverFactory(std::move(solverFactory)) {
+ SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseDtmcParameterLiftingModelChecker(std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>>&& solverFactory) : solverFactory(std::move(solverFactory)), solvingRequiresUpperRewardBounds(false) {
// Intentionally left empty
}
@@ -109,6 +113,8 @@ namespace storm {
// We know some bounds for the results so set them
lowerResultBound = storm::utility::zero<ConstantType>();
upperResultBound = storm::utility::one<ConstantType>();
+ // No requirements for bounded formulas
+ solverFactory->setRequirementsChecked(true);
}
template <typename SparseModelType, typename ConstantType>
@@ -139,6 +145,12 @@ namespace storm {
// We know some bounds for the results so set them
lowerResultBound = storm::utility::zero<ConstantType>();
upperResultBound = storm::utility::one<ConstantType>();
+
+ auto req = solverFactory->getRequirements(storm::solver::EquationSystemType::UntilProbabilities);
+ req.clearBounds();
+ req.clearNoEndComponents(); // We never have end components within the maybestates (assuming graph-preserving instantiations).
+ STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "Unchecked solver requirement.");
+ solverFactory->setRequirementsChecked(true);
}
template <typename SparseModelType, typename ConstantType>
@@ -172,6 +184,17 @@ namespace storm {
// We only know a lower bound for the result
lowerResultBound = storm::utility::zero<ConstantType>();
+
+ auto req = solverFactory->getRequirements(storm::solver::EquationSystemType::ReachabilityRewards);
+ req.clearNoEndComponents(); // We never have end components within the maybestates (assuming graph-preserving instantiations).
+ req.clearLowerBounds();
+ if (req.requiresUpperBounds()) {
+ solvingRequiresUpperRewardBounds = true;
+ req.clearUpperBounds();
+ }
+ STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "Unchecked solver requirement.");
+ solverFactory->setRequirementsChecked(true);
+
}
@@ -200,6 +223,9 @@ namespace storm {
// We only know a lower bound for the result
lowerResultBound = storm::utility::zero<ConstantType>();
+
+ // No requirements for bounded reward formula
+ solverFactory->setRequirementsChecked(true);
}
template <typename SparseModelType, typename ConstantType>
@@ -228,7 +254,23 @@ namespace storm {
}
auto solver = solverFactory->create(parameterLifter->getMatrix());
if (lowerResultBound) solver->setLowerBound(lowerResultBound.get());
- if (upperResultBound) solver->setUpperBound(upperResultBound.get());
+ if (upperResultBound) {
+ solver->setUpperBound(upperResultBound.get());
+ } else if (solvingRequiresUpperRewardBounds) {
+ // For the min-case, we use DS-MPI, for the max-case variant 2 of the Baier et al. paper (CAV'17).
+ std::vector<typename SparseModelType::ValueType> oneStepProbs;
+ oneStepProbs.reserve(parameterLifter->getMatrix().getRowCount());
+ for (uint64_t row = 0; row < parameterLifter->getMatrix().getRowCount(); ++row) {
+ oneStepProbs.push_back(storm::utility::one<typename SparseModelType::ValueType>() - parameterLifter->getMatrix().getRowSum(row));
+ }
+ if (dirForParameters == storm::OptimizationDirection::Minimize) {
+ storm::modelchecker::helper::DsMpiMdpUpperRewardBoundsComputer<typename SparseModelType::ValueType> dsmpi(parameterLifter->getMatrix(), parameterLifter->getVector(), oneStepProbs);
+ solver->setUpperBounds(dsmpi.computeUpperBounds());
+ } else {
+ storm::modelchecker::helper::BaierUpperRewardBoundsComputer<typename SparseModelType::ValueType> baier(parameterLifter->getMatrix(), parameterLifter->getVector(), oneStepProbs);
+ solver->setUpperBound(baier.computeUpperBound());
+ }
+ }
if (!stepBound) solver->setTrackScheduler(true);
if (storm::solver::minimize(dirForParameters) && minSchedChoices && !stepBound) solver->setInitialScheduler(std::move(minSchedChoices.get()));
if (storm::solver::maximize(dirForParameters) && maxSchedChoices && !stepBound) solver->setInitialScheduler(std::move(maxSchedChoices.get()));
@@ -247,7 +289,7 @@ namespace storm {
}
// Invoke the solver
- if(stepBound) {
+ if (stepBound) {
assert(*stepBound > 0);
x = std::vector<ConstantType>(maybeStates.getNumberOfSetBits(), storm::utility::zero<ConstantType>());
solver->repeatedMultiply(dirForParameters, x, ¶meterLifter->getVector(), *stepBound);
diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h
index d6f51032b..b4a8644b6 100644
--- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h
+++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h
@@ -12,7 +12,6 @@
#include "storm/solver/MinMaxLinearEquationSolver.h"
#include "storm/logic/FragmentSpecification.h"
-
namespace storm {
namespace modelchecker {
@@ -49,12 +48,13 @@ namespace storm {
storm::storage::BitVector maybeStates;
std::vector<ConstantType> resultsForNonMaybeStates;
boost::optional<uint_fast64_t> stepBound;
-
+
std::unique_ptr<storm::modelchecker::SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>> instantiationChecker;
-
+
std::unique_ptr<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>> parameterLifter;
std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>> solverFactory;
-
+ bool solvingRequiresUpperRewardBounds;
+
// Results from the most recent solver call.
boost::optional<std::vector<uint_fast64_t>> minSchedChoices, maxSchedChoices;
std::vector<ConstantType> x;
From 1396de3c5face64731f00f33f0096b41c0957c3c Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Thu, 28 Sep 2017 12:15:37 +0200
Subject: [PATCH 3/6] Enforce no end components when we want to compute a
scheduler from a minmax equation system
---
.../IterativeMinMaxLinearEquationSolver.cpp | 5 +++++
src/storm/solver/LpMinMaxLinearEquationSolver.cpp | 15 +++++++++++++++
src/storm/solver/LpMinMaxLinearEquationSolver.h | 2 ++
3 files changed, 22 insertions(+)
diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
index 0ddd5b5fe..70d2de0c1 100644
--- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
@@ -255,6 +255,11 @@ namespace storm {
// Start by copying the requirements of the linear equation solver.
MinMaxLinearEquationSolverRequirements requirements(this->linearEquationSolverFactory->getRequirements());
+ // In case we perform value iteration and need to retrieve a scheduler, end components are forbidden
+ if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration && isTrackSchedulerSet()) {
+ requirements.requireNoEndComponents();
+ }
+
// Guide requirements by whether or not we force soundness.
if (this->getSettings().getForceSoundness()) {
// Only add requirements for value iteration here as the policy iteration requirements are indifferent
diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp
index 2f360f513..0369d301d 100644
--- a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp
@@ -108,6 +108,21 @@ namespace storm {
StandardMinMaxLinearEquationSolver<ValueType>::clearCache();
}
+
+ template<typename ValueType>
+ MinMaxLinearEquationSolverRequirements LpMinMaxLinearEquationSolver<ValueType>::getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
+
+ MinMaxLinearEquationSolverRequirements requirements;
+
+ // In case we need to retrieve a scheduler, end components are forbidden
+ if (isTrackSchedulerSet()) {
+ requirements.requireNoEndComponents();
+ }
+
+ return requirements;
+ }
+
+
template<typename ValueType>
LpMinMaxLinearEquationSolverFactory<ValueType>::LpMinMaxLinearEquationSolverFactory(bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory<ValueType>(MinMaxMethodSelection::LinearProgramming, trackScheduler), lpSolverFactory(std::make_unique<storm::utility::solver::LpSolverFactory<ValueType>>()) {
// Intentionally left empty
diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.h b/src/storm/solver/LpMinMaxLinearEquationSolver.h
index a31ac710b..3e5af458f 100644
--- a/src/storm/solver/LpMinMaxLinearEquationSolver.h
+++ b/src/storm/solver/LpMinMaxLinearEquationSolver.h
@@ -18,6 +18,8 @@ namespace storm {
virtual void clearCache() const override;
+ virtual MinMaxLinearEquationSolverRequirements getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const override;
+
private:
std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>> lpSolverFactory;
};
From 96f45fe77a28faa03cdc88c55d39aef7c1f19075 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Thu, 28 Sep 2017 12:15:54 +0200
Subject: [PATCH 4/6] fixed missing return statements
---
src/storm/settings/modules/EigenEquationSolverSettings.cpp | 1 +
src/storm/settings/modules/NativeEquationSolverSettings.cpp | 1 +
2 files changed, 2 insertions(+)
diff --git a/src/storm/settings/modules/EigenEquationSolverSettings.cpp b/src/storm/settings/modules/EigenEquationSolverSettings.cpp
index 3047a13a4..e43bda28b 100644
--- a/src/storm/settings/modules/EigenEquationSolverSettings.cpp
+++ b/src/storm/settings/modules/EigenEquationSolverSettings.cpp
@@ -113,6 +113,7 @@ namespace storm {
case EigenEquationSolverSettings::LinearEquationMethod::DGMRES: out << "dgmres"; break;
case EigenEquationSolverSettings::LinearEquationMethod::SparseLU: out << "sparselu"; break;
}
+ return out;
}
} // namespace modules
diff --git a/src/storm/settings/modules/NativeEquationSolverSettings.cpp b/src/storm/settings/modules/NativeEquationSolverSettings.cpp
index d797a968a..d85b10569 100644
--- a/src/storm/settings/modules/NativeEquationSolverSettings.cpp
+++ b/src/storm/settings/modules/NativeEquationSolverSettings.cpp
@@ -120,6 +120,7 @@ namespace storm {
case NativeEquationSolverSettings::LinearEquationMethod::WalkerChae: out << "walkerchae"; break;
case NativeEquationSolverSettings::LinearEquationMethod::Power: out << "power"; break;
}
+ return out;
}
} // namespace modules
From f83dbf741bd8011052363908931bb7b1acb5b901 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 2 Oct 2017 12:02:45 +0200
Subject: [PATCH 5/6] fixed wrong template argument
---
.../region/SparseDtmcParameterLiftingModelChecker.cpp | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
index 150a9d86c..8ac2bdea8 100644
--- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
+++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
@@ -258,16 +258,16 @@ namespace storm {
solver->setUpperBound(upperResultBound.get());
} else if (solvingRequiresUpperRewardBounds) {
// For the min-case, we use DS-MPI, for the max-case variant 2 of the Baier et al. paper (CAV'17).
- std::vector<typename SparseModelType::ValueType> oneStepProbs;
+ std::vector<ConstantType> oneStepProbs;
oneStepProbs.reserve(parameterLifter->getMatrix().getRowCount());
for (uint64_t row = 0; row < parameterLifter->getMatrix().getRowCount(); ++row) {
- oneStepProbs.push_back(storm::utility::one<typename SparseModelType::ValueType>() - parameterLifter->getMatrix().getRowSum(row));
+ oneStepProbs.push_back(storm::utility::one<ConstantType>() - parameterLifter->getMatrix().getRowSum(row));
}
if (dirForParameters == storm::OptimizationDirection::Minimize) {
- storm::modelchecker::helper::DsMpiMdpUpperRewardBoundsComputer<typename SparseModelType::ValueType> dsmpi(parameterLifter->getMatrix(), parameterLifter->getVector(), oneStepProbs);
+ storm::modelchecker::helper::DsMpiMdpUpperRewardBoundsComputer<ConstantType> dsmpi(parameterLifter->getMatrix(), parameterLifter->getVector(), oneStepProbs);
solver->setUpperBounds(dsmpi.computeUpperBounds());
} else {
- storm::modelchecker::helper::BaierUpperRewardBoundsComputer<typename SparseModelType::ValueType> baier(parameterLifter->getMatrix(), parameterLifter->getVector(), oneStepProbs);
+ storm::modelchecker::helper::BaierUpperRewardBoundsComputer<ConstantType> baier(parameterLifter->getMatrix(), parameterLifter->getVector(), oneStepProbs);
solver->setUpperBound(baier.computeUpperBound());
}
}
From 20960d56e7ca05078694e2705d0d12e09b2d39c5 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 2 Oct 2017 12:05:39 +0200
Subject: [PATCH 6/6] added missing 'this->'. Also avoid in-place matrix vector
multiplication when extracting a scheduler
---
src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp | 4 ++--
src/storm/solver/LpMinMaxLinearEquationSolver.cpp | 2 +-
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
index 70d2de0c1..a44024125 100644
--- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
@@ -256,7 +256,7 @@ namespace storm {
MinMaxLinearEquationSolverRequirements requirements(this->linearEquationSolverFactory->getRequirements());
// In case we perform value iteration and need to retrieve a scheduler, end components are forbidden
- if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration && isTrackSchedulerSet()) {
+ if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration && this->isTrackSchedulerSet()) {
requirements.requireNoEndComponents();
}
@@ -380,7 +380,7 @@ namespace storm {
// If requested, we store the scheduler for retrieval.
if (this->isTrackSchedulerSet()) {
this->schedulerChoices = std::vector<uint_fast64_t>(this->A->getRowGroupCount());
- this->linEqSolverA->multiplyAndReduce(dir, this->A->getRowGroupIndices(), x, &b, *currentX, &this->schedulerChoices.get());
+ this->linEqSolverA->multiplyAndReduce(dir, this->A->getRowGroupIndices(), x, &b, *auxiliaryRowGroupVector.get(), &this->schedulerChoices.get());
}
if (!this->isCachingEnabled()) {
diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp
index 0369d301d..024bcf260 100644
--- a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp
@@ -115,7 +115,7 @@ namespace storm {
MinMaxLinearEquationSolverRequirements requirements;
// In case we need to retrieve a scheduler, end components are forbidden
- if (isTrackSchedulerSet()) {
+ if (this->isTrackSchedulerSet()) {
requirements.requireNoEndComponents();
}