Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
PrismProgramTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "storm-parsers/parser/PrismParser.h"
3#include "test/storm_gtest.h"
4
5#include "storm/storage/expressions/ExpressionManager.h"
6#include "storm/storage/jani/Model.h"
7#include "storm/utility/solver.h"
8
9#ifdef STORM_HAVE_MSAT
10TEST(PrismProgramTest, FlattenModules) {
11 storm::prism::Program program;
12 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm"));
13
14 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
15
16 ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory));
17 EXPECT_EQ(1ull, program.getNumberOfModules());
18 EXPECT_EQ(74ull, program.getModule(0).getNumberOfCommands());
19}
20
21TEST(PrismProgramTest, FlattenModules_Wlan_Mathsat) {
22 storm::prism::Program program;
23 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0_collide.nm"));
24
25 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
26
27 ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory));
28 EXPECT_EQ(1ull, program.getNumberOfModules());
29 EXPECT_EQ(179ull, program.getModule(0).getNumberOfCommands());
30}
31
32TEST(PrismProgramTest, FlattenModules_Csma_Mathsat) {
33 storm::prism::Program program;
34 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2_2.nm"));
35
36 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
37
38 ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory));
39 EXPECT_EQ(1ull, program.getNumberOfModules());
40 EXPECT_EQ(70ull, program.getModule(0).getNumberOfCommands());
41}
42
43TEST(PrismProgramTest, FlattenModules_Firewire_Mathsat) {
44 storm::prism::Program program;
45 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/firewire.nm"));
46
47 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
48
49 ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory));
50 EXPECT_EQ(1ull, program.getNumberOfModules());
51 EXPECT_EQ(5024ull, program.getModule(0).getNumberOfCommands());
52}
53
54TEST(PrismProgramTest, FlattenModules_Coin_Mathsat) {
55 storm::prism::Program program;
56 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2.nm"));
57
58 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
59
60 ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory));
61 EXPECT_EQ(1ull, program.getNumberOfModules());
62 EXPECT_EQ(13ull, program.getModule(0).getNumberOfCommands());
63}
64
65TEST(PrismProgramTest, FlattenModules_Dice_Mathsat) {
66 storm::prism::Program program;
67 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"));
68
69 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
70
71 ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory));
72 EXPECT_EQ(1ull, program.getNumberOfModules());
73 EXPECT_EQ(16ull, program.getModule(0).getNumberOfCommands());
74}
75#endif
76
77#ifdef STORM_HAVE_Z3
78TEST(PrismProgramTest, FlattenModules_Leader_Z3) {
79 storm::prism::Program program;
80 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm"));
81
82 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
83
84 ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory));
85 EXPECT_EQ(1ull, program.getNumberOfModules());
86 EXPECT_EQ(74ull, program.getModule(0).getNumberOfCommands());
87}
88
89TEST(PrismProgramTest, FlattenModules_Wlan_Z3) {
90 storm::prism::Program program;
91 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0_collide.nm"));
92
93 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
94
95 ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory));
96 EXPECT_EQ(1ull, program.getNumberOfModules());
97 EXPECT_EQ(179ull, program.getModule(0).getNumberOfCommands());
98}
99
100TEST(PrismProgramTest, FlattenModules_Csma_Z3) {
101 storm::prism::Program program;
102 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2_2.nm"));
103
104 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
105
106 ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory));
107 EXPECT_EQ(1ull, program.getNumberOfModules());
108 EXPECT_EQ(70ull, program.getModule(0).getNumberOfCommands());
109}
110
111TEST(PrismProgramTest, FlattenModules_Firewire_Z3) {
112 storm::prism::Program program;
113 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/firewire.nm"));
114
115 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
116
117 ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory));
118 EXPECT_EQ(1ull, program.getNumberOfModules());
119 EXPECT_EQ(5024ull, program.getModule(0).getNumberOfCommands());
120}
121
122TEST(PrismProgramTest, FlattenModules_Coin_Z3) {
123 storm::prism::Program program;
124 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2.nm"));
125
126 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
127
128 ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory));
129 EXPECT_EQ(1ull, program.getNumberOfModules());
130 EXPECT_EQ(13ull, program.getModule(0).getNumberOfCommands());
131}
132
133TEST(PrismProgramTest, FlattenModules_Dice_Z3) {
134 storm::prism::Program program;
135 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"));
136
137 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
138
139 ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory));
140 EXPECT_EQ(1ull, program.getNumberOfModules());
141 EXPECT_EQ(16ull, program.getModule(0).getNumberOfCommands());
142}
143#endif
144
145TEST(PrismProgramTest, ConvertToJani) {
146 storm::prism::Program prismProgram;
147 storm::jani::Model janiModel;
148
149 ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm"));
150 ASSERT_NO_THROW(janiModel = prismProgram.toJani());
151
152 ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0_collide.nm"));
153 ASSERT_NO_THROW(janiModel = prismProgram.toJani());
154
155 ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/brp-16-2.pm"));
156 ASSERT_NO_THROW(janiModel = prismProgram.toJani());
157
158 ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm"));
159 ASSERT_NO_THROW(janiModel = prismProgram.toJani());
160
161 ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm"));
162 ASSERT_NO_THROW(janiModel = prismProgram.toJani());
163
164 ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/nand-5-2.pm"));
165 ASSERT_NO_THROW(janiModel = prismProgram.toJani());
166
167 ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/unbounded.nm"));
168 ASSERT_NO_THROW(janiModel = prismProgram.toJani());
169}
170
171TEST(PrismProgramTest, ReplaceInitialStates) {
172 storm::prism::Program origPrismProgram;
173 storm::prism::Program transformedPrismProgram;
174 ASSERT_NO_THROW(origPrismProgram = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/brp-16-2.pm"));
175 ASSERT_NO_THROW(transformedPrismProgram = origPrismProgram.replaceVariableInitializationByInitExpression());
176 EXPECT_TRUE(origPrismProgram.getInitialStatesExpression().isSyntacticallyEqual(transformedPrismProgram.getInitialStatesExpression()));
177 EXPECT_TRUE(transformedPrismProgram.hasInitialConstruct());
178}
179
180TEST(PrismProgramTest, ReplaceConstantByVariable) {
181 storm::prism::Program origPrismProgram;
182 storm::prism::Program transformedPrismProgram;
183 ASSERT_NO_THROW(origPrismProgram = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-4-3.pm"));
184 ASSERT_NO_THROW(transformedPrismProgram = origPrismProgram.replaceConstantByVariable(
185 origPrismProgram.getConstant("CrowdSize"), origPrismProgram.getManager().integer(0), origPrismProgram.getManager().integer(20), true));
186 EXPECT_NO_THROW(transformedPrismProgram.getGlobalIntegerVariable("CrowdSize"));
187 EXPECT_FALSE(transformedPrismProgram.hasConstant("CrowdSize"));
188}
TEST
TEST(PrismProgramTest, ConvertToJani)
Definition PrismProgramTest.cpp:145
storm::expressions::Expression::isSyntacticallyEqual
bool isSyntacticallyEqual(storm::expressions::Expression const &other) const
Checks whether the two expressions are syntatically the same.
Definition Expression.cpp:216
storm::expressions::ExpressionManager::integer
Expression integer(int_fast64_t value) const
Creates an expression that characterizes the given integer literal.
Definition ExpressionManager.cpp:88
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::prism::Module::getNumberOfCommands
std::size_t getNumberOfCommands() const
Retrieves the number of commands of this module.
Definition Module.cpp:117
storm::prism::Program::replaceConstantByVariable
Program replaceConstantByVariable(Constant const &c, expressions::Expression const &lowerBound, expressions::Expression const &upperBound, bool observable=true) const
Substitutes the given constant by a fresh global variable that is bound between lowerBound and upperB...
Definition Program.cpp:1205
storm::prism::Program::getModule
Module const & getModule(uint_fast64_t index) const
Retrieves the module with the given index.
Definition Program.cpp:615
storm::prism::Program::getGlobalIntegerVariable
IntegerVariable const & getGlobalIntegerVariable(std::string const &variableName) const
Retrieves a the global integer variable with the given name.
Definition Program.cpp:543
storm::prism::Program::getConstant
Constant const & getConstant(std::string const &constantName) const
Retrieves the constant with the given name if it exists.
Definition Program.cpp:397
storm::prism::Program::substituteFormulas
Program substituteFormulas() const
Substitutes all formulas appearing in the expressions of the program by their defining expressions.
Definition Program.cpp:1030
storm::prism::Program::getManager
storm::expressions::ExpressionManager & getManager() const
Retrieves the manager responsible for the expressions of this program.
Definition Program.cpp:2359
storm::prism::Program::replaceVariableInitializationByInitExpression
Program replaceVariableInitializationByInitExpression() const
Replace the initialization in variables by an init-expression.
Definition Program.cpp:1184
storm::prism::Program::hasConstant
bool hasConstant(std::string const &constantName) const
Retrieves whether the given constant exists in the program.
Definition Program.cpp:393
storm::prism::Program::getInitialStatesExpression
storm::expressions::Expression getInitialStatesExpression() const
Retrieves an expression characterizing the initial states.
Definition Program.cpp:662
storm::prism::Program::getNumberOfModules
std::size_t getNumberOfModules() const
Retrieves the number of modules in the program.
Definition Program.cpp:611
storm::prism::Program::hasInitialConstruct
bool hasInitialConstruct() const
Retrieves whether the program specifies an initial construct.
Definition Program.cpp:645
storm::prism::Program::flattenModules
Program flattenModules(std::shared_ptr< storm::utility::solver::SmtSolverFactory > const &smtSolverFactory=std::shared_ptr< storm::utility::solver::SmtSolverFactory >(new storm::utility::solver::SmtSolverFactory())) const
Creates an equivalent program that contains exactly one module.
Definition Program.cpp:1951
storm::prism::Program::toJani
storm::jani::Model toJani(bool allVariablesGlobal=true, std::string suffix="") const
Converts the PRISM model into an equivalent JANI model.
Definition Program.cpp:2321
storm_gtest.h