1#include "storm-config.h"
12TEST(MaximalEndComponentDecomposition, FullSystem1) {
13 std::shared_ptr<storm::models::sparse::Model<double>> abstractModel =
21 ASSERT_EQ(2ul, mecDecomposition.size());
81TEST(MaximalEndComponentDecomposition, FullSystem2) {
82 std::shared_ptr<storm::models::sparse::Model<double>> abstractModel =
90 ASSERT_EQ(1ul, mecDecomposition.size());
111TEST(MaximalEndComponentDecomposition, Subsystem) {
112 std::shared_ptr<storm::models::sparse::Model<double>> abstractModel =
118 subsystem.set(7,
false);
123 ASSERT_EQ(1ul, mecDecomposition.
size());
144TEST(MaximalEndComponentDecomposition, Example1) {
146 GTEST_SKIP() <<
"Z3 not available.";
148 std::string prismModelPath = STORM_TEST_RESOURCES_DIR
"/mdp/prism-mec-example1.nm";
157 EXPECT_EQ(2ull, mecDecomposition.size());
166TEST(MaximalEndComponentDecomposition, Example2) {
168 GTEST_SKIP() <<
"Z3 not available.";
170 std::string prismModelPath = STORM_TEST_RESOURCES_DIR
"/mdp/prism-mec-example2.nm";
179 EXPECT_EQ(2ull, mecDecomposition.size());
TEST(MaximalEndComponentDecomposition, FullSystem1)
std::shared_ptr< storm::models::sparse::Model< ValueType, RewardModelType > > build()
Convert the program given at construction time to an abstract model.
This class represents a Markov automaton.
This class represents a (discrete-time) Markov decision process.
static std::shared_ptr< storm::models::sparse::Model< ValueType, storm::models::sparse::StandardRewardModel< RewardValueType > > > parseModel(std::string const &transitionsFilename, std::string const &labelingFilename, std::string const &stateRewardFilename="", std::string const &transitionRewardFilename="", std::string const &choiceLabelingFilename="")
Checks the given files and parses the model within these files.
static storm::prism::Program parse(std::string const &filename, bool prismCompatability=false)
Parses the given file into the PRISM storage classes assuming it complies with the PRISM syntax.
A bit vector that is internally represented as a vector of 64-bit values.
std::size_t size() const
Retrieves the number of blocks of this decomposition.
This class represents the decomposition of a nondeterministic model into its maximal end components.
This class represents a maximal end-component of a nondeterministic model.
storm::storage::FlatSet< sparse::state_type > set_type
bool containsState(uint_fast64_t state) const
Retrieves whether the given state is contained in this MEC.
storm::prism::Program const & asPrismProgram() const
SymbolicModelDescription preprocess(std::string const &constantDefinitionString="") const