FormulaInformation.cpp File Reference

#include "storm-pomdp/analysis/FormulaInformation.h"
#include "storm/adapters/RationalNumberAdapter.h"
#include "storm/logic/Formulas.h"
#include "storm/logic/FragmentSpecification.h"
#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/models/sparse/Pomdp.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/exceptions/InvalidPropertyException.h"
#include "storm/utility/macros.h"

Include dependency graph for FormulaInformation.cpp:

Go to the source code of this file.

Namespaces
namespace	storm
	LabParser.cpp.
namespace	storm::pomdp
namespace	storm::pomdp::analysis

Functions
template<typename PomdpType >
FormulaInformation::StateSet	storm::pomdp::analysis::getStateSet (PomdpType const &pomdp, storm::storage::BitVector &&inputStates)
template<typename PomdpType >
storm::storage::BitVector	storm::pomdp::analysis::getStates (storm::logic::Formula const &propositionalFormula, bool formulaInverted, PomdpType const &pomdp)
template<typename PomdpType >
FormulaInformation	storm::pomdp::analysis::getFormulaInformation (PomdpType const &pomdp, storm::logic::ProbabilityOperatorFormula const &formula)
template<typename PomdpType >
FormulaInformation	storm::pomdp::analysis::getFormulaInformation (PomdpType const &pomdp, storm::logic::RewardOperatorFormula const &formula)
template<typename PomdpType >
FormulaInformation	storm::pomdp::analysis::getFormulaInformation (PomdpType const &pomdp, storm::logic::Formula const &formula)
template void	storm::pomdp::analysis::FormulaInformation::updateTargetStates< storm::models::sparse::Pomdp< double > > (storm::models::sparse::Pomdp< double > const &pomdp, storm::storage::BitVector &&newTargetStates)
template void	storm::pomdp::analysis::FormulaInformation::updateSinkStates< storm::models::sparse::Pomdp< double > > (storm::models::sparse::Pomdp< double > const &pomdp, storm::storage::BitVector &&newSinkStates)
template FormulaInformation	storm::pomdp::analysis::getFormulaInformation< storm::models::sparse::Pomdp< double > > (storm::models::sparse::Pomdp< double > const &pomdp, storm::logic::Formula const &formula)
template void	storm::pomdp::analysis::FormulaInformation::updateTargetStates< storm::models::sparse::Pomdp< storm::RationalNumber > > (storm::models::sparse::Pomdp< storm::RationalNumber > const &pomdp, storm::storage::BitVector &&newTargetStates)
template void	storm::pomdp::analysis::FormulaInformation::updateSinkStates< storm::models::sparse::Pomdp< storm::RationalNumber > > (storm::models::sparse::Pomdp< storm::RationalNumber > const &pomdp, storm::storage::BitVector &&newSinkStates)
template FormulaInformation	storm::pomdp::analysis::getFormulaInformation< storm::models::sparse::Pomdp< storm::RationalNumber > > (storm::models::sparse::Pomdp< storm::RationalNumber > const &pomdp, storm::logic::Formula const &formula)