diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index e265f70c5..f53d0fd23 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 279548172..3a468d6bc 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 d5b8660b2..687e9fb41 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -79,7 +79,7 @@ namespace storm { } template - ExplicitPrismModelBuilder::Options::Options(std::vector> const& formulas) : explorationOrder(storm::settings::generalSettings().getExplorationOrder()), buildCommandLabels(false), buildAllRewardModels(false), buildStateValuations(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() { + ExplicitPrismModelBuilder::Options::Options(std::vector> const& formulas) : explorationOrder(storm::settings::generalSettings().getExplorationOrder()), buildCommandLabels(false), buildAllRewardModels(false), buildStateValuations(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() { if (formulas.empty()) { this->buildAllRewardModels = true; this->buildAllLabels = true; @@ -489,4 +489,4 @@ namespace storm { template class ExplicitPrismModelBuilder, uint32_t>; #endif } -} \ No newline at end of file +} diff --git a/src/builder/ExplicitPrismModelBuilder.h b/src/builder/ExplicitPrismModelBuilder.h index bd00f1005..92de20f2f 100644 --- a/src/builder/ExplicitPrismModelBuilder.h +++ b/src/builder/ExplicitPrismModelBuilder.h @@ -88,7 +88,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 0b384b539..3b5a5fcc2 100644 --- a/src/cli/cli.cpp +++ b/src/cli/cli.cpp @@ -216,7 +216,7 @@ namespace storm { } // Then proceed to parsing the property (if given), since the model we are building may depend on the property. - std::vector> parsedFormulas; + std::vector> parsedFormulas; if (settings.isPropertySet()) { std::string properties = settings.getProperty(); @@ -227,7 +227,7 @@ namespace storm { } } - std::vector> formulas(parsedFormulas.begin(), parsedFormulas.end()); + std::vector> formulas(parsedFormulas.begin(), parsedFormulas.end()); if (settings.isSymbolicSet()) { #ifdef STORM_HAVE_CARL @@ -247,4 +247,4 @@ namespace storm { } } - } \ No newline at end of file + } diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h index 8748c5a17..c1f88a9b4 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, bool onlyInitialStatesRelevant = false) { + void verifySparseModel(std::shared_ptr> model, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { for (auto const& formula : formulas) { std::cout << std::endl << "Model checking property: " << *formula << " ..."; std::unique_ptr result(storm::verifySparseModel(model, formula, onlyInitialStatesRelevant)); @@ -26,7 +26,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - inline void verifySparseModel(std::shared_ptr> model, std::vector> const& formulas, bool onlyInitialStatesRelevant) { + inline void verifySparseModel(std::shared_ptr> model, std::vector> const& formulas, bool onlyInitialStatesRelevant) { 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, bool onlyInitialStatesRelevant = false) { + void verifySymbolicModelWithAbstractionRefinementEngine(storm::prism::Program const& program, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Abstraction Refinement is not yet implemented."); } template - void verifySymbolicModelWithExplorationEngine(storm::prism::Program const& program, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { + void verifySymbolicModelWithExplorationEngine(storm::prism::Program const& program, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { for (auto const& formula : formulas) { STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::InvalidSettingsException, "Currently exploration-based verification is only available for DTMCs and MDPs."); @@ -80,13 +80,13 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - void verifySymbolicModelWithExplorationEngine(storm::prism::Program const& program, std::vector> const& formulas, bool onlyInitialStatesRelevant) { + void verifySymbolicModelWithExplorationEngine(storm::prism::Program const& program, std::vector> const& formulas, bool onlyInitialStatesRelevant) { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Exploration-based verification does currently not support parametric models."); } #endif template - void verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { + void verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { for (auto const& formula : formulas) { std::cout << std::endl << "Model checking property: " << *formula << " ..."; std::unique_ptr result(storm::verifySymbolicModelWithHybridEngine(model, formula, onlyInitialStatesRelevant)); @@ -103,7 +103,7 @@ namespace storm { } template - void verifySymbolicModelWithSymbolicEngine(std::shared_ptr> model, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { + void verifySymbolicModelWithSymbolicEngine(std::shared_ptr> model, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { for (auto const& formula : formulas) { std::cout << std::endl << "Model checking property: " << *formula << " ..."; std::unique_ptr result(storm::verifySymbolicModelWithDdEngine(model, formula, onlyInitialStatesRelevant)); @@ -145,7 +145,7 @@ namespace storm { } template - void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { + void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); @@ -191,7 +191,7 @@ namespace storm { } template - void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { + void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { if (storm::settings::generalSettings().getDdLibraryType() == storm::dd::DdType::CUDD) { buildAndCheckSymbolicModel(program, formulas, onlyInitialStatesRelevant); } else if (storm::settings::generalSettings().getDdLibraryType() == storm::dd::DdType::Sylvan) { @@ -200,7 +200,7 @@ namespace storm { } template - void buildAndCheckExplicitModel(std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { + void buildAndCheckExplicitModel(std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { 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 ffc398e34..3c805d7fe 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -974,7 +974,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 f7a2704b5..6cf9e9e8a 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 dd0137d9a..80aa2f421 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())); @@ -106,66 +106,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>, Skipper> operatorInformation; qi::rule rewardMeasureType; - qi::rule(), Skipper> probabilityOperator; - qi::rule(), Skipper> rewardOperator; - qi::rule(), Skipper> timeOperator; - qi::rule(), Skipper> longRunAverageOperator; - - qi::rule(), Skipper> simpleFormula; - qi::rule(), Skipper> stateFormula; - qi::rule(storm::logic::FormulaContext), Skipper> pathFormula; - qi::rule(storm::logic::FormulaContext), 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> timeOperator; + qi::rule(), Skipper> longRunAverageOperator; + + qi::rule(), Skipper> simpleFormula; + qi::rule(), Skipper> stateFormula; + qi::rule(storm::logic::FormulaContext), Skipper> pathFormula; + qi::rule(storm::logic::FormulaContext), 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(storm::logic::FormulaContext), Skipper> conditionalFormula; - qi::rule(storm::logic::FormulaContext), Skipper> eventuallyFormula; - qi::rule(storm::logic::FormulaContext), Skipper> nextFormula; - qi::rule(storm::logic::FormulaContext), Skipper> globallyFormula; - qi::rule(storm::logic::FormulaContext), 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(storm::logic::FormulaContext), Skipper> conditionalFormula; + qi::rule(storm::logic::FormulaContext), Skipper> eventuallyFormula; + qi::rule(storm::logic::FormulaContext), Skipper> nextFormula; + qi::rule(storm::logic::FormulaContext), Skipper> globallyFormula; + qi::rule(storm::logic::FormulaContext), Skipper> untilFormula; qi::rule, uint_fast64_t>(), Skipper> timeBound; - qi::rule(), Skipper> rewardPathFormula; - qi::rule(), Skipper> cumulativeRewardFormula; - qi::rule(), Skipper> instantaneousRewardFormula; - qi::rule(), Skipper> longRunAverageRewardFormula; + qi::rule(), Skipper> rewardPathFormula; + qi::rule(), Skipper> cumulativeRewardFormula; + 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 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, storm::logic::FormulaContext context, 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, storm::logic::FormulaContext context) const; + std::shared_ptr createInstantaneousRewardFormula(boost::variant const& timeBound) const; + std::shared_ptr createCumulativeRewardFormula(boost::variant const& timeBound) 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, storm::logic::FormulaContext context, 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, storm::logic::FormulaContext context) const; storm::logic::OperatorInformation createOperatorInformation(boost::optional const& optimizationDirection, boost::optional const& comparisonType, boost::optional const& threshold) const; - std::shared_ptr createLongRunAverageOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const; - std::shared_ptr createRewardOperatorFormula(boost::optional const& rewardMeasureType, boost::optional const& rewardModelName, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const; - std::shared_ptr createTimeOperatorFormula(boost::optional const& rewardMeasureType, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const; - std::shared_ptr createProbabilityOperatorFormula(storm::logic::OperatorInformation 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 createLongRunAverageOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const; + std::shared_ptr createRewardOperatorFormula(boost::optional const& rewardMeasureType, boost::optional const& rewardModelName, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const; + std::shared_ptr createTimeOperatorFormula(boost::optional const& rewardMeasureType, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const; + std::shared_ptr createProbabilityOperatorFormula(storm::logic::OperatorInformation 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; @@ -193,18 +193,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 { @@ -221,13 +221,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 { @@ -399,79 +399,79 @@ 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::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, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const { + std::shared_ptr FormulaParserGrammar::createEventuallyFormula(boost::optional, uint_fast64_t>> const& timeBound, storm::logic::FormulaContext context, 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, context)); + return std::shared_ptr(new storm::logic::EventuallyFormula(subformula, context)); } } - 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, storm::logic::FormulaContext context) const { - return std::shared_ptr(new storm::logic::ConditionalFormula(leftSubformula, rightSubformula, context)); + std::shared_ptr FormulaParserGrammar::createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::FormulaContext context) const { + return std::shared_ptr(new storm::logic::ConditionalFormula(leftSubformula, rightSubformula, context)); } storm::logic::OperatorInformation FormulaParserGrammar::createOperatorInformation(boost::optional const& optimizationDirection, boost::optional const& comparisonType, boost::optional const& threshold) const { @@ -482,37 +482,37 @@ namespace storm { } } - std::shared_ptr FormulaParserGrammar::createLongRunAverageOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const { - return std::shared_ptr(new storm::logic::LongRunAverageOperatorFormula(subformula, operatorInformation)); + std::shared_ptr FormulaParserGrammar::createLongRunAverageOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const { + return std::shared_ptr(new storm::logic::LongRunAverageOperatorFormula(subformula, operatorInformation)); } - std::shared_ptr FormulaParserGrammar::createRewardOperatorFormula(boost::optional const& rewardMeasureType, boost::optional const& rewardModelName, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const { + std::shared_ptr FormulaParserGrammar::createRewardOperatorFormula(boost::optional const& rewardMeasureType, boost::optional const& rewardModelName, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const { storm::logic::RewardMeasureType measureType = storm::logic::RewardMeasureType::Expectation; if (rewardMeasureType) { measureType = rewardMeasureType.get(); } - return std::shared_ptr(new storm::logic::RewardOperatorFormula(subformula, rewardModelName, operatorInformation, measureType)); + return std::shared_ptr(new storm::logic::RewardOperatorFormula(subformula, rewardModelName, operatorInformation, measureType)); } - std::shared_ptr FormulaParserGrammar::createTimeOperatorFormula(boost::optional const& rewardMeasureType, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const { + std::shared_ptr FormulaParserGrammar::createTimeOperatorFormula(boost::optional const& rewardMeasureType, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const { storm::logic::RewardMeasureType measureType = storm::logic::RewardMeasureType::Expectation; if (rewardMeasureType) { measureType = rewardMeasureType.get(); } - return std::shared_ptr(new storm::logic::TimeOperatorFormula(subformula, operatorInformation, measureType)); + return std::shared_ptr(new storm::logic::TimeOperatorFormula(subformula, operatorInformation, measureType)); } - std::shared_ptr FormulaParserGrammar::createProbabilityOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) { - return std::shared_ptr(new storm::logic::ProbabilityOperatorFormula(subformula, operatorInformation)); + std::shared_ptr FormulaParserGrammar::createProbabilityOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) { + return std::shared_ptr(new storm::logic::ProbabilityOperatorFormula(subformula, operatorInformation)); } - 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..86570c4f6 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 fab8cb3d1..48af93f73 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 5c5b3e667..730480fd6 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.cpp +++ b/src/storage/bisimulation/BisimulationDecomposition.cpp @@ -33,7 +33,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 604d15ec3..2c4279f91 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.h +++ b/src/storage/bisimulation/BisimulationDecomposition.h @@ -80,7 +80,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..3f1c713b5 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,13 +29,13 @@ 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); } -} \ No newline at end of file +} diff --git a/src/utility/storm.h b/src/utility/storm.h index 6b1889484..74daf0fa2 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -86,12 +86,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; @@ -141,7 +141,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()) { @@ -157,7 +157,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()) { @@ -174,7 +174,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."); @@ -190,14 +190,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()) { @@ -212,7 +212,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."); @@ -235,13 +235,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, bool onlyInitialStatesRelevant) { + std::unique_ptr verifyModel(std::shared_ptr model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant) { storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); switch(settings.getEngine()) { case storm::settings::modules::GeneralSettings::Engine::Sparse: { @@ -266,7 +266,7 @@ namespace storm { } template - std::unique_ptr verifySparseModel(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant = false) { + std::unique_ptr verifySparseModel(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant = false) { std::unique_ptr result; storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); @@ -333,7 +333,7 @@ namespace storm { } template<> - inline std::unique_ptr verifySparseModel(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant) { + inline std::unique_ptr verifySparseModel(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant) { std::unique_ptr result; std::shared_ptr> dtmc = model->template as>(); @@ -350,7 +350,7 @@ namespace storm { #endif template - std::unique_ptr verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant = false) { + std::unique_ptr verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant = false) { std::unique_ptr result; storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); if (model->getType() == storm::models::ModelType::Dtmc) { @@ -379,7 +379,7 @@ namespace storm { template - std::unique_ptr verifySymbolicModelWithDdEngine(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant) { + std::unique_ptr verifySymbolicModelWithDdEngine(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant) { std::unique_ptr result; storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); if (model->getType() == storm::models::ModelType::Dtmc) { diff --git a/test/functional/logic/FragmentCheckerTest.cpp b/test/functional/logic/FragmentCheckerTest.cpp index bb5d358c9..0280844d3 100644 --- a/test/functional/logic/FragmentCheckerTest.cpp +++ b/test/functional/logic/FragmentCheckerTest.cpp @@ -9,7 +9,7 @@ TEST(FragmentCheckerTest, Propositional) { storm::logic::FragmentSpecification prop = storm::logic::propositional(); storm::parser::FormulaParser formulaParser; - std::shared_ptr formula; + std::shared_ptr formula; ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prop)); @@ -41,7 +41,7 @@ TEST(FragmentCheckerTest, Pctl) { storm::logic::FragmentSpecification pctl = storm::logic::pctl(); storm::parser::FormulaParser formulaParser; - std::shared_ptr formula; + std::shared_ptr formula; ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); EXPECT_TRUE(checker.conformsToSpecification(*formula, pctl)); @@ -61,7 +61,7 @@ TEST(FragmentCheckerTest, Prctl) { storm::logic::FragmentSpecification prctl = storm::logic::prctl(); storm::parser::FormulaParser formulaParser; - std::shared_ptr formula; + std::shared_ptr formula; ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); @@ -87,7 +87,7 @@ TEST(FragmentCheckerTest, Csl) { storm::logic::FragmentSpecification csl = storm::logic::csl(); storm::parser::FormulaParser formulaParser; - std::shared_ptr formula; + std::shared_ptr formula; ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); EXPECT_TRUE(checker.conformsToSpecification(*formula, csl)); @@ -110,7 +110,7 @@ TEST(FragmentCheckerTest, Csrl) { storm::logic::FragmentSpecification csrl = storm::logic::csrl(); storm::parser::FormulaParser formulaParser; - std::shared_ptr formula; + std::shared_ptr formula; ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl)); diff --git a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp index dc9512a38..39c10b59f 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(program).translate(); @@ -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 715489715..8b9550fa3 100644 --- a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp @@ -31,7 +31,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(); @@ -75,7 +75,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(); @@ -112,7 +112,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(); @@ -155,7 +155,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 = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -179,7 +179,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 = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -203,7 +203,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 = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -266,7 +266,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRA) { 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 = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -295,7 +295,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Conditional) { // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"target\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"target\"]"); std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); diff --git a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp index d5bd19fe2..fd32f5f20 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 @@ -625,4 +625,4 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem_Sylvan) { storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult7 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.9100373532, quantitativeCheckResult7.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.9100373532, quantitativeCheckResult7.getMax(), storm::settings::generalSettings().getPrecision()); -} \ No newline at end of file +} diff --git a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp index 6d0eac386..3f3254bdd 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 06a236b4d..06d09f758 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 22e7d8464..bcae93e2d 100644 --- a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -32,7 +32,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(); @@ -148,7 +148,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(); @@ -211,7 +211,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) { solverFactory->setPreferredTechnique(storm::solver::MinMaxTechniqueSelection::PolicyIteration); storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::move(solverFactory)); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"target\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"target\"]"); storm::modelchecker::CheckTask checkTask(*formula); checkTask.setProduceSchedulers(true); @@ -261,7 +261,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, tiny_rewards) { solverFactory->setPreferredTechnique(storm::solver::MinMaxTechniqueSelection::ValueIteration); storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::move(solverFactory)); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"target\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"target\"]"); storm::modelchecker::CheckTask checkTask(*formula); diff --git a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp index 0a1d8ee4c..f166dc34f 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(program).translate(); @@ -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 253417bad..7cb0fa66d 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 = 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 = 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 = 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 = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -279,4 +279,4 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRA) { EXPECT_NEAR(.79 / 3., quantitativeResult1[13], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.3 / 3., quantitativeResult1[14], storm::settings::nativeEquationSolverSettings().getPrecision()); } -} \ No newline at end of file +} diff --git a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp index 6b660acf8..8d098145a 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 @@ -628,4 +628,4 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Sylvan) { // FIXME: because of divergence, these results are not correct. // EXPECT_NEAR(0.9100373532, quantitativeCheckResult7.getMin(), storm::settings::generalSettings().getPrecision()); // EXPECT_NEAR(0.9100373532, quantitativeCheckResult7.getMax(), storm::settings::generalSettings().getPrecision()); -} \ No newline at end of file +} diff --git a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp index 13c4f4f85..488cc5b0c 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())); @@ -331,4 +331,4 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) { EXPECT_NEAR(1.0416666666666643, quantitativeResult3.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0416666666666643, quantitativeResult3.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); -} \ No newline at end of file +} diff --git a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp index 40ce383c5..e01cf5a26 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 85c38e505..e16c93e14 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 = 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 = 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 = 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 = 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 = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -516,4 +516,4 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) { EXPECT_NEAR(.79 / 3., quantitativeResult2[13], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.3 / 3., quantitativeResult2[14], storm::settings::nativeEquationSolverSettings().getPrecision()); } -} \ No newline at end of file +} diff --git a/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp b/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp index ad4d9ab3d..ff5e9da06 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/SparseExplorationModelCheckerTest.cpp b/test/functional/modelchecker/SparseExplorationModelCheckerTest.cpp index 0e7304f81..a9cf4c910 100644 --- a/test/functional/modelchecker/SparseExplorationModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseExplorationModelCheckerTest.cpp @@ -18,7 +18,7 @@ TEST(SparseExplorationModelCheckerTest, Dice) { storm::modelchecker::SparseExplorationModelChecker checker(program); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); std::unique_ptr result = checker.check(storm::modelchecker::CheckTask<>(*formula, true)); storm::modelchecker::ExplicitQuantitativeCheckResult const& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -70,7 +70,7 @@ TEST(SparseExplorationModelCheckerTest, AsynchronousLeader) { storm::modelchecker::SparseExplorationModelChecker checker(program); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); std::unique_ptr result = checker.check(storm::modelchecker::CheckTask<>(*formula, true)); storm::modelchecker::ExplicitQuantitativeCheckResult const& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); diff --git a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp index 8f6c9c9e5..29d6ef4e9 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())); @@ -333,4 +333,4 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) { EXPECT_NEAR(1.0416666666666643, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0416666666666643, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); -} \ No newline at end of file +} diff --git a/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp index a2486280d..ad26ef072 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())); @@ -369,4 +369,4 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { // FIXME: this precision bound is not really good. EXPECT_NEAR(4.2857, quantitativeResult6.getMin(), 100 * storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(4.2857, quantitativeResult6.getMax(), 100 * storm::settings::nativeEquationSolverSettings().getPrecision()); -} \ No newline at end of file +} diff --git a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp index 17b1a871a..d2a4420b7 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 a3d78632b..1435806eb 100644 --- a/test/functional/parser/FormulaParserTest.cpp +++ b/test/functional/parser/FormulaParserTest.cpp @@ -8,7 +8,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()); @@ -18,7 +18,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->isInFragment(storm::logic::propositional())); @@ -33,7 +33,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->isInFragment(storm::logic::propositional())); @@ -48,7 +48,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->isInFragment(storm::logic::propositional())); @@ -62,7 +62,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()); @@ -74,7 +74,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()); @@ -94,7 +94,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()); @@ -106,7 +106,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()); @@ -118,7 +118,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()); @@ -133,7 +133,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 fe0a199b7..65c5ef132 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); @@ -55,4 +55,4 @@ TEST(NondeterministicModelBisimulationDecomposition, TwoDice) { EXPECT_EQ(11ul, result->getNumberOfStates()); EXPECT_EQ(26ul, result->getNumberOfTransitions()); EXPECT_EQ(14ul, result->as>()->getNumberOfChoices()); -} \ No newline at end of file +} diff --git a/test/functional/utility/ModelInstantiatorTest.cpp b/test/functional/utility/ModelInstantiatorTest.cpp index 24512d886..e0b9765d1 100644 --- a/test/functional/utility/ModelInstantiatorTest.cpp +++ b/test/functional/utility/ModelInstantiatorTest.cpp @@ -27,7 +27,7 @@ TEST(ModelInstantiatorTest, BrpProb) { // Program and formula storm::prism::Program program = storm::parseProgram(programFile); program.checkValidity(); - std::vector> formulas = storm::parseFormulasForProgram(formulaAsString, program); + std::vector> formulas = storm::parseFormulasForProgram(formulaAsString, program); ASSERT_TRUE(formulas.size()==1); // Parametric model typename storm::builder::ExplicitPrismModelBuilder::Options options = storm::builder::ExplicitPrismModelBuilder::Options(*formulas[0]); @@ -148,7 +148,7 @@ TEST(ModelInstantiatorTest, Brp_Rew) { // Program and formula storm::prism::Program program = storm::parseProgram(programFile); program.checkValidity(); - std::vector> formulas = storm::parseFormulasForProgram(formulaAsString, program); + std::vector> formulas = storm::parseFormulasForProgram(formulaAsString, program); ASSERT_TRUE(formulas.size()==1); // Parametric model typename storm::builder::ExplicitPrismModelBuilder::Options options = storm::builder::ExplicitPrismModelBuilder::Options(*formulas[0]); @@ -221,7 +221,7 @@ TEST(ModelInstantiatorTest, Consensus) { // Program and formula storm::prism::Program program = storm::parseProgram(programFile); program.checkValidity(); - std::vector> formulas = storm::parseFormulasForProgram(formulaAsString, program); + std::vector> formulas = storm::parseFormulasForProgram(formulaAsString, program); ASSERT_TRUE(formulas.size()==1); // Parametric model typename storm::builder::ExplicitPrismModelBuilder::Options options = storm::builder::ExplicitPrismModelBuilder::Options(*formulas[0]); @@ -262,4 +262,4 @@ TEST(ModelInstantiatorTest, Consensus) { EXPECT_NEAR(0.3526577219, quantitativeChkResult[*instantiated.getInitialStates().begin()], storm::settings::generalSettings().getPrecision()); } -#endif \ No newline at end of file +#endif diff --git a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp index 4284ab85c..21b2ac15e 100644 --- a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp @@ -26,7 +26,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; - 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(); @@ -64,7 +64,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; - 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/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index daf041ec7..63832e20a 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/NativeDtmcPrctlModelCheckerTest.cpp b/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp index 85d6399c9..74b244f5b 100644 --- a/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp @@ -26,7 +26,7 @@ TEST(NativeDtmcPrctlModelCheckerTest, Crowds) { // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; - 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(); @@ -64,7 +64,7 @@ TEST(NativeDtmcPrctlModelCheckerTest, SynchronousLeader) { // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; - 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/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp index f55a45d07..5c3886631 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 b9f90f3b8..fc96aeaf3 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())); @@ -207,4 +207,4 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Sylvan) { EXPECT_NEAR(0.23773283919051694, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.23773283919051694, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); -} \ No newline at end of file +} diff --git a/test/performance/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp index fec7389c9..ad424a8f9 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())); @@ -234,4 +234,4 @@ TEST(SymbolicMdpPrctlModelCheckerTest, CSMA_Sylvan) { // FIXME: not optimal precision. EXPECT_NEAR(93.624117712294478, quantitativeResult5.getMin(), 100 * storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(93.624117712294478, quantitativeResult5.getMax(), 100 * storm::settings::nativeEquationSolverSettings().getPrecision()); -} \ No newline at end of file +} diff --git a/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp index 578e04f42..fa921b479 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); @@ -109,4 +109,4 @@ TEST(DISABLED_TopologicalValueIterationMdpPrctlModelCheckerTest, Consensus) { result = checker.check(*formula); ASSERT_NEAR(2183.142422, result->asExplicitQuantitativeCheckResult()[31168], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); -} \ No newline at end of file +}