From d8191d8c6af5b304ebba09efe430dfb7437d0405 Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 27 Jan 2016 11:36:59 +0100 Subject: [PATCH] const formulae Former-commit-id: 910d7ca5392f710fac32fb044a35a8fc1d381fec --- src/builder/DdPrismModelBuilder.cpp | 2 +- src/builder/DdPrismModelBuilder.h | 2 +- src/builder/ExplicitPrismModelBuilder.cpp | 2 +- src/builder/ExplicitPrismModelBuilder.h | 2 +- src/cli/cli.cpp | 2 +- src/cli/entrypoints.h | 16 +- .../MILPMinimalLabelSetGenerator.h | 2 +- .../SMTMinimalCommandSetGenerator.h | 2 +- src/parser/FormulaParser.cpp | 194 +++++++++--------- src/parser/FormulaParser.h | 6 +- src/storage/ModelFormulasPair.h | 2 +- .../BisimulationDecomposition.cpp | 2 +- .../bisimulation/BisimulationDecomposition.h | 2 +- src/utility/storm.cpp | 6 +- src/utility/storm.h | 32 +-- .../GmmxxCtmcCslModelCheckerTest.cpp | 8 +- .../GmmxxDtmcPrctlModelCheckerTest.cpp | 14 +- .../GmmxxHybridCtmcCslModelCheckerTest.cpp | 16 +- .../GmmxxHybridDtmcPrctlModelCheckerTest.cpp | 12 +- .../GmmxxHybridMdpPrctlModelCheckerTest.cpp | 8 +- .../GmmxxMdpPrctlModelCheckerTest.cpp | 4 +- .../NativeCtmcCslModelCheckerTest.cpp | 8 +- .../NativeDtmcPrctlModelCheckerTest.cpp | 14 +- .../NativeHybridCtmcCslModelCheckerTest.cpp | 16 +- .../NativeHybridDtmcPrctlModelCheckerTest.cpp | 12 +- .../NativeHybridMdpPrctlModelCheckerTest.cpp | 8 +- .../NativeMdpPrctlModelCheckerTest.cpp | 14 +- .../SparseDtmcEliminationModelCheckerTest.cpp | 6 +- .../SymbolicDtmcPrctlModelCheckerTest.cpp | 12 +- .../SymbolicMdpPrctlModelCheckerTest.cpp | 8 +- ...ValueIterationMdpPrctlModelCheckerTest.cpp | 4 +- test/functional/parser/FormulaParserTest.cpp | 20 +- ...sticModelBisimulationDecompositionTest.cpp | 2 +- .../GmmxxMdpPrctlModelCheckerTest.cpp | 4 +- .../NativeMdpPrctlModelCheckerTest.cpp | 4 +- .../SymbolicDtmcPrctlModelCheckerTest.cpp | 8 +- .../SymbolicMdpPrctlModelCheckerTest.cpp | 8 +- ...ValueIterationMdpPrctlModelCheckerTest.cpp | 4 +- 38 files changed, 244 insertions(+), 244 deletions(-) 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..7e53dde92 100644 --- a/src/cli/cli.cpp +++ b/src/cli/cli.cpp @@ -220,7 +220,7 @@ 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> formulas; if (settings.isPropertySet()) { std::string properties = settings.getProperty(); 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/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp index e3c0c9718..96ceee55f 100644 --- a/src/parser/FormulaParser.cpp +++ b/src/parser/FormulaParser.cpp @@ -10,7 +10,7 @@ namespace storm { namespace parser { - class FormulaParserGrammar : public qi::grammar>(), Skipper> { + class FormulaParserGrammar : public qi::grammar>(), Skipper> { public: FormulaParserGrammar(std::shared_ptr const& manager = std::shared_ptr(new storm::expressions::ExpressionManager())); @@ -95,66 +95,66 @@ namespace storm { // they are to be replaced with. qi::symbols identifiers_; - qi::rule>(), Skipper> start; + qi::rule>(), Skipper> start; qi::rule, boost::optional, boost::optional>(), qi::locals, boost::optional, boost::optional>, Skipper> operatorInformation; - qi::rule(), Skipper> probabilityOperator; - qi::rule(), Skipper> rewardOperator; - qi::rule(), Skipper> expectedTimeOperator; - qi::rule(), Skipper> longRunAverageOperator; - - qi::rule(), Skipper> simpleFormula; - qi::rule(), Skipper> stateFormula; - qi::rule(), Skipper> pathFormula; - qi::rule(), Skipper> pathFormulaWithoutUntil; - qi::rule(), Skipper> simplePathFormula; - qi::rule(), Skipper> atomicStateFormula; - qi::rule(), Skipper> operatorFormula; + qi::rule(), Skipper> probabilityOperator; + qi::rule(), Skipper> rewardOperator; + qi::rule(), Skipper> expectedTimeOperator; + qi::rule(), Skipper> longRunAverageOperator; + + qi::rule(), Skipper> simpleFormula; + qi::rule(), Skipper> stateFormula; + qi::rule(), Skipper> pathFormula; + qi::rule(), Skipper> pathFormulaWithoutUntil; + qi::rule(), Skipper> simplePathFormula; + qi::rule(), Skipper> atomicStateFormula; + qi::rule(), Skipper> operatorFormula; qi::rule label; qi::rule rewardModelName; - qi::rule(), Skipper> andStateFormula; - qi::rule(), Skipper> orStateFormula; - qi::rule(), Skipper> notStateFormula; - qi::rule(), Skipper> labelFormula; - qi::rule(), Skipper> expressionFormula; - qi::rule(), qi::locals, Skipper> booleanLiteralFormula; - - qi::rule(), Skipper> conditionalFormula; - qi::rule(), Skipper> eventuallyFormula; - qi::rule(), Skipper> nextFormula; - qi::rule(), Skipper> globallyFormula; - qi::rule(), Skipper> untilFormula; + qi::rule(), Skipper> andStateFormula; + qi::rule(), Skipper> orStateFormula; + qi::rule(), Skipper> notStateFormula; + qi::rule(), Skipper> labelFormula; + qi::rule(), Skipper> expressionFormula; + qi::rule(), qi::locals, Skipper> booleanLiteralFormula; + + qi::rule(), Skipper> conditionalFormula; + qi::rule(), Skipper> eventuallyFormula; + qi::rule(), Skipper> nextFormula; + qi::rule(), Skipper> globallyFormula; + qi::rule(), Skipper> untilFormula; qi::rule, uint_fast64_t>(), Skipper> timeBound; - qi::rule(), Skipper> rewardPathFormula; - qi::rule(), Skipper> cumulativeRewardFormula; - qi::rule(), Skipper> reachabilityRewardFormula; - qi::rule(), Skipper> instantaneousRewardFormula; - qi::rule(), Skipper> longRunAverageRewardFormula; + qi::rule(), Skipper> rewardPathFormula; + qi::rule(), Skipper> cumulativeRewardFormula; + qi::rule(), Skipper> reachabilityRewardFormula; + qi::rule(), Skipper> instantaneousRewardFormula; + qi::rule(), Skipper> longRunAverageRewardFormula; // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser). boost::spirit::qi::real_parser> strict_double; // Methods that actually create the expression objects. - std::shared_ptr createInstantaneousRewardFormula(boost::variant const& timeBound) const; - std::shared_ptr createCumulativeRewardFormula(boost::variant const& timeBound) const; - std::shared_ptr createReachabilityRewardFormula(std::shared_ptr const& stateFormula) const; - std::shared_ptr createLongRunAverageRewardFormula() const; - std::shared_ptr createAtomicExpressionFormula(storm::expressions::Expression const& expression) const; - std::shared_ptr createBooleanLiteralFormula(bool literal) const; - std::shared_ptr createAtomicLabelFormula(std::string const& label) const; - std::shared_ptr createEventuallyFormula(boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& subformula) const; - std::shared_ptr createGloballyFormula(std::shared_ptr const& subformula) const; - std::shared_ptr createNextFormula(std::shared_ptr const& subformula) const; - std::shared_ptr createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& rightSubformula); - std::shared_ptr createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) const; - std::shared_ptr createLongRunAverageOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; - std::shared_ptr createRewardOperatorFormula(boost::optional const& rewardModelName, std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; - std::shared_ptr createExpectedTimeOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; - std::shared_ptr createProbabilityOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula); - std::shared_ptr createBinaryBooleanStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType); - std::shared_ptr createUnaryBooleanStateFormula(std::shared_ptr const& subformula, boost::optional const& operatorType); + std::shared_ptr createInstantaneousRewardFormula(boost::variant const& timeBound) const; + std::shared_ptr createCumulativeRewardFormula(boost::variant const& timeBound) const; + std::shared_ptr createReachabilityRewardFormula(std::shared_ptr const& stateFormula) const; + std::shared_ptr createLongRunAverageRewardFormula() const; + std::shared_ptr createAtomicExpressionFormula(storm::expressions::Expression const& expression) const; + std::shared_ptr createBooleanLiteralFormula(bool literal) const; + std::shared_ptr createAtomicLabelFormula(std::string const& label) const; + std::shared_ptr createEventuallyFormula(boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& subformula) const; + std::shared_ptr createGloballyFormula(std::shared_ptr const& subformula) const; + std::shared_ptr createNextFormula(std::shared_ptr const& subformula) const; + std::shared_ptr createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& rightSubformula); + std::shared_ptr createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) const; + std::shared_ptr createLongRunAverageOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; + std::shared_ptr createRewardOperatorFormula(boost::optional const& rewardModelName, std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; + std::shared_ptr createExpectedTimeOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; + std::shared_ptr createProbabilityOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula); + std::shared_ptr createBinaryBooleanStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType); + std::shared_ptr createUnaryBooleanStateFormula(std::shared_ptr const& subformula, boost::optional const& operatorType); // An error handler function. phoenix::function handler; @@ -182,18 +182,18 @@ namespace storm { return *this; } - std::shared_ptr FormulaParser::parseSingleFormulaFromString(std::string const& formulaString) const { - std::vector> formulas = parseFromString(formulaString); + std::shared_ptr FormulaParser::parseSingleFormulaFromString(std::string const& formulaString) const { + std::vector> formulas = parseFromString(formulaString); STORM_LOG_THROW(formulas.size() == 1, storm::exceptions::WrongFormatException, "Expected exactly one formula, but found " << formulas.size() << " instead."); return formulas.front(); } - std::vector> FormulaParser::parseFromFile(std::string const& filename) const { + std::vector> FormulaParser::parseFromFile(std::string const& filename) const { // Open file and initialize result. std::ifstream inputFileStream(filename, std::ios::in); STORM_LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file '" << filename << "'."); - std::vector> formulas; + std::vector> formulas; // Now try to parse the contents of the file. try { @@ -210,13 +210,13 @@ namespace storm { return formulas; } - std::vector> FormulaParser::parseFromString(std::string const& formulaString) const { + std::vector> FormulaParser::parseFromString(std::string const& formulaString) const { PositionIteratorType first(formulaString.begin()); PositionIteratorType iter = first; PositionIteratorType last(formulaString.end()); // Create empty result; - std::vector> result; + std::vector> result; // Create grammar. try { @@ -390,108 +390,108 @@ namespace storm { this->identifiers_.add(identifier, expression); } - std::shared_ptr FormulaParserGrammar::createInstantaneousRewardFormula(boost::variant const& timeBound) const { + std::shared_ptr FormulaParserGrammar::createInstantaneousRewardFormula(boost::variant const& timeBound) const { if (timeBound.which() == 0) { - return std::shared_ptr(new storm::logic::InstantaneousRewardFormula(static_cast(boost::get(timeBound)))); + return std::shared_ptr(new storm::logic::InstantaneousRewardFormula(static_cast(boost::get(timeBound)))); } else { double timeBoundAsDouble = boost::get(timeBound); STORM_LOG_THROW(timeBoundAsDouble >= 0, storm::exceptions::WrongFormatException, "Cumulative reward property must have non-negative bound."); - return std::shared_ptr(new storm::logic::InstantaneousRewardFormula(static_cast(timeBoundAsDouble))); + return std::shared_ptr(new storm::logic::InstantaneousRewardFormula(static_cast(timeBoundAsDouble))); } } - std::shared_ptr FormulaParserGrammar::createCumulativeRewardFormula(boost::variant const& timeBound) const { + std::shared_ptr FormulaParserGrammar::createCumulativeRewardFormula(boost::variant const& timeBound) const { if (timeBound.which() == 0) { - return std::shared_ptr(new storm::logic::CumulativeRewardFormula(static_cast(boost::get(timeBound)))); + return std::shared_ptr(new storm::logic::CumulativeRewardFormula(static_cast(boost::get(timeBound)))); } else { double timeBoundAsDouble = boost::get(timeBound); STORM_LOG_THROW(timeBoundAsDouble >= 0, storm::exceptions::WrongFormatException, "Cumulative reward property must have non-negative bound."); - return std::shared_ptr(new storm::logic::CumulativeRewardFormula(static_cast(timeBoundAsDouble))); + return std::shared_ptr(new storm::logic::CumulativeRewardFormula(static_cast(timeBoundAsDouble))); } } - std::shared_ptr FormulaParserGrammar::createReachabilityRewardFormula(std::shared_ptr const& stateFormula) const { - return std::shared_ptr(new storm::logic::ReachabilityRewardFormula(stateFormula)); + std::shared_ptr FormulaParserGrammar::createReachabilityRewardFormula(std::shared_ptr const& stateFormula) const { + return std::shared_ptr(new storm::logic::ReachabilityRewardFormula(stateFormula)); } - std::shared_ptr FormulaParserGrammar::createLongRunAverageRewardFormula() const { - return std::shared_ptr(new storm::logic::LongRunAverageRewardFormula()); + std::shared_ptr FormulaParserGrammar::createLongRunAverageRewardFormula() const { + return std::shared_ptr(new storm::logic::LongRunAverageRewardFormula()); } - std::shared_ptr FormulaParserGrammar::createAtomicExpressionFormula(storm::expressions::Expression const& expression) const { + std::shared_ptr FormulaParserGrammar::createAtomicExpressionFormula(storm::expressions::Expression const& expression) const { STORM_LOG_THROW(expression.hasBooleanType(), storm::exceptions::WrongFormatException, "Expected expression of boolean type."); - return std::shared_ptr(new storm::logic::AtomicExpressionFormula(expression)); + return std::shared_ptr(new storm::logic::AtomicExpressionFormula(expression)); } - std::shared_ptr FormulaParserGrammar::createBooleanLiteralFormula(bool literal) const { - return std::shared_ptr(new storm::logic::BooleanLiteralFormula(literal)); + std::shared_ptr FormulaParserGrammar::createBooleanLiteralFormula(bool literal) const { + return std::shared_ptr(new storm::logic::BooleanLiteralFormula(literal)); } - std::shared_ptr FormulaParserGrammar::createAtomicLabelFormula(std::string const& label) const { - return std::shared_ptr(new storm::logic::AtomicLabelFormula(label)); + std::shared_ptr FormulaParserGrammar::createAtomicLabelFormula(std::string const& label) const { + return std::shared_ptr(new storm::logic::AtomicLabelFormula(label)); } - std::shared_ptr FormulaParserGrammar::createEventuallyFormula(boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& subformula) const { + std::shared_ptr FormulaParserGrammar::createEventuallyFormula(boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& subformula) const { if (timeBound) { if (timeBound.get().which() == 0) { std::pair const& bounds = boost::get>(timeBound.get()); - return std::shared_ptr(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, bounds.first, bounds.second)); + return std::shared_ptr(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, bounds.first, bounds.second)); } else { - return std::shared_ptr(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, static_cast(boost::get(timeBound.get())))); + return std::shared_ptr(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, static_cast(boost::get(timeBound.get())))); } } else { - return std::shared_ptr(new storm::logic::EventuallyFormula(subformula)); + return std::shared_ptr(new storm::logic::EventuallyFormula(subformula)); } } - std::shared_ptr FormulaParserGrammar::createGloballyFormula(std::shared_ptr const& subformula) const { - return std::shared_ptr(new storm::logic::GloballyFormula(subformula)); + std::shared_ptr FormulaParserGrammar::createGloballyFormula(std::shared_ptr const& subformula) const { + return std::shared_ptr(new storm::logic::GloballyFormula(subformula)); } - std::shared_ptr FormulaParserGrammar::createNextFormula(std::shared_ptr const& subformula) const { - return std::shared_ptr(new storm::logic::NextFormula(subformula)); + std::shared_ptr FormulaParserGrammar::createNextFormula(std::shared_ptr const& subformula) const { + return std::shared_ptr(new storm::logic::NextFormula(subformula)); } - std::shared_ptr FormulaParserGrammar::createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& rightSubformula) { + std::shared_ptr FormulaParserGrammar::createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& rightSubformula) { if (timeBound) { if (timeBound.get().which() == 0) { std::pair const& bounds = boost::get>(timeBound.get()); - return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, bounds.first, bounds.second)); + return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, bounds.first, bounds.second)); } else { - return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, static_cast(boost::get(timeBound.get())))); + return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, static_cast(boost::get(timeBound.get())))); } } else { - return std::shared_ptr(new storm::logic::UntilFormula(leftSubformula, rightSubformula)); + return std::shared_ptr(new storm::logic::UntilFormula(leftSubformula, rightSubformula)); } } - std::shared_ptr FormulaParserGrammar::createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) const { - return std::shared_ptr(new storm::logic::ConditionalPathFormula(leftSubformula, rightSubformula)); + std::shared_ptr FormulaParserGrammar::createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) const { + return std::shared_ptr(new storm::logic::ConditionalPathFormula(leftSubformula, rightSubformula)); } - std::shared_ptr FormulaParserGrammar::createLongRunAverageOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const { - return std::shared_ptr(new storm::logic::LongRunAverageOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); + std::shared_ptr FormulaParserGrammar::createLongRunAverageOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const { + return std::shared_ptr(new storm::logic::LongRunAverageOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); } - std::shared_ptr FormulaParserGrammar::createRewardOperatorFormula(boost::optional const& rewardModelName, std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const { - return std::shared_ptr(new storm::logic::RewardOperatorFormula(rewardModelName, std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); + std::shared_ptr FormulaParserGrammar::createRewardOperatorFormula(boost::optional const& rewardModelName, std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const { + return std::shared_ptr(new storm::logic::RewardOperatorFormula(rewardModelName, std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); } - std::shared_ptr FormulaParserGrammar::createExpectedTimeOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const { - return std::shared_ptr(new storm::logic::ExpectedTimeOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); + std::shared_ptr FormulaParserGrammar::createExpectedTimeOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const { + return std::shared_ptr(new storm::logic::ExpectedTimeOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); } - std::shared_ptr FormulaParserGrammar::createProbabilityOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) { - return std::shared_ptr(new storm::logic::ProbabilityOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); + std::shared_ptr FormulaParserGrammar::createProbabilityOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) { + return std::shared_ptr(new storm::logic::ProbabilityOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); } - std::shared_ptr FormulaParserGrammar::createBinaryBooleanStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType) { - return std::shared_ptr(new storm::logic::BinaryBooleanStateFormula(operatorType, leftSubformula, rightSubformula)); + std::shared_ptr FormulaParserGrammar::createBinaryBooleanStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType) { + return std::shared_ptr(new storm::logic::BinaryBooleanStateFormula(operatorType, leftSubformula, rightSubformula)); } - std::shared_ptr FormulaParserGrammar::createUnaryBooleanStateFormula(std::shared_ptr const& subformula, boost::optional const& operatorType) { + std::shared_ptr FormulaParserGrammar::createUnaryBooleanStateFormula(std::shared_ptr const& subformula, boost::optional const& operatorType) { if (operatorType) { - return std::shared_ptr(new storm::logic::UnaryBooleanStateFormula(operatorType.get(), subformula)); + return std::shared_ptr(new storm::logic::UnaryBooleanStateFormula(operatorType.get(), subformula)); } else { return subformula; } diff --git a/src/parser/FormulaParser.h b/src/parser/FormulaParser.h index 68ee3c5ab..b791e96fc 100644 --- a/src/parser/FormulaParser.h +++ b/src/parser/FormulaParser.h @@ -31,7 +31,7 @@ namespace storm { * @param formulaString The formula as a string. * @return The resulting formula. */ - std::shared_ptr parseSingleFormulaFromString(std::string const& formulaString) const; + std::shared_ptr parseSingleFormulaFromString(std::string const& formulaString) const; /*! * Parses the formula given by the provided string. @@ -39,7 +39,7 @@ namespace storm { * @param formulaString The formula as a string. * @return The contained formulas. */ - std::vector> parseFromString(std::string const& formulaString) const; + std::vector> parseFromString(std::string const& formulaString) const; /*! * Parses the formulas in the given file. @@ -47,7 +47,7 @@ namespace storm { * @param filename The name of the file to parse. * @return The contained formulas. */ - std::vector> parseFromFile(std::string const& filename) const; + std::vector> parseFromFile(std::string const& filename) const; /*! * Adds an identifier and the expression it is supposed to be replaced with. This can, for example be used 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.cpp b/src/utility/storm.cpp index a690af6f8..9a00c8f2c 100644 --- a/src/utility/storm.cpp +++ b/src/utility/storm.cpp @@ -19,7 +19,7 @@ namespace storm { * @param FormulaParser * @return The formulas. */ - std::vector> parseFormulas(storm::parser::FormulaParser & formulaParser, std::string const& inputString) { + std::vector> parseFormulas(storm::parser::FormulaParser & formulaParser, std::string const& inputString) { // If the given property looks like a file (containing a dot and there exists a file with that name), // we try to parse it as a file, otherwise we assume it's a property. if (inputString.find(".") != std::string::npos && std::ifstream(inputString).good()) { @@ -29,12 +29,12 @@ namespace storm { } } - std::vector> parseFormulasForExplicit(std::string const& inputString) { + std::vector> parseFormulasForExplicit(std::string const& inputString) { storm::parser::FormulaParser formulaParser; return parseFormulas(formulaParser, inputString); } - std::vector> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program) { + std::vector> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program) { storm::parser::FormulaParser formulaParser(program); return parseFormulas(formulaParser, inputString); } diff --git a/src/utility/storm.h b/src/utility/storm.h index 3ca286918..6e4e82a18 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -81,12 +81,12 @@ namespace storm { } storm::prism::Program parseProgram(std::string const& path); - std::vector> parseFormulasForExplicit(std::string const& inputString); - std::vector> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program); + std::vector> parseFormulasForExplicit(std::string const& inputString); + std::vector> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program); 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);