diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index 669cc3512..65a10a438 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -499,6 +499,7 @@ namespace storm { } // Check that the resulting distribution is in fact a distribution. + std::cout << probabilitySum << " vs " << comparator.isOne(probabilitySum) << " // " << (probabilitySum - 1) << std::endl; STORM_LOG_THROW(!discreteTimeModel || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not some to one for some command (actually sum to " << probabilitySum << ")."); // Dispose of the temporary maps. @@ -534,6 +535,7 @@ namespace storm { } // A comparator that can be used to check whether we actually have distributions. + std::cout << "creating comparator.. " << std::endl; storm::utility::ConstantsComparator comparator; // Initialize a queue and insert the initial state. diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp index c398f27cb..879192014 100644 --- a/src/settings/modules/GeneralSettings.cpp +++ b/src/settings/modules/GeneralSettings.cpp @@ -132,8 +132,7 @@ namespace storm { } double GeneralSettings::getPrecision() const { - double value = this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble(); - return value; + return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble(); } bool GeneralSettings::isExportDotSet() const { diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp index 5b5a68348..eedebbd0f 100644 --- a/src/utility/constants.cpp +++ b/src/utility/constants.cpp @@ -184,6 +184,7 @@ namespace storm { } bool ConstantsComparator::isOne(double const& value) const { + std::cout << std::setprecision(10) << std::abs(value - one()) << " prec: " << precision << std::endl; return std::abs(value - one()) <= precision; } diff --git a/src/utility/constants.h b/src/utility/constants.h index 2e5206711..1b64aaef1 100644 --- a/src/utility/constants.h +++ b/src/utility/constants.h @@ -34,7 +34,6 @@ namespace storm { template ValueType pow(ValueType const& value, uint_fast64_t exponent); - template ValueType simplify(ValueType value); @@ -54,8 +53,6 @@ namespace storm { bool isInfinity(ValueType const& value) const; }; - - template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); diff --git a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp index db391045f..b0c7ba3a6 100644 --- a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp @@ -29,8 +29,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Cluster) { #else typename storm::builder::ExplicitPrismModelBuilder::Options options; #endif - options.buildRewards = true; - options.rewardModelName = "num_repairs"; + options.rewardModelsToBuild.insert("num_repairs"); std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); @@ -113,8 +112,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Embedded) { typename storm::builder::ExplicitPrismModelBuilder::Options options; #endif - options.buildRewards = true; - options.rewardModelName = "up"; + options.rewardModelsToBuild.insert("up"); std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); @@ -223,8 +221,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Tandem) { #else typename storm::builder::ExplicitPrismModelBuilder::Options options; #endif - options.buildRewards = true; - options.rewardModelName = "customers"; + options.rewardModelsToBuild.insert("customers"); std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); diff --git a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp index f5580a179..db691e57a 100644 --- a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp @@ -32,8 +32,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) { #else typename storm::builder::DdPrismModelBuilder::Options options; #endif - options.buildRewards = true; - options.rewardModelName = "num_repairs"; + options.rewardModelsToBuild.insert("num_repairs"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); @@ -129,8 +128,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded) { #else typename storm::builder::DdPrismModelBuilder::Options options; #endif - options.buildRewards = true; - options.rewardModelName = "up"; + options.rewardModelsToBuild.insert("up"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); @@ -252,8 +250,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem) { #else typename storm::builder::DdPrismModelBuilder::Options options; #endif - options.buildRewards = true; - options.rewardModelName = "customers"; + options.rewardModelsToBuild.insert("customers"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); diff --git a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp index 4919a2e69..74dec49a7 100644 --- a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp @@ -23,8 +23,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die) { #else typename storm::builder::DdPrismModelBuilder::Options options; #endif - options.buildRewards = true; - options.rewardModelName = "coin_flips"; + options.rewardModelsToBuild.insert("coin_flips"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(20ul, model->getNumberOfTransitions()); @@ -129,8 +128,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader) { #else typename storm::builder::DdPrismModelBuilder::Options options; #endif - options.buildRewards = true; - options.rewardModelName = "num_rounds"; + options.rewardModelsToBuild.insert("num_rounds"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); EXPECT_EQ(273ul, model->getNumberOfStates()); EXPECT_EQ(397ul, model->getNumberOfTransitions()); diff --git a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp index 935cf9fb3..0aee24604 100644 --- a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp @@ -8,6 +8,7 @@ #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" #include "src/parser/PrismParser.h" +#include "src/parser/FormulaParser.h" #include "src/builder/DdPrismModelBuilder.h" #include "src/models/symbolic/Dtmc.h" #include "src/settings/SettingsManager.h" @@ -19,14 +20,16 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + // Build the die model with its reward model. #ifdef WINDOWS storm::builder::DdPrismModelBuilder::Options options; #else typename storm::builder::DdPrismModelBuilder::Options options; #endif - options.buildRewards = true; - options.rewardModelName = "coinflips"; + options.rewardModelsToBuild.insert("coinflips"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); EXPECT_EQ(169ul, model->getNumberOfStates()); EXPECT_EQ(436ul, model->getNumberOfTransitions()); @@ -37,80 +40,72 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) { storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); - auto labelFormula = std::make_shared("two"); - auto eventuallyFormula = std::make_shared(labelFormula); - auto minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + std::shared_ptr formula = parser.parseFromString("Pmin=? [F \"two\"]"); - std::unique_ptr result = checker.check(*minProbabilityOperatorFormula); + std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - auto maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + formula = parser.parseFromString("Pmax=? [F \"two\"]"); - result = checker.check(*maxProbabilityOperatorFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("three"); - eventuallyFormula = std::make_shared(labelFormula); - minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + formula = parser.parseFromString("Pmin=? [F \"three\"]"); - result = checker.check(*minProbabilityOperatorFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + formula = parser.parseFromString("Pmax=? [F \"three\"]"); - result = checker.check(*maxProbabilityOperatorFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("four"); - eventuallyFormula = std::make_shared(labelFormula); - minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + formula = parser.parseFromString("Pmin=? [F \"four\"]"); - result = checker.check(*minProbabilityOperatorFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + formula = parser.parseFromString("Pmax=? [F \"four\"]"); - result = checker.check(*maxProbabilityOperatorFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult6 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("done"); - auto reachabilityRewardFormula = std::make_shared(labelFormula); - auto minRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmin=? [F \"done\"]"); - result = checker.check(*minRewardOperatorFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult7 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(7.3333283960819244, quantitativeResult7.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(7.3333283960819244, quantitativeResult7.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - auto maxRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmax=? [F \"done\"]"); - result = checker.check(*maxRewardOperatorFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult8 = result->asHybridQuantitativeCheckResult(); @@ -121,14 +116,16 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) { TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + // Build the die model with its reward model. #ifdef WINDOWS storm::builder::DdPrismModelBuilder::Options options; #else typename storm::builder::DdPrismModelBuilder::Options options; #endif - options.buildRewards = true; - options.rewardModelName = "rounds"; + options.rewardModelsToBuild.insert("rounds"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); EXPECT_EQ(3172ul, model->getNumberOfStates()); EXPECT_EQ(7144ul, model->getNumberOfTransitions()); @@ -139,61 +136,54 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); - auto labelFormula = std::make_shared("elected"); - auto eventuallyFormula = std::make_shared(labelFormula); - auto minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + std::shared_ptr formula = parser.parseFromString("Pmin=? [F \"elected\"]"); - std::unique_ptr result = checker.check(*minProbabilityOperatorFormula); + std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - auto maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + formula = parser.parseFromString("Pmax=? [F \"elected\"]"); - result = checker.check(*maxProbabilityOperatorFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("elected"); - auto trueFormula = std::make_shared(true); - auto boundedUntilFormula = std::make_shared(trueFormula, labelFormula, 25); - minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, boundedUntilFormula); + formula = parser.parseFromString("Pmin=? [F<=25 \"elected\"]"); - result = checker.check(*minProbabilityOperatorFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.0625, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0625, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, boundedUntilFormula); + formula = parser.parseFromString("Pmax=? [F<=25 \"elected\"]"); - result = checker.check(*maxProbabilityOperatorFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0625, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("elected"); - auto reachabilityRewardFormula = std::make_shared(labelFormula); - auto minRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmin=? [F \"elected\"]"); - result = checker.check(*minRewardOperatorFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(4.2856925589077264, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(4.2856925589077264, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - auto maxRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmax=? [F \"elected\"]"); - result = checker.check(*maxRewardOperatorFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult6 = result->asHybridQuantitativeCheckResult(); diff --git a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index 9983c65e7..5dc655e56 100644 --- a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -1,6 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" +#include "src/parser/FormulaParser.h" #include "src/logic/Formulas.h" #include "src/utility/solver.h" #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" @@ -14,6 +15,9 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew"); + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); std::shared_ptr> mdp = abstractModel->as>(); @@ -23,66 +27,58 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); - auto labelFormula = std::make_shared("two"); - auto eventuallyFormula = std::make_shared(labelFormula); - auto minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + std::shared_ptr formula = parser.parseFromString("Pmin=? [F \"two\"]"); - std::unique_ptr result = checker.check(*minProbabilityOperatorFormula); + std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0277777612209320068, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - auto maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + formula = parser.parseFromString("Pmax=? [F \"two\"]"); - result = checker.check(*maxProbabilityOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0277777612209320068, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("three"); - eventuallyFormula = std::make_shared(labelFormula); - minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + formula = parser.parseFromString("Pmin=? [F \"three\"]"); - result = checker.check(*minProbabilityOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0555555224418640136, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + formula = parser.parseFromString("Pmax=? [F \"three\"]"); - result = checker.check(*maxProbabilityOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0555555224418640136, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("four"); - eventuallyFormula = std::make_shared(labelFormula); - minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + formula = parser.parseFromString("Pmin=? [F \"four\"]"); - result = checker.check(*minProbabilityOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.083333283662796020508, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + formula = parser.parseFromString("Pmax=? [F \"four\"]"); - result = checker.check(*maxProbabilityOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.083333283662796020508, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("done"); - auto reachabilityRewardFormula = std::make_shared(labelFormula); - auto minRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmin=? [F \"done\"]"); - result = checker.check(*minRewardOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult7 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(7.333329499, quantitativeResult7[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - auto maxRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmax=? [F \"done\"]"); - result = checker.check(*maxRewardOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult8 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(7.333329499, quantitativeResult8[0], storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -95,18 +91,16 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { storm::modelchecker::SparseMdpPrctlModelChecker> stateRewardModelChecker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); - labelFormula = std::make_shared("done"); - reachabilityRewardFormula = std::make_shared(labelFormula); - minRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmin=? [F \"done\"]"); - result = stateRewardModelChecker.check(*minRewardOperatorFormula); + result = stateRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult9 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(7.333329499, quantitativeResult9[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - maxRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmax=? [F \"done\"]"); - result = stateRewardModelChecker.check(*maxRewardOperatorFormula); + result = stateRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult10 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(7.333329499, quantitativeResult10[0], storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -119,18 +113,16 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { storm::modelchecker::SparseMdpPrctlModelChecker> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); - labelFormula = std::make_shared("done"); - reachabilityRewardFormula = std::make_shared(labelFormula); - minRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmin=? [F \"done\"]"); - result = stateAndTransitionRewardModelChecker.check(*minRewardOperatorFormula); + result = stateAndTransitionRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult11 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(14.666658998, quantitativeResult11[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - maxRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmax=? [F \"done\"]"); - result = stateAndTransitionRewardModelChecker.check(*maxRewardOperatorFormula); + result = stateAndTransitionRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult12 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(14.666658998, quantitativeResult12[0], storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -139,6 +131,9 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.trans.rew"); + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + ASSERT_EQ(storm::models::ModelType::Mdp, abstractModel->getType()); std::shared_ptr> mdp = abstractModel->as>(); @@ -148,51 +143,44 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); - auto labelFormula = std::make_shared("elected"); - auto eventuallyFormula = std::make_shared(labelFormula); - auto minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + std::shared_ptr formula = parser.parseFromString("Pmin=? [F \"elected\"]"); - std::unique_ptr result = checker.check(*minProbabilityOperatorFormula); + std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - auto maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + formula = parser.parseFromString("Pmax=? [F \"elected\"]"); - result = checker.check(*maxProbabilityOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("elected"); - auto trueFormula = std::make_shared(true); - auto boundedUntilFormula = std::make_shared(trueFormula, labelFormula, 25); - minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, boundedUntilFormula); + formula = parser.parseFromString("Pmin=? [F<=25 \"elected\"]"); - result = checker.check(*minProbabilityOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0625, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, boundedUntilFormula); + formula = parser.parseFromString("Pmax=? [F<=25 \"elected\"]"); - result = checker.check(*maxProbabilityOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0625, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("elected"); - auto reachabilityRewardFormula = std::make_shared(labelFormula); - auto minRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmin=? [F \"elected\"]"); - result = checker.check(*minRewardOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(4.285689611, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - auto maxRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmax=? [F \"elected\"]"); - result = checker.check(*maxRewardOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(4.285689611, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision()); diff --git a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp index 3da0ce7b1..5c6472a88 100644 --- a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp @@ -29,8 +29,7 @@ TEST(SparseCtmcCslModelCheckerTest, Cluster) { #else typename storm::builder::ExplicitPrismModelBuilder::Options options; #endif - options.buildRewards = true; - options.rewardModelName = "num_repairs"; + options.rewardModelsToBuild.insert("num_repairs"); std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); @@ -105,8 +104,7 @@ TEST(SparseCtmcCslModelCheckerTest, Embedded) { #else typename storm::builder::ExplicitPrismModelBuilder::Options options; #endif - options.buildRewards = true; - options.rewardModelName = "up"; + options.rewardModelsToBuild.insert("up"); std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); @@ -201,8 +199,7 @@ TEST(SparseCtmcCslModelCheckerTest, Tandem) { #else typename storm::builder::ExplicitPrismModelBuilder::Options options; #endif - options.buildRewards = true; - options.rewardModelName = "customers"; + options.rewardModelsToBuild.insert("customers"); std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); diff --git a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp index 8cade7ab9..e22750386 100644 --- a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp @@ -31,8 +31,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster) { #else typename storm::builder::DdPrismModelBuilder::Options options; #endif - options.buildRewards = true; - options.rewardModelName = "num_repairs"; + options.rewardModelsToBuild.insert("num_repairs"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); @@ -120,8 +119,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded) { #else typename storm::builder::DdPrismModelBuilder::Options options; #endif - options.buildRewards = true; - options.rewardModelName = "up"; + options.rewardModelsToBuild.insert("up"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); @@ -226,8 +224,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem) { #else typename storm::builder::DdPrismModelBuilder::Options options; #endif - options.buildRewards = true; - options.rewardModelName = "customers"; + options.rewardModelsToBuild.insert("customers"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); diff --git a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp index ad5aa1a1a..851810db8 100644 --- a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp @@ -24,8 +24,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die) { #else typename storm::builder::DdPrismModelBuilder::Options options; #endif - options.buildRewards = true; - options.rewardModelName = "coin_flips"; + options.rewardModelsToBuild.insert("coin_flips"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(20ul, model->getNumberOfTransitions()); @@ -130,8 +129,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader) { #else typename storm::builder::DdPrismModelBuilder::Options options; #endif - options.buildRewards = true; - options.rewardModelName = "num_rounds"; + options.rewardModelsToBuild.insert("num_rounds"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); EXPECT_EQ(273ul, model->getNumberOfStates()); EXPECT_EQ(397ul, model->getNumberOfTransitions()); diff --git a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp index ba6e37abd..7564037f0 100644 --- a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp @@ -7,6 +7,7 @@ #include "src/modelchecker/results/HybridQuantitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" +#include "src/parser/FormulaParser.h" #include "src/parser/PrismParser.h" #include "src/builder/DdPrismModelBuilder.h" #include "src/models/symbolic/Dtmc.h" @@ -17,14 +18,16 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + // Build the die model with its reward model. #ifdef WINDOWS storm::builder::DdPrismModelBuilder::Options options; #else typename storm::builder::DdPrismModelBuilder::Options options; #endif - options.buildRewards = true; - options.rewardModelName = "coinflips"; + options.rewardModelsToBuild.insert("coinflips"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); EXPECT_EQ(169ul, model->getNumberOfStates()); EXPECT_EQ(436ul, model->getNumberOfTransitions()); @@ -35,80 +38,72 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) { storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); - auto labelFormula = std::make_shared("two"); - auto eventuallyFormula = std::make_shared(labelFormula); - auto minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + std::shared_ptr formula = parser.parseFromString("Pmin=? [F \"two\"]"); - std::unique_ptr result = checker.check(*minProbabilityOperatorFormula); + std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - auto maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + formula = parser.parseFromString("Pmax=? [F \"two\"]"); - result = checker.check(*maxProbabilityOperatorFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("three"); - eventuallyFormula = std::make_shared(labelFormula); - minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + formula = parser.parseFromString("Pmin=? [F \"three\"]"); - result = checker.check(*minProbabilityOperatorFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + formula = parser.parseFromString("Pmax=? [F \"three\"]"); - result = checker.check(*maxProbabilityOperatorFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("four"); - eventuallyFormula = std::make_shared(labelFormula); - minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + formula = parser.parseFromString("Pmin=? [F \"four\"]"); - result = checker.check(*minProbabilityOperatorFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + formula = parser.parseFromString("Pmax=? [F \"four\"]"); - result = checker.check(*maxProbabilityOperatorFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult6 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("done"); - auto reachabilityRewardFormula = std::make_shared(labelFormula); - auto minRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmin=? [F \"done\"]"); - result = checker.check(*minRewardOperatorFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult7 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(7.3333283960819244, quantitativeResult7.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(7.3333283960819244, quantitativeResult7.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - auto maxRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmax=? [F \"done\"]"); - result = checker.check(*maxRewardOperatorFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult8 = result->asHybridQuantitativeCheckResult(); @@ -119,14 +114,16 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) { TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + // Build the die model with its reward model. #ifdef WINDOWS storm::builder::DdPrismModelBuilder::Options options; #else typename storm::builder::DdPrismModelBuilder::Options options; #endif - options.buildRewards = true; - options.rewardModelName = "rounds"; + options.rewardModelsToBuild.insert("rounds"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); EXPECT_EQ(3172ul, model->getNumberOfStates()); EXPECT_EQ(7144ul, model->getNumberOfTransitions()); @@ -137,61 +134,54 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); - auto labelFormula = std::make_shared("elected"); - auto eventuallyFormula = std::make_shared(labelFormula); - auto minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + std::shared_ptr formula = parser.parseFromString("Pmin=? [F \"elected\"]"); - std::unique_ptr result = checker.check(*minProbabilityOperatorFormula); + std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - auto maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + formula = parser.parseFromString("Pmax=? [F \"elected\"]"); - result = checker.check(*maxProbabilityOperatorFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("elected"); - auto trueFormula = std::make_shared(true); - auto boundedUntilFormula = std::make_shared(trueFormula, labelFormula, 25); - minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, boundedUntilFormula); + formula = parser.parseFromString("Pmin=? [F<=25 \"elected\"]"); - result = checker.check(*minProbabilityOperatorFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.0625, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0625, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, boundedUntilFormula); + formula = parser.parseFromString("Pmax=? [F \"elected\"]"); - result = checker.check(*maxProbabilityOperatorFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0625, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("elected"); - auto reachabilityRewardFormula = std::make_shared(labelFormula); - auto minRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmin=? [F \"elected\"]"); - result = checker.check(*minRewardOperatorFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(4.2856925589077264, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(4.2856925589077264, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - auto maxRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmax=? [F \"elected\"]"); - result = checker.check(*maxRewardOperatorFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult6 = result->asHybridQuantitativeCheckResult(); diff --git a/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp index c26b9c881..648bdd037 100644 --- a/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp @@ -1,6 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" +#include "src/parser/FormulaParser.h" #include "src/logic/Formulas.h" #include "src/utility/solver.h" #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" @@ -13,6 +14,9 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew"); + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); std::shared_ptr> mdp = abstractModel->as>(); @@ -22,66 +26,58 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); - auto labelFormula = std::make_shared("two"); - auto eventuallyFormula = std::make_shared(labelFormula); - auto minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + std::shared_ptr formula = parser.parseFromString("Pmin=? [F \"two\"]"); - std::unique_ptr result = checker.check(*minProbabilityOperatorFormula); + std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0277777612209320068, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - auto maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); - - result = checker.check(*maxProbabilityOperatorFormula); + formula = parser.parseFromString("Pmax=? [F \"two\"]"); + + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0277777612209320068, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("three"); - eventuallyFormula = std::make_shared(labelFormula); - minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + formula = parser.parseFromString("Pmin=? [F \"three\"]"); - result = checker.check(*minProbabilityOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0555555224418640136, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + formula = parser.parseFromString("Pmax=? [F \"three\"]"); - result = checker.check(*maxProbabilityOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0555555224418640136, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("four"); - eventuallyFormula = std::make_shared(labelFormula); - minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + formula = parser.parseFromString("Pmin=? [F \"four\"]"); - result = checker.check(*minProbabilityOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.083333283662796020508, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + formula = parser.parseFromString("Pmax=? [F \"four\"]"); - result = checker.check(*maxProbabilityOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.083333283662796020508, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("done"); - auto reachabilityRewardFormula = std::make_shared(labelFormula); - auto minRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmin=? [F \"done\"]"); - result = checker.check(*minRewardOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult7 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(7.333329499, quantitativeResult7[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - auto maxRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmax=? [F \"done\"]"); - result = checker.check(*maxRewardOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult8 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(7.333329499, quantitativeResult8[0], storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -94,18 +90,16 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { storm::modelchecker::SparseMdpPrctlModelChecker> stateRewardModelChecker(*stateRewardMdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); - labelFormula = std::make_shared("done"); - reachabilityRewardFormula = std::make_shared(labelFormula); - minRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmin=? [F \"done\"]"); - result = stateRewardModelChecker.check(*minRewardOperatorFormula); + result = stateRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult9 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(7.333329499, quantitativeResult9[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - maxRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmax=? [F \"done\"]"); - result = stateRewardModelChecker.check(*maxRewardOperatorFormula); + result = stateRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult10 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(7.333329499, quantitativeResult10[0], storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -118,18 +112,16 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { storm::modelchecker::SparseMdpPrctlModelChecker> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); - labelFormula = std::make_shared("done"); - reachabilityRewardFormula = std::make_shared(labelFormula); - minRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmin=? [F \"done\"]"); - result = stateAndTransitionRewardModelChecker.check(*minRewardOperatorFormula); + result = stateAndTransitionRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult11 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(14.666658998, quantitativeResult11[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - maxRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmax=? [F \"done\"]"); - result = stateAndTransitionRewardModelChecker.check(*maxRewardOperatorFormula); + result = stateAndTransitionRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult12 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(14.666658998, quantitativeResult12[0], storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -138,6 +130,9 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.trans.rew"); + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + ASSERT_EQ(storm::models::ModelType::Mdp, abstractModel->getType()); std::shared_ptr> mdp = abstractModel->as>(); @@ -147,51 +142,44 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); - auto labelFormula = std::make_shared("elected"); - auto eventuallyFormula = std::make_shared(labelFormula); - auto minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + std::shared_ptr formula = parser.parseFromString("Pmin=? [F \"elected\"]"); - std::unique_ptr result = checker.check(*minProbabilityOperatorFormula); + std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - auto maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + formula = parser.parseFromString("Pmax=? [F \"elected\"]"); - result = checker.check(*maxProbabilityOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("elected"); - auto trueFormula = std::make_shared(true); - auto boundedUntilFormula = std::make_shared(trueFormula, labelFormula, 25); - minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, boundedUntilFormula); + formula = parser.parseFromString("Pmin=? [F<=25 \"elected\"]"); - result = checker.check(*minProbabilityOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0625, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, boundedUntilFormula); + formula = parser.parseFromString("Pmax=? [F<=25 \"elected\"]"); - result = checker.check(*maxProbabilityOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0625, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("elected"); - auto reachabilityRewardFormula = std::make_shared(labelFormula); - auto minRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmin=? [F \"elected\"]"); - result = checker.check(*minRewardOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(4.285689611, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - auto maxRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmax=? [F \"elected\"]"); - result = checker.check(*maxRewardOperatorFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(4.285689611, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -200,7 +188,10 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) { storm::storage::SparseMatrixBuilder matrixBuilder; std::shared_ptr> mdp; - + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + { matrixBuilder = storm::storage::SparseMatrixBuilder(2, 2, 2); matrixBuilder.addNextValue(0, 1, 1.); @@ -215,18 +206,17 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); - auto labelFormula = std::make_shared("a"); - auto lraFormula = std::make_shared(storm::logic::OptimalityType::Maximize, labelFormula); + std::shared_ptr formula = parser.parseFromString("LRAmax=? [\"a\"]"); - std::unique_ptr result = std::move(checker.check(*lraFormula)); + std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(.5, quantitativeResult1[1], storm::settings::nativeEquationSolverSettings().getPrecision()); - lraFormula = std::make_shared(storm::logic::OptimalityType::Minimize, labelFormula); + formula = parser.parseFromString("LRAmin=? [\"a\"]"); - result = std::move(checker.check(*lraFormula)); + result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(.5, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -248,18 +238,17 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); - auto labelFormula = std::make_shared("a"); - auto lraFormula = std::make_shared(storm::logic::OptimalityType::Maximize, labelFormula); + std::shared_ptr formula = parser.parseFromString("LRAmax=? [\"a\"]"); - std::unique_ptr result = std::move(checker.check(*lraFormula)); + std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(.5, quantitativeResult1[1], storm::settings::nativeEquationSolverSettings().getPrecision()); - lraFormula = std::make_shared(storm::logic::OptimalityType::Minimize, labelFormula); + formula = parser.parseFromString("LRAmin=? [\"a\"]"); - result = std::move(checker.check(*lraFormula)); + result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(.5, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -290,57 +279,54 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); - auto labelFormula = std::make_shared("a"); - auto lraFormula = std::make_shared(storm::logic::OptimalityType::Maximize, labelFormula); + std::shared_ptr formula = parser.parseFromString("LRAmax=? [\"a\"]"); - std::unique_ptr result = std::move(checker.check(*lraFormula)); + std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1. / 3., quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1. / 3., quantitativeResult1[1], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1. / 3., quantitativeResult1[2], storm::settings::nativeEquationSolverSettings().getPrecision()); - lraFormula = std::make_shared(storm::logic::OptimalityType::Minimize, labelFormula); + formula = parser.parseFromString("LRAmin=? [\"a\"]"); - result = std::move(checker.check(*lraFormula)); + result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0, quantitativeResult2[1], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0, quantitativeResult2[2], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("b"); - lraFormula = std::make_shared(storm::logic::OptimalityType::Maximize, labelFormula); + formula = parser.parseFromString("LRAmax=? [\"b\"]"); - result = std::move(checker.check(*lraFormula)); + result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.5, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.5, quantitativeResult3[1], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.5, quantitativeResult3[2], storm::settings::nativeEquationSolverSettings().getPrecision()); - lraFormula = std::make_shared(storm::logic::OptimalityType::Minimize, labelFormula); + formula = parser.parseFromString("LRAmin=? [\"b\"]"); - result = std::move(checker.check(*lraFormula)); + result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1. / 3., quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1. / 3., quantitativeResult4[1], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1. / 3., quantitativeResult4[2], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("c"); - lraFormula = std::make_shared(storm::logic::OptimalityType::Maximize, labelFormula); + formula = parser.parseFromString("LRAmax=? [\"c\"]"); - result = std::move(checker.check(*lraFormula)); + result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(2. / 3., quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(2. / 3., quantitativeResult5[1], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(2. / 3., quantitativeResult5[2], storm::settings::nativeEquationSolverSettings().getPrecision()); - lraFormula = std::make_shared(storm::logic::OptimalityType::Minimize, labelFormula); + formula = parser.parseFromString("LRAmin=? [\"c\"]"); - result = std::move(checker.check(*lraFormula)); + result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.5, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -353,6 +339,9 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) { storm::storage::SparseMatrixBuilder matrixBuilder; std::shared_ptr> mdp; + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + { matrixBuilder = storm::storage::SparseMatrixBuilder(4, 3, 4, true, true, 3); matrixBuilder.newRowGroup(0); @@ -376,57 +365,54 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); - auto labelFormula = std::make_shared("a"); - auto lraFormula = std::make_shared(storm::logic::OptimalityType::Maximize, labelFormula); - - std::unique_ptr result = std::move(checker.check(*lraFormula)); + std::shared_ptr formula = parser.parseFromString("LRAmax=? [\"a\"]"); + + std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0, quantitativeResult1[1], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0, quantitativeResult1[2], storm::settings::nativeEquationSolverSettings().getPrecision()); - lraFormula = std::make_shared(storm::logic::OptimalityType::Minimize, labelFormula); + formula = parser.parseFromString("LRAmin=? [\"a\"]"); - result = std::move(checker.check(*lraFormula)); + result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0, quantitativeResult2[1], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0, quantitativeResult2[2], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("b"); - lraFormula = std::make_shared(storm::logic::OptimalityType::Maximize, labelFormula); + formula = parser.parseFromString("LRAmax=? [\"b\"]"); - result = std::move(checker.check(*lraFormula)); + result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0, quantitativeResult3[1], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0, quantitativeResult3[2], storm::settings::nativeEquationSolverSettings().getPrecision()); - lraFormula = std::make_shared(storm::logic::OptimalityType::Minimize, labelFormula); + formula = parser.parseFromString("LRAmin=? [\"b\"]"); - result = std::move(checker.check(*lraFormula)); + result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0, quantitativeResult4[1], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0, quantitativeResult4[2], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("c"); - lraFormula = std::make_shared(storm::logic::OptimalityType::Maximize, labelFormula); + formula = parser.parseFromString("LRAmax=? [\"c\"]"); - result = std::move(checker.check(*lraFormula)); + result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0, quantitativeResult5[1], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0, quantitativeResult5[2], storm::settings::nativeEquationSolverSettings().getPrecision()); - lraFormula = std::make_shared(storm::logic::OptimalityType::Minimize, labelFormula); + formula = parser.parseFromString("LRAmin=? [\"c\"]"); - result = std::move(checker.check(*lraFormula)); + result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -501,10 +487,9 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); - auto labelFormula = std::make_shared("a"); - auto lraFormula = std::make_shared(storm::logic::OptimalityType::Maximize, labelFormula); + std::shared_ptr formula = parser.parseFromString("LRAmax=? [\"a\"]"); - std::unique_ptr result = std::move(checker.check(*lraFormula)); + std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(37./60., quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -515,9 +500,9 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) { EXPECT_NEAR(101./200., quantitativeResult1[13], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(31./60., quantitativeResult1[14], storm::settings::nativeEquationSolverSettings().getPrecision()); - lraFormula = std::make_shared(storm::logic::OptimalityType::Minimize, labelFormula); + formula = parser.parseFromString("LRAmin=? [\"a\"]"); - result = std::move(checker.check(*lraFormula)); + result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.3 / 3., quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision()); diff --git a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp index 3ecea41a7..0aa11f575 100644 --- a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp @@ -22,8 +22,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die) { #else typename storm::builder::DdPrismModelBuilder::Options options; #endif - options.buildRewards = true; - options.rewardModelName = "coin_flips"; + options.rewardModelsToBuild.insert("coin_flips"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(20ul, model->getNumberOfTransitions()); @@ -128,8 +127,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader) { #else typename storm::builder::DdPrismModelBuilder::Options options; #endif - options.buildRewards = true; - options.rewardModelName = "num_rounds"; + options.rewardModelsToBuild.insert("num_rounds"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); EXPECT_EQ(273ul, model->getNumberOfStates()); EXPECT_EQ(397ul, model->getNumberOfTransitions()); diff --git a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp index a71930f44..159568433 100644 --- a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp @@ -1,7 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" - +#include "src/parser/FormulaParser.h" #include "src/logic/Formulas.h" #include "src/utility/solver.h" #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" @@ -19,277 +19,173 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { //storm::settings::Settings* s = storm::settings::Settings::getInstance(); std::shared_ptr> mdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew")->as>(); + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + ASSERT_EQ(mdp->getNumberOfStates(), 169ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); - storm::modelchecker::SparseMdpPrctlModelChecker mc(*mdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> mc(*mdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); - //storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("two"); - auto apFormula = std::make_shared("two"); - //storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); - auto eventuallyFormula = std::make_shared(apFormula); - //storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); - auto probabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + std::shared_ptr formula = parser.parseFromString("Pmin=? [F \"two\"]"); - //std::vector result = mc.checkNoBoundOperator(*probFormula); - std::unique_ptr result = mc.check(*probabilityOperatorFormula); + std::unique_ptr result = mc.check(*formula); - //ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 0.0277777612209320068), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + ASSERT_NEAR(0.0277777612209320068, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - //delete probFormula; - probabilityOperatorFormula.reset(); - - //apFormula = new storm::property::prctl::Ap("two"); - apFormula = std::make_shared("two"); - //eventuallyFormula = new storm::property::prctl::Eventually(apFormula); - eventuallyFormula = std::make_shared(apFormula); - //probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); - probabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + formula = parser.parseFromString("Pmax=? [F \"two\"]"); - //result = mc.checkNoBoundOperator(*probFormula); - result = mc.check(*probabilityOperatorFormula); + result = mc.check(*formula); - //ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 0.0277777612209320068), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + ASSERT_NEAR(0.0277777612209320068, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - //delete probFormula; - probabilityOperatorFormula.reset(); - - // ---------------- test ap "three" ---------------- - apFormula = std::make_shared("three"); - eventuallyFormula = std::make_shared(apFormula); - probabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + formula = parser.parseFromString("Pmin=? [F \"three\"]"); - result = mc.check(*probabilityOperatorFormula); + result = mc.check(*formula); - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 0.0555555224418640136), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - - probabilityOperatorFormula.reset(); + ASSERT_NEAR(0.0555555224418640136, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - apFormula = std::make_shared("three"); - eventuallyFormula = std::make_shared(apFormula); - probabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + formula = parser.parseFromString("Pmax=? [F \"three\"]"); - result = mc.check(*probabilityOperatorFormula); + result = mc.check(*formula); - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 0.0555555224418640136), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + ASSERT_NEAR(0.0555555224418640136, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - probabilityOperatorFormula.reset(); + formula = parser.parseFromString("Pmin=? [F \"four\"]"); - // ---------------- test ap "four" ---------------- - apFormula = std::make_shared("four"); - eventuallyFormula = std::make_shared(apFormula); - probabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + result = mc.check(*formula); - result = mc.check(*probabilityOperatorFormula); + ASSERT_NEAR(0.083333283662796020508, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 0.083333283662796020508), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - - probabilityOperatorFormula.reset(); + formula = parser.parseFromString("Pmax=? [F \"four\"]"); - apFormula = std::make_shared("four"); - eventuallyFormula = std::make_shared(apFormula); - probabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + result = mc.check(*formula); - result = mc.check(*probabilityOperatorFormula); + ASSERT_NEAR(0.083333283662796020508, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 0.083333283662796020508), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + formula = parser.parseFromString("Rmin=? [F \"done\"]"); - probabilityOperatorFormula.reset(); - - - // ---------------- test ap "done" ---------------- - apFormula = std::make_shared("done"); - auto reachabilityRewardFormula = std::make_shared(apFormula); - auto rewardFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); - - result = mc.check(*rewardFormula); + result = mc.check(*formula); #ifdef STORM_HAVE_CUDA - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 7.333329499), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + ASSERT_NEAR(7.333329499, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #else - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 7.33332904), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + ASSERT_NEAR(7.33332904, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #endif - rewardFormula.reset(); - - apFormula = std::make_shared("done"); - reachabilityRewardFormula = std::make_shared(apFormula); - rewardFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmax=? [F \"done\"]"); - result = mc.check(*rewardFormula); + result = mc.check(*formula); #ifdef STORM_HAVE_CUDA - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 7.333329499), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + ASSERT_NEAR(7.333329499, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #else - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 7.33333151), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + ASSERT_NEAR(7.33333151, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #endif - rewardFormula.reset(); // ------------- state rewards -------------- std::shared_ptr> stateRewardMdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", "")->as>(); - storm::modelchecker::SparseMdpPrctlModelChecker stateRewardModelChecker(*stateRewardMdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> stateRewardModelChecker(*stateRewardMdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); - apFormula = std::make_shared("done"); - reachabilityRewardFormula = std::make_shared(apFormula); - rewardFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmin=? [F \"done\"]"); - result = stateRewardModelChecker.check(*rewardFormula); + result = stateRewardModelChecker.check(*formula); #ifdef STORM_HAVE_CUDA - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 7.333329499), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + ASSERT_NEAR(7.333329499, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #else - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 7.33332904), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + ASSERT_NEAR(7.33332904, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #endif - rewardFormula.reset(); - apFormula = std::make_shared("done"); - reachabilityRewardFormula = std::make_shared(apFormula); - rewardFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmax=? [F \"done\"]"); - result = stateRewardModelChecker.check(*rewardFormula); + result = stateRewardModelChecker.check(*formula); #ifdef STORM_HAVE_CUDA - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 7.333329499), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + ASSERT_NEAR(7.333329499, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #else - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 7.33333151), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + ASSERT_NEAR(7.33333151, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #endif - rewardFormula.reset(); // -------------------------------- state and transition reward ------------------------ std::shared_ptr> stateAndTransitionRewardMdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew")->as>(); - storm::modelchecker::SparseMdpPrctlModelChecker stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); + formula = parser.parseFromString("Rmin=? [F \"done\"]"); - apFormula = std::make_shared("done"); - reachabilityRewardFormula = std::make_shared(apFormula); - rewardFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); - - result = stateAndTransitionRewardModelChecker.check(*rewardFormula); + result = stateAndTransitionRewardModelChecker.check(*formula); #ifdef STORM_HAVE_CUDA - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 14.666658998), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + ASSERT_NEAR(14.666658998, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #else - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 14.6666581), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + ASSERT_NEAR(14.6666581, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #endif - rewardFormula.reset(); - - apFormula = std::make_shared("done"); - reachabilityRewardFormula = std::make_shared(apFormula); - rewardFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmax=? [F \"done\"]"); - result = stateAndTransitionRewardModelChecker.check(*rewardFormula); + result = stateAndTransitionRewardModelChecker.check(*formula); #ifdef STORM_HAVE_CUDA - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 14.666658998), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + ASSERT_NEAR(14.666658998, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #else - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 14.666663), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + ASSERT_NEAR(14.666663, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #endif - rewardFormula.reset(); } TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) { std::shared_ptr> mdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.trans.rew")->as>(); + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + ASSERT_EQ(mdp->getNumberOfStates(), 3172ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 7144ull); - storm::modelchecker::SparseMdpPrctlModelChecker mc(*mdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> mc(*mdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); - auto apFormula = std::make_shared("elected"); - auto eventuallyFormula = std::make_shared(apFormula); - auto probabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + std::shared_ptr formula = parser.parseFromString("Pmin=? [F \"elected\"]"); - std::unique_ptr result = mc.check(*probabilityOperatorFormula); - - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 1), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - - probabilityOperatorFormula.reset(); - - apFormula = std::make_shared("elected"); - eventuallyFormula = std::make_shared(apFormula); - probabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); - - result = mc.check(*probabilityOperatorFormula); + std::unique_ptr result = mc.check(*formula); ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 1), storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - probabilityOperatorFormula.reset(); + formula = parser.parseFromString("Pmax=? [F \"elected\"]"); - apFormula = std::make_shared("elected"); - auto boundedEventuallyFormula = std::make_shared(std::make_shared(true), apFormula, 25); - probabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, boundedEventuallyFormula); + result = mc.check(*formula); - result = mc.check(*probabilityOperatorFormula); + ASSERT_NEAR(1, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 0.0625), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + formula = parser.parseFromString("Pmax=? [F<=25 \"elected\"]"); - probabilityOperatorFormula.reset(); + result = mc.check(*formula); - apFormula = std::make_shared("elected"); - boundedEventuallyFormula = std::make_shared(std::make_shared(true), apFormula, 25); - probabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, boundedEventuallyFormula); + ASSERT_NEAR(0.0625, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - result = mc.check(*probabilityOperatorFormula); + formula = parser.parseFromString("Pmin=? [F<=25 \"elected\"]"); - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 0.0625), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + result = mc.check(*formula); - probabilityOperatorFormula.reset(); + ASSERT_NEAR(0.0625, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - apFormula = std::make_shared("elected"); - auto reachabilityRewardFormula = std::make_shared(apFormula); - auto rewardFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmin=? [F \"elected\"]"); - result = mc.check(*rewardFormula); + result = mc.check(*formula); #ifdef STORM_HAVE_CUDA - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 4.285689611), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + ASSERT_NEAR(4.285689611, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #else - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 4.285701547), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + ASSERT_NEAR(4.285701547, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #endif - probabilityOperatorFormula.reset(); - - apFormula = std::make_shared("elected"); - reachabilityRewardFormula = std::make_shared(apFormula); - rewardFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + formula = parser.parseFromString("Rmax=? [F \"elected\"]"); - result = mc.check(*rewardFormula); + result = mc.check(*formula); #ifdef STORM_HAVE_CUDA - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 4.285689611), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + ASSERT_NEAR(4.285689611, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #else - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 4.285703591), - storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + ASSERT_NEAR(4.285703591, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #endif - - probabilityOperatorFormula.reset(); } diff --git a/test/functional/parser/AutoParserTest.cpp b/test/functional/parser/AutoParserTest.cpp index 0894baef0..c3d8e0082 100644 --- a/test/functional/parser/AutoParserTest.cpp +++ b/test/functional/parser/AutoParserTest.cpp @@ -20,8 +20,7 @@ TEST(AutoParserTest, BasicParsing) { ASSERT_EQ(26ul, modelPtr->getNumberOfTransitions()); ASSERT_EQ(1ul, modelPtr->getInitialStates().getNumberOfSetBits()); ASSERT_TRUE(modelPtr->hasLabel("three")); - ASSERT_FALSE(modelPtr->hasStateRewards()); - ASSERT_FALSE(modelPtr->hasTransitionRewards()); + ASSERT_FALSE(modelPtr->hasRewardModel()); } TEST(AutoParserTest, WrongHint) { diff --git a/test/functional/parser/DeterministicModelParserTest.cpp b/test/functional/parser/DeterministicModelParserTest.cpp index 53fe51ca4..154b06114 100644 --- a/test/functional/parser/DeterministicModelParserTest.cpp +++ b/test/functional/parser/DeterministicModelParserTest.cpp @@ -31,19 +31,19 @@ TEST(DeterministicModelParserTest, BasicDtmcParsing) { ASSERT_EQ(5ul, dtmc.getStateLabeling().getNumberOfLabels()); ASSERT_EQ(2ul, dtmc.getLabelsOfState(6).size()); - ASSERT_TRUE(dtmc.hasStateRewards()); - ASSERT_EQ(42, dtmc.getStateRewardVector()[7]); + ASSERT_TRUE(dtmc.hasRewardModel()); + ASSERT_EQ(42, dtmc.getRewardModel("").getStateRewardVector()[7]); double rewardSum = 0; - for(uint_fast64_t i = 0; i < dtmc.getStateRewardVector().size(); i++) { - rewardSum += dtmc.getStateRewardVector()[i]; + for(uint_fast64_t i = 0; i < dtmc.getRewardModel("").getStateRewardVector().size(); i++) { + rewardSum += dtmc.getRewardModel("").getStateRewardVector()[i]; } ASSERT_EQ(263.32, rewardSum); - ASSERT_TRUE(dtmc.hasTransitionRewards()); - ASSERT_EQ(17ul, dtmc.getTransitionRewardMatrix().getEntryCount()); + ASSERT_TRUE(dtmc.getRewardModel("").hasTransitionRewards()); + ASSERT_EQ(17ul, dtmc.getRewardModel("").getTransitionRewardMatrix().getEntryCount()); rewardSum = 0; - for(uint_fast64_t i = 0; i < dtmc.getTransitionRewardMatrix().getRowCount(); i++) { - rewardSum += dtmc.getTransitionRewardMatrix().getRowSum(i); + for(uint_fast64_t i = 0; i < dtmc.getRewardModel("").getTransitionRewardMatrix().getRowCount(); i++) { + rewardSum += dtmc.getRewardModel("").getTransitionRewardMatrix().getRowSum(i); } ASSERT_EQ(125.4, rewardSum); } @@ -63,19 +63,19 @@ TEST(DeterministicModelParserTest, BasicCtmcParsing) { ASSERT_EQ(5ul, ctmc.getStateLabeling().getNumberOfLabels()); ASSERT_EQ(2ul, ctmc.getLabelsOfState(6).size()); - ASSERT_TRUE(ctmc.hasStateRewards()); - ASSERT_EQ(42, ctmc.getStateRewardVector()[7]); + ASSERT_TRUE(ctmc.hasRewardModel()); + ASSERT_EQ(42, ctmc.getRewardModel("").getStateRewardVector()[7]); double rewardSum = 0; - for(uint_fast64_t i = 0; i < ctmc.getStateRewardVector().size(); i++) { - rewardSum += ctmc.getStateRewardVector()[i]; + for(uint_fast64_t i = 0; i < ctmc.getRewardModel("").getStateRewardVector().size(); i++) { + rewardSum += ctmc.getRewardModel("").getStateRewardVector()[i]; } ASSERT_EQ(263.32, rewardSum); - ASSERT_TRUE(ctmc.hasTransitionRewards()); - ASSERT_EQ(17ul, ctmc.getTransitionRewardMatrix().getEntryCount()); + ASSERT_TRUE(ctmc.getRewardModel("").hasTransitionRewards()); + ASSERT_EQ(17ul, ctmc.getRewardModel("").getTransitionRewardMatrix().getEntryCount()); rewardSum = 0; - for(uint_fast64_t i = 0; i < ctmc.getTransitionRewardMatrix().getRowCount(); i++) { - rewardSum += ctmc.getTransitionRewardMatrix().getRowSum(i); + for(uint_fast64_t i = 0; i < ctmc.getRewardModel("").getTransitionRewardMatrix().getRowCount(); i++) { + rewardSum += ctmc.getRewardModel("").getTransitionRewardMatrix().getRowSum(i); } ASSERT_EQ(125.4, rewardSum); } diff --git a/test/functional/parser/MarkovAutomatonParserTest.cpp b/test/functional/parser/MarkovAutomatonParserTest.cpp index 479b60752..9152dab08 100644 --- a/test/functional/parser/MarkovAutomatonParserTest.cpp +++ b/test/functional/parser/MarkovAutomatonParserTest.cpp @@ -41,16 +41,16 @@ TEST(MarkovAutomatonParserTest, BasicParsing) { ASSERT_EQ(1ul, result.getStateLabeling().getStates("goal").getNumberOfSetBits()); // Test the state rewards. - ASSERT_TRUE(result.hasStateRewards()); + ASSERT_TRUE(result.hasRewardModel()); double rewardSum = 0; - for (uint_fast64_t i = 0; i < result.getStateRewardVector().size(); i++) { - rewardSum += result.getStateRewardVector()[i]; + for (uint_fast64_t i = 0; i < result.getRewardModel("").getStateRewardVector().size(); i++) { + rewardSum += result.getRewardModel("").getStateRewardVector()[i]; } ASSERT_EQ(1015.765099984, rewardSum); - ASSERT_EQ(0, result.getStateRewardVector()[0]); + ASSERT_EQ(0, result.getRewardModel("").getStateRewardVector()[0]); // Test the transition rewards. - ASSERT_FALSE(result.hasTransitionRewards()); + ASSERT_FALSE(result.getRewardModel("").hasTransitionRewards()); } TEST(MarkovAutomatonParserTest, MismatchedFiles) { diff --git a/test/functional/parser/NondeterministicModelParserTest.cpp b/test/functional/parser/NondeterministicModelParserTest.cpp index d87b5cdf0..7f956d06f 100644 --- a/test/functional/parser/NondeterministicModelParserTest.cpp +++ b/test/functional/parser/NondeterministicModelParserTest.cpp @@ -28,20 +28,20 @@ TEST(NondeterministicModelParserTest, BasicMdpParsing) { ASSERT_EQ(4ul, mdp.getStateLabeling().getNumberOfLabels()); ASSERT_EQ(3ul, mdp.getLabelsOfState(0).size()); - ASSERT_TRUE(mdp.hasStateRewards()); - ASSERT_EQ(0, mdp.getStateRewardVector()[0]); - ASSERT_EQ(42, mdp.getStateRewardVector()[4]); + ASSERT_TRUE(mdp.hasRewardModel()); + ASSERT_EQ(0, mdp.getRewardModel("").getStateRewardVector()[0]); + ASSERT_EQ(42, mdp.getRewardModel("").getStateRewardVector()[4]); double rewardSum = 0; - for(uint_fast64_t i = 0; i < mdp.getStateRewardVector().size(); i++) { - rewardSum += mdp.getStateRewardVector()[i]; + for(uint_fast64_t i = 0; i < mdp.getRewardModel("").getStateRewardVector().size(); i++) { + rewardSum += mdp.getRewardModel("").getStateRewardVector()[i]; } ASSERT_EQ(158.32, rewardSum); - ASSERT_TRUE(mdp.hasTransitionRewards()); - ASSERT_EQ(17ul, mdp.getTransitionRewardMatrix().getEntryCount()); + ASSERT_TRUE(mdp.getRewardModel("").hasTransitionRewards()); + ASSERT_EQ(17ul, mdp.getRewardModel("").getTransitionRewardMatrix().getEntryCount()); rewardSum = 0; - for(uint_fast64_t i = 0; i < mdp.getTransitionRewardMatrix().getRowCount(); i++) { - rewardSum += mdp.getTransitionRewardMatrix().getRowSum(i); + for(uint_fast64_t i = 0; i < mdp.getRewardModel("").getTransitionRewardMatrix().getRowCount(); i++) { + rewardSum += mdp.getRewardModel("").getTransitionRewardMatrix().getRowSum(i); } ASSERT_EQ(1376.864, rewardSum); }