BisimulationTestHelper.h File Reference

#include "storm-config.h"
#include "test/storm_gtest.h"
#include <map>
#include <memory>
#include <optional>
#include <string>
#include <vector>
#include "storm-parsers/api/explicit_models.h"
#include "storm-parsers/api/properties.h"
#include "storm-parsers/parser/FormulaParser.h"
#include "storm-parsers/parser/PrismParser.h"
#include "storm/api/builder.h"
#include "storm/api/properties.h"
#include "storm/api/verification.h"
#include "storm/builder/BuilderOptions.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/models/sparse/Ctmc.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/MarkovAutomaton.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/storage/BitVector.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/storage/sparse/ModelComponents.h"
#include "storm/transformer/bisimulation/Bisimulation.h"
#include "storm/utility/constants.h"

Include dependency graph for BisimulationTestHelper.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	storm::test::bisimulation::PrismInput< ValueType >
	The model built from the given PRISM file together with the formulas that the minimization has to preserve. More...
struct	storm::test::bisimulation::BuildOptions
	What to build from a PRISM program in addition to what the formulas require. More...

Namespaces
namespace	storm
namespace	storm::test
namespace	storm::test::bisimulation
	Shared helpers for the bisimulation tests, cf.

Typedefs
using	storm::test::bisimulation::Options = storm::bisimulation::Options
using	storm::test::bisimulation::StateLabelPreservation = storm::bisimulation::StateLabelPreservation

Functions
Options	storm::test::bisimulation::strongOptions ()
Options	storm::test::bisimulation::weakOptions ()
template<typename ModelType, typename ValueType = typename ModelType::ValueType>
std::shared_ptr< ModelType >	storm::test::bisimulation::buildModel (storm::storage::SparseMatrix< ValueType > matrix, std::map< std::string, std::vector< uint64_t > > const &labels, std::vector< ValueType > const &stateRewards={}, std::vector< ValueType > const &stateActionRewards={})
	Builds a deterministic model with the given (probability or rate) matrix.
template<typename ValueType = double>
std::shared_ptr< storm::models::sparse::MarkovAutomaton< ValueType > >	storm::test::bisimulation::buildMarkovAutomaton (storm::storage::SparseMatrix< ValueType > matrix, storm::storage::BitVector markovianStates, std::map< std::string, std::vector< uint64_t > > const &labels)
	Builds a Markov automaton.
template<typename ValueType>
ValueType	storm::test::bisimulation::checkFormula (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, std::shared_ptr< storm::logic::Formula const > const &formula)
template<typename ValueType>
ValueType	storm::test::bisimulation::checkFormula (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, std::string const &formulaString)
template<typename ValueType>
PrismInput< ValueType >	storm::test::bisimulation::buildFromPrism (std::string const &prismFile, std::string const &formulaString, BuildOptions const &buildOptions={})