Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
ExplicitJaniModelBuilderTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
4#include "storm/api/storm.h"
12#include "storm/utility/cli.h"
13#include "test/storm_gtest.h"
14
15namespace {
16
17storm::jani::Model getJaniModelFromPrism(std::string const& pathInTestResourcesDir, bool prismCompatability = false) {
19 storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/" + pathInTestResourcesDir, prismCompatability);
20 auto m = modelDescription.toJani().preprocess().asJaniModel();
22 EXPECT_TRUE(unsupportedFeatures.empty()) << "Model '" << pathInTestResourcesDir << "' uses unsupported feature(s) " << unsupportedFeatures.toString();
23 return m;
24}
25
26class ExplicitJaniModelBuilderTest : public ::testing::Test {
27 protected:
28 void SetUp() override {
29#ifndef STORM_HAVE_Z3
30 GTEST_SKIP() << "Z3 not available.";
31#endif
32 }
33};
34
35TEST_F(ExplicitJaniModelBuilderTest, Dtmc) {
36 auto janiModel = getJaniModelFromPrism("/dtmc/die.pm");
37
38 std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
39 EXPECT_EQ(13ul, model->getNumberOfStates());
40 EXPECT_EQ(20ul, model->getNumberOfTransitions());
41
42 janiModel = storm::api::parseJaniModel(STORM_TEST_RESOURCES_DIR "/dtmc/die_array.jani").first;
44 EXPECT_EQ(13ul, model->getNumberOfStates());
45 EXPECT_EQ(20ul, model->getNumberOfTransitions());
46
47 janiModel = storm::api::parseJaniModel(STORM_TEST_RESOURCES_DIR "/dtmc/die_array_nested.jani").first;
49 EXPECT_EQ(13ul, model->getNumberOfStates());
50 EXPECT_EQ(20ul, model->getNumberOfTransitions());
51
52 janiModel = getJaniModelFromPrism("/dtmc/brp-16-2.pm");
54 EXPECT_EQ(677ul, model->getNumberOfStates());
55 EXPECT_EQ(867ul, model->getNumberOfTransitions());
56
57 janiModel = getJaniModelFromPrism("/dtmc/crowds-5-5.pm");
59 EXPECT_EQ(8607ul, model->getNumberOfStates());
60 EXPECT_EQ(15113ul, model->getNumberOfTransitions());
61
62 janiModel = getJaniModelFromPrism("/dtmc/leader-3-5.pm");
64 EXPECT_EQ(273ul, model->getNumberOfStates());
65 EXPECT_EQ(397ul, model->getNumberOfTransitions());
66
67 janiModel = getJaniModelFromPrism("/dtmc/nand-5-2.pm");
69 EXPECT_EQ(1728ul, model->getNumberOfStates());
70 EXPECT_EQ(2505ul, model->getNumberOfTransitions());
71
72 janiModel = storm::api::parseJaniModel(STORM_TEST_RESOURCES_DIR "/dtmc/test_trigonometry.jani").first;
73 auto constants = storm::utility::cli::parseConstantDefinitionString(janiModel.getManager(), "step_size_rad=0.523599"); // step_size = 30 deg
74 janiModel = janiModel.defineUndefinedConstants(constants);
76 EXPECT_EQ(5ul, model->getNumberOfStates());
77 EXPECT_EQ(5ul, model->getNumberOfTransitions());
78}
79
80TEST_F(ExplicitJaniModelBuilderTest, pdtmc) {
81 auto janiModel = getJaniModelFromPrism("/pdtmc/parametric_die.pm");
82 std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model =
84 EXPECT_EQ(13ul, model->getNumberOfStates());
85 EXPECT_EQ(20ul, model->getNumberOfTransitions());
86
87 janiModel = storm::api::parseJaniModel(STORM_TEST_RESOURCES_DIR "/pdtmc/die_array_nested.jani").first;
88 janiModel.substituteConstantsFunctionsTranscendentals();
90 EXPECT_EQ(13ul, model->getNumberOfStates());
91 EXPECT_EQ(20ul, model->getNumberOfTransitions());
92
93 janiModel = getJaniModelFromPrism("/pdtmc/brp16_2.pm");
95 EXPECT_EQ(677ul, model->getNumberOfStates());
96 EXPECT_EQ(867ul, model->getNumberOfTransitions());
97}
98
99TEST_F(ExplicitJaniModelBuilderTest, Ctmc) {
100 auto janiModel = getJaniModelFromPrism("/ctmc/cluster2.sm", true);
101
102 std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
103 EXPECT_EQ(276ul, model->getNumberOfStates());
104 EXPECT_EQ(1120ul, model->getNumberOfTransitions());
105
106 janiModel = getJaniModelFromPrism("/ctmc/embedded2.sm", true);
108 EXPECT_EQ(3478ul, model->getNumberOfStates());
109 EXPECT_EQ(14639ul, model->getNumberOfTransitions());
110
111 janiModel = getJaniModelFromPrism("/ctmc/polling2.sm", true);
113 EXPECT_EQ(12ul, model->getNumberOfStates());
114 EXPECT_EQ(22ul, model->getNumberOfTransitions());
115
116 janiModel = getJaniModelFromPrism("/ctmc/fms2.sm", true);
118 EXPECT_EQ(810ul, model->getNumberOfStates());
119 EXPECT_EQ(3699ul, model->getNumberOfTransitions());
120
121 janiModel = getJaniModelFromPrism("/ctmc/tandem5.sm", true);
123 EXPECT_EQ(66ul, model->getNumberOfStates());
124 EXPECT_EQ(189ul, model->getNumberOfTransitions());
125}
126
127TEST_F(ExplicitJaniModelBuilderTest, Mdp) {
128 auto janiModel = getJaniModelFromPrism("/mdp/two_dice.nm");
129
130 std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
131 EXPECT_EQ(169ul, model->getNumberOfStates());
132 EXPECT_EQ(436ul, model->getNumberOfTransitions());
133
134 janiModel = getJaniModelFromPrism("/mdp/leader3.nm");
136 EXPECT_EQ(364ul, model->getNumberOfStates());
137 EXPECT_EQ(654ul, model->getNumberOfTransitions());
138
139 janiModel = getJaniModelFromPrism("/mdp/coin2-2.nm");
141 EXPECT_EQ(272ul, model->getNumberOfStates());
142 EXPECT_EQ(492ul, model->getNumberOfTransitions());
143
144 janiModel = getJaniModelFromPrism("/mdp/csma2-2.nm");
146 EXPECT_EQ(1038ul, model->getNumberOfStates());
147 EXPECT_EQ(1282ul, model->getNumberOfTransitions());
148
149 janiModel = getJaniModelFromPrism("/mdp/firewire3-0.5.nm");
151 EXPECT_EQ(4093ul, model->getNumberOfStates());
152 EXPECT_EQ(5585ul, model->getNumberOfTransitions());
153
154 janiModel = getJaniModelFromPrism("/mdp/wlan0-2-2.nm");
156 EXPECT_EQ(37ul, model->getNumberOfStates());
157 EXPECT_EQ(59ul, model->getNumberOfTransitions());
158
159 janiModel = getJaniModelFromPrism("/mdp/sync.nm");
161 EXPECT_EQ(5ul, model->getNumberOfStates());
162 EXPECT_EQ(24ul, model->getNumberOfTransitions());
163 EXPECT_EQ(12ul, model->getNumberOfChoices());
164}
165
166TEST_F(ExplicitJaniModelBuilderTest, Ma) {
167 auto janiModel = getJaniModelFromPrism("/ma/simple.ma");
168
169 std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
170 EXPECT_EQ(5ul, model->getNumberOfStates());
171 EXPECT_EQ(8ul, model->getNumberOfTransitions());
172 ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton));
174
175 janiModel = getJaniModelFromPrism("/ma/hybrid_states.ma");
177 EXPECT_EQ(5ul, model->getNumberOfStates());
178 EXPECT_EQ(13ul, model->getNumberOfTransitions());
179 ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton));
181
182 janiModel = getJaniModelFromPrism("/ma/stream2.ma");
184 EXPECT_EQ(12ul, model->getNumberOfStates());
185 EXPECT_EQ(14ul, model->getNumberOfTransitions());
186 ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton));
188
189 janiModel = storm::api::parseJaniModel(STORM_TEST_RESOURCES_DIR "/ma/ftwc.jani").first;
190 auto constants = storm::utility::cli::parseConstantDefinitionString(janiModel.getManager(), "N=2,TIME_BOUND=1");
191 janiModel = janiModel.defineUndefinedConstants(constants);
193 EXPECT_EQ(1536ul, model->getNumberOfStates());
194 EXPECT_EQ(6448ul, model->getNumberOfTransitions());
195 ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton));
197}
198
199TEST_F(ExplicitJaniModelBuilderTest, FailComposition) {
200 auto janiModel = getJaniModelFromPrism("/mdp/system_composition.nm");
201
202 STORM_SILENT_ASSERT_THROW(storm::builder::ExplicitModelBuilder<double>(janiModel).build(), storm::exceptions::WrongFormatException);
203}
204
205TEST_F(ExplicitJaniModelBuilderTest, unassignedVariables) {
206 storm::jani::Model janiModel = storm::api::parseJaniModel(STORM_TEST_RESOURCES_DIR "/mdp/unassigned-variables.jani").first;
207 std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
208 EXPECT_EQ(25ul, model->getNumberOfStates());
209 EXPECT_EQ(81ul, model->getNumberOfTransitions());
210}
211
212TEST_F(ExplicitJaniModelBuilderTest, enumerateInitial) {
213 storm::jani::Model janiModel = storm::api::parseJaniModel(STORM_TEST_RESOURCES_DIR "/mdp/enumerate_init.jani").first;
214 std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
215 EXPECT_EQ(94ul, model->getNumberOfStates());
216 EXPECT_EQ(145ul, model->getNumberOfTransitions());
217 EXPECT_EQ(72ul, model->getInitialStates().getNumberOfSetBits());
218}
219} // namespace
TEST_F(AssumptionCheckerTest, Brp_no_bisimulation)
std::shared_ptr< storm::models::sparse::Model< ValueType, RewardModelType > > build()
Convert the program given at construction time to an abstract model.
std::string toString() const
ModelFeatures restrictToFeatures(ModelFeatures const &modelFeatures)
Attempts to eliminate all features of this model that are not in the given set of features.
Definition Model.cpp:1243
This class represents a discrete-time Markov chain.
Definition Dtmc.h:14
This class represents a Markov automaton.
storm::storage::BitVector const & getMarkovianStates() const
Retrieves the set of Markovian states of the model.
This class represents a (discrete-time) Markov decision process.
Definition Mdp.h:14
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.
uint_fast64_t getNumberOfSetBits() const
Returns the number of bits that are set to true in this bit vector.
SymbolicModelDescription toJani(bool makeVariablesGlobal=true) const
storm::jani::Model const & asJaniModel() const
SymbolicModelDescription preprocess(std::string const &constantDefinitionString="") const
std::pair< storm::jani::Model, std::vector< storm::jani::Property > > parseJaniModel(std::string const &filename, boost::optional< std::vector< std::string > > const &propertyFilter)
std::map< storm::expressions::Variable, storm::expressions::Expression > parseConstantDefinitionString(storm::expressions::ExpressionManager const &manager, std::string const &constantDefinitionString)
Definition cli.cpp:18
#define STORM_SILENT_ASSERT_THROW(statement, expected_exception)
Definition storm_gtest.h:99