fixed out-of-bounds-labelling, added overlapping guards building, and some improved error messages if something goes wrong with highlevel counterex generation

src/storm/builder/ExplicitModelBuilder.cpp

@@ -275,6 +275,7 @@ namespace storm {
                 // (a) the transition matrix
                 // (b) the initial states
                 // (c) the hash map storing the mapping states -> ids
+                // (d) fix remapping for state-generation labels
                 
                 // Fix (a).
                 transitionMatrixBuilder.replaceColumns(remapping, 0);
@@ -287,6 +288,8 @@ namespace storm {
                 
                 // Fix (c).
                 this->stateStorage.stateToId.remap([&remapping] (StateType const& state) { return remapping[state]; } );
+
+                this->generator->remapStateIds([&remapping] (StateType const& state) { return remapping[state]; });
             }
         }
         

src/storm/counterexamples/SMTMinimalLabelSetGenerator.h

@@ -458,6 +458,12 @@ namespace storm {
                     
                     // Now check for possible backward cuts.
                     for (auto const& labelSetAndPrecedingLabelSetsPair : precedingLabels) {
+                        bool backwardImplicationAdded = false;
+//                        std::cout << "labelSetAndPrecedingLabelSetsPair.first ";
+//                        for (auto const& e : labelSetAndPrecedingLabelSetsPair.first) {
+//                            std::cout << e << ", ";
+//                        }
+//                        std::cout << std::endl;
                         // Find out the commands for the currently considered label set.
                         storm::expressions::Expression guardConjunction;
                         
@@ -510,15 +516,18 @@ namespace storm {
                         // If the solver reports unsat, then we know that the current selection is not enabled in the initial state.
                         if (checkResult == storm::solver::SmtSolver::CheckResult::Unsat) {
                             STORM_LOG_DEBUG("Selection not enabled in initial state.");
-                            
+
+                            //std::cout << "not gc: " << !guardConjunction << std::endl;
                             localSolver->add(!guardConjunction);
                             STORM_LOG_DEBUG("Asserted disjunction of negated guards.");
                             
                             
                             // Now check the possible preceding label sets for the essential ones.
                             for (auto const& precedingLabelSet : labelSetAndPrecedingLabelSetsPair.second) {
+
                                 if (labelSetAndPrecedingLabelSetsPair.first == precedingLabelSet) continue;
-                                
+
+                                //std::cout << "push" << std::endl;
                                 // Create a restore point so we can easily pop-off all weakest precondition expressions.
                                 localSolver->push();
                                 
@@ -576,7 +585,9 @@ namespace storm {
                                         }
                                     }
                                 }
-                                
+
+                                //std::cout << "pgc: " << preceedingGuardConjunction << std::endl;
+
                                 // Assert all the guards of the preceding command set.
                                 localSolver->add(preceedingGuardConjunction);
                                 
@@ -624,11 +635,15 @@ namespace storm {
                                 assertDisjunction(*localSolver, formulae, symbolicModel.isPrismProgram() ? symbolicModel.asPrismProgram().getManager() : symbolicModel.asJaniModel().getManager());
                                 
                                 STORM_LOG_DEBUG("Asserted disjunction of all weakest preconditions.");
-                                
-                                if (localSolver->check() == storm::solver::SmtSolver::CheckResult::Sat) {
+                                storm::solver::SmtSolver::CheckResult result = localSolver->check();
+
+                                if (result == storm::solver::SmtSolver::CheckResult::Sat) {
                                     backwardImplications[labelSetAndPrecedingLabelSetsPair.first].insert(precedingLabelSet);
+                                    backwardImplicationAdded = true;
+                                } else if (result == storm::solver::SmtSolver::CheckResult::Unknown) {
+                                    STORM_LOG_ERROR("The SMT solver does not come to a conclusive answer. Does your model contain integer division?");
                                 }
-                                
+
                                 localSolver->pop();
                             }
                             
@@ -637,6 +652,7 @@ namespace storm {
                         } else {
                             STORM_LOG_DEBUG("Selection is enabled in initial state.");
                         }
+                        STORM_LOG_ERROR_COND(backwardImplicationAdded, "Error in adding cuts for counterexample generation (backward implication misses a label set).");
                     }
                 } else if (symbolicModel.isJaniModel()) {
                     STORM_LOG_WARN("Model uses assignment levels, did not assert backward implications.");
@@ -1697,6 +1713,7 @@ namespace storm {
                         labelSets[choice] = choiceOrigins.getEdgeIndexSet(choice);
                     }
                 }
+                assert(labelSets.size() == model.getNumberOfChoices());
                 
                 // (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set.
                 double maximalReachabilityProbability = 0;
@@ -1764,7 +1781,7 @@ namespace storm {
                     solverClock = std::chrono::high_resolution_clock::now();
                     commandSet = findSmallestCommandSet(*solver, variableInformation, currentBound);
                     totalSolverTime += std::chrono::high_resolution_clock::now() - solverClock;
-                    STORM_LOG_DEBUG("Computed minimal command set of size " << (commandSet.size() + relevancyInformation.knownLabels.size()) << ".");
+                    STORM_LOG_DEBUG("Computed minimal command set of size " <<  commandSet.size() + relevancyInformation.knownLabels.size() << " (" << commandSet.size() << " + " << relevancyInformation.knownLabels.size() << ") ");
                     
                     // Restrict the given model to the current set of labels and compute the reachability probability.
                     modelCheckingClock = std::chrono::high_resolution_clock::now();

src/storm/generator/CompressedState.cpp

@@ -46,6 +46,13 @@ namespace storm {
         template void unpackStateIntoEvaluator<double>(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<double>& evaluator);
         storm::expressions::SimpleValuation unpackStateIntoValuation(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionManager const& manager);
 
+        CompressedState createOutOfBoundsState(VariableInformation const& varInfo, bool roundTo64Bit) {
+            CompressedState result(varInfo.getTotalBitOffset(roundTo64Bit));
+            assert(varInfo.hasOutOfBoundsBit());
+            result.set(varInfo.getOutOfBoundsBit());
+            return result;
+        }
+
 #ifdef STORM_HAVE_CARL
         template void unpackStateIntoEvaluator<storm::RationalNumber>(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<storm::RationalNumber>& evaluator);
         template void unpackStateIntoEvaluator<storm::RationalFunction>(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<storm::RationalFunction>& evaluator);

src/storm/generator/CompressedState.h

@@ -36,6 +36,8 @@ namespace storm {
          * @return A valuation that corresponds to the compressed state.
          */
         storm::expressions::SimpleValuation unpackStateIntoValuation(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionManager const& manager);
+
+        CompressedState createOutOfBoundsState(VariableInformation const& varInfo, bool roundTo64Bit = true);
     }
 }
 

src/storm/generator/JaniNextStateGenerator.cpp

@@ -320,6 +320,10 @@ namespace storm {
             // If the model is a deterministic model, we need to fuse the choices into one.
             if (this->isDeterministicModel() && totalNumberOfChoices > 1) {
                 Choice<ValueType> globalChoice;
+
+                if (this->options.isAddOverlappingGuardLabelSet()) {
+                    this->overlappingGuardStates->push_back(stateToIdCallback(*this->state));
+                }
                 
                 // For CTMCs, we need to keep track of the total exit rate to scale the action rewards later. For DTMCs
                 // this is equal to the number of choices, which is why we initialize it like this here.

src/storm/generator/NextStateGenerator.cpp

@@ -1,4 +1,5 @@
 #include <storm/exceptions/WrongFormatException.h>
+#include <storm/exceptions/NotImplementedException.h>
 #include "storm/generator/NextStateGenerator.h"
 
 #include "storm/adapters/RationalFunctionAdapter.h"
@@ -18,12 +19,22 @@ namespace storm {
                     
         template<typename ValueType, typename StateType>
         NextStateGenerator<ValueType, StateType>::NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, VariableInformation const& variableInformation, NextStateGeneratorOptions const& options) : options(options), expressionManager(expressionManager.getSharedPointer()), variableInformation(variableInformation), evaluator(nullptr), state(nullptr) {
-            // Intentionally left empty.
+            if(variableInformation.hasOutOfBoundsBit()) {
+                outOfBoundsState = createOutOfBoundsState(variableInformation);
+            }
+            if (options.isAddOverlappingGuardLabelSet()) {
+                overlappingGuardStates = std::vector<uint64_t>();
+            }
         }
         
         template<typename ValueType, typename StateType>
         NextStateGenerator<ValueType, StateType>::NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, NextStateGeneratorOptions const& options) : options(options), expressionManager(expressionManager.getSharedPointer()), variableInformation(), evaluator(nullptr), state(nullptr) {
-            // Intentionally left empty.
+            if(variableInformation.hasOutOfBoundsBit()) {
+                outOfBoundsState = createOutOfBoundsState(variableInformation);
+            }
+            if (options.isAddOverlappingGuardLabelSet()) {
+                overlappingGuardStates = std::vector<uint64_t>();
+            }
         }
         
         template<typename ValueType, typename StateType>
@@ -101,6 +112,14 @@ namespace storm {
                 }
             }
 
+            if (this->options.isAddOverlappingGuardLabelSet()) {
+                STORM_LOG_THROW(!result.containsLabel("overlap_guards"), storm::exceptions::WrongFormatException, "Label 'overlap_guards' is reserved when adding overlapping guard labels");
+                result.addLabel("overlap_guards");
+                for (auto index : overlappingGuardStates.get()) {
+                    result.addLabelToState("overlap_guards", index);
+                }
+            }
+
             if (this->options.isAddOutOfBoundsStateSet() && stateStorage.stateToId.contains(outOfBoundsState)) {
                 STORM_LOG_THROW(!result.containsLabel("out_of_bounds"),storm::exceptions::WrongFormatException, "Label 'out_of_bounds' is reserved when adding out of bounds states.");
                 result.addLabel("out_of_bounds");
@@ -163,6 +182,13 @@ namespace storm {
             return nullptr;
         }
 
+        template<typename ValueType, typename StateType>
+        void NextStateGenerator<ValueType, StateType>::remapStateIds(std::function<StateType(StateType const&)> const& remapping) {
+            if (overlappingGuardStates != boost::none) {
+                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Remapping of Ids during model building is not supported for overlapping guard statements.");
+            }
+        }
+
         template class NextStateGenerator<double>;
 
 #ifdef STORM_HAVE_CARL

src/storm/generator/NextStateGenerator.h

@@ -66,6 +66,13 @@ namespace storm {
             NextStateGeneratorOptions const& getOptions() const;
             
             virtual std::shared_ptr<storm::storage::sparse::ChoiceOrigins> generateChoiceOrigins(std::vector<boost::any>& dataForChoiceOrigins) const;
+
+            /*!
+             * Performs a remapping of all values stored by applying the given remapping.
+             *
+             * @param remapping The remapping to apply.
+             */
+            void remapStateIds(std::function<StateType(StateType const&)> const& remapping);
             
         protected:
             /*!
@@ -98,6 +105,9 @@ namespace storm {
 
             /// A state that encodes the outOfBoundsState
             CompressedState outOfBoundsState;
+
+            /// A map that stores the indices of states with overlapping guards.
+            boost::optional<std::vector<uint64_t>> overlappingGuardStates;
         };
     }
 }

src/storm/generator/PrismNextStateGenerator.cpp

@@ -229,6 +229,10 @@ namespace storm {
             // If the model is a deterministic model, we need to fuse the choices into one.
             if (this->isDeterministicModel() && totalNumberOfChoices > 1) {
                 Choice<ValueType> globalChoice;
+
+                if (this->options.isAddOverlappingGuardLabelSet()) {
+                    this->overlappingGuardStates->push_back(stateToIdCallback(*this->state));
+                }
                 
                 // For CTMCs, we need to keep track of the total exit rate to scale the action rewards later. For DTMCs
                 // this is equal to the number of choices, which is why we initialize it like this here.

src/storm/generator/VariableInformation.cpp

@@ -31,11 +31,14 @@ namespace storm {
         
         VariableInformation::VariableInformation(storm::prism::Program const& program, bool outOfBoundsState) : totalBitOffset(0) {
             if(outOfBoundsState) {
-                deadlockBit = 0;
+                outOfBoundsBit = 0;
                 ++totalBitOffset;
             } else {
-                deadlockBit = boost::none;
+                outOfBoundsBit = boost::none;
             }
+
+
+
             for (auto const& booleanVariable : program.getGlobalBooleanVariables()) {
                 booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), totalBitOffset, true);
                 ++totalBitOffset;
@@ -75,11 +78,13 @@ namespace storm {
                 STORM_LOG_THROW(!automaton.getVariables().containsNonTransientRealVariables(), storm::exceptions::InvalidArgumentException, "Cannot build model from JANI model that contains non-transient real variables in automaton '" << automaton.getName() << "'.");
             }
             if(outOfBoundsState) {
-                deadlockBit = 0;
+                outOfBoundsBit = 0;
                 ++totalBitOffset;
             } else {
-                deadlockBit = boost::none;
+                outOfBoundsBit = boost::none;
             }
+
+
             
             for (auto const& variable : model.getGlobalVariables().getBooleanVariables()) {
                 if (!variable.isTransient()) {
@@ -133,6 +138,16 @@ namespace storm {
             }
             return result;
         }
+
+        bool VariableInformation::hasOutOfBoundsBit() const {
+            return outOfBoundsBit != boost::none;
+        }
+
+        uint64_t VariableInformation::getOutOfBoundsBit() const {
+            assert(hasOutOfBoundsBit());
+            return outOfBoundsBit.get();
+        }
+
         
         void VariableInformation::sortVariables() {
             // Sort the variables so we can make some assumptions when iterating over them (in the next-state generators).

src/storm/generator/VariableInformation.h

@@ -93,9 +93,12 @@ namespace storm {
             /// The integer variables.
             std::vector<IntegerVariableInformation> integerVariables;
 
-            
+            bool hasOutOfBoundsBit() const;
+
+            uint64_t getOutOfBoundsBit() const;
+
         private:
-            boost::optional<uint64_t> deadlockBit;
+            boost::optional<uint64_t> outOfBoundsBit;
 
             /*!
              * Sorts the variables to establish a known ordering.