diff --git a/src/test/storm/modelchecker/prctl/dtmc/ConditionalDtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/dtmc/ConditionalDtmcPrctlModelCheckerTest.cpp new file mode 100755 index 000000000..fd124f456 --- /dev/null +++ b/src/test/storm/modelchecker/prctl/dtmc/ConditionalDtmcPrctlModelCheckerTest.cpp @@ -0,0 +1,170 @@ +#include "gtest/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_CASE(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/dtmc/DtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp new file mode 100755 index 000000000..6c5f08c86 --- /dev/null +++ b/src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp @@ -0,0 +1,701 @@ +#include "gtest/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_CASE(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/dtmc/ExplicitDtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/dtmc/ExplicitDtmcPrctlModelCheckerTest.cpp new file mode 100755 index 000000000..025bc8c45 --- /dev/null +++ b/src/test/storm/modelchecker/prctl/dtmc/ExplicitDtmcPrctlModelCheckerTest.cpp @@ -0,0 +1,158 @@ +#include "gtest/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/dtmc/LraDtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/dtmc/LraDtmcPrctlModelCheckerTest.cpp new file mode 100755 index 000000000..c964628b9 --- /dev/null +++ b/src/test/storm/modelchecker/prctl/dtmc/LraDtmcPrctlModelCheckerTest.cpp @@ -0,0 +1,268 @@ +#include "gtest/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_CASE(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/mdp/ExplicitMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/ExplicitMdpPrctlModelCheckerTest.cpp new file mode 100755 index 000000000..b295c397b --- /dev/null +++ b/src/test/storm/modelchecker/prctl/mdp/ExplicitMdpPrctlModelCheckerTest.cpp @@ -0,0 +1,199 @@ +#include "gtest/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/mdp/LraMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/LraMdpPrctlModelCheckerTest.cpp new file mode 100755 index 000000000..c0f527bd2 --- /dev/null +++ b/src/test/storm/modelchecker/prctl/mdp/LraMdpPrctlModelCheckerTest.cpp @@ -0,0 +1,468 @@ +#include "gtest/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_CASE(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/mdp/MdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp new file mode 100755 index 000000000..939cf4275 --- /dev/null +++ b/src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp @@ -0,0 +1,607 @@ +#include "gtest/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_CASE(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) { + 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/mdp/QuantileQueryTest.cpp b/src/test/storm/modelchecker/prctl/mdp/QuantileQueryTest.cpp new file mode 100755 index 000000000..c6c718856 --- /dev/null +++ b/src/test/storm/modelchecker/prctl/mdp/QuantileQueryTest.cpp @@ -0,0 +1,302 @@ +#include "gtest/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_CASE(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/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp new file mode 100755 index 000000000..6f82d6a47 --- /dev/null +++ b/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp @@ -0,0 +1,142 @@ +#include "gtest/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_CASE(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