dehnert
12 years ago
57 changed files with 4385 additions and 529 deletions
-
32CMakeLists.txt
-
3109resources/cmake/cotire.cmake
-
2src/formula/AbstractFormula.h
-
2src/formula/AbstractPathFormula.h
-
4src/formula/AbstractStateFormula.h
-
4src/formula/And.h
-
2src/formula/Ap.h
-
6src/formula/BoundedEventually.h
-
11src/formula/BoundedNaryUntil.h
-
3src/formula/BoundedUntil.h
-
6src/formula/Eventually.h
-
11src/formula/Formulas.h
-
1src/formula/Globally.h
-
6src/formula/NoBoundOperator.h
-
2src/formula/Not.h
-
2src/formula/Or.h
-
47src/formula/PathBoundOperator.h
-
11src/formula/PrctlFormulaChecker.h
-
30src/formula/ProbabilisticBoundOperator.h
-
2src/formula/ReachabilityReward.h
-
29src/formula/RewardBoundOperator.h
-
197src/formula/StateBoundOperator.h
-
119src/formula/SteadyStateOperator.h
-
13src/modelchecker/AbstractModelChecker.h
-
27src/modelchecker/DtmcPrctlModelChecker.h
-
2src/modelchecker/EigenDtmcPrctlModelChecker.h
-
26src/modelchecker/ForwardDeclarations.h
-
2src/modelchecker/GmmxxDtmcPrctlModelChecker.h
-
251src/models/Ctmdp.h
-
6src/models/GraphTransitions.h
-
9src/parser/AutoParser.cpp
-
4src/parser/DeterministicModelParser.h
-
40src/parser/MdpParser.h
-
20src/parser/NonDeterministicModelParser.cpp
-
62src/parser/NonDeterministicModelParser.h
-
32src/parser/PrctlFileParser.cpp
-
24src/parser/PrctlFileParser.h
-
312src/parser/PrctlParser.cpp
-
23src/parser/PrctlParser.h
-
13src/storage/SparseMatrix.h
-
4src/storm.cpp
-
8src/utility/ConstTemplates.h
-
4src/utility/Vector.h
-
183src/vector/dense_vector.h
-
1test/parser/.gitignore
-
14test/parser/ParseMdpTest.cpp
-
159test/parser/PrctlParserTest.cpp
-
1test/parser/prctl_files/apOnly.prctl
-
1test/parser/prctl_files/complexFormula.prctl
-
1test/parser/prctl_files/probabilisticFormula.prctl
-
1test/parser/prctl_files/probabilisticNoBoundFormula.prctl
-
1test/parser/prctl_files/propositionalFormula.prctl
-
1test/parser/prctl_files/rewardFormula.prctl
-
1test/parser/prctl_files/rewardNoBoundFormula.prctl
-
2test/storm-tests.cpp
3109
resources/cmake/cotire.cmake
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
@ -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,26 @@ |
|||
/* |
|||
* ForwardDeclarations.h |
|||
* |
|||
* Created on: 14.01.2013 |
|||
* Author: thomas |
|||
*/ |
|||
|
|||
#ifndef STORM_MODELCHECKER_FORWARDDECLARATIONS_H_ |
|||
#define STORM_MODELCHECKER_FORWARDDECLARATIONS_H_ |
|||
|
|||
|
|||
namespace storm { |
|||
|
|||
namespace modelChecker { |
|||
|
|||
template <class Type> |
|||
class AbstractModelChecker; |
|||
|
|||
template <class Type> |
|||
class DtmcPrctlModelChecker; |
|||
|
|||
} //namespace modelChecker |
|||
|
|||
} //namespace storm |
|||
|
|||
#endif /* STORM_MODELCHECKER_FORWARDDECLARATIONS_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,32 @@ |
|||
/*
|
|||
* PrctlFileParser.cpp |
|||
* |
|||
* Created on: 06.02.2013 |
|||
* Author: Thomas Heinemann |
|||
*/ |
|||
|
|||
#include "PrctlFileParser.h"
|
|||
|
|||
namespace storm { |
|||
namespace parser { |
|||
|
|||
PrctlFileParser::PrctlFileParser(std::string filename) { |
|||
// Open file and initialize result.
|
|||
std::ifstream inputFileStream(filename, std::ios::in); |
|||
|
|||
// Prepare iterators to input.
|
|||
// TODO: Right now, this parses the whole contents of the file into a string first.
|
|||
// While this is usually not necessary, because there exist adapters that make an input stream
|
|||
// iterable in both directions without storing it into a string, using the corresponding
|
|||
// Boost classes gives an awful output under valgrind and is thus disabled for the time being.
|
|||
std::string fileContent((std::istreambuf_iterator<char>(inputFileStream)), (std::istreambuf_iterator<char>())); |
|||
parse(fileContent); |
|||
} |
|||
|
|||
PrctlFileParser::~PrctlFileParser() { |
|||
//intentionally left empty
|
|||
//formulas are not deleted with the parser!
|
|||
} |
|||
|
|||
} /* namespace parser */ |
|||
} /* namespace storm */ |
|||
@ -0,0 +1,24 @@ |
|||
/* |
|||
* PrctlFileParser.h |
|||
* |
|||
* Created on: 06.02.2013 |
|||
* Author: Thomas Heinemann |
|||
*/ |
|||
|
|||
#ifndef STORM_PARSER_PRCTLFILEPARSER_H_ |
|||
#define STORM_PARSER_PRCTLFILEPARSER_H_ |
|||
|
|||
#include "PrctlParser.h" |
|||
|
|||
namespace storm { |
|||
namespace parser { |
|||
|
|||
class PrctlFileParser: public storm::parser::PrctlParser { |
|||
public: |
|||
PrctlFileParser(std::string filename); |
|||
virtual ~PrctlFileParser(); |
|||
}; |
|||
|
|||
} /* namespace parser */ |
|||
} /* namespace storm */ |
|||
#endif /* STORM_PARSER_PRCTLFILEPARSER_H_ */ |
|||
@ -1,147 +1,193 @@ |
|||
#include "src/parser/PrctlParser.h"
|
|||
#include "src/utility/OsDetection.h"
|
|||
#include "src/utility/ConstTemplates.h"
|
|||
|
|||
#include <iostream>
|
|||
#include <map>
|
|||
//#include <pair>
|
|||
// If the parser fails due to ill-formed data, this exception is thrown.
|
|||
#include "src/exceptions/WrongFileFormatException.h"
|
|||
|
|||
#include <boost/spirit/include/classic_core.hpp>
|
|||
#include <boost/spirit/include/qi_grammar.hpp>
|
|||
#include <boost/spirit/include/qi_rule.hpp>
|
|||
// Used for Boost spirit.
|
|||
#include <boost/typeof/typeof.hpp>
|
|||
#include <boost/spirit/include/qi.hpp>
|
|||
#include <boost/spirit/include/phoenix_operator.hpp>
|
|||
#include <boost/spirit/include/qi_char_class.hpp>
|
|||
|
|||
#include <boost/bind.hpp>
|
|||
|
|||
namespace bs = boost::spirit; |
|||
|
|||
namespace |
|||
{ |
|||
using namespace bs; |
|||
using namespace bs::qi; |
|||
using namespace bs::standard; |
|||
|
|||
struct SpiritParser : public grammar< char const* > |
|||
{ |
|||
typedef rule< char const* > rule_none; |
|||
typedef rule< char const*, double() > rule_double; |
|||
typedef rule< char const*, std::string() > rule_string; |
|||
|
|||
/*!
|
|||
* @brief Generic Nonterminals. |
|||
*/ |
|||
rule_none ws; |
|||
rule_string variable; |
|||
rule_double value; |
|||
|
|||
/*!
|
|||
* @brief Nonterminals for file header. |
|||
*/ |
|||
rule< char const* > varDef; |
|||
rule_none type; |
|||
|
|||
/*!
|
|||
* @brief Nonterminals for formula. |
|||
*/ |
|||
rule_none formula, opP; |
|||
|
|||
/*!
|
|||
* @brief Nonterminals for high-level file structure. |
|||
*/ |
|||
rule_none file, header; |
|||
|
|||
/*!
|
|||
* @brief Variable assignments. |
|||
*/ |
|||
std::map<std::string, double> variables; |
|||
|
|||
/*!
|
|||
* @brief Resulting formula. |
|||
*/ |
|||
//storm::formula::PctlFormula<double>* result;
|
|||
|
|||
struct dump |
|||
{ |
|||
void print(double const& i, std::string& s) |
|||
{ |
|||
std::cout << s << " = " << i << std::endl; |
|||
} |
|||
void operator()(double const& a, unused_type, unused_type) const |
|||
{ |
|||
std::cout << a << std::endl; |
|||
} |
|||
void operator()(std::string const& a, unused_type, unused_type) const |
|||
{ |
|||
std::cout << a << std::endl; |
|||
} |
|||
void operator()(utree const& a, unused_type, unused_type) const |
|||
{ |
|||
std::cout << &a << std::endl; |
|||
#include <boost/spirit/include/phoenix.hpp>
|
|||
|
|||
// Include headers for spirit iterators. Needed for diagnostics and input stream iteration.
|
|||
#include <boost/spirit/include/classic_position_iterator.hpp>
|
|||
#include <boost/spirit/include/support_multi_pass.hpp>
|
|||
|
|||
// Needed for file IO.
|
|||
#include <fstream>
|
|||
#include <iomanip>
|
|||
|
|||
|
|||
// Some typedefs and namespace definitions to reduce code size.
|
|||
typedef std::string::const_iterator BaseIteratorType; |
|||
typedef boost::spirit::classic::position_iterator2<BaseIteratorType> PositionIteratorType; |
|||
namespace qi = boost::spirit::qi; |
|||
namespace phoenix = boost::phoenix; |
|||
|
|||
|
|||
|
|||
namespace storm { |
|||
|
|||
namespace parser { |
|||
|
|||
template<typename Iterator, typename Skipper> |
|||
struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::formula::AbstractFormula<double>*(), Skipper> { |
|||
PrctlGrammar() : PrctlGrammar::base_type(start) { |
|||
freeIdentifierName = qi::lexeme[+(qi::alpha | qi::char_('_'))]; |
|||
|
|||
//This block defines rules for parsing state formulas
|
|||
stateFormula %= orFormula; |
|||
stateFormula.name("state formula"); |
|||
|
|||
andFormula = notFormula[qi::_val = qi::_1] > *(qi::lit("&") > notFormula)[qi::_val = |
|||
phoenix::new_<storm::formula::And<double>>(qi::_val, qi::_1)]; |
|||
andFormula.name("state formula"); |
|||
orFormula = andFormula[qi::_val = qi::_1] > *(qi::lit("|") > andFormula)[qi::_val = |
|||
phoenix::new_<storm::formula::Or<double>>(qi::_val, qi::_1)]; |
|||
orFormula.name("state formula"); |
|||
notFormula = atomicStateFormula[qi::_val = qi::_1] | (qi::lit("!") > atomicStateFormula)[qi::_val = |
|||
phoenix::new_<storm::formula::Not<double>>(qi::_1)]; |
|||
notFormula.name("state formula"); |
|||
|
|||
atomicStateFormula %= probabilisticBoundOperator | rewardBoundOperator | atomicProposition | qi::lit("(") >> stateFormula >> qi::lit(")"); |
|||
atomicStateFormula.name("state formula"); |
|||
atomicProposition = (freeIdentifierName)[qi::_val = |
|||
phoenix::new_<storm::formula::Ap<double>>(qi::_1)]; |
|||
atomicProposition.name("state formula"); |
|||
probabilisticBoundOperator = ( |
|||
(qi::lit("P") >> qi::lit(">") >> qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = |
|||
phoenix::new_<storm::formula::ProbabilisticBoundOperator<double> >(storm::formula::PathBoundOperator<double>::GREATER, qi::_1, qi::_2)] | |
|||
(qi::lit("P") >> qi::lit(">=") > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = |
|||
phoenix::new_<storm::formula::ProbabilisticBoundOperator<double> >(storm::formula::PathBoundOperator<double>::GREATER_EQUAL, qi::_1, qi::_2)] | |
|||
(qi::lit("P") >> qi::lit("<") >> qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = |
|||
phoenix::new_<storm::formula::ProbabilisticBoundOperator<double> >(storm::formula::PathBoundOperator<double>::LESS, qi::_1, qi::_2)] | |
|||
(qi::lit("P") >> qi::lit("<=") > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = |
|||
phoenix::new_<storm::formula::ProbabilisticBoundOperator<double> >(storm::formula::PathBoundOperator<double>::LESS_EQUAL, qi::_1, qi::_2)] |
|||
); |
|||
probabilisticBoundOperator.name("state formula"); |
|||
rewardBoundOperator = ( |
|||
(qi::lit("R") >> qi::lit(">") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = |
|||
phoenix::new_<storm::formula::RewardBoundOperator<double> >(storm::formula::PathBoundOperator<double>::GREATER, qi::_1, qi::_2)] | |
|||
(qi::lit("R") >> qi::lit(">=") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = |
|||
phoenix::new_<storm::formula::RewardBoundOperator<double> >(storm::formula::PathBoundOperator<double>::GREATER_EQUAL, qi::_1, qi::_2)] | |
|||
(qi::lit("R") >> qi::lit("<") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = |
|||
phoenix::new_<storm::formula::RewardBoundOperator<double> >(storm::formula::PathBoundOperator<double>::LESS, qi::_1, qi::_2)] | |
|||
(qi::lit("R") >> qi::lit("<=")>> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = |
|||
phoenix::new_<storm::formula::RewardBoundOperator<double> >(storm::formula::PathBoundOperator<double>::LESS_EQUAL, qi::_1, qi::_2)] |
|||
); |
|||
rewardBoundOperator.name("state formula"); |
|||
|
|||
//This block defines rules for parsing formulas with noBoundOperators
|
|||
noBoundOperator = (probabilisticNoBoundOperator | rewardNoBoundOperator); |
|||
noBoundOperator.name("no bound operator"); |
|||
probabilisticNoBoundOperator = (qi::lit("P") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = |
|||
phoenix::new_<storm::formula::ProbabilisticNoBoundOperator<double> >(qi::_1)]; |
|||
probabilisticNoBoundOperator.name("no bound operator"); |
|||
rewardNoBoundOperator = (qi::lit("R") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = |
|||
phoenix::new_<storm::formula::RewardNoBoundOperator<double> >(qi::_1)]; |
|||
rewardNoBoundOperator.name("no bound operator"); |
|||
|
|||
//This block defines rules for parsing path formulas
|
|||
pathFormula = (boundedEventually | eventually | globally | boundedUntil | until); |
|||
pathFormula.name("path formula"); |
|||
boundedEventually = (qi::lit("F") >> qi::lit("<=") > qi::int_ > stateFormula)[qi::_val = |
|||
phoenix::new_<storm::formula::BoundedEventually<double>>(qi::_2, qi::_1)]; |
|||
boundedEventually.name("path formula"); |
|||
eventually = (qi::lit("F") > stateFormula)[qi::_val = |
|||
phoenix::new_<storm::formula::Eventually<double> >(qi::_1)]; |
|||
eventually.name("path formula"); |
|||
globally = (qi::lit("G") > stateFormula)[qi::_val = |
|||
phoenix::new_<storm::formula::Globally<double> >(qi::_1)]; |
|||
globally.name("path formula"); |
|||
boundedUntil = (stateFormula >> qi::lit("U") >> qi::lit("<=") > qi::int_ > stateFormula)[qi::_val = |
|||
phoenix::new_<storm::formula::BoundedUntil<double>>(qi::_1, qi::_3, qi::_2)]; |
|||
boundedUntil.name("path formula"); |
|||
until = (stateFormula >> qi::lit("U") > stateFormula)[qi::_val = |
|||
phoenix::new_<storm::formula::Until<double>>(qi::_1, qi::_2)]; |
|||
until.name("path formula"); |
|||
|
|||
start = (noBoundOperator | stateFormula); |
|||
start.name("PRCTL formula"); |
|||
} |
|||
|
|||
qi::rule<Iterator, storm::formula::AbstractFormula<double>*(), Skipper> start; |
|||
|
|||
qi::rule<Iterator, storm::formula::AbstractStateFormula<double>*(), Skipper> stateFormula; |
|||
qi::rule<Iterator, storm::formula::AbstractStateFormula<double>*(), Skipper> atomicStateFormula; |
|||
|
|||
qi::rule<Iterator, storm::formula::AbstractStateFormula<double>*(), Skipper> andFormula; |
|||
qi::rule<Iterator, storm::formula::AbstractStateFormula<double>*(), Skipper> atomicProposition; |
|||
qi::rule<Iterator, storm::formula::AbstractStateFormula<double>*(), Skipper> orFormula; |
|||
qi::rule<Iterator, storm::formula::AbstractStateFormula<double>*(), Skipper> notFormula; |
|||
qi::rule<Iterator, storm::formula::ProbabilisticBoundOperator<double>*(), Skipper> probabilisticBoundOperator; |
|||
qi::rule<Iterator, storm::formula::RewardBoundOperator<double>*(), Skipper> rewardBoundOperator; |
|||
|
|||
qi::rule<Iterator, storm::formula::NoBoundOperator<double>*(), Skipper> noBoundOperator; |
|||
qi::rule<Iterator, storm::formula::NoBoundOperator<double>*(), Skipper> probabilisticNoBoundOperator; |
|||
qi::rule<Iterator, storm::formula::NoBoundOperator<double>*(), Skipper> rewardNoBoundOperator; |
|||
|
|||
qi::rule<Iterator, storm::formula::AbstractPathFormula<double>*(), Skipper> pathFormula; |
|||
qi::rule<Iterator, storm::formula::BoundedEventually<double>*(), Skipper> boundedEventually; |
|||
qi::rule<Iterator, storm::formula::Eventually<double>*(), Skipper> eventually; |
|||
qi::rule<Iterator, storm::formula::Globally<double>*(), Skipper> globally; |
|||
qi::rule<Iterator, storm::formula::BoundedUntil<double>*(), Skipper> boundedUntil; |
|||
qi::rule<Iterator, storm::formula::Until<double>*(), Skipper> until; |
|||
|
|||
qi::rule<Iterator, std::string(), Skipper> freeIdentifierName; |
|||
|
|||
}; |
|||
|
|||
SpiritParser() : SpiritParser::base_type(file, "PRCTL parser") |
|||
{ |
|||
variable %= alnum; |
|||
ws = *( space ); |
|||
value %= ( double_ | int_ ); // double_ must be *before* int_
|
|||
type = string("int") | string("double"); |
|||
|
|||
/*
|
|||
* Todo: |
|||
* Use two arguments at one point in the code, e.g. do something like |
|||
* this->variables[ variable ] = value |
|||
* |
|||
* You can have local variables in rules, but somehow does not work. |
|||
* You can also (somehow) let a rule return some arbitrary class and let boost magically collect the arguments for the constructor. |
|||
* No idea how this can possibly work, did not get this to work. |
|||
* You can also generate a syntax tree and do this manually (-> utree)... somehow. |
|||
* |
|||
* Attention: spirit had some major upgrades in the last few releases. 1.48 already lacks some features that might be useful. |
|||
* |
|||
* The rules parse the const definitions of |
|||
* http://www.prismmodelchecker.org/manual/PropertySpecification/PropertiesFiles
|
|||
* We actually do not need them, but the problems I described above are fairly generic. |
|||
* We will not be able to parse the formulas if we don't solve them... |
|||
* |
|||
* Example input: |
|||
* const int k = 7; |
|||
* const double T = 9; |
|||
* const double p = 0.01; |
|||
* |
|||
* Parser can be run via ./storm --test-prctl <filename> foo bar |
|||
* foo and bar are necessary, otherwise the option parser fails... |
|||
*/ |
|||
|
|||
varDef = |
|||
string("const") >> ws >> |
|||
type >> ws >> |
|||
variable >> ws >> |
|||
string("=") >> ws >> |
|||
value >> ws >> |
|||
string(";"); |
|||
|
|||
header = +( varDef >> ws ); |
|||
|
|||
file = header; |
|||
} //namespace storm
|
|||
} //namespace parser
|
|||
|
|||
void storm::parser::PrctlParser::parse(std::string formulaString) { |
|||
BaseIteratorType stringIteratorBegin = formulaString.begin(); |
|||
BaseIteratorType stringIteratorEnd = formulaString.end(); |
|||
PositionIteratorType positionIteratorBegin(stringIteratorBegin, stringIteratorEnd, formulaString); |
|||
PositionIteratorType positionIteratorEnd; |
|||
|
|||
|
|||
// Prepare resulting intermediate representation of input.
|
|||
storm::formula::AbstractFormula<double>* result_pointer = nullptr; |
|||
|
|||
PrctlGrammar<PositionIteratorType, BOOST_TYPEOF(boost::spirit::ascii::space)> grammar; |
|||
|
|||
try { |
|||
qi::phrase_parse(positionIteratorBegin, positionIteratorEnd, grammar, boost::spirit::ascii::space, result_pointer); |
|||
} catch(const qi::expectation_failure<PositionIteratorType>& e) { |
|||
// If the parser expected content different than the one provided, display information
|
|||
// about the location of the error.
|
|||
const boost::spirit::classic::file_position_base<std::string>& pos = e.first.get_position(); |
|||
|
|||
// Construct the error message including a caret display of the position in the
|
|||
// erroneous line.
|
|||
std::stringstream msg; |
|||
msg << pos.file << ", line " << pos.line << ", column " << pos.column |
|||
<< ": parse error: expected " << e.what_ << std::endl << "\t" |
|||
<< e.first.get_currentline() << std::endl << "\t"; |
|||
int i = 0; |
|||
for (i = 0; i < pos.column; ++i) { |
|||
msg << "-"; |
|||
} |
|||
msg << "^"; |
|||
for (; i < 80; ++i) { |
|||
msg << "-"; |
|||
} |
|||
msg << std::endl; |
|||
|
|||
std::cerr << msg.str(); |
|||
|
|||
}; |
|||
// Now propagate exception.
|
|||
throw storm::exceptions::WrongFileFormatException() << msg.str(); |
|||
} |
|||
if (result_pointer == nullptr) { |
|||
throw storm::exceptions::WrongFileFormatException() << "Syntax error in formula"; |
|||
} |
|||
|
|||
storm::parser::PrctlParser::PrctlParser(const char* filename) |
|||
{ |
|||
SpiritParser p; |
|||
storm::parser::MappedFile file(filename); |
|||
|
|||
char* data = file.data; |
|||
if (bs::qi::parse< char const* >(data, file.dataend, p)) |
|||
{ |
|||
std::cout << "File was parsed" << std::endl; |
|||
std::string rest(data, file.dataend); |
|||
std::cout << "Rest: " << rest << std::endl; |
|||
//this->formula = p.result;
|
|||
formula = result_pointer; |
|||
} |
|||
//else this->formula = NULL;
|
|||
|
|||
storm::parser::PrctlParser::PrctlParser(std::string formula) { |
|||
parse(formula); |
|||
} |
|||
@ -1,183 +0,0 @@ |
|||
#ifndef MRMC_VECTOR_BITVECTOR_H_ |
|||
#define MRMC_VECTOR_BITVECTOR_H_ |
|||
|
|||
#include <exception> |
|||
#include <new> |
|||
#include <cmath> |
|||
#include "boost/integer/integer_mask.hpp" |
|||
|
|||
#include <pantheios/pantheios.hpp> |
|||
#include <pantheios/inserters/integer.hpp> |
|||
|
|||
#include "src/exceptions/invalid_state.h" |
|||
#include "src/exceptions/invalid_argument.h" |
|||
#include "src/exceptions/out_of_range.h" |
|||
|
|||
namespace mrmc { |
|||
|
|||
namespace vector { |
|||
|
|||
//! A Vector |
|||
/*! |
|||
A bit vector for boolean fields or quick selection schemas on Matrix entries. |
|||
Does NOT perform index bound checks! |
|||
*/ |
|||
template <class T> |
|||
class DenseVector { |
|||
public: |
|||
//! Constructor |
|||
/*! |
|||
\param initial_length The initial size of the boolean Array. Can be changed later on via BitVector::resize() |
|||
*/ |
|||
BitVector(uint_fast64_t initial_length) { |
|||
bucket_count = initial_length / 64; |
|||
if (initial_length % 64 != 0) { |
|||
++bucket_count; |
|||
} |
|||
bucket_array = new uint_fast64_t[bucket_count](); |
|||
|
|||
// init all 0 |
|||
for (uint_fast64_t i = 0; i < bucket_count; ++i) { |
|||
bucket_array[i] = 0; |
|||
} |
|||
} |
|||
|
|||
//! Copy Constructor |
|||
/*! |
|||
Copy Constructor. Creates an exact copy of the source bit vector bv. Modification of either bit vector does not affect the other. |
|||
@param bv A reference to the bit vector that should be copied from |
|||
*/ |
|||
BitVector(const BitVector &bv) : bucket_count(bv.bucket_count) |
|||
{ |
|||
pantheios::log_DEBUG("BitVector::CopyCTor: Using Copy() Ctor."); |
|||
bucket_array = new uint_fast64_t[bucket_count](); |
|||
memcpy(bucket_array, bv.bucket_array, sizeof(uint_fast64_t) * bucket_count); |
|||
} |
|||
|
|||
~BitVector() { |
|||
if (bucket_array != NULL) { |
|||
delete[] bucket_array; |
|||
} |
|||
} |
|||
|
|||
void resize(uint_fast64_t new_length) { |
|||
uint_fast64_t* tempArray = new uint_fast64_t[new_length](); |
|||
|
|||
// 64 bit/entries per uint_fast64_t |
|||
uint_fast64_t copySize = (new_length <= (bucket_count * 64)) ? (new_length/64) : (bucket_count); |
|||
memcpy(tempArray, bucket_array, sizeof(uint_fast64_t) * copySize); |
|||
|
|||
bucket_count = new_length / 64; |
|||
if (new_length % 64 != 0) { |
|||
++bucket_count; |
|||
} |
|||
|
|||
delete[] bucket_array; |
|||
bucket_array = tempArray; |
|||
} |
|||
|
|||
void set(const uint_fast64_t index, const bool value) { |
|||
uint_fast64_t bucket = index / 64; |
|||
// Taking the step with mask is crucial as we NEED a 64bit shift, not a 32bit one. |
|||
// MSVC: C4334, use 1i64 or cast to __int64. |
|||
// result of 32-bit shift implicitly converted to 64 bits (was 64-bit shift intended?) |
|||
uint_fast64_t mask = 1; |
|||
mask = mask << (index % 64); |
|||
if (value) { |
|||
bucket_array[bucket] |= mask; |
|||
} else { |
|||
bucket_array[bucket] &= ~mask; |
|||
} |
|||
} |
|||
|
|||
bool get(const uint_fast64_t index) { |
|||
uint_fast64_t bucket = index / 64; |
|||
// Taking the step with mask is crucial as we NEED a 64bit shift, not a 32bit one. |
|||
// MSVC: C4334, use 1i64 or cast to __int64. |
|||
// result of 32-bit shift implicitly converted to 64 bits (was 64-bit shift intended?) |
|||
uint_fast64_t mask = 1; |
|||
mask = mask << (index % 64); |
|||
return ((bucket_array[bucket] & mask) == mask); |
|||
} |
|||
|
|||
// Operators |
|||
BitVector operator &(BitVector const &bv) { |
|||
uint_fast64_t minSize = (bv.bucket_count < this->bucket_count) ? bv.bucket_count : this->bucket_count; |
|||
BitVector result(minSize * 64); |
|||
for (uint_fast64_t i = 0; i < minSize; ++i) { |
|||
result.bucket_array[i] = this->bucket_array[i] & bv.bucket_array[i]; |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
BitVector operator |(BitVector const &bv) { |
|||
uint_fast64_t minSize = (bv.bucket_count < this->bucket_count) ? bv.bucket_count : this->bucket_count; |
|||
BitVector result(minSize * 64); |
|||
for (uint_fast64_t i = 0; i < minSize; ++i) { |
|||
result.bucket_array[i] = this->bucket_array[i] | bv.bucket_array[i]; |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
|
|||
BitVector operator ^(BitVector const &bv) { |
|||
uint_fast64_t minSize = (bv.bucket_count < this->bucket_count) ? bv.bucket_count : this->bucket_count; |
|||
BitVector result(minSize * 64); |
|||
for (uint_fast64_t i = 0; i < minSize; ++i) { |
|||
result.bucket_array[i] = this->bucket_array[i] ^ bv.bucket_array[i]; |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
|
|||
BitVector operator ~() { |
|||
BitVector result(this->bucket_count * 64); |
|||
for (uint_fast64_t i = 0; i < this->bucket_count; ++i) { |
|||
result.bucket_array[i] = ~this->bucket_array[i]; |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
|
|||
/*! |
|||
* Returns the number of bits that are set (to one) in this bit vector. |
|||
* @return The number of bits that are set (to one) in this bit vector. |
|||
*/ |
|||
uint_fast64_t getNumberOfSetBits() { |
|||
uint_fast64_t set_bits = 0; |
|||
for (uint_fast64_t i = 0; i < bucket_count; i++) { |
|||
#ifdef __GNUG__ // check if we are using g++ and use built-in function if available |
|||
set_bits += __builtin_popcount (this->bucket_array[i]); |
|||
#else |
|||
uint_fast32_t cnt; |
|||
uint_fast64_t bitset = this->bucket_array[i]; |
|||
for (cnt = 0; bitset; cnt++) { |
|||
bitset &= bitset - 1; |
|||
} |
|||
set_bits += cnt; |
|||
#endif |
|||
} |
|||
return set_bits; |
|||
} |
|||
|
|||
/*! |
|||
* Returns the size of the bit vector in memory measured in bytes. |
|||
* @return The size of the bit vector in memory measured in bytes. |
|||
*/ |
|||
uint_fast64_t getSizeInMemory() { |
|||
return sizeof(*this) + sizeof(uint_fast64_t) * bucket_count; |
|||
} |
|||
|
|||
private: |
|||
uint_fast64_t bucket_count; |
|||
|
|||
/*! Array containing the boolean bits for each node, 64bits/64nodes per element */ |
|||
uint_fast64_t* bucket_array; |
|||
|
|||
}; |
|||
|
|||
} // namespace vector |
|||
|
|||
} // namespace mrmc |
|||
|
|||
#endif // MRMC_SPARSE_STATIC_SPARSE_MATRIX_H_ |
|||
@ -0,0 +1 @@ |
|||
/output.dot |
|||
@ -0,0 +1,159 @@ |
|||
/*
|
|||
* PrctlParserTest.cpp |
|||
* |
|||
* Created on: 01.02.2013 |
|||
* Author: Thomas Heinemann |
|||
*/ |
|||
|
|||
|
|||
#include "gtest/gtest.h"
|
|||
#include "storm-config.h"
|
|||
#include "src/parser/PrctlParser.h"
|
|||
#include "src/parser/PrctlFileParser.h"
|
|||
|
|||
TEST(PrctlParserTest, parseApOnlyTest) { |
|||
std::string ap = "ap"; |
|||
storm::parser::PrctlParser* prctlParser = nullptr; |
|||
ASSERT_NO_THROW( |
|||
prctlParser = new storm::parser::PrctlParser(ap); |
|||
); |
|||
|
|||
ASSERT_NE(prctlParser->getFormula(), nullptr); |
|||
|
|||
|
|||
ASSERT_EQ(ap, prctlParser->getFormula()->toString()); |
|||
|
|||
delete prctlParser->getFormula(); |
|||
delete prctlParser; |
|||
|
|||
} |
|||
|
|||
TEST(PrctlParserTest, parsePropositionalFormulaTest) { |
|||
storm::parser::PrctlFileParser* prctlFileParser = nullptr; |
|||
ASSERT_NO_THROW( |
|||
prctlFileParser = new storm::parser::PrctlFileParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/propositionalFormula.prctl") |
|||
); |
|||
|
|||
ASSERT_NE(prctlFileParser->getFormula(), nullptr); |
|||
|
|||
|
|||
ASSERT_EQ(prctlFileParser->getFormula()->toString(), "(!(a & b) | (a & !c))"); |
|||
|
|||
delete prctlFileParser->getFormula(); |
|||
delete prctlFileParser; |
|||
|
|||
} |
|||
|
|||
TEST(PrctlParserTest, parseProbabilisticFormulaTest) { |
|||
storm::parser::PrctlFileParser* prctlFileParser = nullptr; |
|||
ASSERT_NO_THROW( |
|||
prctlFileParser = new storm::parser::PrctlFileParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/probabilisticFormula.prctl") |
|||
); |
|||
|
|||
ASSERT_NE(prctlFileParser->getFormula(), nullptr); |
|||
|
|||
storm::formula::ProbabilisticBoundOperator<double>* op = static_cast<storm::formula::ProbabilisticBoundOperator<double>*>(prctlFileParser->getFormula()); |
|||
|
|||
ASSERT_EQ(storm::formula::PathBoundOperator<double>::GREATER, op->getComparisonOperator()); |
|||
ASSERT_EQ(0.5, op->getBound()); |
|||
|
|||
ASSERT_EQ(prctlFileParser->getFormula()->toString(), "P > 0.500000 [F a]"); |
|||
|
|||
delete prctlFileParser->getFormula(); |
|||
delete prctlFileParser; |
|||
|
|||
} |
|||
|
|||
TEST(PrctlParserTest, parseRewardFormulaTest) { |
|||
storm::parser::PrctlFileParser* prctlFileParser = nullptr; |
|||
ASSERT_NO_THROW( |
|||
prctlFileParser = new storm::parser::PrctlFileParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/rewardFormula.prctl") |
|||
); |
|||
|
|||
ASSERT_NE(prctlFileParser->getFormula(), nullptr); |
|||
|
|||
storm::formula::RewardBoundOperator<double>* op = static_cast<storm::formula::RewardBoundOperator<double>*>(prctlFileParser->getFormula()); |
|||
|
|||
ASSERT_EQ(storm::formula::PathBoundOperator<double>::GREATER_EQUAL, op->getComparisonOperator()); |
|||
ASSERT_EQ(15.0, op->getBound()); |
|||
|
|||
ASSERT_EQ(prctlFileParser->getFormula()->toString(), "R >= 15.000000 [(a U !b)]"); |
|||
|
|||
delete prctlFileParser->getFormula(); |
|||
delete prctlFileParser; |
|||
} |
|||
|
|||
TEST(PrctlParserTest, parseRewardNoBoundFormulaTest) { |
|||
storm::parser::PrctlFileParser* prctlFileParser = nullptr; |
|||
ASSERT_NO_THROW( |
|||
prctlFileParser = new storm::parser::PrctlFileParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/rewardNoBoundFormula.prctl") |
|||
); |
|||
|
|||
ASSERT_NE(prctlFileParser->getFormula(), nullptr); |
|||
|
|||
|
|||
ASSERT_EQ(prctlFileParser->getFormula()->toString(), "R = ? [(a U<=4 (b & !c))]"); |
|||
|
|||
delete prctlFileParser->getFormula(); |
|||
delete prctlFileParser; |
|||
|
|||
} |
|||
|
|||
TEST(PrctlParserTest, parseProbabilisticNoBoundFormulaTest) { |
|||
storm::parser::PrctlFileParser* prctlFileParser = nullptr; |
|||
ASSERT_NO_THROW( |
|||
prctlFileParser = new storm::parser::PrctlFileParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/probabilisticNoBoundFormula.prctl") |
|||
); |
|||
|
|||
ASSERT_NE(prctlFileParser->getFormula(), nullptr); |
|||
|
|||
|
|||
ASSERT_EQ(prctlFileParser->getFormula()->toString(), "P = ? [F<=42 !a]"); |
|||
|
|||
delete prctlFileParser->getFormula(); |
|||
delete prctlFileParser; |
|||
|
|||
} |
|||
|
|||
TEST(PrctlParserTest, parseComplexFormulaTest) { |
|||
storm::parser::PrctlFileParser* prctlFileParser = nullptr; |
|||
ASSERT_NO_THROW( |
|||
prctlFileParser = new storm::parser::PrctlFileParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/complexFormula.prctl") |
|||
); |
|||
|
|||
ASSERT_NE(prctlFileParser->getFormula(), nullptr); |
|||
|
|||
|
|||
ASSERT_EQ(prctlFileParser->getFormula()->toString(), "(P <= 0.500000 [F a] & (R > 15.000000 [G P > 0.900000 [F<=7 (a & b)]] | !P < 0.400000 [G !b]))"); |
|||
delete prctlFileParser->getFormula(); |
|||
delete prctlFileParser; |
|||
|
|||
} |
|||
|
|||
TEST(PrctlParserTest, wrongProbabilisticFormulaTest) { |
|||
storm::parser::PrctlParser* prctlParser = nullptr; |
|||
ASSERT_THROW( |
|||
prctlParser = new storm::parser::PrctlParser("P > 0.5 [ a ]"), |
|||
storm::exceptions::WrongFileFormatException |
|||
); |
|||
|
|||
delete prctlParser; |
|||
} |
|||
|
|||
TEST(PrctlParserTest, wrongFormulaTest) { |
|||
storm::parser::PrctlParser* prctlParser = nullptr; |
|||
ASSERT_THROW( |
|||
prctlParser = new storm::parser::PrctlFileParser("& a"), |
|||
storm::exceptions::WrongFileFormatException |
|||
); |
|||
delete prctlParser; |
|||
} |
|||
|
|||
TEST(PrctlParserTest, wrongFormulaTest2) { |
|||
storm::parser::PrctlParser* prctlParser = nullptr; |
|||
ASSERT_THROW( |
|||
prctlParser = new storm::parser::PrctlFileParser("P>0 [ F & a ]"), |
|||
storm::exceptions::WrongFileFormatException |
|||
); |
|||
delete prctlParser; |
|||
} |
|||
@ -0,0 +1 @@ |
|||
P |
|||
@ -0,0 +1 @@ |
|||
P<=0.5 [ F a ] & (R > 15 [ G P>0.9 [F<=7 a & b] ] | !P < 0.4 [ G !b ]) |
|||
@ -0,0 +1 @@ |
|||
P > 0.5 [ F a ] |
|||
@ -0,0 +1 @@ |
|||
P = ? [ F <= 42 !a ] |
|||
@ -0,0 +1 @@ |
|||
!(a & b) | a & ! c |
|||
@ -0,0 +1 @@ |
|||
R >= 15 [ a U !b ] |
|||
@ -0,0 +1 @@ |
|||
R = ? [ a U <= 4 b & (!c) ] |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue