From 0a1ebc2f73d0cb1bd5d80a84ba4e9d267465be3d Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Tue, 26 Jan 2016 17:50:40 +0100
Subject: [PATCH] Distinct error message for parametric model checking
Former-commit-id: 7c1eacb9c28fdf459583f840e46d32ccd9498b8e
---
src/parser/DFTGalileoParser.cpp | 2 +-
src/utility/storm.h | 22 ++++++++++++++++------
2 files changed, 17 insertions(+), 7 deletions(-)
diff --git a/src/parser/DFTGalileoParser.cpp b/src/parser/DFTGalileoParser.cpp
index 57dec65d1..163bc1488 100644
--- a/src/parser/DFTGalileoParser.cpp
+++ b/src/parser/DFTGalileoParser.cpp
@@ -113,7 +113,7 @@ namespace storm {
ValueType dormancyFactor = parseRationalExpression(tokens[2].substr(5));
success = builder.addBasicElement(name, failureRate, dormancyFactor);
} else {
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Type name: " + tokens[1] + " not recognized.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Type name: " << tokens[1] << " not recognized.");
success = false;
}
}
diff --git a/src/utility/storm.h b/src/utility/storm.h
index d1e32f839..c3d7a891a 100644
--- a/src/utility/storm.h
+++ b/src/utility/storm.h
@@ -70,6 +70,7 @@
#include "src/exceptions/InvalidSettingsException.h"
#include "src/exceptions/InvalidTypeException.h"
#include "src/exceptions/NotImplementedException.h"
+#include "src/exceptions/NotSupportedException.h"
namespace storm {
@@ -289,13 +290,22 @@ namespace storm {
template<>
inline std::unique_ptr<storm::modelchecker::CheckResult> verifySparseModel(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula> const& formula) {
std::unique_ptr<storm::modelchecker::CheckResult> result;
- std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
-
- storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>> modelchecker(*dtmc);
- if (modelchecker.canHandle(*formula)) {
- result = modelchecker.check(*formula);
+ if (model->getType() == storm::models::ModelType::Dtmc) {
+ std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
+ storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>> modelchecker(*dtmc);
+ if (modelchecker.canHandle(*formula)) {
+ result = modelchecker.check(*formula);
+ } else {
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The parametric engine currently does not support this property on DTMCs.");
+ }
+ } else if (model->getType() == storm::models::ModelType::Mdp) {
+ std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> mdp = model->template as<storm::models::sparse::Mdp<storm::RationalFunction>>();
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The parametric engine currently does not support MDPs.");
+ } else if (model->getType() == storm::models::ModelType::Ctmc) {
+ std::shared_ptr<storm::models::sparse::Ctmc<storm::RationalFunction>> ctmc = model->template as<storm::models::sparse::Ctmc<storm::RationalFunction>>();
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The parametric engine currently does not support CTMCs.");
} else {
- STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The parametric engine currently does not support this property.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The parametric engine currently does not support " << model->getType());
}
return result;
}