diff --git a/resources/examples/testfiles/dtmc/die.pm b/resources/examples/testfiles/dtmc/die.pm
index 1873bb8c1..e41139001 100644
--- a/resources/examples/testfiles/dtmc/die.pm
+++ b/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
diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h
index 8cf964ca5..4180bdc33 100644
--- a/src/storm-cli-utilities/model-handling.h
+++ b/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);
diff --git a/src/storm/api/counterexamples.cpp b/src/storm/api/counterexamples.cpp
index 98c2f07bf..483dc57d4 100644
--- a/src/storm/api/counterexamples.cpp
+++ b/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);
}
}
diff --git a/src/storm/api/counterexamples.h b/src/storm/api/counterexamples.h
index d8f3d1ddd..6481c4efd 100644
--- a/src/storm/api/counterexamples.h
+++ b/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);
}
}
diff --git a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h
index e659209a3..5ad54a0f5 100644
--- a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h
+++ b/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.");
diff --git a/src/storm/models/sparse/NondeterministicModel.h b/src/storm/models/sparse/NondeterministicModel.h
index 2274e137a..ac8603e7f 100644
--- a/src/storm/models/sparse/NondeterministicModel.h
+++ b/src/storm/models/sparse/NondeterministicModel.h
@@ -19,10 +19,8 @@ namespace storm {
* The base class of sparse nondeterministic models.
*/
template<class ValueType, typename RewardModelType = StandardRewardModel<ValueType>>
- class NondeterministicModel: public Model<ValueType, RewardModelType> {
+ 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
*
diff --git a/src/storm/utility/counterexamples.h b/src/storm/utility/counterexamples.h
index ec20c20cb..1ff429a5d 100644
--- a/src/storm/utility/counterexamples.h
+++ b/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);
}