fixed a formula parsing bug, corrected some result printing

src/storm/builder/DdJaniModelBuilder.cpp

@@ -51,9 +51,7 @@ namespace storm {
         
         template <storm::dd::DdType Type, typename ValueType>
         DdJaniModelBuilder<Type, ValueType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula const>> 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);
                 }

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 << "}";
                     }
                 }
             }

src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp

@@ -94,7 +94,13 @@ namespace storm {
         std::ostream& HybridQuantitativeCheckResult<Type, ValueType>::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()) {

src/storm/modelchecker/results/SymbolicQualitativeCheckResult.cpp

@@ -73,7 +73,13 @@ namespace storm {
         
         template <storm::dd::DdType Type>
         std::ostream& SymbolicQualitativeCheckResult<Type>::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()) {

src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp

@@ -59,7 +59,9 @@ namespace storm {
         
         template<storm::dd::DdType Type, typename ValueType>
         std::ostream& SymbolicQuantitativeCheckResult<Type, ValueType>::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";

src/storm/parser/ExpressionCreator.cpp

@@ -228,7 +228,6 @@ namespace storm {
         }
         
         void ExpressionCreator::setIdentifierMapping(qi::symbols<char, storm::expressions::Expression> const* identifiers_) {
-            
             if (identifiers_ != nullptr) {
                 createExpressions = true;
                 identifiers = identifiers_;

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)];

src/storm/parser/FormulaParserGrammar.h

@@ -141,6 +141,7 @@ namespace storm {
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> pathFormulaWithoutUntil;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> simplePathFormula;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> atomicStateFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> atomicStateFormulaWithoutExpression;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> operatorFormula;
             qi::rule<Iterator, std::string(), Skipper> label;
             qi::rule<Iterator, std::string(), Skipper> rewardModelName;

src/storm/utility/storm.cpp

@@ -75,7 +75,7 @@ namespace storm{
     }
     
     std::vector<storm::jani::Property> parsePropertiesForPrismProgram(std::string const& inputString, storm::prism::Program const& program, boost::optional<std::set<std::string>> 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());
     }