Matthias Volk
8 years ago
42 changed files with 1320 additions and 647 deletions
-
2.gitignore
-
29CHANGELOG.md
-
4src/CMakeLists.txt
-
2src/storm-dft-cli/CMakeLists.txt
-
2src/storm-gspn-cli/CMakeLists.txt
-
2src/storm-pars-cli/CMakeLists.txt
-
23src/storm-pars-cli/storm-pars.cpp
-
10src/storm-pars/api/export.h
-
7src/storm-pars/settings/modules/ParametricSettings.cpp
-
6src/storm-pars/settings/modules/ParametricSettings.h
-
2src/storm/CMakeLists.txt
-
8src/storm/analysis/GraphConditions.cpp
-
9src/storm/analysis/GraphConditions.h
-
42src/storm/counterexamples/MILPMinimalLabelSetGenerator.h
-
8src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
-
8src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
-
7src/storm/parser/JaniParser.cpp
-
4src/storm/permissivesched/MILPPermissiveSchedulers.h
-
2src/storm/permissivesched/PermissiveSchedulers.cpp
-
117src/storm/solver/GlpkLpSolver.cpp
-
49src/storm/solver/GlpkLpSolver.h
-
350src/storm/solver/GurobiLpSolver.cpp
-
27src/storm/solver/GurobiLpSolver.h
-
5src/storm/solver/IterativeMinMaxLinearEquationSolver.h
-
161src/storm/solver/LpMinMaxLinearEquationSolver.cpp
-
41src/storm/solver/LpMinMaxLinearEquationSolver.h
-
14src/storm/solver/LpSolver.cpp
-
25src/storm/solver/LpSolver.h
-
17src/storm/solver/MinMaxLinearEquationSolver.cpp
-
12src/storm/solver/MinMaxLinearEquationSolver.h
-
4src/storm/solver/TopologicalMinMaxLinearEquationSolver.h
-
423src/storm/solver/Z3LpSolver.cpp
-
39src/storm/solver/Z3LpSolver.h
-
12src/storm/storage/geometry/NativePolytope.cpp
-
64src/storm/utility/solver.cpp
-
31src/storm/utility/solver.h
-
272src/test/storm/modelchecker/LpMdpPrctlModelCheckerTest.cpp
-
10src/test/storm/permissiveschedulers/MilpPermissiveSchedulerTest.cpp
-
16src/test/storm/solver/GlpkLpSolverTest.cpp
-
16src/test/storm/solver/GurobiLpSolverTest.cpp
-
69src/test/storm/solver/LpMinMaxLinearEquationSolverTest.cpp
-
16src/test/storm/solver/Z3LpSolverTest.cpp
@ -0,0 +1,161 @@ |
|||
#include "storm/solver/LpMinMaxLinearEquationSolver.h"
|
|||
|
|||
#include "storm/utility/vector.h"
|
|||
#include "storm/utility/macros.h"
|
|||
#include "storm/exceptions/InvalidSettingsException.h"
|
|||
#include "storm/exceptions/InvalidOperationException.h"
|
|||
#include "storm/exceptions/UnexpectedException.h"
|
|||
|
|||
namespace storm { |
|||
namespace solver { |
|||
|
|||
template<typename ValueType> |
|||
LpMinMaxLinearEquationSolver<ValueType>::LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory) : StandardMinMaxLinearEquationSolver<ValueType>(A, std::move(linearEquationSolverFactory)), lpSolverFactory(std::move(lpSolverFactory)) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template<typename ValueType> |
|||
LpMinMaxLinearEquationSolver<ValueType>::LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory) : StandardMinMaxLinearEquationSolver<ValueType>(std::move(A), std::move(linearEquationSolverFactory)), lpSolverFactory(std::move(lpSolverFactory)) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template<typename ValueType> |
|||
bool LpMinMaxLinearEquationSolver<ValueType>::solveEquations(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const { |
|||
|
|||
// Set up the LP solver
|
|||
std::unique_ptr<storm::solver::LpSolver<ValueType>> solver = lpSolverFactory->create(""); |
|||
solver->setOptimizationDirection(invert(dir)); |
|||
|
|||
// Create a variable for each row group
|
|||
std::vector<storm::expressions::Variable> variables; |
|||
variables.reserve(this->A.getRowGroupCount()); |
|||
for (uint64_t rowGroup = 0; rowGroup < this->A.getRowGroupCount(); ++rowGroup) { |
|||
if (this->lowerBound) { |
|||
if (this->upperBound) { |
|||
variables.push_back(solver->addBoundedContinuousVariable("x" + std::to_string(rowGroup), this->lowerBound.get(), this->upperBound.get(), storm::utility::one<ValueType>())); |
|||
} else { |
|||
variables.push_back(solver->addLowerBoundedContinuousVariable("x" + std::to_string(rowGroup), this->lowerBound.get(), storm::utility::one<ValueType>())); |
|||
} |
|||
} else { |
|||
if (this->upperBound) { |
|||
variables.push_back(solver->addUpperBoundedContinuousVariable("x" + std::to_string(rowGroup), this->upperBound.get(), storm::utility::one<ValueType>())); |
|||
} else { |
|||
variables.push_back(solver->addUnboundedContinuousVariable("x" + std::to_string(rowGroup), storm::utility::one<ValueType>())); |
|||
} |
|||
} |
|||
} |
|||
solver->update(); |
|||
|
|||
// Add a constraint for each row
|
|||
for (uint64_t rowGroup = 0; rowGroup < this->A.getRowGroupCount(); ++rowGroup) { |
|||
for (uint64_t row = this->A.getRowGroupIndices()[rowGroup]; row < this->A.getRowGroupIndices()[rowGroup + 1]; ++row) { |
|||
storm::expressions::Expression rowConstraint = solver->getConstant(b[row]); |
|||
for (auto const& entry : this->A.getRow(row)) { |
|||
rowConstraint = rowConstraint + (solver->getConstant(entry.getValue()) * variables[entry.getColumn()].getExpression()); |
|||
} |
|||
if (minimize(dir)) { |
|||
rowConstraint = variables[rowGroup].getExpression() <= rowConstraint; |
|||
} else { |
|||
rowConstraint = variables[rowGroup].getExpression() >= rowConstraint; |
|||
} |
|||
solver->addConstraint("", rowConstraint); |
|||
} |
|||
} |
|||
|
|||
// Invoke optimization
|
|||
solver->optimize(); |
|||
STORM_LOG_THROW(!solver->isInfeasible(), storm::exceptions::UnexpectedException, "The MinMax equation system is infeasible."); |
|||
STORM_LOG_THROW(!solver->isUnbounded(), storm::exceptions::UnexpectedException, "The MinMax equation system is unbounded."); |
|||
STORM_LOG_THROW(solver->isOptimal(), storm::exceptions::UnexpectedException, "Unable to find optimal solution for MinMax equation system."); |
|||
|
|||
// write the solution into the solution vector
|
|||
STORM_LOG_ASSERT(x.size() == variables.size(), "Dimension of x-vector does not match number of varibales."); |
|||
auto xIt = x.begin(); |
|||
auto vIt = variables.begin(); |
|||
for (; xIt != x.end(); ++xIt, ++vIt) { |
|||
*xIt = solver->getContinuousValue(*vIt); |
|||
} |
|||
|
|||
// If requested, we store the scheduler for retrieval.
|
|||
if (this->isTrackSchedulerSet()) { |
|||
this->schedulerChoices = std::vector<uint_fast64_t>(this->A.getRowGroupCount()); |
|||
for (uint64_t rowGroup = 0; rowGroup < this->A.getRowGroupCount(); ++rowGroup) { |
|||
uint64_t row = this->A.getRowGroupIndices()[rowGroup]; |
|||
uint64_t optimalChoiceIndex = 0; |
|||
uint64_t currChoice = 0; |
|||
ValueType optimalGroupValue = this->A.multiplyRowWithVector(row, x) + b[row]; |
|||
for (++row, ++currChoice; row < this->A.getRowGroupIndices()[rowGroup + 1]; ++row, ++currChoice) { |
|||
ValueType rowValue = this->A.multiplyRowWithVector(row, x) + b[row]; |
|||
if ((minimize(dir) && rowValue < optimalGroupValue) || (maximize(dir) && rowValue > optimalGroupValue)) { |
|||
optimalGroupValue = rowValue; |
|||
optimalChoiceIndex = currChoice; |
|||
} |
|||
} |
|||
this->schedulerChoices.get()[rowGroup] = optimalChoiceIndex; |
|||
} |
|||
} |
|||
|
|||
return true; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
void LpMinMaxLinearEquationSolver<ValueType>::clearCache() const { |
|||
StandardMinMaxLinearEquationSolver<ValueType>::clearCache(); |
|||
} |
|||
|
|||
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
|
|||
} |
|||
|
|||
template<typename ValueType> |
|||
LpMinMaxLinearEquationSolverFactory<ValueType>::LpMinMaxLinearEquationSolverFactory(std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory, bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory<ValueType>(MinMaxMethodSelection::LinearProgramming, trackScheduler), lpSolverFactory(std::move(lpSolverFactory)) { |
|||
// Intentionally left empty
|
|||
} |
|||
|
|||
template<typename ValueType> |
|||
LpMinMaxLinearEquationSolverFactory<ValueType>::LpMinMaxLinearEquationSolverFactory(std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory, bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory<ValueType>(std::move(linearEquationSolverFactory), MinMaxMethodSelection::LinearProgramming, trackScheduler), lpSolverFactory(std::move(lpSolverFactory)) { |
|||
// Intentionally left empty
|
|||
} |
|||
|
|||
template<typename ValueType> |
|||
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> LpMinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix) const { |
|||
STORM_LOG_ASSERT(this->linearEquationSolverFactory, "Linear equation solver factory not initialized."); |
|||
STORM_LOG_ASSERT(this->lpSolverFactory, "Lp solver factory not initialized."); |
|||
|
|||
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> result = std::make_unique<LpMinMaxLinearEquationSolver<ValueType>>(std::move(matrix), this->linearEquationSolverFactory->clone(), this->lpSolverFactory->clone()); |
|||
result->setTrackScheduler(this->isTrackSchedulerSet()); |
|||
return result; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> LpMinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType>&& matrix) const { |
|||
STORM_LOG_ASSERT(this->linearEquationSolverFactory, "Linear equation solver factory not initialized."); |
|||
STORM_LOG_ASSERT(this->lpSolverFactory, "Lp solver factory not initialized."); |
|||
|
|||
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> result = std::make_unique<LpMinMaxLinearEquationSolver<ValueType>>(std::move(matrix), this->linearEquationSolverFactory->clone(), this->lpSolverFactory->clone()); |
|||
result->setTrackScheduler(this->isTrackSchedulerSet()); |
|||
return result; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
void LpMinMaxLinearEquationSolverFactory<ValueType>::setMinMaxMethod(MinMaxMethodSelection const& newMethod) { |
|||
STORM_LOG_THROW(newMethod == MinMaxMethodSelection::LinearProgramming, storm::exceptions::InvalidOperationException, "The factory can only create linear programming based MinMax solvers."); |
|||
MinMaxLinearEquationSolverFactory<ValueType>::setMinMaxMethod(newMethod); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
void LpMinMaxLinearEquationSolverFactory<ValueType>::setMinMaxMethod(MinMaxMethod const& newMethod) { |
|||
STORM_LOG_THROW(newMethod == MinMaxMethod::LinearProgramming, storm::exceptions::InvalidOperationException, "The factory can only create linear programming based MinMax solvers."); |
|||
MinMaxLinearEquationSolverFactory<ValueType>::setMinMaxMethod(newMethod); |
|||
} |
|||
|
|||
template class LpMinMaxLinearEquationSolver<double>; |
|||
template class LpMinMaxLinearEquationSolverFactory<double>; |
|||
|
|||
#ifdef STORM_HAVE_CARL
|
|||
template class LpMinMaxLinearEquationSolver<storm::RationalNumber>; |
|||
template class LpMinMaxLinearEquationSolverFactory<storm::RationalNumber>; |
|||
#endif
|
|||
} |
|||
} |
|||
@ -0,0 +1,41 @@ |
|||
#pragma once |
|||
|
|||
#include "storm/solver/LpSolver.h" |
|||
#include "storm/solver/StandardMinMaxLinearEquationSolver.h" |
|||
#include "storm/utility/solver.h" |
|||
|
|||
namespace storm { |
|||
namespace solver { |
|||
|
|||
template<typename ValueType> |
|||
class LpMinMaxLinearEquationSolver : public StandardMinMaxLinearEquationSolver<ValueType> { |
|||
public: |
|||
LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory); |
|||
LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory); |
|||
|
|||
virtual bool solveEquations(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const override; |
|||
|
|||
virtual void clearCache() const override; |
|||
|
|||
private: |
|||
std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>> lpSolverFactory; |
|||
}; |
|||
|
|||
template<typename ValueType> |
|||
class LpMinMaxLinearEquationSolverFactory : public StandardMinMaxLinearEquationSolverFactory<ValueType> { |
|||
public: |
|||
LpMinMaxLinearEquationSolverFactory(bool trackScheduler = false); |
|||
LpMinMaxLinearEquationSolverFactory(std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory, bool trackScheduler = false); |
|||
LpMinMaxLinearEquationSolverFactory(std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory, bool trackScheduler = false); |
|||
|
|||
virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const override; |
|||
virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType>&& matrix) const override; |
|||
|
|||
virtual void setMinMaxMethod(MinMaxMethodSelection const& newMethod) override; |
|||
virtual void setMinMaxMethod(MinMaxMethod const& newMethod) override; |
|||
|
|||
private: |
|||
std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>> lpSolverFactory; |
|||
}; |
|||
} |
|||
} |
|||
@ -0,0 +1,272 @@ |
|||
#include "gtest/gtest.h"
|
|||
#include "storm-config.h"
|
|||
|
|||
#include "storm/parser/FormulaParser.h"
|
|||
#include "storm/logic/Formulas.h"
|
|||
#include "storm/solver/LpMinMaxLinearEquationSolver.h"
|
|||
#include "storm/models/sparse/StandardRewardModel.h"
|
|||
#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
|
|||
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
|
|||
#include "storm/settings/SettingsManager.h"
|
|||
#include "storm/settings/modules/GeneralSettings.h"
|
|||
|
|||
#include "storm/parser/AutoParser.h"
|
|||
#include "storm/parser/PrismParser.h"
|
|||
#include "storm/builder/ExplicitModelBuilder.h"
|
|||
|
|||
TEST(LpMdpPrctlModelCheckerTest, Dice) { |
|||
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", "", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.trans.rew"); |
|||
|
|||
// A parser that we use for conveniently constructing the formulas.
|
|||
storm::parser::FormulaParser formulaParser; |
|||
|
|||
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); |
|||
|
|||
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>(); |
|||
|
|||
ASSERT_EQ(mdp->getNumberOfStates(), 169ull); |
|||
ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); |
|||
|
|||
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::make_unique<storm::solver::LpMinMaxLinearEquationSolverFactory<double>>()); |
|||
|
|||
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult3[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult7 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(7.333333333, quantitativeResult7[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult8 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(7.333333333, quantitativeResult8[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew", ""); |
|||
|
|||
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); |
|||
|
|||
std::shared_ptr<storm::models::sparse::Mdp<double>> stateRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>(); |
|||
|
|||
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateRewardModelChecker(*mdp, std::make_unique<storm::solver::LpMinMaxLinearEquationSolverFactory<double>>()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); |
|||
|
|||
result = stateRewardModelChecker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult9 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(7.333333333, quantitativeResult9[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); |
|||
|
|||
result = stateRewardModelChecker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult10 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(7.333333333, quantitativeResult10[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.trans.rew"); |
|||
|
|||
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); |
|||
|
|||
std::shared_ptr<storm::models::sparse::Mdp<double>> stateAndTransitionRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>(); |
|||
|
|||
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::make_unique<storm::solver::LpMinMaxLinearEquationSolverFactory<double>>()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); |
|||
|
|||
result = stateAndTransitionRewardModelChecker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult11 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(14.666666666, quantitativeResult11[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); |
|||
|
|||
result = stateAndTransitionRewardModelChecker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult12 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(14.666666666, quantitativeResult12[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
} |
|||
|
|||
TEST(LpMdpPrctlModelCheckerTest, AsynchronousLeader) { |
|||
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/leader4.tra", STORM_TEST_RESOURCES_DIR "/lab/leader4.lab", "", STORM_TEST_RESOURCES_DIR "/rew/leader4.trans.rew"); |
|||
|
|||
// A parser that we use for conveniently constructing the formulas.
|
|||
storm::parser::FormulaParser formulaParser; |
|||
|
|||
ASSERT_EQ(storm::models::ModelType::Mdp, abstractModel->getType()); |
|||
|
|||
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>(); |
|||
|
|||
ASSERT_EQ(3172ull, mdp->getNumberOfStates()); |
|||
ASSERT_EQ(7144ull, mdp->getNumberOfTransitions()); |
|||
|
|||
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::make_unique<storm::solver::LpMinMaxLinearEquationSolverFactory<double>>()); |
|||
|
|||
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(1, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(1, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(0.0625, quantitativeResult3[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(0.0625, quantitativeResult4[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(4.285714286, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(4.285714286, quantitativeResult6[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
} |
|||
|
|||
TEST(LpMdpPrctlModelCheckerTest, SchedulerGeneration) { |
|||
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/scheduler_generation.nm"); |
|||
|
|||
// A parser that we use for conveniently constructing the formulas.
|
|||
storm::parser::FormulaParser formulaParser; |
|||
|
|||
storm::generator::NextStateGeneratorOptions options; |
|||
options.setBuildAllLabels(); |
|||
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, options).build(); |
|||
EXPECT_EQ(4ull, model->getNumberOfStates()); |
|||
EXPECT_EQ(11ull, model->getNumberOfTransitions()); |
|||
|
|||
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); |
|||
|
|||
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = model->as<storm::models::sparse::Mdp<double>>(); |
|||
|
|||
EXPECT_EQ(7ull, mdp->getNumberOfChoices()); |
|||
|
|||
auto solverFactory = std::make_unique<storm::solver::LpMinMaxLinearEquationSolverFactory<double>>(); |
|||
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::move(solverFactory)); |
|||
|
|||
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"target\"]"); |
|||
|
|||
storm::modelchecker::CheckTask<storm::logic::Formula> checkTask(*formula); |
|||
checkTask.setProduceSchedulers(true); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(checkTask); |
|||
|
|||
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); |
|||
ASSERT_TRUE(result->asExplicitQuantitativeCheckResult<double>().hasScheduler()); |
|||
storm::storage::Scheduler<double> const& scheduler = result->asExplicitQuantitativeCheckResult<double>().getScheduler(); |
|||
EXPECT_EQ(0ull, scheduler.getChoice(0).getDeterministicChoice()); |
|||
EXPECT_EQ(1ull, scheduler.getChoice(1).getDeterministicChoice()); |
|||
EXPECT_EQ(0ull, scheduler.getChoice(2).getDeterministicChoice()); |
|||
EXPECT_EQ(0ull, scheduler.getChoice(3).getDeterministicChoice()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"target\"]"); |
|||
|
|||
checkTask = storm::modelchecker::CheckTask<storm::logic::Formula>(*formula); |
|||
checkTask.setProduceSchedulers(true); |
|||
result = checker.check(checkTask); |
|||
|
|||
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); |
|||
ASSERT_TRUE(result->asExplicitQuantitativeCheckResult<double>().hasScheduler()); |
|||
storm::storage::Scheduler<double> const& scheduler2 = result->asExplicitQuantitativeCheckResult<double>().getScheduler(); |
|||
EXPECT_EQ(1ull, scheduler2.getChoice(0).getDeterministicChoice()); |
|||
EXPECT_EQ(2ull, scheduler2.getChoice(1).getDeterministicChoice()); |
|||
EXPECT_EQ(0ull, scheduler2.getChoice(2).getDeterministicChoice()); |
|||
EXPECT_EQ(0ull, scheduler2.getChoice(3).getDeterministicChoice()); |
|||
} |
|||
|
|||
// Test is currently disabled as the computation of this property requires eliminating the zero-reward MECs, which is
|
|||
// currently not implemented and also not supported by PRISM.
|
|||
TEST(LpMdpPrctlModelCheckerTest, TinyRewards) { |
|||
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/tiny_rewards.nm"); |
|||
|
|||
// A parser that we use for conveniently constructing the formulas.
|
|||
storm::parser::FormulaParser formulaParser; |
|||
|
|||
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(true, true)).build(); |
|||
EXPECT_EQ(3ull, model->getNumberOfStates()); |
|||
EXPECT_EQ(4ull, model->getNumberOfTransitions()); |
|||
|
|||
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); |
|||
|
|||
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = model->as<storm::models::sparse::Mdp<double>>(); |
|||
|
|||
EXPECT_EQ(4ull, mdp->getNumberOfChoices()); |
|||
|
|||
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::make_unique<storm::solver::LpMinMaxLinearEquationSolverFactory<double>>()); |
|||
|
|||
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"target\"]"); |
|||
|
|||
storm::modelchecker::CheckTask<storm::logic::Formula> checkTask(*formula); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(checkTask); |
|||
|
|||
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); |
|||
EXPECT_NEAR(1, result->asExplicitQuantitativeCheckResult<double>().getValueVector()[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
EXPECT_NEAR(1, result->asExplicitQuantitativeCheckResult<double>().getValueVector()[1], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
EXPECT_NEAR(0, result->asExplicitQuantitativeCheckResult<double>().getValueVector()[2], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
} |
|||
@ -0,0 +1,69 @@ |
|||
#include "gtest/gtest.h"
|
|||
#include "storm-config.h"
|
|||
|
|||
#include "storm/solver/LpMinMaxLinearEquationSolver.h"
|
|||
#include "storm/settings/SettingsManager.h"
|
|||
#include "storm/settings/modules/GeneralSettings.h"
|
|||
|
|||
#include "storm/storage/SparseMatrix.h"
|
|||
|
|||
TEST(LpMinMaxLinearEquationSolver, SolveWithStandardOptions) { |
|||
storm::storage::SparseMatrixBuilder<double> builder(0, 0, 0, false, true); |
|||
ASSERT_NO_THROW(builder.newRowGroup(0)); |
|||
ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9)); |
|||
|
|||
storm::storage::SparseMatrix<double> A; |
|||
ASSERT_NO_THROW(A = builder.build(2)); |
|||
|
|||
std::vector<double> x(1); |
|||
std::vector<double> b = {0.099, 0.5}; |
|||
|
|||
auto factory = storm::solver::LpMinMaxLinearEquationSolverFactory<double>(); |
|||
auto solver = factory.create(A); |
|||
ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Minimize, x, b)); |
|||
ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Maximize, x, b)); |
|||
ASSERT_LT(std::abs(x[0] - 0.99), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
} |
|||
|
|||
TEST(LpMinMaxLinearEquationSolver, MatrixVectorMultiplication) { |
|||
storm::storage::SparseMatrixBuilder<double> builder(0, 0, 0, false, true); |
|||
ASSERT_NO_THROW(builder.newRowGroup(0)); |
|||
ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9)); |
|||
ASSERT_NO_THROW(builder.addNextValue(0, 1, 0.099)); |
|||
ASSERT_NO_THROW(builder.addNextValue(0, 2, 0.001)); |
|||
ASSERT_NO_THROW(builder.addNextValue(1, 1, 0.5)); |
|||
ASSERT_NO_THROW(builder.addNextValue(1, 2, 0.5)); |
|||
ASSERT_NO_THROW(builder.newRowGroup(2)); |
|||
ASSERT_NO_THROW(builder.addNextValue(2, 1, 1)); |
|||
ASSERT_NO_THROW(builder.newRowGroup(3)); |
|||
ASSERT_NO_THROW(builder.addNextValue(3, 2, 1)); |
|||
|
|||
storm::storage::SparseMatrix<double> A; |
|||
ASSERT_NO_THROW(A = builder.build()); |
|||
|
|||
std::vector<double> x = {0, 1, 0}; |
|||
|
|||
auto factory = storm::solver::LpMinMaxLinearEquationSolverFactory<double>(); |
|||
auto solver = factory.create(A); |
|||
|
|||
ASSERT_NO_THROW(solver->repeatedMultiply(storm::OptimizationDirection::Minimize, x, nullptr, 1)); |
|||
ASSERT_LT(std::abs(x[0] - 0.099), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
x = {0, 1, 0}; |
|||
ASSERT_NO_THROW(solver->repeatedMultiply(storm::OptimizationDirection::Minimize, x, nullptr, 2)); |
|||
ASSERT_LT(std::abs(x[0] - 0.1881), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
x = {0, 1, 0}; |
|||
ASSERT_NO_THROW(solver->repeatedMultiply(storm::OptimizationDirection::Minimize, x, nullptr, 20)); |
|||
ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
x = {0, 1, 0}; |
|||
ASSERT_NO_THROW(solver->repeatedMultiply(storm::OptimizationDirection::Maximize, x, nullptr, 1)); |
|||
ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
x = {0, 1, 0}; |
|||
ASSERT_NO_THROW(solver->repeatedMultiply(storm::OptimizationDirection::Maximize, x, nullptr, 20)); |
|||
ASSERT_LT(std::abs(x[0] - 0.9238082658), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
} |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue