Lanchid
12 years ago
87 changed files with 795 additions and 169 deletions
-
10src/formula/Csl.h
-
2src/formula/Csl/AbstractNoBoundOperator.h
-
4src/formula/Csl/AbstractPathFormula.h
-
4src/formula/Csl/AbstractStateFormula.h
-
4src/formula/Csl/And.h
-
4src/formula/Csl/Ap.h
-
4src/formula/Csl/Eventually.h
-
4src/formula/Csl/Globally.h
-
2src/formula/Csl/Next.h
-
4src/formula/Csl/Not.h
-
2src/formula/Csl/Or.h
-
2src/formula/Csl/ProbabilisticBoundOperator.h
-
4src/formula/Csl/ProbabilisticNoBoundOperator.h
-
2src/formula/Csl/SteadyStateBoundOperator.h
-
2src/formula/Csl/SteadyStateNoBoundOperator.h
-
2src/formula/Csl/TimeBoundedEventually.h
-
2src/formula/Csl/TimeBoundedUntil.h
-
2src/formula/Csl/Until.h
-
4src/formula/Ltl.h
-
4src/formula/Ltl/AbstractLtlFormula.h
-
4src/formula/Ltl/And.h
-
2src/formula/Ltl/Ap.h
-
4src/formula/Ltl/BoundedEventually.h
-
4src/formula/Ltl/BoundedUntil.h
-
4src/formula/Ltl/Eventually.h
-
4src/formula/Ltl/Globally.h
-
2src/formula/Ltl/Next.h
-
2src/formula/Ltl/Not.h
-
2src/formula/Ltl/Or.h
-
2src/formula/Ltl/Until.h
-
17src/formula/Prctl.h
-
2src/formula/Prctl/AbstractNoBoundOperator.h
-
4src/formula/Prctl/AbstractPathFormula.h
-
4src/formula/Prctl/AbstractStateFormula.h
-
4src/formula/Prctl/And.h
-
4src/formula/Prctl/Ap.h
-
4src/formula/Prctl/BoundedEventually.h
-
4src/formula/Prctl/BoundedNaryUntil.h
-
4src/formula/Prctl/BoundedUntil.h
-
2src/formula/Prctl/CumulativeReward.h
-
4src/formula/Prctl/Eventually.h
-
4src/formula/Prctl/Globally.h
-
2src/formula/Prctl/InstantaneousReward.h
-
2src/formula/Prctl/Next.h
-
4src/formula/Prctl/Not.h
-
2src/formula/Prctl/Or.h
-
2src/formula/Prctl/ProbabilisticBoundOperator.h
-
2src/formula/Prctl/ProbabilisticNoBoundOperator.h
-
2src/formula/Prctl/ReachabilityReward.h
-
2src/formula/Prctl/RewardBoundOperator.h
-
2src/formula/Prctl/RewardNoBoundOperator.h
-
2src/formula/Prctl/SteadyStateReward.h
-
2src/formula/Prctl/Until.h
-
2src/formula/abstract/AbstractFormula.h
-
1src/formula/abstract/And.h
-
1src/formula/abstract/Ap.h
-
1src/formula/abstract/BoundedEventually.h
-
1src/formula/abstract/BoundedNaryUntil.h
-
1src/formula/abstract/BoundedUntil.h
-
1src/formula/abstract/Eventually.h
-
1src/formula/abstract/Globally.h
-
1src/formula/abstract/Not.h
-
1src/formula/abstract/PathBoundOperator.h
-
1src/formula/abstract/PathNoBoundOperator.h
-
1src/formula/abstract/StateBoundOperator.h
-
1src/formula/abstract/StateNoBoundOperator.h
-
287src/modelchecker/csl/AbstractModelChecker.h
-
2src/modelchecker/csl/ForwardDeclarations.h
-
193src/modelchecker/ltl/AbstractModelChecker.h
-
24src/modelchecker/ltl/ForwardDeclarations.h
-
15src/modelchecker/prctl/AbstractModelChecker.h
-
10src/modelchecker/prctl/EigenDtmcPrctlModelChecker.h
-
24src/modelchecker/prctl/ForwardDeclarations.h
-
12src/modelchecker/prctl/GmmxxDtmcPrctlModelChecker.h
-
12src/modelchecker/prctl/GmmxxMdpPrctlModelChecker.h
-
12src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
-
12src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
-
10src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h
-
49src/parser/LtlFileParser.cpp
-
42src/parser/LtlFileParser.h
-
3src/parser/PrctlFileParser.cpp
-
2src/parser/PrctlFileParser.h
-
2src/parser/PrctlParser.cpp
-
38src/storm.cpp
-
8test/functional/GmmxxDtmcPrctModelCheckerTest.cpp
-
10test/functional/GmmxxMdpPrctModelCheckerTest.cpp
-
4test/storm-tests.cpp
@ -0,0 +1,287 @@ |
|||||
|
/* |
||||
|
* AbstractModelChecker.h |
||||
|
* |
||||
|
* Created on: 22.10.2012 |
||||
|
* Author: Thomas Heinemann |
||||
|
*/ |
||||
|
|
||||
|
#ifndef STORM_MODELCHECKER_CSL_ABSTRACTMODELCHECKER_H_ |
||||
|
#define STORM_MODELCHECKER_CSL_ABSTRACTMODELCHECKER_H_ |
||||
|
|
||||
|
#include "src/exceptions/InvalidPropertyException.h" |
||||
|
#include "src/formula/Csl.h" |
||||
|
#include "src/storage/BitVector.h" |
||||
|
#include "src/models/AbstractModel.h" |
||||
|
|
||||
|
#include "log4cplus/logger.h" |
||||
|
#include "log4cplus/loggingmacros.h" |
||||
|
|
||||
|
#include <iostream> |
||||
|
|
||||
|
extern log4cplus::Logger logger; |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace modelchecker { |
||||
|
namespace csl { |
||||
|
|
||||
|
/*! |
||||
|
* @brief |
||||
|
* (Abstract) interface for all model checker classes. |
||||
|
* |
||||
|
* This class provides basic functions that are common to all model checkers (i.e. subclasses). It mainly declares |
||||
|
* abstract methods that are implemented in the concrete subclasses, but also covers checking procedures that are common |
||||
|
* to all model checkers for state-based models. |
||||
|
*/ |
||||
|
template<class Type> |
||||
|
class AbstractModelChecker : |
||||
|
// A list of interfaces the model checker supports. Typically, for each of the interfaces, a check method needs to |
||||
|
// be implemented that performs the corresponding check. |
||||
|
public virtual storm::property::csl::IApModelChecker<Type>, |
||||
|
public virtual storm::property::csl::IAndModelChecker<Type>, |
||||
|
public virtual storm::property::csl::IOrModelChecker<Type>, |
||||
|
public virtual storm::property::csl::INotModelChecker<Type>, |
||||
|
public virtual storm::property::csl::IUntilModelChecker<Type>, |
||||
|
public virtual storm::property::csl::IEventuallyModelChecker<Type>, |
||||
|
public virtual storm::property::csl::IGloballyModelChecker<Type>, |
||||
|
public virtual storm::property::csl::INextModelChecker<Type>, |
||||
|
public virtual storm::property::csl::ITimeBoundedUntilModelChecker<Type>, |
||||
|
public virtual storm::property::csl::ITimeBoundedEventuallyModelChecker<Type>, |
||||
|
public virtual storm::property::csl::INoBoundOperatorModelChecker<Type>, |
||||
|
public virtual storm::property::csl::IProbabilisticBoundOperatorModelChecker<Type> { |
||||
|
|
||||
|
public: |
||||
|
/*! |
||||
|
* Constructs an AbstractModelChecker with the given model. |
||||
|
*/ |
||||
|
explicit AbstractModelChecker(storm::models::AbstractModel<Type> const& model) : model(model) { |
||||
|
// Intentionally left empty. |
||||
|
} |
||||
|
/*! |
||||
|
* Copy constructs an AbstractModelChecker from the given model checker. In particular, this means that the newly |
||||
|
* constructed model checker will have the model of the given model checker as its associated model. |
||||
|
*/ |
||||
|
explicit AbstractModelChecker(AbstractModelChecker<Type> const& modelchecker) : model(modelchecker.model) { |
||||
|
// Intentionally left empty. |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Virtual destructor. Needs to be virtual, because this class has virtual methods. |
||||
|
*/ |
||||
|
virtual ~AbstractModelChecker() { |
||||
|
// Intentionally left empty. |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Returns a pointer to the model checker object that is of the requested type as given by the template parameters. |
||||
|
* @returns A pointer to the model checker object that is of the requested type as given by the template parameters. |
||||
|
* If the model checker is not of the requested type, type casting will fail and result in an exception. |
||||
|
*/ |
||||
|
template <template <class T> class Target> |
||||
|
const Target<Type>* as() const { |
||||
|
try { |
||||
|
const Target<Type>* target = dynamic_cast<const Target<Type>*>(this); |
||||
|
return target; |
||||
|
} catch (std::bad_cast& bc) { |
||||
|
LOG4CPLUS_ERROR(logger, "Bad cast: tried to cast " << typeid(*this).name() << " to " << typeid(Target<Type>).name() << "."); |
||||
|
throw bc; |
||||
|
} |
||||
|
return nullptr; |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves the model associated with this model checker as a constant reference to an object of the type given |
||||
|
* by the template parameter. |
||||
|
* |
||||
|
* @returns A constant reference of the specified type to the model associated with this model checker. If the model |
||||
|
* is not of the requested type, type casting will fail and result in an exception. |
||||
|
*/ |
||||
|
template <class Model> |
||||
|
Model const& getModel() const { |
||||
|
try { |
||||
|
Model const& target = dynamic_cast<Model const&>(this->model); |
||||
|
return target; |
||||
|
} catch (std::bad_cast& bc) { |
||||
|
LOG4CPLUS_ERROR(logger, "Bad cast: tried to cast " << typeid(this->model).name() << " to " << typeid(Model).name() << "."); |
||||
|
throw bc; |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Checks the given abstract prctl formula on the model and prints the result (depending on the actual type of the formula) |
||||
|
* for all initial states, i.e. states that carry the atomic proposition "init". |
||||
|
* |
||||
|
* @param formula The formula to be checked. |
||||
|
*/ |
||||
|
void check(storm::property::csl::AbstractCslFormula<Type> const& formula) const { |
||||
|
if (dynamic_cast<storm::property::csl::AbstractStateFormula<Type> const*>(&formula) != nullptr) { |
||||
|
this->check(static_cast<storm::property::csl::AbstractStateFormula<Type> const&>(formula)); |
||||
|
} else if (dynamic_cast<storm::property::csl::AbstractNoBoundOperator<Type> const*>(&formula) != nullptr) { |
||||
|
this->check(static_cast<storm::property::csl::AbstractNoBoundOperator<Type> const&>(formula)); |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Checks the given state formula on the model and prints the result (true/false) for all initial states, i.e. |
||||
|
* states that carry the atomic proposition "init". |
||||
|
* |
||||
|
* @param stateFormula The formula to be checked. |
||||
|
*/ |
||||
|
void check(storm::property::csl::AbstractStateFormula<Type> const& stateFormula) const { |
||||
|
std::cout << std::endl; |
||||
|
LOG4CPLUS_INFO(logger, "Model checking formula\t" << stateFormula.toString()); |
||||
|
std::cout << "Model checking formula:\t" << stateFormula.toString() << std::endl; |
||||
|
storm::storage::BitVector* result = nullptr; |
||||
|
try { |
||||
|
result = stateFormula.check(*this); |
||||
|
LOG4CPLUS_INFO(logger, "Result for initial states:"); |
||||
|
std::cout << "Result for initial states:" << std::endl; |
||||
|
for (auto initialState : model.getLabeledStates("init")) { |
||||
|
LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result->get(initialState) ? "satisfied" : "not satisfied")); |
||||
|
std::cout << "\t" << initialState << ": " << result->get(initialState) << std::endl; |
||||
|
} |
||||
|
delete result; |
||||
|
} catch (std::exception& e) { |
||||
|
std::cout << "Error during computation: " << e.what() << "Skipping property." << std::endl; |
||||
|
LOG4CPLUS_ERROR(logger, "Error during computation: " << e.what() << "Skipping property."); |
||||
|
if (result != nullptr) { |
||||
|
delete result; |
||||
|
} |
||||
|
} |
||||
|
std::cout << std::endl; |
||||
|
storm::utility::printSeparationLine(std::cout); |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Checks the given formula (with no bound) on the model and prints the result (probability/rewards) for all |
||||
|
* initial states, i.e. states that carry the atomic proposition "init". |
||||
|
* |
||||
|
* @param noBoundFormula The formula to be checked. |
||||
|
*/ |
||||
|
void check(storm::property::csl::AbstractNoBoundOperator<Type> const& noBoundFormula) const { |
||||
|
std::cout << std::endl; |
||||
|
LOG4CPLUS_INFO(logger, "Model checking formula\t" << noBoundFormula.toString()); |
||||
|
std::cout << "Model checking formula:\t" << noBoundFormula.toString() << std::endl; |
||||
|
std::vector<Type>* result = nullptr; |
||||
|
try { |
||||
|
result = this->checkNoBoundOperator(noBoundFormula); |
||||
|
LOG4CPLUS_INFO(logger, "Result for initial states:"); |
||||
|
std::cout << "Result for initial states:" << std::endl; |
||||
|
for (auto initialState : model.getLabeledStates("init")) { |
||||
|
LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (*result)[initialState]); |
||||
|
std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl; |
||||
|
} |
||||
|
delete result; |
||||
|
} catch (std::exception& e) { |
||||
|
std::cout << "Error during computation: " << e.what() << " Skipping property." << std::endl; |
||||
|
if (result != nullptr) { |
||||
|
delete result; |
||||
|
} |
||||
|
} |
||||
|
std::cout << std::endl; |
||||
|
storm::utility::printSeparationLine(std::cout); |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Checks the given formula consisting of a single atomic proposition. |
||||
|
* |
||||
|
* @param formula The formula to be checked. |
||||
|
* @returns The set of states satisfying the formula represented by a bit vector. |
||||
|
*/ |
||||
|
storm::storage::BitVector* checkAp(storm::property::csl::Ap<Type> const& formula) const { |
||||
|
if (formula.getAp() == "true") { |
||||
|
return new storm::storage::BitVector(model.getNumberOfStates(), true); |
||||
|
} else if (formula.getAp() == "false") { |
||||
|
return new storm::storage::BitVector(model.getNumberOfStates()); |
||||
|
} |
||||
|
|
||||
|
if (!model.hasAtomicProposition(formula.getAp())) { |
||||
|
LOG4CPLUS_ERROR(logger, "Atomic proposition '" << formula.getAp() << "' is invalid."); |
||||
|
throw storm::exceptions::InvalidPropertyException() << "Atomic proposition '" << formula.getAp() << "' is invalid."; |
||||
|
} |
||||
|
|
||||
|
return new storm::storage::BitVector(model.getLabeledStates(formula.getAp())); |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Checks the given formula that is a logical "and" of two formulae. |
||||
|
* |
||||
|
* @param formula The formula to be checked. |
||||
|
* @returns The set of states satisfying the formula represented by a bit vector. |
||||
|
*/ |
||||
|
storm::storage::BitVector* checkAnd(storm::property::csl::And<Type> const& formula) const { |
||||
|
storm::storage::BitVector* result = formula.getLeft().check(*this); |
||||
|
storm::storage::BitVector* right = formula.getRight().check(*this); |
||||
|
(*result) &= (*right); |
||||
|
delete right; |
||||
|
return result; |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Checks the given formula that is a logical "or" of two formulae. |
||||
|
* |
||||
|
* @param formula The formula to check. |
||||
|
* @returns The set of states satisfying the formula represented by a bit vector. |
||||
|
*/ |
||||
|
virtual storm::storage::BitVector* checkOr(storm::property::csl::Or<Type> const& formula) const { |
||||
|
storm::storage::BitVector* result = formula.getLeft().check(*this); |
||||
|
storm::storage::BitVector* right = formula.getRight().check(*this); |
||||
|
(*result) |= (*right); |
||||
|
delete right; |
||||
|
return result; |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Checks the given formula that is a logical "not" of a sub-formula. |
||||
|
* |
||||
|
* @param formula The formula to check. |
||||
|
* @returns The set of states satisfying the formula represented by a bit vector. |
||||
|
*/ |
||||
|
storm::storage::BitVector* checkNot(const storm::property::csl::Not<Type>& formula) const { |
||||
|
storm::storage::BitVector* result = formula.getChild().check(*this); |
||||
|
result->complement(); |
||||
|
return result; |
||||
|
} |
||||
|
|
||||
|
|
||||
|
/*! |
||||
|
* Checks the given formula that is a P operator over a path formula featuring a value bound. |
||||
|
* |
||||
|
* @param formula The formula to check. |
||||
|
* @returns The set of states satisfying the formula represented by a bit vector. |
||||
|
*/ |
||||
|
storm::storage::BitVector* checkProbabilisticBoundOperator(storm::property::csl::ProbabilisticBoundOperator<Type> const& formula) const { |
||||
|
// First, we need to compute the probability for satisfying the path formula for each state. |
||||
|
std::vector<Type>* quantitativeResult = formula.getPathFormula().check(*this, false); |
||||
|
|
||||
|
// Create resulting bit vector that will hold the yes/no-answer for every state. |
||||
|
storm::storage::BitVector* result = new storm::storage::BitVector(quantitativeResult->size()); |
||||
|
|
||||
|
// Now, we can compute which states meet the bound specified in this operator and set the |
||||
|
// corresponding bits to true in the resulting vector. |
||||
|
for (uint_fast64_t i = 0; i < quantitativeResult->size(); ++i) { |
||||
|
if (formula.meetsBound((*quantitativeResult)[i])) { |
||||
|
result->set(i, true); |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
// Delete the probabilities computed for the states and return result. |
||||
|
delete quantitativeResult; |
||||
|
return result; |
||||
|
} |
||||
|
|
||||
|
private: |
||||
|
|
||||
|
/*! |
||||
|
* A constant reference to the model associated with this model checker. |
||||
|
* |
||||
|
* @note that we do not own this object, but merely have a constant reference to it. That means that using the |
||||
|
* model checker object is unsafe after the object has been destroyed. |
||||
|
*/ |
||||
|
storm::models::AbstractModel<Type> const& model; |
||||
|
}; |
||||
|
|
||||
|
} // namespace csl |
||||
|
} // namespace modelchecker |
||||
|
} // namespace storm |
||||
|
|
||||
|
#endif /* STORM_MODELCHECKER_CSL_DTMCPRCTLMODELCHECKER_H_ */ |
||||
@ -0,0 +1,193 @@ |
|||||
|
/* |
||||
|
* AbstractModelChecker.h |
||||
|
* |
||||
|
* Created on: 22.10.2012 |
||||
|
* Author: Thomas Heinemann |
||||
|
*/ |
||||
|
|
||||
|
#ifndef STORM_MODELCHECKER_LTL_ABSTRACTMODELCHECKER_H_ |
||||
|
#define STORM_MODELCHECKER_LTL_ABSTRACTMODELCHECKER_H_ |
||||
|
|
||||
|
#include "src/exceptions/InvalidPropertyException.h" |
||||
|
#include "src/formula/Ltl.h" |
||||
|
#include "src/storage/BitVector.h" |
||||
|
#include "src/models/AbstractModel.h" |
||||
|
|
||||
|
#include "log4cplus/logger.h" |
||||
|
#include "log4cplus/loggingmacros.h" |
||||
|
|
||||
|
#include <iostream> |
||||
|
|
||||
|
extern log4cplus::Logger logger; |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace modelchecker { |
||||
|
namespace ltl { |
||||
|
|
||||
|
/*! |
||||
|
* @brief |
||||
|
* (Abstract) interface for all model checker classes. |
||||
|
* |
||||
|
* This class provides basic functions that are common to all model checkers (i.e. subclasses). It mainly declares |
||||
|
* abstract methods that are implemented in the concrete subclasses, but also covers checking procedures that are common |
||||
|
* to all model checkers for state-based models. |
||||
|
*/ |
||||
|
template<class Type> |
||||
|
class AbstractModelChecker : |
||||
|
// A list of interfaces the model checker supports. Typically, for each of the interfaces, a check method needs to |
||||
|
// be implemented that performs the corresponding check. |
||||
|
public virtual storm::property::ltl::IApModelChecker<Type>, |
||||
|
public virtual storm::property::ltl::IAndModelChecker<Type>, |
||||
|
public virtual storm::property::ltl::IOrModelChecker<Type>, |
||||
|
public virtual storm::property::ltl::INotModelChecker<Type>, |
||||
|
public virtual storm::property::ltl::IUntilModelChecker<Type>, |
||||
|
public virtual storm::property::ltl::IEventuallyModelChecker<Type>, |
||||
|
public virtual storm::property::ltl::IGloballyModelChecker<Type>, |
||||
|
public virtual storm::property::ltl::INextModelChecker<Type>, |
||||
|
public virtual storm::property::ltl::IBoundedUntilModelChecker<Type>, |
||||
|
public virtual storm::property::ltl::IBoundedEventuallyModelChecker<Type> { |
||||
|
|
||||
|
public: |
||||
|
/*! |
||||
|
* Constructs an AbstractModelChecker with the given model. |
||||
|
*/ |
||||
|
explicit AbstractModelChecker(storm::models::AbstractModel<Type> const& model) : model(model) { |
||||
|
// Intentionally left empty. |
||||
|
} |
||||
|
/*! |
||||
|
* Copy constructs an AbstractModelChecker from the given model checker. In particular, this means that the newly |
||||
|
* constructed model checker will have the model of the given model checker as its associated model. |
||||
|
*/ |
||||
|
explicit AbstractModelChecker(AbstractModelChecker<Type> const& modelchecker) : model(modelchecker.model) { |
||||
|
// Intentionally left empty. |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Virtual destructor. Needs to be virtual, because this class has virtual methods. |
||||
|
*/ |
||||
|
virtual ~AbstractModelChecker() { |
||||
|
// Intentionally left empty. |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Returns a pointer to the model checker object that is of the requested type as given by the template parameters. |
||||
|
* @returns A pointer to the model checker object that is of the requested type as given by the template parameters. |
||||
|
* If the model checker is not of the requested type, type casting will fail and result in an exception. |
||||
|
*/ |
||||
|
template <template <class T> class Target> |
||||
|
const Target<Type>* as() const { |
||||
|
try { |
||||
|
const Target<Type>* target = dynamic_cast<const Target<Type>*>(this); |
||||
|
return target; |
||||
|
} catch (std::bad_cast& bc) { |
||||
|
LOG4CPLUS_ERROR(logger, "Bad cast: tried to cast " << typeid(*this).name() << " to " << typeid(Target<Type>).name() << "."); |
||||
|
throw bc; |
||||
|
} |
||||
|
return nullptr; |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves the model associated with this model checker as a constant reference to an object of the type given |
||||
|
* by the template parameter. |
||||
|
* |
||||
|
* @returns A constant reference of the specified type to the model associated with this model checker. If the model |
||||
|
* is not of the requested type, type casting will fail and result in an exception. |
||||
|
*/ |
||||
|
template <class Model> |
||||
|
Model const& getModel() const { |
||||
|
try { |
||||
|
Model const& target = dynamic_cast<Model const&>(this->model); |
||||
|
return target; |
||||
|
} catch (std::bad_cast& bc) { |
||||
|
LOG4CPLUS_ERROR(logger, "Bad cast: tried to cast " << typeid(this->model).name() << " to " << typeid(Model).name() << "."); |
||||
|
throw bc; |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Checks the given state formula on the model and prints the result (true/false) for all initial states, i.e. |
||||
|
* states that carry the atomic proposition "init". |
||||
|
* |
||||
|
* @param stateFormula The formula to be checked. |
||||
|
*/ |
||||
|
void check(storm::property::ltl::AbstractLtlFormula<Type> const& ltlFormula) const { |
||||
|
std::cout << std::endl; |
||||
|
LOG4CPLUS_INFO(logger, "Model checking formula\t" << ltlFormula.toString()); |
||||
|
std::cout << "Model checking formula:\t" << ltlFormula.toString() << std::endl; |
||||
|
storm::storage::BitVector* result = nullptr; |
||||
|
try { |
||||
|
result = ltlFormula.check(*this); |
||||
|
LOG4CPLUS_INFO(logger, "Result for initial states:"); |
||||
|
std::cout << "Result for initial states:" << std::endl; |
||||
|
for (auto initialState : model.getLabeledStates("init")) { |
||||
|
LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result->get(initialState) ? "satisfied" : "not satisfied")); |
||||
|
std::cout << "\t" << initialState << ": " << result->get(initialState) << std::endl; |
||||
|
} |
||||
|
delete result; |
||||
|
} catch (std::exception& e) { |
||||
|
std::cout << "Error during computation: " << e.what() << "Skipping property." << std::endl; |
||||
|
LOG4CPLUS_ERROR(logger, "Error during computation: " << e.what() << "Skipping property."); |
||||
|
if (result != nullptr) { |
||||
|
delete result; |
||||
|
} |
||||
|
} |
||||
|
std::cout << std::endl; |
||||
|
storm::utility::printSeparationLine(std::cout); |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Checks the given formula consisting of a single atomic proposition. |
||||
|
* |
||||
|
* @param formula The formula to be checked. |
||||
|
* @returns The set of states satisfying the formula represented by a bit vector. |
||||
|
*/ |
||||
|
virtual std::vector<Type>* checkAp(storm::property::ltl::Ap<Type> const& formula) const { |
||||
|
return nullptr; |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Checks the given formula that is a logical "and" of two formulae. |
||||
|
* |
||||
|
* @param formula The formula to be checked. |
||||
|
* @returns The set of states satisfying the formula represented by a bit vector. |
||||
|
*/ |
||||
|
virtual std::vector<Type>* checkAnd(storm::property::ltl::And<Type> const& formula) const { |
||||
|
return nullptr; |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Checks the given formula that is a logical "or" of two formulae. |
||||
|
* |
||||
|
* @param formula The formula to check. |
||||
|
* @returns The set of states satisfying the formula represented by a bit vector. |
||||
|
*/ |
||||
|
virtual std::vector<Type>* checkOr(storm::property::ltl::Or<Type> const& formula) const { |
||||
|
return nullptr; |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Checks the given formula that is a logical "not" of a sub-formula. |
||||
|
* |
||||
|
* @param formula The formula to check. |
||||
|
* @returns The set of states satisfying the formula represented by a bit vector. |
||||
|
*/ |
||||
|
virtual std::vector<Type>* checkNot(const storm::property::ltl::Not<Type>& formula) const { |
||||
|
return nullptr; |
||||
|
} |
||||
|
|
||||
|
private: |
||||
|
|
||||
|
/*! |
||||
|
* A constant reference to the model associated with this model checker. |
||||
|
* |
||||
|
* @note that we do not own this object, but merely have a constant reference to it. That means that using the |
||||
|
* model checker object is unsafe after the object has been destroyed. |
||||
|
*/ |
||||
|
storm::models::AbstractModel<Type> const& model; |
||||
|
}; |
||||
|
|
||||
|
} // namespace ltl |
||||
|
} // namespace modelchecker |
||||
|
} // namespace storm |
||||
|
|
||||
|
#endif /* STORM_MODELCHECKER_LTL_ABSTRACTMODELCHECKER_H_ */ |
||||
@ -0,0 +1,24 @@ |
|||||
|
/* |
||||
|
* ForwardDeclarations.h |
||||
|
* |
||||
|
* Created on: 14.01.2013 |
||||
|
* Author: Thomas Heinemann |
||||
|
*/ |
||||
|
|
||||
|
#ifndef STORM_MODELCHECKER_LTL_FORWARDDECLARATIONS_H_ |
||||
|
#define STORM_MODELCHECKER_LTL_FORWARDDECLARATIONS_H_ |
||||
|
|
||||
|
// Forward declare the abstract model checker. This is used by the formula classes that need this declaration for |
||||
|
// the callback methods (i.e., the check methods). |
||||
|
namespace storm { |
||||
|
namespace modelchecker { |
||||
|
namespace ltl { |
||||
|
|
||||
|
template <class Type> |
||||
|
class AbstractModelChecker; |
||||
|
|
||||
|
} //namespace ltl |
||||
|
} //namespace modelchecker |
||||
|
} //namespace storm |
||||
|
|
||||
|
#endif /* STORM_MODELCHECKER_LTL_FORWARDDECLARATIONS_H_ */ |
||||
@ -0,0 +1,24 @@ |
|||||
|
/* |
||||
|
* ForwardDeclarations.h |
||||
|
* |
||||
|
* Created on: 14.01.2013 |
||||
|
* Author: Thomas Heinemann |
||||
|
*/ |
||||
|
|
||||
|
#ifndef STORM_MODELCHECKER_PRCTL_FORWARDDECLARATIONS_H_ |
||||
|
#define STORM_MODELCHECKER_PRCTL_FORWARDDECLARATIONS_H_ |
||||
|
|
||||
|
// Forward declare the abstract model checker. This is used by the formula classes that need this declaration for |
||||
|
// the callback methods (i.e., the check methods). |
||||
|
namespace storm { |
||||
|
namespace modelchecker { |
||||
|
namespace prctl { |
||||
|
|
||||
|
template <class Type> |
||||
|
class AbstractModelChecker; |
||||
|
|
||||
|
} //namespace prctl |
||||
|
} //namespace modelchecker |
||||
|
} //namespace storm |
||||
|
|
||||
|
#endif /* STORM_MODELCHECKER_PRCTL_FORWARDDECLARATIONS_H_ */ |
||||
@ -0,0 +1,49 @@ |
|||||
|
/*
|
||||
|
* LtlFileParser.cpp |
||||
|
* |
||||
|
* Created on: 13.05.2013 |
||||
|
* Author: thomas |
||||
|
*/ |
||||
|
|
||||
|
#include "LtlFileParser.h"
|
||||
|
#include "LtlParser.h"
|
||||
|
|
||||
|
namespace storm { |
||||
|
namespace parser { |
||||
|
|
||||
|
LtlFileParser::LtlFileParser() { |
||||
|
// TODO Auto-generated constructor stub
|
||||
|
|
||||
|
} |
||||
|
|
||||
|
LtlFileParser::~LtlFileParser() { |
||||
|
// TODO Auto-generated destructor stub
|
||||
|
} |
||||
|
|
||||
|
std::list<storm::property::ltl::AbstractLtlFormula<double>*> LtlFileParser::parseFormulas(std::string filename) { |
||||
|
// Open file
|
||||
|
std::ifstream inputFileStream(filename, std::ios::in); |
||||
|
|
||||
|
if (!inputFileStream.is_open()) { |
||||
|
std::string message = "Error while opening file "; |
||||
|
throw storm::exceptions::FileIoException() << message << filename; |
||||
|
} |
||||
|
|
||||
|
std::list<storm::property::ltl::AbstractLtlFormula<double>*> result; |
||||
|
|
||||
|
while(!inputFileStream.eof()) { |
||||
|
std::string line; |
||||
|
//The while loop reads the input file line by line
|
||||
|
while (std::getline(inputFileStream, line)) { |
||||
|
LtlParser parser(line); |
||||
|
result.push_back(parser.getFormula()); |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
return result; |
||||
|
} |
||||
|
|
||||
|
} //namespace parser
|
||||
|
} //namespace storm
|
||||
|
|
||||
|
|
||||
@ -0,0 +1,42 @@ |
|||||
|
/* |
||||
|
* LtlFileParser.h |
||||
|
* |
||||
|
* Created on: 13.05.2013 |
||||
|
* Author: Thonas Heinemann |
||||
|
*/ |
||||
|
|
||||
|
#ifndef LTLFILEPARSER_H_ |
||||
|
#define LTLFILEPARSER_H_ |
||||
|
|
||||
|
#include "formula/Ltl.h" |
||||
|
|
||||
|
#include <list> |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace parser { |
||||
|
|
||||
|
class LtlFileParser { |
||||
|
public: |
||||
|
/*! |
||||
|
* Constructor |
||||
|
*/ |
||||
|
LtlFileParser(); |
||||
|
|
||||
|
/*! |
||||
|
* Destructor |
||||
|
*/ |
||||
|
~LtlFileParser(); |
||||
|
|
||||
|
/*! |
||||
|
* Parses each line of a given file as prctl formula and returns a list containing the results of the parsing. |
||||
|
* |
||||
|
* @param filename |
||||
|
* @return The list of parsed formulas |
||||
|
*/ |
||||
|
std::list<storm::property::ltl::AbstractLtlFormula<double>*> parseFormulas(std::string filename); |
||||
|
}; |
||||
|
|
||||
|
} //namespace parser |
||||
|
} //namespace storm |
||||
|
|
||||
|
#endif /* LTLFILEPARSER_H_ */ |
||||
Reference in new issue
xxxxxxxxxx