moved preprocessing of PRISM program to utility to make it accessible from learning-based model checker

Former-commit-id: 704dde9ec5

src/builder/ExplicitPrismModelBuilder.cpp

@@ -182,57 +182,7 @@ namespace storm {
         }
         
         template <typename ValueType, typename RewardModelType, typename StateType>
-        ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::ExplicitPrismModelBuilder(storm::prism::Program const& program, Options const& options) : program(program), options(options) {
-            // Start by defining the undefined constants in the model.
-            if (options.constantDefinitions) {
-                this->program = program.defineUndefinedConstants(options.constantDefinitions.get());
-            } else {
-                this->program = program;
-            }
-            
-            // If the program still contains undefined constants and we are not in a parametric setting, assemble an appropriate error message.
-            if (!std::is_same<ValueType, storm::RationalFunction>::value && this->program.hasUndefinedConstants()) {
-                std::vector<std::reference_wrapper<storm::prism::Constant const>> undefinedConstants = this->program.getUndefinedConstants();
-                std::stringstream stream;
-                bool printComma = false;
-                for (auto const& constant : undefinedConstants) {
-                    if (printComma) {
-                        stream << ", ";
-                    } else {
-                        printComma = true;
-                    }
-                    stream << constant.get().getName() << " (" << constant.get().getType() << ")";
-                }
-                stream << ".";
-                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str());
-            } else if (std::is_same<ValueType, storm::RationalFunction>::value && !this->program.hasUndefinedConstantsOnlyInUpdateProbabilitiesAndRewards()) {
-                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The program contains undefined constants that appear in some places other than update probabilities and reward value expressions, which is not admitted.");
-            }
-            
-            // If the set of labels we are supposed to built is restricted, we need to remove the other labels from the program.
-            if (options.labelsToBuild) {
-                if (!options.buildAllLabels) {
-                    this->program.filterLabels(options.labelsToBuild.get());
-                }
-            }
-            
-            // If we need to build labels for expressions that may appear in some formula, we need to add appropriate
-            // labels to the program.
-            if (options.expressionLabels) {
-                std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution = this->program.getConstantsSubstitution();
-                
-                for (auto const& expression : options.expressionLabels.get()) {
-                    std::stringstream stream;
-                    stream << expression.substitute(constantsSubstitution);
-                    std::string name = stream.str();
-                    if (!this->program.hasLabel(name)) {
-                        this->program.addLabel(name, expression);
-                    }
-                }
-            }
-            
-            // Now that the program is fixed, we we need to substitute all constants with their concrete value.
-            this->program = this->program.substituteConstants();
+        ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::ExplicitPrismModelBuilder(storm::prism::Program const& program, Options const& options) : program(storm::utility::prism::preprocessProgram<ValueType>(program, options.constantDefinitions, !options.buildAllLabels ? options.labelsToBuild : boost::none, options.expressionLabels)), options(options) {
 
             // Create the variable information for the transformed program.
             this->variableInformation = VariableInformation(this->program);

src/cli/entrypoints.h

@@ -58,12 +58,12 @@ namespace storm {
         void verifySymbolicModelWithLearningEngine(storm::prism::Program const& program, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas, bool onlyInitialStatesRelevant = false) {
             
             for (auto const& formula : formulas) {
-                STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc || model->getType() == storm::models::ModelType::Mdp, storm::exceptions::InvalidSettingsException, "Currently learning-based verification is only available for DTMCs and MDPs.");
+                STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::InvalidSettingsException, "Currently learning-based verification is only available for DTMCs and MDPs.");
                 std::cout << std::endl << "Model checking property: " << *formula << " ...";
-                storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant);
-                storm::modelchecker::SparseLearningModelChecker<ValueType> checker(program);
+                storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant);
+                storm::modelchecker::SparseMdpLearningModelChecker<ValueType> checker(program);
                 std::unique_ptr<storm::modelchecker::CheckResult> result;
-                if (checker.canHandle(formula)) {
+                if (checker.canHandle(task)) {
                     std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(task);
                 } else {
                     std::cout << " skipped, because the formula cannot be handled by the selected engine/method." << std::endl;
@@ -71,13 +71,19 @@ namespace storm {
                 if (result) {
                     std::cout << " done." << std::endl;
                     std::cout << "Result (initial states): ";
-                    result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
                     std::cout << *result << std::endl;
                 } else {
                     std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
                 }
             }
         }
+        
+#ifdef STORM_HAVE_CARL
+        template<>
+        void verifySymbolicModelWithLearningEngine<storm::RationalFunction>(storm::prism::Program const& program, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas, bool onlyInitialStatesRelevant) {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Learning-based verification does currently not support parametric models.");
+        }
+#endif
 
         template<storm::dd::DdType DdType>
         void verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas, bool onlyInitialStatesRelevant = false) {

src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp

@@ -0,0 +1,28 @@
+#include "src/modelchecker/reachability/SparseMdpLearningModelChecker.h"
+
+#include "src/logic/FragmentSpecification.h"
+
+#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+
+namespace storm {
+    namespace modelchecker {
+        template<typename SparseMdpModelType>
+        SparseMdpLearningModelChecker<SparseMdpModelType>::SparseMdpLearningModelChecker(storm::prism::Program const& program) : program(program) {
+            // Intentionally left empty.
+        }
+        
+        template<typename SparseMdpModelType>
+        bool SparseMdpLearningModelChecker<SparseMdpModelType>::canHandle(CheckTask<storm::logic::Formula> const& checkTask) const {
+            storm::logic::Formula const& formula = checkTask.getFormula();
+            storm::logic::FragmentSpecification fragment = storm::logic::propositional().setProbabilityOperatorsAllowed(true).setReachabilityProbabilityFormulasAllowed(true);
+            return formula.isInFragment(fragment);
+        }
+        
+        template<typename SparseMdpModelType>
+        std::unique_ptr<CheckResult> SparseMdpLearningModelChecker<SparseMdpModelType>::computeReachabilityProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+            return nullptr;
+        }
+        
+        template class SparseMdpLearningModelChecker<double>;
+    }
+}

src/modelchecker/reachability/SparseMdpLearningModelChecker.h

@@ -0,0 +1,29 @@
+#ifndef STORM_MODELCHECKER_REACHABILITY_SPARSEMDPLEARNINGMODELCHECKER_H_
+#define STORM_MODELCHECKER_REACHABILITY_SPARSEMDPLEARNINGMODELCHECKER_H_
+
+#include "src/modelchecker/AbstractModelChecker.h"
+
+#include "src/storage/prism/Program.h"
+
+#include "src/utility/constants.h"
+
+namespace storm {
+    namespace modelchecker {
+        
+        template<typename ValueType>
+        class SparseMdpLearningModelChecker : public AbstractModelChecker {
+        public:
+            SparseMdpLearningModelChecker(storm::prism::Program const& program);
+            
+            virtual bool canHandle(CheckTask<storm::logic::Formula> const& checkTask) const override;
+
+            virtual std::unique_ptr<CheckResult> computeReachabilityProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
+            
+        private:
+            // The program that defines the model to check.
+            storm::prism::Program program;
+        };
+    }
+}
+
+#endif /* STORM_MODELCHECKER_REACHABILITY_SPARSEMDPLEARNINGMODELCHECKER_H_ */

src/utility/prism.cpp

@@ -1,13 +1,72 @@
 #include "src/utility/prism.h"
+
+#include "src/adapters/CarlAdapter.h"
+
 #include "src/storage/expressions/ExpressionManager.h"
 #include "src/storage/prism/Program.h"
 
+#include "src/utility/macros.h"
+
 #include "src/exceptions/InvalidArgumentException.h"
-#include "macros.h"
 
 namespace storm {
     namespace utility {
         namespace prism {
+            
+            template<typename ValueType>
+            storm::prism::Program preprocessProgram(storm::prism::Program const& program, boost::optional<std::map<storm::expressions::Variable, storm::expressions::Expression>> const& constantDefinitions, boost::optional<std::set<std::string>> const& restrictedLabelSet, boost::optional<std::vector<storm::expressions::Expression>> const& expressionLabels) {
+                storm::prism::Program result;
+                
+                // Start by defining the undefined constants in the model.
+                if (constantDefinitions) {
+                    result = program.defineUndefinedConstants(constantDefinitions.get());
+                } else {
+                    result = program;
+                }
+                
+                // If the program still contains undefined constants and we are not in a parametric setting, assemble an appropriate error message.
+                if (!std::is_same<ValueType, storm::RationalFunction>::value && result.hasUndefinedConstants()) {
+                    std::vector<std::reference_wrapper<storm::prism::Constant const>> undefinedConstants = result.getUndefinedConstants();
+                    std::stringstream stream;
+                    bool printComma = false;
+                    for (auto const& constant : undefinedConstants) {
+                        if (printComma) {
+                            stream << ", ";
+                        } else {
+                            printComma = true;
+                        }
+                        stream << constant.get().getName() << " (" << constant.get().getType() << ")";
+                    }
+                    stream << ".";
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str());
+                } else if (std::is_same<ValueType, storm::RationalFunction>::value && !result.hasUndefinedConstantsOnlyInUpdateProbabilitiesAndRewards()) {
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The program contains undefined constants that appear in some places other than update probabilities and reward value expressions, which is not admitted.");
+                }
+                
+                // If the set of labels we are supposed to built is restricted, we need to remove the other labels from the program.
+                if (restrictedLabelSet) {
+                    result.filterLabels(restrictedLabelSet.get());
+                }
+                
+                // Build new labels.
+                if (expressionLabels) {
+                    std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution = result.getConstantsSubstitution();
+                    
+                    for (auto const& expression : expressionLabels.get()) {
+                        std::stringstream stream;
+                        stream << expression.substitute(constantsSubstitution);
+                        std::string name = stream.str();
+                        if (!result.hasLabel(name)) {
+                            result.addLabel(name, expression);
+                        }
+                    }
+                }
+                
+                // Now that the program is fixed, we we need to substitute all constants with their concrete value.
+                result = result.substituteConstants();
+                return result;
+            }
+            
             std::map<storm::expressions::Variable, storm::expressions::Expression> parseConstantDefinitionString(storm::prism::Program const& program, std::string const& constantDefinitionString) {
                 std::map<storm::expressions::Variable, storm::expressions::Expression> constantDefinitions;
                 std::set<storm::expressions::Variable> definedConstants;
@@ -64,6 +123,11 @@ namespace storm {
                 
                 return constantDefinitions;
             }
+            
+            template storm::prism::Program preprocessProgram<double>(storm::prism::Program const& program, boost::optional<std::map<storm::expressions::Variable, storm::expressions::Expression>> const& constantDefinitions, boost::optional<std::set<std::string>> const& restrictedLabelSet, boost::optional<std::vector<storm::expressions::Expression>> const& expressionLabels);
+
+            template storm::prism::Program preprocessProgram<storm::RationalFunction>(storm::prism::Program const& program, boost::optional<std::map<storm::expressions::Variable, storm::expressions::Expression>> const& constantDefinitions, boost::optional<std::set<std::string>> const& restrictedLabelSet, boost::optional<std::vector<storm::expressions::Expression>> const& expressionLabels);
+
         }
     }
 }

src/utility/prism.h

@@ -1,13 +1,11 @@
 #ifndef STORM_UTILITY_PRISM_H_
 #define STORM_UTILITY_PRISM_H_
 
-#include <memory>
 #include <map>
-#include <boost/algorithm/string.hpp>
-#include <boost/container/flat_set.hpp>
-
-#include "src/utility/OsDetection.h"
+#include <set>
+#include <vector>
 
+#include <boost/optional.hpp>
 
 namespace storm {
     namespace expressions {
@@ -21,185 +19,9 @@ namespace storm {
     
     namespace utility {
         namespace prism {
-            // A structure holding information about a particular choice.
-            template<typename ValueType, typename KeyType=uint32_t, typename Compare=std::less<uint32_t>>
-            struct Choice {
-            public:
-                Choice(uint_fast64_t actionIndex = 0, bool createChoiceLabels = false) : distribution(), actionIndex(actionIndex), choiceLabels(nullptr) {
-                    if (createChoiceLabels) {
-                        choiceLabels = std::shared_ptr<boost::container::flat_set<uint_fast64_t>>(new boost::container::flat_set<uint_fast64_t>());
-                    }
-                }
-                
-                Choice(Choice const& other) = default;
-                Choice& operator=(Choice const& other) = default;
-#ifndef WINDOWS
-                Choice(Choice&& other) = default;
-                Choice& operator=(Choice&& other) = default;
-#endif
-                
-                /*!
-                 * Returns an iterator to the first element of this choice.
-                 *
-                 * @return An iterator to the first element of this choice.
-                 */
-                typename std::map<KeyType, ValueType>::iterator begin() {
-                    return distribution.begin();
-                }
-                
-                /*!
-                 * Returns an iterator to the first element of this choice.
-                 *
-                 * @return An iterator to the first element of this choice.
-                 */
-                typename std::map<KeyType, ValueType>::const_iterator begin() const {
-                    return distribution.cbegin();
-                }
-                
-                /*!
-                 * Returns an iterator that points past the elements of this choice.
-                 *
-                 * @return An iterator that points past the elements of this choice.
-                 */
-                typename std::map<KeyType, ValueType>::iterator end() {
-                    return distribution.end();
-                }
-                
-                /*!
-                 * Returns an iterator that points past the elements of this choice.
-                 *
-                 * @return An iterator that points past the elements of this choice.
-                 */
-                typename std::map<KeyType, ValueType>::const_iterator end() const {
-                    return distribution.cend();
-                }
-                
-                /*!
-                 * Returns an iterator to the element with the given key, if there is one. Otherwise, the iterator points to
-                 * distribution.end().
-                 *
-                 * @param value The value to find.
-                 * @return An iterator to the element with the given key, if there is one.
-                 */
-                typename std::map<KeyType, ValueType>::iterator find(uint_fast64_t value) {
-                    return distribution.find(value);
-                }
-                
-                /*!
-                 * Inserts the contents of this object to the given output stream.
-                 *
-                 * @param out The stream in which to insert the contents.
-                 */
-                friend std::ostream& operator<<(std::ostream& out, Choice<ValueType> const& choice) {
-                    out << "<";
-                    for (auto const& stateProbabilityPair : choice.distribution) {
-                        out << stateProbabilityPair.first << " : " << stateProbabilityPair.second << ", ";
-                    }
-                    out << ">";
-                    return out;
-                }
-                
-                /*!
-                 * Adds the given label to the labels associated with this choice.
-                 *
-                 * @param label The label to associate with this choice.
-                 */
-                void addChoiceLabel(uint_fast64_t label) {
-                    choiceLabels->insert(label);
-                }
-                
-                /*!
-                 * Adds the given label set to the labels associated with this choice.
-                 *
-                 * @param labelSet The label set to associate with this choice.
-                 */
-                void addChoiceLabels(boost::container::flat_set<uint_fast64_t> const& labelSet) {
-                    for (uint_fast64_t label : labelSet) {
-                        addChoiceLabel(label);
-                    }
-                }
-                
-                /*!
-                 * Retrieves the set of labels associated with this choice.
-                 *
-                 * @return The set of labels associated with this choice.
-                 */
-                boost::container::flat_set<uint_fast64_t> const& getChoiceLabels() const {
-                    return *choiceLabels;
-                }
-                
-                /*!
-                 * Retrieves the index of the action of this choice.
-                 *
-                 * @return The index of the action of this choice.
-                 */
-                uint_fast64_t getActionIndex() const {
-                    return actionIndex;
-                }
-                
-                /*!
-                 * Retrieves the total mass of this choice.
-                 *
-                 * @return The total mass.
-                 */
-                ValueType getTotalMass() const {
-                    return totalMass;
-                }
-                
-                /*!
-                 * Retrieves the entry in the choice that is associated with the given state and creates one if none exists,
-                 * yet.
-                 *
-                 * @param state The state for which to add the entry.
-                 * @return A reference to the entry that is associated with the given state.
-                 */
-                ValueType& getOrAddEntry(uint_fast64_t state) {
-                    auto stateProbabilityPair = distribution.find(state);
-                    
-                    if (stateProbabilityPair == distribution.end()) {
-                        distribution[state] = ValueType();
-                    }
-                    return distribution.at(state);
-                }
-                
-                /*!
-                 * Retrieves the entry in the choice that is associated with the given state and creates one if none exists,
-                 * yet.
-                 *
-                 * @param state The state for which to add the entry.
-                 * @return A reference to the entry that is associated with the given state.
-                 */
-                ValueType const& getOrAddEntry(uint_fast64_t state) const {
-                    auto stateProbabilityPair = distribution.find(state);
-                    
-                    if (stateProbabilityPair == distribution.end()) {
-                        distribution[state] = ValueType();
-                    }
-                    return distribution.at(state);
-                }
-                
-                void addProbability(KeyType state, ValueType value) {
-                    totalMass += value;
-                    distribution[state] += value;
-                }
-                
-                std::size_t size() const {
-                    return distribution.size();
-                }
-                
-            private:
-                // The distribution that is associated with the choice.
-                std::map<KeyType, ValueType, Compare> distribution;
-        
-                // The total probability mass (or rates) of this choice.
-                ValueType totalMass;
-        
-                // The index of the action name.
-                uint_fast64_t actionIndex;
-                
-                // The labels that are associated with this choice.
-                std::shared_ptr<boost::container::flat_set<uint_fast64_t>> choiceLabels;
-            };
+            
+            template<typename ValueType>
+            storm::prism::Program preprocessProgram(storm::prism::Program const& program, boost::optional<std::map<storm::expressions::Variable, storm::expressions::Expression>> const& constantDefinitions = boost::none, boost::optional<std::set<std::string>> const& restrictedLabelSet = boost::none, boost::optional<std::vector<storm::expressions::Expression>> const& expressionLabels = boost::none);
             
             std::map<storm::expressions::Variable, storm::expressions::Expression> parseConstantDefinitionString(storm::prism::Program const& program, std::string const& constantDefinitionString);
             

src/utility/storm.h

@@ -57,6 +57,7 @@
 #include "src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h"
 #include "src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h"
 #include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h"
+#include "src/modelchecker/reachability/SparseMdpLearningModelChecker.h"
 #include "src/modelchecker/csl/SparseCtmcCslModelChecker.h"
 #include "src/modelchecker/csl/HybridCtmcCslModelChecker.h"
 #include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h"