diff --git a/test/functional/logic/FragmentCheckerTest.cpp b/test/functional/logic/FragmentCheckerTest.cpp index 0280844d3..3ae4d52e3 100644 --- a/test/functional/logic/FragmentCheckerTest.cpp +++ b/test/functional/logic/FragmentCheckerTest.cpp @@ -3,12 +3,14 @@ #include "src/parser/FormulaParser.h" #include "src/logic/FragmentChecker.h" #include "src/exceptions/WrongFormatException.h" +#include "src/storage/expressions/ExpressionManager.h" TEST(FragmentCheckerTest, Propositional) { + auto expManager = std::make_shared(); storm::logic::FragmentChecker checker; storm::logic::FragmentSpecification prop = storm::logic::propositional(); - storm::parser::FormulaParser formulaParser; + storm::parser::FormulaParser formulaParser(expManager); std::shared_ptr formula; ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); @@ -37,10 +39,11 @@ TEST(FragmentCheckerTest, Propositional) { } TEST(FragmentCheckerTest, Pctl) { + auto expManager = std::make_shared(); storm::logic::FragmentChecker checker; storm::logic::FragmentSpecification pctl = storm::logic::pctl(); - storm::parser::FormulaParser formulaParser; + storm::parser::FormulaParser formulaParser(expManager); std::shared_ptr formula; ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); @@ -57,10 +60,11 @@ TEST(FragmentCheckerTest, Pctl) { } TEST(FragmentCheckerTest, Prctl) { + auto expManager = std::make_shared(); storm::logic::FragmentChecker checker; storm::logic::FragmentSpecification prctl = storm::logic::prctl(); - storm::parser::FormulaParser formulaParser; + storm::parser::FormulaParser formulaParser(expManager); std::shared_ptr formula; ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); @@ -83,10 +87,11 @@ TEST(FragmentCheckerTest, Prctl) { } TEST(FragmentCheckerTest, Csl) { + auto expManager = std::make_shared(); storm::logic::FragmentChecker checker; storm::logic::FragmentSpecification csl = storm::logic::csl(); - storm::parser::FormulaParser formulaParser; + storm::parser::FormulaParser formulaParser(expManager); std::shared_ptr formula; ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); @@ -106,10 +111,11 @@ TEST(FragmentCheckerTest, Csl) { } TEST(FragmentCheckerTest, Csrl) { + auto expManager = std::make_shared(); storm::logic::FragmentChecker checker; storm::logic::FragmentSpecification csrl = storm::logic::csrl(); - storm::parser::FormulaParser formulaParser; + storm::parser::FormulaParser formulaParser(expManager); std::shared_ptr formula; ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); diff --git a/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp index b66c71f09..9b8b982f7 100644 --- a/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp @@ -15,12 +15,15 @@ #include "src/parser/AutoParser.h" #include "src/parser/PrismParser.h" #include "src/builder/ExplicitModelBuilder.h" +#include "src/storage/expressions/ExpressionManager.h" TEST(EigenDtmcPrctlModelCheckerTest, Die) { std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/die/die.tra", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.coin_flips.trans.rew"); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; + + auto expManager = std::make_shared(); + storm::parser::FormulaParser formulaParser(expManager); ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); @@ -69,7 +72,9 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalNumber) { std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).build(); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; + + auto expManager = std::make_shared(); + storm::parser::FormulaParser formulaParser(expManager); ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); @@ -116,7 +121,9 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalFunction) { std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).build(); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; + + auto expManager = std::make_shared(); + storm::parser::FormulaParser formulaParser(expManager); ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); @@ -168,7 +175,9 @@ TEST(EigenDtmcPrctlModelCheckerTest, Crowds) { ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; + + auto expManager = std::make_shared(); + storm::parser::FormulaParser formulaParser(expManager); std::shared_ptr> dtmc = abstractModel->as>(); @@ -205,7 +214,9 @@ TEST(EigenDtmcPrctlModelCheckerTest, SynchronousLeader) { ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; + + auto expManager = std::make_shared(); + storm::parser::FormulaParser formulaParser(expManager); std::shared_ptr> dtmc = abstractModel->as>(); @@ -241,7 +252,9 @@ TEST(EigenDtmcPrctlModelCheckerTest, LRASingleBscc) { std::shared_ptr> dtmc; // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; + + auto expManager = std::make_shared(); + storm::parser::FormulaParser formulaParser(expManager); { matrixBuilder = storm::storage::SparseMatrixBuilder(2, 2, 2); @@ -321,7 +334,9 @@ TEST(EigenDtmcPrctlModelCheckerTest, LRA) { std::shared_ptr> dtmc; // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; + + auto expManager = std::make_shared(); + storm::parser::FormulaParser formulaParser(expManager); { matrixBuilder = storm::storage::SparseMatrixBuilder(15, 15, 20, true); @@ -398,7 +413,9 @@ TEST(EigenDtmcPrctlModelCheckerTest, Conditional) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; + + auto expManager = std::make_shared(); + storm::parser::FormulaParser formulaParser(expManager); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"target\"]"); std::unique_ptr result = checker.check(*formula); diff --git a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp index 8f6814ded..7ae8fd860 100644 --- a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp @@ -18,6 +18,8 @@ #include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/settings/modules/GmmxxEquationSolverSettings.h" +#include "src/storage/expressions/ExpressionManager.h" + TEST(GmmxxCtmcCslModelCheckerTest, Cluster) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); diff --git a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp index 2290a1cec..e28c643e5 100644 --- a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp @@ -15,12 +15,14 @@ #include "src/parser/AutoParser.h" #include "src/parser/PrismParser.h" #include "src/builder/ExplicitModelBuilder.h" +#include "src/storage/expressions/ExpressionManager.h" TEST(GmmxxDtmcPrctlModelCheckerTest, Die) { std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/die/die.tra", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.coin_flips.trans.rew"); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; + auto expManager = std::make_shared(); + storm::parser::FormulaParser formulaParser(expManager); ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); @@ -66,7 +68,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; + + auto expManager = std::make_shared(); + storm::parser::FormulaParser formulaParser(expManager); std::shared_ptr> dtmc = abstractModel->as>(); @@ -103,7 +107,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; + + auto expManager = std::make_shared(); + storm::parser::FormulaParser formulaParser(expManager); std::shared_ptr> dtmc = abstractModel->as>(); @@ -139,7 +145,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) { std::shared_ptr> dtmc; // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; + + auto expManager = std::make_shared(); + storm::parser::FormulaParser formulaParser(expManager); { matrixBuilder = storm::storage::SparseMatrixBuilder(2, 2, 2); @@ -219,7 +227,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRA) { std::shared_ptr> dtmc; // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; + + auto expManager = std::make_shared(); + storm::parser::FormulaParser formulaParser(expManager); { matrixBuilder = storm::storage::SparseMatrixBuilder(15, 15, 20, true); @@ -294,7 +304,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Conditional) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; + + auto expManager = std::make_shared(); + storm::parser::FormulaParser formulaParser(expManager); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"target\"]"); std::unique_ptr result = checker.check(*formula); diff --git a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp index 96450fa35..c068fc292 100644 --- a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp @@ -21,6 +21,7 @@ #include "src/settings/modules/GmmxxEquationSolverSettings.h" #include "src/settings/modules/NativeEquationSolverSettings.h" +#include "src/storage/expressions/ExpressionManager.h" TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Cudd) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. diff --git a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp index 53e992fd3..1cf195a8d 100644 --- a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp @@ -13,18 +13,21 @@ #include "src/models/symbolic/Dtmc.h" #include "src/models/symbolic/StandardRewardModel.h" #include "src/storage/SymbolicModelDescription.h" +#include "src/storage/expressions/ExpressionManager.h" #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" #include "src/settings/modules/GmmxxEquationSolverSettings.h" - #include "src/settings/modules/NativeEquationSolverSettings.h" + TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Cudd) { storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; + + auto expManager = std::make_shared(); + storm::parser::FormulaParser formulaParser(expManager); // Build the die model with its reward model. #ifdef WINDOWS @@ -86,7 +89,9 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Sylvan) { storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; + + auto expManager = std::make_shared(); + storm::parser::FormulaParser formulaParser(expManager); // Build the die model with its reward model. #ifdef WINDOWS @@ -148,7 +153,9 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Cudd) { storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; + + auto expManager = std::make_shared(); + storm::parser::FormulaParser formulaParser(expManager); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(8607ul, model->getNumberOfStates()); @@ -193,7 +200,9 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) { storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; + + auto expManager = std::make_shared(); + storm::parser::FormulaParser formulaParser(expManager); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(8607ul, model->getNumberOfStates()); @@ -238,7 +247,9 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) { storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; + + auto expManager = std::make_shared(); + storm::parser::FormulaParser formulaParser(expManager); // Build the die model with its reward model. #ifdef WINDOWS @@ -291,7 +302,9 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) { storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; + + auto expManager = std::make_shared(); + storm::parser::FormulaParser formulaParser(expManager); // Build the die model with its reward model. #ifdef WINDOWS diff --git a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp index eb00b67cd..2229546f1 100644 --- a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp @@ -26,6 +26,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Cudd) { storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser formulaParser; // Build the die model with its reward model. diff --git a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp index 29a937a5e..93234108c 100644 --- a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp @@ -22,7 +22,7 @@ TEST(NativeCtmcCslModelCheckerTest, Cluster) { // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); - storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); + storm::parser::FormulaParser formulaParser(program); std::shared_ptr formula(nullptr); // Build the model. @@ -91,7 +91,7 @@ TEST(NativeCtmcCslModelCheckerTest, Embedded) { // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); - storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); + storm::parser::FormulaParser formulaParser(program); std::shared_ptr formula(nullptr); // Build the model. @@ -148,7 +148,7 @@ TEST(NativeCtmcCslModelCheckerTest, Polling) { // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); - storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); + storm::parser::FormulaParser formulaParser(program); std::shared_ptr formula(nullptr); // Build the model. @@ -182,7 +182,7 @@ TEST(NativeCtmcCslModelCheckerTest, Tandem) { // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); - storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); + storm::parser::FormulaParser formulaParser(program); std::shared_ptr formula(nullptr); // Build the model with the customers reward structure. diff --git a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp index 5d8391f5c..0bda60e39 100644 --- a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp @@ -28,7 +28,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Cudd) { // Parse the model description. storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); + storm::parser::FormulaParser formulaParser(program); std::shared_ptr formula(nullptr); // Build the model. @@ -126,7 +126,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Sylvan) { // Parse the model description. storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); + storm::parser::FormulaParser formulaParser(program); std::shared_ptr formula(nullptr); // Build the model. @@ -224,7 +224,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Cudd) { // Parse the model description. storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); + storm::parser::FormulaParser formulaParser(program); std::shared_ptr formula(nullptr); // Build the model. @@ -304,7 +304,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Sylvan) { // Parse the model description. storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); + storm::parser::FormulaParser formulaParser(program); std::shared_ptr formula(nullptr); // Build the model. @@ -384,7 +384,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Cudd) { // Parse the model description. storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); + storm::parser::FormulaParser formulaParser(program); std::shared_ptr formula(nullptr); // Build the model. @@ -421,7 +421,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Sylvan) { // Parse the model description. storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); + storm::parser::FormulaParser formulaParser(program); std::shared_ptr formula(nullptr); // Build the model. @@ -465,7 +465,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Cudd) { // Parse the model description. storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); + storm::parser::FormulaParser formulaParser(program); std::shared_ptr formula(nullptr); // Build the model with the customers reward structure. @@ -556,7 +556,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Sylvan) { // Parse the model description. storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); + storm::parser::FormulaParser formulaParser(program); std::shared_ptr formula(nullptr); // Build the model with the customers reward structure. diff --git a/test/functional/parser/FormulaParserTest.cpp b/test/functional/parser/FormulaParserTest.cpp index 1435806eb..14077658e 100644 --- a/test/functional/parser/FormulaParserTest.cpp +++ b/test/functional/parser/FormulaParserTest.cpp @@ -3,6 +3,7 @@ #include "src/parser/FormulaParser.h" #include "src/logic/FragmentSpecification.h" #include "src/exceptions/WrongFormatException.h" +#include "src/storage/expressions/ExpressionManager.h" TEST(FormulaParserTest, LabelTest) { storm::parser::FormulaParser formulaParser; diff --git a/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp b/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp index 85253c5ca..0d722d125 100644 --- a/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp +++ b/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp @@ -15,7 +15,7 @@ TEST(SmtPermissiveSchedulerTest, DieSelection) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die_c1.nm"); - storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); + storm::parser::FormulaParser formulaParser(program); // auto formula02 = formulaParser.parseSingleFormulaFromString("P>=0.10 [ F \"one\"]")->asProbabilityOperatorFormula(); // ASSERT_TRUE(storm::logic::isLowerBound(formula02.getComparisonType()));