Storm 1.11.1.1
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 std::unique_ptr<storm::modelchecker::CheckResult> result;
39
40 result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[0], true));
41 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
42 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("0")),
43 result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
44
45 result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[1], true));
46 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
47 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("1/8")),
48 result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
49
50 result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[2], true));
51 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
52 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("21/128")),
53 result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
54}
55
56TEST_F(SparseDtmcMultiDimensionalRewardUnfoldingTest, cost_bounded_leader) {
57 storm::Environment env;
58 std::string programFile = STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm";
59 std::string formulasAsString = "P=? [ F{\"num_rounds\"}<=1 \"elected\" ] ";
60 formulasAsString += "; P=? [ F{\"num_rounds\"}<=2 \"elected\" ] ";
61 formulasAsString += "; P=? [ F{\"num_rounds\"}>2 \"elected\" ] ";
62 formulasAsString += "; P=? [ F{\"num_rounds\"}>=2,{\"num_rounds\"}<3 \"elected\" ] ";
63
64 // programm, model, formula
65 storm::prism::Program program = storm::api::parseProgram(programFile);
66 program = storm::utility::prism::preprocess(program, "");
67 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
68 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
69 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalNumber>> dtmc =
70 storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalNumber>>();
71 uint_fast64_t const initState = *dtmc->getInitialStates().begin();
72 std::unique_ptr<storm::modelchecker::CheckResult> result;
73
74 result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[0], true));
75 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
76 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("24/25")),
77 result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
78
79 result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[1], true));
80 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
81 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("624/625")),
82 result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
83
84 result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[2], true));
85 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
86 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("1/625")),
87 result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
88
89 result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[3], true));
90 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
91 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("24/625")),
92 result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
93}
94
95TEST_F(SparseDtmcMultiDimensionalRewardUnfoldingTest, cost_bounded_crowds) {
96 storm::Environment env;
97 std::string programFile = STORM_TEST_RESOURCES_DIR "/dtmc/crowds_cost_bounded.pm";
98 std::string formulasAsString = "P=? [F{\"num_runs\"}<=3,{\"observe0\"}>1 true]";
99 formulasAsString += "; P=? [F{\"num_runs\"}<=3,{\"observe1\"}>1 true]";
100 formulasAsString += "; R{\"observe0\"}=? [C{\"num_runs\"}<=3]";
101
102 // programm, model, formula
103 storm::prism::Program program = storm::api::parseProgram(programFile);
104 program = storm::utility::prism::preprocess(program, "CrowdSize=4");
105 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
106 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
107 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalNumber>> dtmc =
108 storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalNumber>>();
109 uint_fast64_t const initState = *dtmc->getInitialStates().begin();
110 std::unique_ptr<storm::modelchecker::CheckResult> result;
111
112 result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[0], true));
113 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
114 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("78686542099694893/1268858272000000000")),
115 result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
116
117 result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[1], true));
118 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
119 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("13433618626105041/1268858272000000000")),
120 result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
121
122 result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[2], true));
123 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
124 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("620529/1364000")),
125 result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
126}
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:13
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:739
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:93
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