Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SparseDtmcMultiDimensionalRewardUnfoldingTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#include "storm-parsers/api/storm-parsers.h"
5#include "storm/api/storm.h"
6#include "storm/environment/Environment.h"
7#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
8#include "storm/models/sparse/Dtmc.h"
9#include "storm/settings/SettingsManager.h"
10#include "storm/settings/modules/GeneralSettings.h"
11#include "storm/storage/jani/Property.h"
12#include "storm/utility/constants.h"
13
14class SparseDtmcMultiDimensionalRewardUnfoldingTest : public ::testing::Test {
15 protected:
16 void SetUp() override {
17#ifndef STORM_HAVE_Z3
18 GTEST_SKIP() << "Z3 not available.";
19#endif
20 }
21};
22
23TEST_F(SparseDtmcMultiDimensionalRewardUnfoldingTest, cost_bounded_die) {
24 storm::Environment env;
25 std::string programFile = STORM_TEST_RESOURCES_DIR "/dtmc/die.pm";
26 std::string formulasAsString = "P=? [ F{\"coin_flips\"}<=2 \"two\" ] ";
27 formulasAsString += "; P=? [ F{\"coin_flips\"}<=3 \"two\" ] ";
28 formulasAsString += "; P=? [ F{\"coin_flips\"}<=8 \"two\" ] ";
29
30 // programm, model, formula
31 storm::prism::Program program = storm::api::parseProgram(programFile);
32 program = storm::utility::prism::preprocess(program, "");
33 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
34 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
35 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalNumber>> dtmc =
36 storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalNumber>>();
37 uint_fast64_t const initState = *dtmc->getInitialStates().begin();
38 ;
39 std::unique_ptr<storm::modelchecker::CheckResult> result;
40
41 result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[0], true));
42 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
43 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("0")),
44 result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
45
46 result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[1], true));
47 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
48 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("1/8")),
49 result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
50
51 result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[2], true));
52 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
53 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("21/128")),
54 result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
55}
56
57TEST_F(SparseDtmcMultiDimensionalRewardUnfoldingTest, cost_bounded_leader) {
58 storm::Environment env;
59 std::string programFile = STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm";
60 std::string formulasAsString = "P=? [ F{\"num_rounds\"}<=1 \"elected\" ] ";
61 formulasAsString += "; P=? [ F{\"num_rounds\"}<=2 \"elected\" ] ";
62 formulasAsString += "; P=? [ F{\"num_rounds\"}>2 \"elected\" ] ";
63 formulasAsString += "; P=? [ F{\"num_rounds\"}>=2,{\"num_rounds\"}<3 \"elected\" ] ";
64
65 // programm, model, formula
66 storm::prism::Program program = storm::api::parseProgram(programFile);
67 program = storm::utility::prism::preprocess(program, "");
68 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
69 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
70 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalNumber>> dtmc =
71 storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalNumber>>();
72 uint_fast64_t const initState = *dtmc->getInitialStates().begin();
73 ;
74 std::unique_ptr<storm::modelchecker::CheckResult> result;
75
76 result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[0], true));
77 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
78 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("24/25")),
79 result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
80
81 result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[1], true));
82 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
83 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("624/625")),
84 result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
85
86 result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[2], true));
87 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
88 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("1/625")),
89 result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
90
91 result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[3], true));
92 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
93 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("24/625")),
94 result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
95}
96
97TEST_F(SparseDtmcMultiDimensionalRewardUnfoldingTest, cost_bounded_crowds) {
98 storm::Environment env;
99 std::string programFile = STORM_TEST_RESOURCES_DIR "/dtmc/crowds_cost_bounded.pm";
100 std::string formulasAsString = "P=? [F{\"num_runs\"}<=3,{\"observe0\"}>1 true]";
101 formulasAsString += "; P=? [F{\"num_runs\"}<=3,{\"observe1\"}>1 true]";
102 formulasAsString += "; R{\"observe0\"}=? [C{\"num_runs\"}<=3]";
103
104 // programm, model, formula
105 storm::prism::Program program = storm::api::parseProgram(programFile);
106 program = storm::utility::prism::preprocess(program, "CrowdSize=4");
107 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
108 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
109 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalNumber>> dtmc =
110 storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalNumber>>();
111 uint_fast64_t const initState = *dtmc->getInitialStates().begin();
112 ;
113 std::unique_ptr<storm::modelchecker::CheckResult> result;
114
115 result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[0], true));
116 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
117 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("78686542099694893/1268858272000000000")),
118 result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
119
120 result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[1], true));
121 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
122 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("13433618626105041/1268858272000000000")),
123 result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
124
125 result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[2], true));
126 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
127 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("620529/1364000")),
128 result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
129}
TEST_F
TEST_F(SparseDtmcMultiDimensionalRewardUnfoldingTest, cost_bounded_die)
Definition SparseDtmcMultiDimensionalRewardUnfoldingTest.cpp:23
storm::models::sparse::Dtmc
This class represents a discrete-time Markov chain.
Definition Dtmc.h:14
storm::models::sparse::Model::getInitialStates
storm::storage::BitVector const & getInitialStates() const
Retrieves the initial states of the model.
Definition Model.cpp:177
storm::storage::BitVector::begin
const_iterator begin() const
Returns an iterator to the indices of the set bits in the bit vector.
Definition BitVector.cpp:782
storm::api::parsePropertiesForPrismProgram
std::vector< storm::jani::Property > parsePropertiesForPrismProgram(std::string const &inputString, storm::prism::Program const &program, boost::optional< std::set< std::string > > const &propertyFilter)
Definition properties.cpp:69
storm::api::parseProgram
storm::prism::Program parseProgram(std::string const &filename, bool prismCompatibility, bool simplify)
Definition model_descriptions.cpp:17
storm::api::extractFormulasFromProperties
std::vector< std::shared_ptr< storm::logic::Formula const > > extractFormulasFromProperties(std::vector< storm::jani::Property > const &properties)
Definition properties.cpp:64
storm::api::verifyWithSparseEngine
std::unique_ptr< storm::modelchecker::CheckResult > verifyWithSparseEngine(storm::Environment const &env, std::shared_ptr< storm::models::sparse::Dtmc< ValueType > > const &dtmc, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
Definition verification.h:95
storm::utility::prism::preprocess
storm::prism::Program preprocess(storm::prism::Program const &program, std::map< storm::expressions::Variable, storm::expressions::Expression > const &constantDefinitions)
Definition prism.cpp:19
storm_gtest.h