diff --git a/src/formula/Csl/AbstractNoBoundOperator.h b/src/formula/Csl/AbstractNoBoundOperator.h index 8a4badbf8..9960e8de2 100644 --- a/src/formula/Csl/AbstractNoBoundOperator.h +++ b/src/formula/Csl/AbstractNoBoundOperator.h @@ -42,8 +42,8 @@ public: * Interface class for all CSL No Bound operators. */ template -class AbstractNoBoundOperator: public AbstractCslFormula/*, - public virtual storm::property::abstract::IOptimizingOperator*/ { +class AbstractNoBoundOperator: public AbstractCslFormula, + public virtual storm::property::abstract::IOptimizingOperator { public: AbstractNoBoundOperator() { // Intentionally left empty diff --git a/src/formula/abstract/StateNoBoundOperator.h b/src/formula/abstract/StateNoBoundOperator.h index 2961debea..4780f2587 100644 --- a/src/formula/abstract/StateNoBoundOperator.h +++ b/src/formula/abstract/StateNoBoundOperator.h @@ -47,7 +47,7 @@ namespace abstract { * @see StateBoundOperator */ template -class StateNoBoundOperator: public virtual AbstractFormula { +class StateNoBoundOperator: public virtual AbstractFormula, public OptimizingOperator { // Throw a compiler error if FormulaType is not a subclass of AbstractFormula. static_assert(std::is_base_of, FormulaType>::value, diff --git a/src/modelchecker/csl/AbstractModelChecker.h b/src/modelchecker/csl/AbstractModelChecker.h index 7a839bb4f..d1d3bc1dc 100644 --- a/src/modelchecker/csl/AbstractModelChecker.h +++ b/src/modelchecker/csl/AbstractModelChecker.h @@ -211,7 +211,7 @@ public: * @param formula The formula to check. * @returns The set of states satisfying the formula represented by a bit vector. */ - virtual storm::storage::BitVector checkOr(storm::property::csl::Or const& formula) const { + storm::storage::BitVector checkOr(storm::property::csl::Or const& formula) const { storm::storage::BitVector result = formula.getLeft().check(*this); storm::storage::BitVector right = formula.getRight().check(*this); result |= right; diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h new file mode 100644 index 000000000..f3bb6bb23 --- /dev/null +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -0,0 +1,153 @@ +#ifndef STORM_MODELCHECKER_CSL_SPARSEMARKOVAUTOMATONCSLMODELCHECKER_H_ +#define STORM_MODELCHECKER_CSL_SPARSEMARKOVAUTOMATONCSLMODELCHECKER_H_ + +#include + +#include "src/modelchecker/csl/AbstractModelChecker.h" +#include "src/models/MarkovAutomaton.h" +#include "src/storage/BitVector.h" +#include "src/solver/AbstractNondeterministicLinearEquationSolver.h" +#include "src/exceptions/NotImplementedException.h" + +namespace storm { + namespace modelchecker { + namespace csl { + + template + class SparseMarkovAutomatonCslModelChecker : public AbstractModelChecker { + public: + + explicit SparseMarkovAutomatonCslModelChecker(storm::models::MarkovAutomaton const& model, storm::solver::AbstractNondeterministicLinearEquationSolver* linearEquationSolver) : AbstractModelChecker(model), minimumOperatorStack(), linearEquationSolver(linearEquationSolver) { + // Intentionally left empty. + } + + /*! + * Returns a constant reference to the MDP associated with this model checker. + * @returns A constant reference to the MDP associated with this model checker. + */ + storm::models::MarkovAutomaton const& getModel() const { + return AbstractModelChecker::template getModel>(); + } + + std::vector checkUntil(storm::property::csl::Until const& formula, bool qualitative) const { + throw storm::exceptions::NotImplementedException() << "Model checking Until formulas on Markov automata is not yet implemented."; + } + + std::vector checkTimeBoundedUntil(storm::property::csl::TimeBoundedUntil const& formula, bool qualitative) const { + throw storm::exceptions::NotImplementedException() << "Model checking Until formulas on Markov automata is not yet implemented."; + } + + std::vector checkTimeBoundedEventually(storm::property::csl::TimeBoundedEventually const& formula, bool qualitative) const { + throw storm::exceptions::NotImplementedException() << "Model checking time-bounded Until formulas on Markov automata is not yet implemented."; + } + + std::vector checkGlobally(storm::property::csl::Globally const& formula, bool qualitative) const { + throw storm::exceptions::NotImplementedException() << "Model checking Globally formulas on Markov automata is not yet implemented."; + } + + std::vector checkEventually(storm::property::csl::Eventually const& formula, bool qualitative) const { + throw storm::exceptions::NotImplementedException() << "Model checking Eventually formulas on Markov automata is not yet implemented."; + } + + std::vector checkNext(storm::property::csl::Next const& formula, bool qualitative) const { + throw storm::exceptions::NotImplementedException() << "Model checking Next formulas on Markov automata is not yet implemented."; + } + + std::vector checkNoBoundOperator(storm::property::csl::AbstractNoBoundOperator const& formula) const { + // Check if the operator was an non-optimality operator and report an error in that case. + if (!formula.isOptimalityOperator()) { + LOG4CPLUS_ERROR(logger, "Formula does not specify neither min nor max optimality, which is not meaningful for nondeterministic models."); + throw storm::exceptions::InvalidArgumentException() << "Formula does not specify neither min nor max optimality, which is not meaningful for nondeterministic models."; + } + minimumOperatorStack.push(formula.isMinimumOperator()); + std::vector result = formula.check(*this, false); + minimumOperatorStack.pop(); + return result; + } + + std::vector 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. + + // Start by identifying the states for which values need to be computed. + storm::storage::BitVector maybeStates = ~goalStates; + + // Then, we can eliminate the rows and columns for all states whose values are already known to be 0. + std::vector x(maybeStates.getNumberOfSetBits()); + std::vector subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates); + storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(maybeStates, this->getModel().getNondeterministicChoiceIndices()); + + // Now prepare the mean sojourn times for all states so they can be used as the right-hand side of the equation system. + std::vector meanSojournTimes(this->getModel().getExitRates()); + for (auto state : this->getModel().getMarkovianStates()) { + meanSojournTimes[state] = storm::utility::constGetOne() / meanSojournTimes[state]; + } + + // Finally, prepare the actual right-hand side. + std::vector b(submatrix.getRowCount()); + storm::utility::vector::selectVectorValuesRepeatedly(b, maybeStates, this->getModel().getNondeterministicChoiceIndices(), meanSojournTimes); + + // Solve the corresponding system of equations. + if (linearEquationSolver != nullptr) { + this->linearEquationSolver->solveEquationSystem(min, submatrix, x, b, subNondeterministicChoiceIndices); + } else { + throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available."; + } + + // Create resulting vector. + std::vector result(this->getModel().getNumberOfStates()); + + // Set values of resulting vector according to previous result (goal states will have a value of 0) and return the result. + storm::utility::vector::setVectorValues(result, maybeStates, x); + return result; + } + + protected: + /*! + * A stack used for storing whether we are currently computing min or max probabilities or rewards, respectively. + * The topmost element is true if and only if we are currently computing minimum probabilities or rewards. + */ + mutable std::stack minimumOperatorStack; + + private: + /*! + * Computes the nondeterministic choice indices vector resulting from reducing the full system to the states given + * by the parameter constraint. + * + * @param constraint A bit vector specifying which states are kept. + * @returns A vector of the nondeterministic choice indices of the subsystem induced by the given constraint. + */ + std::vector computeNondeterministicChoiceIndicesForConstraint(storm::storage::BitVector const& constraint) const { + // First, get a reference to the full nondeterministic choice indices. + std::vector const& nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices(); + + // Reserve the known amount of slots for the resulting vector. + std::vector subNondeterministicChoiceIndices(constraint.getNumberOfSetBits() + 1); + uint_fast64_t currentRowCount = 0; + uint_fast64_t currentIndexCount = 1; + + // Set the first element as this will clearly begin at offset 0. + subNondeterministicChoiceIndices[0] = 0; + + // Loop over all states that need to be kept and copy the relative indices of the nondeterministic choices over + // to the resulting vector. + for (auto index : constraint) { + subNondeterministicChoiceIndices[currentIndexCount] = currentRowCount + nondeterministicChoiceIndices[index + 1] - nondeterministicChoiceIndices[index]; + currentRowCount += nondeterministicChoiceIndices[index + 1] - nondeterministicChoiceIndices[index]; + ++currentIndexCount; + } + + // Put a sentinel element at the end. + subNondeterministicChoiceIndices[constraint.getNumberOfSetBits()] = currentRowCount; + + return subNondeterministicChoiceIndices; + } + + // An object that is used for solving linear equations and performing matrix-vector multiplication. + std::unique_ptr> linearEquationSolver; + }; + } + } +} + +#endif /* STORM_MODELCHECKER_CSL_SPARSEMARKOVAUTOMATONCSLMODELCHECKER_H_ */ diff --git a/src/modelchecker/prctl/AbstractModelChecker.h b/src/modelchecker/prctl/AbstractModelChecker.h index f67c719bd..4658c779f 100644 --- a/src/modelchecker/prctl/AbstractModelChecker.h +++ b/src/modelchecker/prctl/AbstractModelChecker.h @@ -228,7 +228,7 @@ public: * @param formula The formula to check. * @return The set of states satisfying the formula represented by a bit vector. */ - virtual storm::storage::BitVector checkOr(storm::property::prctl::Or const& formula) const { + storm::storage::BitVector checkOr(storm::property::prctl::Or const& formula) const { storm::storage::BitVector result = formula.getLeft().check(*this); storm::storage::BitVector right = formula.getRight().check(*this); result |= right; diff --git a/src/models/MarkovAutomaton.h b/src/models/MarkovAutomaton.h index a26c39892..7ab2e3fad 100644 --- a/src/models/MarkovAutomaton.h +++ b/src/models/MarkovAutomaton.h @@ -85,7 +85,15 @@ namespace storm { bool isProbabilisticState(uint_fast64_t state) const { return !this->markovianStates.get(state); } - + + std::vector const& getExitRates() const { + return this->exitRates; + } + + storm::storage::BitVector const& getMarkovianStates() const { + return this->markovianStates; + } + void close() { if (!closed) { // First, count the number of hybrid states to know how many Markovian choices @@ -108,6 +116,11 @@ namespace storm { // Now copy over all choices that need to be kept. uint_fast64_t currentChoice = 0; for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) { + // If the state is a hybrid state, closing it will make it a probabilistic state, so we remove the Markovian marking. + if (this->isHybridState(state)) { + this->markovianStates.set(state, false); + } + // Record the new beginning of choices of this state. newNondeterministicChoiceIndices[state] = currentChoice; diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/parser/MarkovAutomatonSparseTransitionParser.cpp index 3b3fce470..46bc05d2f 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.cpp +++ b/src/parser/MarkovAutomatonSparseTransitionParser.cpp @@ -53,6 +53,8 @@ namespace storm { // Record that the current source was the last source. lastsource = source; + buf = trimWhitespaces(buf); + // Depending on the action name, the choice is either a probabilitic one or a markovian one. bool isMarkovianChoice = false; if (buf[0] == '!') { @@ -85,6 +87,7 @@ namespace storm { // At this point, we need to check whether there is an additional successor or we have reached the next choice for the same or a different state. do { + buf = trimWhitespaces(buf); // If the end of the file was reached, we need to abort and check whether we are in a legal state. if (buf[0] == '\0') { if (!hasSuccessorState) { @@ -173,6 +176,8 @@ namespace storm { // Record that the current source was the last source. lastsource = source; + buf = trimWhitespaces(buf); + // Depending on the action name, the choice is either a probabilitic one or a markovian one. bool isMarkovianChoice = false; if (buf[0] == '!') { @@ -192,6 +197,8 @@ namespace storm { // At this point, we need to check whether there is an additional successor or we have reached the next choice for the same or a different state. do { + buf = trimWhitespaces(buf); + // If the end of the file was reached, we need to abort and check whether we are in a legal state. if (buf[0] == '\0') { // Under the assumption that the currently open choice has at least one successor (which is given after the first run) diff --git a/src/storm.cpp b/src/storm.cpp index 880bccb46..bd2ba1f5c 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -24,7 +24,7 @@ #include "src/models/Dtmc.h" #include "src/models/MarkovAutomaton.h" #include "src/storage/SparseMatrix.h" -#include "src/storage/MaximalEndComponentDecomposition.h" +#include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" #include "src/models/AtomicPropositionsLabeling.h" #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" @@ -471,7 +471,10 @@ int main(const int argc, const char* argv[]) { LOG4CPLUS_INFO(logger, "Model is a Markov automaton."); std::shared_ptr> markovAutomaton = parser.getModel>(); markovAutomaton->close(); - storm::storage::MaximalEndComponentDecomposition mecDecomposition(*markovAutomaton); + + storm::modelchecker::csl::SparseMarkovAutomatonCslModelChecker mc(*markovAutomaton, new storm::solver::AbstractNondeterministicLinearEquationSolver()); + mc.checkExpectedTime(true, markovAutomaton->getLabeledStates("goal")); + break; } case storm::models::Unknown: