Storm 1.13.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
AddUncertaintyTest.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-parsers/parser/PrismParser.h"
6#include "storm/adapters/RationalNumberForward.h"
7#include "storm/api/storm.h"
8#include "storm/transformer/AddUncertainty.h"
9
10TEST(AddUncertaintyTransformerTest, BrpTest) {
11#ifndef STORM_HAVE_Z3
12 GTEST_SKIP() << "Z3 not available.";
13#endif
14 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/brp-16-2.pm");
15 std::string formulasString = "P=? [ F \"target\"]";
16 auto formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasString, program));
17 auto model = storm::api::buildSparseModel<double>(program, formulas);
18
19 auto transformer = storm::transformer::AddUncertainty(model);
20 auto uncertainModel = transformer.transform(0.01);
21 EXPECT_EQ(uncertainModel->getNumberOfStates(), model->getNumberOfStates());
22 EXPECT_EQ(uncertainModel->getNumberOfTransitions(), model->getNumberOfTransitions());
23 EXPECT_TRUE(uncertainModel->hasUncertainty());
24}
25
26TEST(AddUncertaintyTransformerTest, Coin22Test) {
27#ifndef STORM_HAVE_Z3
28 GTEST_SKIP() << "Z3 not available.";
29#endif
30 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm");
31 std::string formulasString = "Pmax=? [ F \"all_coins_equal_1\"]";
32 auto formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasString, program));
33 auto model = storm::api::buildSparseModel<double>(program, formulas);
34
35 auto transformer = storm::transformer::AddUncertainty(model);
36 auto uncertainModel = transformer.transform(0.01);
37 EXPECT_EQ(uncertainModel->getNumberOfStates(), model->getNumberOfStates());
38 EXPECT_EQ(uncertainModel->getNumberOfTransitions(), model->getNumberOfTransitions());
39 EXPECT_TRUE(uncertainModel->hasUncertainty());
40}
41
42TEST(AddUncertaintyTransformerTest, BrpTestRational) {
43#ifndef STORM_HAVE_Z3
44 GTEST_SKIP() << "Z3 not available.";
45#endif
46 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/brp-16-2.pm");
47 std::string formulasString = "P=? [ F \"target\"]";
48 auto formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasString, program));
49 auto model = storm::api::buildSparseModel<storm::RationalNumber>(program, formulas);
50
51 auto transformer = storm::transformer::AddUncertainty<storm::RationalNumber>(model);
52 auto uncertainModel = transformer.transform(storm::RationalNumber("1/100"));
53 EXPECT_EQ(uncertainModel->getNumberOfStates(), model->getNumberOfStates());
54 EXPECT_EQ(uncertainModel->getNumberOfTransitions(), model->getNumberOfTransitions());
55 EXPECT_TRUE(uncertainModel->hasUncertainty());
56}
57
58TEST(AddUncertaintyTransformerTest, Coin22TestRational) {
59#ifndef STORM_HAVE_Z3
60 GTEST_SKIP() << "Z3 not available.";
61#endif
62 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm");
63 std::string formulasString = "Pmax=? [ F \"all_coins_equal_1\"]";
64 auto formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasString, program));
65 auto model = storm::api::buildSparseModel<storm::RationalNumber>(program, formulas);
66
67 auto transformer = storm::transformer::AddUncertainty<storm::RationalNumber>(model);
68 auto uncertainModel = transformer.transform(storm::RationalNumber("1/100"));
69 EXPECT_EQ(uncertainModel->getNumberOfStates(), model->getNumberOfStates());
70 EXPECT_EQ(uncertainModel->getNumberOfTransitions(), model->getNumberOfTransitions());
71 EXPECT_TRUE(uncertainModel->hasUncertainty());
72}
TEST
TEST(AddUncertaintyTransformerTest, BrpTest)
Definition AddUncertaintyTest.cpp:10
storm::parser::PrismParser::parse
static storm::prism::Program parse(std::string const &filename, bool prismCompatability=false)
Parses the given file into the PRISM storage classes assuming it complies with the PRISM syntax.
Definition PrismParser.cpp:5
storm::transformer::AddUncertainty
This class is a convenience transformer to add uncertainty.
Definition AddUncertainty.h:23
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::buildSparseModel
std::shared_ptr< storm::models::sparse::Model< ValueType > > buildSparseModel(storm::storage::SymbolicModelDescription const &model, storm::builder::BuilderOptions const &options)
Definition builder.h:109
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_gtest.h