Browse Source

AbstractModelChecker: add getClassName()

tempestpy_adaptions
Joachim Klein 6 years ago
committed by Christian Hensel
parent
commit
da4dfc35a8
  1. 7
      src/storm/modelchecker/AbstractModelChecker.cpp
  2. 8
      src/storm/modelchecker/AbstractModelChecker.h

7
src/storm/modelchecker/AbstractModelChecker.cpp

@ -24,9 +24,16 @@
#include "storm/storage/dd/Add.h" #include "storm/storage/dd/Add.h"
#include "storm/storage/dd/Bdd.h" #include "storm/storage/dd/Bdd.h"
#include <boost/core/typeinfo.hpp>
namespace storm { namespace storm {
namespace modelchecker { namespace modelchecker {
template<typename ModelType>
std::string AbstractModelChecker<ModelType>::getClassName() const {
return std::string(boost::core::demangled_name(BOOST_CORE_TYPEID(*this)));
}
template<typename ModelType> template<typename ModelType>
std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::check(CheckTask<storm::logic::Formula, ValueType> const& checkTask) { std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::check(CheckTask<storm::logic::Formula, ValueType> const& checkTask) {
Environment env; Environment env;

8
src/storm/modelchecker/AbstractModelChecker.h

@ -1,6 +1,7 @@
#ifndef STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_ #ifndef STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_
#define STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_ #define STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_
#include <string>
#include <boost/optional.hpp> #include <boost/optional.hpp>
#include "storm/modelchecker/CheckTask.h" #include "storm/modelchecker/CheckTask.h"
@ -24,7 +25,12 @@ namespace storm {
} }
typedef typename ModelType::ValueType ValueType; typedef typename ModelType::ValueType ValueType;
/*!
* Returns the name of the model checker class (e.g., for display in error messages).
*/
virtual std::string getClassName() const;
/*! /*!
* Determines whether the model checker can handle the given verification task. If this method returns * Determines whether the model checker can handle the given verification task. If this method returns
* false, the task must not be checked using this model checker. * false, the task must not be checked using this model checker.
Loading…
Cancel
Save