Storm 1.11.1.1
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 "test/storm_gtest.h"
3
4#include "storm-parsers/parser/PrismParser.h"
5#include "storm/storage/jani/Model.h"
6#include "storm/utility/solver.h"
7
8#ifdef STORM_HAVE_MATHSAT
9TEST(JaniModelTest, FlattenComposition) {
10 storm::prism::Program program;
11 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm"));
12 storm::jani::Model janiModel = program.toJani();
13
14 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
15
16 janiModel.substituteFunctions();
17 ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
18 EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
19 EXPECT_EQ(74ull, janiModel.getAutomaton(0).getNumberOfEdges());
20}
21
22TEST(JaniModelTest, FlattenComposition_Wlan_Mathsat) {
23 storm::prism::Program program;
24 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0_collide.nm"));
25 storm::jani::Model janiModel = program.toJani();
26
27 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
28
29 janiModel.substituteFunctions();
30 ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
31 EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
32 EXPECT_EQ(179ull, janiModel.getAutomaton(0).getNumberOfEdges());
33}
34
35TEST(JaniModelTest, FlattenComposition_Csma_Mathsat) {
36 storm::prism::Program program;
37 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2_2.nm"));
38 storm::jani::Model janiModel = program.toJani();
39
40 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
41
42 janiModel.substituteFunctions();
43 ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
44 EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
45 EXPECT_EQ(70ull, janiModel.getAutomaton(0).getNumberOfEdges());
46}
47
48TEST(JaniModelTest, FlattenComposition_Firewire_Mathsat) {
49 storm::prism::Program program;
50 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/firewire.nm"));
51 storm::jani::Model janiModel = program.toJani();
52
53 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
54
55 janiModel.substituteFunctions();
56 ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
57 EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
58 EXPECT_EQ(5024ull, janiModel.getAutomaton(0).getNumberOfEdges());
59}
60
61TEST(JaniModelTest, FlattenComposition_Coin_Mathsat) {
62 storm::prism::Program program;
63 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2.nm"));
64 storm::jani::Model janiModel = program.toJani();
65
66 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
67
68 janiModel.substituteFunctions();
69 ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
70 EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
71 EXPECT_EQ(13ull, janiModel.getAutomaton(0).getNumberOfEdges());
72}
73
74TEST(JaniModelTest, FlattenComposition_Dice_Mathsat) {
75 storm::prism::Program program;
76 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"));
77 storm::jani::Model janiModel = program.toJani();
78
79 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
80
81 janiModel.substituteFunctions();
82 ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
83 EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
84 EXPECT_EQ(16ull, janiModel.getAutomaton(0).getNumberOfEdges());
85}
86#endif
87
88#ifdef STORM_HAVE_Z3
89TEST(JaniModelTest, FlattenComposition_Leader_Z3) {
90 storm::prism::Program program;
91 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm"));
92 storm::jani::Model janiModel = program.toJani();
93
94 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
95
96 janiModel.substituteFunctions();
97 ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
98 EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
99 EXPECT_EQ(74ull, janiModel.getAutomaton(0).getNumberOfEdges());
100}
101
102TEST(JaniModelTest, FlattenComposition_Wlan_Z3) {
103 storm::prism::Program program;
104 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0_collide.nm"));
105 storm::jani::Model janiModel = program.toJani();
106
107 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
108
109 janiModel.substituteFunctions();
110 ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
111 EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
112 EXPECT_EQ(179ull, janiModel.getAutomaton(0).getNumberOfEdges());
113}
114
115TEST(JaniModelTest, FlattenComposition_Csma_Z3) {
116 storm::prism::Program program;
117 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2_2.nm"));
118 storm::jani::Model janiModel = program.toJani();
119
120 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
121
122 janiModel.substituteFunctions();
123 ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
124 EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
125 EXPECT_EQ(70ull, janiModel.getAutomaton(0).getNumberOfEdges());
126}
127
128TEST(JaniModelTest, FlattenComposition_Firewire_Z3) {
129 storm::prism::Program program;
130 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/firewire.nm"));
131 storm::jani::Model janiModel = program.toJani();
132
133 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
134
135 janiModel.substituteFunctions();
136 ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
137 EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
138 EXPECT_EQ(5024ull, janiModel.getAutomaton(0).getNumberOfEdges());
139}
140
141TEST(JaniModelTest, FlattenComposition_Coin_Z3) {
142 storm::prism::Program program;
143 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2.nm"));
144 storm::jani::Model janiModel = program.toJani();
145
146 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
147
148 janiModel.substituteFunctions();
149 ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
150 EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
151 EXPECT_EQ(13ull, janiModel.getAutomaton(0).getNumberOfEdges());
152}
153
154TEST(JaniModelTest, FlattenComposition_Dice_Z3) {
155 storm::prism::Program program;
156 ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"));
157 storm::jani::Model janiModel = program.toJani();
158
159 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
160
161 janiModel.substituteFunctions();
162 ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
163 EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
164 EXPECT_EQ(16ull, janiModel.getAutomaton(0).getNumberOfEdges());
165}
166#endif
TEST
TEST(OrderTest, Simple)
Definition OrderTest.cpp:15
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:2340
storm_gtest.h