fixed abstraction by considering related predicates for all sources. started on command decomposition

src/storm/abstraction/LocalExpressionInformation.cpp

@@ -141,6 +141,15 @@ namespace storm {
             return this->variableToBlockMapping.find(variable)->second;
         }
         
+        template <storm::dd::DdType DdType>
+        std::set<uint_fast64_t> LocalExpressionInformation<DdType>::getBlockIndicesOfVariables(std::set<storm::expressions::Variable> const& variables) const {
+            std::set<uint_fast64_t> result;
+            for (auto const& variable : variables) {
+                result.insert(getBlockIndexOfVariable(variable));
+            }
+            return result;
+        }
+        
         template <storm::dd::DdType DdType>
         std::set<uint_fast64_t> const& LocalExpressionInformation<DdType>::getRelatedExpressions(storm::expressions::Variable const& variable) const {
             return this->expressionBlocks[getBlockIndexOfVariable(variable)];

src/storm/abstraction/LocalExpressionInformation.h

@@ -76,6 +76,14 @@ namespace storm {
              */
             uint_fast64_t getBlockIndexOfVariable(storm::expressions::Variable const& variable) const;
 
+            /*!
+             * Retrieves the block indices of the given variables.
+             *
+             * @param variables The variables for which to retrieve the blocks.
+             * @return The block indices of the given variables.
+             */
+            std::set<uint_fast64_t> getBlockIndicesOfVariables(std::set<storm::expressions::Variable> const& variables) const;
+
             /*!
              * Retrieves the number of blocks of the variable partition.
              *

src/storm/abstraction/MenuGameRefiner.cpp

@@ -254,6 +254,10 @@ namespace storm {
             } else {
                 STORM_LOG_TRACE("No bottom state successor. Deriving a new predicate using weakest precondition.");
             
+//                player1Choice.template toAdd<ValueType>().exportToDot("choice.dot");
+//                lowerChoice.template toAdd<ValueType>().exportToDot("lower.dot");
+//                upperChoice.template toAdd<ValueType>().exportToDot("upper.dot");
+                
                 // Decode both choices to explicit mappings.
                 std::map<uint64_t, std::pair<storm::storage::BitVector, ValueType>> lowerChoiceUpdateToSuccessorMapping = abstractionInformation.template decodeChoiceToUpdateSuccessorMapping<ValueType>(lowerChoice);
                 std::map<uint64_t, std::pair<storm::storage::BitVector, ValueType>> upperChoiceUpdateToSuccessorMapping = abstractionInformation.template decodeChoiceToUpdateSuccessorMapping<ValueType>(upperChoice);

src/storm/abstraction/prism/CommandAbstractor.cpp

@@ -70,6 +70,68 @@ namespace storm {
                 return command.get().getUpdate(auxiliaryChoice).getAsVariableToExpressionMap();
             }
 
+            template <storm::dd::DdType DdType, typename ValueType>
+            void CommandAbstractor<DdType, ValueType>::recomputeCachedBddUsingDecomposition() {
+                STORM_LOG_TRACE("Recomputing BDD for command " << command.get() << " using the decomposition.");
+                auto start = std::chrono::high_resolution_clock::now();
+
+                // compute a decomposition of the command
+                //  * start with all relevant blocks: blocks of assignment variables and variables in the rhs of assignments
+                //  * go through all assignments of all updates and merge relevant blocks that are related via an assignment
+                //  * repeat this until nothing changes anymore
+                //  * the resulting blocks are the decomposition
+                
+                // Start by constructing the relevant blocks.
+                std::set<uint64_t> allRelevantBlocks;
+                std::map<storm::expressions::Variable, uint64_t> variableToBlockIndex;
+                for (auto const& update : command.get().getUpdates()) {
+                    for (auto const& assignment : update.getAssignments()) {
+                        allRelevantBlocks.insert(localExpressionInformation.getBlockIndexOfVariable(assignment.getVariable()));
+
+                        auto rhsVariableBlocks = localExpressionInformation.getBlockIndicesOfVariables(assignment.getExpression().getVariables());
+                        allRelevantBlocks.insert(rhsVariableBlocks.begin(), rhsVariableBlocks.end());
+                    }
+                }
+                STORM_LOG_TRACE("Found " << allRelevantBlocks.size() << " relevant block.");
+
+                // Create a block partition.
+                std::vector<std::set<uint64_t>> relevantBlockPartition;
+                std::map<storm::expressions::Variable, uint64_t> variableToLocalBlockIndex;
+                uint64_t index = 0;
+                for (auto const& blockIndex : allRelevantBlocks) {
+                    relevantBlockPartition.emplace_back(std::set<uint64_t>({blockIndex}));
+                    for (auto const& variable : localExpressionInformation.getVariableBlockWithIndex(blockIndex)) {
+                        variableToLocalBlockIndex[variable] = index;
+                    }
+                    ++index;
+                }
+                
+                // Proceed by relating the blocks via assignments until nothing changes anymore.
+                bool changed = false;
+                do {
+                    for (auto const& update : command.get().getUpdates()) {
+                        for (auto const& assignment : update.getAssignments()) {
+                            std::set<storm::expressions::Variable> rhsVariables = assignment.getExpression().getVariables();
+                            
+                        }
+                    }
+                } while (changed);
+                
+                // if the decomposition has size 1, use the plain technique from before
+                
+                // otherwise, enumerate the abstract guard so we do this only once
+                
+                // then enumerate the solutions for each of the blocks of the decomposition
+                
+                // multiply the results
+                
+                // multiply with the abstract guard
+                
+                // multiply with missing identities
+                
+                // cache and return result
+            }
+            
             template <storm::dd::DdType DdType, typename ValueType>
             void CommandAbstractor<DdType, ValueType>::recomputeCachedBdd() {
                 STORM_LOG_TRACE("Recomputing BDD for command " << command.get());
@@ -140,12 +202,12 @@ namespace storm {
                 std::set<storm::expressions::Variable> assignedVariables;
                 for (auto const& assignment : assignments) {
                     // Also, variables appearing on the right-hand side of an assignment are relevant for source state.
-                    auto const& rightHandSidePredicates = localExpressionInformation.getExpressionsUsingVariables(assignment.getExpression().getVariables());
+                    auto const& rightHandSidePredicates = localExpressionInformation.getRelatedExpressions(assignment.getExpression().getVariables());
                     result.first.insert(rightHandSidePredicates.begin(), rightHandSidePredicates.end());
                     
                     // Variables that are being assigned are relevant for the successor state.
                     storm::expressions::Variable const& assignedVariable = assignment.getVariable();
-                    auto const& leftHandSidePredicates = localExpressionInformation.getExpressionsUsingVariable(assignedVariable);
+                    auto const& leftHandSidePredicates = localExpressionInformation.getRelatedExpressions(assignedVariable);
                     result.second.insert(leftHandSidePredicates.begin(), leftHandSidePredicates.end());
                     
                     // Keep track of all assigned variables, so we can find the related predicates later.
@@ -165,7 +227,7 @@ namespace storm {
                 std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> result;
 
                 // To start with, all predicates related to the guard are relevant source predicates.
-                result.first = localExpressionInformation.getExpressionsUsingVariables(command.get().getGuardExpression().getVariables());
+                result.first = localExpressionInformation.getRelatedExpressions(command.get().getGuardExpression().getVariables());
                 
                 // Then, we add the predicates that become relevant, because of some update.
                 for (auto const& update : command.get().getUpdates()) {
@@ -223,13 +285,10 @@ namespace storm {
             template <storm::dd::DdType DdType, typename ValueType>
             storm::dd::Bdd<DdType> CommandAbstractor<DdType, ValueType>::getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model) const {
                 storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddOne();
-//                std::cout << "new model ----------------" << std::endl;
                 for (auto const& variableIndexPair : relevantPredicatesAndVariables.first) {
                     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/prism/CommandAbstractor.h

@@ -162,6 +162,11 @@ namespace storm {
                  */
                 void recomputeCachedBdd();
                 
+                /*!
+                 * Recomputes the cached BDD using a decomposition. This needs to be triggered if any relevant predicates change.
+                 */
+                void recomputeCachedBddUsingDecomposition();
+
                 /*!
                  * Computes the missing state identities.
                  *

src/storm/settings/modules/AbstractionSettings.cpp

@@ -39,7 +39,7 @@ namespace storm {
 
                 std::vector<std::string> invalidBlockStrategies = {"none", "local", "global"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, invalidBlockStrategyOptionName, true, "Sets the strategy to detect invalid blocks.")
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an available strategy. Available are: 'none', 'local' and 'global'.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(invalidBlockStrategies)).setDefaultValueString("global").build()).build());
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an available strategy. Available are: 'none', 'local' and 'global'.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(invalidBlockStrategies)).setDefaultValueString("local").build()).build());
                 
                 this->addOption(storm::settings::OptionBuilder(moduleName, reuseQualitativeResultsOptionName, true, "Sets whether to reuse qualitative results.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, reuseQuantitativeResultsOptionName, true, "Sets whether to reuse quantitative results.").build());

src/storm/storage/SymbolicModelDescription.cpp

@@ -119,7 +119,6 @@ namespace storm {
             if (this->isJaniModel()) {
                 std::map<storm::expressions::Variable, storm::expressions::Expression> substitution = storm::utility::jani::parseConstantDefinitionString(this->asJaniModel(), constantDefinitionString);
                 storm::jani::Model preparedModel = this->asJaniModel().defineUndefinedConstants(substitution).substituteConstants();
-                preparedModel = preparedModel.flattenComposition();
                 return SymbolicModelDescription(preparedModel);
             } else if (this->isPrismProgram()) {
                 std::map<storm::expressions::Variable, storm::expressions::Expression> substitution = storm::utility::prism::parseConstantDefinitionString(this->asPrismProgram(), constantDefinitionString);

src/storm/storage/jani/Model.cpp

@@ -511,7 +511,17 @@ namespace storm {
             newAutomaton.changeAssignmentVariables(variableRemapping);
             
             // Finalize the flattened model.
+            storm::expressions::Expression initialStatesRestriction = getManager().boolean(true);
+            for (auto const& automaton : composedAutomata) {
+                if (automaton.get().hasInitialStatesRestriction()) {
+                    initialStatesRestriction = initialStatesRestriction && automaton.get().getInitialStatesRestriction();
+                }
+            }
+            
             newAutomaton.setInitialStatesRestriction(this->getInitialStatesExpression(composedAutomata));
+            if (this->hasInitialStatesRestriction()) {
+                flattenedModel.setInitialStatesRestriction(this->getInitialStatesRestriction());
+            }
             flattenedModel.addAutomaton(newAutomaton);
             flattenedModel.setStandardSystemComposition();
             flattenedModel.finalize();
@@ -879,6 +889,10 @@ namespace storm {
             this->initialStatesRestriction = initialStatesRestriction;
         }
         
+        bool Model::hasInitialStatesRestriction() const {
+            return this->initialStatesRestriction.isInitialized();
+        }
+        
         storm::expressions::Expression const& Model::getInitialStatesRestriction() const {
             return initialStatesRestriction;
         }