From 7b0b6fa333fe9d116906eb139fd49f9b2f1bf754 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 13 Jan 2017 17:42:34 +0100 Subject: [PATCH] fixed a formula parsing bug, corrected some result printing --- src/storm/builder/DdJaniModelBuilder.cpp | 4 +--- .../ExplicitQuantitativeCheckResult.cpp | 20 ++++++++++++------- .../results/HybridQuantitativeCheckResult.cpp | 8 +++++++- .../SymbolicQualitativeCheckResult.cpp | 8 +++++++- .../SymbolicQuantitativeCheckResult.cpp | 4 +++- src/storm/parser/ExpressionCreator.cpp | 1 - src/storm/parser/FormulaParserGrammar.cpp | 8 +++++--- src/storm/parser/FormulaParserGrammar.h | 1 + src/storm/utility/storm.cpp | 2 +- 9 files changed, 38 insertions(+), 18 deletions(-) diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp index 929595495..33ee40758 100644 --- a/src/storm/builder/DdJaniModelBuilder.cpp +++ b/src/storm/builder/DdJaniModelBuilder.cpp @@ -51,9 +51,7 @@ namespace storm { template DdJaniModelBuilder::Options::Options(std::vector> const& formulas) : buildAllLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() { - if (formulas.empty()) { - this->buildAllRewardModels = true; - } else { + if (!formulas.empty()) { for (auto const& formula : formulas) { this->preserveFormula(*formula); } diff --git a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp index ff46fc8f4..0392a37c5 100644 --- a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp @@ -208,14 +208,20 @@ namespace storm { if (valuesAsMap.size() >= 10 && minMaxSupported) { printAsRange = true; } else { - bool first = true; - for (auto const& element : valuesAsMap) { - if (!first) { - out << ", "; - } else { - first = false; + if (valuesAsMap.size() == 1) { + out << valuesAsMap.begin()->second; + } else { + out << "{"; + bool first = true; + for (auto const& element : valuesAsMap) { + if (!first) { + out << ", "; + } else { + first = false; + } + print(out, element.second); } - print(out, element.second); + out << "}"; } } } diff --git a/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp index 008dab7d1..a712f1125 100644 --- a/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp @@ -94,7 +94,13 @@ namespace storm { std::ostream& HybridQuantitativeCheckResult::writeToStream(std::ostream& out) const { uint64_t totalNumberOfStates = this->symbolicStates.getNonZeroCount() + this->explicitStates.getNonZeroCount(); - if (totalNumberOfStates < 10) { + if (totalNumberOfStates == 1) { + if (this->symbolicStates.isZero()) { + out << *this->explicitValues.begin(); + } else { + out << this->symbolicValues.getMax(); + } + } else if (totalNumberOfStates < 10) { out << "{"; bool first = true; if (!this->symbolicStates.isZero()) { diff --git a/src/storm/modelchecker/results/SymbolicQualitativeCheckResult.cpp b/src/storm/modelchecker/results/SymbolicQualitativeCheckResult.cpp index b638c031f..eb407eaa3 100644 --- a/src/storm/modelchecker/results/SymbolicQualitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/SymbolicQualitativeCheckResult.cpp @@ -73,7 +73,13 @@ namespace storm { template std::ostream& SymbolicQualitativeCheckResult::writeToStream(std::ostream& out) const { - if (states == truthValues) { + if (states.getNonZeroCount() == 1) { + if (truthValues.isZero()) { + out << "false"; + } else { + out << "true"; + } + } else if (states == truthValues) { out << "{true}" << std::endl; } else { if (truthValues.isZero()) { diff --git a/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp index f46c1dc68..6bd18f1b8 100644 --- a/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp @@ -59,7 +59,9 @@ namespace storm { template std::ostream& SymbolicQuantitativeCheckResult::writeToStream(std::ostream& out) const { - if (states.getNonZeroCount() < 10) { + if (states.getNonZeroCount() == 1) { + out << this->values.getMax(); + } else if (states.getNonZeroCount() < 10) { out << "{"; if (this->values.isZero()) { out << "0"; diff --git a/src/storm/parser/ExpressionCreator.cpp b/src/storm/parser/ExpressionCreator.cpp index 0be1846f4..6266206ef 100644 --- a/src/storm/parser/ExpressionCreator.cpp +++ b/src/storm/parser/ExpressionCreator.cpp @@ -228,7 +228,6 @@ namespace storm { } void ExpressionCreator::setIdentifierMapping(qi::symbols const* identifiers_) { - if (identifiers_ != nullptr) { createExpressions = true; identifiers = identifiers_; diff --git a/src/storm/parser/FormulaParserGrammar.cpp b/src/storm/parser/FormulaParserGrammar.cpp index 86b34f19f..537a7f899 100644 --- a/src/storm/parser/FormulaParserGrammar.cpp +++ b/src/storm/parser/FormulaParserGrammar.cpp @@ -16,8 +16,7 @@ namespace storm { // Register all variables so we can parse them in the expressions. for (auto variableTypePair : *constManager) { identifiers_.add(variableTypePair.first.getName(), variableTypePair.first); - } - + } // Set the identifier mapping to actually generate expressions. expressionParser.setIdentifierMapping(&identifiers_); @@ -54,7 +53,10 @@ namespace storm { atomicStateFormula = booleanLiteralFormula | labelFormula | expressionFormula | (qi::lit("(") > stateFormula > qi::lit(")")) | operatorFormula; atomicStateFormula.name("atomic state formula"); - notStateFormula = (-unaryBooleanOperator_ >> atomicStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createUnaryBooleanStateFormula, phoenix::ref(*this), qi::_2, qi::_1)]; + atomicStateFormulaWithoutExpression = booleanLiteralFormula | labelFormula | (qi::lit("(") > stateFormula > qi::lit(")")) | operatorFormula; + atomicStateFormula.name("atomic state formula without expression"); + + notStateFormula = (unaryBooleanOperator_ >> atomicStateFormulaWithoutExpression)[qi::_val = phoenix::bind(&FormulaParserGrammar::createUnaryBooleanStateFormula, phoenix::ref(*this), qi::_2, qi::_1)] | atomicStateFormula[qi::_val = qi::_1]; notStateFormula.name("negation formula"); eventuallyFormula = (qi::lit("F") >> -timeBound >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createEventuallyFormula, phoenix::ref(*this), qi::_1, qi::_r1, qi::_2)]; diff --git a/src/storm/parser/FormulaParserGrammar.h b/src/storm/parser/FormulaParserGrammar.h index c25e1394c..4bd546199 100644 --- a/src/storm/parser/FormulaParserGrammar.h +++ b/src/storm/parser/FormulaParserGrammar.h @@ -141,6 +141,7 @@ namespace storm { qi::rule(storm::logic::FormulaContext), Skipper> pathFormulaWithoutUntil; qi::rule(), Skipper> simplePathFormula; qi::rule(), Skipper> atomicStateFormula; + qi::rule(), Skipper> atomicStateFormulaWithoutExpression; qi::rule(), Skipper> operatorFormula; qi::rule label; qi::rule rewardModelName; diff --git a/src/storm/utility/storm.cpp b/src/storm/utility/storm.cpp index 8ad4283b1..1023d6aa6 100644 --- a/src/storm/utility/storm.cpp +++ b/src/storm/utility/storm.cpp @@ -75,7 +75,7 @@ namespace storm{ } std::vector parsePropertiesForPrismProgram(std::string const& inputString, storm::prism::Program const& program, boost::optional> const& propertyFilter) { - storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); + storm::parser::FormulaParser formulaParser(program); auto formulas = parseProperties(formulaParser, inputString, propertyFilter); return substituteConstantsInProperties(formulas, program.getConstantsSubstitution()); }