From 0cb390b186e04e5b8562e793671773eca3e31853 Mon Sep 17 00:00:00 2001 From: masawei Date: Mon, 14 Oct 2013 11:53:49 +0200 Subject: [PATCH] More integration work. Ran into problem with the AbstractModelChecker being declared const for the model check. I use it for the subsystem generation and tell it what the current subsystem is. so I have two options: 1. Carry the subsystem as argument through all checking functions of the complete checking tree 2. Store the subsystem in the checker and use it in checkAp to induce the correct result back through the tree. In the original implementation I used option 2. But that does only work if it is not constant. Former-commit-id: 8a833cc05e4c7d2eb90a5f3659ed2f9cdda05087 --- src/modelchecker/prctl/AbstractModelChecker.h | 32 ++++++++++++++++--- 1 file changed, 28 insertions(+), 4 deletions(-) diff --git a/src/modelchecker/prctl/AbstractModelChecker.h b/src/modelchecker/prctl/AbstractModelChecker.h index 793af403e..a45a1dc50 100644 --- a/src/modelchecker/prctl/AbstractModelChecker.h +++ b/src/modelchecker/prctl/AbstractModelChecker.h @@ -68,14 +68,14 @@ public: /*! * Constructs an AbstractModelChecker with the given model. */ - explicit AbstractModelChecker(storm::models::AbstractModel const& model) : model(model) { + explicit AbstractModelChecker(storm::models::AbstractModel const& model, storm::storage::BitVector* subSystem = nullptr) : model(model), subSystem(subSystem) { // Intentionally left empty. } /*! * Copy constructs an AbstractModelChecker from the given model checker. In particular, this means that the newly * constructed model checker will have the model of the given model checker as its associated model. */ - explicit AbstractModelChecker(AbstractModelChecker const& modelchecker) : model(modelchecker.model) { + explicit AbstractModelChecker(AbstractModelChecker const& modelchecker) : model(modelchecker.model), subSystem(modelchecker.subSystem) { // Intentionally left empty. } @@ -205,7 +205,11 @@ public: */ storm::storage::BitVector checkAp(storm::property::prctl::Ap const& formula) const { if (formula.getAp() == "true") { - return storm::storage::BitVector(model.getNumberOfStates(), true); + if(subSystem != nullptr) { + return *subSystem; + } else { + return storm::storage::BitVector(model.getNumberOfStates(), true); + } } else if (formula.getAp() == "false") { return storm::storage::BitVector(model.getNumberOfStates()); } @@ -215,7 +219,11 @@ public: throw storm::exceptions::InvalidPropertyException() << "Atomic proposition '" << formula.getAp() << "' is invalid."; } - return storm::storage::BitVector(model.getLabeledStates(formula.getAp())); + if(subSystem != nullptr) { + return *subSystem & storm::storage::BitVector(model.getLabeledStates(formula.getAp())); + } else { + return storm::storage::BitVector(model.getLabeledStates(formula.getAp())); + } } /*! @@ -305,6 +313,15 @@ public: return result; } + /*! + * Sets the subsystem. + * + * @param subSystem The subsystem the model check is to be confined to. + */ + void setSubSystem(storm::storage::BitVector* subSys) { + subSystem = subSys; + } + private: /*! @@ -314,6 +331,13 @@ private: * model checker object is unsafe after the object has been destroyed. */ storm::models::AbstractModel const& model; + + /*! + * A pointer to the subsystem of the Model to which the check of the model is to be confined. + * + * @note that this is a nullptr iff the check is not to be confined. + */ + storm::storage::BitVector* subSystem; }; } // namespace prctl