1#include "storm-config.h"
17storm::jani::Model getJaniModelFromPrism(std::string
const& pathInTestResourcesDir,
bool prismCompatability =
false) {
22 EXPECT_TRUE(unsupportedFeatures.empty()) <<
"Model '" << pathInTestResourcesDir <<
"' uses unsupported feature(s) " << unsupportedFeatures.
toString();
26class ExplicitJaniModelBuilderTest :
public ::testing::Test {
28 void SetUp()
override {
30 GTEST_SKIP() <<
"Z3 not available.";
36 auto janiModel = getJaniModelFromPrism(
"/dtmc/die.pm");
39 EXPECT_EQ(13ul, model->getNumberOfStates());
40 EXPECT_EQ(20ul, model->getNumberOfTransitions());
44 EXPECT_EQ(13ul, model->getNumberOfStates());
45 EXPECT_EQ(20ul, model->getNumberOfTransitions());
49 EXPECT_EQ(13ul, model->getNumberOfStates());
50 EXPECT_EQ(20ul, model->getNumberOfTransitions());
52 janiModel = getJaniModelFromPrism(
"/dtmc/brp-16-2.pm");
54 EXPECT_EQ(677ul, model->getNumberOfStates());
55 EXPECT_EQ(867ul, model->getNumberOfTransitions());
57 janiModel = getJaniModelFromPrism(
"/dtmc/crowds-5-5.pm");
59 EXPECT_EQ(8607ul, model->getNumberOfStates());
60 EXPECT_EQ(15113ul, model->getNumberOfTransitions());
62 janiModel = getJaniModelFromPrism(
"/dtmc/leader-3-5.pm");
64 EXPECT_EQ(273ul, model->getNumberOfStates());
65 EXPECT_EQ(397ul, model->getNumberOfTransitions());
67 janiModel = getJaniModelFromPrism(
"/dtmc/nand-5-2.pm");
69 EXPECT_EQ(1728ul, model->getNumberOfStates());
70 EXPECT_EQ(2505ul, model->getNumberOfTransitions());
74 janiModel = janiModel.defineUndefinedConstants(constants);
76 EXPECT_EQ(5ul, model->getNumberOfStates());
77 EXPECT_EQ(5ul, model->getNumberOfTransitions());
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());
88 janiModel.substituteConstantsFunctionsTranscendentals();
90 EXPECT_EQ(13ul, model->getNumberOfStates());
91 EXPECT_EQ(20ul, model->getNumberOfTransitions());
93 janiModel = getJaniModelFromPrism(
"/pdtmc/brp16_2.pm");
95 EXPECT_EQ(677ul, model->getNumberOfStates());
96 EXPECT_EQ(867ul, model->getNumberOfTransitions());
99TEST_F(ExplicitJaniModelBuilderTest, Ctmc) {
100 auto janiModel = getJaniModelFromPrism(
"/ctmc/cluster2.sm",
true);
103 EXPECT_EQ(276ul, model->getNumberOfStates());
104 EXPECT_EQ(1120ul, model->getNumberOfTransitions());
106 janiModel = getJaniModelFromPrism(
"/ctmc/embedded2.sm",
true);
108 EXPECT_EQ(3478ul, model->getNumberOfStates());
109 EXPECT_EQ(14639ul, model->getNumberOfTransitions());
111 janiModel = getJaniModelFromPrism(
"/ctmc/polling2.sm",
true);
113 EXPECT_EQ(12ul, model->getNumberOfStates());
114 EXPECT_EQ(22ul, model->getNumberOfTransitions());
116 janiModel = getJaniModelFromPrism(
"/ctmc/fms2.sm",
true);
118 EXPECT_EQ(810ul, model->getNumberOfStates());
119 EXPECT_EQ(3699ul, model->getNumberOfTransitions());
121 janiModel = getJaniModelFromPrism(
"/ctmc/tandem5.sm",
true);
123 EXPECT_EQ(66ul, model->getNumberOfStates());
124 EXPECT_EQ(189ul, model->getNumberOfTransitions());
127TEST_F(ExplicitJaniModelBuilderTest,
Mdp) {
128 auto janiModel = getJaniModelFromPrism(
"/mdp/two_dice.nm");
131 EXPECT_EQ(169ul, model->getNumberOfStates());
132 EXPECT_EQ(436ul, model->getNumberOfTransitions());
134 janiModel = getJaniModelFromPrism(
"/mdp/leader3.nm");
136 EXPECT_EQ(364ul, model->getNumberOfStates());
137 EXPECT_EQ(654ul, model->getNumberOfTransitions());
139 janiModel = getJaniModelFromPrism(
"/mdp/coin2-2.nm");
141 EXPECT_EQ(272ul, model->getNumberOfStates());
142 EXPECT_EQ(492ul, model->getNumberOfTransitions());
144 janiModel = getJaniModelFromPrism(
"/mdp/csma2-2.nm");
146 EXPECT_EQ(1038ul, model->getNumberOfStates());
147 EXPECT_EQ(1282ul, model->getNumberOfTransitions());
149 janiModel = getJaniModelFromPrism(
"/mdp/firewire3-0.5.nm");
151 EXPECT_EQ(4093ul, model->getNumberOfStates());
152 EXPECT_EQ(5585ul, model->getNumberOfTransitions());
154 janiModel = getJaniModelFromPrism(
"/mdp/wlan0-2-2.nm");
156 EXPECT_EQ(37ul, model->getNumberOfStates());
157 EXPECT_EQ(59ul, model->getNumberOfTransitions());
159 janiModel = getJaniModelFromPrism(
"/mdp/sync.nm");
161 EXPECT_EQ(5ul, model->getNumberOfStates());
162 EXPECT_EQ(24ul, model->getNumberOfTransitions());
163 EXPECT_EQ(12ul, model->getNumberOfChoices());
166TEST_F(ExplicitJaniModelBuilderTest, Ma) {
167 auto janiModel = getJaniModelFromPrism(
"/ma/simple.ma");
170 EXPECT_EQ(5ul, model->getNumberOfStates());
171 EXPECT_EQ(8ul, model->getNumberOfTransitions());
175 janiModel = getJaniModelFromPrism(
"/ma/hybrid_states.ma");
177 EXPECT_EQ(5ul, model->getNumberOfStates());
178 EXPECT_EQ(13ul, model->getNumberOfTransitions());
182 janiModel = getJaniModelFromPrism(
"/ma/stream2.ma");
184 EXPECT_EQ(12ul, model->getNumberOfStates());
185 EXPECT_EQ(14ul, model->getNumberOfTransitions());
191 janiModel = janiModel.defineUndefinedConstants(constants);
193 EXPECT_EQ(1536ul, model->getNumberOfStates());
194 EXPECT_EQ(6448ul, model->getNumberOfTransitions());
199TEST_F(ExplicitJaniModelBuilderTest, FailComposition) {
200 auto janiModel = getJaniModelFromPrism(
"/mdp/system_composition.nm");
205TEST_F(ExplicitJaniModelBuilderTest, unassignedVariables) {
208 EXPECT_EQ(25ul, model->getNumberOfStates());
209 EXPECT_EQ(81ul, model->getNumberOfTransitions());
212TEST_F(ExplicitJaniModelBuilderTest, enumerateInitial) {
215 EXPECT_EQ(94ul, model->getNumberOfStates());
216 EXPECT_EQ(145ul, model->getNumberOfTransitions());
217 EXPECT_EQ(72ul, model->getInitialStates().getNumberOfSetBits());
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.
This class represents a discrete-time Markov chain.
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.
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)
#define STORM_SILENT_ASSERT_THROW(statement, expected_exception)