diff --git a/CMakeLists.txt b/CMakeLists.txt index 57774cee4..06195f63b 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -194,7 +194,15 @@ if(CUSTOM_BOOST_ROOT) endif(CUSTOM_BOOST_ROOT) if(STORM_PYTHON) -find_package(Boost REQUIRED COMPONENTS python3) + find_package(Boost REQUIRED COMPONENTS python3) + #HACK for DEBIAN + if(NOT Boost_PYTHON3_FOUND) + set(PYVERSION 34) + load_library(pycarl Boost 1.55 COMPONENTS python-py${PYVERSION}) + if(NOT Boost_PYTHON-PY${PYVERSION}_FOUND) + message(FATAL_ERROR "Could not find Boost Python") + endif() +endif() else() find_package(Boost REQUIRED) endif() diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index 20929afc7..18a156e08 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -201,7 +201,7 @@ namespace storm { } template - DdPrismModelBuilder::Options::Options(std::vector> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), terminalStates(), negatedTerminalStates() { + DdPrismModelBuilder::Options::Options(std::vector> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), terminalStates(), negatedTerminalStates() { if (formulas.empty()) { this->buildAllRewardModels = true; this->buildAllLabels = true; diff --git a/src/builder/DdPrismModelBuilder.h b/src/builder/DdPrismModelBuilder.h index 1ee9e5168..279548172 100644 --- a/src/builder/DdPrismModelBuilder.h +++ b/src/builder/DdPrismModelBuilder.h @@ -48,7 +48,7 @@ namespace storm { * * @param formula Thes formula based on which to choose the building options. */ - Options(std::vector> const& formulas); + 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', diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index a3d80d067..ed0f43d3b 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -129,7 +129,7 @@ namespace storm { } template - ExplicitPrismModelBuilder::Options::Options(std::vector> const& formulas) : buildCommandLabels(false), buildAllRewardModels(false), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() { + ExplicitPrismModelBuilder::Options::Options(std::vector> const& formulas) : buildCommandLabels(false), buildAllRewardModels(false), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() { if (formulas.empty()) { this->buildAllRewardModels = true; this->buildAllLabels = true; diff --git a/src/builder/ExplicitPrismModelBuilder.h b/src/builder/ExplicitPrismModelBuilder.h index 31b8e03b7..ccb0622e7 100644 --- a/src/builder/ExplicitPrismModelBuilder.h +++ b/src/builder/ExplicitPrismModelBuilder.h @@ -163,7 +163,7 @@ namespace storm { * * @param formula Thes formula based on which to choose the building options. */ - Options(std::vector> const& formulas); + 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', diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp index 54643d32a..0909b25de 100644 --- a/src/cli/cli.cpp +++ b/src/cli/cli.cpp @@ -220,17 +220,18 @@ namespace storm { } // Then proceed to parsing the property (if given), since the model we are building may depend on the property. - std::vector> formulas; + std::vector> parsedFormulas; if (settings.isPropertySet()) { std::string properties = settings.getProperty(); if(program) { - formulas = storm::parseFormulasForProgram(properties, program.get()); + parsedFormulas = storm::parseFormulasForProgram(properties, program.get()); } else { - formulas = storm::parseFormulasForExplicit(properties); + parsedFormulas = storm::parseFormulasForExplicit(properties); } } + std::vector> formulas(parsedFormulas.begin(), parsedFormulas.end()); if (settings.isSymbolicSet()) { #ifdef STORM_HAVE_CARL diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h index 114a74668..cddebdf7f 100644 --- a/src/cli/entrypoints.h +++ b/src/cli/entrypoints.h @@ -9,7 +9,7 @@ namespace storm { namespace cli { template - void verifySparseModel(std::shared_ptr> model, std::vector> const& formulas) { + void verifySparseModel(std::shared_ptr> model, std::vector> const& formulas) { for (auto const& formula : formulas) { std::cout << std::endl << "Model checking property: " << *formula << " ..."; std::unique_ptr result(storm::verifySparseModel(model, formula)); @@ -26,7 +26,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - inline void verifySparseModel(std::shared_ptr> model, std::vector> const& formulas) { + inline void verifySparseModel(std::shared_ptr> model, std::vector> const& formulas) { for (auto const& formula : formulas) { STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc, storm::exceptions::InvalidSettingsException, "Currently parametric verification is only available for DTMCs."); @@ -50,12 +50,12 @@ namespace storm { #endif template - void verifySymbolicModelWithAbstractionRefinementEngine(storm::prism::Program const& program, std::vector> const& formulas) { + void verifySymbolicModelWithAbstractionRefinementEngine(storm::prism::Program const& program, std::vector> const& formulas) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Abstraction Refinement is not yet implemented."); } template - void verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::vector> const& formulas) { + void verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::vector> const& formulas) { for (auto const& formula : formulas) { std::cout << std::endl << "Model checking property: " << *formula << " ..."; std::unique_ptr result(storm::verifySymbolicModelWithHybridEngine(model, formula)); @@ -72,7 +72,7 @@ namespace storm { } template - void verifySymbolicModelWithSymbolicEngine(std::shared_ptr> model, std::vector> const& formulas) { + void verifySymbolicModelWithSymbolicEngine(std::shared_ptr> model, std::vector> const& formulas) { for (auto const& formula : formulas) { std::cout << std::endl << "Model checking property: " << *formula << " ..."; std::unique_ptr result(storm::verifySymbolicModelWithDdEngine(model, formula)); @@ -114,7 +114,7 @@ namespace storm { } template - void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { + void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); @@ -159,7 +159,7 @@ namespace storm { } template - void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { + void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { if (storm::settings::generalSettings().getDdLibraryType() == storm::dd::DdType::CUDD) { buildAndCheckSymbolicModel(program, formulas); } else if (storm::settings::generalSettings().getDdLibraryType() == storm::dd::DdType::Sylvan) { @@ -168,7 +168,7 @@ namespace storm { } template - void buildAndCheckExplicitModel(std::vector> const& formulas) { + void buildAndCheckExplicitModel(std::vector> const& formulas) { storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); STORM_LOG_THROW(settings.isExplicitSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files."); diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index 8d56086e7..bc5be2111 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -977,7 +977,7 @@ namespace storm { * @param formulaPtr A pointer to a safety formula. The outermost operator must be a probabilistic bound operator with a strict upper bound. The nested * formula can be either an unbounded until formula or an eventually formula. */ - static void computeCounterexample(storm::prism::Program const& program, storm::models::sparse::Mdp const& labeledMdp, std::shared_ptr const& formula) { + static void computeCounterexample(storm::prism::Program const& program, storm::models::sparse::Mdp const& labeledMdp, std::shared_ptr const& formula) { std::cout << std::endl << "Generating minimal label counterexample for formula " << *formula << std::endl; STORM_LOG_THROW(formula->isProbabilityOperatorFormula(), storm::exceptions::InvalidPropertyException, "Counterexample generation does not support this kind of formula. Expecting a probability operator as the outermost formula element."); diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index d8d29bcdd..7c85f7644 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -1751,7 +1751,7 @@ namespace storm { #endif } - static void computeCounterexample(storm::prism::Program program, std::string const& constantDefinitionString, storm::models::sparse::Mdp const& labeledMdp, std::shared_ptr const& formula) { + static void computeCounterexample(storm::prism::Program program, std::string const& constantDefinitionString, storm::models::sparse::Mdp const& labeledMdp, std::shared_ptr const& formula) { #ifdef STORM_HAVE_Z3 std::cout << std::endl << "Generating minimal label counterexample for formula " << *formula << std::endl; diff --git a/src/logic/ComparisonType.h b/src/logic/ComparisonType.h index ccfff25b6..b91b2432b 100644 --- a/src/logic/ComparisonType.h +++ b/src/logic/ComparisonType.h @@ -5,16 +5,17 @@ namespace storm { namespace logic { - enum class ComparisonType { Less, LessEqual, Greater, GreaterEqual }; - - inline bool isStrict(ComparisonType t) { - return (t == ComparisonType::Less || t == ComparisonType::Greater); - } - - inline bool isLowerBound(ComparisonType t) { - return (t == ComparisonType::Greater || t == ComparisonType::GreaterEqual); - } - std::ostream& operator<<(std::ostream& out, ComparisonType const& comparisonType); + enum class ComparisonType { Less, LessEqual, Greater, GreaterEqual }; + + inline bool isStrict(ComparisonType t) { + return (t == ComparisonType::Less || t == ComparisonType::Greater); + } + + inline bool isLowerBound(ComparisonType t) { + return (t == ComparisonType::Greater || t == ComparisonType::GreaterEqual); + } + + std::ostream& operator<<(std::ostream& out, ComparisonType const& comparisonType); } } diff --git a/src/logic/OperatorFormula.cpp b/src/logic/OperatorFormula.cpp index 5997c957d..39fad071d 100644 --- a/src/logic/OperatorFormula.cpp +++ b/src/logic/OperatorFormula.cpp @@ -10,14 +10,22 @@ namespace storm { return static_cast(bound); } - ComparisonType const& OperatorFormula::getComparisonType() const { + ComparisonType OperatorFormula::getComparisonType() const { return comparisonType.get(); } + void OperatorFormula::setComparisonType(ComparisonType t) { + comparisonType = boost::optional(t); + } + double OperatorFormula::getBound() const { return bound.get(); } + void OperatorFormula::setBound(double b) { + bound = boost::optional(b); + } + bool OperatorFormula::hasOptimalityType() const { return static_cast(optimalityType); } diff --git a/src/logic/OperatorFormula.h b/src/logic/OperatorFormula.h index 8bdc14d21..a059ddb8b 100644 --- a/src/logic/OperatorFormula.h +++ b/src/logic/OperatorFormula.h @@ -18,8 +18,10 @@ namespace storm { } bool hasBound() const; - ComparisonType const& getComparisonType() const; + ComparisonType getComparisonType() const; + void setComparisonType(ComparisonType); double getBound() const; + void setBound(double); bool hasOptimalityType() const; OptimizationDirection const& getOptimalityType() const; diff --git a/src/python/helpers.h b/src/python/helpers.h index 9e96700e0..f37d350d9 100644 --- a/src/python/helpers.h +++ b/src/python/helpers.h @@ -7,10 +7,11 @@ void shared_ptr_implicitly_convertible() { boost::python::implicitly_convertible, std::shared_ptr>(); } - template void register_shared_ptr() { boost::python::register_ptr_to_python>(); + boost::python::register_ptr_to_python>(); + } diff --git a/src/python/storm-core.cpp b/src/python/storm-core.cpp index 60504d93e..4bde9ca91 100644 --- a/src/python/storm-core.cpp +++ b/src/python/storm-core.cpp @@ -18,7 +18,7 @@ public: // Thin wrapper for model building std::shared_ptr buildModel(storm::prism::Program const& program, std::shared_ptr const& formula) { - return storm::buildSymbolicModel(program, std::vector>(1,formula)).model; + return storm::buildSymbolicModel(program, std::vector>(1,formula)).model; } // Thin wrapper for parametric state elimination @@ -98,9 +98,6 @@ BOOST_PYTHON_MODULE(_core) defineClass, storm::models::sparse::Model>("SparseParametricDtmc", ""); defineClass, storm::models::sparse::Model>("SparseParametricMdp", ""); - defineClass>, void, void>("FormulaVec", "Vector of formulas") - .def(vector_indexing_suite>, true>()) - ; //////////////////////////////////////////// // Bisimulation @@ -109,7 +106,7 @@ BOOST_PYTHON_MODULE(_core) .value("STRONG", storm::storage::BisimulationType::Strong) .value("WEAK", storm::storage::BisimulationType::Weak) ; - def("perform_bisimulation_parametric", static_cast> (*)(std::shared_ptr> const&, std::shared_ptr const&, storm::storage::BisimulationType)>(&storm::performBisimulationMinimization>)); + def("perform_bisimulation_parametric", static_cast> (*)(std::shared_ptr> const&, std::shared_ptr const&, storm::storage::BisimulationType)>(&storm::performBisimulationMinimization>)); diff --git a/src/python/storm-logic.cpp b/src/python/storm-logic.cpp index a6da9725f..e2934859c 100644 --- a/src/python/storm-logic.cpp +++ b/src/python/storm-logic.cpp @@ -5,13 +5,24 @@ #include "helpers.h" #include "boostPyExtension.h" - +// Less, LessEqual, Greater, GreaterEqual BOOST_PYTHON_MODULE(_logic) { using namespace boost::python; + enum_("ComparisonType") + .value("LESS", storm::logic::ComparisonType::Less) + .value("LEQ", storm::logic::ComparisonType::LessEqual) + .value("GREATER", storm::logic::ComparisonType::Greater) + .value("GEQ", storm::logic::ComparisonType::GreaterEqual) + ; + + defineClass>, void, void>("FormulaVec", "Vector of formulas") + .def(vector_indexing_suite>, true>()) + ; + //////////////////////////////////////////// // Formula //////////////////////////////////////////// @@ -72,7 +83,11 @@ BOOST_PYTHON_MODULE(_logic) defineClass("UnaryBooleanStateFormula", ""); defineClass("OperatorFormula", - ""); + "") + .add_property("has_bound", &storm::logic::OperatorFormula::hasBound) + .add_property("bound", &storm::logic::OperatorFormula::getBound, &storm::logic::OperatorFormula::setBound) + .add_property("comparison_type", &storm::logic::OperatorFormula::getComparisonType, &storm::logic::OperatorFormula::setComparisonType) + ; defineClass("ExpectedTimeOperator", "The expected time between two events"); defineClass("LongRunAvarageOperator", diff --git a/src/storage/ModelFormulasPair.h b/src/storage/ModelFormulasPair.h index 57181a566..490116c46 100644 --- a/src/storage/ModelFormulasPair.h +++ b/src/storage/ModelFormulasPair.h @@ -10,7 +10,7 @@ namespace storm { namespace storage { struct ModelFormulasPair { std::shared_ptr model; - std::vector> formulas; + std::vector> formulas; }; } } \ No newline at end of file diff --git a/src/storage/bisimulation/BisimulationDecomposition.cpp b/src/storage/bisimulation/BisimulationDecomposition.cpp index b6158ed06..c8c47c5a8 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.cpp +++ b/src/storage/bisimulation/BisimulationDecomposition.cpp @@ -30,7 +30,7 @@ namespace storm { } template - BisimulationDecomposition::Options::Options(ModelType const& model, std::vector> const& formulas) : Options() { + BisimulationDecomposition::Options::Options(ModelType const& model, std::vector> const& formulas) : Options() { if (formulas.empty()) { this->respectedAtomicPropositions = model.getStateLabeling().getLabels(); this->keepRewards = true; diff --git a/src/storage/bisimulation/BisimulationDecomposition.h b/src/storage/bisimulation/BisimulationDecomposition.h index f7b2379de..420d528c9 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.h +++ b/src/storage/bisimulation/BisimulationDecomposition.h @@ -79,7 +79,7 @@ namespace storm { * derive a suitable initial partition. * @param formulas The formulas that need to be preserved. */ - Options(ModelType const& model, std::vector> const& formulas); + Options(ModelType const& model, std::vector> const& formulas); /*! * Changes the options in a way that the given formula is preserved. diff --git a/src/utility/storm.h b/src/utility/storm.h index 3ca286918..7ffba8c85 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -86,7 +86,7 @@ namespace storm { template - storm::storage::ModelFormulasPair buildSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { + storm::storage::ModelFormulasPair buildSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { storm::storage::ModelFormulasPair result; storm::prism::Program translatedProgram; @@ -136,7 +136,7 @@ namespace storm { } template - std::shared_ptr performDeterministicSparseBisimulationMinimization(std::shared_ptr model, std::vector> const& formulas, storm::storage::BisimulationType type) { + std::shared_ptr performDeterministicSparseBisimulationMinimization(std::shared_ptr model, std::vector> const& formulas, storm::storage::BisimulationType type) { std::cout << "Performing bisimulation minimization... "; typename storm::storage::DeterministicModelBisimulationDecomposition::Options options; if (!formulas.empty()) { @@ -152,7 +152,7 @@ namespace storm { } template - std::shared_ptr performNondeterministicSparseBisimulationMinimization(std::shared_ptr model, std::vector> const& formulas, storm::storage::BisimulationType type) { + std::shared_ptr performNondeterministicSparseBisimulationMinimization(std::shared_ptr model, std::vector> const& formulas, storm::storage::BisimulationType type) { std::cout << "Performing bisimulation minimization... "; typename storm::storage::DeterministicModelBisimulationDecomposition::Options options; if (!formulas.empty()) { @@ -169,7 +169,7 @@ namespace storm { } template - std::shared_ptr> performBisimulationMinimization(std::shared_ptr> const& model, std::vector> const& formulas, storm::storage::BisimulationType type) { + std::shared_ptr> performBisimulationMinimization(std::shared_ptr> const& model, std::vector> const& formulas, storm::storage::BisimulationType type) { using ValueType = typename ModelType::ValueType; STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Dtmc) || model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for DTMCs, CTMCs and MDPs."); @@ -185,14 +185,14 @@ namespace storm { } template - std::shared_ptr> performBisimulationMinimization(std::shared_ptr> const& model, std::shared_ptr const& formula, storm::storage::BisimulationType type) { - std::vector> formulas = { formula }; + std::shared_ptr> performBisimulationMinimization(std::shared_ptr> const& model, std::shared_ptr const& formula, storm::storage::BisimulationType type) { + std::vector> formulas = { formula }; return performBisimulationMinimization(model, formulas , type); } template - std::shared_ptr preprocessModel(std::shared_ptr model, std::vector> const& formulas) { + std::shared_ptr preprocessModel(std::shared_ptr model, std::vector> const& formulas) { if (model->isSparseModel() && storm::settings::generalSettings().isBisimulationSet()) { storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong; if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) { @@ -207,7 +207,7 @@ namespace storm { template - void generateCounterexample(storm::prism::Program const& program, std::shared_ptr> model, std::shared_ptr const& formula) { + void generateCounterexample(storm::prism::Program const& program, std::shared_ptr> model, std::shared_ptr const& formula) { if (storm::settings::counterexampleGeneratorSettings().isMinimalCommandSetGenerationSet()) { STORM_LOG_THROW(model->getType() == storm::models::ModelType::Mdp, storm::exceptions::InvalidTypeException, "Minimal command set generation is only available for MDPs."); STORM_LOG_THROW(storm::settings::generalSettings().isSymbolicSet(), storm::exceptions::InvalidSettingsException, "Minimal command set generation is only available for symbolic models."); @@ -230,13 +230,13 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - inline void generateCounterexample(storm::prism::Program const& program, std::shared_ptr> model, std::shared_ptr const& formula) { + inline void generateCounterexample(storm::prism::Program const& program, std::shared_ptr> model, std::shared_ptr const& formula) { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for parametric model."); } #endif template - std::unique_ptr verifyModel(std::shared_ptr model, std::shared_ptr const& formula) { + std::unique_ptr verifyModel(std::shared_ptr model, std::shared_ptr const& formula) { storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); switch(settings.getEngine()) { case storm::settings::modules::GeneralSettings::Engine::Sparse: { @@ -261,7 +261,7 @@ namespace storm { } template - std::unique_ptr verifySparseModel(std::shared_ptr> model, std::shared_ptr const& formula) { + std::unique_ptr verifySparseModel(std::shared_ptr> model, std::shared_ptr const& formula) { std::unique_ptr result; if (model->getType() == storm::models::ModelType::Dtmc) { @@ -317,7 +317,7 @@ namespace storm { } template<> - inline std::unique_ptr verifySparseModel(std::shared_ptr> model, std::shared_ptr const& formula) { + inline std::unique_ptr verifySparseModel(std::shared_ptr> model, std::shared_ptr const& formula) { std::unique_ptr result; std::shared_ptr> dtmc = model->template as>(); @@ -333,7 +333,7 @@ namespace storm { #endif template - std::unique_ptr verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::shared_ptr const& formula) { + std::unique_ptr verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::shared_ptr const& formula) { std::unique_ptr result; if (model->getType() == storm::models::ModelType::Dtmc) { std::shared_ptr> dtmc = model->template as>(); @@ -361,7 +361,7 @@ namespace storm { template - std::unique_ptr verifySymbolicModelWithDdEngine(std::shared_ptr> model, std::shared_ptr const& formula) { + std::unique_ptr verifySymbolicModelWithDdEngine(std::shared_ptr> model, std::shared_ptr const& formula) { std::unique_ptr result; if (model->getType() == storm::models::ModelType::Dtmc) { std::shared_ptr> dtmc = model->template as>(); diff --git a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp index 601851b05..b36983962 100644 --- a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp @@ -24,7 +24,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, 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()); - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); // Build the model. #ifdef WINDOWS @@ -107,7 +107,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, 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()); - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); // Build the model. #ifdef WINDOWS @@ -176,7 +176,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, 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()); - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); // Build the model. std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder().translateProgram(program); @@ -217,7 +217,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, 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()); - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); // Build the model. #ifdef WINDOWS diff --git a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp index d33a3f00e..7999da353 100644 --- a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp @@ -29,7 +29,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Die) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -73,7 +73,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -110,7 +110,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -153,7 +153,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -177,7 +177,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -201,7 +201,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -264,7 +264,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRA) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); diff --git a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp index 401402f6e..d5bd19fe2 100644 --- a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp @@ -27,7 +27,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Cudd) { // 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()); - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); // Build the model. #ifdef WINDOWS @@ -124,7 +124,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Sylvan) { // 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()); - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); // Build the model. #ifdef WINDOWS @@ -221,7 +221,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Cudd) { // 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()); - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); // Build the model. #ifdef WINDOWS @@ -300,7 +300,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Sylvan) { // 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()); - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); // Build the model. #ifdef WINDOWS @@ -379,7 +379,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Cudd) { // 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()); - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); // Build the model. std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program); @@ -415,7 +415,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Sylvan) { // 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()); - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); // Build the model. std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program); @@ -458,7 +458,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem_Cudd) { // 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()); - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); // Build the model with the customers reward structure. #ifdef WINDOWS @@ -546,7 +546,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem_Sylvan) { // 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()); - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); // Build the model with the customers reward structure. #ifdef WINDOWS diff --git a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp index bb7c2eb5a..6d0eac386 100644 --- a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp @@ -42,7 +42,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Cudd) { storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -103,7 +103,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Sylvan) { storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -156,7 +156,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Cudd) { storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -200,7 +200,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) { storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -252,7 +252,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) { storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -304,7 +304,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) { storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); diff --git a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp index 5b83e5558..06a236b4d 100644 --- a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp @@ -44,7 +44,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Cudd) { storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Gmmxx))); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -141,7 +141,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Sylvan) { storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Gmmxx))); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -238,7 +238,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Gmmxx))); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -317,7 +317,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Gmmxx))); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); diff --git a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index 9559c8423..23184f61f 100644 --- a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -30,7 +30,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Gmmxx))); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -146,7 +146,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Gmmxx))); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); diff --git a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp index bebc48930..72788de80 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()); - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); // Build the model. #ifdef WINDOWS @@ -98,7 +98,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()); - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); // Build the model. #ifdef WINDOWS @@ -160,7 +160,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()); - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); // Build the model. std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder().translateProgram(program); @@ -194,7 +194,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()); - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); // Build the model with the customers reward structure. #ifdef WINDOWS diff --git a/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp index 5f11f683f..6af4c51cc 100644 --- a/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp @@ -31,7 +31,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, Die) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -75,7 +75,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, Crowds) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -112,7 +112,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, SynchronousLeader) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -155,7 +155,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory(storm::solver::NativeLinearEquationSolverSolutionMethod::SOR, 0.9))); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -179,7 +179,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory(storm::solver::NativeLinearEquationSolverSolutionMethod::SOR, 0.9))); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -203,7 +203,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory(storm::solver::NativeLinearEquationSolverSolutionMethod::SOR, 0.9))); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -266,7 +266,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRA) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory(storm::solver::NativeLinearEquationSolverSolutionMethod::SOR, 0.9))); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); diff --git a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp index 65a8d4ec2..6b660acf8 100644 --- a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp @@ -26,7 +26,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Cudd) { // 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()); - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); // Build the model. #ifdef WINDOWS @@ -123,7 +123,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Sylvan) { // 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()); - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); // Build the model. #ifdef WINDOWS @@ -220,7 +220,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Cudd) { // 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()); - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); // Build the model. #ifdef WINDOWS @@ -299,7 +299,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Sylvan) { // 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()); - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); // Build the model. #ifdef WINDOWS @@ -378,7 +378,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Cudd) { // 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()); - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); // Build the model. std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program); @@ -414,7 +414,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Sylvan) { // 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()); - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); // Build the model. std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program); @@ -457,7 +457,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Cudd) { // 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()); - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); // Build the model with the customers reward structure. #ifdef WINDOWS @@ -547,7 +547,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Sylvan) { // 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()); - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); // Build the model with the customers reward structure. #ifdef WINDOWS diff --git a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp index 559979667..13c4f4f85 100644 --- a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp @@ -43,7 +43,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_Cudd) { storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -104,7 +104,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_Sylvan) { storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -157,7 +157,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_Cudd) { storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -201,7 +201,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) { storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -253,7 +253,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) { storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -305,7 +305,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) { storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); diff --git a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp index c66c5b6d2..40ce383c5 100644 --- a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp @@ -41,7 +41,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Cudd) { std::shared_ptr> mdp = model->as>(); storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -137,7 +137,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Sylvan) { std::shared_ptr> mdp = model->as>(); storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -234,7 +234,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -313,7 +313,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); diff --git a/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp index 0a61bb2ea..da5a2cd34 100644 --- a/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp @@ -29,7 +29,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -145,7 +145,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -209,7 +209,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -241,7 +241,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -282,7 +282,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -368,7 +368,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -490,7 +490,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); diff --git a/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp b/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp index 9c3347b72..7ce394070 100644 --- a/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp @@ -27,7 +27,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, Die) { storm::modelchecker::SparseDtmcEliminationModelChecker> checker(*dtmc); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -71,7 +71,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, Crowds) { storm::modelchecker::SparseDtmcEliminationModelChecker> checker(*dtmc); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -121,7 +121,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, SynchronousLeader) { storm::modelchecker::SparseDtmcEliminationModelChecker> checker(*dtmc); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); diff --git a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp index b8443686a..8f6c9c9e5 100644 --- a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp @@ -41,7 +41,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Cudd) { storm::modelchecker::SymbolicDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::SymbolicLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -102,7 +102,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Sylvan) { storm::modelchecker::SymbolicDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::SymbolicLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -156,7 +156,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Cudd) { storm::modelchecker::SymbolicDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::SymbolicLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -200,7 +200,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Sylvan) { storm::modelchecker::SymbolicDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::SymbolicLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -255,7 +255,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) { storm::modelchecker::SymbolicDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::SymbolicLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -307,7 +307,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) { storm::modelchecker::SymbolicDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::SymbolicLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); diff --git a/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp index 81c02ac38..a2486280d 100644 --- a/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp @@ -41,7 +41,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Cudd) { storm::modelchecker::SymbolicMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -138,7 +138,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Sylvan) { storm::modelchecker::SymbolicMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -235,7 +235,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { storm::modelchecker::SymbolicMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -314,7 +314,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { storm::modelchecker::SymbolicMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); diff --git a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp index e4251f819..17b1a871a 100644 --- a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp @@ -28,7 +28,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { storm::modelchecker::SparseMdpPrctlModelChecker> mc(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Topological))); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); std::unique_ptr result = mc.check(*formula); @@ -145,7 +145,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) { storm::modelchecker::SparseMdpPrctlModelChecker> mc(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Topological))); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); std::unique_ptr result = mc.check(*formula); diff --git a/test/functional/parser/FormulaParserTest.cpp b/test/functional/parser/FormulaParserTest.cpp index ce80d873c..15f116125 100644 --- a/test/functional/parser/FormulaParserTest.cpp +++ b/test/functional/parser/FormulaParserTest.cpp @@ -7,7 +7,7 @@ TEST(FormulaParserTest, LabelTest) { storm::parser::FormulaParser formulaParser; std::string input = "\"label\""; - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); EXPECT_TRUE(formula->isAtomicLabelFormula()); @@ -17,7 +17,7 @@ TEST(FormulaParserTest, ComplexLabelTest) { storm::parser::FormulaParser formulaParser; std::string input = "!(\"a\" & \"b\") | \"a\" & !\"c\""; - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); EXPECT_TRUE(formula->isPropositionalFormula()); @@ -32,7 +32,7 @@ TEST(FormulaParserTest, ExpressionTest) { storm::parser::FormulaParser formulaParser(manager); std::string input = "!(x | y > 3)"; - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); EXPECT_TRUE(formula->isPropositionalFormula()); @@ -47,7 +47,7 @@ TEST(FormulaParserTest, LabelAndExpressionTest) { storm::parser::FormulaParser formulaParser(manager); std::string input = "!\"a\" | x | y > 3"; - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); EXPECT_TRUE(formula->isPropositionalFormula()); @@ -61,7 +61,7 @@ TEST(FormulaParserTest, ProbabilityOperatorTest) { storm::parser::FormulaParser formulaParser; std::string input = "P<0.9 [\"a\" U \"b\"]"; - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); EXPECT_TRUE(formula->isProbabilityOperatorFormula()); @@ -73,7 +73,7 @@ TEST(FormulaParserTest, RewardOperatorTest) { storm::parser::FormulaParser formulaParser; std::string input = "Rmin<0.9 [F \"a\"]"; - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); EXPECT_TRUE(formula->isRewardOperatorFormula()); @@ -93,7 +93,7 @@ TEST(FormulaParserTest, ConditionalProbabilityTest) { storm::parser::FormulaParser formulaParser; std::string input = "P<0.9 [F \"a\" || F \"b\"]"; - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); EXPECT_TRUE(formula->isProbabilityOperatorFormula()); @@ -105,7 +105,7 @@ TEST(FormulaParserTest, NestedPathFormulaTest) { storm::parser::FormulaParser formulaParser; std::string input = "P<0.9 [F X \"a\"]"; - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); EXPECT_TRUE(formula->isProbabilityOperatorFormula()); @@ -117,7 +117,7 @@ TEST(FormulaParserTest, CommentTest) { storm::parser::FormulaParser formulaParser; std::string input = "// This is a comment. And this is a commented out formula: P<=0.5 [ F \"a\" ] The next line contains the actual formula. \n P<=0.5 [ X \"b\" ] // Another comment \n // And again: another comment."; - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); EXPECT_TRUE(formula->isProbabilityOperatorFormula()); ASSERT_TRUE(formula->asProbabilityOperatorFormula().getSubformula().isNextFormula()); @@ -132,7 +132,7 @@ TEST(FormulaParserTest, WrongFormatTest) { storm::parser::FormulaParser formulaParser(manager); std::string input = "P>0.5 [ a ]"; - std::shared_ptr formula(nullptr); + std::shared_ptr formula(nullptr); EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException); input = "P=0.5 [F \"a\"]"; diff --git a/test/functional/storage/NondeterministicModelBisimulationDecompositionTest.cpp b/test/functional/storage/NondeterministicModelBisimulationDecompositionTest.cpp index e2207bebb..3754b03fd 100644 --- a/test/functional/storage/NondeterministicModelBisimulationDecompositionTest.cpp +++ b/test/functional/storage/NondeterministicModelBisimulationDecompositionTest.cpp @@ -43,7 +43,7 @@ TEST(NondeterministicModelBisimulationDecomposition, TwoDice) { // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); typename storm::storage::NondeterministicModelBisimulationDecomposition>::Options options2(*mdp, *formula); diff --git a/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index ee9889104..daf041ec7 100644 --- a/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -26,7 +26,7 @@ TEST(GmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Gmmxx))); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -84,7 +84,7 @@ TEST(GmxxMdpPrctlModelCheckerTest, Consensus) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Gmmxx))); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]"); std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); diff --git a/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp index a18916a80..f55a45d07 100644 --- a/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp @@ -27,7 +27,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -85,7 +85,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]"); std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); diff --git a/test/performance/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp b/test/performance/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp index 4de317610..b9f90f3b8 100644 --- a/test/performance/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp @@ -41,7 +41,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) { storm::modelchecker::SymbolicDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::SymbolicLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -93,7 +93,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) { storm::modelchecker::SymbolicDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::SymbolicLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -137,7 +137,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Cudd) { storm::modelchecker::SymbolicDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::SymbolicLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -181,7 +181,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Sylvan) { storm::modelchecker::SymbolicDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::SymbolicLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); diff --git a/test/performance/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp index ee0a7913c..fec7389c9 100644 --- a/test/performance/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp @@ -41,7 +41,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { storm::modelchecker::SymbolicMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -93,7 +93,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { storm::modelchecker::SymbolicMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -149,7 +149,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, CSMA_Cudd) { storm::modelchecker::SymbolicMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [ !\"collision_max_backoff\" U \"all_delivered\" ]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [ !\"collision_max_backoff\" U \"all_delivered\" ]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -206,7 +206,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, CSMA_Sylvan) { storm::modelchecker::SymbolicMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory())); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [ !\"collision_max_backoff\" U \"all_delivered\" ]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [ !\"collision_max_backoff\" U \"all_delivered\" ]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); diff --git a/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp index e8d62e1b3..578e04f42 100644 --- a/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp @@ -22,7 +22,7 @@ TEST(DISABLED_TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLea storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Topological))); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); @@ -69,7 +69,7 @@ TEST(DISABLED_TopologicalValueIterationMdpPrctlModelCheckerTest, Consensus) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Topological))); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]"); std::unique_ptr result = checker.check(*formula);