diff --git a/src/test/storm/modelchecker/prctl/ConditionalDtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/ConditionalDtmcPrctlModelCheckerTest.cpp deleted file mode 100755 index 5b8eea78d..000000000 --- a/src/test/storm/modelchecker/prctl/ConditionalDtmcPrctlModelCheckerTest.cpp +++ /dev/null @@ -1,170 +0,0 @@ -#include "test/storm_gtest.h" -#include "test/storm_gtest.h" -#include "storm-config.h" - -#include "storm-parsers/parser/FormulaParser.h" -#include "storm/logic/Formulas.h" -#include "storm/models/sparse/StandardRewardModel.h" -#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" -#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" -#include "storm-parsers/parser/PrismParser.h" -#include "storm/api/builder.h" -#include "storm/storage/expressions/ExpressionManager.h" - -#include "storm/environment/solver/GmmxxSolverEnvironment.h" -#include "storm/environment/solver/EigenSolverEnvironment.h" -#include "storm/environment/solver/NativeSolverEnvironment.h" - -namespace { - - class GmmxxDoubleGmresEnvironment { - public: - typedef double ValueType; - static const bool isExact = false; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx); - env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres); - env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu); - env.solver().gmmxx().setPrecision(storm::utility::convertNumber(1e-8)); - return env; - } - }; - - class EigenDoubleDGmresEnvironment { - public: - typedef double ValueType; - static const bool isExact = false; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen); - env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::DGmres); - env.solver().eigen().setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner::Ilu); - env.solver().eigen().setPrecision(storm::utility::convertNumber(1e-8)); - return env; - } - }; - - class EigenRationalLUEnvironment { - public: - typedef storm::RationalNumber ValueType; - static const bool isExact = true; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen); - env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU); - return env; - } - }; - - class NativeSorEnvironment { - public: - typedef double ValueType; - static const bool isExact = false; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native); - env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::SOR); - env.solver().native().setSorOmega(storm::utility::convertNumber(0.9)); - env.solver().native().setPrecision(storm::utility::convertNumber(1e-8)); - return env; - } - }; - - class NativePowerEnvironment { - public: - typedef double ValueType; - static const bool isExact = false; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native); - env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Power); - env.solver().native().setPrecision(storm::utility::convertNumber(1e-8)); - return env; - } - }; - - class NativeWalkerChaeEnvironment { - public: - typedef double ValueType; - static const bool isExact = false; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native); - env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::WalkerChae); - env.solver().native().setPrecision(storm::utility::convertNumber(1e-8)); - env.solver().native().setMaximalNumberOfIterations(50000); - return env; - } - }; - - template - class ConditionalDtmcPrctlModelCheckerTest : public ::testing::Test { - public: - typedef typename TestType::ValueType ValueType; - ConditionalDtmcPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {} - storm::Environment const& env() const { return _environment; } - ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber(input);} - ValueType precision() const { return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");} - - private: - storm::Environment _environment; - }; - - typedef ::testing::Types< - GmmxxDoubleGmresEnvironment, - EigenDoubleDGmresEnvironment, - EigenRationalLUEnvironment, - NativeSorEnvironment, - NativePowerEnvironment, - NativeWalkerChaeEnvironment - > TestingTypes; - - TYPED_TEST_SUITE(ConditionalDtmcPrctlModelCheckerTest, TestingTypes); - - - TYPED_TEST(ConditionalDtmcPrctlModelCheckerTest, Conditional) { - typedef typename TestFixture::ValueType ValueType; - - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/test_conditional.pm"); - - storm::generator::NextStateGeneratorOptions options; - options.setBuildAllLabels().setBuildAllRewardModels(); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).build(); - ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc); - ASSERT_EQ(4ul, model->getNumberOfStates()); - ASSERT_EQ(5ul, model->getNumberOfTransitions()); - - std::shared_ptr> dtmc = model->template as>(); - - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc); - - // A parser that we use for conveniently constructing the formulas. - - auto expManager = std::make_shared(); - storm::parser::FormulaParser formulaParser(expManager); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"target\"]"); - - std::unique_ptr result = checker.check(this->env(), *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[0], this->precision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"target\" || F \"condition\"]"); - - result = checker.check(this->env(), *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(storm::utility::one(), quantitativeResult2[0], this->precision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"target\"]"); - - result = checker.check(this->env(), *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - EXPECT_EQ(storm::utility::infinity(), quantitativeResult3[0]); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"target\" || F \"condition\"]"); - - result = checker.check(this->env(), *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(storm::utility::one(), quantitativeResult4[0], this->precision()); - } -} diff --git a/src/test/storm/modelchecker/prctl/DtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/DtmcPrctlModelCheckerTest.cpp deleted file mode 100755 index 861b5d67f..000000000 --- a/src/test/storm/modelchecker/prctl/DtmcPrctlModelCheckerTest.cpp +++ /dev/null @@ -1,701 +0,0 @@ -#include "test/storm_gtest.h" -#include "test/storm_gtest.h" -#include "storm-config.h" - -#include "storm/api/builder.h" -#include "storm-conv/api/storm-conv.h" -#include "storm-parsers/api/model_descriptions.h" -#include "storm/api/properties.h" -#include "storm-parsers/api/properties.h" -#include "storm-parsers/parser/FormulaParser.h" -#include "storm/logic/Formulas.h" -#include "storm/solver/EigenLinearEquationSolver.h" -#include "storm/models/sparse/StandardRewardModel.h" -#include "storm/models/symbolic/StandardRewardModel.h" -#include "storm/models/sparse/Dtmc.h" -#include "storm/models/symbolic/Dtmc.h" -#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" -#include "storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h" -#include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h" -#include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h" -#include "storm/modelchecker/results/QuantitativeCheckResult.h" -#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" -#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" -#include "storm/modelchecker/results/QualitativeCheckResult.h" -#include "storm-parsers/parser/PrismParser.h" -#include "storm/storage/expressions/ExpressionManager.h" -#include "storm/settings/modules/CoreSettings.h" -#include "storm/environment/solver/NativeSolverEnvironment.h" -#include "storm/environment/solver/GmmxxSolverEnvironment.h" -#include "storm/environment/solver/EigenSolverEnvironment.h" -#include "storm/environment/solver/TopologicalSolverEnvironment.h" - -namespace { - - enum class DtmcEngine {PrismSparse, JaniSparse, JitSparse, Hybrid, PrismDd, JaniDd}; - - class SparseGmmxxGmresIluEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models - static const DtmcEngine engine = DtmcEngine::PrismSparse; - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::sparse::Dtmc ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx); - env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres); - env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu); - env.solver().gmmxx().setPrecision(storm::utility::convertNumber(1e-8)); - return env; - } - }; - - class JaniSparseGmmxxGmresIluEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models - static const DtmcEngine engine = DtmcEngine::JaniSparse; - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::sparse::Dtmc ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx); - env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres); - env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu); - env.solver().gmmxx().setPrecision(storm::utility::convertNumber(1e-8)); - return env; - } - }; - - class JitSparseGmmxxGmresIluEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models - static const DtmcEngine engine = DtmcEngine::JitSparse; - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::sparse::Dtmc ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx); - env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres); - env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu); - env.solver().gmmxx().setPrecision(storm::utility::convertNumber(1e-8)); - return env; - } - }; - - class SparseGmmxxGmresDiagEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models - static const DtmcEngine engine = DtmcEngine::PrismSparse; - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::sparse::Dtmc ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx); - env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres); - env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Diagonal); - env.solver().gmmxx().setPrecision(storm::utility::convertNumber(1e-8)); - return env; - } - }; - - class SparseGmmxxBicgstabIluEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models - static const DtmcEngine engine = DtmcEngine::PrismSparse; - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::sparse::Dtmc ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx); - env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Bicgstab); - env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu); - env.solver().gmmxx().setPrecision(storm::utility::convertNumber(1e-8)); - return env; - } - }; - - class SparseEigenDGmresEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models - static const DtmcEngine engine = DtmcEngine::PrismSparse; - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::sparse::Dtmc ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen); - env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::DGmres); - env.solver().eigen().setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner::Ilu); - env.solver().eigen().setPrecision(storm::utility::convertNumber(1e-8)); - return env; - } - }; - - class SparseEigenDoubleLUEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models - static const DtmcEngine engine = DtmcEngine::PrismSparse; - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::sparse::Dtmc ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen); - env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU); - return env; - } - }; - - class SparseEigenRationalLUEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models - static const DtmcEngine engine = DtmcEngine::PrismSparse; - static const bool isExact = true; - typedef storm::RationalNumber ValueType; - typedef storm::models::sparse::Dtmc ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen); - env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU); - return env; - } - }; - - class SparseRationalEliminationEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models - static const DtmcEngine engine = DtmcEngine::PrismSparse; - static const bool isExact = true; - typedef storm::RationalNumber ValueType; - typedef storm::models::sparse::Dtmc ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Elimination); - return env; - } - }; - - class SparseNativeJacobiEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models - static const DtmcEngine engine = DtmcEngine::PrismSparse; - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::sparse::Dtmc ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native); - env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Jacobi); - env.solver().native().setPrecision(storm::utility::convertNumber(1e-8)); - return env; - } - }; - - class SparseNativeWalkerChaeEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models - static const DtmcEngine engine = DtmcEngine::PrismSparse; - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::sparse::Dtmc ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native); - env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::WalkerChae); - env.solver().native().setMaximalNumberOfIterations(1000000); - env.solver().native().setPrecision(storm::utility::convertNumber(1e-7)); - return env; - } - }; - - class SparseNativeSorEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models - static const DtmcEngine engine = DtmcEngine::PrismSparse; - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::sparse::Dtmc ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native); - env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::SOR); - env.solver().native().setPrecision(storm::utility::convertNumber(1e-8)); - return env; - } - }; - - class SparseNativePowerEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models - static const DtmcEngine engine = DtmcEngine::PrismSparse; - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::sparse::Dtmc ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native); - env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Power); - env.solver().native().setPrecision(storm::utility::convertNumber(1e-8)); - return env; - } - }; - - class SparseNativeSoundValueIterationEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models - static const DtmcEngine engine = DtmcEngine::PrismSparse; - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::sparse::Dtmc ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setForceSoundness(true); - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native); - env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::SoundValueIteration); - env.solver().native().setPrecision(storm::utility::convertNumber(1e-6)); - return env; - } - }; - - class SparseNativeIntervalIterationEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models - static const DtmcEngine engine = DtmcEngine::PrismSparse; - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::sparse::Dtmc ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setForceSoundness(true); - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native); - env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::IntervalIteration); - env.solver().native().setRelativeTerminationCriterion(false); - env.solver().native().setPrecision(storm::utility::convertNumber(1e-6)); - return env; - } - }; - - class SparseNativeRationalSearchEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models - static const DtmcEngine engine = DtmcEngine::PrismSparse; - static const bool isExact = true; - typedef storm::RationalNumber ValueType; - typedef storm::models::sparse::Dtmc ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native); - env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::RationalSearch); - return env; - } - }; - - class SparseTopologicalEigenLUEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models - static const DtmcEngine engine = DtmcEngine::PrismSparse; - static const bool isExact = true; - typedef storm::RationalNumber ValueType; - typedef storm::models::sparse::Dtmc ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Topological); - env.solver().topological().setUnderlyingEquationSolverType(storm::solver::EquationSolverType::Eigen); - env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU); - return env; - } - }; - - class HybridSylvanGmmxxGmresEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; - static const DtmcEngine engine = DtmcEngine::Hybrid; - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::symbolic::Dtmc ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx); - env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres); - env.solver().gmmxx().setPrecision(storm::utility::convertNumber(1e-8)); - return env; - } - }; - - class HybridCuddNativeJacobiEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::CUDD; - static const DtmcEngine engine = DtmcEngine::Hybrid; - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::symbolic::Dtmc ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native); - env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Jacobi); - env.solver().native().setPrecision(storm::utility::convertNumber(1e-8)); - return env; - } - }; - - class HybridCuddNativeSoundValueIterationEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::CUDD; - static const DtmcEngine engine = DtmcEngine::Hybrid; - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::symbolic::Dtmc ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setForceSoundness(true); - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native); - env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Power); - env.solver().native().setPrecision(storm::utility::convertNumber(1e-6)); - return env; - } - }; - - class HybridSylvanNativeRationalSearchEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; - static const DtmcEngine engine = DtmcEngine::Hybrid; - static const bool isExact = true; - typedef storm::RationalNumber ValueType; - typedef storm::models::symbolic::Dtmc ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native); - env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::RationalSearch); - return env; - } - }; - - class DdSylvanNativePowerEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; - static const DtmcEngine engine = DtmcEngine::PrismDd; - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::symbolic::Dtmc ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native); - env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Power); - env.solver().native().setPrecision(storm::utility::convertNumber(1e-8)); - return env; - } - }; - - class JaniDdSylvanNativePowerEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; - static const DtmcEngine engine = DtmcEngine::JaniDd; - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::symbolic::Dtmc ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native); - env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Power); - env.solver().native().setPrecision(storm::utility::convertNumber(1e-8)); - return env; - } - }; - - class DdCuddNativeJacobiEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::CUDD; - static const DtmcEngine engine = DtmcEngine::PrismDd; - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::symbolic::Dtmc ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native); - env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Power); - env.solver().native().setPrecision(storm::utility::convertNumber(1e-8)); - return env; - } - }; - - class DdSylvanRationalSearchEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; - static const DtmcEngine engine = DtmcEngine::PrismDd; - static const bool isExact = true; - typedef storm::RationalNumber ValueType; - typedef storm::models::symbolic::Dtmc ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native); - env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::RationalSearch); - return env; - } - }; - - template - class DtmcPrctlModelCheckerTest : public ::testing::Test { - public: - typedef typename TestType::ValueType ValueType; - typedef typename storm::models::sparse::Dtmc SparseModelType; - typedef typename storm::models::symbolic::Dtmc SymbolicModelType; - - DtmcPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {} - storm::Environment const& env() const { return _environment; } - ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber(input);} - ValueType precision() const { return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");} - bool isSparseModel() const { return std::is_same::value; } - bool isSymbolicModel() const { return std::is_same::value; } - - template - typename std::enable_if::value, std::pair, std::vector>>>::type - buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { - std::pair, std::vector>> result; - storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); - program = storm::utility::prism::preprocess(program, constantDefinitionString); - if (TestType::engine == DtmcEngine::PrismSparse) { - result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); - result.first = storm::api::buildSparseModel(program, result.second)->template as(); - } else if (TestType::engine == DtmcEngine::JaniSparse || TestType::engine == DtmcEngine::JitSparse) { - auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); - result.second = storm::api::extractFormulasFromProperties(janiData.second); - result.first = storm::api::buildSparseModel(janiData.first, result.second, TestType::engine == DtmcEngine::JitSparse)->template as(); - } - - return result; - } - - template - typename std::enable_if::value, std::pair, std::vector>>>::type - buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { - std::pair, std::vector>> result; - storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); - program = storm::utility::prism::preprocess(program, constantDefinitionString); - if (TestType::engine == DtmcEngine::Hybrid || TestType::engine == DtmcEngine::PrismDd) { - result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); - result.first = storm::api::buildSymbolicModel(program, result.second)->template as(); - } else if (TestType::engine == DtmcEngine::JaniDd) { - auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); - janiData.first.substituteFunctions(); - result.second = storm::api::extractFormulasFromProperties(janiData.second); - result.first = storm::api::buildSymbolicModel(janiData.first, result.second)->template as(); - } - return result; - } - - std::vector> getTasks(std::vector> const& formulas) const { - std::vector> result; - for (auto const& f : formulas) { - result.emplace_back(*f); - } - return result; - } - - template - typename std::enable_if::value, std::shared_ptr>>::type - createModelChecker(std::shared_ptr const& model) const { - if (TestType::engine == DtmcEngine::PrismSparse || TestType::engine == DtmcEngine::JaniSparse || TestType::engine == DtmcEngine::JitSparse) { - return std::make_shared>(*model); - } - } - - template - typename std::enable_if::value, std::shared_ptr>>::type - createModelChecker(std::shared_ptr const& model) const { - if (TestType::engine == DtmcEngine::Hybrid) { - return std::make_shared>(*model); - } else if (TestType::engine == DtmcEngine::PrismDd || TestType::engine == DtmcEngine::JaniDd) { - return std::make_shared>(*model); - } - } - - bool getQualitativeResultAtInitialState(std::shared_ptr> const& model, std::unique_ptr& result) { - auto filter = getInitialStateFilter(model); - result->filter(*filter); - return result->asQualitativeCheckResult().forallTrue(); - } - - ValueType getQuantitativeResultAtInitialState(std::shared_ptr> const& model, std::unique_ptr& result) { - auto filter = getInitialStateFilter(model); - result->filter(*filter); - return result->asQuantitativeCheckResult().getMin(); - } - - private: - storm::Environment _environment; - - std::unique_ptr getInitialStateFilter(std::shared_ptr> const& model) const { - if (isSparseModel()) { - return std::make_unique(model->template as()->getInitialStates()); - } else { - return std::make_unique>(model->template as()->getReachableStates(), model->template as()->getInitialStates()); - } - } - }; - - typedef ::testing::Types< - SparseGmmxxGmresIluEnvironment, - JaniSparseGmmxxGmresIluEnvironment, - JitSparseGmmxxGmresIluEnvironment, - SparseGmmxxGmresDiagEnvironment, - SparseGmmxxBicgstabIluEnvironment, - SparseEigenDGmresEnvironment, - SparseEigenDoubleLUEnvironment, - SparseEigenRationalLUEnvironment, - SparseRationalEliminationEnvironment, - SparseNativeJacobiEnvironment, - SparseNativeWalkerChaeEnvironment, - SparseNativeSorEnvironment, - SparseNativePowerEnvironment, - SparseNativeSoundValueIterationEnvironment, - SparseNativeIntervalIterationEnvironment, - SparseNativeRationalSearchEnvironment, - SparseTopologicalEigenLUEnvironment, - HybridSylvanGmmxxGmresEnvironment, - HybridCuddNativeJacobiEnvironment, - HybridCuddNativeSoundValueIterationEnvironment, - HybridSylvanNativeRationalSearchEnvironment, - DdSylvanNativePowerEnvironment, - JaniDdSylvanNativePowerEnvironment, - DdCuddNativeJacobiEnvironment, - DdSylvanRationalSearchEnvironment - > TestingTypes; - - TYPED_TEST_SUITE(DtmcPrctlModelCheckerTest, TestingTypes); - - TYPED_TEST(DtmcPrctlModelCheckerTest, Die) { - std::string formulasString = "P=? [F \"one\"]"; - formulasString += "; P=? [F \"two\"]"; - formulasString += "; P=? [F \"three\"]"; - formulasString += "; R=? [F \"done\"]"; - - auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm", formulasString); - auto model = std::move(modelFormulas.first); - auto tasks = this->getTasks(modelFormulas.second); - EXPECT_EQ(13ul, model->getNumberOfStates()); - EXPECT_EQ(20ul, model->getNumberOfTransitions()); - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - auto checker = this->createModelChecker(model); - std::unique_ptr result; - - result = checker->check(this->env(), tasks[0]); - EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[1]); - EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[2]); - EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[3]); - EXPECT_NEAR(this->parseNumber("11/3"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - } - - TYPED_TEST(DtmcPrctlModelCheckerTest, Crowds) { - std::string formulasString = "P=? [F observe0>1]"; - formulasString += "; P=? [F \"observeIGreater1\"]"; - formulasString += "; P=? [F observe1>1]"; - - auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-4-3.pm", formulasString); - auto model = std::move(modelFormulas.first); - auto tasks = this->getTasks(modelFormulas.second); - EXPECT_EQ(726ul, model->getNumberOfStates()); - EXPECT_EQ(1146ul, model->getNumberOfTransitions()); - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - auto checker = this->createModelChecker(model); - std::unique_ptr result; - - result = checker->check(this->env(), tasks[0]); - EXPECT_NEAR(this->parseNumber("78686542099694893/1268858272000000000"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[1]); - EXPECT_NEAR(this->parseNumber("40300855878315123/1268858272000000000"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[2]); - EXPECT_NEAR(this->parseNumber("13433618626105041/1268858272000000000"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - } - - TYPED_TEST(DtmcPrctlModelCheckerTest, SynchronousLeader) { - std::string formulasString = "P=? [F \"elected\"]"; - formulasString += "; P=? [F<=5 \"elected\"]"; - formulasString += "; R=? [F \"elected\"]"; - - auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm", formulasString); - auto model = std::move(modelFormulas.first); - auto tasks = this->getTasks(modelFormulas.second); - EXPECT_EQ(273ul, model->getNumberOfStates()); - EXPECT_EQ(397ul, model->getNumberOfTransitions()); - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - auto checker = this->createModelChecker(model); - std::unique_ptr result; - - result = checker->check(this->env(), tasks[0]); - EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[1]); - EXPECT_NEAR(this->parseNumber("24/25"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[2]); - EXPECT_NEAR(this->parseNumber("25/24"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - } - - TEST(DtmcPrctlModelCheckerTest, AllUntilProbabilities) { - std::string formulasString = "P=? [F \"one\"]"; - formulasString += "; P=? [F \"two\"]"; - formulasString += "; P=? [F \"three\"]"; - - storm::prism::Program program = storm::api::parseProgram(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); - auto formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasString, program)); - std::vector> tasks; - for (auto const& f : formulas) { - tasks.emplace_back(*f); - } - auto model = storm::api::buildSparseModel(program, formulas)->template as>(); - EXPECT_EQ(13ul, model->getNumberOfStates()); - EXPECT_EQ(20ul, model->getNumberOfTransitions()); - - storm::storage::SparseMatrix matrix = model->getTransitionMatrix(); - storm::storage::BitVector initialStates(13); - initialStates.set(0); - storm::storage::BitVector phiStates(13); - storm::storage::BitVector psiStates(13); - psiStates.set(7); - psiStates.set(8); - psiStates.set(9); - psiStates.set(10); - psiStates.set(11); - psiStates.set(12); - storm::Environment env; - storm::solver::SolveGoal goal(*model, tasks[0]); - std::vector result = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeAllUntilProbabilities(env, std::move(goal), matrix, initialStates, phiStates, psiStates); - - EXPECT_NEAR(1.0/6, result[7], 1e-6); - EXPECT_NEAR(1.0/6, result[8], 1e-6); - EXPECT_NEAR(1.0/6, result[9], 1e-6); - EXPECT_NEAR(1.0/6, result[10], 1e-6); - EXPECT_NEAR(1.0/6, result[11], 1e-6); - EXPECT_NEAR(1.0/6, result[12], 1e-6); - - phiStates.set(6); - psiStates.set(1); - result = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeAllUntilProbabilities(env, std::move(goal), matrix, initialStates, phiStates, psiStates); - - EXPECT_NEAR(1, result[0], 1e-6); - EXPECT_NEAR(0.5, result[1], 1e-6); - EXPECT_NEAR(0.5, result[2], 1e-6); - EXPECT_NEAR(0.25, result[5], 1e-6); - EXPECT_NEAR(0, result[7], 1e-6); - EXPECT_NEAR(0, result[8], 1e-6); - EXPECT_NEAR(0, result[9], 1e-6); - EXPECT_NEAR(0.125, result[10], 1e-6); - EXPECT_NEAR(0.125, result[11], 1e-6); - EXPECT_NEAR(0, result[12], 1e-6); - } - -} diff --git a/src/test/storm/modelchecker/prctl/ExplicitDtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/ExplicitDtmcPrctlModelCheckerTest.cpp deleted file mode 100755 index 1ab3c07a7..000000000 --- a/src/test/storm/modelchecker/prctl/ExplicitDtmcPrctlModelCheckerTest.cpp +++ /dev/null @@ -1,158 +0,0 @@ -#include "test/storm_gtest.h" -#include "storm-config.h" - -#include "storm-parsers/parser/FormulaParser.h" -#include "storm/logic/Formulas.h" -#include "storm/models/sparse/StandardRewardModel.h" -#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" -#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/GeneralSettings.h" -#include "storm/settings/SettingMemento.h" -#include "storm-parsers/parser/AutoParser.h" -#include "storm-parsers/parser/PrismParser.h" -#include "storm/builder/ExplicitModelBuilder.h" -#include "storm/storage/expressions/ExpressionManager.h" - -#include "storm/environment/solver/SolverEnvironment.h" - -TEST(ExplicitDtmcPrctlModelCheckerTest, Die) { - std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/die.tra", STORM_TEST_RESOURCES_DIR "/lab/die.lab", "", STORM_TEST_RESOURCES_DIR "/rew/die.coin_flips.trans.rew"); - - storm::Environment env; - double const precision = 1e-6; - // Increase precision a little to get more accurate results - env.solver().setLinearEquationSolverPrecision(storm::utility::convertNumber(1e-8)); - - // A parser that we use for conveniently constructing the formulas. - - auto expManager = std::make_shared(); - storm::parser::FormulaParser formulaParser(expManager); - - ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = abstractModel->as>(); - - ASSERT_EQ(dtmc->getNumberOfStates(), 13ull); - ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull); - - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); - - std::unique_ptr result = checker.check(env, *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0 / 6.0, quantitativeResult1[0], precision); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]"); - - result = checker.check(env, *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0 / 6.0, quantitativeResult2[0], precision); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]"); - - result = checker.check(env, *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0 / 6.0, quantitativeResult3[0], precision); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]"); - - result = checker.check(env, *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(11.0 / 3.0, quantitativeResult4[0], precision); -} - -TEST(ExplicitDtmcPrctlModelCheckerTest, Crowds) { - - storm::Environment env; - double const precision = 1e-6; - // Increase precision a little to get more accurate results - env.solver().setLinearEquationSolverPrecision(storm::utility::convertNumber(1e-8)); - - - std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/crowds5_5.tra", STORM_TEST_RESOURCES_DIR "/lab/crowds5_5.lab", "", ""); - - ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); - - // A parser that we use for conveniently constructing the formulas. - - auto expManager = std::make_shared(); - storm::parser::FormulaParser formulaParser(expManager); - - std::shared_ptr> dtmc = abstractModel->as>(); - - ASSERT_EQ(8607ull, dtmc->getNumberOfStates()); - ASSERT_EQ(15113ull, dtmc->getNumberOfTransitions()); - - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); - - std::unique_ptr result = checker.check(env, *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.3328800375801578281, quantitativeResult1[0], precision); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]"); - - result = checker.check(env, *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.1522194965, quantitativeResult2[0], precision); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]"); - - result = checker.check(env, *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.32153724292835045, quantitativeResult3[0], precision); -} - -TEST(ExplicitDtmcPrctlModelCheckerTest, SynchronousLeader) { - storm::Environment env; - double const precision = 1e-6; - // Increase precision a little to get more accurate results - env.solver().setLinearEquationSolverPrecision(storm::utility::convertNumber(1e-8)); - - std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/leader4_8.tra", STORM_TEST_RESOURCES_DIR "/lab/leader4_8.lab", "", STORM_TEST_RESOURCES_DIR "/rew/leader4_8.pick.trans.rew"); - - ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); - - // A parser that we use for conveniently constructing the formulas. - - auto expManager = std::make_shared(); - storm::parser::FormulaParser formulaParser(expManager); - - std::shared_ptr> dtmc = abstractModel->as>(); - - ASSERT_EQ(12400ull, dtmc->getNumberOfStates()); - ASSERT_EQ(16495ull, dtmc->getNumberOfTransitions()); - - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); - - std::unique_ptr result = checker.check(env, *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0, quantitativeResult1[0], precision); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]"); - - result = checker.check(env, *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.9999965911265462636, quantitativeResult2[0], precision); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]"); - - result = checker.check(env, *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0448979591836789, quantitativeResult3[0], precision); -} diff --git a/src/test/storm/modelchecker/prctl/ExplicitMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/ExplicitMdpPrctlModelCheckerTest.cpp deleted file mode 100755 index f6502ae54..000000000 --- a/src/test/storm/modelchecker/prctl/ExplicitMdpPrctlModelCheckerTest.cpp +++ /dev/null @@ -1,199 +0,0 @@ -#include "test/storm_gtest.h" -#include "storm-config.h" - -#include "storm-parsers/parser/FormulaParser.h" -#include "storm/logic/Formulas.h" -#include "storm/solver/StandardMinMaxLinearEquationSolver.h" -#include "storm/models/sparse/StandardRewardModel.h" -#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" -#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" - -#include "storm/environment/solver/MinMaxSolverEnvironment.h" - -#include "storm-parsers/parser/AutoParser.h" -#include "storm-parsers/parser/PrismParser.h" -#include "storm/builder/ExplicitModelBuilder.h" - -TEST(ExplicitMdpPrctlModelCheckerTest, Dice) { - std::shared_ptr> 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"); - storm::Environment env; - double const precision = 1e-6; - // Increase precision a little to get more accurate results - env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-8)); - - // 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> mdp = abstractModel->as>(); - - ASSERT_EQ(mdp->getNumberOfStates(), 169ull); - ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); - - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); - - std::unique_ptr result = checker.check(env, *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0/36.0, quantitativeResult1[0], precision); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); - - result = checker.check(env, *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0/36.0, quantitativeResult2[0], precision); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); - - result = checker.check(env, *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(2.0/36.0, quantitativeResult3[0], precision); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); - - result = checker.check(env, *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(2.0/36.0, quantitativeResult4[0], precision); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); - - result = checker.check(env, *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(3.0/36.0, quantitativeResult5[0], precision); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); - - result = checker.check(env, *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(3.0/36.0, quantitativeResult6[0], precision); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); - - result = checker.check(env, *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult7 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(22.0/3.0, quantitativeResult7[0], precision); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); - - result = checker.check(env, *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult8 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(22.0/3.0, quantitativeResult8[0], precision); - - 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> stateRewardMdp = abstractModel->as>(); - - storm::modelchecker::SparseMdpPrctlModelChecker> stateRewardModelChecker(*mdp); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); - - result = stateRewardModelChecker.check(env, *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult9 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(22.0/3.0, quantitativeResult9[0], precision); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); - - result = stateRewardModelChecker.check(env, *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult10 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(22.0/3.0, quantitativeResult10[0], precision); - - 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> stateAndTransitionRewardMdp = abstractModel->as>(); - - storm::modelchecker::SparseMdpPrctlModelChecker> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); - - result = stateAndTransitionRewardModelChecker.check(env, *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult11 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(44.0/3.0, quantitativeResult11[0], precision); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); - - result = stateAndTransitionRewardModelChecker.check(env, *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult12 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(44.0/3.0, quantitativeResult12[0], precision); -} - -TEST(ExplicitMdpPrctlModelCheckerTest, AsynchronousLeader) { - storm::Environment env; - double const precision = 1e-6; - // Increase precision a little to get more accurate results - env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-8)); - - std::shared_ptr> 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> mdp = abstractModel->as>(); - - ASSERT_EQ(3172ull, mdp->getNumberOfStates()); - ASSERT_EQ(7144ull, mdp->getNumberOfTransitions()); - - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); - - std::unique_ptr result = checker.check(env, *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0, quantitativeResult1[0], precision); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); - - result = checker.check(env, *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0, quantitativeResult2[0], precision); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); - - result = checker.check(env, *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0/16.0, quantitativeResult3[0], precision); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); - - result = checker.check(env, *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0/16.0, quantitativeResult4[0], precision); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); - - result = checker.check(env, *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(30.0/7.0, quantitativeResult5[0], precision); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); - - result = checker.check(env, *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(30.0/7.0, quantitativeResult6[0], precision); -} - diff --git a/src/test/storm/modelchecker/prctl/LraDtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/LraDtmcPrctlModelCheckerTest.cpp deleted file mode 100755 index 9c7cf76f0..000000000 --- a/src/test/storm/modelchecker/prctl/LraDtmcPrctlModelCheckerTest.cpp +++ /dev/null @@ -1,268 +0,0 @@ -#include "test/storm_gtest.h" -#include "storm-config.h" -#include "test/storm_gtest.h" - -#include "storm-parsers/parser/FormulaParser.h" -#include "storm/settings/SettingMemento.h" -#include "storm/logic/Formulas.h" -#include "storm/solver/NativeLinearEquationSolver.h" -#include "storm/models/sparse/StandardRewardModel.h" -#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" -#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" -#include "storm/settings/SettingsManager.h" -#include "storm/solver/NativeLinearEquationSolver.h" -#include "storm/settings/modules/GeneralSettings.h" - -#include "storm/environment/solver/NativeSolverEnvironment.h" -#include "storm/environment/solver/EigenSolverEnvironment.h" -#include "storm/environment/solver/GmmxxSolverEnvironment.h" - -#include "storm-parsers/parser/AutoParser.h" -#include "storm/builder/ExplicitModelBuilder.h" - -namespace { - - class GmmxxDoubleGmresEnvironment { - public: - typedef double ValueType; - static const bool isExact = false; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx); - env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres); - env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu); - env.solver().gmmxx().setPrecision(storm::utility::convertNumber(1e-8)); - return env; - } - }; - - class EigenDoubleDGmresEnvironment { - public: - typedef double ValueType; - static const bool isExact = false; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen); - env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::DGmres); - env.solver().eigen().setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner::Ilu); - env.solver().eigen().setPrecision(storm::utility::convertNumber(1e-8)); - return env; - } - }; - - class EigenRationalLUEnvironment { - public: - typedef double ValueType; - static const bool isExact = true; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen); - env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU); - return env; - } - }; - - class NativeSorEnvironment { - public: - typedef double ValueType; - static const bool isExact = false; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native); - env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::SOR); - env.solver().native().setSorOmega(storm::utility::convertNumber(0.9)); - env.solver().native().setPrecision(storm::utility::convertNumber(1e-8)); - return env; - } - }; - - class NativeWalkerChaeEnvironment { - public: - typedef double ValueType; - static const bool isExact = false; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native); - env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::WalkerChae); - env.solver().native().setPrecision(storm::utility::convertNumber(1e-8)); - env.solver().native().setMaximalNumberOfIterations(50000); - return env; - } - }; - - template - class LraDtmcPrctlModelCheckerTest : public ::testing::Test { - public: - typedef typename TestType::ValueType ValueType; - LraDtmcPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {} - storm::Environment const& env() const { return _environment; } - ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber(input);} - ValueType precision() const { return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");} - - private: - storm::Environment _environment; - }; - - typedef ::testing::Types< - GmmxxDoubleGmresEnvironment, - EigenDoubleDGmresEnvironment, - EigenRationalLUEnvironment, - NativeSorEnvironment, - NativeWalkerChaeEnvironment - > TestingTypes; - - TYPED_TEST_SUITE(LraDtmcPrctlModelCheckerTest, TestingTypes); - - - - TYPED_TEST(LraDtmcPrctlModelCheckerTest, LRASingleBscc) { - typedef typename TestFixture::ValueType ValueType; - - storm::storage::SparseMatrixBuilder matrixBuilder; - std::shared_ptr> dtmc; - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - { - matrixBuilder = storm::storage::SparseMatrixBuilder(2, 2, 2); - matrixBuilder.addNextValue(0, 1, this->parseNumber("1")); - matrixBuilder.addNextValue(1, 0, this->parseNumber("1")); - storm::storage::SparseMatrix transitionMatrix = matrixBuilder.build(); - - storm::models::sparse::StateLabeling ap(2); - ap.addLabel("a"); - ap.addLabelToState("a", 1); - - dtmc.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap)); - - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); - - std::unique_ptr result = checker.check(this->env(), *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[0], this->precision()); - EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[1], this->precision()); - } - { - matrixBuilder = storm::storage::SparseMatrixBuilder(2, 2, 4); - matrixBuilder.addNextValue(0, 0, this->parseNumber("0.5")); - matrixBuilder.addNextValue(0, 1, this->parseNumber("0.5")); - matrixBuilder.addNextValue(1, 0, this->parseNumber("0.5")); - matrixBuilder.addNextValue(1, 1, this->parseNumber("0.5")); - storm::storage::SparseMatrix transitionMatrix = matrixBuilder.build(); - - storm::models::sparse::StateLabeling ap(2); - ap.addLabel("a"); - ap.addLabelToState("a", 1); - - dtmc.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap)); - - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); - - std::unique_ptr result = checker.check(this->env(), *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[0], this->precision()); - EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[1], this->precision()); - } - - { - matrixBuilder = storm::storage::SparseMatrixBuilder(3, 3, 3); - matrixBuilder.addNextValue(0, 1, this->parseNumber("1")); - matrixBuilder.addNextValue(1, 2, this->parseNumber("1")); - matrixBuilder.addNextValue(2, 0, this->parseNumber("1")); - storm::storage::SparseMatrix transitionMatrix = matrixBuilder.build(); - - storm::models::sparse::StateLabeling ap(3); - ap.addLabel("a"); - ap.addLabelToState("a", 2); - - dtmc.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap)); - - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); - - std::unique_ptr result = checker.check(this->env(), *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[0], this->precision()); - EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[1], this->precision()); - EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[2], this->precision()); - } - } - - TYPED_TEST(LraDtmcPrctlModelCheckerTest, LRA) { - typedef typename TestFixture::ValueType ValueType; - - storm::storage::SparseMatrixBuilder matrixBuilder; - std::shared_ptr> dtmc; - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - { - matrixBuilder = storm::storage::SparseMatrixBuilder(15, 15, 20, true); - matrixBuilder.addNextValue(0, 1, this->parseNumber("1")); - matrixBuilder.addNextValue(1, 4, this->parseNumber("0.7")); - matrixBuilder.addNextValue(1, 6, this->parseNumber("0.3")); - matrixBuilder.addNextValue(2, 0, this->parseNumber("1")); - - matrixBuilder.addNextValue(3, 5, this->parseNumber("0.8")); - matrixBuilder.addNextValue(3, 9, this->parseNumber("0.2")); - matrixBuilder.addNextValue(4, 3, this->parseNumber("1")); - matrixBuilder.addNextValue(5, 3, this->parseNumber("1")); - - matrixBuilder.addNextValue(6, 7, this->parseNumber("1")); - matrixBuilder.addNextValue(7, 8, this->parseNumber("1")); - matrixBuilder.addNextValue(8, 6, this->parseNumber("1")); - - matrixBuilder.addNextValue(9, 10, this->parseNumber("1")); - matrixBuilder.addNextValue(10, 9, this->parseNumber("1")); - matrixBuilder.addNextValue(11, 9, this->parseNumber("1")); - - matrixBuilder.addNextValue(12, 5, this->parseNumber("0.4")); - matrixBuilder.addNextValue(12, 8, this->parseNumber("0.3")); - matrixBuilder.addNextValue(12, 11, this->parseNumber("0.3")); - - matrixBuilder.addNextValue(13, 7, this->parseNumber("0.7")); - matrixBuilder.addNextValue(13, 12, this->parseNumber("0.3")); - - matrixBuilder.addNextValue(14, 12, this->parseNumber("1")); - - storm::storage::SparseMatrix transitionMatrix = matrixBuilder.build(); - - storm::models::sparse::StateLabeling ap(15); - ap.addLabel("a"); - ap.addLabelToState("a", 1); - ap.addLabelToState("a", 4); - ap.addLabelToState("a", 5); - ap.addLabelToState("a", 7); - ap.addLabelToState("a", 11); - ap.addLabelToState("a", 13); - ap.addLabelToState("a", 14); - - dtmc.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap)); - - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); - - std::unique_ptr result = checker.check(this->env(), *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(this->parseNumber("1/10"), quantitativeResult1[0], this->precision()); - EXPECT_NEAR(this->parseNumber("0"), quantitativeResult1[3], this->precision()); - EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[6], this->precision()); - EXPECT_NEAR(this->parseNumber("0"), quantitativeResult1[9], this->precision()); - EXPECT_NEAR(this->parseNumber("1/10"), quantitativeResult1[12], this->precision()); - EXPECT_NEAR(this->parseNumber("79/300"), quantitativeResult1[13], this->precision()); - EXPECT_NEAR(this->parseNumber("1/10"), quantitativeResult1[14], this->precision()); - } - } -} \ No newline at end of file diff --git a/src/test/storm/modelchecker/prctl/LraMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/LraMdpPrctlModelCheckerTest.cpp deleted file mode 100755 index e18f7640e..000000000 --- a/src/test/storm/modelchecker/prctl/LraMdpPrctlModelCheckerTest.cpp +++ /dev/null @@ -1,468 +0,0 @@ -#include "test/storm_gtest.h" - -#include "test/storm_gtest.h" - -#include "storm-config.h" - -#include "storm/api/builder.h" -#include "storm-conv/api/storm-conv.h" -#include "storm-parsers/api/model_descriptions.h" -#include "storm/api/properties.h" -#include "storm-parsers/api/properties.h" - -#include "storm-parsers/parser/FormulaParser.h" -#include "storm/logic/Formulas.h" -#include "storm/solver/StandardMinMaxLinearEquationSolver.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/settings/modules/NativeEquationSolverSettings.h" -#include "storm-parsers/parser/AutoParser.h" -#include "storm/environment/solver/MinMaxSolverEnvironment.h" - -namespace { - - - class SparseValueTypeValueIterationEnvironment { - public: - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::sparse::Mdp ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().minMax().setLraMethod(storm::solver::LraMethod::ValueIteration); - env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); - return env; - } - }; - - class SparseValueTypeLinearProgrammingEnvironment { - public: - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::sparse::Mdp ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().minMax().setLraMethod(storm::solver::LraMethod::LinearProgramming); - env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); - return env; - } - }; - - class SparseRationalLinearProgrammingEnvironment { - public: - static const bool isExact = true; - typedef storm::RationalNumber ValueType; - typedef storm::models::sparse::Mdp ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().minMax().setLraMethod(storm::solver::LraMethod::LinearProgramming); - return env; - } - }; - - template - class LraMdpPrctlModelCheckerTest : public ::testing::Test { - public: - typedef typename TestType::ValueType ValueType; - typedef typename storm::models::sparse::Mdp SparseModelType; - - LraMdpPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {} - storm::Environment const& env() const { return _environment; } - ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber(input);} - ValueType precision() const { return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");} - bool isSparseModel() const { return std::is_same::value; } - - std::pair, std::vector>> buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { - std::pair, std::vector>> result; - storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); - program = storm::utility::prism::preprocess(program, constantDefinitionString); - result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); - result.first = storm::api::buildSparseModel(program, result.second)->template as(); - return result; - } - - std::vector> getTasks(std::vector> const& formulas) const { - std::vector> result; - for (auto const& f : formulas) { - result.emplace_back(*f); - } - return result; - } - - private: - storm::Environment _environment; - }; - - typedef ::testing::Types< - SparseValueTypeValueIterationEnvironment, - SparseValueTypeLinearProgrammingEnvironment -#ifdef STORM_HAVE_Z3_OPTIMIZE - , SparseRationalLinearProgrammingEnvironment -#endif - > TestingTypes; - - TYPED_TEST_SUITE(LraMdpPrctlModelCheckerTest, TestingTypes); - - - TYPED_TEST(LraMdpPrctlModelCheckerTest, LRA_SingleMec) { - typedef typename TestFixture::ValueType ValueType; - - storm::storage::SparseMatrixBuilder matrixBuilder; - std::shared_ptr> mdp; - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - { - matrixBuilder = storm::storage::SparseMatrixBuilder(2, 2, 2); - matrixBuilder.addNextValue(0, 1, this->parseNumber("1")); - matrixBuilder.addNextValue(1, 0, this->parseNumber("1")); - storm::storage::SparseMatrix transitionMatrix = matrixBuilder.build(); - - storm::models::sparse::StateLabeling ap(2); - ap.addLabel("a"); - ap.addLabelToState("a", 1); - - mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); - - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); - - std::unique_ptr result = checker.check(this->env(), *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[0], this->precision()); - EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[1], this->precision()); - - formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]"); - - result = checker.check(this->env(), *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult2[0], this->precision()); - EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult2[1], this->precision()); - } - { - matrixBuilder = storm::storage::SparseMatrixBuilder(2, 2, 4); - matrixBuilder.addNextValue(0, 0, this->parseNumber("0.5")); - matrixBuilder.addNextValue(0, 1, this->parseNumber("0.5")); - matrixBuilder.addNextValue(1, 0, this->parseNumber("0.5")); - matrixBuilder.addNextValue(1, 1, this->parseNumber("0.5")); - storm::storage::SparseMatrix transitionMatrix = matrixBuilder.build(); - - storm::models::sparse::StateLabeling ap(2); - ap.addLabel("a"); - ap.addLabelToState("a", 1); - - mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); - - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); - - std::unique_ptr result = checker.check(this->env(), *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[0], this->precision()); - EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[1], this->precision()); - - formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]"); - - result = checker.check(this->env(), *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult2[0], this->precision()); - EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult2[1], this->precision()); - } - { - matrixBuilder = storm::storage::SparseMatrixBuilder(4, 3, 4, true, true, 3); - matrixBuilder.newRowGroup(0); - matrixBuilder.addNextValue(0, 1, this->parseNumber("1")); - matrixBuilder.newRowGroup(1); - matrixBuilder.addNextValue(1, 0, this->parseNumber("1")); - matrixBuilder.addNextValue(2, 2, this->parseNumber("1")); - matrixBuilder.newRowGroup(3); - matrixBuilder.addNextValue(3, 0, this->parseNumber("1")); - storm::storage::SparseMatrix transitionMatrix = matrixBuilder.build(); - - storm::models::sparse::StateLabeling ap(3); - ap.addLabel("a"); - ap.addLabelToState("a", 2); - ap.addLabel("b"); - ap.addLabelToState("b", 0); - ap.addLabel("c"); - ap.addLabelToState("c", 0); - ap.addLabelToState("c", 2); - - mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); - - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); - - std::unique_ptr result = checker.check(this->env(), *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[0], this->precision()); - EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[1], this->precision()); - EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[2], this->precision()); - - formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]"); - - result = checker.check(this->env(), *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[0], this->precision()); - EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[1], this->precision()); - EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[2], this->precision()); - - formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"b\"]"); - - result = checker.check(this->env(), *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult3[0], this->precision()); - EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult3[1], this->precision()); - EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult3[2], this->precision()); - - formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"b\"]"); - - result = checker.check(this->env(), *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult4[0], this->precision()); - EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult4[1], this->precision()); - EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult4[2], this->precision()); - - formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"c\"]"); - - result = checker.check(this->env(), *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(this->parseNumber("2/3"), quantitativeResult5[0], this->precision()); - EXPECT_NEAR(this->parseNumber("2/3"), quantitativeResult5[1], this->precision()); - EXPECT_NEAR(this->parseNumber("2/3"), quantitativeResult5[2], this->precision()); - - formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"c\"]"); - - result = checker.check(this->env(), *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult6[0], this->precision()); - EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult6[1], this->precision()); - EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult6[2], this->precision()); - } - } - - TYPED_TEST(LraMdpPrctlModelCheckerTest, LRA) { - typedef typename TestFixture::ValueType ValueType; - - storm::storage::SparseMatrixBuilder matrixBuilder; - std::shared_ptr> mdp; - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - { - matrixBuilder = storm::storage::SparseMatrixBuilder(4, 3, 4, true, true, 3); - matrixBuilder.newRowGroup(0); - matrixBuilder.addNextValue(0, 1, this->parseNumber("1")); - matrixBuilder.newRowGroup(1); - matrixBuilder.addNextValue(1, 1, this->parseNumber("1")); - matrixBuilder.addNextValue(2, 2, this->parseNumber("1")); - matrixBuilder.newRowGroup(3); - matrixBuilder.addNextValue(3, 2, this->parseNumber("1")); - storm::storage::SparseMatrix transitionMatrix = matrixBuilder.build(); - - storm::models::sparse::StateLabeling ap(3); - ap.addLabel("a"); - ap.addLabelToState("a", 0); - ap.addLabel("b"); - ap.addLabelToState("b", 1); - ap.addLabel("c"); - ap.addLabelToState("c", 2); - - mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); - - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); - - std::unique_ptr result = checker.check(this->env(), *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(this->parseNumber("0"), quantitativeResult1[0], this->precision()); - EXPECT_NEAR(this->parseNumber("0"), quantitativeResult1[1], this->precision()); - EXPECT_NEAR(this->parseNumber("0"), quantitativeResult1[2], this->precision()); - - formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]"); - - result = checker.check(this->env(), *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[0], this->precision()); - EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[1], this->precision()); - EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[2], this->precision()); - - formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"b\"]"); - - result = checker.check(this->env(), *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(this->parseNumber("1"), quantitativeResult3[0], this->precision()); - EXPECT_NEAR(this->parseNumber("1"), quantitativeResult3[1], this->precision()); - EXPECT_NEAR(this->parseNumber("0"), quantitativeResult3[2], this->precision()); - - formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"b\"]"); - - result = checker.check(this->env(), *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(this->parseNumber("0"), quantitativeResult4[0], this->precision()); - EXPECT_NEAR(this->parseNumber("0"), quantitativeResult4[1], this->precision()); - EXPECT_NEAR(this->parseNumber("0"), quantitativeResult4[2], this->precision()); - - formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"c\"]"); - - result = checker.check(this->env(), *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(this->parseNumber("1"), quantitativeResult5[0], this->precision()); - EXPECT_NEAR(this->parseNumber("1"), quantitativeResult5[1], this->precision()); - EXPECT_NEAR(this->parseNumber("1"), quantitativeResult5[2], this->precision()); - - formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"c\"]"); - - result = checker.check(this->env(), *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(this->parseNumber("0"), quantitativeResult6[0], this->precision()); - EXPECT_NEAR(this->parseNumber("0"), quantitativeResult6[1], this->precision()); - EXPECT_NEAR(this->parseNumber("1"), quantitativeResult6[2], this->precision()); - } - { - matrixBuilder = storm::storage::SparseMatrixBuilder(22, 15, 28, true, true, 15); - matrixBuilder.newRowGroup(0); - matrixBuilder.addNextValue(0, 1, this->parseNumber("1")); - matrixBuilder.newRowGroup(1); - matrixBuilder.addNextValue(1, 0, this->parseNumber("1")); - matrixBuilder.addNextValue(2, 2, this->parseNumber("1")); - matrixBuilder.addNextValue(3, 4, this->parseNumber("0.7")); - matrixBuilder.addNextValue(3, 6, this->parseNumber("0.3")); - matrixBuilder.newRowGroup(4); - matrixBuilder.addNextValue(4, 0, this->parseNumber("1")); - - matrixBuilder.newRowGroup(5); - matrixBuilder.addNextValue(5, 4, this->parseNumber("1")); - matrixBuilder.addNextValue(6, 5, this->parseNumber("0.8")); - matrixBuilder.addNextValue(6, 9, this->parseNumber("0.2")); - matrixBuilder.newRowGroup(7); - matrixBuilder.addNextValue(7, 3, this->parseNumber("1")); - matrixBuilder.addNextValue(8, 5, this->parseNumber("1")); - matrixBuilder.newRowGroup(9); - matrixBuilder.addNextValue(9, 3, this->parseNumber("1")); - - matrixBuilder.newRowGroup(10); - matrixBuilder.addNextValue(10, 7, this->parseNumber("1")); - matrixBuilder.newRowGroup(11); - matrixBuilder.addNextValue(11, 6, this->parseNumber("1")); - matrixBuilder.addNextValue(12, 8, this->parseNumber("1")); - matrixBuilder.newRowGroup(13); - matrixBuilder.addNextValue(13, 6, this->parseNumber("1")); - - matrixBuilder.newRowGroup(14); - matrixBuilder.addNextValue(14, 10, this->parseNumber("1")); - matrixBuilder.newRowGroup(15); - matrixBuilder.addNextValue(15, 9, this->parseNumber("1")); - matrixBuilder.addNextValue(16, 11, this->parseNumber("1")); - matrixBuilder.newRowGroup(17); - matrixBuilder.addNextValue(17, 9, this->parseNumber("1")); - - matrixBuilder.newRowGroup(18); - matrixBuilder.addNextValue(18, 5, this->parseNumber("0.4")); - matrixBuilder.addNextValue(18, 8, this->parseNumber("0.3")); - matrixBuilder.addNextValue(18, 11, this->parseNumber("0.3")); - - matrixBuilder.newRowGroup(19); - matrixBuilder.addNextValue(19, 7, this->parseNumber("0.7")); - matrixBuilder.addNextValue(19, 12, this->parseNumber("0.3")); - - matrixBuilder.newRowGroup(20); - matrixBuilder.addNextValue(20, 12, this->parseNumber("0.1")); - matrixBuilder.addNextValue(20, 13, this->parseNumber("0.9")); - matrixBuilder.addNextValue(21, 12, this->parseNumber("1")); - - storm::storage::SparseMatrix transitionMatrix = matrixBuilder.build(); - - storm::models::sparse::StateLabeling ap(15); - ap.addLabel("a"); - ap.addLabelToState("a", 1); - ap.addLabelToState("a", 4); - ap.addLabelToState("a", 5); - ap.addLabelToState("a", 7); - ap.addLabelToState("a", 11); - ap.addLabelToState("a", 13); - ap.addLabelToState("a", 14); - - mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); - - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); - - std::unique_ptr result = checker.check(this->env(), *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(this->parseNumber("37 / 60"), quantitativeResult1[0], this->precision()); - EXPECT_NEAR(this->parseNumber("2/3"), quantitativeResult1[3], this->precision()); - EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[6], this->precision()); - EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[9], this->precision()); - EXPECT_NEAR(this->parseNumber("31 / 60"), quantitativeResult1[12], this->precision()); - EXPECT_NEAR(this->parseNumber("101 / 200"), quantitativeResult1[13], this->precision()); - EXPECT_NEAR(this->parseNumber("31 / 60"), quantitativeResult1[14], this->precision()); - - formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]"); - - result = checker.check(this->env(), *formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(this->parseNumber("0.1"), quantitativeResult2[0], this->precision()); - EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[3], this->precision()); - EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult2[6], this->precision()); - EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[9], this->precision()); - EXPECT_NEAR(this->parseNumber("0.1"), quantitativeResult2[12], this->precision()); - EXPECT_NEAR(this->parseNumber("79 / 300"), quantitativeResult2[13], this->precision()); - EXPECT_NEAR(this->parseNumber("0.1"), quantitativeResult2[14], this->precision()); - } - } - - TYPED_TEST(LraMdpPrctlModelCheckerTest, cs_nfail) { - typedef typename TestFixture::ValueType ValueType; - - std::string formulasString = "R{\"grants\"}max=? [ MP ]"; - - auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/cs_nfail3.nm", formulasString); - auto model = std::move(modelFormulas.first); - auto tasks = this->getTasks(modelFormulas.second); - EXPECT_EQ(184ul, model->getNumberOfStates()); - EXPECT_EQ(541ul, model->getNumberOfTransitions()); - ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); - auto mdp = model->template as>(); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); - std::unique_ptr result; - - result = checker.check(this->env(), tasks[0]); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(this->parseNumber("333/1000"), quantitativeResult[*mdp->getInitialStates().begin()], this->precision()); - - } - - -} \ No newline at end of file diff --git a/src/test/storm/modelchecker/prctl/MdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/MdpPrctlModelCheckerTest.cpp deleted file mode 100755 index ecab40f54..000000000 --- a/src/test/storm/modelchecker/prctl/MdpPrctlModelCheckerTest.cpp +++ /dev/null @@ -1,607 +0,0 @@ -#include "test/storm_gtest.h" -#include "storm-config.h" - -#include "test/storm_gtest.h" - -#include "storm/api/builder.h" -#include "storm-conv/api/storm-conv.h" -#include "storm-parsers/api/model_descriptions.h" -#include "storm/api/properties.h" -#include "storm-parsers/api/properties.h" - -#include "storm/models/sparse/Mdp.h" -#include "storm/models/symbolic/Mdp.h" -#include "storm/models/sparse/StandardRewardModel.h" -#include "storm/models/symbolic/StandardRewardModel.h" -#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" -#include "storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h" -#include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h" -#include "storm/modelchecker/results/QuantitativeCheckResult.h" -#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" -#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" -#include "storm/modelchecker/results/QualitativeCheckResult.h" -#include "storm/environment/solver/MinMaxSolverEnvironment.h" -#include "storm/environment/solver/TopologicalSolverEnvironment.h" -#include "storm/settings/modules/CoreSettings.h" -#include "storm/logic/Formulas.h" -#include "storm/storage/jani/Property.h" -#include "storm/exceptions/UncheckedRequirementException.h" - -namespace { - - enum class MdpEngine {PrismSparse, JaniSparse, JitSparse, Hybrid, PrismDd, JaniDd}; - - class SparseDoubleValueIterationEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models - static const MdpEngine engine = MdpEngine::PrismSparse; - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::sparse::Mdp ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); - env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); - return env; - } - }; - - class JaniSparseDoubleValueIterationEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models - static const MdpEngine engine = MdpEngine::JaniSparse; - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::sparse::Mdp ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); - env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); - return env; - } - }; - - class JitSparseDoubleValueIterationEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models - static const MdpEngine engine = MdpEngine::JitSparse; - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::sparse::Mdp ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); - env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); - return env; - } - }; - - class SparseDoubleIntervalIterationEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models - static const MdpEngine engine = MdpEngine::PrismSparse; - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::sparse::Mdp ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setForceSoundness(true); - env.solver().minMax().setMethod(storm::solver::MinMaxMethod::IntervalIteration); - env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); - env.solver().minMax().setRelativeTerminationCriterion(false); - return env; - } - }; - class SparseDoubleSoundValueIterationEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models - static const MdpEngine engine = MdpEngine::PrismSparse; - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::sparse::Mdp ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setForceSoundness(true); - env.solver().minMax().setMethod(storm::solver::MinMaxMethod::SoundValueIteration); - env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); - env.solver().minMax().setRelativeTerminationCriterion(false); - return env; - } - }; - - class SparseDoubleTopologicalValueIterationEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models - static const MdpEngine engine = MdpEngine::PrismSparse; - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::sparse::Mdp ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().minMax().setMethod(storm::solver::MinMaxMethod::Topological); - env.solver().topological().setUnderlyingMinMaxMethod(storm::solver::MinMaxMethod::ValueIteration); - env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-8)); - env.solver().minMax().setRelativeTerminationCriterion(false); - return env; - } - }; - - class SparseDoubleTopologicalSoundValueIterationEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models - static const MdpEngine engine = MdpEngine::PrismSparse; - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::sparse::Mdp ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setForceSoundness(true); - env.solver().minMax().setMethod(storm::solver::MinMaxMethod::Topological); - env.solver().topological().setUnderlyingMinMaxMethod(storm::solver::MinMaxMethod::SoundValueIteration); - env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); - env.solver().minMax().setRelativeTerminationCriterion(false); - return env; - } - }; - - class SparseRationalPolicyIterationEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models - static const MdpEngine engine = MdpEngine::PrismSparse; - static const bool isExact = true; - typedef storm::RationalNumber ValueType; - typedef storm::models::sparse::Mdp ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration); - return env; - } - }; - - class SparseRationalViToPiEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models - static const MdpEngine engine = MdpEngine::PrismSparse; - static const bool isExact = true; - typedef storm::RationalNumber ValueType; - typedef storm::models::sparse::Mdp ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ViToPi); - return env; - } - }; - - class SparseRationalRationalSearchEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models - static const MdpEngine engine = MdpEngine::PrismSparse; - static const bool isExact = true; - typedef storm::RationalNumber ValueType; - typedef storm::models::sparse::Mdp ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().minMax().setMethod(storm::solver::MinMaxMethod::RationalSearch); - return env; - } - }; - class HybridCuddDoubleValueIterationEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::CUDD; - static const MdpEngine engine = MdpEngine::Hybrid; - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::symbolic::Mdp ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); - env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); - return env; - } - }; - class HybridSylvanDoubleValueIterationEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; - static const MdpEngine engine = MdpEngine::Hybrid; - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::symbolic::Mdp ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); - env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); - return env; - } - }; - class HybridCuddDoubleSoundValueIterationEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::CUDD; - static const MdpEngine engine = MdpEngine::Hybrid; - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::symbolic::Mdp ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setForceSoundness(true); - env.solver().minMax().setMethod(storm::solver::MinMaxMethod::SoundValueIteration); - env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); - env.solver().minMax().setRelativeTerminationCriterion(false); - return env; - } - }; - class HybridSylvanRationalPolicyIterationEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; - static const MdpEngine engine = MdpEngine::Hybrid; - static const bool isExact = true; - typedef storm::RationalNumber ValueType; - typedef storm::models::symbolic::Mdp ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration); - return env; - } - }; - class DdCuddDoubleValueIterationEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::CUDD; - static const MdpEngine engine = MdpEngine::PrismDd; - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::symbolic::Mdp ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); - env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); - return env; - } - }; - class JaniDdCuddDoubleValueIterationEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::CUDD; - static const MdpEngine engine = MdpEngine::JaniDd; - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::symbolic::Mdp ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); - env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); - return env; - } - }; - class DdSylvanDoubleValueIterationEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; - static const MdpEngine engine = MdpEngine::PrismDd; - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::symbolic::Mdp ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); - env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); - return env; - } - }; - class DdCuddDoublePolicyIterationEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::CUDD; - static const MdpEngine engine = MdpEngine::PrismDd; - static const bool isExact = false; - typedef double ValueType; - typedef storm::models::symbolic::Mdp ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration); - env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); - return env; - } - }; - class DdSylvanRationalRationalSearchEnvironment { - public: - static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; - static const MdpEngine engine = MdpEngine::PrismDd; - static const bool isExact = true; - typedef storm::RationalNumber ValueType; - typedef storm::models::symbolic::Mdp ModelType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().minMax().setMethod(storm::solver::MinMaxMethod::RationalSearch); - return env; - } - }; - - template - class MdpPrctlModelCheckerTest : public ::testing::Test { - public: - typedef typename TestType::ValueType ValueType; - typedef typename storm::models::sparse::Mdp SparseModelType; - typedef typename storm::models::symbolic::Mdp SymbolicModelType; - - MdpPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {} - storm::Environment const& env() const { return _environment; } - ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber(input);} - ValueType precision() const { return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");} - bool isSparseModel() const { return std::is_same::value; } - bool isSymbolicModel() const { return std::is_same::value; } - - template - typename std::enable_if::value, std::pair, std::vector>>>::type - buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { - std::pair, std::vector>> result; - storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); - program = storm::utility::prism::preprocess(program, constantDefinitionString); - if (TestType::engine == MdpEngine::PrismSparse) { - result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); - result.first = storm::api::buildSparseModel(program, result.second)->template as(); - } else if (TestType::engine == MdpEngine::JaniSparse || TestType::engine == MdpEngine::JitSparse) { - auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); - janiData.first.substituteFunctions(); - result.second = storm::api::extractFormulasFromProperties(janiData.second); - result.first = storm::api::buildSparseModel(janiData.first, result.second, TestType::engine == MdpEngine::JitSparse)->template as(); - } - return result; - } - - template - typename std::enable_if::value, std::pair, std::vector>>>::type - buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { - std::pair, std::vector>> result; - storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); - program = storm::utility::prism::preprocess(program, constantDefinitionString); - if (TestType::engine == MdpEngine::Hybrid || TestType::engine == MdpEngine::PrismDd) { - result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); - result.first = storm::api::buildSymbolicModel(program, result.second)->template as(); - } else if (TestType::engine == MdpEngine::JaniDd) { - auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); - janiData.first.substituteFunctions(); - result.second = storm::api::extractFormulasFromProperties(janiData.second); - result.first = storm::api::buildSymbolicModel(janiData.first, result.second)->template as(); - } - return result; - } - - std::vector> getTasks(std::vector> const& formulas) const { - std::vector> result; - for (auto const& f : formulas) { - result.emplace_back(*f); - } - return result; - } - - template - typename std::enable_if::value, std::shared_ptr>>::type - createModelChecker(std::shared_ptr const& model) const { - if (TestType::engine == MdpEngine::PrismSparse || TestType::engine == MdpEngine::JaniSparse || TestType::engine == MdpEngine::JitSparse) { - return std::make_shared>(*model); - } - } - - template - typename std::enable_if::value, std::shared_ptr>>::type - createModelChecker(std::shared_ptr const& model) const { - if (TestType::engine == MdpEngine::Hybrid) { - return std::make_shared>(*model); - } else if (TestType::engine == MdpEngine::PrismDd || TestType::engine == MdpEngine::JaniDd) { - return std::make_shared>(*model); - } - } - - bool getQualitativeResultAtInitialState(std::shared_ptr> const& model, std::unique_ptr& result) { - auto filter = getInitialStateFilter(model); - result->filter(*filter); - return result->asQualitativeCheckResult().forallTrue(); - } - - ValueType getQuantitativeResultAtInitialState(std::shared_ptr> const& model, std::unique_ptr& result) { - auto filter = getInitialStateFilter(model); - result->filter(*filter); - return result->asQuantitativeCheckResult().getMin(); - } - - private: - storm::Environment _environment; - - std::unique_ptr getInitialStateFilter(std::shared_ptr> const& model) const { - if (isSparseModel()) { - return std::make_unique(model->template as()->getInitialStates()); - } else { - return std::make_unique>(model->template as()->getReachableStates(), model->template as()->getInitialStates()); - } - } - }; - - typedef ::testing::Types< - SparseDoubleValueIterationEnvironment, - JaniSparseDoubleValueIterationEnvironment, - JitSparseDoubleValueIterationEnvironment, - SparseDoubleIntervalIterationEnvironment, - SparseDoubleSoundValueIterationEnvironment, - SparseDoubleTopologicalValueIterationEnvironment, - SparseDoubleTopologicalSoundValueIterationEnvironment, - SparseRationalPolicyIterationEnvironment, - SparseRationalViToPiEnvironment, - SparseRationalRationalSearchEnvironment, - HybridCuddDoubleValueIterationEnvironment, - HybridSylvanDoubleValueIterationEnvironment, - HybridCuddDoubleSoundValueIterationEnvironment, - HybridSylvanRationalPolicyIterationEnvironment, - DdCuddDoubleValueIterationEnvironment, - JaniDdCuddDoubleValueIterationEnvironment, - DdSylvanDoubleValueIterationEnvironment, - DdCuddDoublePolicyIterationEnvironment, - DdSylvanRationalRationalSearchEnvironment - > TestingTypes; - - TYPED_TEST_SUITE(MdpPrctlModelCheckerTest, TestingTypes); - - - TYPED_TEST(MdpPrctlModelCheckerTest, Dice) { - std::string formulasString = "Pmin=? [F \"two\"]"; - formulasString += "; Pmax=? [F \"two\"]"; - formulasString += "; Pmin=? [F \"three\"]"; - formulasString += "; Pmax=? [F \"three\"]"; - formulasString += "; Pmin=? [F \"four\"]"; - formulasString += "; Pmax=? [F \"four\"]"; - formulasString += "; Rmin=? [F \"done\"]"; - formulasString += "; Rmax=? [F \"done\"]"; - - auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm", formulasString); - auto model = std::move(modelFormulas.first); - auto tasks = this->getTasks(modelFormulas.second); - EXPECT_EQ(169ul, model->getNumberOfStates()); - EXPECT_EQ(436ul, model->getNumberOfTransitions()); - ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); - auto checker = this->createModelChecker(model); - std::unique_ptr result; - - result = checker->check(this->env(), tasks[0]); - EXPECT_NEAR(this->parseNumber("1/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[1]); - EXPECT_NEAR(this->parseNumber("1/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[2]); - EXPECT_NEAR(this->parseNumber("2/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[3]); - EXPECT_NEAR(this->parseNumber("2/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[4]); - EXPECT_NEAR(this->parseNumber("3/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[5]); - EXPECT_NEAR(this->parseNumber("3/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[6]); - EXPECT_NEAR(this->parseNumber("22/3"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[7]); - EXPECT_NEAR(this->parseNumber("22/3"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - } - - TYPED_TEST(MdpPrctlModelCheckerTest, AsynchronousLeader) { - std::string formulasString = "Pmin=? [F \"elected\"]"; - formulasString += "; Pmax=? [F \"elected\"]"; - formulasString += "; Pmin=? [F<=25 \"elected\"]"; - formulasString += "; Pmax=? [F<=25 \"elected\"]"; - formulasString += "; Rmin=? [F \"elected\"]"; - formulasString += "; Rmax=? [F \"elected\"]"; - - auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/leader4.nm", formulasString); - auto model = std::move(modelFormulas.first); - auto tasks = this->getTasks(modelFormulas.second); - EXPECT_EQ(3172ul, model->getNumberOfStates()); - EXPECT_EQ(7144ul, model->getNumberOfTransitions()); - ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); - auto checker = this->createModelChecker(model); - std::unique_ptr result; - - - result = checker->check(this->env(), tasks[0]); - EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[1]); - EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[2]); - EXPECT_NEAR(this->parseNumber("1/16"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[3]); - EXPECT_NEAR(this->parseNumber("1/16"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[4]); - EXPECT_NEAR(this->parseNumber("30/7"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[5]); - EXPECT_NEAR(this->parseNumber("30/7"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - } - - TYPED_TEST(MdpPrctlModelCheckerTest, consensus) { - std::string formulasString = "Pmax=? [F \"finished\"]"; - formulasString += "; Pmax=? [F \"all_coins_equal_1\"]"; - formulasString += "; P<0.8 [F \"all_coins_equal_1\"]"; - formulasString += "; P<0.9 [F \"all_coins_equal_1\"]"; - formulasString += "; Rmax=? [F \"all_coins_equal_1\"]"; - formulasString += "; Rmin=? [F \"all_coins_equal_1\"]"; - formulasString += "; Rmax=? [F \"finished\"]"; - formulasString += "; Rmin=? [F \"finished\"]"; - - auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm", formulasString); - auto model = std::move(modelFormulas.first); - auto tasks = this->getTasks(modelFormulas.second); - EXPECT_EQ(272ul, model->getNumberOfStates()); - EXPECT_EQ(492ul, model->getNumberOfTransitions()); - ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); - auto checker = this->createModelChecker(model); - std::unique_ptr result; - - result = checker->check(this->env(), tasks[0]); - EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[1]); - EXPECT_NEAR(this->parseNumber("57/64"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[2]); - EXPECT_FALSE(this->getQualitativeResultAtInitialState(model, result)); - - result = checker->check(this->env(), tasks[3]); - EXPECT_TRUE(this->getQualitativeResultAtInitialState(model, result)); - - result = checker->check(this->env(), tasks[4]); - EXPECT_TRUE(storm::utility::isInfinity(this->getQuantitativeResultAtInitialState(model, result))); - - result = checker->check(this->env(), tasks[5]); - EXPECT_TRUE(storm::utility::isInfinity(this->getQuantitativeResultAtInitialState(model, result))); - - result = checker->check(this->env(), tasks[6]); - EXPECT_NEAR(this->parseNumber("75"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[7]); - EXPECT_NEAR(this->parseNumber("48"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - } - - TYPED_TEST(MdpPrctlModelCheckerTest, TinyRewards) { - std::string formulasString = "Rmin=? [F \"target\"]"; - auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/tiny_rewards.nm", formulasString); - auto model = std::move(modelFormulas.first); - auto tasks = this->getTasks(modelFormulas.second); - EXPECT_EQ(3ul, model->getNumberOfStates()); - EXPECT_EQ(4ul, model->getNumberOfTransitions()); - ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); - auto checker = this->createModelChecker(model); - std::unique_ptr result; - - // This example considers a zero-reward end component that does not reach the target - // For some methods this requires end-component elimination which is (currently) not supported in the Dd engine - - if (TypeParam::engine == MdpEngine::PrismDd && this->env().solver().minMax().getMethod() == storm::solver::MinMaxMethod::RationalSearch) { - STORM_SILENT_EXPECT_THROW(checker->check(this->env(), tasks[0]), storm::exceptions::UncheckedRequirementException); - } else { - result = checker->check(this->env(), tasks[0]); - EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - } - } - - TYPED_TEST(MdpPrctlModelCheckerTest, Team) { - std::string formulasString = "R{\"w_1_total\"}max=? [ C ]"; - auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/multiobj_team3.nm", formulasString); - auto model = std::move(modelFormulas.first); - auto tasks = this->getTasks(modelFormulas.second); - EXPECT_EQ(12475ul, model->getNumberOfStates()); - EXPECT_EQ(15228ul, model->getNumberOfTransitions()); - ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); - auto checker = this->createModelChecker(model); - std::unique_ptr result; - - // This example considers an expected total reward formula, which is not supported in all engines - - if (TypeParam::engine == MdpEngine::PrismSparse || TypeParam::engine == MdpEngine::JaniSparse || TypeParam::engine == MdpEngine::JitSparse) { - result = checker->check(this->env(), tasks[0]); - EXPECT_NEAR(this->parseNumber("114/49"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - } else { - EXPECT_FALSE(checker->canHandle(tasks[0])); - } - } -} diff --git a/src/test/storm/modelchecker/prctl/QuantileQueryTest.cpp b/src/test/storm/modelchecker/prctl/QuantileQueryTest.cpp deleted file mode 100755 index cbd67db56..000000000 --- a/src/test/storm/modelchecker/prctl/QuantileQueryTest.cpp +++ /dev/null @@ -1,302 +0,0 @@ -#include "test/storm_gtest.h" -#include "storm-config.h" - -#include "test/storm_gtest.h" - -#include "storm/api/builder.h" -#include "storm-parsers/api/model_descriptions.h" -#include "storm/api/properties.h" -#include "storm-parsers/api/properties.h" -#include "storm/parser/CSVParser.h" - -#include "storm/models/sparse/Mdp.h" -#include "storm/models/sparse/StandardRewardModel.h" -#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" -#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" -#include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h" -#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" -#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" -#include "storm/environment/solver/MinMaxSolverEnvironment.h" -#include "storm/logic/Formulas.h" -#include "storm/storage/jani/Property.h" - -namespace { - - enum class MdpEngine {PrismSparse, JaniSparse, JitSparse, Hybrid, PrismDd, JaniDd}; - - class UnsoundEnvironment { - public: - typedef double ValueType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); - return env; - } - }; - - class SoundEnvironment { - public: - typedef double ValueType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().setForceSoundness(true); - return env; - } - }; - - class ExactEnvironment { - public: - typedef storm::RationalNumber ValueType; - static storm::Environment createEnvironment() { - storm::Environment env; - return env; - } - }; - - template - class QuantileQueryTest : public ::testing::Test { - public: - typedef typename TestType::ValueType ValueType; - QuantileQueryTest() : _environment(TestType::createEnvironment()) {} - storm::Environment const& env() const { return _environment; } - ValueType parseNumber(std::string const& input) const { - if (input.find("inf") != std::string::npos) { - return storm::utility::infinity(); - } - return storm::utility::convertNumber(input); - } - - template - std::pair, std::vector>> buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { - std::pair, std::vector>> result; - storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); - program = storm::utility::prism::preprocess(program, constantDefinitionString); - result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); - result.first = storm::api::buildSparseModel(program, result.second)->template as(); - return result; - } - - std::vector> getTasks(std::vector> const& formulas) const { - std::vector> result; - for (auto const& f : formulas) { - result.emplace_back(*f, true); // only initial states are relevant - } - return result; - } - - template - typename std::enable_if>::value, std::shared_ptr>>::type - createModelChecker(std::shared_ptr const& model) const { - return std::make_shared>(*model); - } - template - typename std::enable_if>::value, std::shared_ptr>>::type - createModelChecker(std::shared_ptr const& model) const { - return std::make_shared>(*model); - } - - std::pair compareResult(std::shared_ptr> const& model, std::unique_ptr& result, std::vector const& expected) { - bool equal = true; - std::string errorMessage = ""; - auto filter = getInitialStateFilter(model); - result->filter(*filter); - std::vector> resultPoints; - if (result->isExplicitParetoCurveCheckResult()) { - resultPoints = result->asExplicitParetoCurveCheckResult().getPoints(); - } else { - if (!result->isExplicitQuantitativeCheckResult()) { - return { false, "The CheckResult has unexpected type."}; - } - resultPoints = {{ result->asExplicitQuantitativeCheckResult().getMax() }}; - } - std::vector> expectedPoints; - for (auto const& pointAsString : expected) { - std::vector point; - for (auto const& entry : storm::parser::parseCommaSeperatedValues(pointAsString)) { - point.push_back(parseNumber(entry)); - } - expectedPoints.push_back(std::move(point)); - } - for (auto const& resPoint : resultPoints) { - bool contained = false; - for (auto const& expPoint : expectedPoints) { - if (resPoint == expPoint) { - contained = true; - break; - } - } - if (!contained) { - equal = false; - errorMessage += "The result " + storm::utility::vector::toString(resPoint) + " is not contained in the expected solution. "; - } - } - for (auto const& expPoint : expectedPoints) { - bool contained = false; - for (auto const& resPoint : resultPoints) { - if (resPoint == expPoint) { - contained = true; - break; - } - } - if (!contained) { - equal = false; - errorMessage += "The expected " + storm::utility::vector::toString(expPoint) + " is not contained in the obtained solution. "; - } - } - return {equal, errorMessage}; - } - - private: - storm::Environment _environment; - - std::unique_ptr getInitialStateFilter(std::shared_ptr> const& model) const { - return std::make_unique(model->getInitialStates()); - } - }; - - typedef ::testing::Types< - UnsoundEnvironment, - SoundEnvironment, - ExactEnvironment - > TestingTypes; - - TYPED_TEST_SUITE(QuantileQueryTest, TestingTypes); - - - TYPED_TEST(QuantileQueryTest, simple_Dtmc) { - typedef storm::models::sparse::Dtmc ModelType; - - std::string formulasString = "quantile(max A, max B, P>0.95 [F{\"first\"}<=A,{\"second\"}<=B s=3]);\n"; - - auto modelFormulas = this->template buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/quantiles_simple_dtmc.pm", formulasString); - auto model = std::move(modelFormulas.first); - auto tasks = this->getTasks(modelFormulas.second); - EXPECT_EQ(4ul, model->getNumberOfStates()); - EXPECT_EQ(6ul, model->getNumberOfTransitions()); - auto checker = this->template createModelChecker(model); - std::unique_ptr result; - std::vector expectedResult; - std::pair compare; - uint64_t taskId = 0; - - expectedResult.clear(); - expectedResult.push_back("7, 18"); - expectedResult.push_back("8, 16"); - expectedResult.push_back("9, 14"); - result = checker->check(this->env(), tasks[taskId++]); - compare = this->compareResult(model, result, expectedResult); - EXPECT_TRUE(compare.first) << compare.second; - } - - TYPED_TEST(QuantileQueryTest, simple_Mdp) { - typedef storm::models::sparse::Mdp ModelType; - - std::string formulasString = "quantile(B1, B2, Pmax>0.5 [F{\"first\"}>=B1,{\"second\"}>=B2 s=1]);\n"; - formulasString += "quantile(B1, B2, Pmax>0.5 [F{\"first\"}<=B1,{\"second\"}<=B2 s=1]);\n"; - formulasString += "quantile(B1, B2, Pmin>0.5 [F{\"first\"}<=B1,{\"second\"}<=B2 s=1]);\n"; - formulasString += "quantile(B1, Pmax>0.5 [F{\"second\"}>=B1 s=1]);\n"; - formulasString += "quantile(B1, B2, B3, Pmax>0.5 [F{\"first\"}<=B1,{\"second\"}<=B2,{\"third\"}<=B3 s=1]);\n"; - - auto modelFormulas = this->template buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/quantiles_simple_mdp.nm", formulasString); - auto model = std::move(modelFormulas.first); - auto tasks = this->getTasks(modelFormulas.second); - EXPECT_EQ(7ul, model->getNumberOfStates()); - EXPECT_EQ(13ul, model->getNumberOfTransitions()); - auto checker = this->template createModelChecker(model); - std::unique_ptr result; - std::vector expectedResult; - std::pair compare; - uint64_t taskId = 0; - - expectedResult.clear(); - expectedResult.push_back(" 0, 6"); - expectedResult.push_back(" 1, 5"); - expectedResult.push_back(" 2, 4"); - expectedResult.push_back(" 3, 3"); - expectedResult.push_back("inf, 2"); - result = checker->check(this->env(), tasks[taskId++]); - compare = this->compareResult(model, result, expectedResult); - EXPECT_TRUE(compare.first) << compare.second; - - expectedResult.clear(); - expectedResult.push_back(" 0, 2"); - expectedResult.push_back(" 5, 1"); - expectedResult.push_back(" 6, 0"); - result = checker->check(this->env(), tasks[taskId++]); - compare = this->compareResult(model, result, expectedResult); - EXPECT_TRUE(compare.first) << compare.second; - - expectedResult.clear(); - result = checker->check(this->env(), tasks[taskId++]); - compare = this->compareResult(model, result, expectedResult); - EXPECT_TRUE(compare.first) << compare.second; - - expectedResult.clear(); - expectedResult.push_back(" 6"); - result = checker->check(this->env(), tasks[taskId++]); - compare = this->compareResult(model, result, expectedResult); - EXPECT_TRUE(compare.first) << compare.second; - - expectedResult.clear(); - expectedResult.push_back(" 0, 2, 1.4"); - expectedResult.push_back(" 5, 1, 9.8"); - expectedResult.push_back(" 6, 0, 9.8"); - result = checker->check(this->env(), tasks[taskId++]); - compare = this->compareResult(model, result, expectedResult); - EXPECT_TRUE(compare.first) << compare.second; - } - - TYPED_TEST(QuantileQueryTest, firewire) { - typedef storm::models::sparse::Mdp ModelType; - - std::string formulasString = "quantile(min TIME, min ROUNDS, Pmax>0.95 [F{\"time\"}<=TIME,{\"rounds\"}<=ROUNDS \"done\"]);\n"; - - auto modelFormulas = this->template buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/quantiles_firewire.nm", formulasString, "delay=36"); - auto model = std::move(modelFormulas.first); - auto tasks = this->getTasks(modelFormulas.second); - EXPECT_EQ(776ul, model->getNumberOfStates()); - EXPECT_EQ(1411ul, model->getNumberOfTransitions()); - auto checker = this->template createModelChecker(model); - std::unique_ptr result; - std::vector expectedResult; - std::pair compare; - uint64_t taskId = 0; - - expectedResult.clear(); - expectedResult.push_back("123, 1"); - result = checker->check(this->env(), tasks[taskId++]); - compare = this->compareResult(model, result, expectedResult); - EXPECT_TRUE(compare.first) << compare.second; - - } - - TYPED_TEST(QuantileQueryTest, resources) { - typedef storm::models::sparse::Mdp ModelType; - - std::string formulasString = "quantile(max GOLD, max GEM, Pmax>0.95 [F{\"gold\"}>=GOLD,{\"gem\"}>=GEM,{\"steps\"}<=100 true]);\n"; - - auto modelFormulas = this->template buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/quantiles_resources.nm", formulasString); - auto model = std::move(modelFormulas.first); - auto tasks = this->getTasks(modelFormulas.second); - EXPECT_EQ(94ul, model->getNumberOfStates()); - EXPECT_EQ(326ul, model->getNumberOfTransitions()); - auto checker = this->template createModelChecker(model); - std::unique_ptr result; - std::vector expectedResult; - std::pair compare; - uint64_t taskId = 0; - - expectedResult.clear(); - expectedResult.push_back("0, 10"); - expectedResult.push_back("1, 9"); - expectedResult.push_back("4, 8"); - expectedResult.push_back("7, 7"); - expectedResult.push_back("8, 4"); - expectedResult.push_back("9, 2"); - expectedResult.push_back("10, 0"); - result = checker->check(this->env(), tasks[taskId++]); - compare = this->compareResult(model, result, expectedResult); - EXPECT_TRUE(compare.first) << compare.second; - - } -} diff --git a/src/test/storm/modelchecker/prctl/SchedulerGenerationMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/SchedulerGenerationMdpPrctlModelCheckerTest.cpp deleted file mode 100755 index 52498f641..000000000 --- a/src/test/storm/modelchecker/prctl/SchedulerGenerationMdpPrctlModelCheckerTest.cpp +++ /dev/null @@ -1,142 +0,0 @@ -#include "test/storm_gtest.h" -#include "storm-config.h" - -#include "storm-parsers/parser/FormulaParser.h" -#include "storm/logic/Formulas.h" -#include "storm/solver/StandardMinMaxLinearEquationSolver.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/environment/solver/MinMaxSolverEnvironment.h" - -#include "storm-parsers/parser/AutoParser.h" -#include "storm-parsers/parser/PrismParser.h" -#include "storm/builder/ExplicitModelBuilder.h" - -namespace { - class DoubleViEnvironment { - public: - typedef double ValueType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); - env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-8)); - return env; - } - }; - class DoubleSoundViEnvironment { - public: - typedef double ValueType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); - env.solver().setForceSoundness(true); - env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); - return env; - } - }; - class DoublePIEnvironment { - public: - typedef double ValueType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration); - env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-8)); - return env; - } - }; - class RationalPIEnvironment { - public: - typedef storm::RationalNumber ValueType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration); - return env; - } - }; - // class RationalRationalSearchEnvironment { - // public: - // typedef storm::RationalNumber ValueType; - // static storm::Environment createEnvironment() { - // storm::Environment env; - // env.solver().minMax().setMethod(storm::solver::MinMaxMethod::RationalSearch); - // return env; - // } - // }; - - template - class SchedulerGenerationMdpPrctlModelCheckerTest : public ::testing::Test { - public: - typedef typename TestType::ValueType ValueType; - SchedulerGenerationMdpPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {} - storm::Environment const& env() const { return _environment; } - private: - storm::Environment _environment; - }; - - typedef ::testing::Types< - DoubleViEnvironment, - DoubleSoundViEnvironment, - DoublePIEnvironment, - RationalPIEnvironment - //RationalRationalSearchEnvironment - > TestingTypes; - - TYPED_TEST_SUITE(SchedulerGenerationMdpPrctlModelCheckerTest, TestingTypes); - - - TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, reachability) { - typedef typename TestFixture::ValueType ValueType; - - 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> model = storm::builder::ExplicitModelBuilder(program, options).build(); - EXPECT_EQ(4ull, model->getNumberOfStates()); - EXPECT_EQ(11ull, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); - - std::shared_ptr> mdp = model->template as>(); - - EXPECT_EQ(7ull, mdp->getNumberOfChoices()); - - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"target\"]"); - - storm::modelchecker::CheckTask checkTask(*formula); - checkTask.setProduceSchedulers(true); - - std::unique_ptr result = checker.check(this->env(), checkTask); - - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - ASSERT_TRUE(result->asExplicitQuantitativeCheckResult().hasScheduler()); - storm::storage::Scheduler const& scheduler = result->asExplicitQuantitativeCheckResult().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(*formula); - checkTask.setProduceSchedulers(true); - result = checker.check(checkTask); - - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - ASSERT_TRUE(result->asExplicitQuantitativeCheckResult().hasScheduler()); - storm::storage::Scheduler const& scheduler2 = result->asExplicitQuantitativeCheckResult().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()); - } -} \ No newline at end of file