fixing more of Lindas issues

src/storm-cli-utilities/model-handling.h

@@ -131,6 +131,19 @@ namespace storm {
                 }
             }
             
+            // Make sure there are no undefined constants remaining in any property.
+            for (auto const& property : output.properties) {
+                std::set<storm::expressions::Variable> usedUndefinedConstants = property.getUndefinedConstants();
+                if (!usedUndefinedConstants.empty()) {
+                    std::vector<std::string> undefinedConstantsNames;
+                    for (auto const& constant : usedUndefinedConstants) {
+                        undefinedConstantsNames.emplace_back(constant.getName());
+                    }
+
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The property '" << property << " still refers to the undefined constants " << boost::algorithm::join(undefinedConstantsNames, ",") << ".");
+                }
+            }
+            
             // Check whether conversion for PRISM to JANI is requested or necessary.
             if (input.model && input.model.get().isPrismProgram()) {
                 bool transformToJani = ioSettings.isPrismToJaniSet();
@@ -567,6 +580,10 @@ namespace storm {
             expressionParser.setIdentifierMapping(variableMapping);
             
             for (auto const& constraintString : constraintsAsStrings) {
+                if (constraintString.empty()) {
+                    continue;
+                }
+
                 storm::expressions::Expression constraint = expressionParser.parseFromString(constraintString);
                 STORM_LOG_TRACE("Adding special (user-provided) constraint " << constraint << ".");
                 constraints.emplace_back(constraint);
@@ -588,25 +605,34 @@ namespace storm {
             std::vector<std::string> predicateGroupsAsStrings;
             boost::split(predicateGroupsAsStrings, refinementPredicatesString, boost::is_any_of(";"));
             
-            for (auto const& predicateGroupString : predicateGroupsAsStrings) {
-                std::vector<std::string> predicatesAsStrings;
-                boost::split(predicatesAsStrings, predicateGroupString, boost::is_any_of(":"));
-                
-                injectedRefinementPredicates.emplace_back();
-                for (auto const& predicateString : predicatesAsStrings) {
-                    storm::expressions::Expression predicate = expressionParser.parseFromString(predicateString);
-                    STORM_LOG_TRACE("Adding special (user-provided) refinement predicate " << predicateString << ".");
-                    injectedRefinementPredicates.back().emplace_back(predicate);
+            if (!predicateGroupsAsStrings.empty()) {
+                for (auto const& predicateGroupString : predicateGroupsAsStrings) {
+                    if (predicateGroupString.empty()) {
+                        continue;
+                    }
+                    
+                    std::vector<std::string> predicatesAsStrings;
+                    boost::split(predicatesAsStrings, predicateGroupString, boost::is_any_of(":"));
+                    
+                    if (!predicatesAsStrings.empty()) {
+                        injectedRefinementPredicates.emplace_back();
+                        for (auto const& predicateString : predicatesAsStrings) {
+                            storm::expressions::Expression predicate = expressionParser.parseFromString(predicateString);
+                            STORM_LOG_TRACE("Adding special (user-provided) refinement predicate " << predicateString << ".");
+                            injectedRefinementPredicates.back().emplace_back(predicate);
+                        }
+                        
+                        STORM_LOG_THROW(!injectedRefinementPredicates.back().empty(), storm::exceptions::InvalidArgumentException, "Expecting non-empty list of predicates to inject for each (mentioned) refinement step.");
+                        
+                        // Finally reverse the list, because we take the predicates from the back.
+                        std::reverse(injectedRefinementPredicates.back().begin(), injectedRefinementPredicates.back().end());
+                    }
                 }
-                STORM_LOG_THROW(!injectedRefinementPredicates.back().empty(), storm::exceptions::InvalidArgumentException, "Expecting non-empty list of predicates to inject for each (mentioned) refinement step.");
                 
                 // Finally reverse the list, because we take the predicates from the back.
-                std::reverse(injectedRefinementPredicates.back().begin(), injectedRefinementPredicates.back().end());
+                std::reverse(injectedRefinementPredicates.begin(), injectedRefinementPredicates.end());
             }
             
-            // Finally reverse the list, because we take the predicates from the back.
-            std::reverse(injectedRefinementPredicates.begin(), injectedRefinementPredicates.end());
-            
             return injectedRefinementPredicates;
         }
         

src/storm-dft/api/storm-dft.cpp

@@ -57,7 +57,7 @@ namespace storm {
 
                     auto evFormula = std::make_shared<storm::logic::EventuallyFormula>(evtlFormula, storm::logic::FormulaContext::Time);
                     auto rewFormula = std::make_shared<storm::logic::TimeOperatorFormula>(evFormula, storm::logic::OperatorInformation(), storm::logic::RewardMeasureType::Expectation);
-                    std::vector<storm::jani::Property> res({storm::jani::Property("time-bounded", tbUntil), storm::jani::Property("mttf", rewFormula)});
+                    std::vector<storm::jani::Property> res({storm::jani::Property("time-bounded", tbUntil, {}), storm::jani::Property("mttf", rewFormula, {})});
                     return res;
                 }
             );

src/storm-gspn/builder/JaniGSPNBuilder.cpp

@@ -275,11 +275,12 @@ namespace storm {
             auto const& deadlockVar = addDeadlockTransientVariable(model, getUniqueVarName(*expressionManager, "deadl"));
             auto deadlock = std::make_shared<storm::logic::AtomicExpressionFormula>(deadlockVar.getExpressionVariable().getExpression());
             auto trueFormula = std::make_shared<storm::logic::BooleanLiteralFormula>(true);
+            std::set<storm::expressions::Variable> emptyVariableSet;
             
             auto maxReachDeadlock = std::make_shared<storm::logic::ProbabilityOperatorFormula>(
                     std::make_shared<storm::logic::EventuallyFormula>(deadlock, storm::logic::FormulaContext::Probability),
                     storm::logic::OperatorInformation(storm::solver::OptimizationDirection::Maximize));
-            standardProperties.emplace_back("MaxPrReachDeadlock", maxReachDeadlock, "The maximal probability to eventually reach a deadlock.");
+            standardProperties.emplace_back("MaxPrReachDeadlock", maxReachDeadlock, emptyVariableSet, "The maximal probability to eventually reach a deadlock.");
             
             auto exprTB = expressionManager->declareRationalVariable(getUniqueVarName(*expressionManager, "TIME_BOUND"));
             auto janiTB = storm::jani::Constant(exprTB.getName(), exprTB);
@@ -289,15 +290,15 @@ namespace storm {
             auto maxReachDeadlockTimeBounded = std::make_shared<storm::logic::ProbabilityOperatorFormula>(
                     std::make_shared<storm::logic::BoundedUntilFormula>(trueFormula, deadlock, boost::none, tb, tbr),
                     storm::logic::OperatorInformation(storm::solver::OptimizationDirection::Maximize));
-            standardProperties.emplace_back("MaxPrReachDeadlockTB", maxReachDeadlockTimeBounded, "The maximal probability to reach a deadlock within 'TIME_BOUND' steps.");
+            standardProperties.emplace_back("MaxPrReachDeadlockTB", maxReachDeadlockTimeBounded, emptyVariableSet, "The maximal probability to reach a deadlock within 'TIME_BOUND' steps.");
             
             auto expTimeDeadlock = std::make_shared<storm::logic::TimeOperatorFormula>(
                     std::make_shared<storm::logic::EventuallyFormula>(deadlock, storm::logic::FormulaContext::Time),
                     storm::logic::OperatorInformation(storm::solver::OptimizationDirection::Maximize));
-            standardProperties.emplace_back("MinExpTimeDeadlock", expTimeDeadlock, "The minimal expected time to reach a deadlock.");
+            standardProperties.emplace_back("MinExpTimeDeadlock", expTimeDeadlock, emptyVariableSet, "The minimal expected time to reach a deadlock.");
             
         }
 
         
     }
-}
+}

src/storm-parsers/parser/FormulaParserGrammar.cpp

@@ -224,6 +224,7 @@ namespace storm {
             if (expression) {
                 addIdentifierExpression(name, expression.get());
             } else {
+                undefinedConstants.insert(newVariable);
                 addIdentifierExpression(name, newVariable);
             }
         }
@@ -417,24 +418,31 @@ namespace storm {
                 return std::shared_ptr<storm::logic::Formula const>(new storm::logic::MultiObjectiveFormula(subformulas));
             }
         }
-                                               
+        
+        std::set<storm::expressions::Variable> FormulaParserGrammar::getUndefinedConstants(std::shared_ptr<storm::logic::Formula const> const& formula) const {
+            std::set<storm::expressions::Variable> result;
+            std::set<storm::expressions::Variable> usedVariables = formula->getUsedVariables();
+            std::set_intersection(usedVariables.begin(), usedVariables.end(), undefinedConstants.begin(), undefinedConstants.end(), std::inserter(result, result.begin()));
+            return result;
+        }
+        
         storm::jani::Property FormulaParserGrammar::createProperty(boost::optional<std::string> const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
             storm::jani::FilterExpression filterExpression(formula, filterType, states);
             
             ++propertyCount;
             if (propertyName) {
-                return storm::jani::Property(propertyName.get(), filterExpression);
+                return storm::jani::Property(propertyName.get(), filterExpression, this->getUndefinedConstants(formula));
             } else {
-                return storm::jani::Property(std::to_string(propertyCount -1 ), filterExpression);
+                return storm::jani::Property(std::to_string(propertyCount - 1), filterExpression, this->getUndefinedConstants(formula));
             }
         }
                                                
         storm::jani::Property FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates(boost::optional<std::string> const& propertyName, std::shared_ptr<storm::logic::Formula const> const& formula) {
             ++propertyCount;
             if (propertyName) {
-                return storm::jani::Property(propertyName.get(), formula);
+                return storm::jani::Property(propertyName.get(), formula, this->getUndefinedConstants(formula));
             } else {
-                return storm::jani::Property(std::to_string(propertyCount), formula);
+                return storm::jani::Property(std::to_string(propertyCount), formula, this->getUndefinedConstants(formula));
             }
         }
 

src/storm-parsers/parser/FormulaParserGrammar.h

@@ -230,6 +230,7 @@ namespace storm {
             std::shared_ptr<storm::logic::Formula const> createUnaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula const> const& subformula, boost::optional<storm::logic::UnaryBooleanStateFormula::OperatorType> const& operatorType);
             std::shared_ptr<storm::logic::Formula const> createMultiFormula(std::vector<std::shared_ptr<storm::logic::Formula const>> const& subformulas);
             
+            std::set<storm::expressions::Variable> getUndefinedConstants(std::shared_ptr<storm::logic::Formula const> const& formula) const;
             storm::jani::Property createProperty(boost::optional<std::string> const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states);
             storm::jani::Property createPropertyWithDefaultFilterTypeAndStates(boost::optional<std::string> const& propertyName, std::shared_ptr<storm::logic::Formula const> const& formula);
             
@@ -237,6 +238,8 @@ namespace storm {
             phoenix::function<SpiritErrorHandler> handler;
             
             uint64_t propertyCount;
+            
+            std::set<storm::expressions::Variable> undefinedConstants;
         };
 
     }

src/storm-parsers/parser/JaniParser.cpp

@@ -560,7 +560,7 @@ namespace storm {
             STORM_LOG_THROW(statesFormula, storm::exceptions::NotImplementedException, "Could not derive states formula.");
             STORM_LOG_THROW(expressionStructure.count("values") == 1, storm::exceptions::InvalidJaniException, "Values as input for a filter must be given");
             auto formula = parseFormula(expressionStructure.at("values"), storm::logic::FormulaContext::Undefined, globalVars, constants, "Values of property " + name);
-            return storm::jani::Property(name, storm::jani::FilterExpression(formula, ft, statesFormula), comment);
+            return storm::jani::Property(name, storm::jani::FilterExpression(formula, ft, statesFormula), {}, comment);
         }
 
         std::shared_ptr<storm::jani::Constant> JaniParser::parseConstant(json const& constantStructure, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::string const& scopeDescription) {

src/storm/logic/BoundedUntilFormula.cpp

@@ -89,14 +89,22 @@ namespace storm {
                 for (unsigned i = 0; i < this->getDimension(); ++i) {
                     this->getLeftSubformula(i).gatherUsedVariables(usedVariables);
                     this->getRightSubformula(i).gatherUsedVariables(usedVariables);
-                    this->getLowerBound(i).gatherVariables(usedVariables);
-                    this->getUpperBound(i).gatherVariables(usedVariables);
+                    if (this->hasLowerBound(i)) {
+                        this->getLowerBound(i).gatherVariables(usedVariables);
+                    }
+                    if (this->hasUpperBound(i)) {
+                        this->getUpperBound(i).gatherVariables(usedVariables);
+                    }
                 }
             } else {
                 this->getLeftSubformula().gatherUsedVariables(usedVariables);
                 this->getRightSubformula().gatherUsedVariables(usedVariables);
-                this->getLowerBound().gatherVariables(usedVariables);
-                this->getUpperBound().gatherVariables(usedVariables);
+                if (this->hasLowerBound()) {
+                    this->getLowerBound().gatherVariables(usedVariables);
+                }
+                if (this->hasUpperBound()) {
+                    this->getUpperBound().gatherVariables(usedVariables);
+                }
             }
         }
         

src/storm/logic/OperatorFormula.cpp

@@ -86,7 +86,10 @@ namespace storm {
         }
         
         void OperatorFormula::gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const {
-            this->getThreshold().gatherVariables(usedVariables);
+            UnaryStateFormula::gatherUsedVariables(usedVariables);
+            if (this->hasBound()) {
+                this->getThreshold().gatherVariables(usedVariables);
+            }
         }
         
         std::ostream& OperatorFormula::writeToStream(std::ostream& out) const {

src/storm/logic/RewardAccumulationEliminationVisitor.cpp

@@ -25,7 +25,7 @@ namespace storm {
                 auto formula = eliminateRewardAccumulations(*p.getFilter().getFormula());
                 auto states = eliminateRewardAccumulations(*p.getFilter().getStatesFormula());
                 storm::jani::FilterExpression fe(formula, p.getFilter().getFilterType(), states);
-                p = storm::jani::Property(p.getName(), storm::jani::FilterExpression(formula, p.getFilter().getFilterType(), states), p.getComment());
+                p = storm::jani::Property(p.getName(), storm::jani::FilterExpression(formula, p.getFilter().getFilterType(), states), p.getUndefinedConstants(), p.getComment());
             }
         }
         

src/storm/settings/modules/AbstractionSettings.cpp

@@ -111,11 +111,11 @@ namespace storm {
                                 .build());
 
                 this->addOption(storm::settings::OptionBuilder(moduleName, constraintsOptionName, true, "Specifies additional constraints used by the abstraction.")
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("constraints", "The constraints to use.").build())
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("constraints", "The constraints to use.").setDefaultValueString("").build())
                                 .build());
 
                 this->addOption(storm::settings::OptionBuilder(moduleName, injectRefinementPredicatesOptionName, true, "Specifies predicates used by the refinement instead of the derived predicates.")
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("predicates", "The (semicolon-separated) refinement predicates to use.").build())
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("predicates", "The (semicolon-separated) refinement predicates to use.").setDefaultValueString("").build())
                                 .build());
                 
                 this->addOption(storm::settings::OptionBuilder(moduleName, fixPlayer1StrategyOptionName, true, "Sets whether to fix player 1 strategies.")

src/storm/storage/jani/Property.cpp

@@ -1,20 +1,19 @@
 #include "Property.h"
+
 namespace storm {
     namespace jani {
         
-        
-        
         std::ostream& operator<<(std::ostream& os, FilterExpression const& fe) {
-            return os << "Obtain " << toString(fe.getFilterType()) << " of the '" << fe.getStatesFormula() << "'-states with values described by '" << *fe.getFormula() << "'";
+            return os << "Obtain " << toString(fe.getFilterType()) << " of the '" << *fe.getStatesFormula() << "'-states with values described by '" << *fe.getFormula() << "'";
         }
         
-        Property::Property(std::string const& name, std::shared_ptr<storm::logic::Formula const> const& formula, std::string const& comment)
-        : name(name), comment(comment), filterExpression(FilterExpression(formula)) {
+        Property::Property(std::string const& name, std::shared_ptr<storm::logic::Formula const> const& formula, std::set<storm::expressions::Variable> const& undefinedConstants, std::string const& comment)
+        : name(name), comment(comment), filterExpression(FilterExpression(formula)), undefinedConstants(undefinedConstants) {
             // Intentionally left empty.
         }
         
-        Property::Property(std::string const& name, FilterExpression const& fe, std::string const& comment)
-        : name(name), comment(comment), filterExpression(fe) {
+        Property::Property(std::string const& name, FilterExpression const& fe, std::set<storm::expressions::Variable> const& undefinedConstants, std::string const& comment)
+        : name(name), comment(comment), filterExpression(fe), undefinedConstants(undefinedConstants) {
             // Intentionally left empty.
         }
 
@@ -27,11 +26,17 @@ namespace storm {
         }
         
         Property Property::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return Property(name, filterExpression.substitute(substitution), comment);
+            std::set<storm::expressions::Variable> remainingUndefinedConstants;
+            for (auto const& constant : undefinedConstants) {
+                if (substitution.find(constant) == substitution.end()) {
+                    remainingUndefinedConstants.insert(constant);
+                }
+            }
+            return Property(name, filterExpression.substitute(substitution), remainingUndefinedConstants, comment);
         }
         
         Property Property::substituteLabels(std::map<std::string, std::string> const& substitution) const {
-            return Property(name, filterExpression.substituteLabels(substitution), comment);
+            return Property(name, filterExpression.substituteLabels(substitution), undefinedConstants, comment);
         }
         
         FilterExpression const& Property::getFilter() const {
@@ -42,8 +47,16 @@ namespace storm {
             return this->filterExpression.getFormula();
         }
         
+        std::set<storm::expressions::Variable> const& Property::getUndefinedConstants() const {
+            return undefinedConstants;
+        }
+        
+        bool Property::containsUndefinedConstants() const {
+            return !undefinedConstants.empty();
+        }
+        
         std::ostream& operator<<(std::ostream& os, Property const& p) {
-            return os << "(" << p.getName() << ") : " << p.getFilter();
+            return os << "(" << p.getName() << "): " << p.getFilter();
         }
         
     }

src/storm/storage/jani/Property.h

@@ -78,9 +78,10 @@ namespace storm {
              * Constructs the property
              * @param name the name
              * @param formula the formula representation
+             * @param undefinedConstants the undefined constants used in the property
              * @param comment An optional comment
              */
-            Property(std::string const& name, std::shared_ptr<storm::logic::Formula const> const& formula, std::string const& comment = "");
+            Property(std::string const& name, std::shared_ptr<storm::logic::Formula const> const& formula, std::set<storm::expressions::Variable> const& undefinedConstants, std::string const& comment = "");
             
             /**
              * Constructs the property
@@ -88,7 +89,7 @@ namespace storm {
              * @param formula the formula representation
              * @param comment An optional comment
              */
-            Property(std::string const& name, FilterExpression const& fe, std::string const& comment = "");
+            Property(std::string const& name, FilterExpression const& fe, std::set<storm::expressions::Variable> const& undefinedConstants, std::string const& comment = "");
             
             /**
              * Get the provided name
@@ -107,11 +108,15 @@ namespace storm {
             
             FilterExpression const& getFilter() const;
             
+            std::set<storm::expressions::Variable> const& getUndefinedConstants() const;
+            bool containsUndefinedConstants() const;
+            
             std::shared_ptr<storm::logic::Formula const> getRawFormula() const;
         private:
             std::string name;
             std::string comment;
             FilterExpression filterExpression;
+            std::set<storm::expressions::Variable> undefinedConstants;
         };