SAT based zerostate analysis: work in progress

src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp

@@ -26,6 +26,7 @@ namespace storm {
             std::vector<std::string> fscModes = {"standard", "simple-linear", "simple-linear-inverse"};
             const std::string transformBinaryOption = "transformbinary";
             const std::string transformSimpleOption = "transformsimple";
+            const std::string memlessSearchOption = "memlesssearch";
 
             POMDPSettings::POMDPSettings() : ModuleSettings(moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportAsParametricModelOption, false, "Export the parametric file.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which to write the model.").build()).build());
@@ -45,6 +46,7 @@ namespace storm {
                                 10).addValidatorUnsignedInteger(
                                 storm::settings::ArgumentValidatorFactory::createUnsignedGreaterValidator(
                                         0)).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, memlessSearchOption, false, "Search for a qualitative memoryless scheuler").build());
             }
 
             bool POMDPSettings::isExportToParametricSet() const {
@@ -80,6 +82,10 @@ namespace storm {
                         "resolution").getValueAsUnsignedInteger();
             }
 
+            bool POMDPSettings::isMemlessSearchSet() const {
+                return this->getOption(memlessSearchOption).getHasOptionBeenSet();
+            }
+
             uint64_t POMDPSettings::getMemoryBound() const {
                 return this->getOption(memoryBoundOption).getArgumentByName("bound").getValueAsUnsignedInteger();
             }

src/storm-pomdp-cli/settings/modules/POMDPSettings.h

@@ -32,6 +32,7 @@ namespace storm {
                 bool isSelfloopReductionSet() const;
                 bool isTransformSimpleSet() const;
                 bool isTransformBinarySet() const;
+                bool isMemlessSearchSet() const;
                 std::string getFscApplicationTypeString() const;
                 uint64_t getMemoryBound() const;
 

src/storm-pomdp-cli/storm-pomdp.cpp

@@ -43,6 +43,7 @@
 #include "storm-pomdp/analysis/UniqueObservationStates.h"
 #include "storm-pomdp/analysis/QualitativeAnalysis.h"
 #include "storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h"
+#include "storm-pomdp/analysis/MemlessStrategySearchQualitative.h"
 #include "storm/api/storm.h"
 
 #include <typeinfo>
@@ -77,6 +78,91 @@ void initializeSettings() {
     storm::settings::addModule<storm::settings::modules::POMDPSettings>();
 }
 
+template<typename ValueType>
+bool extractTargetAndSinkObservationSets(std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> const& pomdp, storm::logic::Formula const& subformula, std::set<uint32_t>& targetObservationSet, storm::storage::BitVector&  badStates) {
+    //TODO refactor (use model checker to determine the states, then transform into observations).
+
+    bool validFormula = false;
+    if (subformula.isEventuallyFormula()) {
+        storm::logic::EventuallyFormula const &eventuallyFormula = subformula.asEventuallyFormula();
+        storm::logic::Formula const &subformula2 = eventuallyFormula.getSubformula();
+        if (subformula2.isAtomicLabelFormula()) {
+            storm::logic::AtomicLabelFormula const &alFormula = subformula2.asAtomicLabelFormula();
+            validFormula = true;
+            std::string targetLabel = alFormula.getLabel();
+            auto labeling = pomdp->getStateLabeling();
+            for (size_t state = 0; state < pomdp->getNumberOfStates(); ++state) {
+                if (labeling.getStateHasLabel(targetLabel, state)) {
+                    targetObservationSet.insert(pomdp->getObservation(state));
+                }
+            }
+        } else if (subformula2.isAtomicExpressionFormula()) {
+            validFormula = true;
+            std::stringstream stream;
+            stream << subformula2.asAtomicExpressionFormula().getExpression();
+            storm::logic::AtomicLabelFormula formula3 = storm::logic::AtomicLabelFormula(stream.str());
+            std::string targetLabel = formula3.getLabel();
+            auto labeling = pomdp->getStateLabeling();
+            for (size_t state = 0; state < pomdp->getNumberOfStates(); ++state) {
+                if (labeling.getStateHasLabel(targetLabel, state)) {
+                    targetObservationSet.insert(pomdp->getObservation(state));
+                }
+            }
+        }
+    } else if (subformula.isUntilFormula()) {
+        storm::logic::UntilFormula const &eventuallyFormula = subformula.asUntilFormula();
+        storm::logic::Formula const &subformula1 = eventuallyFormula.getLeftSubformula();
+        if (subformula1.isAtomicLabelFormula()) {
+            storm::logic::AtomicLabelFormula const &alFormula = subformula1.asAtomicLabelFormula();
+            std::string targetLabel = alFormula.getLabel();
+            auto labeling = pomdp->getStateLabeling();
+            for (size_t state = 0; state < pomdp->getNumberOfStates(); ++state) {
+                if (labeling.getStateHasLabel(targetLabel, state)) {
+                    badStates.set(state);
+                }
+            }
+        } else if (subformula1.isAtomicExpressionFormula()) {
+            std::stringstream stream;
+            stream << subformula1.asAtomicExpressionFormula().getExpression();
+            storm::logic::AtomicLabelFormula formula3 = storm::logic::AtomicLabelFormula(stream.str());
+            std::string targetLabel = formula3.getLabel();
+            auto labeling = pomdp->getStateLabeling();
+            for (size_t state = 0; state < pomdp->getNumberOfStates(); ++state) {
+                if (labeling.getStateHasLabel(targetLabel, state)) {
+                    badStates.set(state);
+                }
+            }
+        } else {
+            return false;
+        }
+        storm::logic::Formula const &subformula2 = eventuallyFormula.getRightSubformula();
+        if (subformula2.isAtomicLabelFormula()) {
+            storm::logic::AtomicLabelFormula const &alFormula = subformula2.asAtomicLabelFormula();
+            validFormula = true;
+            std::string targetLabel = alFormula.getLabel();
+            auto labeling = pomdp->getStateLabeling();
+            for (size_t state = 0; state < pomdp->getNumberOfStates(); ++state) {
+                if (labeling.getStateHasLabel(targetLabel, state)) {
+                    targetObservationSet.insert(pomdp->getObservation(state));
+                }
+            }
+        } else if (subformula2.isAtomicExpressionFormula()) {
+            validFormula = true;
+            std::stringstream stream;
+            stream << subformula2.asAtomicExpressionFormula().getExpression();
+            storm::logic::AtomicLabelFormula formula3 = storm::logic::AtomicLabelFormula(stream.str());
+            std::string targetLabel = formula3.getLabel();
+            auto labeling = pomdp->getStateLabeling();
+            for (size_t state = 0; state < pomdp->getNumberOfStates(); ++state) {
+                if (labeling.getStateHasLabel(targetLabel, state)) {
+                    targetObservationSet.insert(pomdp->getObservation(state));
+                }
+            }
+        }
+    }
+    return validFormula;
+}
+
 /*!
  * Entry point for the pomdp backend.
  *
@@ -85,7 +171,7 @@ void initializeSettings() {
  * @return Return code, 0 if successfull, not 0 otherwise.
  */
 int main(const int argc, const char** argv) {
-    try {
+    //try {
         storm::utility::setUp();
         storm::cli::printHeader("Storm-pomdp", argc, argv);
         initializeSettings();
@@ -134,7 +220,21 @@ int main(const int argc, const char** argv) {
         }
 
         if (formula) {
+            storm::logic::ProbabilityOperatorFormula const &probFormula = formula->asProbabilityOperatorFormula();
+            storm::logic::Formula const &subformula1 = probFormula.getSubformula();
+
+
             if (formula->isProbabilityOperatorFormula()) {
+
+                std::set<uint32_t> targetObservationSet;
+                std::set<uint32_t> badObservationSet;
+
+                bool validFormula = extractTargetAndSinkObservationSets(pomdp, subformula1, targetObservationSet, badObservationSet);
+                STORM_LOG_THROW(validFormula, storm::exceptions::InvalidPropertyException,
+                                "The formula is not supported by the grid approximation");
+                STORM_LOG_ASSERT(!targetObservationSet.empty(), "The set of target observations is empty!");
+
+
                 boost::optional<storm::storage::BitVector> prob1States;
                 boost::optional<storm::storage::BitVector> prob0States;
                 if (pomdpSettings.isSelfloopReductionSet() && !storm::solver::minimize(formula->asProbabilityOperatorFormula().getOptimalityType())) {
@@ -159,42 +259,6 @@ int main(const int argc, const char** argv) {
                     pomdp = kpt.transform(*pomdp, *prob0States, *prob1States);
                 }
                 if (pomdpSettings.isGridApproximationSet()) {
-                    storm::logic::ProbabilityOperatorFormula const &probFormula = formula->asProbabilityOperatorFormula();
-                    storm::logic::Formula const &subformula1 = probFormula.getSubformula();
-
-                    std::set<uint32_t> targetObservationSet;
-                    //TODO refactor
-                    bool validFormula = false;
-                    if (subformula1.isEventuallyFormula()) {
-                        storm::logic::EventuallyFormula const &eventuallyFormula = subformula1.asEventuallyFormula();
-                        storm::logic::Formula const &subformula2 = eventuallyFormula.getSubformula();
-                        if (subformula2.isAtomicLabelFormula()) {
-                            storm::logic::AtomicLabelFormula const &alFormula = subformula2.asAtomicLabelFormula();
-                            validFormula = true;
-                            std::string targetLabel = alFormula.getLabel();
-                            auto labeling = pomdp->getStateLabeling();
-                            for (size_t state = 0; state < pomdp->getNumberOfStates(); ++state) {
-                                if (labeling.getStateHasLabel(targetLabel, state)) {
-                                    targetObservationSet.insert(pomdp->getObservation(state));
-                                }
-                            }
-                        } else if (subformula2.isAtomicExpressionFormula()) {
-                            validFormula = true;
-                            std::stringstream stream;
-                            stream << subformula2.asAtomicExpressionFormula().getExpression();
-                            storm::logic::AtomicLabelFormula formula3 = storm::logic::AtomicLabelFormula(stream.str());
-                            std::string targetLabel = formula3.getLabel();
-                            auto labeling = pomdp->getStateLabeling();
-                            for (size_t state = 0; state < pomdp->getNumberOfStates(); ++state) {
-                                if (labeling.getStateHasLabel(targetLabel, state)) {
-                                    targetObservationSet.insert(pomdp->getObservation(state));
-                                }
-                            }
-                        }
-                    }
-                    STORM_LOG_THROW(validFormula, storm::exceptions::InvalidPropertyException,
-                                    "The formula is not supported by the grid approximation");
-                    STORM_LOG_ASSERT(!targetObservationSet.empty(), "The set of target observations is empty!");
 
                     storm::pomdp::modelchecker::ApproximatePOMDPModelchecker<double> checker = storm::pomdp::modelchecker::ApproximatePOMDPModelchecker<double>();
                     double overRes = storm::utility::one<double>();
@@ -213,6 +277,14 @@ int main(const int argc, const char** argv) {
                         STORM_PRINT("Result: " << overRes << std::endl)
                     }
                 }
+                if (pomdpSettings.isMemlessSearchSet()) {
+                    storm::expressions::ExpressionManager expressionManager;
+                    std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
+
+                    storm::pomdp::MemlessStrategySearchQualitative<double> memlessSearch(*pomdp, targetObservationSet, smtSolverFactory);
+                    memlessSearch.analyze(5);
+
+                }
             } else if (formula->isRewardOperatorFormula()) {
                 if (pomdpSettings.isSelfloopReductionSet() && storm::solver::minimize(formula->asRewardOperatorFormula().getOptimalityType())) {
                     STORM_PRINT_AND_LOG("Eliminating self-loop choices ...");
@@ -344,16 +416,14 @@ int main(const int argc, const char** argv) {
             STORM_LOG_WARN("Nothing to be done. Did you forget to specify a formula?");
         }
 
-
-
         // All operations have now been performed, so we clean up everything and terminate.
         storm::utility::cleanUp();
         return 0;
-    } catch (storm::exceptions::BaseException const &exception) {
-        STORM_LOG_ERROR("An exception caused Storm-pomdp to terminate. The message of the exception is: " << exception.what());
-        return 1;
-    } catch (std::exception const &exception) {
-        STORM_LOG_ERROR("An unexpected exception occurred and caused Storm-pomdp to terminate. The message of this exception is: " << exception.what());
-        return 2;
-    }
+    // } catch (storm::exceptions::BaseException const &exception) {
+    //    STORM_LOG_ERROR("An exception caused Storm-pomdp to terminate. The message of the exception is: " << exception.what());
+    //    return 1;
+    //} catch (std::exception const &exception) {
+    //    STORM_LOG_ERROR("An unexpected exception occurred and caused Storm-pomdp to terminate. The message of this exception is: " << exception.what());
+    //    return 2;
+    //}
 }

src/storm-pomdp/analysis/MemlessStrategySearchQualitative.cpp

@@ -0,0 +1,114 @@
+#include "storm-pomdp/analysis/MemlessStrategySearchQualitative.h"
+
+
+namespace storm {
+    namespace pomdp {
+
+        template <typename ValueType>
+        void MemlessStrategySearchQualitative<ValueType>::initialize(uint64_t k) {
+            if (maxK == -1) {
+                // not initialized at all.
+
+                // Create some data structures.
+                for(uint64_t obs = 0; obs < pomdp.getNrObservations(); ++obs) {
+                    actionSelectionVars.push_back(std::vector<storm::expressions::Expression>());
+                    statesPerObservation.push_back(std::vector<uint64_t>()); // Consider using bitvectors instead.
+                }
+
+                // Fill the states-per-observation mapping,
+                // declare the reachability variables,
+                // declare the path variables.
+                uint64_t stateId = 0;
+                for(auto obs : pomdp.getObservations()) {
+                    pathVars.push_back(std::vector<storm::expressions::Expression>());
+                    for (uint64_t i = 0; i < k; ++i) {
+                        pathVars.back().push_back(expressionManager->declareBooleanVariable("P-"+std::to_string(stateId)+"-"+std::to_string(i)).getExpression());
+                    }
+                    reachVars.push_back(expressionManager->declareBooleanVariable("C-" + std::to_string(stateId)).getExpression());
+
+                    statesPerObservation.at(obs).push_back(stateId++);
+
+                }
+                assert(pathVars.size() == pomdp.getNumberOfStates());
+
+                // Create the action selection variables.
+                uint64_t obs = 0;
+                for(auto const& statesForObservation : statesPerObservation) {
+                    for (uint64_t a = 0; a < pomdp.getNumberOfChoices(statesForObservation.front()); ++a) {
+                        std::string varName = "A-" + std::to_string(obs) + "-" + std::to_string(a);
+                        actionSelectionVars.at(obs).push_back(expressionManager->declareBooleanVariable(varName).getExpression());
+                    }
+                    ++obs;
+                }
+
+
+            } else {
+
+                assert(false);
+
+            }
+
+            uint64_t rowindex = 0;
+            for (uint64_t state = 0; state < pomdp.getNumberOfStates(); ++state) {
+                std::vector<std::vector<storm::expressions::Expression>> pathsubsubexprs;
+                for (uint64_t j = 1; j < k; ++j) {
+                    pathsubsubexprs.push_back(std::vector<storm::expressions::Expression>());
+                }
+
+                if (targetObservations.count(pomdp.getObservation(state)) > 0) {
+                    smtSolver->add(pathVars[state][0]);
+                } else {
+                    smtSolver->add(!pathVars[state][0]);
+                }
+
+                if (surelyReachSinkStates.at(state)) {
+                    smtSolver->add(!reachVars[state]);
+                }
+                else {
+                    for (uint64_t action = 0; action < pomdp.getNumberOfChoices(state); ++action) {
+                        std::vector<storm::expressions::Expression> subexprreach;
+
+                        subexprreach.push_back(!reachVars.at(state));
+                        subexprreach.push_back(!actionSelectionVars.at(pomdp.getObservation(state)).at(action));
+                        for (auto const &entries : pomdp.getTransitionMatrix().getRow(rowindex)) {
+                            subexprreach.push_back(reachVars.at(entries.getColumn()));
+                        }
+                        smtSolver->add(storm::expressions::disjunction(subexprreach));
+                        for (auto const &entries : pomdp.getTransitionMatrix().getRow(rowindex)) {
+                            for (uint64_t j = 1; j < k; ++j) {
+                                pathsubsubexprs[j - 1].push_back(pathVars[entries.getColumn()][j - 1]);
+                            }
+                        }
+                        rowindex++;
+                    }
+                    smtSolver->add(storm::expressions::implies(reachVars.at(state), pathVars.at(state).back()));
+
+
+                    for (uint64_t j = 1; j < k; ++j) {
+                        std::vector<storm::expressions::Expression> pathsubexprs;
+
+                        for (uint64_t action = 0; action < pomdp.getNumberOfChoices(state); ++action) {
+                            pathsubexprs.push_back(actionSelectionVars.at(pomdp.getObservation(state)).at(action) && storm::expressions::disjunction(pathsubsubexprs[j - 1]));
+                        }
+                        smtSolver->add(storm::expressions::iff(pathVars[state][j], storm::expressions::disjunction(pathsubexprs)));
+                    }
+                }
+
+            }
+
+            for (auto const& actionVars : actionSelectionVars) {
+                smtSolver->add(storm::expressions::disjunction(actionVars));
+            }
+
+
+
+
+            //for (auto const& )
+
+        }
+
+
+
+        template class MemlessStrategySearchQualitative<double>;
+    }
+}