sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

functional tests compile again, started to debug changes 

Former-commit-id: efef0e6487
main
dehnert 10 years ago
parent
1a07b24682
commit
dbc7d860a4
20 changed files with 330 additions and 501 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      src/builder/ExplicitPrismModelBuilder.cpp
  2. 3
      src/settings/modules/GeneralSettings.cpp
  3. 1
      src/utility/constants.cpp
  4. 3
      src/utility/constants.h
  5. 9
      test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
  6. 9
      test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
  7. 6
      test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
  8. 84
      test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
  9. 98
      test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
  10. 9
      test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
  11. 9
      test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp
  12. 6
      test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp
  13. 84
      test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
  14. 191
      test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
  15. 6
      test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
  16. 248
      test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp
  17. 3
      test/functional/parser/AutoParserTest.cpp
  18. 32
      test/functional/parser/DeterministicModelParserTest.cpp
  19. 10
      test/functional/parser/MarkovAutomatonParserTest.cpp
  20. 18
      test/functional/parser/NondeterministicModelParserTest.cpp

2
src/builder/ExplicitPrismModelBuilder.cpp
View File

@ -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<ValueType> comparator;
// Initialize a queue and insert the initial state.

3
src/settings/modules/GeneralSettings.cpp
View File

@ -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 {

1
src/utility/constants.cpp
View File

@ -184,6 +184,7 @@ namespace storm {
}
bool ConstantsComparator<double>::isOne(double const& value) const {
std::cout << std::setprecision(10) << std::abs(value - one<double>()) << " prec: " << precision << std::endl;
return std::abs(value - one<double>()) <= precision;
}

3
src/utility/constants.h
View File

@ -34,7 +34,6 @@ namespace storm {
template<typename ValueType>
ValueType pow(ValueType const& value, uint_fast64_t exponent);
template<typename ValueType>
ValueType simplify(ValueType value);
@ -54,8 +53,6 @@ namespace storm {
bool isInfinity(ValueType const& value) const;
};
template<typename IndexType, typename ValueType>
storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry);

9
test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
View File

@ -29,8 +29,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Cluster) {
#else
typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
#endif
options.buildRewards = true;
options.rewardModelName = "num_repairs";
options.rewardModelsToBuild.insert("num_repairs");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
@ -113,8 +112,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Embedded) {
typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
#endif
options.buildRewards = true;
options.rewardModelName = "up";
options.rewardModelsToBuild.insert("up");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
@ -223,8 +221,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Tandem) {
#else
typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
#endif
options.buildRewards = true;
options.rewardModelName = "customers";
options.rewardModelsToBuild.insert("customers");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();

9
test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
View File

@ -32,8 +32,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) {
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
options.buildRewards = true;
options.rewardModelName = "num_repairs";
options.rewardModelsToBuild.insert("num_repairs");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>> ctmc = model->as<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>>();
@ -129,8 +128,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded) {
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
options.buildRewards = true;
options.rewardModelName = "up";
options.rewardModelsToBuild.insert("up");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>> ctmc = model->as<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>>();
@ -252,8 +250,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem) {
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
options.buildRewards = true;
options.rewardModelName = "customers";
options.rewardModelsToBuild.insert("customers");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>> ctmc = model->as<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>>();

6
test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
View File

@ -23,8 +23,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die) {
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
options.buildRewards = true;
options.rewardModelName = "coin_flips";
options.rewardModelsToBuild.insert("coin_flips");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::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<storm::dd::DdType::CUDD>::Options options;
#endif
options.buildRewards = true;
options.rewardModelName = "num_rounds";
options.rewardModelsToBuild.insert("num_rounds");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
EXPECT_EQ(273ul, model->getNumberOfStates());
EXPECT_EQ(397ul, model->getNumberOfTransitions());

84
test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
View File

@ -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<storm::dd::DdType::CUDD>::Options options;
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
options.buildRewards = true;
options.rewardModelName = "coinflips";
options.rewardModelsToBuild.insert("coinflips");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
EXPECT_EQ(169ul, model->getNumberOfStates());
EXPECT_EQ(436ul, model->getNumberOfTransitions());
@ -37,80 +40,72 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) {
storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("two");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
auto minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("Pmin=? [F \"two\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*minProbabilityOperatorFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult1 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
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::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
formula = parser.parseFromString("Pmax=? [F \"two\"]");
result = checker.check(*maxProbabilityOperatorFormula);
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult2 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("three");
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
formula = parser.parseFromString("Pmin=? [F \"three\"]");
result = checker.check(*minProbabilityOperatorFormula);
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult3 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
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::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
formula = parser.parseFromString("Pmax=? [F \"three\"]");
result = checker.check(*maxProbabilityOperatorFormula);
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult4 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("four");
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
formula = parser.parseFromString("Pmin=? [F \"four\"]");
result = checker.check(*minProbabilityOperatorFormula);
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
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::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
formula = parser.parseFromString("Pmax=? [F \"four\"]");
result = checker.check(*maxProbabilityOperatorFormula);
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult6 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done");
auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
auto minRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
formula = parser.parseFromString("Rmin=? [F \"done\"]");
result = checker.check(*minRewardOperatorFormula);
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult7 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
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::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
formula = parser.parseFromString("Rmax=? [F \"done\"]");
result = checker.check(*maxRewardOperatorFormula);
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult8 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
@ -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<storm::dd::DdType::CUDD>::Options options;
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
options.buildRewards = true;
options.rewardModelName = "rounds";
options.rewardModelsToBuild.insert("rounds");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
EXPECT_EQ(3172ul, model->getNumberOfStates());
EXPECT_EQ(7144ul, model->getNumberOfTransitions());
@ -139,61 +136,54 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader) {
storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
auto minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("Pmin=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*minProbabilityOperatorFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>();
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::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
formula = parser.parseFromString("Pmax=? [F \"elected\"]");
result = checker.check(*maxProbabilityOperatorFormula);
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>();
EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(1, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto trueFormula = std::make_shared<storm::logic::BooleanLiteralFormula>(true);
auto boundedUntilFormula = std::make_shared<storm::logic::BoundedUntilFormula>(trueFormula, labelFormula, 25);
minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(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<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult3 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
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::ProbabilityOperatorFormula>(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<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult4 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0625, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
auto minRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
formula = parser.parseFromString("Rmin=? [F \"elected\"]");
result = checker.check(*minRewardOperatorFormula);
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
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::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
formula = parser.parseFromString("Rmax=? [F \"elected\"]");
result = checker.check(*maxRewardOperatorFormula);
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult6 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();

98
test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
View File

@ -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<storm::models::sparse::Model<double>> 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<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
@ -23,66 +27,58 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("two");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
auto minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("Pmin=? [F \"two\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*minProbabilityOperatorFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0277777612209320068, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
auto maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
formula = parser.parseFromString("Pmax=? [F \"two\"]");
result = checker.check(*maxProbabilityOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("three");
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
formula = parser.parseFromString("Pmin=? [F \"three\"]");
result = checker.check(*minProbabilityOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0555555224418640136, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision());
maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
formula = parser.parseFromString("Pmax=? [F \"three\"]");
result = checker.check(*maxProbabilityOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("four");
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
formula = parser.parseFromString("Pmin=? [F \"four\"]");
result = checker.check(*minProbabilityOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.083333283662796020508, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision());
maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
formula = parser.parseFromString("Pmax=? [F \"four\"]");
result = checker.check(*maxProbabilityOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done");
auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
auto minRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
formula = parser.parseFromString("Rmin=? [F \"done\"]");
result = checker.check(*minRewardOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult7 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(7.333329499, quantitativeResult7[0], storm::settings::nativeEquationSolverSettings().getPrecision());
auto maxRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
formula = parser.parseFromString("Rmax=? [F \"done\"]");
result = checker.check(*maxRewardOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult8 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(7.333329499, quantitativeResult8[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -95,18 +91,16 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateRewardModelChecker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done");
reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
minRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
formula = parser.parseFromString("Rmin=? [F \"done\"]");
result = stateRewardModelChecker.check(*minRewardOperatorFormula);
result = stateRewardModelChecker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult9 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(7.333329499, quantitativeResult9[0], storm::settings::nativeEquationSolverSettings().getPrecision());
maxRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
formula = parser.parseFromString("Rmax=? [F \"done\"]");
result = stateRewardModelChecker.check(*maxRewardOperatorFormula);
result = stateRewardModelChecker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult10 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(7.333329499, quantitativeResult10[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -119,18 +113,16 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done");
reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
minRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
formula = parser.parseFromString("Rmin=? [F \"done\"]");
result = stateAndTransitionRewardModelChecker.check(*minRewardOperatorFormula);
result = stateAndTransitionRewardModelChecker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult11 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(14.666658998, quantitativeResult11[0], storm::settings::nativeEquationSolverSettings().getPrecision());
maxRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
formula = parser.parseFromString("Rmax=? [F \"done\"]");
result = stateAndTransitionRewardModelChecker.check(*maxRewardOperatorFormula);
result = stateAndTransitionRewardModelChecker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult12 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(14.666658998, quantitativeResult12[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -139,6 +131,9 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
std::shared_ptr<storm::models::sparse::Model<double>> 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<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
@ -148,51 +143,44 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
auto minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("Pmin=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*minProbabilityOperatorFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
auto maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
formula = parser.parseFromString("Pmax=? [F \"elected\"]");
result = checker.check(*maxProbabilityOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto trueFormula = std::make_shared<storm::logic::BooleanLiteralFormula>(true);
auto boundedUntilFormula = std::make_shared<storm::logic::BoundedUntilFormula>(trueFormula, labelFormula, 25);
minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, boundedUntilFormula);
formula = parser.parseFromString("Pmin=? [F<=25 \"elected\"]");
result = checker.check(*minProbabilityOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0625, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision());
maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, boundedUntilFormula);
formula = parser.parseFromString("Pmax=? [F<=25 \"elected\"]");
result = checker.check(*maxProbabilityOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0625, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
auto minRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
formula = parser.parseFromString("Rmin=? [F \"elected\"]");
result = checker.check(*minRewardOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(4.285689611, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision());
auto maxRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
formula = parser.parseFromString("Rmax=? [F \"elected\"]");
result = checker.check(*maxRewardOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(4.285689611, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision());

9
test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
View File

@ -29,8 +29,7 @@ TEST(SparseCtmcCslModelCheckerTest, Cluster) {
#else
typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
#endif
options.buildRewards = true;
options.rewardModelName = "num_repairs";
options.rewardModelsToBuild.insert("num_repairs");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
@ -105,8 +104,7 @@ TEST(SparseCtmcCslModelCheckerTest, Embedded) {
#else
typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
#endif
options.buildRewards = true;
options.rewardModelName = "up";
options.rewardModelsToBuild.insert("up");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
@ -201,8 +199,7 @@ TEST(SparseCtmcCslModelCheckerTest, Tandem) {
#else
typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
#endif
options.buildRewards = true;
options.rewardModelName = "customers";
options.rewardModelsToBuild.insert("customers");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();

9
test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp
View File

@ -31,8 +31,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster) {
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
options.buildRewards = true;
options.rewardModelName = "num_repairs";
options.rewardModelsToBuild.insert("num_repairs");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>> ctmc = model->as<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>>();
@ -120,8 +119,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded) {
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
options.buildRewards = true;
options.rewardModelName = "up";
options.rewardModelsToBuild.insert("up");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>> ctmc = model->as<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>>();
@ -226,8 +224,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem) {
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
options.buildRewards = true;
options.rewardModelName = "customers";
options.rewardModelsToBuild.insert("customers");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>> ctmc = model->as<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>>();

6
test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp
View File

@ -24,8 +24,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die) {
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
options.buildRewards = true;
options.rewardModelName = "coin_flips";
options.rewardModelsToBuild.insert("coin_flips");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::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<storm::dd::DdType::CUDD>::Options options;
#endif
options.buildRewards = true;
options.rewardModelName = "num_rounds";
options.rewardModelsToBuild.insert("num_rounds");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
EXPECT_EQ(273ul, model->getNumberOfStates());
EXPECT_EQ(397ul, model->getNumberOfTransitions());

84
test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
View File

@ -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<storm::dd::DdType::CUDD>::Options options;
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
options.buildRewards = true;
options.rewardModelName = "coinflips";
options.rewardModelsToBuild.insert("coinflips");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
EXPECT_EQ(169ul, model->getNumberOfStates());
EXPECT_EQ(436ul, model->getNumberOfTransitions());
@ -35,80 +38,72 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) {
storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("two");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
auto minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("Pmin=? [F \"two\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*minProbabilityOperatorFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult1 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
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::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
formula = parser.parseFromString("Pmax=? [F \"two\"]");
result = checker.check(*maxProbabilityOperatorFormula);
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult2 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("three");
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
formula = parser.parseFromString("Pmin=? [F \"three\"]");
result = checker.check(*minProbabilityOperatorFormula);
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult3 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
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::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
formula = parser.parseFromString("Pmax=? [F \"three\"]");
result = checker.check(*maxProbabilityOperatorFormula);
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult4 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("four");
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
formula = parser.parseFromString("Pmin=? [F \"four\"]");
result = checker.check(*minProbabilityOperatorFormula);
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
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::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
formula = parser.parseFromString("Pmax=? [F \"four\"]");
result = checker.check(*maxProbabilityOperatorFormula);
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult6 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done");
auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
auto minRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
formula = parser.parseFromString("Rmin=? [F \"done\"]");
result = checker.check(*minRewardOperatorFormula);
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult7 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
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::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
formula = parser.parseFromString("Rmax=? [F \"done\"]");
result = checker.check(*maxRewardOperatorFormula);
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult8 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
@ -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<storm::dd::DdType::CUDD>::Options options;
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
options.buildRewards = true;
options.rewardModelName = "rounds";
options.rewardModelsToBuild.insert("rounds");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
EXPECT_EQ(3172ul, model->getNumberOfStates());
EXPECT_EQ(7144ul, model->getNumberOfTransitions());
@ -137,61 +134,54 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) {
storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
auto minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("Pmin=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*minProbabilityOperatorFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>();
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::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
formula = parser.parseFromString("Pmax=? [F \"elected\"]");
result = checker.check(*maxProbabilityOperatorFormula);
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>();
EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(1, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto trueFormula = std::make_shared<storm::logic::BooleanLiteralFormula>(true);
auto boundedUntilFormula = std::make_shared<storm::logic::BoundedUntilFormula>(trueFormula, labelFormula, 25);
minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(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<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult3 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
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::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, boundedUntilFormula);
formula = parser.parseFromString("Pmax=? [F \"elected\"]");
result = checker.check(*maxProbabilityOperatorFormula);
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult4 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0625, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
auto minRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
formula = parser.parseFromString("Rmin=? [F \"elected\"]");
result = checker.check(*minRewardOperatorFormula);
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
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::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
formula = parser.parseFromString("Rmax=? [F \"elected\"]");
result = checker.check(*maxRewardOperatorFormula);
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult6 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();

191
test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
View File

@ -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<storm::models::sparse::Model<double>> 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<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
@ -22,66 +26,58 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("two");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
auto minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("Pmin=? [F \"two\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*minProbabilityOperatorFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0277777612209320068, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
auto maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
result = checker.check(*maxProbabilityOperatorFormula);
formula = parser.parseFromString("Pmax=? [F \"two\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("three");
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
formula = parser.parseFromString("Pmin=? [F \"three\"]");
result = checker.check(*minProbabilityOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0555555224418640136, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision());
maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
formula = parser.parseFromString("Pmax=? [F \"three\"]");
result = checker.check(*maxProbabilityOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("four");
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
formula = parser.parseFromString("Pmin=? [F \"four\"]");
result = checker.check(*minProbabilityOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.083333283662796020508, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision());
maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
formula = parser.parseFromString("Pmax=? [F \"four\"]");
result = checker.check(*maxProbabilityOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done");
auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
auto minRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
formula = parser.parseFromString("Rmin=? [F \"done\"]");
result = checker.check(*minRewardOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult7 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(7.333329499, quantitativeResult7[0], storm::settings::nativeEquationSolverSettings().getPrecision());
auto maxRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
formula = parser.parseFromString("Rmax=? [F \"done\"]");
result = checker.check(*maxRewardOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult8 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(7.333329499, quantitativeResult8[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -94,18 +90,16 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateRewardModelChecker(*stateRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done");
reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
minRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
formula = parser.parseFromString("Rmin=? [F \"done\"]");
result = stateRewardModelChecker.check(*minRewardOperatorFormula);
result = stateRewardModelChecker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult9 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(7.333329499, quantitativeResult9[0], storm::settings::nativeEquationSolverSettings().getPrecision());
maxRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
formula = parser.parseFromString("Rmax=? [F \"done\"]");
result = stateRewardModelChecker.check(*maxRewardOperatorFormula);
result = stateRewardModelChecker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult10 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(7.333329499, quantitativeResult10[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -118,18 +112,16 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done");
reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
minRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
formula = parser.parseFromString("Rmin=? [F \"done\"]");
result = stateAndTransitionRewardModelChecker.check(*minRewardOperatorFormula);
result = stateAndTransitionRewardModelChecker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult11 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(14.666658998, quantitativeResult11[0], storm::settings::nativeEquationSolverSettings().getPrecision());
maxRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
formula = parser.parseFromString("Rmax=? [F \"done\"]");
result = stateAndTransitionRewardModelChecker.check(*maxRewardOperatorFormula);
result = stateAndTransitionRewardModelChecker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult12 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(14.666658998, quantitativeResult12[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -138,6 +130,9 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
std::shared_ptr<storm::models::sparse::Model<double>> 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<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
@ -147,51 +142,44 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
auto minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("Pmin=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*minProbabilityOperatorFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
auto maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
formula = parser.parseFromString("Pmax=? [F \"elected\"]");
result = checker.check(*maxProbabilityOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto trueFormula = std::make_shared<storm::logic::BooleanLiteralFormula>(true);
auto boundedUntilFormula = std::make_shared<storm::logic::BoundedUntilFormula>(trueFormula, labelFormula, 25);
minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, boundedUntilFormula);
formula = parser.parseFromString("Pmin=? [F<=25 \"elected\"]");
result = checker.check(*minProbabilityOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0625, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision());
maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, boundedUntilFormula);
formula = parser.parseFromString("Pmax=? [F<=25 \"elected\"]");
result = checker.check(*maxProbabilityOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0625, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
auto minRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
formula = parser.parseFromString("Rmin=? [F \"elected\"]");
result = checker.check(*minRewardOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(4.285689611, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision());
auto maxRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
formula = parser.parseFromString("Rmax=? [F \"elected\"]");
result = checker.check(*maxRewardOperatorFormula);
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(4.285689611, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -200,7 +188,10 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
storm::storage::SparseMatrixBuilder<double> matrixBuilder;
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp;
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
{
matrixBuilder = storm::storage::SparseMatrixBuilder<double>(2, 2, 2);
matrixBuilder.addNextValue(0, 1, 1.);
@ -215,18 +206,17 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("a");
auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(storm::logic::OptimalityType::Maximize, labelFormula);
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("LRAmax=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*lraFormula));
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(.5, quantitativeResult1[1], storm::settings::nativeEquationSolverSettings().getPrecision());
lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(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<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(.5, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -248,18 +238,17 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("a");
auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(storm::logic::OptimalityType::Maximize, labelFormula);
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("LRAmax=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*lraFormula));
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(.5, quantitativeResult1[1], storm::settings::nativeEquationSolverSettings().getPrecision());
lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(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<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(.5, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -290,57 +279,54 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("a");
auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(storm::logic::OptimalityType::Maximize, labelFormula);
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("LRAmax=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*lraFormula));
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
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::LongRunAverageOperatorFormula>(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<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
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<storm::logic::AtomicLabelFormula>("b");
lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(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<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
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::LongRunAverageOperatorFormula>(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<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
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<storm::logic::AtomicLabelFormula>("c");
lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(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<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
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::LongRunAverageOperatorFormula>(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<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.5, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -353,6 +339,9 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {
storm::storage::SparseMatrixBuilder<double> matrixBuilder;
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp;
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
{
matrixBuilder = storm::storage::SparseMatrixBuilder<double>(4, 3, 4, true, true, 3);
matrixBuilder.newRowGroup(0);
@ -376,57 +365,54 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("a");
auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(storm::logic::OptimalityType::Maximize, labelFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*lraFormula));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("LRAmax=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
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::LongRunAverageOperatorFormula>(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<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
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<storm::logic::AtomicLabelFormula>("b");
lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(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<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
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::LongRunAverageOperatorFormula>(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<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
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<storm::logic::AtomicLabelFormula>("c");
lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(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<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
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::LongRunAverageOperatorFormula>(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<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -501,10 +487,9 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("a");
auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(storm::logic::OptimalityType::Maximize, labelFormula);
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("LRAmax=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*lraFormula));
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
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::LongRunAverageOperatorFormula>(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<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.3 / 3., quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());

6
test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
View File

@ -22,8 +22,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die) {
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
options.buildRewards = true;
options.rewardModelName = "coin_flips";
options.rewardModelsToBuild.insert("coin_flips");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::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<storm::dd::DdType::CUDD>::Options options;
#endif
options.buildRewards = true;
options.rewardModelName = "num_rounds";
options.rewardModelsToBuild.insert("num_rounds");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
EXPECT_EQ(273ul, model->getNumberOfStates());
EXPECT_EQ(397ul, model->getNumberOfTransitions());

248
test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp
View File

@ -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<storm::models::sparse::Mdp<double>> 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<storm::models::sparse::Mdp<double>>();
// 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<double> mc(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> mc(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>()));
//storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("two");
auto apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("two");
//storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(apFormula);
//storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
auto probabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("Pmin=? [F \"two\"]");
//std::vector<double> result = mc.checkNoBoundOperator(*probFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = mc.check(*probabilityOperatorFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = mc.check(*formula);
//ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 0.0277777612209320068),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
ASSERT_NEAR(0.0277777612209320068, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
//delete probFormula;
probabilityOperatorFormula.reset();
//apFormula = new storm::property::prctl::Ap<double>("two");
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("two");
//eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(apFormula);
//probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
probabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(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<double>()[0] - 0.0277777612209320068),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
ASSERT_NEAR(0.0277777612209320068, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
//delete probFormula;
probabilityOperatorFormula.reset();
// ---------------- test ap "three" ----------------
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("three");
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(apFormula);
probabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(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<double>()[0] - 0.0555555224418640136),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
probabilityOperatorFormula.reset();
ASSERT_NEAR(0.0555555224418640136, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("three");
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(apFormula);
probabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(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<double>()[0] - 0.0555555224418640136),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
ASSERT_NEAR(0.0555555224418640136, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
probabilityOperatorFormula.reset();
formula = parser.parseFromString("Pmin=? [F \"four\"]");
// ---------------- test ap "four" ----------------
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("four");
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(apFormula);
probabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
result = mc.check(*formula);
result = mc.check(*probabilityOperatorFormula);
ASSERT_NEAR(0.083333283662796020508, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 0.083333283662796020508),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
probabilityOperatorFormula.reset();
formula = parser.parseFromString("Pmax=? [F \"four\"]");
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("four");
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(apFormula);
probabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
result = mc.check(*formula);
result = mc.check(*probabilityOperatorFormula);
ASSERT_NEAR(0.083333283662796020508, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 0.083333283662796020508),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Rmin=? [F \"done\"]");
probabilityOperatorFormula.reset();
// ---------------- test ap "done" ----------------
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done");
auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(apFormula);
auto rewardFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
result = mc.check(*rewardFormula);
result = mc.check(*formula);
#ifdef STORM_HAVE_CUDA
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 7.333329499),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
ASSERT_NEAR(7.333329499, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
#else
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 7.33332904),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
ASSERT_NEAR(7.33332904, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
#endif
rewardFormula.reset();
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done");
reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(apFormula);
rewardFormula = std::make_shared<storm::logic::RewardOperatorFormula>(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<double>()[0] - 7.333329499),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
ASSERT_NEAR(7.333329499, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
#else
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 7.33333151),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
ASSERT_NEAR(7.33333151, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
#endif
rewardFormula.reset();
// ------------- state rewards --------------
std::shared_ptr<storm::models::sparse::Mdp<double>> 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::models::sparse::Mdp<double>>();
storm::modelchecker::SparseMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateRewardModelChecker(*stateRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>()));
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done");
reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(apFormula);
rewardFormula = std::make_shared<storm::logic::RewardOperatorFormula>(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<double>()[0] - 7.333329499),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
ASSERT_NEAR(7.333329499, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
#else
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 7.33332904),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
ASSERT_NEAR(7.33332904, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
#endif
rewardFormula.reset();
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done");
reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(apFormula);
rewardFormula = std::make_shared<storm::logic::RewardOperatorFormula>(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<double>()[0] - 7.333329499),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
ASSERT_NEAR(7.333329499, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
#else
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 7.33333151),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
ASSERT_NEAR(7.33333151, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
#endif
rewardFormula.reset();
// -------------------------------- state and transition reward ------------------------
std::shared_ptr<storm::models::sparse::Mdp<double>> 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::models::sparse::Mdp<double>>();
storm::modelchecker::SparseMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>()));
formula = parser.parseFromString("Rmin=? [F \"done\"]");
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done");
reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(apFormula);
rewardFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
result = stateAndTransitionRewardModelChecker.check(*rewardFormula);
result = stateAndTransitionRewardModelChecker.check(*formula);
#ifdef STORM_HAVE_CUDA
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 14.666658998),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
ASSERT_NEAR(14.666658998, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
#else
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 14.6666581),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
ASSERT_NEAR(14.6666581, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
#endif
rewardFormula.reset();
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done");
reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(apFormula);
rewardFormula = std::make_shared<storm::logic::RewardOperatorFormula>(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<double>()[0] - 14.666658998),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
ASSERT_NEAR(14.666658998, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
#else
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 14.666663),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
ASSERT_NEAR(14.666663, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
#endif
rewardFormula.reset();
}
TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) {
std::shared_ptr<storm::models::sparse::Mdp<double>> 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<storm::models::sparse::Mdp<double>>();
// 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<double> mc(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> mc(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>()));
auto apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(apFormula);
auto probabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("Pmin=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = mc.check(*probabilityOperatorFormula);
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 1),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
probabilityOperatorFormula.reset();
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(apFormula);
probabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
result = mc.check(*probabilityOperatorFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = mc.check(*formula);
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 1),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
probabilityOperatorFormula.reset();
formula = parser.parseFromString("Pmax=? [F \"elected\"]");
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto boundedEventuallyFormula = std::make_shared<storm::logic::BoundedUntilFormula>(std::make_shared<storm::logic::BooleanLiteralFormula>(true), apFormula, 25);
probabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, boundedEventuallyFormula);
result = mc.check(*formula);
result = mc.check(*probabilityOperatorFormula);
ASSERT_NEAR(1, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 0.0625),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmax=? [F<=25 \"elected\"]");
probabilityOperatorFormula.reset();
result = mc.check(*formula);
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
boundedEventuallyFormula = std::make_shared<storm::logic::BoundedUntilFormula>(std::make_shared<storm::logic::BooleanLiteralFormula>(true), apFormula, 25);
probabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, boundedEventuallyFormula);
ASSERT_NEAR(0.0625, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
result = mc.check(*probabilityOperatorFormula);
formula = parser.parseFromString("Pmin=? [F<=25 \"elected\"]");
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 0.0625),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
result = mc.check(*formula);
probabilityOperatorFormula.reset();
ASSERT_NEAR(0.0625, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(apFormula);
auto rewardFormula = std::make_shared<storm::logic::RewardOperatorFormula>(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<double>()[0] - 4.285689611),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
ASSERT_NEAR(4.285689611, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
#else
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 4.285701547),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
ASSERT_NEAR(4.285701547, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
#endif
probabilityOperatorFormula.reset();
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(apFormula);
rewardFormula = std::make_shared<storm::logic::RewardOperatorFormula>(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<double>()[0] - 4.285689611),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
ASSERT_NEAR(4.285689611, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
#else
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 4.285703591),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
ASSERT_NEAR(4.285703591, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
#endif
probabilityOperatorFormula.reset();
}

3
test/functional/parser/AutoParserTest.cpp
View File

@ -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) {

32
test/functional/parser/DeterministicModelParserTest.cpp
View File

@ -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);
}

10
test/functional/parser/MarkovAutomatonParserTest.cpp
View File

@ -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) {

18
test/functional/parser/NondeterministicModelParserTest.cpp
View File

@ -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);
}

Write Preview
Loading…
Cancel
Save