Browse Source
refactored some tests -- making testing with different settings/environments more easy
main
refactored some tests -- making testing with different settings/environments more easy
main
20 changed files with 1436 additions and 2750 deletions
-
736src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp
-
574src/test/storm-pars/modelchecker/SparseMdpParameterLiftingTest.cpp
-
200src/test/storm/modelchecker/ExplicitMdpPrctlModelCheckerTest.cpp
-
380src/test/storm/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
-
273src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
-
272src/test/storm/modelchecker/LpMdpPrctlModelCheckerTest.cpp
-
189src/test/storm/modelchecker/LraMdpPrctlModelCheckerTest.cpp
-
278src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp
-
374src/test/storm/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
-
142src/test/storm/modelchecker/SchedulerGenerationMdpPrctlModelCheckerTest.cpp
-
6src/test/storm/modelchecker/SparseMaCbMultiObjectiveModelCheckerTest.cpp
-
27src/test/storm/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp
-
10src/test/storm/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp
-
63src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp
-
21src/test/storm/modelchecker/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp
-
377src/test/storm/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp
-
192src/test/storm/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp
-
14src/test/storm/solver/MinMaxLinearEquationSolverTest.cpp
-
30src/test/storm/testmacros.h
-
28src/test/storm_gtest.h
@ -0,0 +1,200 @@ |
|||
#include "gtest/gtest.h"
|
|||
#include "storm-config.h"
|
|||
|
|||
#include "storm/parser/FormulaParser.h"
|
|||
#include "storm/logic/Formulas.h"
|
|||
#include "storm/solver/StandardMinMaxLinearEquationSolver.h"
|
|||
#include "storm/models/sparse/StandardRewardModel.h"
|
|||
#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
|
|||
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
|
|||
#include "storm/settings/SettingsManager.h"
|
|||
#include "storm/settings/modules/GeneralSettings.h"
|
|||
|
|||
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
|
|||
|
|||
#include "storm/settings/modules/NativeEquationSolverSettings.h"
|
|||
#include "storm/parser/AutoParser.h"
|
|||
#include "storm/parser/PrismParser.h"
|
|||
#include "storm/builder/ExplicitModelBuilder.h"
|
|||
|
|||
TEST(ExplicitMdpPrctlModelCheckerTest, Dice) { |
|||
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", "", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.trans.rew"); |
|||
storm::Environment env; |
|||
// Increase precision a little to get more accurate results
|
|||
env.solver().minMax().setPrecision(env.solver().minMax().getPrecision() * storm::utility::convertNumber<storm::RationalNumber>(1e-2)); |
|||
|
|||
// A parser that we use for conveniently constructing the formulas.
|
|||
storm::parser::FormulaParser formulaParser; |
|||
|
|||
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); |
|||
|
|||
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>(); |
|||
|
|||
ASSERT_EQ(mdp->getNumberOfStates(), 169ull); |
|||
ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); |
|||
|
|||
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp); |
|||
|
|||
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(env, *formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(1.0/36.0, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); |
|||
|
|||
result = checker.check(env, *formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(1.0/36.0, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); |
|||
|
|||
result = checker.check(env, *formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(2.0/36.0, quantitativeResult3[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); |
|||
|
|||
result = checker.check(env, *formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(2.0/36.0, quantitativeResult4[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); |
|||
|
|||
result = checker.check(env, *formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(3.0/36.0, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); |
|||
|
|||
result = checker.check(env, *formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(3.0/36.0, quantitativeResult6[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); |
|||
|
|||
result = checker.check(env, *formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult7 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(22.0/3.0, quantitativeResult7[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); |
|||
|
|||
result = checker.check(env, *formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult8 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(22.0/3.0, quantitativeResult8[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew", ""); |
|||
|
|||
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); |
|||
|
|||
std::shared_ptr<storm::models::sparse::Mdp<double>> stateRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>(); |
|||
|
|||
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateRewardModelChecker(*mdp); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); |
|||
|
|||
result = stateRewardModelChecker.check(env, *formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult9 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(22.0/3.0, quantitativeResult9[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); |
|||
|
|||
result = stateRewardModelChecker.check(env, *formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult10 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(22.0/3.0, quantitativeResult10[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.trans.rew"); |
|||
|
|||
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); |
|||
|
|||
std::shared_ptr<storm::models::sparse::Mdp<double>> stateAndTransitionRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>(); |
|||
|
|||
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); |
|||
|
|||
result = stateAndTransitionRewardModelChecker.check(env, *formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult11 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(44.0/3.0, quantitativeResult11[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); |
|||
|
|||
result = stateAndTransitionRewardModelChecker.check(env, *formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult12 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(44.0/3.0, quantitativeResult12[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
} |
|||
|
|||
TEST(ExplicitMdpPrctlModelCheckerTest, AsynchronousLeader) { |
|||
storm::Environment env; |
|||
// Increase precision a little to get more accurate results
|
|||
env.solver().minMax().setPrecision(env.solver().minMax().getPrecision() * storm::utility::convertNumber<storm::RationalNumber>(1e-2)); |
|||
|
|||
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/leader4.tra", STORM_TEST_RESOURCES_DIR "/lab/leader4.lab", "", STORM_TEST_RESOURCES_DIR "/rew/leader4.trans.rew"); |
|||
|
|||
// A parser that we use for conveniently constructing the formulas.
|
|||
storm::parser::FormulaParser formulaParser; |
|||
|
|||
ASSERT_EQ(storm::models::ModelType::Mdp, abstractModel->getType()); |
|||
|
|||
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>(); |
|||
|
|||
ASSERT_EQ(3172ull, mdp->getNumberOfStates()); |
|||
ASSERT_EQ(7144ull, mdp->getNumberOfTransitions()); |
|||
|
|||
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp); |
|||
|
|||
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(env, *formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); |
|||
|
|||
result = checker.check(env, *formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(1.0, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); |
|||
|
|||
result = checker.check(env, *formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(1.0/16.0, quantitativeResult3[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); |
|||
|
|||
result = checker.check(env, *formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(1.0/16.0, quantitativeResult4[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); |
|||
|
|||
result = checker.check(env, *formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(30.0/7.0, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); |
|||
|
|||
result = checker.check(env, *formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(30.0/7.0, quantitativeResult6[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
} |
|||
|
@ -1,380 +0,0 @@ |
|||
#include "gtest/gtest.h"
|
|||
#include "storm-config.h"
|
|||
|
|||
#include "storm/logic/Formulas.h"
|
|||
#include "storm/solver/StandardMinMaxLinearEquationSolver.h"
|
|||
#include "storm/modelchecker/prctl/HybridMdpPrctlModelChecker.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/parser/FormulaParser.h"
|
|||
#include "storm/builder/DdPrismModelBuilder.h"
|
|||
#include "storm/storage/SymbolicModelDescription.h"
|
|||
#include "storm/models/symbolic/Dtmc.h"
|
|||
#include "storm/models/symbolic/Mdp.h"
|
|||
#include "storm/models/symbolic/StandardRewardModel.h"
|
|||
#include "storm/settings/SettingsManager.h"
|
|||
|
|||
#include "storm/settings/SettingsManager.h"
|
|||
#include "storm/settings/modules/GeneralSettings.h"
|
|||
#include "storm/settings/modules/NativeEquationSolverSettings.h"
|
|||
#include "storm/settings/modules/GmmxxEquationSolverSettings.h"
|
|||
|
|||
TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Cudd) { |
|||
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); |
|||
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<storm::dd::DdType::CUDD>::Options options; |
|||
#else
|
|||
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options; |
|||
#endif
|
|||
options.buildAllRewardModels = false; |
|||
options.rewardModelsToBuild.insert("coinflips"); |
|||
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program, options); |
|||
EXPECT_EQ(169ul, model->getNumberOfStates()); |
|||
EXPECT_EQ(436ul, model->getNumberOfTransitions()); |
|||
|
|||
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); |
|||
|
|||
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>(); |
|||
|
|||
storm::modelchecker::HybridMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>> checker(*mdp, std::make_unique<storm::solver::GmmxxMinMaxLinearEquationSolverFactory<double>>()); |
|||
|
|||
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult1 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult2 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult3 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult4 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult6 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult7 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(7.3333333333333375, quantitativeResult7.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(7.3333333333333375, quantitativeResult7.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult8 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(7.3333316743373871, quantitativeResult8.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(7.3333316743373871, quantitativeResult8.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
} |
|||
|
|||
TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Sylvan) { |
|||
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); |
|||
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<storm::dd::DdType::Sylvan>::Options options; |
|||
#else
|
|||
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::Options options; |
|||
#endif
|
|||
options.buildAllRewardModels = false; |
|||
options.rewardModelsToBuild.insert("coinflips"); |
|||
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program, options); |
|||
EXPECT_EQ(169ul, model->getNumberOfStates()); |
|||
EXPECT_EQ(436ul, model->getNumberOfTransitions()); |
|||
|
|||
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); |
|||
|
|||
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>(); |
|||
|
|||
storm::modelchecker::HybridMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>> checker(*mdp, std::make_unique<storm::solver::GmmxxMinMaxLinearEquationSolverFactory<double>>()); |
|||
|
|||
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult1 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult2 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult3 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult4 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult6 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult7 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(7.3333333333333375, quantitativeResult7.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(7.3333333333333375, quantitativeResult7.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult8 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(7.3333316743373871, quantitativeResult8.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(7.3333316743373871, quantitativeResult8.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
} |
|||
|
|||
TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { |
|||
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader4.nm"); |
|||
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<storm::dd::DdType::CUDD>::Options options; |
|||
#else
|
|||
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options; |
|||
#endif
|
|||
options.buildAllRewardModels = false; |
|||
options.rewardModelsToBuild.insert("rounds"); |
|||
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program, options); |
|||
EXPECT_EQ(3172ul, model->getNumberOfStates()); |
|||
EXPECT_EQ(7144ul, model->getNumberOfTransitions()); |
|||
|
|||
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); |
|||
|
|||
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>(); |
|||
|
|||
storm::modelchecker::HybridMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>> checker(*mdp, std::make_unique<storm::solver::GmmxxMinMaxLinearEquationSolverFactory<double>>()); |
|||
|
|||
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(1, quantitativeResult2.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult3 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(0.0625, quantitativeResult3.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0625, quantitativeResult3.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult4 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0625, quantitativeResult4.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(4.285716, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(4.285716, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult6 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(4.2857120959008661, quantitativeResult6.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(4.2857120959008661, quantitativeResult6.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
} |
|||
|
|||
TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { |
|||
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader4.nm"); |
|||
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<storm::dd::DdType::Sylvan>::Options options; |
|||
#else
|
|||
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::Options options; |
|||
#endif
|
|||
options.buildAllRewardModels = false; |
|||
options.rewardModelsToBuild.insert("rounds"); |
|||
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program, options); |
|||
EXPECT_EQ(3172ul, model->getNumberOfStates()); |
|||
EXPECT_EQ(7144ul, model->getNumberOfTransitions()); |
|||
|
|||
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); |
|||
|
|||
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>(); |
|||
|
|||
storm::modelchecker::HybridMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>> checker(*mdp, std::make_unique<storm::solver::GmmxxMinMaxLinearEquationSolverFactory<double>>()); |
|||
|
|||
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(1, quantitativeResult2.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult3 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(0.0625, quantitativeResult3.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0625, quantitativeResult3.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult4 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0625, quantitativeResult4.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(4.285716, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(4.285716, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult6 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(4.2857120959008661, quantitativeResult6.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(4.2857120959008661, quantitativeResult6.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
} |
|||
|
@ -1,273 +0,0 @@ |
|||
#include "gtest/gtest.h"
|
|||
#include "storm-config.h"
|
|||
|
|||
#include "storm/parser/FormulaParser.h"
|
|||
#include "storm/logic/Formulas.h"
|
|||
#include "storm/solver/StandardMinMaxLinearEquationSolver.h"
|
|||
#include "storm/models/sparse/StandardRewardModel.h"
|
|||
#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
|
|||
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
|
|||
#include "storm/settings/SettingsManager.h"
|
|||
#include "storm/settings/modules/GeneralSettings.h"
|
|||
|
|||
#include "storm/settings/modules/GmmxxEquationSolverSettings.h"
|
|||
|
|||
#include "storm/settings/modules/NativeEquationSolverSettings.h"
|
|||
#include "storm/parser/AutoParser.h"
|
|||
#include "storm/parser/PrismParser.h"
|
|||
#include "storm/builder/ExplicitModelBuilder.h"
|
|||
|
|||
TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { |
|||
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", "", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.trans.rew"); |
|||
|
|||
// A parser that we use for conveniently constructing the formulas.
|
|||
storm::parser::FormulaParser formulaParser; |
|||
|
|||
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); |
|||
|
|||
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>(); |
|||
|
|||
ASSERT_EQ(mdp->getNumberOfStates(), 169ull); |
|||
ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); |
|||
|
|||
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::make_unique<storm::solver::GmmxxMinMaxLinearEquationSolverFactory<double>>()); |
|||
|
|||
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult3[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult7 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(7.3333333333333375, quantitativeResult7[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult8 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(7.3333316743373871, quantitativeResult8[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew", ""); |
|||
|
|||
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); |
|||
|
|||
std::shared_ptr<storm::models::sparse::Mdp<double>> stateRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>(); |
|||
|
|||
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateRewardModelChecker(*mdp, std::make_unique<storm::solver::GmmxxMinMaxLinearEquationSolverFactory<double>>()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); |
|||
|
|||
result = stateRewardModelChecker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult9 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(7.3333333333333375, quantitativeResult9[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); |
|||
|
|||
result = stateRewardModelChecker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult10 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(7.3333316743373871, quantitativeResult10[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.trans.rew"); |
|||
|
|||
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); |
|||
|
|||
std::shared_ptr<storm::models::sparse::Mdp<double>> stateAndTransitionRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>(); |
|||
|
|||
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::make_unique<storm::solver::GmmxxMinMaxLinearEquationSolverFactory<double>>()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); |
|||
|
|||
result = stateAndTransitionRewardModelChecker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult11 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(14.6666677, quantitativeResult11[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); |
|||
|
|||
result = stateAndTransitionRewardModelChecker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult12 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(14.666663348674774, quantitativeResult12[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
} |
|||
|
|||
TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { |
|||
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/leader4.tra", STORM_TEST_RESOURCES_DIR "/lab/leader4.lab", "", STORM_TEST_RESOURCES_DIR "/rew/leader4.trans.rew"); |
|||
|
|||
// A parser that we use for conveniently constructing the formulas.
|
|||
storm::parser::FormulaParser formulaParser; |
|||
|
|||
ASSERT_EQ(storm::models::ModelType::Mdp, abstractModel->getType()); |
|||
|
|||
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>(); |
|||
|
|||
ASSERT_EQ(3172ull, mdp->getNumberOfStates()); |
|||
ASSERT_EQ(7144ull, mdp->getNumberOfTransitions()); |
|||
|
|||
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::make_unique<storm::solver::GmmxxMinMaxLinearEquationSolverFactory<double>>()); |
|||
|
|||
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(1, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(1, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(0.0625, quantitativeResult3[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(0.0625, quantitativeResult4[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(4.285716, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(4.2857120959008661, quantitativeResult6[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
} |
|||
|
|||
TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) { |
|||
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/scheduler_generation.nm"); |
|||
|
|||
// A parser that we use for conveniently constructing the formulas.
|
|||
storm::parser::FormulaParser formulaParser; |
|||
|
|||
storm::generator::NextStateGeneratorOptions options; |
|||
options.setBuildAllLabels(); |
|||
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, options).build(); |
|||
EXPECT_EQ(4ull, model->getNumberOfStates()); |
|||
EXPECT_EQ(11ull, model->getNumberOfTransitions()); |
|||
|
|||
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); |
|||
|
|||
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = model->as<storm::models::sparse::Mdp<double>>(); |
|||
|
|||
EXPECT_EQ(7ull, mdp->getNumberOfChoices()); |
|||
|
|||
auto solverFactory = std::make_unique<storm::solver::GmmxxMinMaxLinearEquationSolverFactory<double>>(storm::solver::MinMaxMethodSelection::PolicyIteration); |
|||
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::move(solverFactory)); |
|||
|
|||
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"target\"]"); |
|||
|
|||
storm::modelchecker::CheckTask<storm::logic::Formula> checkTask(*formula); |
|||
checkTask.setProduceSchedulers(true); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(checkTask); |
|||
|
|||
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); |
|||
ASSERT_TRUE(result->asExplicitQuantitativeCheckResult<double>().hasScheduler()); |
|||
storm::storage::Scheduler<double> const& scheduler = result->asExplicitQuantitativeCheckResult<double>().getScheduler(); |
|||
EXPECT_EQ(0ull, scheduler.getChoice(0).getDeterministicChoice()); |
|||
EXPECT_EQ(1ull, scheduler.getChoice(1).getDeterministicChoice()); |
|||
EXPECT_EQ(0ull, scheduler.getChoice(2).getDeterministicChoice()); |
|||
EXPECT_EQ(0ull, scheduler.getChoice(3).getDeterministicChoice()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"target\"]"); |
|||
|
|||
checkTask = storm::modelchecker::CheckTask<storm::logic::Formula>(*formula); |
|||
checkTask.setProduceSchedulers(true); |
|||
result = checker.check(checkTask); |
|||
|
|||
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); |
|||
ASSERT_TRUE(result->asExplicitQuantitativeCheckResult<double>().hasScheduler()); |
|||
storm::storage::Scheduler<double> const& scheduler2 = result->asExplicitQuantitativeCheckResult<double>().getScheduler(); |
|||
EXPECT_EQ(1ull, scheduler2.getChoice(0).getDeterministicChoice()); |
|||
EXPECT_EQ(2ull, scheduler2.getChoice(1).getDeterministicChoice()); |
|||
EXPECT_EQ(0ull, scheduler2.getChoice(2).getDeterministicChoice()); |
|||
EXPECT_EQ(0ull, scheduler2.getChoice(3).getDeterministicChoice()); |
|||
} |
|||
|
|||
TEST(GmmxxMdpPrctlModelCheckerTest, TinyRewards) { |
|||
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/tiny_rewards.nm"); |
|||
|
|||
// A parser that we use for conveniently constructing the formulas.
|
|||
storm::parser::FormulaParser formulaParser; |
|||
|
|||
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(true, true)).build(); |
|||
EXPECT_EQ(3ull, model->getNumberOfStates()); |
|||
EXPECT_EQ(4ull, model->getNumberOfTransitions()); |
|||
|
|||
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); |
|||
|
|||
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = model->as<storm::models::sparse::Mdp<double>>(); |
|||
|
|||
EXPECT_EQ(4ull, mdp->getNumberOfChoices()); |
|||
|
|||
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::make_unique<storm::solver::GmmxxMinMaxLinearEquationSolverFactory<double>>()); |
|||
|
|||
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"target\"]"); |
|||
|
|||
storm::modelchecker::CheckTask<storm::logic::Formula> checkTask(*formula); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(checkTask); |
|||
|
|||
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); |
|||
EXPECT_NEAR(1, result->asExplicitQuantitativeCheckResult<double>().getValueVector()[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(1, result->asExplicitQuantitativeCheckResult<double>().getValueVector()[1], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0, result->asExplicitQuantitativeCheckResult<double>().getValueVector()[2], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
} |
@ -1,272 +0,0 @@ |
|||
#include "gtest/gtest.h"
|
|||
#include "storm-config.h"
|
|||
|
|||
#include "storm/parser/FormulaParser.h"
|
|||
#include "storm/logic/Formulas.h"
|
|||
#include "storm/solver/LpMinMaxLinearEquationSolver.h"
|
|||
#include "storm/models/sparse/StandardRewardModel.h"
|
|||
#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
|
|||
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
|
|||
#include "storm/settings/SettingsManager.h"
|
|||
#include "storm/settings/modules/GeneralSettings.h"
|
|||
|
|||
#include "storm/parser/AutoParser.h"
|
|||
#include "storm/parser/PrismParser.h"
|
|||
#include "storm/builder/ExplicitModelBuilder.h"
|
|||
|
|||
TEST(LpMdpPrctlModelCheckerTest, Dice) { |
|||
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", "", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.trans.rew"); |
|||
|
|||
// A parser that we use for conveniently constructing the formulas.
|
|||
storm::parser::FormulaParser formulaParser; |
|||
|
|||
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); |
|||
|
|||
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>(); |
|||
|
|||
ASSERT_EQ(mdp->getNumberOfStates(), 169ull); |
|||
ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); |
|||
|
|||
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::make_unique<storm::solver::LpMinMaxLinearEquationSolverFactory<double>>()); |
|||
|
|||
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult3[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult7 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(7.333333333, quantitativeResult7[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult8 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(7.333333333, quantitativeResult8[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew", ""); |
|||
|
|||
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); |
|||
|
|||
std::shared_ptr<storm::models::sparse::Mdp<double>> stateRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>(); |
|||
|
|||
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateRewardModelChecker(*mdp, std::make_unique<storm::solver::LpMinMaxLinearEquationSolverFactory<double>>()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); |
|||
|
|||
result = stateRewardModelChecker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult9 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(7.333333333, quantitativeResult9[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); |
|||
|
|||
result = stateRewardModelChecker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult10 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(7.333333333, quantitativeResult10[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.trans.rew"); |
|||
|
|||
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); |
|||
|
|||
std::shared_ptr<storm::models::sparse::Mdp<double>> stateAndTransitionRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>(); |
|||
|
|||
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::make_unique<storm::solver::LpMinMaxLinearEquationSolverFactory<double>>()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); |
|||
|
|||
result = stateAndTransitionRewardModelChecker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult11 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(14.666666666, quantitativeResult11[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); |
|||
|
|||
result = stateAndTransitionRewardModelChecker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult12 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(14.666666666, quantitativeResult12[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
} |
|||
|
|||
TEST(LpMdpPrctlModelCheckerTest, AsynchronousLeader) { |
|||
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/leader4.tra", STORM_TEST_RESOURCES_DIR "/lab/leader4.lab", "", STORM_TEST_RESOURCES_DIR "/rew/leader4.trans.rew"); |
|||
|
|||
// A parser that we use for conveniently constructing the formulas.
|
|||
storm::parser::FormulaParser formulaParser; |
|||
|
|||
ASSERT_EQ(storm::models::ModelType::Mdp, abstractModel->getType()); |
|||
|
|||
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>(); |
|||
|
|||
ASSERT_EQ(3172ull, mdp->getNumberOfStates()); |
|||
ASSERT_EQ(7144ull, mdp->getNumberOfTransitions()); |
|||
|
|||
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::make_unique<storm::solver::LpMinMaxLinearEquationSolverFactory<double>>()); |
|||
|
|||
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(1, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(1, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(0.0625, quantitativeResult3[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(0.0625, quantitativeResult4[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(4.285714286, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
EXPECT_NEAR(4.285714286, quantitativeResult6[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
} |
|||
|
|||
TEST(LpMdpPrctlModelCheckerTest, SchedulerGeneration) { |
|||
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/scheduler_generation.nm"); |
|||
|
|||
// A parser that we use for conveniently constructing the formulas.
|
|||
storm::parser::FormulaParser formulaParser; |
|||
|
|||
storm::generator::NextStateGeneratorOptions options; |
|||
options.setBuildAllLabels(); |
|||
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, options).build(); |
|||
EXPECT_EQ(4ull, model->getNumberOfStates()); |
|||
EXPECT_EQ(11ull, model->getNumberOfTransitions()); |
|||
|
|||
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); |
|||
|
|||
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = model->as<storm::models::sparse::Mdp<double>>(); |
|||
|
|||
EXPECT_EQ(7ull, mdp->getNumberOfChoices()); |
|||
|
|||
auto solverFactory = std::make_unique<storm::solver::LpMinMaxLinearEquationSolverFactory<double>>(); |
|||
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::move(solverFactory)); |
|||
|
|||
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"target\"]"); |
|||
|
|||
storm::modelchecker::CheckTask<storm::logic::Formula> checkTask(*formula); |
|||
checkTask.setProduceSchedulers(true); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(checkTask); |
|||
|
|||
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); |
|||
ASSERT_TRUE(result->asExplicitQuantitativeCheckResult<double>().hasScheduler()); |
|||
storm::storage::Scheduler<double> const& scheduler = result->asExplicitQuantitativeCheckResult<double>().getScheduler(); |
|||
EXPECT_EQ(0ull, scheduler.getChoice(0).getDeterministicChoice()); |
|||
EXPECT_EQ(1ull, scheduler.getChoice(1).getDeterministicChoice()); |
|||
EXPECT_EQ(0ull, scheduler.getChoice(2).getDeterministicChoice()); |
|||
EXPECT_EQ(0ull, scheduler.getChoice(3).getDeterministicChoice()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"target\"]"); |
|||
|
|||
checkTask = storm::modelchecker::CheckTask<storm::logic::Formula>(*formula); |
|||
checkTask.setProduceSchedulers(true); |
|||
result = checker.check(checkTask); |
|||
|
|||
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); |
|||
ASSERT_TRUE(result->asExplicitQuantitativeCheckResult<double>().hasScheduler()); |
|||
storm::storage::Scheduler<double> const& scheduler2 = result->asExplicitQuantitativeCheckResult<double>().getScheduler(); |
|||
EXPECT_EQ(1ull, scheduler2.getChoice(0).getDeterministicChoice()); |
|||
EXPECT_EQ(2ull, scheduler2.getChoice(1).getDeterministicChoice()); |
|||
EXPECT_EQ(0ull, scheduler2.getChoice(2).getDeterministicChoice()); |
|||
EXPECT_EQ(0ull, scheduler2.getChoice(3).getDeterministicChoice()); |
|||
} |
|||
|
|||
// Test is currently disabled as the computation of this property requires eliminating the zero-reward MECs, which is
|
|||
// currently not implemented and also not supported by PRISM.
|
|||
TEST(LpMdpPrctlModelCheckerTest, TinyRewards) { |
|||
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/tiny_rewards.nm"); |
|||
|
|||
// A parser that we use for conveniently constructing the formulas.
|
|||
storm::parser::FormulaParser formulaParser; |
|||
|
|||
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(true, true)).build(); |
|||
EXPECT_EQ(3ull, model->getNumberOfStates()); |
|||
EXPECT_EQ(4ull, model->getNumberOfTransitions()); |
|||
|
|||
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); |
|||
|
|||
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = model->as<storm::models::sparse::Mdp<double>>(); |
|||
|
|||
EXPECT_EQ(4ull, mdp->getNumberOfChoices()); |
|||
|
|||
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::make_unique<storm::solver::LpMinMaxLinearEquationSolverFactory<double>>()); |
|||
|
|||
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"target\"]"); |
|||
|
|||
storm::modelchecker::CheckTask<storm::logic::Formula> checkTask(*formula); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(checkTask); |
|||
|
|||
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); |
|||
EXPECT_NEAR(1, result->asExplicitQuantitativeCheckResult<double>().getValueVector()[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
EXPECT_NEAR(1, result->asExplicitQuantitativeCheckResult<double>().getValueVector()[1], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
EXPECT_NEAR(0, result->asExplicitQuantitativeCheckResult<double>().getValueVector()[2], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); |
|||
} |
@ -0,0 +1,278 @@ |
|||
#include "gtest/gtest.h"
|
|||
#include "storm-config.h"
|
|||
|
|||
#include "test/storm_gtest.h"
|
|||
|
|||
#include "storm/parser/FormulaParser.h"
|
|||
#include "storm/logic/Formulas.h"
|
|||
#include "storm/models/sparse/Mdp.h"
|
|||
#include "storm/models/symbolic/Mdp.h"
|
|||
#include "storm/models/sparse/StandardRewardModel.h"
|
|||
#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
|
|||
#include "storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h"
|
|||
#include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h"
|
|||
#include "storm/modelchecker/results/QuantitativeCheckResult.h"
|
|||
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
|
|||
#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
|
|||
#include "storm/modelchecker/results/QualitativeCheckResult.h"
|
|||
#include "storm/settings/SettingsManager.h"
|
|||
#include "storm/api/builder.h"
|
|||
#include "storm/api/model_descriptions.h"
|
|||
#include "storm/api/properties.h"
|
|||
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
|
|||
|
|||
#include "storm/settings/modules/GeneralSettings.h"
|
|||
#include "storm/settings/modules/CoreSettings.h"
|
|||
#include "storm/parser/AutoParser.h"
|
|||
|
|||
namespace { |
|||
class SparseDoubleValueIterationEnvironment { |
|||
public: |
|||
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
|
|||
static const bool isExact = false; |
|||
typedef double ValueType; |
|||
typedef storm::models::sparse::Mdp<ValueType> ModelType; |
|||
static storm::Environment createEnvironment() { |
|||
storm::Environment env; |
|||
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); |
|||
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8)); |
|||
return env; |
|||
} |
|||
// TODO: this should be part of the environment
|
|||
static storm::settings::modules::CoreSettings::Engine engine() { return storm::settings::modules::CoreSettings::Engine::Sparse; } |
|||
}; |
|||
class SparseDoubleSoundValueIterationEnvironment { |
|||
public: |
|||
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
|
|||
static const bool isExact = false; |
|||
typedef double ValueType; |
|||
typedef storm::models::sparse::Mdp<ValueType> ModelType; |
|||
static storm::Environment createEnvironment() { |
|||
storm::Environment env; |
|||
env.solver().setForceSoundness(true); |
|||
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); |
|||
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6)); |
|||
return env; |
|||
} |
|||
// TODO: this should be part of the environment
|
|||
static storm::settings::modules::CoreSettings::Engine engine() { return storm::settings::modules::CoreSettings::Engine::Sparse; } |
|||
}; |
|||
class SparseRationalPolicyIterationEnvironment { |
|||
public: |
|||
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
|
|||
static const bool isExact = true; |
|||
typedef storm::RationalNumber ValueType; |
|||
typedef storm::models::sparse::Mdp<ValueType> ModelType; |
|||
static storm::Environment createEnvironment() { |
|||
storm::Environment env; |
|||
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration); |
|||
return env; |
|||
} |
|||
// TODO: this should be part of the environment
|
|||
static storm::settings::modules::CoreSettings::Engine engine() { return storm::settings::modules::CoreSettings::Engine::Sparse; } |
|||
}; |
|||
class SparseRationalRationalSearchEnvironment { |
|||
public: |
|||
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
|
|||
static const bool isExact = true; |
|||
typedef storm::RationalNumber ValueType; |
|||
typedef storm::models::sparse::Mdp<ValueType> ModelType; |
|||
static storm::Environment createEnvironment() { |
|||
storm::Environment env; |
|||
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::RationalSearch); |
|||
return env; |
|||
} |
|||
// TODO: this should be part of the environment
|
|||
static storm::settings::modules::CoreSettings::Engine engine() { return storm::settings::modules::CoreSettings::Engine::Sparse; } |
|||
}; |
|||
|
|||
template<typename TestType> |
|||
class MdpPrctlModelCheckerTest : public ::testing::Test { |
|||
public: |
|||
typedef typename TestType::ValueType ValueType; |
|||
typedef typename storm::models::sparse::Mdp<ValueType> SparseModelType; |
|||
typedef typename storm::models::symbolic::Mdp<TestType::ddType, ValueType> SymbolicModelType; |
|||
|
|||
MdpPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {} |
|||
storm::Environment const& env() const { return _environment; } |
|||
ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber<ValueType>(input);} |
|||
ValueType precision() const { return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");} |
|||
bool isSparseModel() const { return std::is_same<typename TestType::ModelType, SparseModelType>::value; } |
|||
bool isSymbolicModel() const { return std::is_same<typename TestType::ModelType, SymbolicModelType>::value; } |
|||
|
|||
template <typename MT = typename TestType::ModelType> |
|||
typename std::enable_if<std::is_same<MT, SparseModelType>::value, std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>>>::type |
|||
buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { |
|||
std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> 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<ValueType>(program, result.second)->template as<MT>(); |
|||
return result; |
|||
} |
|||
|
|||
template <typename MT = typename TestType::ModelType> |
|||
typename std::enable_if<std::is_same<MT, SymbolicModelType>::value, std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>>>::type |
|||
buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { |
|||
std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> 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<TestType::ddType, ValueType>(program, result.second)->template as<MT>(); |
|||
return result; |
|||
} |
|||
|
|||
std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> getTasks(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) const { |
|||
std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> result; |
|||
for (auto const& f : formulas) { |
|||
result.emplace_back(*f); |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
template <typename MT = typename TestType::ModelType> |
|||
typename std::enable_if<std::is_same<MT, SparseModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type |
|||
createModelChecker(std::shared_ptr<MT> const& model) const { |
|||
return std::make_shared<storm::modelchecker::SparseMdpPrctlModelChecker<SparseModelType>>(*model); |
|||
} |
|||
|
|||
template <typename MT = typename TestType::ModelType> |
|||
typename std::enable_if<std::is_same<MT, SymbolicModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type |
|||
createModelChecker(std::shared_ptr<MT> const& model) const { |
|||
if (TestType::engine() == storm::settings::modules::CoreSettings::Engine::Hybrid) { |
|||
return std::make_shared<storm::modelchecker::HybridMdpPrctlModelChecker<SymbolicModelType>>(*model); |
|||
} else if (TestType::engine() == storm::settings::modules::CoreSettings::Engine::Dd) { |
|||
return std::make_shared<storm::modelchecker::SymbolicMdpPrctlModelChecker<SymbolicModelType>>(*model); |
|||
} |
|||
} |
|||
|
|||
bool getQualitativeResultAtInitialState(std::shared_ptr<storm::models::Model<ValueType>> const& model, std::unique_ptr<storm::modelchecker::CheckResult>& result) { |
|||
auto filter = getInitialStateFilter(model); |
|||
result->filter(*filter); |
|||
return result->asQualitativeCheckResult().forallTrue(); |
|||
} |
|||
|
|||
ValueType getQuantitativeResultAtInitialState(std::shared_ptr<storm::models::Model<ValueType>> const& model, std::unique_ptr<storm::modelchecker::CheckResult>& result) { |
|||
auto filter = getInitialStateFilter(model); |
|||
result->filter(*filter); |
|||
return result->asQuantitativeCheckResult<ValueType>().getMin(); |
|||
} |
|||
|
|||
private: |
|||
storm::Environment _environment; |
|||
|
|||
std::unique_ptr<storm::modelchecker::QualitativeCheckResult> getInitialStateFilter(std::shared_ptr<storm::models::Model<ValueType>> const& model) const { |
|||
if (isSparseModel()) { |
|||
return std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult>(model->template as<SparseModelType>()->getInitialStates()); |
|||
} else { |
|||
return std::make_unique<storm::modelchecker::SymbolicQualitativeCheckResult<TestType::ddType>>(model->template as<SymbolicModelType>()->getReachableStates(), model->template as<SymbolicModelType>()->getInitialStates()); |
|||
} |
|||
} |
|||
}; |
|||
|
|||
typedef ::testing::Types< |
|||
SparseDoubleValueIterationEnvironment, |
|||
SparseDoubleSoundValueIterationEnvironment, |
|||
SparseRationalPolicyIterationEnvironment, |
|||
SparseRationalRationalSearchEnvironment |
|||
> TestingTypes; |
|||
|
|||
TYPED_TEST_CASE(MdpPrctlModelCheckerTest, TestingTypes); |
|||
|
|||
|
|||
TYPED_TEST(MdpPrctlModelCheckerTest, Dice) { |
|||
std::string formulasString = "Pmin=? [F \"two\"]"; |
|||
formulasString += "; Pmax=? [F \"two\"]"; |
|||
formulasString += "; Pmin=? [F \"three\"]"; |
|||
formulasString += "; Pmax=? [F \"three\"]"; |
|||
formulasString += "; Pmin=? [F \"four\"]"; |
|||
formulasString += "; Pmax=? [F \"four\"]"; |
|||
formulasString += "; Rmin=? [F \"done\"]"; |
|||
formulasString += "; Rmax=? [F \"done\"]"; |
|||
|
|||
auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm", formulasString); |
|||
auto model = std::move(modelFormulas.first); |
|||
auto tasks = this->getTasks(modelFormulas.second); |
|||
EXPECT_EQ(169ul, model->getNumberOfStates()); |
|||
EXPECT_EQ(436ul, model->getNumberOfTransitions()); |
|||
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); |
|||
auto checker = this->createModelChecker(model); |
|||
std::unique_ptr<storm::modelchecker::CheckResult> result; |
|||
|
|||
result = checker->check(this->env(), tasks[0]); |
|||
EXPECT_NEAR(this->parseNumber("1/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); |
|||
|
|||
result = checker->check(this->env(), tasks[1]); |
|||
EXPECT_NEAR(this->parseNumber("1/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); |
|||
|
|||
result = checker->check(this->env(), tasks[2]); |
|||
EXPECT_NEAR(this->parseNumber("2/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); |
|||
|
|||
result = checker->check(this->env(), tasks[3]); |
|||
EXPECT_NEAR(this->parseNumber("2/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); |
|||
|
|||
result = checker->check(this->env(), tasks[4]); |
|||
EXPECT_NEAR(this->parseNumber("3/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); |
|||
|
|||
result = checker->check(this->env(), tasks[5]); |
|||
EXPECT_NEAR(this->parseNumber("3/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); |
|||
|
|||
result = checker->check(this->env(), tasks[6]); |
|||
EXPECT_NEAR(this->parseNumber("22/3"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); |
|||
|
|||
result = checker->check(this->env(), tasks[7]); |
|||
EXPECT_NEAR(this->parseNumber("22/3"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); |
|||
} |
|||
|
|||
TYPED_TEST(MdpPrctlModelCheckerTest, AsynchronousLeader) { |
|||
std::string formulasString = "Pmin=? [F \"elected\"]"; |
|||
formulasString += "; Pmax=? [F \"elected\"]"; |
|||
formulasString += "; Pmin=? [F<=25 \"elected\"]"; |
|||
formulasString += "; Pmax=? [F<=25 \"elected\"]"; |
|||
formulasString += "; Rmin=? [F \"elected\"]"; |
|||
formulasString += "; Rmax=? [F \"elected\"]"; |
|||
|
|||
auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/leader4.nm", formulasString); |
|||
auto model = std::move(modelFormulas.first); |
|||
auto tasks = this->getTasks(modelFormulas.second); |
|||
EXPECT_EQ(3172ul, model->getNumberOfStates()); |
|||
EXPECT_EQ(7144ul, model->getNumberOfTransitions()); |
|||
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); |
|||
auto checker = this->createModelChecker(model); |
|||
std::unique_ptr<storm::modelchecker::CheckResult> result; |
|||
|
|||
|
|||
result = checker->check(this->env(), tasks[0]); |
|||
EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); |
|||
|
|||
result = checker->check(this->env(), tasks[1]); |
|||
EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); |
|||
|
|||
result = checker->check(this->env(), tasks[2]); |
|||
EXPECT_NEAR(this->parseNumber("1/16"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); |
|||
|
|||
result = checker->check(this->env(), tasks[3]); |
|||
EXPECT_NEAR(this->parseNumber("1/16"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); |
|||
|
|||
result = checker->check(this->env(), tasks[4]); |
|||
EXPECT_NEAR(this->parseNumber("30/7"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); |
|||
|
|||
result = checker->check(this->env(), tasks[5]); |
|||
EXPECT_NEAR(this->parseNumber("30/7"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); |
|||
} |
|||
|
|||
TYPED_TEST(MdpPrctlModelCheckerTest, TinyRewards) { |
|||
std::string formulasString = "Rmin=? [F \"target\"]"; |
|||
auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/tiny_rewards.nm", formulasString); |
|||
auto model = std::move(modelFormulas.first); |
|||
auto tasks = this->getTasks(modelFormulas.second); |
|||
EXPECT_EQ(3ul, model->getNumberOfStates()); |
|||
EXPECT_EQ(4ul, model->getNumberOfTransitions()); |
|||
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); |
|||
auto checker = this->createModelChecker(model); |
|||
std::unique_ptr<storm::modelchecker::CheckResult> result; |
|||
|
|||
result = checker->check(this->env(), tasks[0]); |
|||
EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); |
|||
} |
|||
} |
@ -1,374 +0,0 @@ |
|||
#include "gtest/gtest.h"
|
|||
#include "storm-config.h"
|
|||
|
|||
#include "storm/logic/Formulas.h"
|
|||
#include "storm/solver/StandardMinMaxLinearEquationSolver.h"
|
|||
#include "storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h"
|
|||
#include "storm/modelchecker/results/HybridQuantitativeCheckResult.h"
|
|||
#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
|
|||
#include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h"
|
|||
#include "storm/storage/SymbolicModelDescription.h"
|
|||
#include "storm/parser/FormulaParser.h"
|
|||
#include "storm/parser/PrismParser.h"
|
|||
#include "storm/builder/DdPrismModelBuilder.h"
|
|||
#include "storm/models/symbolic/Mdp.h"
|
|||
#include "storm/models/symbolic/StandardRewardModel.h"
|
|||
#include "storm/settings/SettingsManager.h"
|
|||
|
|||
#include "storm/settings/modules/GeneralSettings.h"
|
|||
|
|||
#include "storm/settings/modules/NativeEquationSolverSettings.h"
|
|||
|
|||
TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Cudd) { |
|||
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); |
|||
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<storm::dd::DdType::CUDD>::Options options; |
|||
#else
|
|||
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options; |
|||
#endif
|
|||
options.buildAllRewardModels = false; |
|||
options.rewardModelsToBuild.insert("coinflips"); |
|||
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program, options); |
|||
EXPECT_EQ(169ul, model->getNumberOfStates()); |
|||
EXPECT_EQ(436ul, model->getNumberOfTransitions()); |
|||
|
|||
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); |
|||
|
|||
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>(); |
|||
|
|||
storm::modelchecker::HybridMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>> checker(*mdp, std::make_unique<storm::solver::NativeMinMaxLinearEquationSolverFactory<double>>()); |
|||
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult1 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult2 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult3 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult4 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult6 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult7 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(7.333333333, quantitativeResult7.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(7.333333333, quantitativeResult7.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult8 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(7.3333316743373871, quantitativeResult8.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(7.3333316743373871, quantitativeResult8.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
} |
|||
|
|||
TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Sylvan) { |
|||
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); |
|||
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<storm::dd::DdType::Sylvan>::Options options; |
|||
#else
|
|||
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::Options options; |
|||
#endif
|
|||
options.buildAllRewardModels = false; |
|||
options.rewardModelsToBuild.insert("coinflips"); |
|||
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program, options); |
|||
EXPECT_EQ(169ul, model->getNumberOfStates()); |
|||
EXPECT_EQ(436ul, model->getNumberOfTransitions()); |
|||
|
|||
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); |
|||
|
|||
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>(); |
|||
|
|||
storm::modelchecker::HybridMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>> checker(*mdp, std::make_unique<storm::solver::NativeMinMaxLinearEquationSolverFactory<double>>()); |
|||
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult1 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult2 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult3 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult4 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult6 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult7 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(7.333333333, quantitativeResult7.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(7.333333333, quantitativeResult7.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult8 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(7.3333316743373871, quantitativeResult8.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(7.3333316743373871, quantitativeResult8.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
} |
|||
|
|||
TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { |
|||
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader4.nm"); |
|||
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<storm::dd::DdType::CUDD>::Options options; |
|||
#else
|
|||
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options; |
|||
#endif
|
|||
options.buildAllRewardModels = false; |
|||
options.rewardModelsToBuild.insert("rounds"); |
|||
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program, options); |
|||
EXPECT_EQ(3172ul, model->getNumberOfStates()); |
|||
EXPECT_EQ(7144ul, model->getNumberOfTransitions()); |
|||
|
|||
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); |
|||
|
|||
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>(); |
|||
|
|||
storm::modelchecker::HybridMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>> checker(*mdp, std::make_unique<storm::solver::NativeMinMaxLinearEquationSolverFactory<double>>()); |
|||
|
|||
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(1, quantitativeResult2.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult3 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(0.0625, quantitativeResult3.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0625, quantitativeResult3.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult4 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0625, quantitativeResult4.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(4.285716, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(4.285716, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult6 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(4.2857120959008661, quantitativeResult6.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(4.2857120959008661, quantitativeResult6.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
} |
|||
|
|||
TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { |
|||
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader4.nm"); |
|||
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<storm::dd::DdType::Sylvan>::Options options; |
|||
#else
|
|||
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::Options options; |
|||
#endif
|
|||
options.buildAllRewardModels = false; |
|||
options.rewardModelsToBuild.insert("rounds"); |
|||
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program, options); |
|||
EXPECT_EQ(3172ul, model->getNumberOfStates()); |
|||
EXPECT_EQ(7144ul, model->getNumberOfTransitions()); |
|||
|
|||
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); |
|||
|
|||
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>(); |
|||
|
|||
storm::modelchecker::HybridMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>> checker(*mdp, std::make_unique<storm::solver::NativeMinMaxLinearEquationSolverFactory<double>>()); |
|||
|
|||
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(1, quantitativeResult2.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult3 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(0.0625, quantitativeResult3.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0625, quantitativeResult3.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult4 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0625, quantitativeResult4.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(4.285716, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(4.285716, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult6 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(4.2857120959008661, quantitativeResult6.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(4.2857120959008661, quantitativeResult6.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
} |
@ -0,0 +1,142 @@ |
|||
#include "gtest/gtest.h"
|
|||
#include "storm-config.h"
|
|||
|
|||
#include "storm/parser/FormulaParser.h"
|
|||
#include "storm/logic/Formulas.h"
|
|||
#include "storm/solver/StandardMinMaxLinearEquationSolver.h"
|
|||
#include "storm/models/sparse/StandardRewardModel.h"
|
|||
#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
|
|||
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
|
|||
#include "storm/settings/SettingsManager.h"
|
|||
#include "storm/settings/modules/GeneralSettings.h"
|
|||
|
|||
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
|
|||
|
|||
#include "storm/parser/AutoParser.h"
|
|||
#include "storm/parser/PrismParser.h"
|
|||
#include "storm/builder/ExplicitModelBuilder.h"
|
|||
|
|||
namespace { |
|||
class DoubleViEnvironment { |
|||
public: |
|||
typedef double ValueType; |
|||
static storm::Environment createEnvironment() { |
|||
storm::Environment env; |
|||
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); |
|||
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8)); |
|||
return env; |
|||
} |
|||
}; |
|||
class DoubleSoundViEnvironment { |
|||
public: |
|||
typedef double ValueType; |
|||
static storm::Environment createEnvironment() { |
|||
storm::Environment env; |
|||
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); |
|||
env.solver().setForceSoundness(true); |
|||
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6)); |
|||
return env; |
|||
} |
|||
}; |
|||
class DoublePIEnvironment { |
|||
public: |
|||
typedef double ValueType; |
|||
static storm::Environment createEnvironment() { |
|||
storm::Environment env; |
|||
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration); |
|||
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8)); |
|||
return env; |
|||
} |
|||
}; |
|||
class RationalPIEnvironment { |
|||
public: |
|||
typedef storm::RationalNumber ValueType; |
|||
static storm::Environment createEnvironment() { |
|||
storm::Environment env; |
|||
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration); |
|||
return env; |
|||
} |
|||
}; |
|||
// class RationalRationalSearchEnvironment {
|
|||
// public:
|
|||
// typedef storm::RationalNumber ValueType;
|
|||
// static storm::Environment createEnvironment() {
|
|||
// storm::Environment env;
|
|||
// env.solver().minMax().setMethod(storm::solver::MinMaxMethod::RationalSearch);
|
|||
// return env;
|
|||
// }
|
|||
// };
|
|||
|
|||
template<typename TestType> |
|||
class SchedulerGenerationMdpPrctlModelCheckerTest : public ::testing::Test { |
|||
public: |
|||
typedef typename TestType::ValueType ValueType; |
|||
SchedulerGenerationMdpPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {} |
|||
storm::Environment const& env() const { return _environment; } |
|||
private: |
|||
storm::Environment _environment; |
|||
}; |
|||
|
|||
typedef ::testing::Types< |
|||
DoubleViEnvironment, |
|||
DoubleSoundViEnvironment, |
|||
DoublePIEnvironment, |
|||
RationalPIEnvironment |
|||
//RationalRationalSearchEnvironment
|
|||
> TestingTypes; |
|||
|
|||
TYPED_TEST_CASE(SchedulerGenerationMdpPrctlModelCheckerTest, TestingTypes); |
|||
|
|||
|
|||
TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, reachability) { |
|||
typedef typename TestFixture::ValueType ValueType; |
|||
|
|||
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/scheduler_generation.nm"); |
|||
|
|||
// A parser that we use for conveniently constructing the formulas.
|
|||
storm::parser::FormulaParser formulaParser; |
|||
|
|||
storm::generator::NextStateGeneratorOptions options; |
|||
options.setBuildAllLabels(); |
|||
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = storm::builder::ExplicitModelBuilder<ValueType>(program, options).build(); |
|||
EXPECT_EQ(4ull, model->getNumberOfStates()); |
|||
EXPECT_EQ(11ull, model->getNumberOfTransitions()); |
|||
|
|||
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); |
|||
|
|||
std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp = model->template as<storm::models::sparse::Mdp<ValueType>>(); |
|||
|
|||
EXPECT_EQ(7ull, mdp->getNumberOfChoices()); |
|||
|
|||
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp); |
|||
|
|||
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"target\"]"); |
|||
|
|||
storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> checkTask(*formula); |
|||
checkTask.setProduceSchedulers(true); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), checkTask); |
|||
|
|||
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); |
|||
ASSERT_TRUE(result->asExplicitQuantitativeCheckResult<ValueType>().hasScheduler()); |
|||
storm::storage::Scheduler<ValueType> const& scheduler = result->asExplicitQuantitativeCheckResult<ValueType>().getScheduler(); |
|||
EXPECT_EQ(0ull, scheduler.getChoice(0).getDeterministicChoice()); |
|||
EXPECT_EQ(1ull, scheduler.getChoice(1).getDeterministicChoice()); |
|||
EXPECT_EQ(0ull, scheduler.getChoice(2).getDeterministicChoice()); |
|||
EXPECT_EQ(0ull, scheduler.getChoice(3).getDeterministicChoice()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"target\"]"); |
|||
|
|||
checkTask = storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>(*formula); |
|||
checkTask.setProduceSchedulers(true); |
|||
result = checker.check(checkTask); |
|||
|
|||
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); |
|||
ASSERT_TRUE(result->asExplicitQuantitativeCheckResult<ValueType>().hasScheduler()); |
|||
storm::storage::Scheduler<ValueType> const& scheduler2 = result->asExplicitQuantitativeCheckResult<ValueType>().getScheduler(); |
|||
EXPECT_EQ(1ull, scheduler2.getChoice(0).getDeterministicChoice()); |
|||
EXPECT_EQ(2ull, scheduler2.getChoice(1).getDeterministicChoice()); |
|||
EXPECT_EQ(0ull, scheduler2.getChoice(2).getDeterministicChoice()); |
|||
EXPECT_EQ(0ull, scheduler2.getChoice(3).getDeterministicChoice()); |
|||
} |
|||
} |
@ -1,377 +0,0 @@ |
|||
#include "gtest/gtest.h"
|
|||
#include "storm-config.h"
|
|||
|
|||
#include "storm/logic/Formulas.h"
|
|||
#include "storm/utility/solver.h"
|
|||
#include "storm/storage/SymbolicModelDescription.h"
|
|||
#include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h"
|
|||
#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
|
|||
#include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h"
|
|||
#include "storm/parser/FormulaParser.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/settings/SettingsManager.h"
|
|||
|
|||
#include "storm/settings/modules/NativeEquationSolverSettings.h"
|
|||
|
|||
#include "storm/settings/modules/GeneralSettings.h"
|
|||
|
|||
TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Cudd) { |
|||
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); |
|||
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<storm::dd::DdType::CUDD>::Options options; |
|||
#else
|
|||
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options; |
|||
#endif
|
|||
options.buildAllRewardModels = false; |
|||
options.rewardModelsToBuild.insert("coinflips"); |
|||
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program, options); |
|||
EXPECT_EQ(169ul, model->getNumberOfStates()); |
|||
EXPECT_EQ(436ul, model->getNumberOfTransitions()); |
|||
|
|||
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); |
|||
|
|||
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>(); |
|||
|
|||
storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>> checker(*mdp, std::unique_ptr<storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>())); |
|||
|
|||
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult6 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult7 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(7.3333317041397095, quantitativeResult7.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(7.3333317041397095, quantitativeResult7.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult8 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(7.3333294987678528, quantitativeResult8.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(7.3333294987678528, quantitativeResult8.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
} |
|||
|
|||
TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Sylvan) { |
|||
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); |
|||
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<storm::dd::DdType::Sylvan>::Options options; |
|||
#else
|
|||
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::Options options; |
|||
#endif
|
|||
options.buildAllRewardModels = false; |
|||
options.rewardModelsToBuild.insert("coinflips"); |
|||
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program, options); |
|||
EXPECT_EQ(169ul, model->getNumberOfStates()); |
|||
EXPECT_EQ(436ul, model->getNumberOfTransitions()); |
|||
|
|||
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); |
|||
|
|||
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>(); |
|||
|
|||
storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>> checker(*mdp, std::unique_ptr<storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>())); |
|||
|
|||
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult6 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult7 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(7.3333317041397095, quantitativeResult7.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(7.3333317041397095, quantitativeResult7.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult8 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(7.3333294987678528, quantitativeResult8.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(7.3333294987678528, quantitativeResult8.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
} |
|||
|
|||
TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { |
|||
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader4.nm"); |
|||
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<storm::dd::DdType::CUDD>::Options options; |
|||
#else
|
|||
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options; |
|||
#endif
|
|||
options.buildAllRewardModels = false; |
|||
options.rewardModelsToBuild.insert("rounds"); |
|||
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program, options); |
|||
EXPECT_EQ(3172ul, model->getNumberOfStates()); |
|||
EXPECT_EQ(7144ul, model->getNumberOfTransitions()); |
|||
|
|||
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); |
|||
|
|||
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>(); |
|||
|
|||
storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>> checker(*mdp, std::unique_ptr<storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>())); |
|||
|
|||
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(1, quantitativeResult2.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(0.0625, quantitativeResult3.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0625, quantitativeResult3.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0625, quantitativeResult4.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(4.2856904569131631, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(4.2856904569131631, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult6 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); |
|||
|
|||
EXPECT_NEAR(4.2856904354441401, quantitativeResult6.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(4.2856904354441401, quantitativeResult6.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
} |
|||
|
|||
TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { |
|||
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader4.nm"); |
|||
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<storm::dd::DdType::Sylvan>::Options options; |
|||
#else
|
|||
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::Options options; |
|||
#endif
|
|||
options.buildAllRewardModels = false; |
|||
options.rewardModelsToBuild.insert("rounds"); |
|||
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program, options); |
|||
EXPECT_EQ(3172ul, model->getNumberOfStates()); |
|||
EXPECT_EQ(7144ul, model->getNumberOfTransitions()); |
|||
|
|||
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); |
|||
|
|||
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>(); |
|||
|
|||
storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>> checker(*mdp, std::unique_ptr<storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>())); |
|||
|
|||
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(1, quantitativeResult2.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(0.0625, quantitativeResult3.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0625, quantitativeResult3.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(0.0625, quantitativeResult4.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
// FIXME: this precision bound is not really good.
|
|||
EXPECT_NEAR(4.2857, quantitativeResult5.getMin(), 100 * storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(4.2857, quantitativeResult5.getMax(), 100 * storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult6 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); |
|||
|
|||
// FIXME: this precision bound is not really good.
|
|||
EXPECT_NEAR(4.2857, quantitativeResult6.getMin(), 100 * storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
EXPECT_NEAR(4.2857, quantitativeResult6.getMax(), 100 * storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); |
|||
} |
@ -1,192 +0,0 @@ |
|||
#include "gtest/gtest.h"
|
|||
#include "storm-config.h"
|
|||
|
|||
#include "storm/parser/FormulaParser.h"
|
|||
#include "storm/logic/Formulas.h"
|
|||
#include "storm/solver/TopologicalMinMaxLinearEquationSolver.h"
|
|||
#include "storm/models/sparse/StandardRewardModel.h"
|
|||
#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
|
|||
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
|
|||
#include "storm/settings/SettingsManager.h"
|
|||
|
|||
#include "storm/settings/modules/GeneralSettings.h"
|
|||
#include "storm/settings/modules/TopologicalValueIterationEquationSolverSettings.h"
|
|||
#include "storm/settings/SettingMemento.h"
|
|||
#include "storm/parser/AutoParser.h"
|
|||
|
|||
#include "storm-config.h"
|
|||
|
|||
TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { |
|||
//storm::settings::Settings* s = storm::settings::Settings::getInstance();
|
|||
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = 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")->as<storm::models::sparse::Mdp<double>>(); |
|||
|
|||
// A parser that we use for conveniently constructing the formulas.
|
|||
storm::parser::FormulaParser formulaParser; |
|||
|
|||
ASSERT_EQ(mdp->getNumberOfStates(), 169ull); |
|||
ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); |
|||
|
|||
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> mc(*mdp, std::make_unique<storm::solver::TopologicalMinMaxLinearEquationSolverFactory<double>>()); |
|||
|
|||
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result = mc.check(*formula); |
|||
|
|||
ASSERT_NEAR(0.0277777612209320068, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); |
|||
|
|||
result = mc.check(*formula); |
|||
|
|||
ASSERT_NEAR(0.0277777612209320068, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); |
|||
|
|||
result = mc.check(*formula); |
|||
|
|||
ASSERT_NEAR(0.0555555224418640136, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); |
|||
|
|||
result = mc.check(*formula); |
|||
|
|||
ASSERT_NEAR(0.0555555224418640136, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); |
|||
|
|||
result = mc.check(*formula); |
|||
|
|||
ASSERT_NEAR(0.083333283662796020508, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); |
|||
|
|||
result = mc.check(*formula); |
|||
|
|||
ASSERT_NEAR(0.083333283662796020508, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); |
|||
|
|||
result = mc.check(*formula); |
|||
|
|||
#ifdef STORM_HAVE_CUDA
|
|||
ASSERT_NEAR(7.333329499, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision()); |
|||
#else
|
|||
ASSERT_NEAR(7.33332904, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision()); |
|||
#endif
|
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); |
|||
|
|||
result = mc.check(*formula); |
|||
|
|||
#ifdef STORM_HAVE_CUDA
|
|||
ASSERT_NEAR(7.333329499, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision()); |
|||
#else
|
|||
ASSERT_NEAR(7.33333151, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision()); |
|||
#endif
|
|||
|
|||
// ------------- state rewards --------------
|
|||
std::shared_ptr<storm::models::sparse::Mdp<double>> stateRewardMdp = 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", "")->as<storm::models::sparse::Mdp<double>>(); |
|||
|
|||
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateRewardModelChecker(*stateRewardMdp, std::make_unique<storm::solver::TopologicalMinMaxLinearEquationSolverFactory<double>>()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); |
|||
|
|||
result = stateRewardModelChecker.check(*formula); |
|||
|
|||
#ifdef STORM_HAVE_CUDA
|
|||
ASSERT_NEAR(7.333329499, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision()); |
|||
#else
|
|||
ASSERT_NEAR(7.33332904, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision()); |
|||
#endif
|
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); |
|||
|
|||
result = stateRewardModelChecker.check(*formula); |
|||
|
|||
#ifdef STORM_HAVE_CUDA
|
|||
ASSERT_NEAR(7.333329499, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision()); |
|||
#else
|
|||
ASSERT_NEAR(7.33333151, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision()); |
|||
#endif
|
|||
|
|||
// -------------------------------- state and transition reward ------------------------
|
|||
std::shared_ptr<storm::models::sparse::Mdp<double>> stateAndTransitionRewardMdp = 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")->as<storm::models::sparse::Mdp<double>>(); |
|||
|
|||
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::make_unique<storm::solver::TopologicalMinMaxLinearEquationSolverFactory<double>>()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); |
|||
|
|||
result = stateAndTransitionRewardModelChecker.check(*formula); |
|||
|
|||
#ifdef STORM_HAVE_CUDA
|
|||
ASSERT_NEAR(14.666658998, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision()); |
|||
#else
|
|||
ASSERT_NEAR(14.6666581, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision()); |
|||
#endif
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); |
|||
|
|||
result = stateAndTransitionRewardModelChecker.check(*formula); |
|||
|
|||
#ifdef STORM_HAVE_CUDA
|
|||
ASSERT_NEAR(14.666658998, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision()); |
|||
#else
|
|||
ASSERT_NEAR(14.666663, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision()); |
|||
#endif
|
|||
} |
|||
|
|||
TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) { |
|||
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = 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")->as<storm::models::sparse::Mdp<double>>(); |
|||
|
|||
// A parser that we use for conveniently constructing the formulas.
|
|||
storm::parser::FormulaParser formulaParser; |
|||
|
|||
ASSERT_EQ(mdp->getNumberOfStates(), 3172ull); |
|||
ASSERT_EQ(mdp->getNumberOfTransitions(), 7144ull); |
|||
|
|||
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> mc(*mdp, std::make_unique<storm::solver::TopologicalMinMaxLinearEquationSolverFactory<double>>()); |
|||
|
|||
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result = mc.check(*formula); |
|||
|
|||
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 1), |
|||
storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); |
|||
|
|||
result = mc.check(*formula); |
|||
|
|||
ASSERT_NEAR(1, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); |
|||
|
|||
result = mc.check(*formula); |
|||
|
|||
ASSERT_NEAR(0.0625, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); |
|||
|
|||
result = mc.check(*formula); |
|||
|
|||
ASSERT_NEAR(0.0625, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision()); |
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); |
|||
|
|||
result = mc.check(*formula); |
|||
|
|||
#ifdef STORM_HAVE_CUDA
|
|||
ASSERT_NEAR(4.285689611, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision()); |
|||
#else
|
|||
ASSERT_NEAR(4.285701547, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision()); |
|||
#endif
|
|||
|
|||
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); |
|||
|
|||
result = mc.check(*formula); |
|||
|
|||
#ifdef STORM_HAVE_CUDA
|
|||
ASSERT_NEAR(4.285689611, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision()); |
|||
#else
|
|||
ASSERT_NEAR(4.285703591, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision()); |
|||
#endif
|
|||
} |
@ -1,30 +0,0 @@ |
|||
#pragma once |
|||
|
|||
#include <type_traits> |
|||
#include <typeinfo> |
|||
|
|||
#include "storm/utility/constants.h" |
|||
#include "gtest/gtest.h" |
|||
|
|||
#define STORM_EXPECT_NEAR(val1, val2, abs_error) \ |
|||
do { \ |
|||
if (std::is_same<typename std::remove_const<typename std::remove_reference<decltype(val1)>::type>::type, double>::value) { \ |
|||
EXPECT_NEAR(storm::utility::convertNumber<double>(val1), \ |
|||
storm::utility::convertNumber<double>(val2), \ |
|||
storm::utility::convertNumber<double>(abs_error)); \ |
|||
} else if (storm::utility::isZero(abs_error)) { \ |
|||
EXPECT_EQ(val1, val2); \ |
|||
} else { \ |
|||
auto valueDifference = val1; \ |
|||
valueDifference -= val2; \ |
|||
valueDifference = storm::utility::abs(valueDifference); \ |
|||
EXPECT_LT(storm::utility::abs(valueDifference), abs_error); \ |
|||
if (valueDifference > abs_error) { \ |
|||
std::cout << "Expected " << val2 \ |
|||
<< " (approx " << storm::utility::convertNumber<double>(val2) \ |
|||
<< ") but got " << val1 \ |
|||
<< " (approx " << storm::utility::convertNumber<double>(val1) \ |
|||
<< ")." << std::endl; \ |
|||
} \ |
|||
} \ |
|||
} while (false) |
@ -0,0 +1,28 @@ |
|||
#pragma once |
|||
|
|||
#include "gtest/gtest.h" |
|||
|
|||
#include "storm/adapters/RationalNumberAdapter.h" |
|||
#include "storm/utility/constants.h" |
|||
|
|||
|
|||
namespace testing { |
|||
namespace internal { |
|||
|
|||
GTEST_API_ AssertionResult DoubleNearPredFormat(const char* expr1, |
|||
const char* expr2, |
|||
const char* abs_error_expr, |
|||
storm::RationalNumber val1, |
|||
storm::RationalNumber val2, |
|||
storm::RationalNumber abs_error) { |
|||
const storm::RationalNumber diff = storm::utility::abs<storm::RationalNumber>(val1 - val2); |
|||
if (diff <= abs_error) return AssertionSuccess(); |
|||
return AssertionFailure() |
|||
<< "The difference between " << expr1 << " and " << expr2 |
|||
<< " is " << diff << " (approx. " << storm::utility::convertNumber<double>(diff) << "), which exceeds " << abs_error_expr << ", where\n" |
|||
<< expr1 << " evaluates to " << val1 << " (approx. " << storm::utility::convertNumber<double>(val1) << "),\n" |
|||
<< expr2 << " evaluates to " << val2 << " (approx. " << storm::utility::convertNumber<double>(val2) << "),\n" |
|||
<< abs_error_expr << " evaluates to " << abs_error << " (approx. " << storm::utility::convertNumber<double>(abs_error) << ")."; |
|||
} |
|||
} |
|||
} |
Write
Preview
Loading…
Cancel
Save
Reference in new issue