From d35c99e8441bae919c233541814207a00fe69b77 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 9 Jun 2016 09:57:04 +0200 Subject: [PATCH] renamed central model builder function Former-commit-id: 92cfaeae19aa114bb293456f3805217044021532 --- src/builder/DdJaniModelBuilder.cpp | 2 +- src/builder/DdJaniModelBuilder.h | 2 +- src/builder/DdPrismModelBuilder.cpp | 2 +- src/builder/DdPrismModelBuilder.h | 15 +--- src/builder/ExplicitModelBuilder.cpp | 2 +- src/builder/ExplicitModelBuilder.h | 2 +- src/utility/storm.h | 4 +- .../builder/DdJaniModelBuilderTest.cpp | 66 ++++++++--------- .../builder/DdPrismModelBuilderTest.cpp | 72 +++++++++---------- .../builder/ExplicitPrismModelBuilderTest.cpp | 34 ++++----- .../GmmxxCtmcCslModelCheckerTest.cpp | 8 +-- .../GmmxxDtmcPrctlModelCheckerTest.cpp | 2 +- .../GmmxxHybridCtmcCslModelCheckerTest.cpp | 16 ++--- .../GmmxxHybridDtmcPrctlModelCheckerTest.cpp | 12 ++-- .../GmmxxHybridMdpPrctlModelCheckerTest.cpp | 8 +-- .../GmmxxMdpPrctlModelCheckerTest.cpp | 4 +- .../NativeCtmcCslModelCheckerTest.cpp | 8 +-- .../NativeHybridCtmcCslModelCheckerTest.cpp | 16 ++--- .../NativeHybridDtmcPrctlModelCheckerTest.cpp | 12 ++-- .../NativeHybridMdpPrctlModelCheckerTest.cpp | 8 +-- .../SymbolicDtmcPrctlModelCheckerTest.cpp | 12 ++-- .../SymbolicMdpPrctlModelCheckerTest.cpp | 8 +-- .../MilpPermissiveSchedulerTest.cpp | 2 +- .../SmtPermissiveSchedulerTest.cpp | 2 +- ...sticModelBisimulationDecompositionTest.cpp | 2 +- test/functional/utility/GraphTest.cpp | 24 +++---- .../utility/ModelInstantiatorTest.cpp | 6 +- .../SymbolicDtmcPrctlModelCheckerTest.cpp | 8 +-- .../SymbolicMdpPrctlModelCheckerTest.cpp | 8 +-- 29 files changed, 177 insertions(+), 190 deletions(-) diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index a889f54d5..2d9be972d 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -1731,7 +1731,7 @@ namespace storm { } template - std::shared_ptr> DdJaniModelBuilder::translate() { + std::shared_ptr> DdJaniModelBuilder::build() { // Create all necessary variables. CompositionVariableCreator variableCreator(*this->model); CompositionVariables variables = variableCreator.create(); diff --git a/src/builder/DdJaniModelBuilder.h b/src/builder/DdJaniModelBuilder.h index a90f911b5..605a4ea9d 100644 --- a/src/builder/DdJaniModelBuilder.h +++ b/src/builder/DdJaniModelBuilder.h @@ -99,7 +99,7 @@ namespace storm { * @param model The model to translate. * @return A pointer to the resulting model. */ - std::shared_ptr> translate(); + std::shared_ptr> build(); /*! * Retrieves the model that was actually translated (i.e. including constant substitutions etc.). Note diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index 147843c9c..ac02b9761 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -1247,7 +1247,7 @@ namespace storm { } template - std::shared_ptr> DdPrismModelBuilder::translateProgram(storm::prism::Program const& program, Options const& options) { + std::shared_ptr> DdPrismModelBuilder::build(storm::prism::Program const& program, Options const& options) { if (options.constantDefinitions) { preparedProgram = program.defineUndefinedConstants(options.constantDefinitions.get()); } else { diff --git a/src/builder/DdPrismModelBuilder.h b/src/builder/DdPrismModelBuilder.h index 22733ba29..0cb8cc6fd 100644 --- a/src/builder/DdPrismModelBuilder.h +++ b/src/builder/DdPrismModelBuilder.h @@ -50,16 +50,6 @@ namespace storm { */ Options(std::vector> const& formulas); - /*! - * Sets the constants definitions from the given string. The string must be of the form 'X=a,Y=b,Z=c', - * etc. where X,Y,Z are the variable names and a,b,c are the values of the constants. - * - * @param program The program managing the constants that shall be defined. Note that the program itself - * is not modified whatsoever. - * @param constantDefinitionString The string from which to parse the constants' values. - */ - void addConstantDefinitionsFromString(storm::prism::Program const& program, std::string const& constantDefinitionString); - /*! * Changes the options in a way that ensures that the given formula can be checked on the model once it * has been built. @@ -84,9 +74,6 @@ namespace storm { // A list of reward models to be build in case not all reward models are to be build. std::set rewardModelsToBuild; - // An optional mapping that, if given, contains defining expressions for undefined constants. - boost::optional> constantDefinitions; - // A flag indicating whether all labels are to be build. bool buildAllLabels; @@ -109,7 +96,7 @@ namespace storm { * @param program The program to translate. * @return A pointer to the resulting model. */ - std::shared_ptr> translateProgram(storm::prism::Program const& program, Options const& options = Options()); + std::shared_ptr> build(storm::prism::Program const& program, Options const& options = Options()); /*! * Retrieves the program that was actually translated (i.e. including constant substitutions etc.). Note diff --git a/src/builder/ExplicitModelBuilder.cpp b/src/builder/ExplicitModelBuilder.cpp index d1265df9a..dbb5dd5d5 100644 --- a/src/builder/ExplicitModelBuilder.cpp +++ b/src/builder/ExplicitModelBuilder.cpp @@ -107,7 +107,7 @@ namespace storm { } template - std::shared_ptr> ExplicitModelBuilder::translate() { + std::shared_ptr> ExplicitModelBuilder::build() { STORM_LOG_DEBUG("Exploration order is: " << options.explorationOrder); ModelComponents modelComponents = buildModelComponents(); diff --git a/src/builder/ExplicitModelBuilder.h b/src/builder/ExplicitModelBuilder.h index 685ff8870..ef7703033 100644 --- a/src/builder/ExplicitModelBuilder.h +++ b/src/builder/ExplicitModelBuilder.h @@ -101,7 +101,7 @@ namespace storm { * @param rewardModel The reward model that is to be built. * @return The explicit model that was given by the probabilistic program. */ - std::shared_ptr> translate(); + std::shared_ptr> build(); /*! * If requested in the options, information about the variable valuations in the reachable states can be diff --git a/src/utility/storm.h b/src/utility/storm.h index fff7e8576..0676cf1ef 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -117,14 +117,14 @@ namespace storm { std::shared_ptr> generator = std::make_shared>(preprocessedProgram, options); storm::builder::ExplicitModelBuilder builder(generator); - result.model = builder.translate(); + result.model = builder.build(); } else if (storm::settings::getModule().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Dd || storm::settings::getModule().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Hybrid) { typename storm::builder::DdPrismModelBuilder::Options options; options = typename storm::builder::DdPrismModelBuilder::Options(formulas); options.addConstantDefinitionsFromString(program, constantDefinitionString); storm::builder::DdPrismModelBuilder builder; - result.model = builder.translateProgram(program, options); + result.model = builder.build(program, options); } // There may be constants of the model appearing in the formulas, so we replace all their occurrences diff --git a/test/functional/builder/DdJaniModelBuilderTest.cpp b/test/functional/builder/DdJaniModelBuilderTest.cpp index 60fe8ddf4..46f73055a 100644 --- a/test/functional/builder/DdJaniModelBuilderTest.cpp +++ b/test/functional/builder/DdJaniModelBuilderTest.cpp @@ -20,28 +20,28 @@ TEST(DdJaniModelBuilderTest_Sylvan, Dtmc) { storm::jani::Model janiModel = program.toJani(true); storm::builder::DdJaniModelBuilder builder(janiModel); - std::shared_ptr> model = builder.translate(); + std::shared_ptr> model = builder.build(); EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(20ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); janiModel = program.toJani(true); builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.translate(); + model = builder.build(); EXPECT_EQ(677ul, model->getNumberOfStates()); EXPECT_EQ(867ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); janiModel = program.toJani(true); builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.translate(); + model = builder.build(); EXPECT_EQ(8607ul, model->getNumberOfStates()); EXPECT_EQ(15113ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); janiModel = program.toJani(true); builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.translate(); + model = builder.build(); EXPECT_EQ(273ul, model->getNumberOfStates()); EXPECT_EQ(397ul, model->getNumberOfTransitions()); @@ -49,7 +49,7 @@ TEST(DdJaniModelBuilderTest_Sylvan, Dtmc) { janiModel = program.toJani(true); builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.translate(); + model = builder.build(); EXPECT_EQ(1728ul, model->getNumberOfStates()); EXPECT_EQ(2505ul, model->getNumberOfTransitions()); } @@ -59,35 +59,35 @@ TEST(DdJaniModelBuilderTest_Cudd, Dtmc) { storm::jani::Model janiModel = program.toJani(true); storm::builder::DdJaniModelBuilder builder(janiModel); - std::shared_ptr> model = builder.translate(); + std::shared_ptr> model = builder.build(); EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(20ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); janiModel = program.toJani(true); builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.translate(); + model = builder.build(); EXPECT_EQ(677ul, model->getNumberOfStates()); EXPECT_EQ(867ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); janiModel = program.toJani(true); builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.translate(); + model = builder.build(); EXPECT_EQ(8607ul, model->getNumberOfStates()); EXPECT_EQ(15113ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); janiModel = program.toJani(true); builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.translate(); + model = builder.build(); EXPECT_EQ(273ul, model->getNumberOfStates()); EXPECT_EQ(397ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); janiModel = program.toJani(true); builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.translate(); + model = builder.build(); EXPECT_EQ(1728ul, model->getNumberOfStates()); EXPECT_EQ(2505ul, model->getNumberOfTransitions()); } @@ -99,35 +99,35 @@ TEST(DdJaniModelBuilderTest_Sylvan, Ctmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); storm::jani::Model janiModel = program.toJani(true); storm::builder::DdJaniModelBuilder builder(janiModel); - std::shared_ptr> model = builder.translate(); + std::shared_ptr> model = builder.build(); EXPECT_EQ(276ul, model->getNumberOfStates()); EXPECT_EQ(1120ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); janiModel = program.toJani(true); builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.translate(); + model = builder.build(); EXPECT_EQ(3478ul, model->getNumberOfStates()); EXPECT_EQ(14639ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); janiModel = program.toJani(true); builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.translate(); + model = builder.build(); EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(22ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm"); janiModel = program.toJani(true); builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.translate(); + model = builder.build(); EXPECT_EQ(810ul, model->getNumberOfStates()); EXPECT_EQ(3699ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); janiModel = program.toJani(true); builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.translate(); + model = builder.build(); EXPECT_EQ(66ul, model->getNumberOfStates()); EXPECT_EQ(189ul, model->getNumberOfTransitions()); } @@ -139,35 +139,35 @@ TEST(DdJaniModelBuilderTest_Cudd, Ctmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); storm::jani::Model janiModel = program.toJani(true); storm::builder::DdJaniModelBuilder builder(janiModel); - std::shared_ptr> model = builder.translate(); + std::shared_ptr> model = builder.build(); EXPECT_EQ(276ul, model->getNumberOfStates()); EXPECT_EQ(1120ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); janiModel = program.toJani(true); builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.translate(); + model = builder.build(); EXPECT_EQ(3478ul, model->getNumberOfStates()); EXPECT_EQ(14639ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); janiModel = program.toJani(true); builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.translate(); + model = builder.build(); EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(22ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm"); janiModel = program.toJani(true); builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.translate(); + model = builder.build(); EXPECT_EQ(810ul, model->getNumberOfStates()); EXPECT_EQ(3699ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); janiModel = program.toJani(true); builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.translate(); + model = builder.build(); EXPECT_EQ(66ul, model->getNumberOfStates()); EXPECT_EQ(189ul, model->getNumberOfTransitions()); } @@ -176,7 +176,7 @@ TEST(DdJaniModelBuilderTest_Sylvan, Mdp) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); storm::jani::Model janiModel = program.toJani(true); storm::builder::DdJaniModelBuilder builder(janiModel); - std::shared_ptr> model = builder.translate(); + std::shared_ptr> model = builder.build(); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); std::shared_ptr> mdp = model->as>(); @@ -188,7 +188,7 @@ TEST(DdJaniModelBuilderTest_Sylvan, Mdp) { program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); janiModel = program.toJani(true); builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.translate(); + model = builder.build(); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -200,7 +200,7 @@ TEST(DdJaniModelBuilderTest_Sylvan, Mdp) { program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); janiModel = program.toJani(true); builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.translate(); + model = builder.build(); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -212,7 +212,7 @@ TEST(DdJaniModelBuilderTest_Sylvan, Mdp) { program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); janiModel = program.toJani(true); builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.translate(); + model = builder.build(); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -224,7 +224,7 @@ TEST(DdJaniModelBuilderTest_Sylvan, Mdp) { program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm"); janiModel = program.toJani(true); builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.translate(); + model = builder.build(); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -236,7 +236,7 @@ TEST(DdJaniModelBuilderTest_Sylvan, Mdp) { program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); janiModel = program.toJani(true); builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.translate(); + model = builder.build(); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -250,7 +250,7 @@ TEST(DdJaniModelBuilderTest_Cudd, Mdp) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); storm::jani::Model janiModel = program.toJani(true); storm::builder::DdJaniModelBuilder builder(janiModel); - std::shared_ptr> model = builder.translate(); + std::shared_ptr> model = builder.build(); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); std::shared_ptr> mdp = model->as>(); @@ -262,7 +262,7 @@ TEST(DdJaniModelBuilderTest_Cudd, Mdp) { program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); janiModel = program.toJani(true); builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.translate(); + model = builder.build(); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -274,7 +274,7 @@ TEST(DdJaniModelBuilderTest_Cudd, Mdp) { program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); janiModel = program.toJani(true); builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.translate(); + model = builder.build(); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -286,7 +286,7 @@ TEST(DdJaniModelBuilderTest_Cudd, Mdp) { program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); janiModel = program.toJani(true); builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.translate(); + model = builder.build(); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -298,7 +298,7 @@ TEST(DdJaniModelBuilderTest_Cudd, Mdp) { program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm"); janiModel = program.toJani(true); builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.translate(); + model = builder.build(); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -310,7 +310,7 @@ TEST(DdJaniModelBuilderTest_Cudd, Mdp) { program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); janiModel = program.toJani(true); builder = storm::builder::DdJaniModelBuilder(janiModel); - model = builder.translate(); + model = builder.build(); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -324,5 +324,5 @@ TEST(DdJaniModelBuilderTest_Cudd, IllegalFragment) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2-illegalSynchronizingWrite.nm"); storm::jani::Model janiModel = program.toJani(true); storm::builder::DdJaniModelBuilder builder(janiModel); - EXPECT_THROW(std::shared_ptr> model = builder.translate(), storm::exceptions::WrongFormatException); + EXPECT_THROW(std::shared_ptr> model = builder.build(), storm::exceptions::WrongFormatException); } \ No newline at end of file diff --git a/test/functional/builder/DdPrismModelBuilderTest.cpp b/test/functional/builder/DdPrismModelBuilderTest.cpp index fe0e00def..a6b73779a 100644 --- a/test/functional/builder/DdPrismModelBuilderTest.cpp +++ b/test/functional/builder/DdPrismModelBuilderTest.cpp @@ -13,27 +13,27 @@ TEST(DdPrismModelBuilderTest_Sylvan, Dtmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(20ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); - model = storm::builder::DdPrismModelBuilder().translateProgram(program); + model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(677ul, model->getNumberOfStates()); EXPECT_EQ(867ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); - model = storm::builder::DdPrismModelBuilder().translateProgram(program); + model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(8607ul, model->getNumberOfStates()); EXPECT_EQ(15113ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); - model = storm::builder::DdPrismModelBuilder().translateProgram(program); + model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(273ul, model->getNumberOfStates()); EXPECT_EQ(397ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); - model = storm::builder::DdPrismModelBuilder().translateProgram(program); + model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(1728ul, model->getNumberOfStates()); EXPECT_EQ(2505ul, model->getNumberOfTransitions()); } @@ -41,27 +41,27 @@ TEST(DdPrismModelBuilderTest_Sylvan, Dtmc) { TEST(DdPrismModelBuilderTest_Cudd, Dtmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(20ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); - model = storm::builder::DdPrismModelBuilder().translateProgram(program); + model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(677ul, model->getNumberOfStates()); EXPECT_EQ(867ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); - model = storm::builder::DdPrismModelBuilder().translateProgram(program); + model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(8607ul, model->getNumberOfStates()); EXPECT_EQ(15113ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); - model = storm::builder::DdPrismModelBuilder().translateProgram(program); + model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(273ul, model->getNumberOfStates()); EXPECT_EQ(397ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); - model = storm::builder::DdPrismModelBuilder().translateProgram(program); + model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(1728ul, model->getNumberOfStates()); EXPECT_EQ(2505ul, model->getNumberOfTransitions()); } @@ -72,27 +72,27 @@ TEST(DdPrismModelBuilderTest_Sylvan, Ctmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(276ul, model->getNumberOfStates()); EXPECT_EQ(1120ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); - model = storm::builder::DdPrismModelBuilder().translateProgram(program); + model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(3478ul, model->getNumberOfStates()); EXPECT_EQ(14639ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); - model = storm::builder::DdPrismModelBuilder().translateProgram(program); + model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(22ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm"); - model = storm::builder::DdPrismModelBuilder().translateProgram(program); + model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(810ul, model->getNumberOfStates()); EXPECT_EQ(3699ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); - model = storm::builder::DdPrismModelBuilder().translateProgram(program); + model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(66ul, model->getNumberOfStates()); EXPECT_EQ(189ul, model->getNumberOfTransitions()); } @@ -103,34 +103,34 @@ TEST(DdPrismModelBuilderTest_Cudd, Ctmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(276ul, model->getNumberOfStates()); EXPECT_EQ(1120ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); - model = storm::builder::DdPrismModelBuilder().translateProgram(program); + model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(3478ul, model->getNumberOfStates()); EXPECT_EQ(14639ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); - model = storm::builder::DdPrismModelBuilder().translateProgram(program); + model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(22ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm"); - model = storm::builder::DdPrismModelBuilder().translateProgram(program); + model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(810ul, model->getNumberOfStates()); EXPECT_EQ(3699ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); - model = storm::builder::DdPrismModelBuilder().translateProgram(program); + model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(66ul, model->getNumberOfStates()); EXPECT_EQ(189ul, model->getNumberOfTransitions()); } TEST(DdPrismModelBuilderTest_Sylvan, Mdp) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); std::shared_ptr> mdp = model->as>(); @@ -140,7 +140,7 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) { EXPECT_EQ(254ul, mdp->getNumberOfChoices()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); - model = storm::builder::DdPrismModelBuilder().translateProgram(program); + model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -150,7 +150,7 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) { EXPECT_EQ(573ul, mdp->getNumberOfChoices()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); - model = storm::builder::DdPrismModelBuilder().translateProgram(program); + model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -160,7 +160,7 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) { EXPECT_EQ(400ul, mdp->getNumberOfChoices()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); - model = storm::builder::DdPrismModelBuilder().translateProgram(program); + model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -170,7 +170,7 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) { EXPECT_EQ(1054ul, mdp->getNumberOfChoices()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm"); - model = storm::builder::DdPrismModelBuilder().translateProgram(program); + model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -180,7 +180,7 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) { EXPECT_EQ(5519ul, mdp->getNumberOfChoices()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); - model = storm::builder::DdPrismModelBuilder().translateProgram(program); + model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -192,7 +192,7 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) { TEST(DdPrismModelBuilderTest_Cudd, Mdp) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); std::shared_ptr> mdp = model->as>(); @@ -202,7 +202,7 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) { EXPECT_EQ(254ul, mdp->getNumberOfChoices()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); - model = storm::builder::DdPrismModelBuilder().translateProgram(program); + model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -212,7 +212,7 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) { EXPECT_EQ(573ul, mdp->getNumberOfChoices()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); - model = storm::builder::DdPrismModelBuilder().translateProgram(program); + model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -222,7 +222,7 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) { EXPECT_EQ(400ul, mdp->getNumberOfChoices()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); - model = storm::builder::DdPrismModelBuilder().translateProgram(program); + model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -232,7 +232,7 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) { EXPECT_EQ(1054ul, mdp->getNumberOfChoices()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm"); - model = storm::builder::DdPrismModelBuilder().translateProgram(program); + model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -242,7 +242,7 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) { EXPECT_EQ(5519ul, mdp->getNumberOfChoices()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); - model = storm::builder::DdPrismModelBuilder().translateProgram(program); + model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -255,7 +255,7 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) { TEST(DdPrismModelBuilderTest_Sylvan, Composition) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); std::shared_ptr> mdp = model->as>(); @@ -266,7 +266,7 @@ TEST(DdPrismModelBuilderTest_Sylvan, Composition) { program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition2.nm"); - model = storm::builder::DdPrismModelBuilder().translateProgram(program); + model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -279,7 +279,7 @@ TEST(DdPrismModelBuilderTest_Sylvan, Composition) { TEST(DdPrismModelBuilderTest_Cudd, Composition) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); std::shared_ptr> mdp = model->as>(); @@ -290,7 +290,7 @@ TEST(DdPrismModelBuilderTest_Cudd, Composition) { program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition2.nm"); - model = storm::builder::DdPrismModelBuilder().translateProgram(program); + model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); diff --git a/test/functional/builder/ExplicitPrismModelBuilderTest.cpp b/test/functional/builder/ExplicitPrismModelBuilderTest.cpp index 159966d76..d91eb64c4 100644 --- a/test/functional/builder/ExplicitPrismModelBuilderTest.cpp +++ b/test/functional/builder/ExplicitPrismModelBuilderTest.cpp @@ -10,27 +10,27 @@ TEST(ExplicitModelBuilderTest, Dtmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).translate(); + 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_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); - model = storm::builder::ExplicitModelBuilder(program).translate(); + model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(677ul, model->getNumberOfStates()); EXPECT_EQ(867ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); - model = storm::builder::ExplicitModelBuilder(program).translate(); + model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(8607ul, model->getNumberOfStates()); EXPECT_EQ(15113ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); - model = storm::builder::ExplicitModelBuilder(program).translate(); + model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(273ul, model->getNumberOfStates()); EXPECT_EQ(397ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); - model = storm::builder::ExplicitModelBuilder(program).translate(); + model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(1728ul, model->getNumberOfStates()); EXPECT_EQ(2505ul, model->getNumberOfTransitions()); } @@ -41,27 +41,27 @@ TEST(ExplicitModelBuilderTest, Ctmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).translate(); + 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_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); - model = storm::builder::ExplicitModelBuilder(program).translate(); + model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(3478ul, model->getNumberOfStates()); EXPECT_EQ(14639ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); - model = storm::builder::ExplicitModelBuilder(program).translate(); + model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(22ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm"); - model = storm::builder::ExplicitModelBuilder(program).translate(); + model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(810ul, model->getNumberOfStates()); EXPECT_EQ(3699ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); - model = storm::builder::ExplicitModelBuilder(program).translate(); + model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(66ul, model->getNumberOfStates()); EXPECT_EQ(189ul, model->getNumberOfTransitions()); } @@ -69,32 +69,32 @@ TEST(ExplicitModelBuilderTest, Ctmc) { TEST(ExplicitModelBuilderTest, Mdp) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).translate(); + 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_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); - model = storm::builder::ExplicitModelBuilder(program).translate(); + model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(364ul, model->getNumberOfStates()); EXPECT_EQ(654ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); - model = storm::builder::ExplicitModelBuilder(program).translate(); + model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(272ul, model->getNumberOfStates()); EXPECT_EQ(492ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); - model = storm::builder::ExplicitModelBuilder(program).translate(); + model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(1038ul, model->getNumberOfStates()); EXPECT_EQ(1282ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm"); - model = storm::builder::ExplicitModelBuilder(program).translate(); + model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(4093ul, model->getNumberOfStates()); EXPECT_EQ(5585ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); - model = storm::builder::ExplicitModelBuilder(program).translate(); + model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(37ul, model->getNumberOfStates()); EXPECT_EQ(59ul, model->getNumberOfTransitions()); } @@ -102,5 +102,5 @@ TEST(ExplicitModelBuilderTest, Mdp) { TEST(ExplicitModelBuilderTest, Fail) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm"); - ASSERT_THROW(storm::builder::ExplicitModelBuilder(program).translate(), storm::exceptions::WrongFormatException); + ASSERT_THROW(storm::builder::ExplicitModelBuilder(program).build(), storm::exceptions::WrongFormatException); } diff --git a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp index b3afe2657..7cdbc2159 100644 --- a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp @@ -35,7 +35,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Cluster) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("num_repairs"); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).translate(); + 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(); @@ -118,7 +118,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Embedded) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("up"); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).translate(); + 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(); @@ -180,7 +180,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Polling) { std::shared_ptr formula(nullptr); // Build the model. - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).translate(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).build(); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); uint_fast64_t initialState = *ctmc->getInitialStates().begin(); @@ -227,7 +227,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Tandem) { typename storm::builder::ExplicitModelBuilder::Options options; #endif options.rewardModelsToBuild.insert("customers"); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).translate(); + 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(); diff --git a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp index 55a015eeb..9feeda286 100644 --- a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp @@ -284,7 +284,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRA) { TEST(GmmxxDtmcPrctlModelCheckerTest, Conditional) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/test_conditional.pm"); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).translate(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).build(); ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc); ASSERT_EQ(4ul, model->getNumberOfStates()); ASSERT_EQ(5ul, model->getNumberOfTransitions()); diff --git a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp index 757f69aad..52196371d 100644 --- a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp @@ -38,7 +38,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Cudd) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("num_repairs"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); @@ -135,7 +135,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Sylvan) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("num_repairs"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); @@ -232,7 +232,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Cudd) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("up"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); @@ -311,7 +311,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Sylvan) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("up"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); @@ -383,7 +383,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Cudd) { std::shared_ptr formula(nullptr); // Build the model. - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); @@ -419,7 +419,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Sylvan) { std::shared_ptr formula(nullptr); // Build the model. - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); @@ -469,7 +469,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem_Cudd) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("customers"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); @@ -557,7 +557,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem_Sylvan) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("customers"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); diff --git a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp index 38d914ae9..0c4679382 100644 --- a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp @@ -32,7 +32,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Cudd) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("coin_flips"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(20ul, model->getNumberOfTransitions()); @@ -93,7 +93,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Sylvan) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("coin_flips"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(20ul, model->getNumberOfTransitions()); @@ -146,7 +146,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Cudd) { // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(8607ul, model->getNumberOfStates()); EXPECT_EQ(15113ul, model->getNumberOfTransitions()); @@ -190,7 +190,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) { // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(8607ul, model->getNumberOfStates()); EXPECT_EQ(15113ul, model->getNumberOfTransitions()); @@ -242,7 +242,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("num_rounds"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); EXPECT_EQ(273ul, model->getNumberOfStates()); EXPECT_EQ(397ul, model->getNumberOfTransitions()); @@ -294,7 +294,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("num_rounds"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); EXPECT_EQ(273ul, model->getNumberOfStates()); EXPECT_EQ(397ul, model->getNumberOfTransitions()); diff --git a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp index 17f5300a0..98c91ec1a 100644 --- a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp @@ -34,7 +34,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Cudd) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("coinflips"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); EXPECT_EQ(169ul, model->getNumberOfStates()); EXPECT_EQ(436ul, model->getNumberOfTransitions()); @@ -131,7 +131,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Sylvan) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("coinflips"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); EXPECT_EQ(169ul, model->getNumberOfStates()); EXPECT_EQ(436ul, model->getNumberOfTransitions()); @@ -228,7 +228,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("rounds"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); EXPECT_EQ(3172ul, model->getNumberOfStates()); EXPECT_EQ(7144ul, model->getNumberOfTransitions()); @@ -307,7 +307,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("rounds"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); EXPECT_EQ(3172ul, model->getNumberOfStates()); EXPECT_EQ(7144ul, model->getNumberOfTransitions()); diff --git a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index 917dbfe6a..02ea39e5f 100644 --- a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -197,7 +197,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) { // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).translate(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(4ul, model->getNumberOfStates()); EXPECT_EQ(11ul, model->getNumberOfTransitions()); @@ -247,7 +247,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, tiny_rewards) { // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).translate(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(3ul, model->getNumberOfStates()); EXPECT_EQ(4ul, model->getNumberOfTransitions()); diff --git a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp index ecee3f5a4..fa3f89a02 100644 --- a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp @@ -33,7 +33,7 @@ TEST(NativeCtmcCslModelCheckerTest, Cluster) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("num_repairs"); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).translate(); + 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(); @@ -109,7 +109,7 @@ TEST(NativeCtmcCslModelCheckerTest, Embedded) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("up"); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).translate(); + 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(); @@ -164,7 +164,7 @@ TEST(NativeCtmcCslModelCheckerTest, Polling) { std::shared_ptr formula(nullptr); // Build the model. - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).translate(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).build(); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); uint_fast64_t initialState = *ctmc->getInitialStates().begin(); @@ -205,7 +205,7 @@ TEST(NativeCtmcCslModelCheckerTest, Tandem) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("customers"); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).translate(); + 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(); diff --git a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp index 80b467d22..d2e3ff7d6 100644 --- a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp @@ -37,7 +37,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Cudd) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("num_repairs"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); @@ -134,7 +134,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Sylvan) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("num_repairs"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); @@ -231,7 +231,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Cudd) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("up"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); @@ -310,7 +310,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Sylvan) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("up"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); @@ -382,7 +382,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Cudd) { std::shared_ptr formula(nullptr); // Build the model. - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); @@ -418,7 +418,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Sylvan) { std::shared_ptr formula(nullptr); // Build the model. - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); @@ -468,7 +468,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Cudd) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("customers"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); @@ -558,7 +558,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Sylvan) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("customers"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); diff --git a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp index fe5b5e202..072745694 100644 --- a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp @@ -33,7 +33,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_Cudd) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("coin_flips"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(20ul, model->getNumberOfTransitions()); @@ -94,7 +94,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_Sylvan) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("coin_flips"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(20ul, model->getNumberOfTransitions()); @@ -147,7 +147,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_Cudd) { // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(8607ul, model->getNumberOfStates()); EXPECT_EQ(15113ul, model->getNumberOfTransitions()); @@ -191,7 +191,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) { // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(8607ul, model->getNumberOfStates()); EXPECT_EQ(15113ul, model->getNumberOfTransitions()); @@ -243,7 +243,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("num_rounds"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); EXPECT_EQ(273ul, model->getNumberOfStates()); EXPECT_EQ(397ul, model->getNumberOfTransitions()); @@ -295,7 +295,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("num_rounds"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); EXPECT_EQ(273ul, model->getNumberOfStates()); EXPECT_EQ(397ul, model->getNumberOfTransitions()); diff --git a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp index abd2650e9..07eacac65 100644 --- a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp @@ -32,7 +32,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Cudd) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("coinflips"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); EXPECT_EQ(169ul, model->getNumberOfStates()); EXPECT_EQ(436ul, model->getNumberOfTransitions()); @@ -128,7 +128,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Sylvan) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("coinflips"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); EXPECT_EQ(169ul, model->getNumberOfStates()); EXPECT_EQ(436ul, model->getNumberOfTransitions()); @@ -224,7 +224,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("rounds"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); EXPECT_EQ(3172ul, model->getNumberOfStates()); EXPECT_EQ(7144ul, model->getNumberOfTransitions()); @@ -303,7 +303,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("rounds"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); EXPECT_EQ(3172ul, model->getNumberOfStates()); EXPECT_EQ(7144ul, model->getNumberOfTransitions()); diff --git a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp index b1ea8296a..a653f8e16 100644 --- a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp @@ -31,7 +31,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Cudd) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("coin_flips"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(20ul, model->getNumberOfTransitions()); @@ -92,7 +92,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Sylvan) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("coin_flips"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(20ul, model->getNumberOfTransitions()); @@ -146,7 +146,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Cudd) { // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(8607ul, model->getNumberOfStates()); EXPECT_EQ(15113ul, model->getNumberOfTransitions()); @@ -190,7 +190,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Sylvan) { // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(8607ul, model->getNumberOfStates()); EXPECT_EQ(15113ul, model->getNumberOfTransitions()); @@ -245,7 +245,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("num_rounds"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); EXPECT_EQ(273ul, model->getNumberOfStates()); EXPECT_EQ(397ul, model->getNumberOfTransitions()); @@ -297,7 +297,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("num_rounds"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); EXPECT_EQ(273ul, model->getNumberOfStates()); EXPECT_EQ(397ul, model->getNumberOfTransitions()); diff --git a/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp index fa24aaa6f..9ad5265a9 100644 --- a/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp @@ -31,7 +31,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Cudd) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("coinflips"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); EXPECT_EQ(169ul, model->getNumberOfStates()); EXPECT_EQ(436ul, model->getNumberOfTransitions()); @@ -128,7 +128,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Sylvan) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("coinflips"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); EXPECT_EQ(169ul, model->getNumberOfStates()); EXPECT_EQ(436ul, model->getNumberOfTransitions()); @@ -225,7 +225,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("rounds"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); EXPECT_EQ(3172ul, model->getNumberOfStates()); EXPECT_EQ(7144ul, model->getNumberOfTransitions()); @@ -304,7 +304,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("rounds"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); EXPECT_EQ(3172ul, model->getNumberOfStates()); EXPECT_EQ(7144ul, model->getNumberOfTransitions()); diff --git a/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp b/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp index a7b025009..80b4184f4 100644 --- a/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp +++ b/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp @@ -28,7 +28,7 @@ TEST(MilpPermissiveSchedulerTest, DieSelection) { options.addConstantDefinitionsFromString(program, ""); options.buildCommandLabels = true; - std::shared_ptr> mdp = storm::builder::ExplicitModelBuilder(program, options).translate()->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/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp b/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp index f61c18c41..e72b2fff4 100644 --- a/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp +++ b/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp @@ -31,7 +31,7 @@ TEST(SmtPermissiveSchedulerTest, DieSelection) { options.addConstantDefinitionsFromString(program, ""); options.buildCommandLabels = true; - std::shared_ptr> mdp = storm::builder::ExplicitModelBuilder(program, options).translate()->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/test/functional/storage/NondeterministicModelBisimulationDecompositionTest.cpp b/test/functional/storage/NondeterministicModelBisimulationDecompositionTest.cpp index 19ea6f8a6..045a26071 100644 --- a/test/functional/storage/NondeterministicModelBisimulationDecompositionTest.cpp +++ b/test/functional/storage/NondeterministicModelBisimulationDecompositionTest.cpp @@ -14,7 +14,7 @@ TEST(NondeterministicModelBisimulationDecomposition, TwoDice) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); // Build the die model without its reward model. - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).translate(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).build(); ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); std::shared_ptr> mdp = model->as>(); diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp index cf1517013..ae3893fa5 100644 --- a/test/functional/utility/GraphTest.cpp +++ b/test/functional/utility/GraphTest.cpp @@ -17,7 +17,7 @@ TEST(GraphTest, SymbolicProb01_Cudd) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc); @@ -38,7 +38,7 @@ TEST(GraphTest, SymbolicProb01_Cudd) { TEST(GraphTest, SymbolicProb01_Sylvan) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc); @@ -59,7 +59,7 @@ TEST(GraphTest, SymbolicProb01_Sylvan) { TEST(GraphTest, SymbolicProb01MinMax_Cudd) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -76,7 +76,7 @@ TEST(GraphTest, SymbolicProb01MinMax_Cudd) { } program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); - model = storm::builder::DdPrismModelBuilder().translateProgram(program); + model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -101,7 +101,7 @@ TEST(GraphTest, SymbolicProb01MinMax_Cudd) { } program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); - model = storm::builder::DdPrismModelBuilder().translateProgram(program); + model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -120,7 +120,7 @@ TEST(GraphTest, SymbolicProb01MinMax_Cudd) { TEST(GraphTest, SymbolicProb01MinMax_Sylvan) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -137,7 +137,7 @@ TEST(GraphTest, SymbolicProb01MinMax_Sylvan) { } program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); - model = storm::builder::DdPrismModelBuilder().translateProgram(program); + model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -162,7 +162,7 @@ TEST(GraphTest, SymbolicProb01MinMax_Sylvan) { } program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); - model = storm::builder::DdPrismModelBuilder().translateProgram(program); + model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -181,7 +181,7 @@ TEST(GraphTest, SymbolicProb01MinMax_Sylvan) { TEST(GraphTest, ExplicitProb01) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).translate(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).build(); ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc); @@ -202,7 +202,7 @@ TEST(GraphTest, ExplicitProb01) { TEST(GraphTest, ExplicitProb01MinMax) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).translate(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).build(); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -217,7 +217,7 @@ TEST(GraphTest, ExplicitProb01MinMax) { EXPECT_EQ(364ul, statesWithProbability01.second.getNumberOfSetBits()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); - model = storm::builder::ExplicitModelBuilder(program).translate(); + model = storm::builder::ExplicitModelBuilder(program).build(); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -238,7 +238,7 @@ TEST(GraphTest, ExplicitProb01MinMax) { EXPECT_EQ(35ul, statesWithProbability01.second.getNumberOfSetBits()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); - model = storm::builder::ExplicitModelBuilder(program).translate(); + model = storm::builder::ExplicitModelBuilder(program).build(); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); diff --git a/test/functional/utility/ModelInstantiatorTest.cpp b/test/functional/utility/ModelInstantiatorTest.cpp index 9caf16632..5fbd811a6 100644 --- a/test/functional/utility/ModelInstantiatorTest.cpp +++ b/test/functional/utility/ModelInstantiatorTest.cpp @@ -33,7 +33,7 @@ TEST(ModelInstantiatorTest, BrpProb) { typename storm::builder::ExplicitModelBuilder::Options options = storm::builder::ExplicitModelBuilder::Options(*formulas[0]); options.addConstantDefinitionsFromString(program, constantsAsString); options.preserveFormula(*formulas[0]); - std::shared_ptr> dtmc = storm::builder::ExplicitModelBuilder(program, options).translate()->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()); @@ -154,7 +154,7 @@ TEST(ModelInstantiatorTest, Brp_Rew) { typename storm::builder::ExplicitModelBuilder::Options options = storm::builder::ExplicitModelBuilder::Options(*formulas[0]); options.addConstantDefinitionsFromString(program, constantsAsString); options.preserveFormula(*formulas[0]); - std::shared_ptr> dtmc = storm::builder::ExplicitModelBuilder(program, options).translate()->as>(); + std::shared_ptr> dtmc = storm::builder::ExplicitModelBuilder(program, options).build()->as>(); storm::utility::ModelInstantiator, storm::models::sparse::Dtmc> modelInstantiator(*dtmc); @@ -227,7 +227,7 @@ TEST(ModelInstantiatorTest, Consensus) { typename storm::builder::ExplicitModelBuilder::Options options = storm::builder::ExplicitModelBuilder::Options(*formulas[0]); options.addConstantDefinitionsFromString(program, constantsAsString); options.preserveFormula(*formulas[0]); - std::shared_ptr> mdp = storm::builder::ExplicitModelBuilder(program, options).translate()->as>(); + std::shared_ptr> mdp = storm::builder::ExplicitModelBuilder(program, options).build()->as>(); storm::utility::ModelInstantiator, storm::models::sparse::Mdp> modelInstantiator(*mdp); diff --git a/test/performance/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp b/test/performance/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp index c1c76347f..22c6532a8 100644 --- a/test/performance/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp @@ -31,7 +31,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("num_rounds"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); EXPECT_EQ(131521ul, model->getNumberOfStates()); EXPECT_EQ(164288ul, model->getNumberOfTransitions()); @@ -83,7 +83,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("num_rounds"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); EXPECT_EQ(131521ul, model->getNumberOfStates()); EXPECT_EQ(164288ul, model->getNumberOfTransitions()); @@ -127,7 +127,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Cudd) { // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(586242ul, model->getNumberOfStates()); EXPECT_EQ(1753883ul, model->getNumberOfTransitions()); @@ -171,7 +171,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Sylvan) { // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(586242ul, model->getNumberOfStates()); EXPECT_EQ(1753883ul, model->getNumberOfTransitions()); diff --git a/test/performance/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp index 67f92a29f..b31b37a71 100644 --- a/test/performance/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp @@ -31,7 +31,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("rounds"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); EXPECT_EQ(27299ul, model->getNumberOfStates()); EXPECT_EQ(74365ul, model->getNumberOfTransitions()); @@ -83,7 +83,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("rounds"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program, options); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); EXPECT_EQ(27299ul, model->getNumberOfStates()); EXPECT_EQ(74365ul, model->getNumberOfTransitions()); @@ -137,7 +137,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, CSMA_Cudd) { options.rewardModelsToBuild.insert("time"); storm::builder::DdPrismModelBuilder builder; - std::shared_ptr> model = builder.translateProgram(program, options); + std::shared_ptr> model = builder.build(program, options); storm::prism::Program translatedProgram = builder.getTranslatedProgram(); EXPECT_EQ(36850ul, model->getNumberOfStates()); @@ -194,7 +194,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, CSMA_Sylvan) { options.rewardModelsToBuild.insert("time"); storm::builder::DdPrismModelBuilder builder; - std::shared_ptr> model = builder.translateProgram(program, options); + std::shared_ptr> model = builder.build(program, options); storm::prism::Program translatedProgram = builder.getTranslatedProgram(); EXPECT_EQ(36850ul, model->getNumberOfStates());