added option to feed additional constraints to abstraction

src/storm/abstraction/AbstractionInformation.cpp

@@ -1,9 +1,16 @@
 #include "storm/abstraction/AbstractionInformation.h"
 
+#include <boost/algorithm/string.hpp>
+
 #include "storm/storage/BitVector.h"
 
 #include "storm/storage/dd/DdManager.h"
 
+#include "storm/settings/modules/AbstractionSettings.h"
+#include "storm/settings/SettingsManager.h"
+
+#include "storm/parser/ExpressionParser.h"
+
 #include "storm/utility/macros.h"
 #include "storm/exceptions/InvalidOperationException.h"
 
@@ -15,7 +22,28 @@ namespace storm {
 
         template<storm::dd::DdType DdType>
         AbstractionInformation<DdType>::AbstractionInformation(storm::expressions::ExpressionManager& expressionManager, std::set<storm::expressions::Variable> const& abstractedVariables, std::unique_ptr<storm::solver::SmtSolver>&& smtSolver, std::shared_ptr<storm::dd::DdManager<DdType>> ddManager) : expressionManager(expressionManager), equivalenceChecker(std::move(smtSolver)), abstractedVariables(abstractedVariables), ddManager(ddManager), allPredicateIdentities(ddManager->getBddOne()), allLocationIdentities(ddManager->getBddOne()), expressionToBddMap() {
-            // Intentionally left empty.
+            
+            // Obtain additional constraints from the settings.
+            auto const& settings = storm::settings::getModule<storm::settings::modules::AbstractionSettings>();
+            if (settings.isConstraintsSet()) {
+                std::string constraintsString = settings.getConstraintString();
+                
+                std::vector<std::string> constraintsAsStrings;
+                boost::split(constraintsAsStrings, constraintsString, boost::is_any_of(","));
+                
+                storm::parser::ExpressionParser expressionParser(expressionManager);
+                std::unordered_map<std::string, storm::expressions::Expression> variableMapping;
+                for (auto const& variableTypePair : expressionManager) {
+                    variableMapping[variableTypePair.first.getName()] = variableTypePair.first;
+                }
+                expressionParser.setIdentifierMapping(variableMapping);
+                
+                for (auto const& constraintString : constraintsAsStrings) {
+                    storm::expressions::Expression constraint = expressionParser.parseFromString(constraintString);
+                    STORM_LOG_TRACE("Adding special (user-provided) constraint " << constraint << ".");
+                    constraints.emplace_back(constraint);
+                }
+            }
         }
         
         template<storm::dd::DdType DdType>

src/storm/abstraction/StateSetAbstractor.cpp

@@ -16,6 +16,10 @@ namespace storm {
         template <storm::dd::DdType DdType, typename ValueType>
         StateSetAbstractor<DdType, ValueType>::StateSetAbstractor(AbstractionInformation<DdType>& abstractionInformation, std::vector<storm::expressions::Expression> const& statePredicates, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), localExpressionInformation(abstractionInformation), relevantPredicatesAndVariables(), concretePredicateVariables(), forceRecomputation(true), cachedBdd(abstractionInformation.getDdManager().getBddOne()), constraint(abstractionInformation.getDdManager().getBddOne()) {
             
+            for (auto const& constraint : abstractionInformation.getConstraints()) {
+                smtSolver->add(constraint);
+            }
+            
             // Assert all state predicates.
             for (auto const& predicate : statePredicates) {
                 smtSolver->add(predicate);

src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -58,7 +58,9 @@ namespace storm {
 
         template<storm::dd::DdType Type, typename ModelType>
         GameBasedMdpModelChecker<Type, ModelType>::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getPrecision()), reuseQualitativeResults(false), reuseQuantitativeResults(false), solveMode(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getSolveMode()) {
-            model.requireNoUndefinedConstants();
+
+            STORM_LOG_WARN_COND(!model.hasUndefinedConstants(), "Model contains undefined constants. Game-based abstraction can treat such models, but you should make sure that you did not simply forget to define these constants. In particular, it may be necessary to constrain the values of the undefined constants.");
+            
             if (model.isPrismProgram()) {
                 storm::prism::Program const& originalProgram = model.asPrismProgram();
                 STORM_LOG_THROW(originalProgram.getModelType() == storm::prism::Program::ModelType::DTMC || originalProgram.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::NotSupportedException, "Currently only DTMCs/MDPs are supported by the game-based model checker.");
@@ -566,7 +568,7 @@ namespace storm {
                 
                 // (2) Prepare initial, constraint and target state BDDs for later use.
                 storm::dd::Bdd<Type> initialStates = game.getInitialStates();
-                STORM_LOG_THROW(initialStates.getNonZeroCount() == 1 || checkTask.isBoundSet(), storm::exceptions::InvalidPropertyException, "Game-based abstraction refinement requires a bound on the formula for model with " << initialStates.getNonZeroCount() << " initial states.");
+//                STORM_LOG_THROW(initialStates.getNonZeroCount() == 1 || checkTask.isBoundSet(), storm::exceptions::InvalidPropertyException, "Game-based abstraction refinement requires a bound on the formula for model with " << initialStates.getNonZeroCount() << " initial states.");
                 storm::dd::Bdd<Type> constraintStates = globalConstraintStates && game.getReachableStates();
                 storm::dd::Bdd<Type> targetStates = globalTargetStates && game.getReachableStates();
                 if (player1Direction == storm::OptimizationDirection::Minimize) {

src/storm/parser/ExpressionCreator.cpp

@@ -16,6 +16,12 @@ namespace storm {
             // Intenetionally left empty.
         }
         
+        ExpressionCreator::~ExpressionCreator() {
+            if (deleteIdentifierMapping) {
+                delete this->identifiers;
+            }
+        }
+        
         storm::expressions::Expression ExpressionCreator::createIteExpression(storm::expressions::Expression const& e1, storm::expressions::Expression const& e2, storm::expressions::Expression const& e3, bool& pass) const {
             if (this->createExpressions) {
                 try {
@@ -241,7 +247,7 @@ namespace storm {
         void ExpressionCreator::setIdentifierMapping(std::unordered_map<std::string, storm::expressions::Expression> const& identifierMapping) {
             unsetIdentifierMapping();
             
-            createExpressions =true;
+            createExpressions = true;
             identifiers = new qi::symbols<char, storm::expressions::Expression>();
             for (auto const& identifierExpressionPair : identifierMapping) {
                 identifiers->add(identifierExpressionPair.first, identifierExpressionPair.second);
@@ -257,9 +263,6 @@ namespace storm {
             }
             this->identifiers = nullptr;
         }
-        
 
-
-        
     }
 }

src/storm/parser/ExpressionCreator.h

@@ -19,11 +19,7 @@ namespace storm {
         public:
             ExpressionCreator(storm::expressions::ExpressionManager const& manager);
             
-            virtual ~ExpressionCreator() {
-                if (deleteIdentifierMapping) {
-                    delete this->identifiers;
-                }
-            }
+            ~ExpressionCreator();
             
             /*!
              * Sets an identifier mapping that is used to determine valid variables in the expression. The mapped-to

src/storm/parser/ExpressionParser.cpp

@@ -38,7 +38,7 @@ namespace storm {
     namespace parser {
         ExpressionParser::ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols<char, uint_fast64_t> const& invalidIdentifiers_, bool enableErrorHandling, bool allowBacktracking) : ExpressionParser::base_type(expression), orOperator_(), andOperator_(), equalityOperator_(), relationalOperator_(), plusOperator_(), multiplicationOperator_(), infixPowerModuloOperator_(), unaryOperator_(), floorCeilOperator_(), minMaxOperator_(), prefixPowerModuloOperator_(), invalidIdentifiers_(invalidIdentifiers_) {
             
-            expressionCreator = new ExpressionCreator(manager);
+            expressionCreator = std::make_unique<ExpressionCreator>(manager);
             
             identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_') | qi::char_('.')) >> *(qi::alnum | qi::char_('_')))]]][qi::_pass = phoenix::bind(&ExpressionParser::isValidIdentifier, phoenix::ref(*this), qi::_1)];
             identifier.name("identifier");
@@ -176,6 +176,10 @@ namespace storm {
             }
         }
         
+        ExpressionParser::~ExpressionParser() {
+            // Needed, because auto-generated destructor requires ExpressionCreator to be a complete type in the header.
+        }
+        
         void ExpressionParser::setIdentifierMapping(qi::symbols<char, storm::expressions::Expression> const* identifiers_) {
             expressionCreator->setIdentifierMapping(identifiers_);
         }

src/storm/parser/ExpressionParser.h

@@ -1,6 +1,7 @@
 #pragma once
 
 #include <sstream>
+#include <memory>
 
 #include "storm/parser/SpiritParserDefinitions.h"
 #include "storm/parser/SpiritErrorHandler.h"
@@ -46,6 +47,7 @@ namespace storm {
              * also parses boolean conjuncts that are erroneously consumed by the expression parser.
              */
             ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols<char, uint_fast64_t> const& invalidIdentifiers_ = qi::symbols<char, uint_fast64_t>(), bool enableErrorHandling = true, bool allowBacktracking = false);
+            ~ExpressionParser();
             
             ExpressionParser(ExpressionParser const& other) = default;
             ExpressionParser& operator=(ExpressionParser const& other) = default;
@@ -207,7 +209,7 @@ namespace storm {
             prefixPowerModuloOperatorStruct prefixPowerModuloOperator_;
             
             
-            ExpressionCreator* expressionCreator;
+            std::unique_ptr<ExpressionCreator> expressionCreator;
             
             
             // The symbol table of invalid identifiers.

src/storm/settings/modules/AbstractionSettings.cpp

@@ -25,6 +25,7 @@ namespace storm {
             const std::string AbstractionSettings::solveModeOptionName = "solve";
             const std::string AbstractionSettings::maximalAbstractionOptionName = "maxabs";
             const std::string AbstractionSettings::rankRefinementPredicatesOptionName = "rankpred";
+            const std::string AbstractionSettings::constraintsOptionName = "constraints";
             
             AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) {
                 std::vector<std::string> methods = {"games", "bisimulation", "bisim"};
@@ -86,6 +87,11 @@ namespace storm {
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff))
                                              .setDefaultValueString("off").build())
                                 .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())
+                                .build());
+
             }
             
             AbstractionSettings::Method AbstractionSettings::getAbstractionRefinementMethod() const {
@@ -176,6 +182,14 @@ namespace storm {
                 return this->getOption(rankRefinementPredicatesOptionName).getArgumentByName("value").getValueAsString() == "on";
             }
             
+            bool AbstractionSettings::isConstraintsSet() const {
+                return this->getOption(constraintsOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string AbstractionSettings::getConstraintString() const {
+                return this->getOption(constraintsOptionName).getArgumentByName("constraints").getValueAsString();
+            }
+            
         }
     }
 }

src/storm/settings/modules/AbstractionSettings.h

@@ -123,6 +123,20 @@ namespace storm {
                  */
                 bool isRankRefinementPredicatesSet() const;
                 
+                /*!
+                 * Retrieves whether the constraints option was set.
+                 *
+                 * @return True if the constraints option was set.
+                 */
+                bool isConstraintsSet() const;
+                
+                /*!
+                 * Retrieves the string that specifies additional constraints.
+                 *
+                 * @return The string that defines the constraints.
+                 */
+                std::string getConstraintString() const;
+                
                 const static std::string moduleName;
                 
             private:
@@ -138,6 +152,7 @@ namespace storm {
                 const static std::string solveModeOptionName;
                 const static std::string maximalAbstractionOptionName;
                 const static std::string rankRefinementPredicatesOptionName;
+                const static std::string constraintsOptionName;
             };
             
         }

src/storm/settings/modules/IOSettings.h

@@ -214,9 +214,9 @@ namespace storm {
                 std::string getChoiceLabelingFilename() const;
 
                 /*!
-                 * Retrieves whether the export-to-dot option was set.
+                 * Retrieves whether the constants option was set.
                  *
-                 * @return True if the export-to-dot option was set.
+                 * @return True if the constants option was set.
                  */
                 bool isConstantsSet() const;
 

src/storm/storage/SymbolicModelDescription.cpp

@@ -179,6 +179,30 @@ namespace storm {
             }
         }
         
+        bool SymbolicModelDescription::hasUndefinedConstants() const {
+            if (this->isPrismProgram()) {
+                return this->asPrismProgram().hasUndefinedConstants();
+            } else {
+                return this->asJaniModel().hasUndefinedConstants();
+            }
+        }
+        
+        std::vector<storm::expressions::Variable> SymbolicModelDescription::getUndefinedConstants() const {
+            std::vector<storm::expressions::Variable> result;
+            if (this->isPrismProgram()) {
+                std::vector<std::reference_wrapper<storm::prism::Constant const>> constants = this->asPrismProgram().getUndefinedConstants();
+                for (auto const& constant : constants) {
+                    result.emplace_back(constant.get().getExpressionVariable());
+                }
+            } else {
+                std::vector<std::reference_wrapper<storm::jani::Constant const>> constants = this->asJaniModel().getUndefinedConstants();
+                for (auto const& constant : constants) {
+                    result.emplace_back(constant.get().getExpressionVariable());
+                }
+            }
+            return result;
+        }
+        
         std::ostream& operator<<(std::ostream& out, SymbolicModelDescription const& model) {
             if (model.isPrismProgram()) {
                 out << model.asPrismProgram();

src/storm/storage/SymbolicModelDescription.h

@@ -47,6 +47,8 @@ namespace storm {
             std::map<storm::expressions::Variable, storm::expressions::Expression> parseConstantDefinitions(std::string const& constantDefinitionString) const;
             
             void requireNoUndefinedConstants() const;
+            bool hasUndefinedConstants() const;
+            std::vector<storm::expressions::Variable> getUndefinedConstants() const;
             
         private:
             boost::optional<boost::variant<storm::jani::Model, storm::prism::Program>> modelDescription;