From 61c1ec8537ba8767501868e5da3014ba54a79824 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 12 Nov 2019 14:12:29 +0100 Subject: [PATCH] Check for Zeno cycles in MA --- resources/examples/testfiles/ma/zeno.ma | 14 ++++++++ src/storm-cli-utilities/model-handling.h | 2 ++ src/storm/models/sparse/MarkovAutomaton.cpp | 28 ++++++++++++++- src/storm/models/sparse/MarkovAutomaton.h | 22 ++++++++++-- src/test/storm/CMakeLists.txt | 2 +- src/test/storm/model/MarkovAutomatonTest.cpp | 38 ++++++++++++++++++++ 6 files changed, 101 insertions(+), 5 deletions(-) create mode 100644 resources/examples/testfiles/ma/zeno.ma create mode 100644 src/test/storm/model/MarkovAutomatonTest.cpp diff --git a/resources/examples/testfiles/ma/zeno.ma b/resources/examples/testfiles/ma/zeno.ma new file mode 100644 index 000000000..c6f442bb4 --- /dev/null +++ b/resources/examples/testfiles/ma/zeno.ma @@ -0,0 +1,14 @@ + +ma + +module simple + + s : [0..4]; + + [alpha] (s=0) -> 1 : (s' = 1); + [beta] (s=0) -> 0.8 : (s'=0) + 0.2 : (s'=2); + <> (s=1) -> 9 : (s'=0) + 1 : (s'=3); + <> (s=2) -> 12 : (s'=4); + [gamma] (s>2) -> 1 : true; + +endmodule \ No newline at end of file diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 6ea904594..060f87dcd 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -332,6 +332,8 @@ namespace storm { std::shared_ptr> result = model; model->close(); + STORM_LOG_WARN_COND(!model->containsZenoCycle(), "MA contains a Zeno cycle. Model checking results cannot be trusted."); + if (model->isConvertibleToCtmc()) { STORM_LOG_WARN_COND(false, "MA is convertible to a CTMC, consider using a CTMC instead."); result = model->convertToCtmc(); diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp index 85f6b5d21..5a6f00466 100644 --- a/src/storm/models/sparse/MarkovAutomaton.cpp +++ b/src/storm/models/sparse/MarkovAutomaton.cpp @@ -6,6 +6,7 @@ #include "storm/models/sparse/StandardRewardModel.h" #include "storm/solver/stateelimination/StateEliminator.h" #include "storm/storage/FlexibleSparseMatrix.h" +#include "storm/storage/MaximalEndComponentDecomposition.h" #include "storm/utility/constants.h" #include "storm/utility/ConstantsComparator.h" #include "storm/utility/vector.h" @@ -68,6 +69,15 @@ namespace storm { return closed; } + template + bool MarkovAutomaton::containsZenoCycle() const { + if (!this->hasZenoCycle.is_initialized()) { + this->hasZenoCycle = this->checkContainsZenoCycle(); + } + return this->hasZenoCycle.get(); + } + + template bool MarkovAutomaton::isHybridState(storm::storage::sparse::state_type state) const { return isMarkovianState(state) && (this->getTransitionMatrix().getRowGroupSize(state) > 1); @@ -267,13 +277,29 @@ namespace storm { return std::make_shared>(std::move(rateMatrix), std::move(stateLabeling)); } + template + bool MarkovAutomaton::checkContainsZenoCycle() const { + if (isClosed() && markovianStates.empty()) { + return true; + } + + storm::storage::MaximalEndComponentDecomposition maxEnd(this->getTransitionMatrix(), this->getBackwardTransitions(),~markovianStates); + return !maxEnd.empty(); + } + template void MarkovAutomaton::printModelInformationToStream(std::ostream& out) const { this->printModelInformationHeaderToStream(out); out << "Choices: \t" << this->getNumberOfChoices() << std::endl; out << "Markovian St.: \t" << this->getMarkovianStates().getNumberOfSetBits() << std::endl; - out << "Max. Rate.: \t" << this->getMaximalExitRate() << std::endl; + out << "Max. Rate.: \t"; + if (this->getMarkovianStates().empty()) { + out << "None"; + } else { + out << this->getMaximalExitRate(); + } + out << std::endl; this->printModelInformationFooterToStream(out); } diff --git a/src/storm/models/sparse/MarkovAutomaton.h b/src/storm/models/sparse/MarkovAutomaton.h index c7ca80f35..94f71dc1d 100644 --- a/src/storm/models/sparse/MarkovAutomaton.h +++ b/src/storm/models/sparse/MarkovAutomaton.h @@ -68,6 +68,14 @@ namespace storm { * @return True iff the Markov automaton is closed. */ bool isClosed() const; + + /*! + * Retrieves whether the Markov automaton contains Zeno cycles. + * A Zeno cyle contains only non-Markovian states and allows to visit infinitely many states in finite time. + * + * @return True iff the Markov automaton contains Zeno cycles. + */ + bool containsZenoCycle() const; /*! * Retrieves whether the given state is a hybrid state, i.e. Markovian and probabilistic. @@ -148,7 +156,6 @@ namespace storm { */ std::shared_ptr> convertToCtmc() const; - virtual void printModelInformationToStream(std::ostream& out) const override; private: @@ -164,6 +171,13 @@ namespace storm { * Checks whether the automaton is closed by actually looking at the transition information. */ bool checkIsClosed() const; + + /*! + * Checks whether a Zeno cycle is present. + * + * @return True iff a Zeno cycle is present. + */ + bool checkContainsZenoCycle() const; // A bit vector representing the set of Markovian states. storm::storage::BitVector markovianStates; @@ -171,9 +185,11 @@ namespace storm { // A vector storing the exit rates of all states of the model. std::vector exitRates; - // A flag indicating whether the Markov automaton has been closed, which is typically a prerequisite - // for model checking. + // A flag indicating whether the Markov automaton has been closed, which is typically a prerequisite for model checking. bool closed; + + // A flag indicating whether the Markov automaton contains Zeno cycles. + mutable boost::optional hasZenoCycle; }; } // namespace sparse diff --git a/src/test/storm/CMakeLists.txt b/src/test/storm/CMakeLists.txt index f3f4ebabc..20e27e95b 100755 --- a/src/test/storm/CMakeLists.txt +++ b/src/test/storm/CMakeLists.txt @@ -10,7 +10,7 @@ register_source_groups_from_filestructure("${ALL_FILES}" test) include_directories(${GTEST_INCLUDE_DIR}) # Set split and non-split test directories -set(NON_SPLIT_TESTS abstraction adapter builder logic parser permissiveschedulers solver storage transformer utility) +set(NON_SPLIT_TESTS abstraction adapter builder logic model parser permissiveschedulers solver storage transformer utility) set(MODELCHECKER_TEST_SPLITS abstraction csl exploration multiobjective reachability) set(MODELCHECKER_PRCTL_TEST_SPLITS dtmc mdp) diff --git a/src/test/storm/model/MarkovAutomatonTest.cpp b/src/test/storm/model/MarkovAutomatonTest.cpp new file mode 100644 index 000000000..eb4b75b9a --- /dev/null +++ b/src/test/storm/model/MarkovAutomatonTest.cpp @@ -0,0 +1,38 @@ +#include "test/storm_gtest.h" +#include "storm-config.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/models/sparse/MarkovAutomaton.h" +#include "storm-parsers/parser/PrismParser.h" +#include "storm/builder/ExplicitModelBuilder.h" + + +TEST(MarkovAutomatonTest, ZenoCycleCheck) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/simple.ma"); + + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).build(); + EXPECT_EQ(5ul, model->getNumberOfStates()); + EXPECT_EQ(8ul, model->getNumberOfTransitions()); + ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton)); + EXPECT_FALSE(model->as>()->containsZenoCycle()); + + program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/hybrid_states.ma"); + model = storm::builder::ExplicitModelBuilder(program).build(); + EXPECT_EQ(5ul, model->getNumberOfStates()); + EXPECT_EQ(13ul, model->getNumberOfTransitions()); + ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton)); + EXPECT_FALSE(model->as>()->containsZenoCycle()); + + program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/stream2.ma"); + model = storm::builder::ExplicitModelBuilder(program).build(); + EXPECT_EQ(12ul, model->getNumberOfStates()); + EXPECT_EQ(14ul, model->getNumberOfTransitions()); + ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton)); + EXPECT_FALSE(model->as>()->containsZenoCycle()); + + program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/zeno.ma"); + model = storm::builder::ExplicitModelBuilder(program).build(); + EXPECT_EQ(5ul, model->getNumberOfStates()); + EXPECT_EQ(8ul, model->getNumberOfTransitions()); + ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton)); + EXPECT_TRUE(model->as>()->containsZenoCycle()); +}