From 45f137face763a79e7fc09580854ccb80549d9e6 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 26 Nov 2013 17:08:41 +0100
Subject: [PATCH] Prepared stub for Long-Run Average computation for Markov
 automata.

Former-commit-id: fef601a81d7e43208f838c6ce8341235a2c9241a
---
 .../csl/SparseMarkovAutomatonCslModelChecker.h         | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
index 552c19314..1a3fe138f 100644
--- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
+++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
@@ -67,6 +67,16 @@ namespace storm {
                     return result;
                 }
                 
+                std::vector<ValueType> checkLongRunAverage(bool min, storm::storage::BitVector const& goalStates) const {
+                    // Start by decomposing the Markov automaton into its MECs.
+                    storm::storage::MaximalEndComponentDecomposition<double> mecDecomposition(this->getModel(), ~goalStates);
+                    
+                    // Now compute the long-run average for all end components in isolation.
+                    for (storm::storage::MaximalEndComponent const& mec : mecDecomposition) {
+                        
+                    }
+                }
+                
                 std::vector<ValueType> checkExpectedTime(bool min, storm::storage::BitVector const& goalStates) const {
                     // TODO: check whether the Markov automaton is closed once again? Or should that rather be done when constructing the model checker?
                     // For now we just assume that it is closed already.