diff --git a/src/test/storm/modelchecker/ConditionalDtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/ConditionalDtmcPrctlModelCheckerTest.cpp new file mode 100644 index 000000000..a0377209c --- /dev/null +++ b/src/test/storm/modelchecker/ConditionalDtmcPrctlModelCheckerTest.cpp @@ -0,0 +1,170 @@ +#include "gtest/gtest.h" +#include "test/storm_gtest.h" +#include "storm-config.h" + +#include "storm/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/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 storm::RationalNumber 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 storm::RationalNumber 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/CtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp new file mode 100644 index 000000000..47a3f5e5b --- /dev/null +++ b/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp @@ -0,0 +1,366 @@ +#include "gtest/gtest.h" +#include "test/storm_gtest.h" +#include "storm-config.h" + +#include "storm/api/builder.h" +#include "storm/api/model_descriptions.h" +#include "storm/api/properties.h" +#include "storm/parser/FormulaParser.h" +#include "storm/logic/Formulas.h" +#include "storm/solver/EigenLinearEquationSolver.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/models/sparse/Ctmc.h" +#include "storm/models/symbolic/Ctmc.h" +#include "storm/modelchecker/csl/SparseCtmcCslModelChecker.h" +#include "storm/modelchecker/csl/HybridCtmcCslModelChecker.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/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" + +namespace { + + class SparseGmmxxGmresIluEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models + static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Ctmc 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 SparseEigenDGmresEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models + static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Ctmc 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 storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Ctmc 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 SparseNativeSorEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models + static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Ctmc 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)); + env.solver().native().setRelativeTerminationCriterion(false); + env.solver().native().setMaximalNumberOfIterations(5000000); + return env; + } + }; + + class HybridCuddGmmxxGmresEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::CUDD; + static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Hybrid; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::symbolic::Ctmc 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 HybridSylvanGmmxxGmresEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; + static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Hybrid; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::symbolic::Ctmc 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; + } + }; + + template + class CtmcCslModelCheckerTest : public ::testing::Test { + public: + typedef typename TestType::ValueType ValueType; + typedef typename storm::models::sparse::Ctmc SparseModelType; + typedef typename storm::models::symbolic::Ctmc SymbolicModelType; + + CtmcCslModelCheckerTest() : _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, true); + 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; + } + + 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, true); + program = storm::utility::prism::preprocess(program, constantDefinitionString); + result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + result.first = storm::api::buildSymbolicModel(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; + } + + template + typename std::enable_if::value, std::shared_ptr>>::type + createModelChecker(std::shared_ptr const& model) const { + if (TestType::engine == storm::settings::modules::CoreSettings::Engine::Sparse) { + 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 == storm::settings::modules::CoreSettings::Engine::Hybrid) { + 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, + SparseEigenDGmresEnvironment, + SparseEigenDoubleLUEnvironment, + SparseNativeSorEnvironment, + HybridCuddGmmxxGmresEnvironment, + HybridSylvanGmmxxGmresEnvironment + > TestingTypes; + + TYPED_TEST_CASE(CtmcCslModelCheckerTest, TestingTypes); + + TYPED_TEST(CtmcCslModelCheckerTest, Cluster) { + std::string formulasString = "P=? [ F<=100 !\"minimum\"]"; + formulasString += "; P=? [ F[100,100] !\"minimum\"]"; + formulasString += "; P=? [ F[100,2000] !\"minimum\"]"; + formulasString += "; P=? [ \"minimum\" U<=10 \"premium\"]"; + formulasString += "; P=? [ !\"minimum\" U>=1 \"minimum\"]"; + formulasString += "; P=? [ \"minimum\" U>=1 !\"minimum\"]"; + formulasString += "; R=? [C<=100]"; + formulasString += "; LRA=? [\"minimum\"]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(276ul, model->getNumberOfStates()); + EXPECT_EQ(1120ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc); + auto checker = this->createModelChecker(model); + std::unique_ptr result; + + result = checker->check(this->env(), tasks[0]); + EXPECT_NEAR(this->parseNumber("5.5461254704419085E-5"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[1]); + EXPECT_NEAR(this->parseNumber("2.3397873548343415E-6"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[2]); + EXPECT_NEAR(this->parseNumber("0.001105335651670241"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[3]); + EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[4]); + EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[5]); + EXPECT_NEAR(this->parseNumber("0.9999999033633374"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[6]); + EXPECT_NEAR(this->parseNumber("0.8602815057967503"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[7]); + EXPECT_NEAR(this->parseNumber("0.99999766034263426"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + } + + TYPED_TEST(CtmcCslModelCheckerTest, Embedded) { + std::string formulasString = "P=? [ F<=10000 \"down\"]"; + formulasString += "; P=? [ !\"down\" U<=10000 \"fail_actuators\"]"; + formulasString += "; P=? [ !\"down\" U<=10000 \"fail_io\"]"; + formulasString += "; P=? [ !\"down\" U<=10000 \"fail_sensors\"]"; + formulasString += "; R{\"up\"}=? [C<=10000]"; + formulasString += "; LRA=? [\"fail_sensors\"]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(3478ul, model->getNumberOfStates()); + EXPECT_EQ(14639ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc); + auto checker = this->createModelChecker(model); + std::unique_ptr result; + + result = checker->check(this->env(), tasks[0]); + EXPECT_NEAR(this->parseNumber("0.0019216435246119591"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[1]); + EXPECT_NEAR(this->parseNumber("3.7079151806696567E-6"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[2]); + EXPECT_NEAR(this->parseNumber("0.001556839327673734"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[3]); + EXPECT_NEAR(this->parseNumber("4.429620626755424E-5"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[4]); + EXPECT_NEAR(this->parseNumber("2.7745274082080154"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[5]); + EXPECT_NEAR(this->parseNumber("0.93458866427696596"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + } + + TYPED_TEST(CtmcCslModelCheckerTest, Polling) { + std::string formulasString = "P=?[ F<=10 \"target\"]"; + formulasString += "; LRA=?[\"target\"]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(12ul, model->getNumberOfStates()); + EXPECT_EQ(22ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc); + 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("0.20079750055570736"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + } + + TYPED_TEST(CtmcCslModelCheckerTest, Tandem) { + std::string formulasString = "P=? [ F<=10 \"network_full\" ]"; + formulasString += "; P=? [ F<=10 \"first_queue_full\" ]"; + formulasString += "; P=? [\"second_queue_full\" U<=1 !\"second_queue_full\"]"; + formulasString += "; R=? [I=10]"; + formulasString += "; R=? [C<=10]"; + formulasString += "; R=? [F \"first_queue_full\"&\"second_queue_full\"]"; + formulasString += "; LRA=? [\"first_queue_full\"]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(66ul, model->getNumberOfStates()); + EXPECT_EQ(189ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc); + auto checker = this->createModelChecker(model); + std::unique_ptr result; + + result = checker->check(this->env(), tasks[0]); + EXPECT_NEAR(this->parseNumber("0.015446370562428037"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[1]); + EXPECT_NEAR(this->parseNumber("0.999999837225515"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[2]); + EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[3]); + EXPECT_NEAR(this->parseNumber("5.679243850315877"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[4]); + EXPECT_NEAR(this->parseNumber("55.44792186036232"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[5]); + EXPECT_NEAR(this->parseNumber("262.85103824276308"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[6]); + EXPECT_NEAR(this->parseNumber("0.9100373532"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + + } +} \ No newline at end of file diff --git a/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp new file mode 100644 index 000000000..e72c5b334 --- /dev/null +++ b/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp @@ -0,0 +1,539 @@ +#include "gtest/gtest.h" +#include "test/storm_gtest.h" +#include "storm-config.h" + +#include "storm/api/builder.h" +#include "storm/api/model_descriptions.h" +#include "storm/api/properties.h" +#include "storm/parser/FormulaParser.h" +#include "storm/logic/Formulas.h" +#include "storm/solver/EigenLinearEquationSolver.h" +#include "storm/models/sparse/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/results/QuantitativeCheckResult.h" +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" +#include "storm/modelchecker/results/QualitativeCheckResult.h" +#include "storm/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" + +namespace { + + class SparseGmmxxGmresIluEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models + static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; + 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 storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; + 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 storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; + 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 storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; + 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 storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; + 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 storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; + 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 storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; + 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 storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; + 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 storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; + 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 storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; + 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 storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; + 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 SparseNativeSoundPowerEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models + static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; + 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::Power); + 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 storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; + 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 HybridSylvanGmmxxGmresEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; + static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::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 storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::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 HybridCuddNativeSoundPowerEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::CUDD; + static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::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 storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::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 storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Dd; + 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 storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Dd; + 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 storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Dd; + 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); + result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + result.first = storm::api::buildSparseModel(program, result.second)->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); + result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + result.first = storm::api::buildSymbolicModel(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; + } + + template + typename std::enable_if::value, std::shared_ptr>>::type + createModelChecker(std::shared_ptr const& model) const { + if (TestType::engine == storm::settings::modules::CoreSettings::Engine::Sparse) { + 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 == storm::settings::modules::CoreSettings::Engine::Hybrid) { + return std::make_shared>(*model); + } else if (TestType::engine == storm::settings::modules::CoreSettings::Engine::Dd) { + 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, + SparseGmmxxGmresDiagEnvironment, + SparseGmmxxBicgstabIluEnvironment, + SparseEigenDGmresEnvironment, + SparseEigenDoubleLUEnvironment, + SparseEigenRationalLUEnvironment, + SparseRationalEliminationEnvironment, + SparseNativeJacobiEnvironment, + SparseNativeWalkerChaeEnvironment, + SparseNativeSorEnvironment, + SparseNativePowerEnvironment, + SparseNativeSoundPowerEnvironment, + SparseNativeRationalSearchEnvironment, + HybridSylvanGmmxxGmresEnvironment, + HybridCuddNativeJacobiEnvironment, + HybridCuddNativeSoundPowerEnvironment, + HybridSylvanNativeRationalSearchEnvironment, + DdSylvanNativePowerEnvironment, + 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()); + } + + +} diff --git a/src/test/storm/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp deleted file mode 100644 index 8ec80c0b7..000000000 --- a/src/test/storm/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp +++ /dev/null @@ -1,442 +0,0 @@ -#include "gtest/gtest.h" -#include "storm-config.h" - -#include "storm/parser/FormulaParser.h" -#include "storm/logic/Formulas.h" -#include "storm/solver/EigenLinearEquationSolver.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/modules/EigenEquationSolverSettings.h" -#include "storm/settings/modules/NativeEquationSolverSettings.h" -#include "storm/settings/SettingMemento.h" -#include "storm/parser/AutoParser.h" -#include "storm/parser/PrismParser.h" -#include "storm/builder/ExplicitModelBuilder.h" -#include "storm/storage/expressions/ExpressionManager.h" - -TEST(EigenDtmcPrctlModelCheckerTest, 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"); - - // 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::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0 / 6.0, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0 / 6.0, quantitativeResult2[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0 / 6.0, quantitativeResult3[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(11.0 / 3.0, quantitativeResult4[0], storm::settings::getModule().getPrecision()); -} - -#ifdef STORM_HAVE_CARL -TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalNumber) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); - - storm::generator::NextStateGeneratorOptions options; - options.setBuildAllLabels().setBuildAllRewardModels(); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).build(); - - // A parser that we use for conveniently constructing the formulas. - - auto expManager = std::make_shared(); - storm::parser::FormulaParser formulaParser(expManager); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = model->as>(); - - ASSERT_EQ(dtmc->getNumberOfStates(), 13ull); - ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull); - - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_EQ(storm::RationalNumber(1) / storm::RationalNumber(6), quantitativeResult1[0]); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_EQ(storm::RationalNumber(1) / storm::RationalNumber(6), quantitativeResult2[0]); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_EQ(storm::RationalNumber(1) / storm::RationalNumber(6), quantitativeResult3[0]); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_EQ(storm::RationalNumber(11) / storm::RationalNumber(3), quantitativeResult4[0]); -} - -TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalFunction) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/pdtmc/parametric_die.pm"); - storm::generator::NextStateGeneratorOptions options; - options.setBuildAllLabels().setBuildAllRewardModels(); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).build(); - - // A parser that we use for conveniently constructing the formulas. - - auto expManager = std::make_shared(); - storm::parser::FormulaParser formulaParser(expManager); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = model->as>(); - - ASSERT_EQ(dtmc->getNumberOfStates(), 13ull); - ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull); - - std::map instantiation; - std::set variables = storm::models::sparse::getProbabilityParameters(*dtmc); - ASSERT_EQ(variables.size(), 1ull); - instantiation.emplace(*variables.begin(), storm::utility::one() / storm::utility::convertNumber(2)); - - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_EQ(storm::utility::one() / storm::utility::convertNumber(6), quantitativeResult1[0].evaluate(instantiation)); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_EQ(storm::utility::one() / storm::utility::convertNumber(6), quantitativeResult2[0].evaluate(instantiation)); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_EQ(storm::utility::one() / storm::utility::convertNumber(6), quantitativeResult3[0].evaluate(instantiation)); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_EQ(storm::utility::convertNumber(11) / storm::utility::convertNumber(3), quantitativeResult4[0].evaluate(instantiation)); -} -#endif - -TEST(EigenDtmcPrctlModelCheckerTest, Crowds) { - 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::unique_ptr>(new storm::solver::EigenLinearEquationSolverFactory())); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.3328800375801578281, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.1522194965, quantitativeResult2[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.32153724292835045, quantitativeResult3[0], storm::settings::getModule().getPrecision()); -} - -TEST(EigenDtmcPrctlModelCheckerTest, SynchronousLeader) { - 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::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.9999965911265462636, quantitativeResult2[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0448979591836789, quantitativeResult3[0], storm::settings::getModule().getPrecision()); -} - -TEST(EigenDtmcPrctlModelCheckerTest, LRASingleBscc) { - storm::storage::SparseMatrixBuilder matrixBuilder; - std::shared_ptr> dtmc; - - // A parser that we use for conveniently constructing the formulas. - - auto expManager = std::make_shared(); - storm::parser::FormulaParser formulaParser(expManager); - - { - matrixBuilder = storm::storage::SparseMatrixBuilder(2, 2, 2); - matrixBuilder.addNextValue(0, 1, 1.); - matrixBuilder.addNextValue(1, 0, 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::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(.5, quantitativeResult1[1], storm::settings::getModule().getPrecision()); - } - { - matrixBuilder = storm::storage::SparseMatrixBuilder(2, 2, 4); - matrixBuilder.addNextValue(0, 0, .5); - matrixBuilder.addNextValue(0, 1, .5); - matrixBuilder.addNextValue(1, 0, .5); - matrixBuilder.addNextValue(1, 1, .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::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(.5, quantitativeResult1[1], storm::settings::getModule().getPrecision()); - } - - { - matrixBuilder = storm::storage::SparseMatrixBuilder(3, 3, 3); - matrixBuilder.addNextValue(0, 1, 1); - matrixBuilder.addNextValue(1, 2, 1); - matrixBuilder.addNextValue(2, 0, 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::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1. / 3., quantitativeResult1[0], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1. / 3., quantitativeResult1[1], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1. / 3., quantitativeResult1[2], storm::settings::getModule().getPrecision()); - } -} - -TEST(EigenDtmcPrctlModelCheckerTest, LRA) { - storm::storage::SparseMatrixBuilder matrixBuilder; - std::shared_ptr> dtmc; - - // A parser that we use for conveniently constructing the formulas. - - auto expManager = std::make_shared(); - storm::parser::FormulaParser formulaParser(expManager); - - { - matrixBuilder = storm::storage::SparseMatrixBuilder(15, 15, 20, true); - matrixBuilder.addNextValue(0, 1, 1); - matrixBuilder.addNextValue(1, 4, 0.7); - matrixBuilder.addNextValue(1, 6, 0.3); - matrixBuilder.addNextValue(2, 0, 1); - - matrixBuilder.addNextValue(3, 5, 0.8); - matrixBuilder.addNextValue(3, 9, 0.2); - matrixBuilder.addNextValue(4, 3, 1); - matrixBuilder.addNextValue(5, 3, 1); - - matrixBuilder.addNextValue(6, 7, 1); - matrixBuilder.addNextValue(7, 8, 1); - matrixBuilder.addNextValue(8, 6, 1); - - matrixBuilder.addNextValue(9, 10, 1); - matrixBuilder.addNextValue(10, 9, 1); - matrixBuilder.addNextValue(11, 9, 1); - - matrixBuilder.addNextValue(12, 5, 0.4); - matrixBuilder.addNextValue(12, 8, 0.3); - matrixBuilder.addNextValue(12, 11, 0.3); - - matrixBuilder.addNextValue(13, 7, 0.7); - matrixBuilder.addNextValue(13, 12, 0.3); - - matrixBuilder.addNextValue(14, 12, 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::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.3 / 3., quantitativeResult1[0], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0, quantitativeResult1[3], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1. / 3., quantitativeResult1[6], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0, quantitativeResult1[9], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.3 / 3., quantitativeResult1[12], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(.79 / 3., quantitativeResult1[13], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.3 / 3., quantitativeResult1[14], storm::settings::getModule().getPrecision()); - } -} - -TEST(EigenDtmcPrctlModelCheckerTest, Conditional) { - 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->as>(); - - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); - - // 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(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(0.5, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"target\" || F \"condition\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(storm::utility::one(), quantitativeResult2[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"target\"]"); - - result = checker.check(*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(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(storm::utility::one(), quantitativeResult4[0], storm::settings::getModule().getPrecision()); -} diff --git a/src/test/storm/modelchecker/ExplicitDtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/ExplicitDtmcPrctlModelCheckerTest.cpp new file mode 100644 index 000000000..06b90270b --- /dev/null +++ b/src/test/storm/modelchecker/ExplicitDtmcPrctlModelCheckerTest.cpp @@ -0,0 +1,158 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "storm/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/parser/AutoParser.h" +#include "storm/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/ExplicitMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/ExplicitMdpPrctlModelCheckerTest.cpp index 2db2b5703..91db98302 100644 --- a/src/test/storm/modelchecker/ExplicitMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/ExplicitMdpPrctlModelCheckerTest.cpp @@ -7,12 +7,9 @@ #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/settings/modules/NativeEquationSolverSettings.h" #include "storm/parser/AutoParser.h" #include "storm/parser/PrismParser.h" #include "storm/builder/ExplicitModelBuilder.h" @@ -20,8 +17,9 @@ 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(env.solver().minMax().getPrecision() * storm::utility::convertNumber(1e-2)); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-8)); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -40,56 +38,56 @@ TEST(ExplicitMdpPrctlModelCheckerTest, Dice) { std::unique_ptr result = checker.check(env, *formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(1.0/36.0, quantitativeResult1[0], storm::settings::getModule().getPrecision()); + 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], storm::settings::getModule().getPrecision()); + 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], storm::settings::getModule().getPrecision()); + 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], storm::settings::getModule().getPrecision()); + 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], storm::settings::getModule().getPrecision()); + 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], storm::settings::getModule().getPrecision()); + 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], storm::settings::getModule().getPrecision()); + 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], storm::settings::getModule().getPrecision()); + 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", ""); @@ -104,14 +102,14 @@ TEST(ExplicitMdpPrctlModelCheckerTest, Dice) { result = stateRewardModelChecker.check(env, *formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult9 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(22.0/3.0, quantitativeResult9[0], storm::settings::getModule().getPrecision()); + 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], storm::settings::getModule().getPrecision()); + 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"); @@ -126,20 +124,21 @@ TEST(ExplicitMdpPrctlModelCheckerTest, Dice) { result = stateAndTransitionRewardModelChecker.check(env, *formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult11 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(44.0/3.0, quantitativeResult11[0], storm::settings::getModule().getPrecision()); + 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], storm::settings::getModule().getPrecision()); + 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(env.solver().minMax().getPrecision() * storm::utility::convertNumber(1e-2)); + 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"); @@ -160,41 +159,41 @@ TEST(ExplicitMdpPrctlModelCheckerTest, AsynchronousLeader) { std::unique_ptr result = checker.check(env, *formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::getModule().getPrecision()); + 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], storm::settings::getModule().getPrecision()); + 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], storm::settings::getModule().getPrecision()); + 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], storm::settings::getModule().getPrecision()); + 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], storm::settings::getModule().getPrecision()); + 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], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(30.0/7.0, quantitativeResult6[0], precision); } diff --git a/src/test/storm/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp deleted file mode 100644 index 62f77d023..000000000 --- a/src/test/storm/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp +++ /dev/null @@ -1,255 +0,0 @@ -#include "gtest/gtest.h" -#include "storm-config.h" -#include "storm/settings/SettingMemento.h" -#include "storm/parser/PrismParser.h" -#include "storm/parser/FormulaParser.h" -#include "storm/logic/Formulas.h" -#include "storm/builder/ExplicitModelBuilder.h" - -#include "storm/solver/GmmxxLinearEquationSolver.h" -#include "storm/models/sparse/StandardRewardModel.h" -#include "storm/modelchecker/csl/SparseCtmcCslModelChecker.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/settings/modules/GmmxxEquationSolverSettings.h" - -#include "storm/storage/expressions/ExpressionManager.h" - -TEST(GmmxxCtmcCslModelCheckerTest, Cluster) { - // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true); - storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); - std::shared_ptr formula(nullptr); - - // Build the model. - storm::generator::NextStateGeneratorOptions options; - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true). addRewardModel("num_repairs")).build(); - ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); - std::shared_ptr> ctmc = model->as>(); - uint_fast64_t initialState = *ctmc->getInitialStates().begin(); - - // Create model checker. - storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::make_unique>()); - - // Start checking properties. - formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=100 !\"minimum\"]"); - std::unique_ptr checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(5.5461254704419085E-5, quantitativeCheckResult1[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ F[100,100] !\"minimum\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(2.3397873548343415E-6, quantitativeCheckResult2[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ F[100,2000] !\"minimum\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U<=10 \"premium\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(1, quantitativeCheckResult4[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"minimum\" U>=1 \"minimum\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(0, quantitativeCheckResult5[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U>=1 !\"minimum\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(0.9999999033633374, quantitativeCheckResult6[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [C<=100]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult7 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(0.8602815057967503, quantitativeCheckResult7[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"minimum\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult8 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(0.99999766034263426, quantitativeCheckResult8[initialState], storm::settings::getModule().getPrecision()); -} - -TEST(GmmxxCtmcCslModelCheckerTest, Embedded) { - // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true); - storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); - std::shared_ptr formula(nullptr); - - // Build the model. - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true). addRewardModel("up")).build(); - ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); - std::shared_ptr> ctmc = model->as>(); - uint_fast64_t initialState = *ctmc->getInitialStates().begin(); - - // Create model checker. - storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::make_unique>()); - - // Start checking properties. - formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10000 \"down\"]"); - std::unique_ptr checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(0.0019216435246119591, quantitativeCheckResult1[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_actuators\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(3.7079151806696567E-6, quantitativeCheckResult2[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_io\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(0.001556839327673734, quantitativeCheckResult3[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_sensors\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [C<=10000]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(2.7745274082080154, quantitativeCheckResult5[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"fail_sensors\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(0.93458866427696596, quantitativeCheckResult6[initialState], storm::settings::getModule().getPrecision()); -} - -TEST(GmmxxCtmcCslModelCheckerTest, Polling) { - // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true); - storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); - std::shared_ptr formula(nullptr); - - // Build the model. - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true)).build(); - ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); - std::shared_ptr> ctmc = model->as>(); - uint_fast64_t initialState = *ctmc->getInitialStates().begin(); - - // Create model checker. - storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::make_unique>()); - - // Start checking properties. - formula = formulaParser.parseSingleFormulaFromString("P=?[ F<=10 \"target\"]"); - std::unique_ptr checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(1, quantitativeCheckResult1[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("LRA=?[\"target\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(0.20079750055570736, quantitativeCheckResult2[initialState], storm::settings::getModule().getPrecision()); -} - -TEST(GmmxxCtmcCslModelCheckerTest, Fms) { - // No properties to check at this point. -} - -TEST(GmmxxCtmcCslModelCheckerTest, Tandem) { - - // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true); - storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); - std::shared_ptr formula(nullptr); - - // Build the model. - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true). addRewardModel("customers")).build(); - ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); - std::shared_ptr> ctmc = model->as>(); - uint_fast64_t initialState = *ctmc->getInitialStates().begin(); - - // Create model checker. - storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::make_unique>()); - - // Start checking properties. - formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"network_full\" ]"); - std::unique_ptr checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(0.015446370562428037, quantitativeCheckResult1[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"first_queue_full\" ]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(0.999999837225515, quantitativeCheckResult2[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [\"second_queue_full\" U<=1 !\"second_queue_full\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(1, quantitativeCheckResult3[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [I=10]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(5.679243850315877, quantitativeCheckResult4[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [C<=10]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(55.44792186036232, quantitativeCheckResult5[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"first_queue_full\"&\"second_queue_full\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(262.85103661561755, quantitativeCheckResult6[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"first_queue_full\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult7 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(0.9100373532, quantitativeCheckResult7[initialState], storm::settings::getModule().getPrecision()); -} diff --git a/src/test/storm/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp deleted file mode 100644 index 5535edf4f..000000000 --- a/src/test/storm/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp +++ /dev/null @@ -1,333 +0,0 @@ -#include "gtest/gtest.h" -#include "storm-config.h" - -#include "storm/parser/FormulaParser.h" -#include "storm/logic/Formulas.h" -#include "storm/solver/GmmxxLinearEquationSolver.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/modules/GmmxxEquationSolverSettings.h" -#include "storm/settings/modules/NativeEquationSolverSettings.h" -#include "storm/settings/SettingMemento.h" -#include "storm/parser/AutoParser.h" -#include "storm/parser/PrismParser.h" -#include "storm/builder/ExplicitModelBuilder.h" -#include "storm/storage/expressions/ExpressionManager.h" - -TEST(GmmxxDtmcPrctlModelCheckerTest, 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"); - - // 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::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0 / 6.0, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0 / 6.0, quantitativeResult2[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0 / 6.0, quantitativeResult3[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(11.0 / 3.0, quantitativeResult4[0], storm::settings::getModule().getPrecision()); -} - -TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { - 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::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.3328800375801578281, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.1522194965, quantitativeResult2[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.32153724292835045, quantitativeResult3[0], storm::settings::getModule().getPrecision()); -} - -TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { - 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::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.9999965911265462636, quantitativeResult2[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.044879046, quantitativeResult3[0], storm::settings::getModule().getPrecision()); -} - -TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) { - storm::storage::SparseMatrixBuilder matrixBuilder; - std::shared_ptr> dtmc; - - // A parser that we use for conveniently constructing the formulas. - - auto expManager = std::make_shared(); - storm::parser::FormulaParser formulaParser(expManager); - - { - matrixBuilder = storm::storage::SparseMatrixBuilder(2, 2, 2); - matrixBuilder.addNextValue(0, 1, 1.); - matrixBuilder.addNextValue(1, 0, 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::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(.5, quantitativeResult1[1], storm::settings::getModule().getPrecision()); - } - { - matrixBuilder = storm::storage::SparseMatrixBuilder(2, 2, 4); - matrixBuilder.addNextValue(0, 0, .5); - matrixBuilder.addNextValue(0, 1, .5); - matrixBuilder.addNextValue(1, 0, .5); - matrixBuilder.addNextValue(1, 1, .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::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(.5, quantitativeResult1[1], storm::settings::getModule().getPrecision()); - } - - { - matrixBuilder = storm::storage::SparseMatrixBuilder(3, 3, 3); - matrixBuilder.addNextValue(0, 1, 1); - matrixBuilder.addNextValue(1, 2, 1); - matrixBuilder.addNextValue(2, 0, 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::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1. / 3., quantitativeResult1[0], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1. / 3., quantitativeResult1[1], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1. / 3., quantitativeResult1[2], storm::settings::getModule().getPrecision()); - } -} - -TEST(GmmxxDtmcPrctlModelCheckerTest, LRA) { - storm::storage::SparseMatrixBuilder matrixBuilder; - std::shared_ptr> dtmc; - - // A parser that we use for conveniently constructing the formulas. - - auto expManager = std::make_shared(); - storm::parser::FormulaParser formulaParser(expManager); - - { - matrixBuilder = storm::storage::SparseMatrixBuilder(15, 15, 20, true); - matrixBuilder.addNextValue(0, 1, 1); - matrixBuilder.addNextValue(1, 4, 0.7); - matrixBuilder.addNextValue(1, 6, 0.3); - matrixBuilder.addNextValue(2, 0, 1); - - matrixBuilder.addNextValue(3, 5, 0.8); - matrixBuilder.addNextValue(3, 9, 0.2); - matrixBuilder.addNextValue(4, 3, 1); - matrixBuilder.addNextValue(5, 3, 1); - - matrixBuilder.addNextValue(6, 7, 1); - matrixBuilder.addNextValue(7, 8, 1); - matrixBuilder.addNextValue(8, 6, 1); - - matrixBuilder.addNextValue(9, 10, 1); - matrixBuilder.addNextValue(10, 9, 1); - matrixBuilder.addNextValue(11, 9, 1); - - matrixBuilder.addNextValue(12, 5, 0.4); - matrixBuilder.addNextValue(12, 8, 0.3); - matrixBuilder.addNextValue(12, 11, 0.3); - - matrixBuilder.addNextValue(13, 7, 0.7); - matrixBuilder.addNextValue(13, 12, 0.3); - - matrixBuilder.addNextValue(14, 12, 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::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.3 / 3., quantitativeResult1[0], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0, quantitativeResult1[3], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1. / 3., quantitativeResult1[6], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0, quantitativeResult1[9], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.3 / 3., quantitativeResult1[12], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(.79 / 3., quantitativeResult1[13], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.3 / 3., quantitativeResult1[14], storm::settings::getModule().getPrecision()); - } -} - -TEST(GmmxxDtmcPrctlModelCheckerTest, Conditional) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/test_conditional.pm"); - - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(true, true)).build(); - ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc); - ASSERT_EQ(4ul, model->getNumberOfStates()); - ASSERT_EQ(5ul, model->getNumberOfTransitions()); - - std::shared_ptr> dtmc = model->as>(); - - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); - - // 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(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(0.5, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"target\" || F \"condition\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(storm::utility::one(), quantitativeResult2[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"target\"]"); - - result = checker.check(*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(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(storm::utility::one(), quantitativeResult4[0], storm::settings::getModule().getPrecision()); -} diff --git a/src/test/storm/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp deleted file mode 100644 index 821bf9297..000000000 --- a/src/test/storm/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp +++ /dev/null @@ -1,614 +0,0 @@ -#include "gtest/gtest.h" -#include "storm-config.h" -#include "storm/settings/SettingMemento.h" -#include "storm/parser/PrismParser.h" -#include "storm/parser/FormulaParser.h" -#include "storm/logic/Formulas.h" -#include "storm/builder/DdPrismModelBuilder.h" -#include "storm/storage/dd/DdType.h" -#include "storm/storage/SymbolicModelDescription.h" - -#include "storm/solver/GmmxxLinearEquationSolver.h" -#include "storm/models/symbolic/StandardRewardModel.h" -#include "storm/modelchecker/csl/HybridCtmcCslModelChecker.h" -#include "storm/modelchecker/results/HybridQuantitativeCheckResult.h" -#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" -#include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h" - -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/GeneralSettings.h" -#include "storm/settings/modules/GmmxxEquationSolverSettings.h" - -#include "storm/settings/modules/NativeEquationSolverSettings.h" -#include "storm/storage/expressions/ExpressionManager.h" - -TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Cudd) { - - // Parse the model description. - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); - std::shared_ptr formula(nullptr); - - // Build the model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("num_repairs"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); - std::shared_ptr> ctmc = model->as>(); - - // Create model checker. - storm::modelchecker::HybridCtmcCslModelChecker> modelchecker(*ctmc, std::make_unique>()); - - // Start checking properties. - formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=100 !\"minimum\"]"); - std::unique_ptr checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(5.5461254704419085E-5, quantitativeCheckResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(5.5461254704419085E-5, quantitativeCheckResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ F[100,100] !\"minimum\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(2.3397873548343415E-6, quantitativeCheckResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(2.3397873548343415E-6, quantitativeCheckResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ F[100,2000] !\"minimum\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U<=10 \"premium\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(1, quantitativeCheckResult4.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1, quantitativeCheckResult4.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"minimum\" U>=1 \"minimum\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0, quantitativeCheckResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0, quantitativeCheckResult5.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U>=1 !\"minimum\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.9999999033633374, quantitativeCheckResult6.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.9999999033633374, quantitativeCheckResult6.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [C<=100]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult7 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.8602815057967503, quantitativeCheckResult7.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.8602815057967503, quantitativeCheckResult7.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"minimum\"]"); - checkResult = modelchecker.check(*formula); - - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult8 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.99999766034263426, quantitativeCheckResult8.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.99999766034263426, quantitativeCheckResult8.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Sylvan) { - // Parse the model description. - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); - std::shared_ptr formula(nullptr); - - // Build the model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("num_repairs"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); - std::shared_ptr> ctmc = model->as>(); - - // Create model checker. - storm::modelchecker::HybridCtmcCslModelChecker> modelchecker(*ctmc, std::make_unique>()); - - // Start checking properties. - formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=100 !\"minimum\"]"); - std::unique_ptr checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(5.5461254704419085E-5, quantitativeCheckResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(5.5461254704419085E-5, quantitativeCheckResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ F[100,100] !\"minimum\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(2.3397873548343415E-6, quantitativeCheckResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(2.3397873548343415E-6, quantitativeCheckResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ F[100,2000] !\"minimum\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U<=10 \"premium\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(1, quantitativeCheckResult4.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1, quantitativeCheckResult4.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"minimum\" U>=1 \"minimum\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0, quantitativeCheckResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0, quantitativeCheckResult5.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U>=1 !\"minimum\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.9999999033633374, quantitativeCheckResult6.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.9999999033633374, quantitativeCheckResult6.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [C<=100]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult7 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.8602815057967503, quantitativeCheckResult7.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.8602815057967503, quantitativeCheckResult7.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"minimum\"]"); - checkResult = modelchecker.check(*formula); - - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult8 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.99999766034263426, quantitativeCheckResult8.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.99999766034263426, quantitativeCheckResult8.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Cudd) { - // Parse the model description. - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); - std::shared_ptr formula(nullptr); - - // Build the model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("up"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); - std::shared_ptr> ctmc = model->as>(); - - // Create model checker. - storm::modelchecker::HybridCtmcCslModelChecker> modelchecker(*ctmc, std::make_unique>()); - - // Start checking properties. - formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10000 \"down\"]"); - std::unique_ptr checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.0019216435246119591, quantitativeCheckResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0019216435246119591, quantitativeCheckResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_actuators\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(3.7079151806696567E-6, quantitativeCheckResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(3.7079151806696567E-6, quantitativeCheckResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_io\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.001556839327673734, quantitativeCheckResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.001556839327673734, quantitativeCheckResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_sensors\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [C<=10000]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(2.7745274082080154, quantitativeCheckResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(2.7745274082080154, quantitativeCheckResult5.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"fail_sensors\"]"); - checkResult = modelchecker.check(*formula); - - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.934586179, quantitativeCheckResult6.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.934586179, quantitativeCheckResult6.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Sylvan) { - // Parse the model description. - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); - std::shared_ptr formula(nullptr); - - // Build the model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("up"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); - std::shared_ptr> ctmc = model->as>(); - - // Create model checker. - storm::modelchecker::HybridCtmcCslModelChecker> modelchecker(*ctmc, std::make_unique>()); - - // Start checking properties. - formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10000 \"down\"]"); - std::unique_ptr checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.0019216435246119591, quantitativeCheckResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0019216435246119591, quantitativeCheckResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_actuators\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(3.7079151806696567E-6, quantitativeCheckResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(3.7079151806696567E-6, quantitativeCheckResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_io\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.001556839327673734, quantitativeCheckResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.001556839327673734, quantitativeCheckResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_sensors\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [C<=10000]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(2.7745274082080154, quantitativeCheckResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(2.7745274082080154, quantitativeCheckResult5.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"fail_sensors\"]"); - checkResult = modelchecker.check(*formula); - - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.934586179, quantitativeCheckResult6.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.934586179, quantitativeCheckResult6.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Cudd) { - // Parse the model description. - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); - std::shared_ptr formula(nullptr); - - // Build the model. - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); - ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); - std::shared_ptr> ctmc = model->as>(); - - // Create model checker. - storm::modelchecker::HybridCtmcCslModelChecker> modelchecker(*ctmc, std::make_unique>()); - - // Start checking properties. - formula = formulaParser.parseSingleFormulaFromString("P=?[ F<=10 \"target\"]"); - std::unique_ptr checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(1, quantitativeCheckResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1, quantitativeCheckResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"target\"]"); - checkResult = modelchecker.check(*formula); - - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.20079750055570736, quantitativeCheckResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.20079750055570736, quantitativeCheckResult2.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Sylvan) { - - // Parse the model description. - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); - std::shared_ptr formula(nullptr); - - // Build the model. - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); - ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); - std::shared_ptr> ctmc = model->as>(); - - // Create model checker. - storm::modelchecker::HybridCtmcCslModelChecker> modelchecker(*ctmc, std::make_unique>()); - - // Start checking properties. - formula = formulaParser.parseSingleFormulaFromString("P=?[ F<=10 \"target\"]"); - std::unique_ptr checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(1, quantitativeCheckResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1, quantitativeCheckResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"target\"]"); - checkResult = modelchecker.check(*formula); - - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.20079750055570736, quantitativeCheckResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.20079750055570736, quantitativeCheckResult2.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(GmmxxHybridCtmcCslModelCheckerTest, Fms) { - - // No properties to check at this point. -} - -TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem_Cudd) { - // Parse the model description. - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); - std::shared_ptr formula(nullptr); - - // Build the model with the customers reward structure. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("customers"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); - std::shared_ptr> ctmc = model->as>(); - - // Create model checker. - storm::modelchecker::HybridCtmcCslModelChecker> modelchecker(*ctmc, std::make_unique>()); - - // Start checking properties. - formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"network_full\" ]"); - std::unique_ptr checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.015446370562428037, quantitativeCheckResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.015446370562428037, quantitativeCheckResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"first_queue_full\" ]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.999999837225515, quantitativeCheckResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.999999837225515, quantitativeCheckResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [\"second_queue_full\" U<=1 !\"second_queue_full\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(1, quantitativeCheckResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1, quantitativeCheckResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [I=10]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(5.679243850315877, quantitativeCheckResult4.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(5.679243850315877, quantitativeCheckResult4.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [C<=10]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(55.44792186036232, quantitativeCheckResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(55.44792186036232, quantitativeCheckResult5.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"first_queue_full\"&\"second_queue_full\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(262.85103498583413, quantitativeCheckResult6.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(262.85103498583413, quantitativeCheckResult6.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"first_queue_full\"]"); - checkResult = modelchecker.check(*formula); - - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult7 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.9100373532, quantitativeCheckResult7.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.9100373532, quantitativeCheckResult7.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem_Sylvan) { - // Parse the model description. - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); - std::shared_ptr formula(nullptr); - - // Build the model with the customers reward structure. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("customers"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); - std::shared_ptr> ctmc = model->as>(); - - // Create model checker. - storm::modelchecker::HybridCtmcCslModelChecker> modelchecker(*ctmc, std::make_unique>()); - - // Start checking properties. - formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"network_full\" ]"); - std::unique_ptr checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.015446370562428037, quantitativeCheckResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.015446370562428037, quantitativeCheckResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"first_queue_full\" ]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.999999837225515, quantitativeCheckResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.999999837225515, quantitativeCheckResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [\"second_queue_full\" U<=1 !\"second_queue_full\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(1, quantitativeCheckResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1, quantitativeCheckResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [I=10]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(5.679243850315877, quantitativeCheckResult4.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(5.679243850315877, quantitativeCheckResult4.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [C<=10]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(55.44792186036232, quantitativeCheckResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(55.44792186036232, quantitativeCheckResult5.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"first_queue_full\"&\"second_queue_full\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(262.85103498583413, quantitativeCheckResult6.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(262.85103498583413, quantitativeCheckResult6.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"first_queue_full\"]"); - checkResult = modelchecker.check(*formula); - - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult7 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.9100373532, quantitativeCheckResult7.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.9100373532, quantitativeCheckResult7.getMax(), storm::settings::getModule().getPrecision()); -} diff --git a/src/test/storm/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp deleted file mode 100644 index 2b41266a5..000000000 --- a/src/test/storm/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp +++ /dev/null @@ -1,353 +0,0 @@ -#include "gtest/gtest.h" -#include "storm-config.h" - -#include "storm/parser/FormulaParser.h" -#include "storm/logic/Formulas.h" -#include "storm/solver/GmmxxLinearEquationSolver.h" -#include "storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h" -#include "storm/modelchecker/results/HybridQuantitativeCheckResult.h" -#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" -#include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h" -#include "storm/parser/PrismParser.h" -#include "storm/builder/DdPrismModelBuilder.h" -#include "storm/models/symbolic/Dtmc.h" -#include "storm/models/symbolic/StandardRewardModel.h" -#include "storm/storage/SymbolicModelDescription.h" -#include "storm/storage/expressions/ExpressionManager.h" -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/GeneralSettings.h" -#include "storm/settings/modules/GmmxxEquationSolverSettings.h" -#include "storm/settings/modules/NativeEquationSolverSettings.h" - - -TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Cudd) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - - // A parser that we use for conveniently constructing the formulas. - - auto expManager = std::make_shared(); - storm::parser::FormulaParser formulaParser(expManager); - - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("coin_flips"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(13ul, model->getNumberOfStates()); - EXPECT_EQ(20ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = model->as>(); - - storm::modelchecker::HybridDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(11.0/3.0, quantitativeResult4.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(11.0/3.0, quantitativeResult4.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Sylvan) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - - // A parser that we use for conveniently constructing the formulas. - - auto expManager = std::make_shared(); - storm::parser::FormulaParser formulaParser(expManager); - - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("coin_flips"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(13ul, model->getNumberOfStates()); - EXPECT_EQ(20ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = model->as>(); - - storm::modelchecker::HybridDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(11.0/3.0, quantitativeResult4.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(11.0/3.0, quantitativeResult4.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Cudd) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm"); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - - // A parser that we use for conveniently constructing the formulas. - - auto expManager = std::make_shared(); - storm::parser::FormulaParser formulaParser(expManager); - - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_EQ(8607ul, model->getNumberOfStates()); - EXPECT_EQ(15113ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = model->as>(); - - storm::modelchecker::HybridDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.3328800375801578281, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.3328800375801578281, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.1522194965, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.1522194965, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.32153724292835045, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.32153724292835045, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm"); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - - // A parser that we use for conveniently constructing the formulas. - - auto expManager = std::make_shared(); - storm::parser::FormulaParser formulaParser(expManager); - - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_EQ(8607ul, model->getNumberOfStates()); - EXPECT_EQ(15113ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = model->as>(); - - storm::modelchecker::HybridDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.3328800375801578281, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.3328800375801578281, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.1522194965, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.1522194965, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.32153724292835045, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.32153724292835045, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm"); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - - // A parser that we use for conveniently constructing the formulas. - - auto expManager = std::make_shared(); - storm::parser::FormulaParser formulaParser(expManager); - - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("num_rounds"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(273ul, model->getNumberOfStates()); - EXPECT_EQ(397ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = model->as>(); - - storm::modelchecker::HybridDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1.0, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(1.0416666666666643, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0416666666666643, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm"); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - - // A parser that we use for conveniently constructing the formulas. - - auto expManager = std::make_shared(); - storm::parser::FormulaParser formulaParser(expManager); - - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("num_rounds"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(273ul, model->getNumberOfStates()); - EXPECT_EQ(397ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = model->as>(); - - storm::modelchecker::HybridDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1.0, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(1.0416666666666643, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0416666666666643, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); -} diff --git a/src/test/storm/modelchecker/LraDtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/LraDtmcPrctlModelCheckerTest.cpp new file mode 100644 index 000000000..ee1d88c30 --- /dev/null +++ b/src/test/storm/modelchecker/LraDtmcPrctlModelCheckerTest.cpp @@ -0,0 +1,268 @@ +#include "gtest/gtest.h" +#include "storm-config.h" +#include "test/storm_gtest.h" + +#include "storm/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/parser/AutoParser.h" +#include "storm/builder/ExplicitModelBuilder.h" + +namespace { + + class GmmxxDoubleGmresEnvironment { + public: + typedef storm::RationalNumber 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 storm::RationalNumber 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 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/MdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp index 758c9bd74..04dd3076a 100644 --- a/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp @@ -50,6 +50,7 @@ namespace { env.solver().setForceSoundness(true); env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); + env.solver().minMax().setRelativeTerminationCriterion(false); return env; } }; @@ -119,6 +120,7 @@ namespace { env.solver().setForceSoundness(true); env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); + env.solver().minMax().setRelativeTerminationCriterion(false); return env; } }; diff --git a/src/test/storm/modelchecker/NativeCtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/NativeCtmcCslModelCheckerTest.cpp deleted file mode 100644 index 246ac41ca..000000000 --- a/src/test/storm/modelchecker/NativeCtmcCslModelCheckerTest.cpp +++ /dev/null @@ -1,226 +0,0 @@ -#include "gtest/gtest.h" -#include "storm-config.h" -#include "storm/settings/SettingMemento.h" -#include "storm/parser/PrismParser.h" -#include "storm/parser/FormulaParser.h" -#include "storm/logic/Formulas.h" -#include "storm/builder/ExplicitModelBuilder.h" - -#include "storm/solver/NativeLinearEquationSolver.h" -#include "storm/models/sparse/StandardRewardModel.h" -#include "storm/modelchecker/csl/SparseCtmcCslModelChecker.h" -#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/NativeEquationSolverSettings.h" - -#include "storm/settings/modules/GeneralSettings.h" - -TEST(NativeCtmcCslModelCheckerTest, Cluster) { - // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true); - storm::parser::FormulaParser formulaParser(program); - std::shared_ptr formula(nullptr); - - // Build the model. - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true). addRewardModel("num_repairs")).build(); - ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); - std::shared_ptr> ctmc = model->as>(); - uint_fast64_t initialState = *ctmc->getInitialStates().begin(); - - // Create model checker. - storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::make_unique>()); - - // Start checking properties. - formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=100 !\"minimum\"]"); - std::unique_ptr checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(5.5461254704419085E-5, quantitativeCheckResult1[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ F[100,100] !\"minimum\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(2.3397873548343415E-6, quantitativeCheckResult2[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ F[100,2000] !\"minimum\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U<=10 \"premium\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(1, quantitativeCheckResult4[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"minimum\" U>=1 \"minimum\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(0, quantitativeCheckResult5[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U>=1 !\"minimum\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(0.9999999033633374, quantitativeCheckResult6[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [C<=100]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult7 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(0.8602815057967503, quantitativeCheckResult7[initialState], storm::settings::getModule().getPrecision()); -} - -TEST(NativeCtmcCslModelCheckerTest, Embedded) { - - // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true); - storm::parser::FormulaParser formulaParser(program); - std::shared_ptr formula(nullptr); - - // Build the model. - storm::generator::NextStateGeneratorOptions options; - options.addRewardModel("up").setBuildAllLabels(); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).build(); - ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); - std::shared_ptr> ctmc = model->as>(); - uint_fast64_t initialState = *ctmc->getInitialStates().begin(); - - // Create model checker. - storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::make_unique>()); - - // Start checking properties. - formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10000 \"down\"]"); - std::unique_ptr checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(0.0019216435246119591, quantitativeCheckResult1[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_actuators\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(3.7079151806696567E-6, quantitativeCheckResult2[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_io\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(0.001556839327673734, quantitativeCheckResult3[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_sensors\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [C<=10000]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(2.7745274082080154, quantitativeCheckResult5[initialState], storm::settings::getModule().getPrecision()); -} - -TEST(NativeCtmcCslModelCheckerTest, Polling) { - // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true); - storm::parser::FormulaParser formulaParser(program); - std::shared_ptr formula(nullptr); - - // Build the model. - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true)).build(); - ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); - std::shared_ptr> ctmc = model->as>(); - uint_fast64_t initialState = *ctmc->getInitialStates().begin(); - - // Create model checker. - storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::make_unique>()); - - // Start checking properties. - formula = formulaParser.parseSingleFormulaFromString("P=?[ F<=10 \"target\"]"); - std::unique_ptr checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(1, quantitativeCheckResult1[initialState], storm::settings::getModule().getPrecision()); -} - -TEST(NativeCtmcCslModelCheckerTest, Fms) { - - // No properties to check at this point. -} - -TEST(NativeCtmcCslModelCheckerTest, Tandem) { - - // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true); - storm::parser::FormulaParser formulaParser(program); - std::shared_ptr formula(nullptr); - - // Build the model with the customers reward structure. - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true).addRewardModel("customers")).build(); - ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); - std::shared_ptr> ctmc = model->as>(); - uint_fast64_t initialState = *ctmc->getInitialStates().begin(); - - // Create model checker. - storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::make_unique>()); - - // Start checking properties. - formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"network_full\" ]"); - std::unique_ptr checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(0.015446370562428037, quantitativeCheckResult1[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"first_queue_full\" ]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(0.999999837225515, quantitativeCheckResult2[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [\"second_queue_full\" U<=1 !\"second_queue_full\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(1, quantitativeCheckResult3[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [I=10]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(5.679243850315877, quantitativeCheckResult4[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [C<=10]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(55.44792186036232, quantitativeCheckResult5[initialState], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"first_queue_full\"&\"second_queue_full\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(262.78584491454814, quantitativeCheckResult6[initialState], storm::settings::getModule().getPrecision()); -} diff --git a/src/test/storm/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp deleted file mode 100644 index 24e72c778..000000000 --- a/src/test/storm/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp +++ /dev/null @@ -1,294 +0,0 @@ -#include "gtest/gtest.h" -#include "storm-config.h" - -#include "storm/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/settings/modules/NativeEquationSolverSettings.h" -#include "storm/settings/SettingMemento.h" -#include "storm/parser/AutoParser.h" - -TEST(NativeDtmcPrctlModelCheckerTest, 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"); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - 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::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0/6.0, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0/6.0, quantitativeResult2[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0/6.0, quantitativeResult3[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(3.6666650772094727, quantitativeResult4[0], storm::settings::getModule().getPrecision()); -} - -TEST(NativeDtmcPrctlModelCheckerTest, Crowds) { - 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. - storm::parser::FormulaParser formulaParser; - - std::shared_ptr> dtmc = abstractModel->as>(); - - ASSERT_EQ(8607ull, dtmc->getNumberOfStates()); - ASSERT_EQ(15113ull, dtmc->getNumberOfTransitions()); - - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.33288205191646525, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.15222066094730619, quantitativeResult2[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.32153900158185761, quantitativeResult3[0], storm::settings::getModule().getPrecision()); -} - -TEST(NativeDtmcPrctlModelCheckerTest, SynchronousLeader) { - 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. - storm::parser::FormulaParser formulaParser; - - std::shared_ptr> dtmc = abstractModel->as>(); - - ASSERT_EQ(12400ull, dtmc->getNumberOfStates()); - ASSERT_EQ(16495ull, dtmc->getNumberOfTransitions()); - - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.9999965911265462636, quantitativeResult2[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0448979589010925, quantitativeResult3[0], storm::settings::getModule().getPrecision()); -} - -TEST(NativeDtmcPrctlModelCheckerTest, LRASingleBscc) { - 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, 1.); - matrixBuilder.addNextValue(1, 0, 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)); - - auto factory = std::make_unique>(); - factory->getSettings().setSolutionMethod(storm::solver::NativeLinearEquationSolverSettings::SolutionMethod::SOR); - factory->getSettings().setOmega(0.9); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::move(factory)); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(.5, quantitativeResult1[1], storm::settings::getModule().getPrecision()); - } - { - matrixBuilder = storm::storage::SparseMatrixBuilder(2, 2, 4); - matrixBuilder.addNextValue(0, 0, .5); - matrixBuilder.addNextValue(0, 1, .5); - matrixBuilder.addNextValue(1, 0, .5); - matrixBuilder.addNextValue(1, 1, .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)); - - auto factory = std::make_unique>(); - factory->getSettings().setSolutionMethod(storm::solver::NativeLinearEquationSolverSettings::SolutionMethod::SOR); - factory->getSettings().setOmega(0.9); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::move(factory)); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(.5, quantitativeResult1[1], storm::settings::getModule().getPrecision()); - } - - { - matrixBuilder = storm::storage::SparseMatrixBuilder(3, 3, 3); - matrixBuilder.addNextValue(0, 1, 1); - matrixBuilder.addNextValue(1, 2, 1); - matrixBuilder.addNextValue(2, 0, 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)); - - auto factory = std::make_unique>(); - factory->getSettings().setSolutionMethod(storm::solver::NativeLinearEquationSolverSettings::SolutionMethod::WalkerChae); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::move(factory)); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1. / 3., quantitativeResult1[0], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1. / 3., quantitativeResult1[1], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1. / 3., quantitativeResult1[2], storm::settings::getModule().getPrecision()); - } -} - -TEST(NativeDtmcPrctlModelCheckerTest, LRA) { - 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, 1); - matrixBuilder.addNextValue(1, 4, 0.7); - matrixBuilder.addNextValue(1, 6, 0.3); - matrixBuilder.addNextValue(2, 0, 1); - - matrixBuilder.addNextValue(3, 5, 0.8); - matrixBuilder.addNextValue(3, 9, 0.2); - matrixBuilder.addNextValue(4, 3, 1); - matrixBuilder.addNextValue(5, 3, 1); - - matrixBuilder.addNextValue(6, 7, 1); - matrixBuilder.addNextValue(7, 8, 1); - matrixBuilder.addNextValue(8, 6, 1); - - matrixBuilder.addNextValue(9, 10, 1); - matrixBuilder.addNextValue(10, 9, 1); - matrixBuilder.addNextValue(11, 9, 1); - - matrixBuilder.addNextValue(12, 5, 0.4); - matrixBuilder.addNextValue(12, 8, 0.3); - matrixBuilder.addNextValue(12, 11, 0.3); - - matrixBuilder.addNextValue(13, 7, 0.7); - matrixBuilder.addNextValue(13, 12, 0.3); - - matrixBuilder.addNextValue(14, 12, 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)); - - auto factory = std::make_unique>(); - factory->getSettings().setSolutionMethod(storm::solver::NativeLinearEquationSolverSettings::SolutionMethod::WalkerChae); - factory->getSettings().setPrecision(1e-7); - factory->getSettings().setMaximalNumberOfIterations(50000); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::move(factory)); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.3 / 3., quantitativeResult1[0], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0, quantitativeResult1[3], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1. / 3., quantitativeResult1[6], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0, quantitativeResult1[9], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.3/3., quantitativeResult1[12], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(.79 / 3., quantitativeResult1[13], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.3 / 3., quantitativeResult1[14], storm::settings::getModule().getPrecision()); - } -} diff --git a/src/test/storm/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp deleted file mode 100644 index f8aa35701..000000000 --- a/src/test/storm/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp +++ /dev/null @@ -1,617 +0,0 @@ -#include "gtest/gtest.h" -#include "storm-config.h" -#include "storm/settings/SettingMemento.h" -#include "storm/parser/PrismParser.h" -#include "storm/parser/FormulaParser.h" -#include "storm/logic/Formulas.h" -#include "storm/builder/DdPrismModelBuilder.h" -#include "storm/storage/dd/DdType.h" -#include "storm/storage/SymbolicModelDescription.h" - -#include "storm/solver/NativeLinearEquationSolver.h" -#include "storm/models/symbolic/StandardRewardModel.h" -#include "storm/modelchecker/csl/HybridCtmcCslModelChecker.h" -#include "storm/modelchecker/results/HybridQuantitativeCheckResult.h" -#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" -#include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h" - -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/GeneralSettings.h" - -#include "storm/settings/modules/NativeEquationSolverSettings.h" - -TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Cudd) { - // Parse the model description. - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - storm::parser::FormulaParser formulaParser(program); - std::shared_ptr formula(nullptr); - - // Build the model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("num_repairs"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); - std::shared_ptr> ctmc = model->as>(); - - // Create model checker. - storm::modelchecker::HybridCtmcCslModelChecker> modelchecker(*ctmc, std::make_unique>()); - - // Start checking properties. - formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=100 !\"minimum\"]"); - std::unique_ptr checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(5.5461254704419085E-5, quantitativeCheckResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(5.5461254704419085E-5, quantitativeCheckResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ F[100,100] !\"minimum\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(2.3397873548343415E-6, quantitativeCheckResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(2.3397873548343415E-6, quantitativeCheckResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ F[100,2000] !\"minimum\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U<=10 \"premium\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(1, quantitativeCheckResult4.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1, quantitativeCheckResult4.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"minimum\" U>=1 \"minimum\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0, quantitativeCheckResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0, quantitativeCheckResult5.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U>=1 !\"minimum\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.9999999033633374, quantitativeCheckResult6.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.9999999033633374, quantitativeCheckResult6.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [C<=100]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult7 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.8602815057967503, quantitativeCheckResult7.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.8602815057967503, quantitativeCheckResult7.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"minimum\"]"); - checkResult = modelchecker.check(*formula); - - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult8 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.99979112284455396, quantitativeCheckResult8.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.99979112284455396, quantitativeCheckResult8.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Sylvan) { - // Parse the model description. - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - storm::parser::FormulaParser formulaParser(program); - std::shared_ptr formula(nullptr); - - // Build the model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("num_repairs"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); - std::shared_ptr> ctmc = model->as>(); - - // Create model checker. - storm::modelchecker::HybridCtmcCslModelChecker> modelchecker(*ctmc, std::make_unique>()); - - // Start checking properties. - formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=100 !\"minimum\"]"); - std::unique_ptr checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(5.5461254704419085E-5, quantitativeCheckResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(5.5461254704419085E-5, quantitativeCheckResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ F[100,100] !\"minimum\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(2.3397873548343415E-6, quantitativeCheckResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(2.3397873548343415E-6, quantitativeCheckResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ F[100,2000] !\"minimum\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U<=10 \"premium\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(1, quantitativeCheckResult4.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1, quantitativeCheckResult4.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"minimum\" U>=1 \"minimum\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0, quantitativeCheckResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0, quantitativeCheckResult5.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U>=1 !\"minimum\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.9999999033633374, quantitativeCheckResult6.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.9999999033633374, quantitativeCheckResult6.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [C<=100]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult7 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.8602815057967503, quantitativeCheckResult7.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.8602815057967503, quantitativeCheckResult7.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"minimum\"]"); - checkResult = modelchecker.check(*formula); - - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult8 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.99979112284455396, quantitativeCheckResult8.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.99979112284455396, quantitativeCheckResult8.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Cudd) { - // Parse the model description. - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - storm::parser::FormulaParser formulaParser(program); - std::shared_ptr formula(nullptr); - - // Build the model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("up"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); - std::shared_ptr> ctmc = model->as>(); - - // Create model checker. - storm::modelchecker::HybridCtmcCslModelChecker> modelchecker(*ctmc, std::make_unique>()); - - // Start checking properties. - formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10000 \"down\"]"); - std::unique_ptr checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.0019216435246119591, quantitativeCheckResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0019216435246119591, quantitativeCheckResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_actuators\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(3.7079151806696567E-6, quantitativeCheckResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(3.7079151806696567E-6, quantitativeCheckResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_io\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.001556839327673734, quantitativeCheckResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.001556839327673734, quantitativeCheckResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_sensors\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [C<=10000]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(2.7745274082080154, quantitativeCheckResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(2.7745274082080154, quantitativeCheckResult5.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"fail_sensors\"]"); - checkResult = modelchecker.check(*formula); - - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.93458777106146362, quantitativeCheckResult6.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.93458777106146362, quantitativeCheckResult6.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Sylvan) { - - // Parse the model description. - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - storm::parser::FormulaParser formulaParser(program); - std::shared_ptr formula(nullptr); - - // Build the model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("up"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); - std::shared_ptr> ctmc = model->as>(); - - // Create model checker. - storm::modelchecker::HybridCtmcCslModelChecker> modelchecker(*ctmc, std::make_unique>()); - - // Start checking properties. - formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10000 \"down\"]"); - std::unique_ptr checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.0019216435246119591, quantitativeCheckResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0019216435246119591, quantitativeCheckResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_actuators\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(3.7079151806696567E-6, quantitativeCheckResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(3.7079151806696567E-6, quantitativeCheckResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_io\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.001556839327673734, quantitativeCheckResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.001556839327673734, quantitativeCheckResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_sensors\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [C<=10000]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(2.7745274082080154, quantitativeCheckResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(2.7745274082080154, quantitativeCheckResult5.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"fail_sensors\"]"); - checkResult = modelchecker.check(*formula); - - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.93458777106146362, quantitativeCheckResult6.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.93458777106146362, quantitativeCheckResult6.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Cudd) { - // Parse the model description. - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - storm::parser::FormulaParser formulaParser(program); - std::shared_ptr formula(nullptr); - - // Build the model. - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); - ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); - std::shared_ptr> ctmc = model->as>(); - - // Create model checker. - storm::modelchecker::HybridCtmcCslModelChecker> modelchecker(*ctmc, std::make_unique>()); - - // Start checking properties. - formula = formulaParser.parseSingleFormulaFromString("P=?[ F<=10 \"target\"]"); - std::unique_ptr checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(1, quantitativeCheckResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1, quantitativeCheckResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"target\"]"); - checkResult = modelchecker.check(*formula); - - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.20079750055570736, quantitativeCheckResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.20079750055570736, quantitativeCheckResult2.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Sylvan) { - - // Parse the model description. - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - storm::parser::FormulaParser formulaParser(program); - std::shared_ptr formula(nullptr); - - // Build the model. - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); - ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); - std::shared_ptr> ctmc = model->as>(); - - // Create model checker. - storm::modelchecker::HybridCtmcCslModelChecker> modelchecker(*ctmc, std::make_unique>()); - - // Start checking properties. - formula = formulaParser.parseSingleFormulaFromString("P=?[ F<=10 \"target\"]"); - std::unique_ptr checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(1, quantitativeCheckResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1, quantitativeCheckResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"target\"]"); - checkResult = modelchecker.check(*formula); - - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.20079750055570736, quantitativeCheckResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.20079750055570736, quantitativeCheckResult2.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(NativeHybridCtmcCslModelCheckerTest, Fms) { - - // No properties to check at this point. -} - -TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Cudd) { - - // Parse the model description. - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - storm::parser::FormulaParser formulaParser(program); - std::shared_ptr formula(nullptr); - - // Build the model with the customers reward structure. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("customers"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); - std::shared_ptr> ctmc = model->as>(); - - // Create model checker. - storm::modelchecker::HybridCtmcCslModelChecker> modelchecker(*ctmc, std::make_unique>()); - - // Start checking properties. - formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"network_full\" ]"); - std::unique_ptr checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.015446370562428037, quantitativeCheckResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.015446370562428037, quantitativeCheckResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"first_queue_full\" ]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.999999837225515, quantitativeCheckResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.999999837225515, quantitativeCheckResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [\"second_queue_full\" U<=1 !\"second_queue_full\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(1, quantitativeCheckResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1, quantitativeCheckResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [I=10]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(5.679243850315877, quantitativeCheckResult4.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(5.679243850315877, quantitativeCheckResult4.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [C<=10]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(55.44792186036232, quantitativeCheckResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(55.44792186036232, quantitativeCheckResult5.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"first_queue_full\"&\"second_queue_full\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(262.78571505691389, quantitativeCheckResult6.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(262.78571505691389, quantitativeCheckResult6.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"first_queue_full\"]"); - checkResult = modelchecker.check(*formula); - - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult7 = checkResult->asHybridQuantitativeCheckResult(); - - // FIXME: because of divergence, these results are not correct. -// EXPECT_NEAR(0.9100373532, quantitativeCheckResult7.getMin(), storm::settings::getModule().getPrecision()); -// EXPECT_NEAR(0.9100373532, quantitativeCheckResult7.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Sylvan) { - // Parse the model description. - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - storm::parser::FormulaParser formulaParser(program); - std::shared_ptr formula(nullptr); - - // Build the model with the customers reward structure. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("customers"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); - std::shared_ptr> ctmc = model->as>(); - - // Create model checker. - storm::modelchecker::HybridCtmcCslModelChecker> modelchecker(*ctmc, std::make_unique>()); - - // Start checking properties. - formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"network_full\" ]"); - std::unique_ptr checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.015446370562428037, quantitativeCheckResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.015446370562428037, quantitativeCheckResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"first_queue_full\" ]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.999999837225515, quantitativeCheckResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.999999837225515, quantitativeCheckResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [\"second_queue_full\" U<=1 !\"second_queue_full\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(1, quantitativeCheckResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1, quantitativeCheckResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [I=10]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(5.679243850315877, quantitativeCheckResult4.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(5.679243850315877, quantitativeCheckResult4.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [C<=10]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(55.44792186036232, quantitativeCheckResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(55.44792186036232, quantitativeCheckResult5.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"first_queue_full\"&\"second_queue_full\"]"); - checkResult = modelchecker.check(*formula); - - ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(262.78571505691389, quantitativeCheckResult6.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(262.78571505691389, quantitativeCheckResult6.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"first_queue_full\"]"); - checkResult = modelchecker.check(*formula); - - checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult7 = checkResult->asHybridQuantitativeCheckResult(); - - // FIXME: because of divergence, these results are not correct. -// EXPECT_NEAR(0.9100373532, quantitativeCheckResult7.getMin(), storm::settings::getModule().getPrecision()); -// EXPECT_NEAR(0.9100373532, quantitativeCheckResult7.getMax(), storm::settings::getModule().getPrecision()); -} diff --git a/src/test/storm/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp deleted file mode 100644 index 6398b2c1e..000000000 --- a/src/test/storm/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp +++ /dev/null @@ -1,339 +0,0 @@ -#include "gtest/gtest.h" -#include "storm-config.h" - -#include "storm/parser/FormulaParser.h" -#include "storm/logic/Formulas.h" -#include "storm/solver/NativeLinearEquationSolver.h" -#include "storm/storage/SymbolicModelDescription.h" -#include "storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h" -#include "storm/modelchecker/results/HybridQuantitativeCheckResult.h" -#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" -#include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h" -#include "storm/parser/PrismParser.h" -#include "storm/builder/DdPrismModelBuilder.h" -#include "storm/models/symbolic/StandardRewardModel.h" -#include "storm/models/symbolic/Dtmc.h" -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/GeneralSettings.h" -#include "storm/settings/modules/GmmxxEquationSolverSettings.h" -#include "storm/settings/modules/NativeEquationSolverSettings.h" - -TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_Cudd) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("coin_flips"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(13ul, model->getNumberOfStates()); - EXPECT_EQ(20ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = model->as>(); - - storm::modelchecker::HybridDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(3.6666646003723145, quantitativeResult4.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(3.6666646003723145, quantitativeResult4.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_Sylvan) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("coin_flips"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(13ul, model->getNumberOfStates()); - EXPECT_EQ(20ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = model->as>(); - - storm::modelchecker::HybridDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(3.6666646003723145, quantitativeResult4.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(3.6666646003723145, quantitativeResult4.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_Cudd) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm"); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_EQ(8607ul, model->getNumberOfStates()); - EXPECT_EQ(15113ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = model->as>(); - - storm::modelchecker::HybridDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.33288205191646525, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.33288205191646525, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.15222066094730619, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.15222066094730619, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.32153900158185761, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.32153900158185761, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm"); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_EQ(8607ul, model->getNumberOfStates()); - EXPECT_EQ(15113ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = model->as>(); - - storm::modelchecker::HybridDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.33288205191646525, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.33288205191646525, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.15222066094730619, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.15222066094730619, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.32153900158185761, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.32153900158185761, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm"); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("num_rounds"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(273ul, model->getNumberOfStates()); - EXPECT_EQ(397ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = model->as>(); - - storm::modelchecker::HybridDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1.0, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(1.0416666666666643, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0416666666666643, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm"); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("num_rounds"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(273ul, model->getNumberOfStates()); - EXPECT_EQ(397ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = model->as>(); - - storm::modelchecker::HybridDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1.0, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(1.0416666666666643, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0416666666666643, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); -} diff --git a/src/test/storm/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp deleted file mode 100644 index 97ed361ce..000000000 --- a/src/test/storm/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp +++ /dev/null @@ -1,460 +0,0 @@ -#include "gtest/gtest.h" -#include "storm-config.h" - -#include "storm/parser/FormulaParser.h" -#include "storm/logic/Formulas.h" -#include "storm/utility/solver.h" -#include "storm/storage/SymbolicModelDescription.h" -#include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h" -#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" -#include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h" -#include "storm/solver/SymbolicEliminationLinearEquationSolver.h" -#include "storm/parser/PrismParser.h" -#include "storm/builder/DdPrismModelBuilder.h" -#include "storm/models/symbolic/StandardRewardModel.h" -#include "storm/models/symbolic/Dtmc.h" -#include "storm/settings/SettingsManager.h" - -#include "storm/settings/modules/NativeEquationSolverSettings.h" - -#include "storm/settings/modules/GeneralSettings.h" - -TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Cudd) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("coin_flips"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(13ul, model->getNumberOfStates()); - EXPECT_EQ(20ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = model->as>(); - - storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::GeneralSymbolicLinearEquationSolverFactory())); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(3.6666646003723145, quantitativeResult4.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(3.6666646003723145, quantitativeResult4.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Sylvan) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("coin_flips"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(13ul, model->getNumberOfStates()); - EXPECT_EQ(20ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = model->as>(); - - storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::GeneralSymbolicLinearEquationSolverFactory())); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult(); - - // FIXME: precision is not optimal. - EXPECT_NEAR(3.6666622161865234, quantitativeResult4.getMin(), 10 * storm::settings::getModule().getPrecision()); - EXPECT_NEAR(3.6666622161865234, quantitativeResult4.getMax(), 10 * storm::settings::getModule().getPrecision()); -} - -TEST(SymbolicDtmcPrctlModelCheckerTest, Die_RationalNumber_Sylvan) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - // Build the die model with its reward model. - typename storm::builder::DdPrismModelBuilder::Options options; - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("coin_flips"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(13ul, model->getNumberOfStates()); - EXPECT_EQ(20ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = model->as>(); - - storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::SymbolicEliminationLinearEquationSolverFactory())); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_EQ(quantitativeResult1.getMin(), storm::utility::convertNumber(std::string("1/6"))); - EXPECT_EQ(quantitativeResult1.getMax(), storm::utility::convertNumber(std::string("1/6"))); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_EQ(quantitativeResult2.getMin(), storm::utility::convertNumber(std::string("1/6"))); - EXPECT_EQ(quantitativeResult2.getMax(), storm::utility::convertNumber(std::string("1/6"))); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_EQ(quantitativeResult3.getMin(), storm::utility::convertNumber(std::string("1/6"))); - EXPECT_EQ(quantitativeResult3.getMax(), storm::utility::convertNumber(std::string("1/6"))); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_EQ(quantitativeResult4.getMin(), storm::utility::convertNumber(std::string("11/3"))); - EXPECT_EQ(quantitativeResult4.getMax(), storm::utility::convertNumber(std::string("11/3"))); -} - -TEST(SymbolicDtmcPrctlModelCheckerTest, Die_RationalFunction_Sylvan) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/pdtmc/parametric_die.pm"); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - // Build the die model with its reward model. - typename storm::builder::DdPrismModelBuilder::Options options; - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("coin_flips"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(13ul, model->getNumberOfStates()); - EXPECT_EQ(20ul, model->getNumberOfTransitions()); - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - - std::map instantiation; - std::set variables = model->getParameters(); - ASSERT_EQ(1ull, variables.size()); - instantiation.emplace(*variables.begin(), storm::utility::convertNumber(std::string("1/2"))); - - std::shared_ptr> dtmc = model->as>(); - - storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::SymbolicEliminationLinearEquationSolverFactory())); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_EQ(storm::utility::convertNumber(quantitativeResult1.sum().evaluate(instantiation)), storm::utility::convertNumber(std::string("1/6"))); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_EQ(storm::utility::convertNumber(quantitativeResult2.sum().evaluate(instantiation)), storm::utility::convertNumber(std::string("1/6"))); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_EQ(storm::utility::convertNumber(quantitativeResult3.sum().evaluate(instantiation)), storm::utility::convertNumber(std::string("1/6"))); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_EQ(storm::utility::convertNumber(quantitativeResult4.sum().evaluate(instantiation)), storm::utility::convertNumber(std::string("11/3"))); -} - -TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Cudd) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm"); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_EQ(8607ul, model->getNumberOfStates()); - EXPECT_EQ(15113ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = model->as>(); - - storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::GeneralSymbolicLinearEquationSolverFactory())); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(0.3328777473921436, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.3328777473921436, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(0.15221847380560186, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.15221847380560186, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(0.32153516079959443, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.32153516079959443, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Sylvan) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm"); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_EQ(8607ul, model->getNumberOfStates()); - EXPECT_EQ(15113ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = model->as>(); - - storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::GeneralSymbolicLinearEquationSolverFactory())); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); - - // FIXME: precision not optimal. - EXPECT_NEAR(0.33288236360191303, quantitativeResult1.getMin(), 10 * storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.33288236360191303, quantitativeResult1.getMax(), 10 * storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); - - // FIXME: precision not optimal. - EXPECT_NEAR(0.15222081144084315, quantitativeResult2.getMin(), 10 * storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.15222081144084315, quantitativeResult2.getMax(), 10 * storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); - - // FIXME: precision not optimal. - EXPECT_NEAR(0.3215392962289586, quantitativeResult3.getMin(), 10 * storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.3215392962289586, quantitativeResult3.getMax(), 10 * storm::settings::getModule().getPrecision()); -} - -TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm"); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("num_rounds"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(273ul, model->getNumberOfStates()); - EXPECT_EQ(397ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = model->as>(); - - storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::GeneralSymbolicLinearEquationSolverFactory())); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1.0, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1.0416666666666643, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0416666666666643, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm"); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("num_rounds"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(273ul, model->getNumberOfStates()); - EXPECT_EQ(397ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = model->as>(); - - storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::GeneralSymbolicLinearEquationSolverFactory())); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1.0, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1.0416666666666643, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0416666666666643, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); -}