Check for Zeno cycles in MA

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

src/storm-cli-utilities/model-handling.h

@@ -332,6 +332,8 @@ namespace storm {
 
             std::shared_ptr<storm::models::sparse::Model<ValueType>> 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();

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 <typename ValueType, typename RewardModelType>
+            bool MarkovAutomaton<ValueType, RewardModelType>::containsZenoCycle() const {
+                if (!this->hasZenoCycle.is_initialized()) {
+                    this->hasZenoCycle = this->checkContainsZenoCycle();
+                }
+                return this->hasZenoCycle.get();
+            }
+
+
             template <typename ValueType, typename RewardModelType>
             bool MarkovAutomaton<ValueType, RewardModelType>::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<storm::models::sparse::Ctmc<ValueType, RewardModelType>>(std::move(rateMatrix), std::move(stateLabeling));
             }
 
+            template<typename ValueType, typename RewardModelType>
+            bool MarkovAutomaton<ValueType, RewardModelType>::checkContainsZenoCycle() const {
+                if (isClosed() && markovianStates.empty()) {
+                    return true;
+                }
+
+                storm::storage::MaximalEndComponentDecomposition<ValueType> maxEnd(this->getTransitionMatrix(), this->getBackwardTransitions(),~markovianStates);
+                return !maxEnd.empty();
+            }
+
 
             template<typename ValueType, typename RewardModelType>
             void MarkovAutomaton<ValueType, RewardModelType>::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);
             }
 

src/storm/models/sparse/MarkovAutomaton.h

@@ -69,6 +69,14 @@ namespace storm {
                  */
                 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<storm::models::sparse::Ctmc<ValueType, RewardModelType>> convertToCtmc() const;
 
-                
                 virtual void printModelInformationToStream(std::ostream& out) const override;
                 
             private:
@@ -165,15 +172,24 @@ namespace storm {
                  */
                 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;
                 
                 // A vector storing the exit rates of all states of the model.
                 std::vector<ValueType> 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<bool> hasZenoCycle;
             };
             
         } // namespace sparse

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)
 

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<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
+    EXPECT_EQ(5ul, model->getNumberOfStates());
+    EXPECT_EQ(8ul, model->getNumberOfTransitions());
+    ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton));
+    EXPECT_FALSE(model->as<storm::models::sparse::MarkovAutomaton<double>>()->containsZenoCycle());
+
+    program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/hybrid_states.ma");
+    model = storm::builder::ExplicitModelBuilder<double>(program).build();
+    EXPECT_EQ(5ul, model->getNumberOfStates());
+    EXPECT_EQ(13ul, model->getNumberOfTransitions());
+    ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton));
+    EXPECT_FALSE(model->as<storm::models::sparse::MarkovAutomaton<double>>()->containsZenoCycle());
+
+    program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/stream2.ma");
+    model = storm::builder::ExplicitModelBuilder<double>(program).build();
+    EXPECT_EQ(12ul, model->getNumberOfStates());
+    EXPECT_EQ(14ul, model->getNumberOfTransitions());
+    ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton));
+    EXPECT_FALSE(model->as<storm::models::sparse::MarkovAutomaton<double>>()->containsZenoCycle());
+
+    program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/zeno.ma");
+    model = storm::builder::ExplicitModelBuilder<double>(program).build();
+    EXPECT_EQ(5ul, model->getNumberOfStates());
+    EXPECT_EQ(8ul, model->getNumberOfTransitions());
+    ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton));
+    EXPECT_TRUE(model->as<storm::models::sparse::MarkovAutomaton<double>>()->containsZenoCycle());
+}