Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
JaniModelTest.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/utility/solver.h"
6
7#include "storm/storage/jani/Model.h"
8
9#ifdef STORM_HAVE_MSAT
10TEST(JaniModelTest, FlattenComposition) {
11 storm::prism::Program program;
12 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm"));
13 storm::jani::Model janiModel = program.toJani();
14
15 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
16
17 janiModel.substituteFunctions();
18 ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
19 EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
20 EXPECT_EQ(74ull, janiModel.getAutomaton(0).getNumberOfEdges());
21}
22
23TEST(JaniModelTest, FlattenComposition_Wlan_Mathsat) {
24 storm::prism::Program program;
25 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0_collide.nm"));
26 storm::jani::Model janiModel = program.toJani();
27
28 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
29
30 janiModel.substituteFunctions();
31 ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
32 EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
33 EXPECT_EQ(179ull, janiModel.getAutomaton(0).getNumberOfEdges());
34}
35
36TEST(JaniModelTest, FlattenComposition_Csma_Mathsat) {
37 storm::prism::Program program;
38 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2_2.nm"));
39 storm::jani::Model janiModel = program.toJani();
40
41 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
42
43 janiModel.substituteFunctions();
44 ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
45 EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
46 EXPECT_EQ(70ull, janiModel.getAutomaton(0).getNumberOfEdges());
47}
48
49TEST(JaniModelTest, FlattenComposition_Firewire_Mathsat) {
50 storm::prism::Program program;
51 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/firewire.nm"));
52 storm::jani::Model janiModel = program.toJani();
53
54 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
55
56 janiModel.substituteFunctions();
57 ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
58 EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
59 EXPECT_EQ(5024ull, janiModel.getAutomaton(0).getNumberOfEdges());
60}
61
62TEST(JaniModelTest, FlattenComposition_Coin_Mathsat) {
63 storm::prism::Program program;
64 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2.nm"));
65 storm::jani::Model janiModel = program.toJani();
66
67 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
68
69 janiModel.substituteFunctions();
70 ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
71 EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
72 EXPECT_EQ(13ull, janiModel.getAutomaton(0).getNumberOfEdges());
73}
74
75TEST(JaniModelTest, FlattenComposition_Dice_Mathsat) {
76 storm::prism::Program program;
77 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"));
78 storm::jani::Model janiModel = program.toJani();
79
80 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
81
82 janiModel.substituteFunctions();
83 ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
84 EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
85 EXPECT_EQ(16ull, janiModel.getAutomaton(0).getNumberOfEdges());
86}
87#endif
88
89#ifdef STORM_HAVE_Z3
90TEST(JaniModelTest, FlattenComposition_Leader_Z3) {
91 storm::prism::Program program;
92 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm"));
93 storm::jani::Model janiModel = program.toJani();
94
95 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
96
97 janiModel.substituteFunctions();
98 ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
99 EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
100 EXPECT_EQ(74ull, janiModel.getAutomaton(0).getNumberOfEdges());
101}
102
103TEST(JaniModelTest, FlattenComposition_Wlan_Z3) {
104 storm::prism::Program program;
105 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0_collide.nm"));
106 storm::jani::Model janiModel = program.toJani();
107
108 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
109
110 janiModel.substituteFunctions();
111 ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
112 EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
113 EXPECT_EQ(179ull, janiModel.getAutomaton(0).getNumberOfEdges());
114}
115
116TEST(JaniModelTest, FlattenComposition_Csma_Z3) {
117 storm::prism::Program program;
118 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2_2.nm"));
119 storm::jani::Model janiModel = program.toJani();
120
121 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
122
123 janiModel.substituteFunctions();
124 ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
125 EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
126 EXPECT_EQ(70ull, janiModel.getAutomaton(0).getNumberOfEdges());
127}
128
129TEST(JaniModelTest, FlattenComposition_Firewire_Z3) {
130 storm::prism::Program program;
131 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/firewire.nm"));
132 storm::jani::Model janiModel = program.toJani();
133
134 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
135
136 janiModel.substituteFunctions();
137 ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
138 EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
139 EXPECT_EQ(5024ull, janiModel.getAutomaton(0).getNumberOfEdges());
140}
141
142TEST(JaniModelTest, FlattenComposition_Coin_Z3) {
143 storm::prism::Program program;
144 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2.nm"));
145 storm::jani::Model janiModel = program.toJani();
146
147 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
148
149 janiModel.substituteFunctions();
150 ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
151 EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
152 EXPECT_EQ(13ull, janiModel.getAutomaton(0).getNumberOfEdges());
153}
154
155TEST(JaniModelTest, FlattenComposition_Dice_Z3) {
156 storm::prism::Program program;
157 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"));
158 storm::jani::Model janiModel = program.toJani();
159
160 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
161
162 janiModel.substituteFunctions();
163 ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
164 EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
165 EXPECT_EQ(16ull, janiModel.getAutomaton(0).getNumberOfEdges());
166}
167#endif
TEST
TEST(OrderTest, Simple)
Definition OrderTest.cpp:8
storm::jani::Automaton::getNumberOfEdges
uint64_t getNumberOfEdges() const
Retrieves the number of edges.
Definition Automaton.cpp:328
storm::jani::Model::substituteFunctions
void substituteFunctions()
Substitutes all function calls with the corresponding function definition.
Definition Model.cpp:1210
storm::jani::Model::flattenComposition
Model flattenComposition(std::shared_ptr< storm::utility::solver::SmtSolverFactory > const &smtSolverFactory=std::make_shared< storm::utility::solver::SmtSolverFactory >()) const
Flatten the composition to obtain an equivalent model that contains exactly one automaton that has th...
Definition Model.cpp:442
storm::jani::Model::getNumberOfAutomata
std::size_t getNumberOfAutomata() const
Retrieves the number of automata in this model.
Definition Model.cpp:914
storm::jani::Model::getAutomaton
Automaton & getAutomaton(std::string const &name)
Retrieves the automaton with the given name.
Definition Model.cpp:888
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::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