Lanchid
13 years ago
36 changed files with 723 additions and 129 deletions
-
2src/formula/AbstractFormula.h
-
2src/formula/AbstractPathFormula.h
-
4src/formula/AbstractStateFormula.h
-
2src/formula/And.h
-
2src/formula/Ap.h
-
6src/formula/BoundedEventually.h
-
10src/formula/BoundedNaryUntil.h
-
2src/formula/BoundedUntil.h
-
6src/formula/Eventually.h
-
5src/formula/Formulas.h
-
6src/formula/NoBoundOperator.h
-
2src/formula/Not.h
-
28src/formula/PathBoundOperator.h
-
14src/formula/ProbabilisticBoundOperator.h
-
2src/formula/ReachabilityReward.h
-
12src/formula/RewardBoundOperator.h
-
197src/formula/StateBoundOperator.h
-
119src/formula/SteadyStateOperator.h
-
0src/modelchecker/AbstractModelChecker.h
-
6src/modelchecker/DtmcPrctlModelChecker.h
-
2src/modelchecker/EigenDtmcPrctlModelChecker.h
-
0src/modelchecker/ForwardDeclarations.h
-
2src/modelchecker/GmmxxDtmcPrctlModelChecker.h
-
251src/models/Ctmdp.h
-
2src/models/GraphTransitions.h
-
9src/parser/AutoParser.cpp
-
4src/parser/DeterministicModelParser.h
-
40src/parser/MdpParser.h
-
20src/parser/NonDeterministicModelParser.cpp
-
62src/parser/NonDeterministicModelParser.h
-
16src/parser/PrctlParser.cpp
-
4src/storm.cpp
-
1test/parser/.gitignore
-
6test/parser/ParseMdpTest.cpp
-
4test/parser/PrctlParserTest.cpp
-
2test/storm-tests.cpp
@ -0,0 +1,197 @@ |
|||||
|
/* |
||||
|
* BoundOperator.h |
||||
|
* |
||||
|
* Created on: 27.12.2012 |
||||
|
* Author: Christian Dehnert |
||||
|
*/ |
||||
|
|
||||
|
#ifndef STORM_FORMULA_STATEBOUNDOPERATOR_H_ |
||||
|
#define STORM_FORMULA_STATEBOUNDOPERATOR_H_ |
||||
|
|
||||
|
#include "src/formula/AbstractStateFormula.h" |
||||
|
#include "src/formula/AbstractPathFormula.h" |
||||
|
#include "src/formula/AbstractFormulaChecker.h" |
||||
|
#include "src/modelchecker/AbstractModelChecker.h" |
||||
|
#include "src/utility/ConstTemplates.h" |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace formula { |
||||
|
|
||||
|
template <class T> class StateBoundOperator; |
||||
|
|
||||
|
/*! |
||||
|
* @brief Interface class for model checkers that support StateBoundOperator. |
||||
|
* |
||||
|
* All model checkers that support the formula class StateBoundOperator must inherit |
||||
|
* this pure virtual class. |
||||
|
*/ |
||||
|
template <class T> |
||||
|
class IStateBoundOperatorModelChecker { |
||||
|
public: |
||||
|
virtual storm::storage::BitVector* checkStateBoundOperator(const StateBoundOperator<T>& obj) const = 0; |
||||
|
}; |
||||
|
|
||||
|
/*! |
||||
|
* @brief |
||||
|
* Class for a Abstract formula tree with a P (probablistic) operator node over a probability interval |
||||
|
* as root. |
||||
|
* |
||||
|
* Has one Abstract state formula as sub formula/tree. |
||||
|
* |
||||
|
* @par Semantics |
||||
|
* The formula holds iff the probability that the state formula holds is inside the bounds |
||||
|
* specified in this operator |
||||
|
* |
||||
|
* The subtree is seen as part of the object and deleted with it |
||||
|
* (this behavior can be prevented by setting them to NULL before deletion) |
||||
|
* |
||||
|
* |
||||
|
* @see AbstractStateFormula |
||||
|
* @see AbstractPathFormula |
||||
|
* @see ProbabilisticOperator |
||||
|
* @see ProbabilisticNoBoundsOperator |
||||
|
* @see AbstractFormula |
||||
|
*/ |
||||
|
template<class T> |
||||
|
class StateBoundOperator : public AbstractStateFormula<T> { |
||||
|
|
||||
|
public: |
||||
|
enum ComparisonType { LESS, LESS_EQUAL, GREATER, GREATER_EQUAL }; |
||||
|
|
||||
|
/*! |
||||
|
* Constructor |
||||
|
* |
||||
|
* @param comparisonOperator The relation for the bound. |
||||
|
* @param bound The bound for the probability |
||||
|
* @param stateFormula The child node |
||||
|
*/ |
||||
|
StateBoundOperator(ComparisonType comparisonOperator, T bound, AbstractStateFormula<T>* stateFormula) |
||||
|
: comparisonOperator(comparisonOperator), bound(bound), stateFormula(stateFormula) { |
||||
|
// Intentionally left empty |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Destructor |
||||
|
* |
||||
|
* The subtree is deleted with the object |
||||
|
* (this behavior can be prevented by setting them to NULL before deletion) |
||||
|
*/ |
||||
|
virtual ~StateBoundOperator() { |
||||
|
if (stateFormula != nullptr) { |
||||
|
delete stateFormula; |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* @returns the child node (representation of a Abstract state formula) |
||||
|
*/ |
||||
|
const AbstractStateFormula<T>& getStateFormula () const { |
||||
|
return *stateFormula; |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Sets the child node |
||||
|
* |
||||
|
* @param stateFormula the state formula that becomes the new child node |
||||
|
*/ |
||||
|
void setStateFormula(AbstractStateFormula<T>* stateFormula) { |
||||
|
this->stateFormula = stateFormula; |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* @returns the comparison relation |
||||
|
*/ |
||||
|
const ComparisonType getComparisonOperator() const { |
||||
|
return comparisonOperator; |
||||
|
} |
||||
|
|
||||
|
void setComparisonOperator(ComparisonType comparisonOperator) { |
||||
|
this->comparisonOperator = comparisonOperator; |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* @returns the bound for the measure |
||||
|
*/ |
||||
|
const T& getBound() const { |
||||
|
return bound; |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Sets the interval in which the probability that the path formula holds may lie in. |
||||
|
* |
||||
|
* @param bound The bound for the measure |
||||
|
*/ |
||||
|
void setBound(T bound) { |
||||
|
this->bound = bound; |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* @returns a string representation of the formula |
||||
|
*/ |
||||
|
virtual std::string toString() const { |
||||
|
std::string result = ""; |
||||
|
switch (comparisonOperator) { |
||||
|
case LESS: result += "< "; break; |
||||
|
case LESS_EQUAL: result += "<= "; break; |
||||
|
case GREATER: result += "> "; break; |
||||
|
case GREATER_EQUAL: result += ">= "; break; |
||||
|
} |
||||
|
result += std::to_string(bound); |
||||
|
result += " ["; |
||||
|
result += stateFormula->toString(); |
||||
|
result += "]"; |
||||
|
return result; |
||||
|
} |
||||
|
|
||||
|
bool meetsBound(T value) const { |
||||
|
switch (comparisonOperator) { |
||||
|
case LESS: return value < bound; break; |
||||
|
case LESS_EQUAL: return value <= bound; break; |
||||
|
case GREATER: return value > bound; break; |
||||
|
case GREATER_EQUAL: return value >= bound; break; |
||||
|
default: return false; |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Clones the called object. |
||||
|
* |
||||
|
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones |
||||
|
* |
||||
|
* @returns a new AND-object that is identical the called object. |
||||
|
*/ |
||||
|
virtual AbstractStateFormula<T>* clone() const = 0; |
||||
|
|
||||
|
/*! |
||||
|
* Calls the model checker to check this formula. |
||||
|
* Needed to infer the correct type of formula class. |
||||
|
* |
||||
|
* @note This function should only be called in a generic check function of a model checker class. For other uses, |
||||
|
* the methods of the model checker should be used. |
||||
|
* |
||||
|
* @returns A bit vector indicating all states that satisfy the formula represented by the called object. |
||||
|
*/ |
||||
|
virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const { |
||||
|
return modelChecker.template as<IStateBoundOperatorModelChecker>()->checkStateBoundOperator(*this); |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* @brief Checks if the subtree conforms to some logic. |
||||
|
* |
||||
|
* @param checker Formula checker object. |
||||
|
* @return true iff the subtree conforms to some logic. |
||||
|
*/ |
||||
|
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const { |
||||
|
return checker.conforms(this->stateFormula); |
||||
|
} |
||||
|
|
||||
|
private: |
||||
|
ComparisonType comparisonOperator; |
||||
|
T bound; |
||||
|
AbstractStateFormula<T>* stateFormula; |
||||
|
}; |
||||
|
|
||||
|
} //namespace formula |
||||
|
} //namespace storm |
||||
|
|
||||
|
#endif /* STORM_FORMULA_STATEBOUNDOPERATOR_H_ */ |
||||
@ -0,0 +1,119 @@ |
|||||
|
/* |
||||
|
* SteadyState.h |
||||
|
* |
||||
|
* Created on: 19.10.2012 |
||||
|
* Author: Thomas Heinemann |
||||
|
*/ |
||||
|
|
||||
|
#ifndef STORM_FORMULA_STEADYSTATEOPERATOR_H_ |
||||
|
#define STORM_FORMULA_STEADYSTATEOPERATOR_H_ |
||||
|
|
||||
|
#include "src/formula/AbstractPathFormula.h" |
||||
|
#include "src/formula/AbstractStateFormula.h" |
||||
|
#include "src/formula/StateBoundOperator.h" |
||||
|
#include "src/formula/AbstractFormulaChecker.h" |
||||
|
|
||||
|
namespace storm { |
||||
|
|
||||
|
namespace formula { |
||||
|
|
||||
|
template <class T> class SteadyStateOperator; |
||||
|
|
||||
|
/*! |
||||
|
* @brief Interface class for model checkers that support SteadyStateOperator. |
||||
|
* |
||||
|
* All model checkers that support the formula class SteadyStateOperator must inherit |
||||
|
* this pure virtual class. |
||||
|
*/ |
||||
|
template <class T> |
||||
|
class ISteadyStateOperatorModelChecker { |
||||
|
public: |
||||
|
/*! |
||||
|
* @brief Evaluates SteadyStateOperator formula within a model checker. |
||||
|
* |
||||
|
* @param obj Formula object with subformulas. |
||||
|
* @return Result of the formula for every node. |
||||
|
*/ |
||||
|
virtual storm::storage::BitVector* checkSteadyStateOperator(const SteadyStateOperator<T>& obj) const = 0; |
||||
|
}; |
||||
|
|
||||
|
/*! |
||||
|
* @brief |
||||
|
* Class for a Abstract (path) formula tree with a SteadyStateOperator node as root. |
||||
|
* |
||||
|
* Has two Abstract state formulas as sub formulas/trees. |
||||
|
* |
||||
|
* @par Semantics |
||||
|
* The formula holds iff \e child holds SteadyStateOperator step, \e child holds |
||||
|
* |
||||
|
* The subtree is seen as part of the object and deleted with the object |
||||
|
* (this behavior can be prevented by setting them to NULL before deletion) |
||||
|
* |
||||
|
* @see AbstractPathFormula |
||||
|
* @see AbstractFormula |
||||
|
*/ |
||||
|
template <class T> |
||||
|
class SteadyStateOperator : public StateBoundOperator<T> { |
||||
|
|
||||
|
public: |
||||
|
/*! |
||||
|
* Empty constructor |
||||
|
*/ |
||||
|
SteadyStateOperator() : StateBoundOperator<T> |
||||
|
(StateBoundOperator<T>::LESS_EQUAL, storm::utility::constGetZero<T>(), nullptr) { |
||||
|
// Intentionally left empty |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Constructor |
||||
|
* |
||||
|
* @param stateFormula The child node |
||||
|
*/ |
||||
|
SteadyStateOperator( |
||||
|
typename StateBoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractStateFormula<T>* stateFormula) : |
||||
|
StateBoundOperator<T>(comparisonRelation, bound, stateFormula) { |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* @returns a string representation of the formula |
||||
|
*/ |
||||
|
virtual std::string toString() const { |
||||
|
std::string result = "("; |
||||
|
result += " S "; |
||||
|
result += StateBoundOperator<T>::toString(); |
||||
|
result += ")"; |
||||
|
return result; |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Clones the called object. |
||||
|
* |
||||
|
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones |
||||
|
* |
||||
|
* @returns a new BoundedUntil-object that is identical the called object. |
||||
|
*/ |
||||
|
virtual AbstractStateFormula<T>* clone() const { |
||||
|
SteadyStateOperator<T>* result = new SteadyStateOperator<T>(); |
||||
|
result->setStateFormula(this->getStateFormula().clone()); |
||||
|
return result; |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Calls the model checker to check this formula. |
||||
|
* Needed to infer the correct type of formula class. |
||||
|
* |
||||
|
* @note This function should only be called in a generic check function of a model checker class. For other uses, |
||||
|
* the methods of the model checker should be used. |
||||
|
* |
||||
|
* @returns A vector indicating the probability that the formula holds for each state. |
||||
|
*/ |
||||
|
virtual storm::storage::BitVector* check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const { |
||||
|
return modelChecker.template as<ISteadyStateOperatorModelChecker>()->checkSteadyStateOperator(*this); |
||||
|
} |
||||
|
|
||||
|
}; |
||||
|
|
||||
|
} //namespace formula |
||||
|
} //namespace storm |
||||
|
|
||||
|
#endif /* STORM_FORMULA_STEADYSTATEOPERATOR_H_ */ |
||||
@ -0,0 +1,251 @@ |
|||||
|
/* |
||||
|
* Ctmdp.h |
||||
|
* |
||||
|
* Created on: 14.01.2013 |
||||
|
* Author: Philipp Berger |
||||
|
*/ |
||||
|
|
||||
|
#ifndef STORM_MODELS_CTMDP_H_ |
||||
|
#define STORM_MODELS_CTMDP_H_ |
||||
|
|
||||
|
#include <ostream> |
||||
|
#include <iostream> |
||||
|
#include <memory> |
||||
|
#include <cstdlib> |
||||
|
|
||||
|
#include "AtomicPropositionsLabeling.h" |
||||
|
#include "GraphTransitions.h" |
||||
|
#include "src/storage/SparseMatrix.h" |
||||
|
#include "src/exceptions/InvalidArgumentException.h" |
||||
|
#include "src/utility/CommandLine.h" |
||||
|
#include "src/utility/Settings.h" |
||||
|
#include "src/models/AbstractModel.h" |
||||
|
#include "src/parser/NonDeterministicSparseTransitionParser.h" |
||||
|
|
||||
|
namespace storm { |
||||
|
|
||||
|
namespace models { |
||||
|
|
||||
|
/*! |
||||
|
* This class represents a Markov Decision Process (CTMDP) whose states are |
||||
|
* labeled with atomic propositions. |
||||
|
*/ |
||||
|
template <class T> |
||||
|
class Ctmdp : public storm::models::AbstractModel { |
||||
|
|
||||
|
public: |
||||
|
//! Constructor |
||||
|
/*! |
||||
|
* Constructs a CTMDP object from the given transition probability matrix and |
||||
|
* the given labeling of the states. |
||||
|
* @param probabilityMatrix The transition probability relation of the |
||||
|
* CTMDP given by a matrix. |
||||
|
* @param stateLabeling The labeling that assigns a set of atomic |
||||
|
* propositions to each state. |
||||
|
*/ |
||||
|
Ctmdp(std::shared_ptr<storm::storage::SparseMatrix<T>> probabilityMatrix, |
||||
|
std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling, |
||||
|
std::shared_ptr<std::vector<uint_fast64_t>> rowMapping, |
||||
|
std::shared_ptr<std::vector<T>> stateRewards = nullptr, |
||||
|
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix = nullptr) |
||||
|
: probabilityMatrix(probabilityMatrix), stateLabeling(stateLabeling), rowMapping(rowMapping), |
||||
|
stateRewards(stateRewards), transitionRewardMatrix(transitionRewardMatrix), |
||||
|
backwardTransitions(nullptr) { |
||||
|
if (!this->checkValidityOfProbabilityMatrix()) { |
||||
|
LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); |
||||
|
throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
//! Copy Constructor |
||||
|
/*! |
||||
|
* Copy Constructor. Performs a deep copy of the given CTMDP. |
||||
|
* @param ctmdp A reference to the CTMDP that is to be copied. |
||||
|
*/ |
||||
|
Ctmdp(const Ctmdp<T> &ctmdp) : probabilityMatrix(ctmdp.probabilityMatrix), |
||||
|
stateLabeling(ctmdp.stateLabeling), rowMapping(ctmdp.rowMapping), stateRewards(ctmdp.stateRewards), |
||||
|
transitionRewardMatrix(ctmdp.transitionRewardMatrix) { |
||||
|
if (ctmdp.backwardTransitions != nullptr) { |
||||
|
this->backwardTransitions = new storm::models::GraphTransitions<T>(*ctmdp.backwardTransitions); |
||||
|
} |
||||
|
if (!this->checkValidityOfProbabilityMatrix()) { |
||||
|
LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); |
||||
|
throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
//! Destructor |
||||
|
/*! |
||||
|
* Destructor. Frees the matrix and labeling associated with this CTMDP. |
||||
|
*/ |
||||
|
~Ctmdp() { |
||||
|
if (this->backwardTransitions != nullptr) { |
||||
|
delete this->backwardTransitions; |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Returns the state space size of the CTMDP. |
||||
|
* @return The size of the state space of the CTMDP. |
||||
|
*/ |
||||
|
uint_fast64_t getNumberOfStates() const { |
||||
|
return this->probabilityMatrix->getColumnCount(); |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Returns the number of (non-zero) transitions of the CTMDP. |
||||
|
* @return The number of (non-zero) transitions of the CTMDP. |
||||
|
*/ |
||||
|
uint_fast64_t getNumberOfTransitions() const { |
||||
|
return this->probabilityMatrix->getNonZeroEntryCount(); |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Returns a bit vector in which exactly those bits are set to true that |
||||
|
* correspond to a state labeled with the given atomic proposition. |
||||
|
* @param ap The atomic proposition for which to get the bit vector. |
||||
|
* @return A bit vector in which exactly those bits are set to true that |
||||
|
* correspond to a state labeled with the given atomic proposition. |
||||
|
*/ |
||||
|
storm::storage::BitVector* getLabeledStates(std::string ap) const { |
||||
|
return this->stateLabeling->getAtomicProposition(ap); |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Returns a pointer to the matrix representing the transition probability |
||||
|
* function. |
||||
|
* @return A pointer to the matrix representing the transition probability |
||||
|
* function. |
||||
|
*/ |
||||
|
std::shared_ptr<storm::storage::SparseMatrix<T>> getTransitionProbabilityMatrix() const { |
||||
|
return this->probabilityMatrix; |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Returns a pointer to the matrix representing the transition rewards. |
||||
|
* @return A pointer to the matrix representing the transition rewards. |
||||
|
*/ |
||||
|
std::shared_ptr<storm::storage::SparseMatrix<T>> getTransitionRewardMatrix() const { |
||||
|
return this->transitionRewardMatrix; |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Returns a pointer to the vector representing the state rewards. |
||||
|
* @return A pointer to the vector representing the state rewards. |
||||
|
*/ |
||||
|
std::shared_ptr<std::vector<T>> getStateRewards() const { |
||||
|
return this->stateRewards; |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* |
||||
|
*/ |
||||
|
std::set<std::string> const getPropositionsForState(uint_fast64_t const &state) const { |
||||
|
return stateLabeling->getPropositionsForState(state); |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* 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 = new storm::models::GraphTransitions<T>(this->probabilityMatrix, false); |
||||
|
} |
||||
|
return *this->backwardTransitions; |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves whether this CTMDP has a state reward model. |
||||
|
* @return True if this CTMDP has a state reward model. |
||||
|
*/ |
||||
|
bool hasStateRewards() { |
||||
|
return this->stateRewards != nullptr; |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves whether this CTMDP has a transition reward model. |
||||
|
* @return True if this CTMDP has a transition reward model. |
||||
|
*/ |
||||
|
bool hasTransitionRewards() { |
||||
|
return this->transitionRewardMatrix != nullptr; |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves whether the given atomic proposition is a valid atomic proposition in this model. |
||||
|
* @param atomicProposition The atomic proposition to be checked for validity. |
||||
|
* @return True if the given atomic proposition is valid in this model. |
||||
|
*/ |
||||
|
bool hasAtomicProposition(std::string const& atomicProposition) { |
||||
|
return this->stateLabeling->containsAtomicProposition(atomicProposition); |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Prints information about the model to the specified stream. |
||||
|
* @param out The stream the information is to be printed to. |
||||
|
*/ |
||||
|
void printModelInformationToStream(std::ostream& out) const { |
||||
|
storm::utility::printSeparationLine(out); |
||||
|
out << std::endl; |
||||
|
out << "Model type: \t\tCTMDP" << std::endl; |
||||
|
out << "States: \t\t" << this->getNumberOfStates() << std::endl; |
||||
|
out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl; |
||||
|
this->stateLabeling->printAtomicPropositionsInformationToStream(out); |
||||
|
out << "Size in memory: \t" |
||||
|
<< (this->probabilityMatrix->getSizeInMemory() + |
||||
|
this->stateLabeling->getSizeInMemory() + |
||||
|
sizeof(*this))/1024 << " kbytes" << std::endl; |
||||
|
out << std::endl; |
||||
|
storm::utility::printSeparationLine(out); |
||||
|
} |
||||
|
|
||||
|
storm::models::ModelType getType() { |
||||
|
return CTMDP; |
||||
|
} |
||||
|
|
||||
|
private: |
||||
|
|
||||
|
/*! |
||||
|
* @brief Perform some sanity checks. |
||||
|
* |
||||
|
* Checks probability matrix if all rows sum up to one. |
||||
|
*/ |
||||
|
bool checkValidityOfProbabilityMatrix() { |
||||
|
// Get the settings object to customize linear solving. |
||||
|
storm::settings::Settings* s = storm::settings::instance(); |
||||
|
double precision = s->get<double>("precision"); |
||||
|
for (uint_fast64_t row = 0; row < this->probabilityMatrix->getRowCount(); row++) { |
||||
|
T sum = this->probabilityMatrix->getRowSum(row); |
||||
|
if (sum == 0) continue; |
||||
|
if (std::abs(sum - 1) > precision) return false; |
||||
|
} |
||||
|
return true; |
||||
|
} |
||||
|
|
||||
|
/*! A matrix representing the transition probability function of the CTMDP. */ |
||||
|
std::shared_ptr<storm::storage::SparseMatrix<T>> probabilityMatrix; |
||||
|
|
||||
|
/*! The labeling of the states of the CTMDP. */ |
||||
|
std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling; |
||||
|
|
||||
|
/*! The mapping from states to rows. */ |
||||
|
std::shared_ptr<std::vector<uint_fast64_t>> rowMapping; |
||||
|
|
||||
|
/*! The state-based rewards of the CTMDP. */ |
||||
|
std::shared_ptr<std::vector<T>> stateRewards; |
||||
|
|
||||
|
/*! The transition-based rewards of the CTMDP. */ |
||||
|
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix; |
||||
|
|
||||
|
/*! |
||||
|
* A data structure that stores the predecessors for all states. This is |
||||
|
* needed for backwards directed searches. |
||||
|
*/ |
||||
|
storm::models::GraphTransitions<T>* backwardTransitions; |
||||
|
}; |
||||
|
|
||||
|
} // namespace models |
||||
|
|
||||
|
} // namespace storm |
||||
|
|
||||
|
#endif /* STORM_MODELS_CTMDP_H_ */ |
||||
@ -1,40 +0,0 @@ |
|||||
/* |
|
||||
* MdpParser.h |
|
||||
* |
|
||||
* Created on: 14.01.2013 |
|
||||
* Author: thomas |
|
||||
*/ |
|
||||
|
|
||||
#ifndef STORM_PARSER_MDPPARSER_H_ |
|
||||
#define STORM_PARSER_MDPPARSER_H_ |
|
||||
|
|
||||
#include "src/parser/Parser.h" |
|
||||
#include "src/models/Mdp.h" |
|
||||
|
|
||||
namespace storm { |
|
||||
namespace parser { |
|
||||
|
|
||||
/*! |
|
||||
* @brief Load label and transition file and return initialized mdp object |
|
||||
* |
|
||||
* @Note This class creates a new Mdp object that can |
|
||||
* be accessed via getMdp(). However, it will not delete this object! |
|
||||
* |
|
||||
* @Note The labeling representation in the file may use at most as much nodes as are specified in the mdp. |
|
||||
*/ |
|
||||
class MdpParser: public storm::parser::Parser { |
|
||||
public: |
|
||||
MdpParser(std::string const & transitionSystemFile, std::string const & labelingFile, |
|
||||
std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); |
|
||||
|
|
||||
std::shared_ptr<storm::models::Mdp<double>> getMdp() { |
|
||||
return this->mdp; |
|
||||
} |
|
||||
|
|
||||
private: |
|
||||
std::shared_ptr<storm::models::Mdp<double>> mdp; |
|
||||
}; |
|
||||
|
|
||||
} /* namespace parser */ |
|
||||
} /* namespace storm */ |
|
||||
#endif /* STORM_PARSER_MDPPARSER_H_ */ |
|
||||
@ -0,0 +1,62 @@ |
|||||
|
/* |
||||
|
* NonDeterministicModelParser.h |
||||
|
* |
||||
|
* Created on: 14.01.2013 |
||||
|
* Author: thomas |
||||
|
*/ |
||||
|
|
||||
|
#ifndef STORM_PARSER_NONDETERMINISTICMODELPARSER_H_ |
||||
|
#define STORM_PARSER_NONDETERMINISTICMODELPARSER_H_ |
||||
|
|
||||
|
#include "src/parser/Parser.h" |
||||
|
#include "src/models/Mdp.h" |
||||
|
#include "src/models/Ctmdp.h" |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace parser { |
||||
|
|
||||
|
/*! |
||||
|
* @brief Load label and transition file and return initialized mdp object |
||||
|
* |
||||
|
* @note This class creates a new Mdp object that can |
||||
|
* be accessed via getMdp(). However, it will not delete this object! |
||||
|
* |
||||
|
* @note The labeling representation in the file may use at most as much nodes as are specified in the mdp. |
||||
|
*/ |
||||
|
class NonDeterministicModelParser: public storm::parser::Parser { |
||||
|
public: |
||||
|
NonDeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile, |
||||
|
std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); |
||||
|
|
||||
|
std::shared_ptr<storm::models::Mdp<double>> getMdp() { |
||||
|
if (this->mdp == nullptr) { |
||||
|
this->mdp = std::shared_ptr<storm::models::Mdp<double>>(new storm::models::Mdp<double>( |
||||
|
this->probabilityMatrix, this->stateLabeling, this->rowMapping, this->stateRewards, this->transitionRewardMatrix |
||||
|
)); |
||||
|
} |
||||
|
return this->mdp; |
||||
|
} |
||||
|
|
||||
|
std::shared_ptr<storm::models::Ctmdp<double>> getCtmdp() { |
||||
|
if (this->ctmdp == nullptr) { |
||||
|
this->ctmdp = std::shared_ptr<storm::models::Ctmdp<double>>(new storm::models::Ctmdp<double>( |
||||
|
this->probabilityMatrix, this->stateLabeling, this->rowMapping, this->stateRewards, this->transitionRewardMatrix |
||||
|
)); |
||||
|
} |
||||
|
return this->ctmdp; |
||||
|
} |
||||
|
|
||||
|
private: |
||||
|
std::shared_ptr<storm::storage::SparseMatrix<double>> probabilityMatrix; |
||||
|
std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling; |
||||
|
std::shared_ptr<std::vector<uint_fast64_t>> rowMapping; |
||||
|
std::shared_ptr<std::vector<double>> stateRewards; |
||||
|
std::shared_ptr<storm::storage::SparseMatrix<double>> transitionRewardMatrix; |
||||
|
|
||||
|
std::shared_ptr<storm::models::Mdp<double>> mdp; |
||||
|
std::shared_ptr<storm::models::Ctmdp<double>> ctmdp; |
||||
|
}; |
||||
|
|
||||
|
} /* namespace parser */ |
||||
|
} /* namespace storm */ |
||||
|
#endif /* STORM_PARSER_NONDETERMINISTICMODELPARSER_H_ */ |
||||
@ -0,0 +1 @@ |
|||||
|
/output.dot |
||||
Write
Preview
Loading…
Cancel
Save
Reference in new issue