Browse Source
Fixed bug in AbstractModelChecker: it does now correctly inherit from a lot more interface classes. NOTE: checking a formula on a model checker that does not support it failed silently. This should NOT be the case. Re-enabled DEBUG option for cmake. NOTE: why was this disabled anyway? Introduced another layer AbstractDeterministicModel and AbstractNonDeterministicModel in model hierarchy to allow for easily distinguishing these classes. Made necessary adaptions in (hopefully) all classes. Move the graph analyzer to utility folder.
tempestpy_adaptions
Fixed bug in AbstractModelChecker: it does now correctly inherit from a lot more interface classes. NOTE: checking a formula on a model checker that does not support it failed silently. This should NOT be the case. Re-enabled DEBUG option for cmake. NOTE: why was this disabled anyway? Introduced another layer AbstractDeterministicModel and AbstractNonDeterministicModel in model hierarchy to allow for easily distinguishing these classes. Made necessary adaptions in (hopefully) all classes. Move the graph analyzer to utility folder.
tempestpy_adaptions
dehnert
12 years ago
19 changed files with 414 additions and 661 deletions
-
14CMakeLists.txt
-
1src/formula/ReachabilityReward.h
-
13src/modelchecker/AbstractModelChecker.h
-
5src/modelchecker/DtmcPrctlModelChecker.h
-
28src/modelchecker/GmmxxDtmcPrctlModelChecker.h
-
61src/models/AbstractDeterministicModel.h
-
140src/models/AbstractModel.h
-
49src/models/AbstractNonDeterministicModel.h
-
127src/models/Ctmc.h
-
152src/models/Ctmdp.h
-
156src/models/Dtmc.h
-
6src/models/GraphTransitions.h
-
152src/models/Mdp.h
-
79src/parser/AutoParser.cpp
-
76src/parser/AutoParser.h
-
2src/storm.cpp
-
10src/utility/GraphAnalyzer.h
-
2src/utility/IoUtility.cpp
-
2test/parser/ParseMdpTest.cpp
@ -0,0 +1,61 @@ |
|||
#ifndef STORM_MODELS_ABSTRACTDETERMINISTICMODEL_H_ |
|||
#define STORM_MODELS_ABSTRACTDETERMINISTICMODEL_H_ |
|||
|
|||
#include "AbstractModel.h" |
|||
#include "GraphTransitions.h" |
|||
|
|||
#include <memory> |
|||
|
|||
namespace storm { |
|||
|
|||
namespace models { |
|||
|
|||
/*! |
|||
* @brief Base class for all deterministic model classes. |
|||
* |
|||
* This is base class defines a common interface for all deterministic models. |
|||
*/ |
|||
template<class T> |
|||
class AbstractDeterministicModel: public AbstractModel<T> { |
|||
|
|||
public: |
|||
AbstractDeterministicModel(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix, |
|||
std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling, |
|||
std::shared_ptr<std::vector<T>> stateRewardVector, std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix) |
|||
: AbstractModel<T>(transitionMatrix, stateLabeling, stateRewardVector, transitionRewardMatrix), backwardTransitions(nullptr) { |
|||
} |
|||
|
|||
virtual ~AbstractDeterministicModel() { |
|||
// Intentionally left empty. |
|||
} |
|||
|
|||
AbstractDeterministicModel(AbstractDeterministicModel const& other) : AbstractModel<T>(other), backwardTransitions(nullptr) { |
|||
if (other.backwardTransitions != nullptr) { |
|||
backwardTransitions = new storm::models::GraphTransitions<T>(*other.backwardTransitions); |
|||
} |
|||
} |
|||
|
|||
/*! |
|||
* Retrieves a reference to the backwards transition relation. |
|||
* @return A reference to the backwards transition relation. |
|||
*/ |
|||
storm::models::GraphTransitions<T>& getBackwardTransitions() { |
|||
if (this->backwardTransitions == nullptr) { |
|||
this->backwardTransitions = std::shared_ptr<storm::models::GraphTransitions<T>>(new storm::models::GraphTransitions<T>(this->getTransitionMatrix(), this->getNumberOfStates(), false)); |
|||
} |
|||
return *this->backwardTransitions; |
|||
} |
|||
|
|||
private: |
|||
/*! |
|||
* A data structure that stores the predecessors for all states. This is |
|||
* needed for backwards directed searches. |
|||
*/ |
|||
std::shared_ptr<storm::models::GraphTransitions<T>> backwardTransitions; |
|||
}; |
|||
|
|||
} // namespace models |
|||
|
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_MODELS_ABSTRACTDETERMINISTICMODEL_H_ */ |
|||
@ -0,0 +1,49 @@ |
|||
#ifndef STORM_MODELS_ABSTRACTNONDETERMINISTICMODEL_H_ |
|||
#define STORM_MODELS_ABSTRACTNONDETERMINISTICMODEL_H_ |
|||
|
|||
#include "AbstractModel.h" |
|||
#include "GraphTransitions.h" |
|||
|
|||
#include <memory> |
|||
|
|||
namespace storm { |
|||
|
|||
namespace models { |
|||
|
|||
/*! |
|||
* @brief Base class for all non-deterministic model classes. |
|||
* |
|||
* This is base class defines a common interface for all non-deterministic models. |
|||
*/ |
|||
template<class T> |
|||
class AbstractNonDeterministicModel: public AbstractModel<T> { |
|||
|
|||
public: |
|||
AbstractNonDeterministicModel(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix, |
|||
std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling, |
|||
std::shared_ptr<std::vector<uint_fast64_t>> choiceIndices, |
|||
std::shared_ptr<std::vector<T>> stateRewardVector, |
|||
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix) |
|||
: AbstractModel<T>(transitionMatrix, stateLabeling, stateRewardVector, transitionRewardMatrix), |
|||
choiceIndices(choiceIndices) { |
|||
} |
|||
|
|||
virtual ~AbstractNonDeterministicModel() { |
|||
// Intentionally left empty. |
|||
} |
|||
|
|||
AbstractNonDeterministicModel(AbstractNonDeterministicModel const& other) : AbstractModel<T>(other), |
|||
choiceIndices(other.choiceIndices) { |
|||
|
|||
} |
|||
|
|||
private: |
|||
/*! A vector of indices mapping states to the choices (rows) in the transition matrix. */ |
|||
std::shared_ptr<std::vector<uint_fast64_t>> choiceIndices; |
|||
}; |
|||
|
|||
} // namespace models |
|||
|
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_MODELS_ABSTRACTDETERMINISTICMODEL_H_ */ |
|||
@ -1,79 +0,0 @@ |
|||
#include "src/parser/AutoParser.h"
|
|||
|
|||
#include <string>
|
|||
#include <cctype>
|
|||
|
|||
#include "src/exceptions/WrongFileFormatException.h"
|
|||
#include "src/models/AbstractModel.h"
|
|||
#include "src/parser/DeterministicModelParser.h"
|
|||
#include "src/parser/NonDeterministicModelParser.h"
|
|||
|
|||
namespace storm { |
|||
namespace parser { |
|||
|
|||
AutoParser::AutoParser(std::string const & transitionSystemFile, std::string const & labelingFile, |
|||
std::string const & stateRewardFile, std::string const & transitionRewardFile) |
|||
: model(nullptr) { |
|||
storm::models::ModelType type = this->analyzeHint(transitionSystemFile); |
|||
|
|||
if (type == storm::models::Unknown) { |
|||
LOG4CPLUS_ERROR(logger, "Could not determine file type of " << transitionSystemFile << "."); |
|||
LOG4CPLUS_ERROR(logger, "The first line of the file should contain a format hint. Please fix your file and try again."); |
|||
throw storm::exceptions::WrongFileFormatException() << "Could not determine type of file " << transitionSystemFile; |
|||
} else { |
|||
LOG4CPLUS_INFO(logger, "Model type seems to be " << type); |
|||
} |
|||
|
|||
// Do actual parsing
|
|||
switch (type) { |
|||
case storm::models::DTMC: { |
|||
DeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); |
|||
this->model = parser.getDtmc(); |
|||
break; |
|||
} |
|||
case storm::models::CTMC: { |
|||
DeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); |
|||
this->model = parser.getCtmc(); |
|||
break; |
|||
} |
|||
case storm::models::MDP: { |
|||
NonDeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); |
|||
this->model = parser.getMdp(); |
|||
break; |
|||
} |
|||
case storm::models::CTMDP: { |
|||
NonDeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); |
|||
this->model = parser.getCtmdp(); |
|||
break; |
|||
} |
|||
default: ; // Unknown
|
|||
} |
|||
|
|||
|
|||
if (!this->model) { |
|||
LOG4CPLUS_WARN(logger, "Model is still null."); |
|||
} |
|||
} |
|||
|
|||
storm::models::ModelType AutoParser::analyzeHint(const std::string& filename) { |
|||
storm::models::ModelType hintType = storm::models::Unknown; |
|||
// Open file
|
|||
MappedFile file(filename.c_str()); |
|||
char* buf = file.data; |
|||
|
|||
// parse hint
|
|||
char hint[128]; |
|||
sscanf(buf, "%s\n", hint); |
|||
for (char* c = hint; *c != '\0'; c++) *c = toupper(*c); |
|||
|
|||
// check hint
|
|||
if (strncmp(hint, "DTMC", sizeof(hint)) == 0) hintType = storm::models::DTMC; |
|||
else if (strncmp(hint, "CTMC", sizeof(hint)) == 0) hintType = storm::models::CTMC; |
|||
else if (strncmp(hint, "MDP", sizeof(hint)) == 0) hintType = storm::models::MDP; |
|||
else if (strncmp(hint, "CTMDP", sizeof(hint)) == 0) hintType = storm::models::CTMDP; |
|||
|
|||
return hintType; |
|||
} |
|||
|
|||
} // namespace parser
|
|||
} // namespace storm
|
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue