From adb42b3ac08edb72a9ed86a5fa45cf8fdf8a1cb0 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 11 Mar 2016 16:37:59 +0100 Subject: [PATCH] fixed minor things related to merge Former-commit-id: f428c2808b1db2a0a5ac458118b546554ff6a22a --- .../utility/ModelInstantiatorTest.cpp | 29 +++++++++---------- 1 file changed, 14 insertions(+), 15 deletions(-) diff --git a/test/functional/utility/ModelInstantiatorTest.cpp b/test/functional/utility/ModelInstantiatorTest.cpp index af8f5b8d2..fe2ee4a7c 100644 --- a/test/functional/utility/ModelInstantiatorTest.cpp +++ b/test/functional/utility/ModelInstantiatorTest.cpp @@ -17,12 +17,12 @@ #include "src/models/sparse/Dtmc.h" #include "src/models/sparse/Mdp.h" -TEST(ModelInstantiatorTest, Brp_Prob) { +TEST(ModelInstantiatorTest, BrpProb) { carl::VariablePool::getInstance().clear(); - std::string const& programFile = STORM_CPP_TESTS_BASE_PATH "/functional/utility/brp16_2.pm"; - std::string const& formulaAsString = "P=? [F s=5 ]"; - std::string const& constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + std::string programFile = STORM_CPP_TESTS_BASE_PATH "/functional/utility/brp16_2.pm"; + std::string formulaAsString = "P=? [F s=5 ]"; + std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 // Program and formula storm::prism::Program program = storm::parseProgram(programFile); @@ -33,7 +33,7 @@ TEST(ModelInstantiatorTest, Brp_Prob) { typename storm::builder::ExplicitPrismModelBuilder::Options options = storm::builder::ExplicitPrismModelBuilder::Options(*formulas[0]); options.addConstantDefinitionsFromString(program, constantsAsString); options.preserveFormula(*formulas[0]); - std::shared_ptr> dtmc = storm::builder::ExplicitPrismModelBuilder().translateProgram(program, options)->as>(); + std::shared_ptr> dtmc = storm::builder::ExplicitPrismModelBuilder(program, options).translate()->as>(); storm::utility::ModelInstantiator, storm::models::sparse::Dtmc> modelInstantiator(*dtmc); EXPECT_FALSE(dtmc->hasRewardModel()); @@ -141,9 +141,9 @@ TEST(ModelInstantiatorTest, Brp_Prob) { TEST(ModelInstantiatorTest, Brp_Rew) { carl::VariablePool::getInstance().clear(); - std::string const& programFile = STORM_CPP_TESTS_BASE_PATH "/functional/utility/brp16_2.pm"; - std::string const& formulaAsString = "R=? [F ((s=5) | (s=0&srep=3)) ]"; - std::string const& constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + std::string programFile = STORM_CPP_TESTS_BASE_PATH "/functional/utility/brp16_2.pm"; + std::string formulaAsString = "R=? [F ((s=5) | (s=0&srep=3)) ]"; + std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 // Program and formula storm::prism::Program program = storm::parseProgram(programFile); @@ -154,7 +154,7 @@ TEST(ModelInstantiatorTest, Brp_Rew) { typename storm::builder::ExplicitPrismModelBuilder::Options options = storm::builder::ExplicitPrismModelBuilder::Options(*formulas[0]); options.addConstantDefinitionsFromString(program, constantsAsString); options.preserveFormula(*formulas[0]); - std::shared_ptr> dtmc = storm::builder::ExplicitPrismModelBuilder().translateProgram(program, options)->as>(); + std::shared_ptr> dtmc = storm::builder::ExplicitPrismModelBuilder(program, options).translate()->as>(); storm::utility::ModelInstantiator, storm::models::sparse::Dtmc> modelInstantiator(*dtmc); @@ -211,12 +211,12 @@ TEST(ModelInstantiatorTest, Brp_Rew) { } -TEST(ModelInstantiatorTest, consensus) { +TEST(ModelInstantiatorTest, Consensus) { carl::VariablePool::getInstance().clear(); - std::string const& programFile = STORM_CPP_TESTS_BASE_PATH "/functional/utility/coin2_2.pm"; - std::string const& formulaAsString = "Pmin=? [F \"finished\"&\"all_coins_equal_1\" ]"; - std::string const& constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + std::string programFile = STORM_CPP_TESTS_BASE_PATH "/functional/utility/coin2_2.pm"; + std::string formulaAsString = "Pmin=? [F \"finished\"&\"all_coins_equal_1\" ]"; + std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 // Program and formula storm::prism::Program program = storm::parseProgram(programFile); @@ -227,7 +227,7 @@ TEST(ModelInstantiatorTest, consensus) { typename storm::builder::ExplicitPrismModelBuilder::Options options = storm::builder::ExplicitPrismModelBuilder::Options(*formulas[0]); options.addConstantDefinitionsFromString(program, constantsAsString); options.preserveFormula(*formulas[0]); - std::shared_ptr> mdp = storm::builder::ExplicitPrismModelBuilder().translateProgram(program, options)->as>(); + std::shared_ptr> mdp = storm::builder::ExplicitPrismModelBuilder(program, options).translate()->as>(); storm::utility::ModelInstantiator, storm::models::sparse::Mdp> modelInstantiator(*mdp); @@ -260,7 +260,6 @@ TEST(ModelInstantiatorTest, consensus) { std::unique_ptr chkResult = modelchecker.check(*formulas[0]); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeChkResult = chkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.3526577219, quantitativeChkResult[*instantiated.getInitialStates().begin()], storm::settings::generalSettings().getPrecision()); - } #endif \ No newline at end of file