made maxsat-based counterexample generation be applicable to DTMCs and MDPs

resources/examples/testfiles/dtmc/die.pm

@@ -1,5 +1,5 @@
 // Knuth's model of a fair die using only fair coins
-mdp
+dtmc
 
 module die
 

src/storm-cli-utilities/model-handling.h

@@ -373,8 +373,7 @@ namespace storm {
             STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::NotSupportedException, "Counterexample generation is currently only supported for sparse models.");
             auto sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
             
-            STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "Counterexample is currently only supported for MDPs.");
-            auto mdp = sparseModel->template as<storm::models::sparse::Mdp<ValueType>>();
+            STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Dtmc) || sparseModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "Counterexample is currently only supported for discrete-time models.");
             
             auto counterexampleSettings = storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>();
             if (counterexampleSettings.isMinimalCommandSetGenerationSet()) {
@@ -387,9 +386,15 @@ namespace storm {
                     printComputingCounterexample(property);
                     storm::utility::Stopwatch watch(true);
                     if (useMilp) {
-                        counterexample = storm::api::computePrismHighLevelCounterexampleMilp(program, mdp, property.getRawFormula());
+                        STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "Counterexample generation using MILP is currently only supported for MDPs.");
+                        counterexample = storm::api::computePrismHighLevelCounterexampleMilp(program, sparseModel->template as<storm::models::sparse::Mdp<ValueType>>(), property.getRawFormula());
                     } else {
-                        counterexample = storm::api::computePrismHighLevelCounterexampleMaxSmt(program, mdp, property.getRawFormula());
+                        STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Dtmc) || sparseModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "Counterexample generation using MaxSAT is currently only supported for discrete-time models.");
+                        if (sparseModel->isOfType(storm::models::ModelType::Dtmc)) {
+                            counterexample = storm::api::computePrismHighLevelCounterexampleMaxSmt(program, sparseModel->template as<storm::models::sparse::Dtmc<ValueType>>(), property.getRawFormula());
+                        } else {
+                            counterexample = storm::api::computePrismHighLevelCounterexampleMaxSmt(program, sparseModel->template as<storm::models::sparse::Mdp<ValueType>>(), property.getRawFormula());
+                        }
                     }
                     watch.stop();
                     printCounterexample(counterexample, &watch);

src/storm/api/counterexamples.cpp

@@ -10,9 +10,9 @@ namespace storm {
             return storm::counterexamples::MILPMinimalLabelSetGenerator<double>::computeCounterexample(env, program, *mdp, formula);
         }
         
-        std::shared_ptr<storm::counterexamples::Counterexample> computePrismHighLevelCounterexampleMaxSmt(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Mdp<double>> mdp, std::shared_ptr<storm::logic::Formula const> const& formula) {
+        std::shared_ptr<storm::counterexamples::Counterexample> computePrismHighLevelCounterexampleMaxSmt(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<double>> model, std::shared_ptr<storm::logic::Formula const> const& formula) {
             Environment env;
-            return storm::counterexamples::SMTMinimalLabelSetGenerator<double>::computeCounterexample(env, program, *mdp, formula);
+            return storm::counterexamples::SMTMinimalLabelSetGenerator<double>::computeCounterexample(env, program, *model, formula);
         }
         
     }

src/storm/api/counterexamples.h

@@ -8,7 +8,7 @@ namespace storm {
         
         std::shared_ptr<storm::counterexamples::Counterexample> computePrismHighLevelCounterexampleMilp(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Mdp<double>> mdp, std::shared_ptr<storm::logic::Formula const> const& formula);
         
-        std::shared_ptr<storm::counterexamples::Counterexample> computePrismHighLevelCounterexampleMaxSmt(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Mdp<double>> mdp, std::shared_ptr<storm::logic::Formula const> const& formula);
+        std::shared_ptr<storm::counterexamples::Counterexample> computePrismHighLevelCounterexampleMaxSmt(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<double>> model, std::shared_ptr<storm::logic::Formula const> const& formula);
         
     }
 }

src/storm/counterexamples/SMTMinimalLabelSetGenerator.h

@@ -119,7 +119,7 @@ namespace storm {
 
                 // Retrieve some references for convenient access.
                 storm::storage::SparseMatrix<T> const& transitionMatrix = model.getTransitionMatrix();
-                std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices();
+                std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices();
 
                 // Now traverse all choices of all relevant states and check whether there is a successor target state.
                 // If so, the associated labels become relevant. Also, if a choice of a relevant state has at least one
@@ -1374,7 +1374,7 @@ namespace storm {
                 }
                 
                 storm::storage::SparseMatrix<T> const& transitionMatrix = subModel.getTransitionMatrix();
-                std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = subModel.getNondeterministicChoiceIndices();
+                std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices();
                 
                 // Now determine which states and labels are actually reachable.
                 boost::container::flat_set<uint_fast64_t> reachableLabels;
@@ -1498,7 +1498,7 @@ namespace storm {
                 }
                 
                 storm::storage::SparseMatrix<T> const& transitionMatrix = subModel.getTransitionMatrix();
-                std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = subModel.getNondeterministicChoiceIndices();
+                std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices();
                 
                 // Now determine which states and labels are actually reachable.
                 boost::container::flat_set<uint_fast64_t> reachableLabels;
@@ -1821,10 +1821,10 @@ namespace storm {
                 auto startTime = std::chrono::high_resolution_clock::now();
                 
                 // Create sub-model that only contains the choices allowed by the given command set.
-                storm::models::sparse::Model<T> subModel = restrictModelToLabelSet(model, commandSet).first;
+                std::shared_ptr<storm::models::sparse::Model<T>> subModel = restrictModelToLabelSet(model, commandSet).first;
                 
                 // Then determine all prob0E(psi) states that are reachable in the sub-model.
-                storm::storage::BitVector reachableProb0EStates = storm::utility::graph::getReachableStates(subModel.getTransitionMatrix(), subModel.getInitialStates(), phiStates, psiStates);
+                storm::storage::BitVector reachableProb0EStates = storm::utility::graph::getReachableStates(subModel->getTransitionMatrix(), subModel->getInitialStates(), phiStates, psiStates);
                 
                 // Create a queue of reachable prob0E(psi) states so we can check which commands need to be added
                 // to give them a strategy that avoids psi states.
@@ -1887,6 +1887,7 @@ namespace storm {
             }
 
             static boost::container::flat_set<uint_fast64_t>  computeCounterexampleCommandSet(Environment const& env, storm::prism::Program program, storm::models::sparse::Model<T> const& model, std::shared_ptr<storm::logic::Formula const> const& formula) {
+                STORM_LOG_THROW(model.isOfType(storm::models::ModelType::Dtmc) || model.isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "MaxSAT-based counterexample generation is supported only for discrete-time models.");
                 std::cout << std::endl << "Generating minimal label counterexample for formula " << *formula << std::endl;
 
                 STORM_LOG_THROW(formula->isProbabilityOperatorFormula(), storm::exceptions::InvalidPropertyException, "Counterexample generation does not support this kind of formula. Expecting a probability operator as the outermost formula element.");

src/storm/models/sparse/NondeterministicModel.h

@@ -21,8 +21,6 @@ namespace storm {
             template<class ValueType, typename RewardModelType = StandardRewardModel<ValueType>>
             class NondeterministicModel : public Model<ValueType, RewardModelType> {
             public:
-                
-                
                 /*!
                  * Constructs a model from the given data.
                  *
@@ -39,6 +37,8 @@ namespace storm {
                  */
                 std::vector<uint_fast64_t> const& getNondeterministicChoiceIndices() const;
                 
+                using Model<ValueType, RewardModelType>::getNumberOfChoices;
+                
                 /*!
                  * @param state State for which we want to know how many choices it has
                  * 

src/storm/utility/counterexamples.h

@@ -18,20 +18,20 @@ namespace storm {
              * @return The set of labels that is visited on all paths from any state to a target state.
              */
             template <typename T>
-            std::vector<boost::container::flat_set<uint_fast64_t>> getGuaranteedLabelSets(storm::models::sparse::Mdp<T> const& mdp, std::vector<boost::container::flat_set<uint_fast64_t>> const& labelSets, storm::storage::BitVector const& psiStates, boost::container::flat_set<uint_fast64_t> const& relevantLabels) {
-                STORM_LOG_THROW(mdp.getNumberOfChoices() == labelSets.size(), storm::exceptions::InvalidArgumentException, "The given number of labels does not match the number of choices.");
+            std::vector<boost::container::flat_set<uint_fast64_t>> getGuaranteedLabelSets(storm::models::sparse::Model<T> const& model, std::vector<boost::container::flat_set<uint_fast64_t>> const& labelSets, storm::storage::BitVector const& psiStates, boost::container::flat_set<uint_fast64_t> const& relevantLabels) {
+                STORM_LOG_THROW(model.getNumberOfChoices() == labelSets.size(), storm::exceptions::InvalidArgumentException, "The given number of labels does not match the number of choices.");
                 
-                // Get some data from the MDP for convenient access.
-                storm::storage::SparseMatrix<T> const& transitionMatrix = mdp.getTransitionMatrix();
-                std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = mdp.getNondeterministicChoiceIndices();
-                storm::storage::SparseMatrix<T> backwardTransitions = mdp.getBackwardTransitions();
+                // Get some data from the model for convenient access.
+                storm::storage::SparseMatrix<T> const& transitionMatrix = model.getTransitionMatrix();
+                std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices();
+                storm::storage::SparseMatrix<T> backwardTransitions = model.getBackwardTransitions();
 
                 // Now we compute the set of labels that is present on all paths from the initial to the target states.
-                std::vector<boost::container::flat_set<uint_fast64_t>> analysisInformation(mdp.getNumberOfStates(), relevantLabels);
+                std::vector<boost::container::flat_set<uint_fast64_t>> analysisInformation(model.getNumberOfStates(), relevantLabels);
                 
                 std::queue<uint_fast64_t> worklist;
-                storm::storage::BitVector statesInWorkList(mdp.getNumberOfStates());
-                storm::storage::BitVector markedStates(mdp.getNumberOfStates());
+                storm::storage::BitVector statesInWorkList(model.getNumberOfStates());
+                storm::storage::BitVector markedStates(model.getNumberOfStates());
                 
                 // Initially, put all predecessors of target states in the worklist and empty the analysis information them.
                 for (auto state : psiStates) {
@@ -108,12 +108,12 @@ namespace storm {
              * @return The set of labels that is executed on all paths from an initial state to a target state.
              */
             template <typename T>
-            boost::container::flat_set<uint_fast64_t> getGuaranteedLabelSet(storm::models::sparse::Mdp<T> const& mdp, std::vector<boost::container::flat_set<uint_fast64_t>> const& labelSets, storm::storage::BitVector const& psiStates, boost::container::flat_set<uint_fast64_t> const& relevantLabels) {
-                std::vector<boost::container::flat_set<uint_fast64_t>> guaranteedLabels = getGuaranteedLabelSets(mdp, labelSets, psiStates, relevantLabels);
+            boost::container::flat_set<uint_fast64_t> getGuaranteedLabelSet(storm::models::sparse::Model<T> const& model, std::vector<boost::container::flat_set<uint_fast64_t>> const& labelSets, storm::storage::BitVector const& psiStates, boost::container::flat_set<uint_fast64_t> const& relevantLabels) {
+                std::vector<boost::container::flat_set<uint_fast64_t>> guaranteedLabels = getGuaranteedLabelSets(model, labelSets, psiStates, relevantLabels);
                 
                 boost::container::flat_set<uint_fast64_t> knownLabels(relevantLabels);
                 boost::container::flat_set<uint_fast64_t> tempIntersection;
-                for (auto initialState : mdp.getInitialStates()) {
+                for (auto initialState : model.getInitialStates()) {
                     std::set_intersection(knownLabels.begin(), knownLabels.end(), guaranteedLabels[initialState].begin(), guaranteedLabels[initialState].end(), std::inserter(tempIntersection, tempIntersection.end()));
                     std::swap(knownLabels, tempIntersection);
                 }