several fixes related to game-based abstraction

src/storm/abstraction/MenuGameRefiner.cpp

@@ -1362,18 +1362,21 @@ namespace storm {
                 }
                 
                 // Now clean the classes in the sense that redundant predicates are cleaned.
+                uint64_t checkCounter = 0;
                 for (auto& predicateClass : predicateClasses) {
                     std::vector<storm::expressions::Expression> cleanedAtomsOfClass;
                     
                     for (auto const& predicate : predicateClass.second) {
                         bool addPredicate = true;
                         for (auto const& atom : cleanedAtomsOfClass) {
+                            ++checkCounter;
                             if (predicate.areSame(atom)) {
                                 addPredicate = false;
                                 break;
                             }
                             
-                            if (addPredicate && equivalenceChecker.areEquivalentModuloNegation(predicate, atom)) {
+                            ++checkCounter;
+                            if (equivalenceChecker.areEquivalentModuloNegation(predicate, atom)) {
                                 addPredicate = false;
                                 break;
                             }
@@ -1397,19 +1400,21 @@ namespace storm {
                     auto oldPredicateClassIt = oldPredicateClasses.find(predicateClass.first);
                     if (oldPredicateClassIt != oldPredicateClasses.end()) {
                         for (auto const& newAtom : predicateClass.second) {
+                            bool addAtom = true;
                             for (auto const& oldPredicate : oldPredicateClassIt->second) {
-                                bool addAtom = true;
+                                ++checkCounter;
                                 if (newAtom.areSame(oldPredicate)) {
                                     addAtom = false;
                                     break;
                                 }
+                                ++checkCounter;
                                 if (equivalenceChecker.areEquivalentModuloNegation(newAtom, oldPredicate)) {
                                     addAtom = false;
                                     break;
                                 }
-                                if (addAtom) {
-                                    cleanedAtoms.push_back(newAtom);
-                                }
+                            }
+                            if (addAtom) {
+                                cleanedAtoms.push_back(newAtom);
                             }
                         }
                     } else {
@@ -1417,7 +1422,7 @@ namespace storm {
                     }
                 }
                 auto end = std::chrono::high_resolution_clock::now();
-                STORM_LOG_TRACE("Preprocessing predicates took " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
+                STORM_LOG_TRACE("Preprocessing predicates took " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms (" << checkCounter << " checks).");
                 
                 return cleanedAtoms;
             } else {

src/storm/abstraction/StateSetAbstractor.cpp

@@ -23,8 +23,8 @@ namespace storm {
                 // Extract the variables of the predicate, so we know which variables were used when abstracting.
                 std::set<storm::expressions::Variable> usedVariables = predicate.getVariables();
                 concretePredicateVariables.insert(usedVariables.begin(), usedVariables.end());
-                localExpressionInformation.relate(usedVariables);
             }
+            localExpressionInformation.relate(concretePredicateVariables);
         }
         
         template <storm::dd::DdType DdType, typename ValueType>

src/storm/abstraction/ValidBlockAbstractor.cpp

@@ -34,6 +34,13 @@ namespace storm {
             return validBlocks;
         }
         
+        template <storm::dd::DdType DdType>
+        void ValidBlockAbstractor<DdType>::constrain(storm::expressions::Expression const& constraint) {
+            for (uint64_t i = 0; i < smtSolvers.size(); ++i) {
+                smtSolvers[i]->add(constraint);
+            }
+        }
+        
         template <storm::dd::DdType DdType>
         void ValidBlockAbstractor<DdType>::refine(std::vector<uint64_t> const& predicates) {
             for (auto const& predicate : predicates) {
@@ -114,13 +121,10 @@ namespace storm {
         template <storm::dd::DdType DdType>
         storm::dd::Bdd<DdType> ValidBlockAbstractor<DdType>::getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model, uint64_t blockIndex) const {
             storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddOne();
-//            std::cout << "new model ----------------" << std::endl;
             for (auto const& variableIndexPair : relevantVariablesAndPredicates[blockIndex]) {
                 if (model.getBooleanValue(variableIndexPair.first)) {
-//                    std::cout << this->getAbstractionInformation().getPredicateByIndex(variableIndexPair.second) << " is true" << std::endl;
                     result &= this->getAbstractionInformation().encodePredicateAsSource(variableIndexPair.second);
                 } else {
-//                    std::cout << this->getAbstractionInformation().getPredicateByIndex(variableIndexPair.second) << " is false" << std::endl;
                     result &= !this->getAbstractionInformation().encodePredicateAsSource(variableIndexPair.second);
                 }
             }

src/storm/abstraction/ValidBlockAbstractor.h

@@ -33,6 +33,8 @@ namespace storm {
             
             void refine(std::vector<uint64_t> const& predicates);
             
+            void constrain(storm::expressions::Expression const& constraint);
+            
         private:
             /*!
              * Checks which parts of the valid blocks need to be recomputed.

src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp

@@ -48,6 +48,7 @@ namespace storm {
                 for (auto const& range : this->model.get().getAllRangeExpressions()) {
                     abstractionInformation.addConstraint(range);
                     initialStateAbstractor.constrain(range);
+                    validBlockAbstractor.constrain(range);
                 }
                 
                 uint_fast64_t totalNumberOfCommands = 0;
@@ -181,6 +182,9 @@ namespace storm {
                 // Do a reachability analysis on the raw transition relation.
                 storm::dd::Bdd<DdType> transitionRelation = nonTerminalStates && game.bdd.existsAbstract(variablesToAbstract);
                 storm::dd::Bdd<DdType> initialStates = initialLocationsBdd && initialStateAbstractor.getAbstractStates();
+                if (!model.get().hasTrivialInitialStatesExpression()) {
+                    initialStates &= validBlockAbstractor.getValidBlocks();
+                }
                 initialStates.addMetaVariables(abstractionInformation.getSourcePredicateVariables());
                 storm::dd::Bdd<DdType> reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables());
                 

src/storm/abstraction/prism/ModuleAbstractor.cpp

@@ -26,8 +26,10 @@ namespace storm {
             ModuleAbstractor<DdType, ValueType>::ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), commands(), module(module) {
                 
                 // For each concrete command, we create an abstract counterpart.
+                uint64_t counter = 0;
                 for (auto const& command : module.getCommands()) {
                     commands.emplace_back(command, abstractionInformation, smtSolverFactory, useDecomposition);
+                    ++counter;
                 }
             }
             
@@ -83,7 +85,8 @@ namespace storm {
             BottomStateResult<DdType> ModuleAbstractor<DdType, ValueType>::getBottomStateTransitions(storm::dd::Bdd<DdType> const& reachableStates, uint_fast64_t numberOfPlayer2Variables) {
                 BottomStateResult<DdType> result(this->getAbstractionInformation().getDdManager().getBddZero(), this->getAbstractionInformation().getDdManager().getBddZero());
                 
-                for (auto& command : commands) {
+                for (uint64_t index = 0; index < commands.size(); ++index) {
+                    auto& command = commands[index];
                     BottomStateResult<DdType> commandBottomStateResult = command.getBottomStateTransitions(reachableStates, numberOfPlayer2Variables);
                     result.states |= commandBottomStateResult.states;
                     result.transitions |= commandBottomStateResult.transitions;

src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp

@@ -45,6 +45,7 @@ namespace storm {
                 for (auto const& range : this->program.get().getAllRangeExpressions()) {
                     abstractionInformation.addConstraint(range);
                     initialStateAbstractor.constrain(range);
+                    validBlockAbstractor.constrain(range);
                 }
                 
                 uint_fast64_t totalNumberOfCommands = 0;
@@ -174,6 +175,9 @@ namespace storm {
                 // Do a reachability analysis on the raw transition relation.
                 storm::dd::Bdd<DdType> transitionRelation = nonTerminalStates && game.bdd.existsAbstract(variablesToAbstract);
                 storm::dd::Bdd<DdType> initialStates = initialStateAbstractor.getAbstractStates();
+                if (program.get().hasInitialConstruct()) {
+                    initialStates &= validBlockAbstractor.getValidBlocks();
+                }
                 initialStates.addMetaVariables(abstractionInformation.getSourcePredicateVariables());
                 storm::dd::Bdd<DdType> reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables());
 

src/storm/adapters/MathsatExpressionAdapter.h

@@ -58,11 +58,13 @@ namespace storm {
              * @return An equivalent term for MathSAT.
              */
 			msat_term translateExpression(storm::expressions::Expression const& expression) {
+                additionalConstraints.clear();
                 msat_term result = boost::any_cast<msat_term>(expression.getBaseExpression().accept(*this, boost::none));
                 if (MSAT_ERROR_TERM(result)) {
                     std::string errorMessage(msat_last_error_message(env));
                     STORM_LOG_THROW(!MSAT_ERROR_TERM(result), storm::exceptions::ExpressionEvaluationException, "Could not translate expression to MathSAT's format. (Message: " << errorMessage << ")");
                 }
+                
 				return result;
 			}
             
@@ -82,6 +84,17 @@ namespace storm {
                 return msat_make_constant(env, variableExpressionPair->second);
             }
             
+            bool hasAdditionalConstraints() const {
+                return !additionalConstraints.empty();
+            }
+            
+            /*!
+             * Retrieves additional constraints that were created because of encodings using auxiliary variables.
+             */
+            std::vector<msat_term> const& getAdditionalConstraints() const {
+                return additionalConstraints;
+            }
+            
             /*!
              * Retrieves the variable that is associated with the given MathSAT variable declaration.
              *
@@ -118,6 +131,12 @@ namespace storm {
 
                 msat_term result = leftResult;
                 int_fast64_t exponent;
+                int_fast64_t modulus;
+                storm::expressions::Variable freshAuxiliaryVariable;
+                msat_term modVariable;
+                msat_term lower;
+                msat_term upper;
+                typename storm::NumberTraits<storm::GmpRationalNumber>::IntegerType gmpModulus;
 				switch (expression.getOperatorType()) {
 					case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Plus:
 						return msat_make_plus(env, leftResult, rightResult);
@@ -141,6 +160,23 @@ namespace storm {
                             }
                         }
                         return result;
+                    case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Modulo:
+                        modulus = expression.getSecondOperand()->evaluateAsInt();
+                        STORM_LOG_THROW(modulus > 0, storm::exceptions::ExpressionEvaluationException, "Cannot evaluate expression with negative modulus.");
+                        
+                        freshAuxiliaryVariable = manager.declareFreshVariable(manager.getIntegerType(), true);
+                        modVariable = msat_make_constant(env, createVariable(freshAuxiliaryVariable));
+                        
+                        gmpModulus = typename storm::NumberTraits<storm::GmpRationalNumber>::IntegerType(static_cast<unsigned>(modulus));
+                        
+                        // Create the constraint that fixes the value of the fresh variable.
+                        additionalConstraints.push_back(msat_make_int_modular_congruence(env, gmpModulus.get_mpz_t(), modVariable, leftResult));
+
+                        // Create the constraint that limits the value of the modulo operation to 0 <= val <= modulus-1.
+                        lower = msat_make_number(env, "-1");
+                        upper = msat_make_number(env, std::to_string(modulus - 1).c_str());
+                        additionalConstraints.push_back(msat_make_and(env, msat_make_not(env, msat_make_leq(env, modVariable, lower)), msat_make_leq(env, modVariable, upper)));
+                        return modVariable;
 					default:
                         STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Cannot evaluate expression: unknown numerical binary operator '" << static_cast<uint_fast64_t>(expression.getOperatorType()) << "' in expression " << expression << ".");
 				}
@@ -313,11 +349,15 @@ namespace storm {
 
             // The MathSAT environment used.
 			msat_env& env;
+            
+            // A vector of constraints that need to be kept separate, because they were only implicitly part of an
+            // assertion that was added.
+            std::vector<msat_term> additionalConstraints;
 
             // A mapping of variable names to their declaration in the MathSAT environment.
             std::unordered_map<storm::expressions::Variable, msat_decl> variableToDeclarationMapping;
 
-            // A mapping from MathSAT variable declaration to our variables.
+            // A mapping from MathSAT variable declarations to our variables.
             std::unordered_map<msat_decl, storm::expressions::Variable> declarationToVariableMapping;
 		};
 #endif

src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -574,9 +574,10 @@ namespace storm {
                 }
                 
                 // #ifdef LOCAL_DEBUG
-                // targetStates.template toAdd<ValueType>().exportToDot("target.dot");
-                // abstractor->exportToDot("game" + std::to_string(iterations) + ".dot", targetStates, game.getManager().getBddOne());
-                // game.getReachableStates().template toAdd<ValueType>().exportToDot("reach.dot");
+//                initialStates.template toAdd<ValueType>().exportToDot("init.dot");
+//                targetStates.template toAdd<ValueType>().exportToDot("target.dot");
+//                abstractor->exportToDot("game" + std::to_string(iterations) + ".dot", targetStates, game.getManager().getBddOne());
+//                game.getReachableStates().template toAdd<ValueType>().exportToDot("reach.dot");
                 // #endif
                 
                 std::unique_ptr<CheckResult> result;

src/storm/solver/MathsatSmtSolver.cpp

@@ -139,7 +139,13 @@ namespace storm {
 		void MathsatSmtSolver::add(storm::expressions::Expression const& e)
 		{
 #ifdef STORM_HAVE_MSAT
-			msat_assert_formula(env, expressionAdapter->translateExpression(e));
+            msat_term expression = expressionAdapter->translateExpression(e);
+			msat_assert_formula(env, expression);
+            if (expressionAdapter->hasAdditionalConstraints()) {
+                for (auto const& constraint : expressionAdapter->getAdditionalConstraints()) {
+                    msat_assert_formula(env, constraint);
+                }
+            }
 #else
 			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support.");
 #endif

src/storm/storage/expressions/EquivalenceChecker.cpp

@@ -39,6 +39,7 @@ namespace storm {
             this->smtSolver->push();
             this->smtSolver->add(!storm::expressions::iff(first, !second));
             equivalent = smtSolver->check() == storm::solver::SmtSolver::CheckResult::Unsat;
+            
             this->smtSolver->pop();
             return equivalent;
         }

src/storm/storage/jani/Automaton.cpp

@@ -351,6 +351,27 @@ namespace storm {
             return result;
         }
         
+        bool Automaton::hasTrivialInitialStatesExpression() const {
+            if (this->hasInitialStatesRestriction()) {
+                return false;
+            }
+            
+            bool result = true;
+            for (auto const& variable : this->getVariables()) {
+                if (variable.isTransient()) {
+                    continue;
+                }
+                
+                result &= variable.hasInitExpression();
+                
+                if (!result) {
+                    break;
+                }
+            }
+            
+            return result;
+        }
+        
         bool Automaton::hasEdgeLabeledWithActionIndex(uint64_t actionIndex) const {
             return actionIndices.find(actionIndex) != actionIndices.end();
         }

src/storm/storage/jani/Automaton.h

@@ -252,6 +252,12 @@ namespace storm {
              */
             storm::expressions::Expression getInitialStatesExpression() const;
             
+            /*!
+             * Retrieves whether the initial states expression is trivial in the sense that the automaton has no initial
+             * states restriction and all non-transient variables have initial values.
+             */
+            bool hasTrivialInitialStatesExpression() const;
+            
             /*!
              * Retrieves whether there is an edge labeled with the action with the given index in this automaton.
              */

src/storm/storage/jani/Model.cpp

@@ -928,6 +928,21 @@ namespace storm {
             return getInitialStatesExpression(allAutomata);
         }
         
+        bool Model::hasTrivialInitialStatesExpression() const {
+            if (this->hasInitialStatesRestriction()) {
+                return false;
+            }
+            
+            bool result = true;
+            for (auto const& automaton : this->getAutomata()) {
+                result &= automaton.hasTrivialInitialStatesExpression();
+                if (!result) {
+                    break;
+                }
+            }
+            return result;
+        }
+        
         storm::expressions::Expression Model::getInitialStatesExpression(std::vector<std::reference_wrapper<storm::jani::Automaton const>> const& automata) const {
             // Start with the restriction of variables.
             storm::expressions::Expression result = initialStatesRestriction;

src/storm/storage/jani/Model.h

@@ -349,6 +349,12 @@ namespace storm {
              */
             storm::expressions::Expression getInitialStatesExpression() const;
 
+            /*!
+             * Retrieves whether the initial states expression is trivial in the sense that no automaton has an initial
+             * states restriction and all variables have initial values.
+             */
+            bool hasTrivialInitialStatesExpression() const;
+            
             /*!
              * Retrieves the expression defining the legal initial values of the variables.
              *

src/storm/storage/prism/InitialConstruct.cpp

@@ -16,9 +16,9 @@ namespace storm {
         }
         
         std::ostream& operator<<(std::ostream& stream, InitialConstruct const& initialConstruct) {
-            stream << "initial " << std::endl;
+            stream << "init " << std::endl;
             stream << "\t" << initialConstruct.getInitialStatesExpression() << std::endl;
-            stream << "endinitial" << std::endl;
+            stream << "endinit" << std::endl;
             return stream;
         }
     } // namespace prism

src/storm/storage/prism/Program.cpp

@@ -1554,6 +1554,7 @@ namespace storm {
             
             // Finally, we can create the module and the program and return it.
             storm::prism::Module singleModule(newModuleName.str(), allBooleanVariables, allIntegerVariables, newCommands, this->getFilename(), 0);
+            
             return Program(manager, this->getModelType(), this->getConstants(), std::vector<storm::prism::BooleanVariable>(), std::vector<storm::prism::IntegerVariable>(), this->getFormulas(), {singleModule}, actionToIndexMap, this->getRewardModels(), this->getLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility, this->getFilename(), 0, true);
         }
 

src/storm/utility/constants.h

@@ -16,6 +16,8 @@
 #include <vector>
 #include <map>
 
+#include "storm/utility/NumberTraits.h"
+
 namespace storm {
 
     // Forward-declare MatrixEntry class.