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: 8a833cc05e

src/modelchecker/prctl/AbstractModelChecker.h

@@ -68,14 +68,14 @@ public:
 	/*!
 	 * Constructs an AbstractModelChecker with the given model.
 	 */
-	explicit AbstractModelChecker(storm::models::AbstractModel<Type> const& model) : model(model) {
+	explicit AbstractModelChecker(storm::models::AbstractModel<Type> 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<Type> const& modelchecker) : model(modelchecker.model) {
+	explicit AbstractModelChecker(AbstractModelChecker<Type> const& modelchecker) : model(modelchecker.model), subSystem(modelchecker.subSystem) {
 		// Intentionally left empty.
 	}
 	
@@ -205,7 +205,11 @@ public:
 	 */
 	storm::storage::BitVector checkAp(storm::property::prctl::Ap<Type> const& formula) const {
 		if (formula.getAp() == "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,8 +219,12 @@ public:
 			throw storm::exceptions::InvalidPropertyException() << "Atomic proposition '" << formula.getAp() << "' is invalid.";
 		}
 
+		if(subSystem != nullptr) {
+			return *subSystem & storm::storage::BitVector(model.getLabeledStates(formula.getAp()));
+		} else {
 			return storm::storage::BitVector(model.getLabeledStates(formula.getAp()));
 		}
+	}
 
 	/*!
 	 * Checks the given formula that is a logical "and" of two formulae.
@@ -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<Type> 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