diff --git a/src/test/builder/ExplicitJaniModelBuilderTest.cpp b/src/test/builder/ExplicitJaniModelBuilderTest.cpp index 72918d0f8..4a0584ea9 100644 --- a/src/test/builder/ExplicitJaniModelBuilderTest.cpp +++ b/src/test/builder/ExplicitJaniModelBuilderTest.cpp @@ -14,31 +14,31 @@ TEST(ExplicitJaniModelBuilderTest, Dtmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); storm::jani::Model janiModel = program.toJani(); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(janiModel).build().getModel(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(20ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/brp-16-2.pm"); janiModel = program.toJani(); - model = storm::builder::ExplicitModelBuilder(janiModel).build().getModel(); + model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(677ul, model->getNumberOfStates()); EXPECT_EQ(867ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm"); janiModel = program.toJani(); - model = storm::builder::ExplicitModelBuilder(janiModel).build().getModel(); + model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(8607ul, model->getNumberOfStates()); EXPECT_EQ(15113ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm"); janiModel = program.toJani(); - model = storm::builder::ExplicitModelBuilder(janiModel).build().getModel(); + model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(273ul, model->getNumberOfStates()); EXPECT_EQ(397ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/nand-5-2.pm"); janiModel = program.toJani(); - model = storm::builder::ExplicitModelBuilder(janiModel).build().getModel(); + model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(1728ul, model->getNumberOfStates()); EXPECT_EQ(2505ul, model->getNumberOfTransitions()); } @@ -50,31 +50,31 @@ TEST(ExplicitJaniModelBuilderTest, Ctmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm"); storm::jani::Model janiModel = program.toJani(); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(janiModel).build().getModel(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(276ul, model->getNumberOfStates()); EXPECT_EQ(1120ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm"); janiModel = program.toJani(); - model = storm::builder::ExplicitModelBuilder(janiModel).build().getModel(); + model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(3478ul, model->getNumberOfStates()); EXPECT_EQ(14639ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm"); janiModel = program.toJani(); - model = storm::builder::ExplicitModelBuilder(janiModel).build().getModel(); + model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(22ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm"); janiModel = program.toJani(); - model = storm::builder::ExplicitModelBuilder(janiModel).build().getModel(); + model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(810ul, model->getNumberOfStates()); EXPECT_EQ(3699ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm"); janiModel = program.toJani(); - model = storm::builder::ExplicitModelBuilder(janiModel).build().getModel(); + model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(66ul, model->getNumberOfStates()); EXPECT_EQ(189ul, model->getNumberOfTransitions()); } @@ -83,37 +83,37 @@ TEST(ExplicitJaniModelBuilderTest, Mdp) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); storm::jani::Model janiModel = program.toJani(); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(janiModel).build().getModel(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(169ul, model->getNumberOfStates()); EXPECT_EQ(436ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm"); janiModel = program.toJani(); - model = storm::builder::ExplicitModelBuilder(janiModel).build().getModel(); + model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(364ul, model->getNumberOfStates()); EXPECT_EQ(654ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm"); janiModel = program.toJani(); - model = storm::builder::ExplicitModelBuilder(janiModel).build().getModel(); + model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(272ul, model->getNumberOfStates()); EXPECT_EQ(492ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2-2.nm"); janiModel = program.toJani(); - model = storm::builder::ExplicitModelBuilder(janiModel).build().getModel(); + model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(1038ul, model->getNumberOfStates()); EXPECT_EQ(1282ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/firewire3-0.5.nm"); janiModel = program.toJani(); - model = storm::builder::ExplicitModelBuilder(janiModel).build().getModel(); + model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(4093ul, model->getNumberOfStates()); EXPECT_EQ(5585ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-2.nm"); janiModel = program.toJani(); - model = storm::builder::ExplicitModelBuilder(janiModel).build().getModel(); + model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(37ul, model->getNumberOfStates()); EXPECT_EQ(59ul, model->getNumberOfTransitions()); } @@ -122,7 +122,7 @@ TEST(ExplicitJaniModelBuilderTest, Ma) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/simple.ma"); storm::jani::Model janiModel = program.toJani(); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(janiModel).build().getModel(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(5ul, model->getNumberOfStates()); EXPECT_EQ(8ul, model->getNumberOfTransitions()); ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton)); @@ -130,7 +130,7 @@ TEST(ExplicitJaniModelBuilderTest, Ma) { program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/hybrid_states.ma"); janiModel = program.toJani(); - model = storm::builder::ExplicitModelBuilder(janiModel).build().getModel(); + model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(5ul, model->getNumberOfStates()); EXPECT_EQ(13ul, model->getNumberOfTransitions()); ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton)); @@ -138,7 +138,7 @@ TEST(ExplicitJaniModelBuilderTest, Ma) { program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/stream2.ma"); janiModel = program.toJani(); - model = storm::builder::ExplicitModelBuilder(janiModel).build().getModel(); + model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(14ul, model->getNumberOfTransitions()); ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton)); diff --git a/src/test/builder/ExplicitPrismModelBuilderTest.cpp b/src/test/builder/ExplicitPrismModelBuilderTest.cpp index 0e5f1d399..4da7e5039 100644 --- a/src/test/builder/ExplicitPrismModelBuilderTest.cpp +++ b/src/test/builder/ExplicitPrismModelBuilderTest.cpp @@ -11,27 +11,27 @@ TEST(ExplicitPrismModelBuilderTest, Dtmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).build().getModel(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(20ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/brp-16-2.pm"); - model = storm::builder::ExplicitModelBuilder(program).build().getModel(); + model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(677ul, model->getNumberOfStates()); EXPECT_EQ(867ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm"); - model = storm::builder::ExplicitModelBuilder(program).build().getModel(); + model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(8607ul, model->getNumberOfStates()); EXPECT_EQ(15113ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm"); - model = storm::builder::ExplicitModelBuilder(program).build().getModel(); + model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(273ul, model->getNumberOfStates()); EXPECT_EQ(397ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/nand-5-2.pm"); - model = storm::builder::ExplicitModelBuilder(program).build().getModel(); + model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(1728ul, model->getNumberOfStates()); EXPECT_EQ(2505ul, model->getNumberOfTransitions()); } @@ -42,27 +42,27 @@ TEST(ExplicitPrismModelBuilderTest, Ctmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm"); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).build().getModel(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(276ul, model->getNumberOfStates()); EXPECT_EQ(1120ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm"); - model = storm::builder::ExplicitModelBuilder(program).build().getModel(); + model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(3478ul, model->getNumberOfStates()); EXPECT_EQ(14639ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm"); - model = storm::builder::ExplicitModelBuilder(program).build().getModel(); + model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(22ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm"); - model = storm::builder::ExplicitModelBuilder(program).build().getModel(); + model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(810ul, model->getNumberOfStates()); EXPECT_EQ(3699ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm"); - model = storm::builder::ExplicitModelBuilder(program).build().getModel(); + model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(66ul, model->getNumberOfStates()); EXPECT_EQ(189ul, model->getNumberOfTransitions()); } @@ -70,32 +70,32 @@ TEST(ExplicitPrismModelBuilderTest, Ctmc) { TEST(ExplicitPrismModelBuilderTest, Mdp) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).build().getModel(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(169ul, model->getNumberOfStates()); EXPECT_EQ(436ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm"); - model = storm::builder::ExplicitModelBuilder(program).build().getModel(); + model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(364ul, model->getNumberOfStates()); EXPECT_EQ(654ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm"); - model = storm::builder::ExplicitModelBuilder(program).build().getModel(); + model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(272ul, model->getNumberOfStates()); EXPECT_EQ(492ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2-2.nm"); - model = storm::builder::ExplicitModelBuilder(program).build().getModel(); + model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(1038ul, model->getNumberOfStates()); EXPECT_EQ(1282ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/firewire3-0.5.nm"); - model = storm::builder::ExplicitModelBuilder(program).build().getModel(); + model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(4093ul, model->getNumberOfStates()); EXPECT_EQ(5585ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-2.nm"); - model = storm::builder::ExplicitModelBuilder(program).build().getModel(); + model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(37ul, model->getNumberOfStates()); EXPECT_EQ(59ul, model->getNumberOfTransitions()); } @@ -103,21 +103,21 @@ TEST(ExplicitPrismModelBuilderTest, Mdp) { TEST(ExplicitPrismModelBuilderTest, Ma) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/simple.ma"); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).build().getModel(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(5ul, model->getNumberOfStates()); EXPECT_EQ(8ul, model->getNumberOfTransitions()); ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton)); EXPECT_EQ(4ul, model->as>()->getMarkovianStates().getNumberOfSetBits()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/hybrid_states.ma"); - model = storm::builder::ExplicitModelBuilder(program).build().getModel(); + model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(5ul, model->getNumberOfStates()); EXPECT_EQ(13ul, model->getNumberOfTransitions()); ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton)); EXPECT_EQ(5ul, model->as>()->getMarkovianStates().getNumberOfSetBits()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/stream2.ma"); - model = storm::builder::ExplicitModelBuilder(program).build().getModel(); + model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(14ul, model->getNumberOfTransitions()); ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton)); diff --git a/src/test/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp b/src/test/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp index 83847029e..8ec80c0b7 100644 --- a/src/test/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp +++ b/src/test/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp @@ -69,7 +69,7 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalNumber) { storm::generator::NextStateGeneratorOptions options; options.setBuildAllLabels().setBuildAllRewardModels(); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).build().getModel(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).build(); // A parser that we use for conveniently constructing the formulas. @@ -118,7 +118,7 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalFunction) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/pdtmc/parametric_die.pm"); storm::generator::NextStateGeneratorOptions options; options.setBuildAllLabels().setBuildAllRewardModels(); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).build().getModel(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).build(); // A parser that we use for conveniently constructing the formulas. @@ -403,7 +403,7 @@ TEST(EigenDtmcPrctlModelCheckerTest, Conditional) { storm::generator::NextStateGeneratorOptions options; options.setBuildAllLabels().setBuildAllRewardModels(); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).build().getModel(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).build(); ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc); ASSERT_EQ(4ul, model->getNumberOfStates()); ASSERT_EQ(5ul, model->getNumberOfTransitions()); diff --git a/src/test/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp b/src/test/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp index b28bf4464..56a1a498f 100644 --- a/src/test/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp +++ b/src/test/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp @@ -31,7 +31,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Cluster) { // Build the model. storm::generator::NextStateGeneratorOptions options; - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true). addRewardModel("num_repairs")).build().getModel(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true). addRewardModel("num_repairs")).build(); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); uint_fast64_t initialState = *ctmc->getInitialStates().begin(); @@ -107,7 +107,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Embedded) { std::shared_ptr formula(nullptr); // Build the model. - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true). addRewardModel("up")).build().getModel(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true). addRewardModel("up")).build(); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); uint_fast64_t initialState = *ctmc->getInitialStates().begin(); @@ -169,7 +169,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Polling) { std::shared_ptr formula(nullptr); // Build the model. - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true)).build().getModel(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true)).build(); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); uint_fast64_t initialState = *ctmc->getInitialStates().begin(); @@ -210,7 +210,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Tandem) { std::shared_ptr formula(nullptr); // Build the model. - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true). addRewardModel("customers")).build().getModel(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true). addRewardModel("customers")).build(); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); uint_fast64_t initialState = *ctmc->getInitialStates().begin(); diff --git a/src/test/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp b/src/test/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp index 069498637..5535edf4f 100644 --- a/src/test/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp +++ b/src/test/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp @@ -294,7 +294,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRA) { TEST(GmmxxDtmcPrctlModelCheckerTest, Conditional) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/test_conditional.pm"); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(true, true)).build().getModel(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(true, true)).build(); ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc); ASSERT_EQ(4ul, model->getNumberOfStates()); ASSERT_EQ(5ul, model->getNumberOfTransitions()); diff --git a/src/test/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/src/test/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index f7fc4819c..3a38b9dc4 100644 --- a/src/test/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/src/test/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -199,7 +199,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) { storm::generator::NextStateGeneratorOptions options; options.setBuildAllLabels(); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).build().getModel(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).build(); EXPECT_EQ(4ull, model->getNumberOfStates()); EXPECT_EQ(11ull, model->getNumberOfTransitions()); @@ -251,7 +251,7 @@ TEST(DISABLED_GmmxxMdpPrctlModelCheckerTest, TinyRewards) { // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(true, true)).build().getModel(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(true, true)).build(); EXPECT_EQ(3ull, model->getNumberOfStates()); EXPECT_EQ(4ull, model->getNumberOfTransitions()); diff --git a/src/test/modelchecker/NativeCtmcCslModelCheckerTest.cpp b/src/test/modelchecker/NativeCtmcCslModelCheckerTest.cpp index 5e746cec4..ed79b2db8 100644 --- a/src/test/modelchecker/NativeCtmcCslModelCheckerTest.cpp +++ b/src/test/modelchecker/NativeCtmcCslModelCheckerTest.cpp @@ -26,7 +26,7 @@ TEST(NativeCtmcCslModelCheckerTest, Cluster) { std::shared_ptr formula(nullptr); // Build the model. - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true). addRewardModel("num_repairs")).build().getModel(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true). addRewardModel("num_repairs")).build(); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); uint_fast64_t initialState = *ctmc->getInitialStates().begin(); @@ -97,7 +97,7 @@ TEST(NativeCtmcCslModelCheckerTest, Embedded) { // Build the model. storm::generator::NextStateGeneratorOptions options; options.addRewardModel("up").setBuildAllLabels(); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).build().getModel(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).build(); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); uint_fast64_t initialState = *ctmc->getInitialStates().begin(); @@ -152,7 +152,7 @@ TEST(NativeCtmcCslModelCheckerTest, Polling) { std::shared_ptr formula(nullptr); // Build the model. - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true)).build().getModel(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true)).build(); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); uint_fast64_t initialState = *ctmc->getInitialStates().begin(); @@ -186,7 +186,7 @@ TEST(NativeCtmcCslModelCheckerTest, Tandem) { std::shared_ptr formula(nullptr); // Build the model with the customers reward structure. - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true).addRewardModel("customers")).build().getModel(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true).addRewardModel("customers")).build(); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); uint_fast64_t initialState = *ctmc->getInitialStates().begin(); diff --git a/src/test/permissiveschedulers/MilpPermissiveSchedulerTest.cpp b/src/test/permissiveschedulers/MilpPermissiveSchedulerTest.cpp index 6352b1d78..155212770 100644 --- a/src/test/permissiveschedulers/MilpPermissiveSchedulerTest.cpp +++ b/src/test/permissiveschedulers/MilpPermissiveSchedulerTest.cpp @@ -26,7 +26,7 @@ TEST(MilpPermissiveSchedulerTest, DieSelection) { // Customize and perform model-building. storm::generator::NextStateGeneratorOptions options; options.setBuildAllLabels().setBuildChoiceLabels(true); - std::shared_ptr> mdp = storm::builder::ExplicitModelBuilder(program, options).build().getModel()->as>(); + std::shared_ptr> mdp = storm::builder::ExplicitModelBuilder(program, options).build()->as>(); boost::optional> perms = storm::ps::computePermissiveSchedulerViaMILP<>(*mdp, formula02); EXPECT_NE(perms, boost::none); diff --git a/src/test/permissiveschedulers/SmtPermissiveSchedulerTest.cpp b/src/test/permissiveschedulers/SmtPermissiveSchedulerTest.cpp index c52704506..ae9fad1d2 100644 --- a/src/test/permissiveschedulers/SmtPermissiveSchedulerTest.cpp +++ b/src/test/permissiveschedulers/SmtPermissiveSchedulerTest.cpp @@ -29,7 +29,7 @@ TEST(SmtPermissiveSchedulerTest, DISABLED_DieSelection) { // Customize and perform model-building. storm::generator::NextStateGeneratorOptions options(formula02b); - std::shared_ptr> mdp = storm::builder::ExplicitModelBuilder(program, options).build().getModel()->as>(); + std::shared_ptr> mdp = storm::builder::ExplicitModelBuilder(program, options).build()->as>(); // boost::optional> perms = storm::ps::computePermissiveSchedulerViaSMT<>(*mdp, formula02); // EXPECT_NE(perms, boost::none); diff --git a/src/test/storage/NondeterministicModelBisimulationDecompositionTest.cpp b/src/test/storage/NondeterministicModelBisimulationDecompositionTest.cpp index e048d4faa..596938852 100644 --- a/src/test/storage/NondeterministicModelBisimulationDecompositionTest.cpp +++ b/src/test/storage/NondeterministicModelBisimulationDecompositionTest.cpp @@ -14,7 +14,7 @@ TEST(NondeterministicModelBisimulationDecomposition, TwoDice) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); // Build the die model without its reward model. - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true)).build().getModel(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true)).build(); ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); std::shared_ptr> mdp = model->as>(); diff --git a/src/test/utility/GraphTest.cpp b/src/test/utility/GraphTest.cpp index 9571204a0..ac646d99a 100644 --- a/src/test/utility/GraphTest.cpp +++ b/src/test/utility/GraphTest.cpp @@ -596,7 +596,7 @@ TEST(GraphTest, SymbolicProb01StochasticGameWlan) { TEST(GraphTest, ExplicitProb01) { storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm"); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true)).build().getModel(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true)).build(); ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc); @@ -618,7 +618,7 @@ TEST(GraphTest, ExplicitProb01) { TEST(GraphTest, ExplicitProb01MinMax) { storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm"); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true)).build().getModel(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true)).build(); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -634,7 +634,7 @@ TEST(GraphTest, ExplicitProb01MinMax) { modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm"); program = modelDescription.preprocess().asPrismProgram(); - model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true)).build().getModel(); + model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true)).build(); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -656,7 +656,7 @@ TEST(GraphTest, ExplicitProb01MinMax) { modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2-2.nm"); program = modelDescription.preprocess().asPrismProgram(); - model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true)).build().getModel(); + model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true)).build(); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); diff --git a/src/test/utility/KSPTest.cpp b/src/test/utility/KSPTest.cpp index f69de42c7..df8b4f212 100644 --- a/src/test/utility/KSPTest.cpp +++ b/src/test/utility/KSPTest.cpp @@ -17,7 +17,7 @@ std::shared_ptr> buildExampleModel() { std::string prismModelPath = STORM_TEST_RESOURCES_DIR "/dtmc/brp-16-2.pm"; storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(prismModelPath); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - return storm::builder::ExplicitModelBuilder(program).build().getModel(); + return storm::builder::ExplicitModelBuilder(program).build(); } // NOTE: these are hardcoded (obviously), but the model's state indices might change diff --git a/src/test/utility/ModelInstantiatorTest.cpp b/src/test/utility/ModelInstantiatorTest.cpp index 78c2dcf5e..646b51f2d 100644 --- a/src/test/utility/ModelInstantiatorTest.cpp +++ b/src/test/utility/ModelInstantiatorTest.cpp @@ -30,7 +30,7 @@ TEST(ModelInstantiatorTest, BrpProb) { ASSERT_TRUE(formulas.size()==1); // Parametric model storm::generator::NextStateGeneratorOptions options(*formulas.front()); - std::shared_ptr> dtmc = storm::builder::ExplicitModelBuilder(program, options).build().getModel()->as>(); + std::shared_ptr> dtmc = storm::builder::ExplicitModelBuilder(program, options).build()->as>(); storm::utility::ModelInstantiator, storm::models::sparse::Dtmc> modelInstantiator(*dtmc); EXPECT_FALSE(dtmc->hasRewardModel()); @@ -148,7 +148,7 @@ TEST(ModelInstantiatorTest, Brp_Rew) { ASSERT_TRUE(formulas.size()==1); // Parametric model storm::generator::NextStateGeneratorOptions options(*formulas.front()); - std::shared_ptr> dtmc = storm::builder::ExplicitModelBuilder(program, options).build().getModel()->as>(); + std::shared_ptr> dtmc = storm::builder::ExplicitModelBuilder(program, options).build()->as>(); storm::utility::ModelInstantiator, storm::models::sparse::Dtmc> modelInstantiator(*dtmc); @@ -218,7 +218,7 @@ TEST(ModelInstantiatorTest, Consensus) { ASSERT_TRUE(formulas.size()==1); // Parametric model storm::generator::NextStateGeneratorOptions options(*formulas.front()); - std::shared_ptr> mdp = storm::builder::ExplicitModelBuilder(program, options).build().getModel()->as>(); + std::shared_ptr> mdp = storm::builder::ExplicitModelBuilder(program, options).build()->as>(); storm::utility::ModelInstantiator, storm::models::sparse::Mdp> modelInstantiator(*mdp);