First implementation of the BitVector to Dtmc subsystem converter in Dtmc.h

-Had to add a addState function to AtomicPropositionLabeling to be able to throw out the unneeded states using the substates constructor while at the end adding the absorbing state and its label.
 An alternative for that would be to provide a constructor taking the mapping and the single labelings vector as well as a getter for the single labelings.
-The --counterexample command now only uses the pctl file given as argument to it and therefore it is now superflous to give the --prctl command in that case.
-Also fixed a bug in the filter constructor of the BitVector.
 Now it copies all bit values specified by the filter to the correct index of new instance instead of all to index 0.

Next up: Handle the optionals of the Dtmc when creating the sub-Dtmc.


Former-commit-id: b45ee94cb2

src/counterexamples/PathBasedSubsystemGenerator.h

@@ -513,7 +513,7 @@ public:
 	/*!
 	 *
 	 */
-	static void computeCriticalSubsystem(storm::models::Dtmc<T> const& model, storm::property::prctl::AbstractStateFormula<T> const& stateFormula) {
+	static storm::models::Dtmc<T> computeCriticalSubsystem(storm::models::Dtmc<T>& model, storm::property::prctl::AbstractStateFormula<T> const& stateFormula) {
 
 		//-------------------------------------------------------------
 		// 1. Strip and handle formulas
@@ -539,7 +539,7 @@ public:
 
 		if(boundOperator == nullptr){
 			LOG4CPLUS_ERROR(logger, "No path bound operator at formula root.");
-			return;
+			return model.getSubDtmc(subSys);
 		}
 		bound = boundOperator->getBound();
 
@@ -582,7 +582,7 @@ public:
 		}
 		else {
 			LOG4CPLUS_ERROR(logger, "Strange path formula. Can't decipher.");
-			return;
+			return model.getSubDtmc(subSys);
 		}
 
 		//-------------------------------------------------------------
@@ -620,7 +620,7 @@ public:
 			LOG4CPLUS_INFO(logger, "Critical subsystem: " << subSys.toString());
 			std::cout << "Critical subsystem: " << subSys.toString() << std::endl;
 
-			return;
+			return model.getSubDtmc(subSys);
 		}
 
 
@@ -704,6 +704,7 @@ public:
 		std::cout << "Critical subsystem: " << subSys.toString() << std::endl;
 #endif
 
+		return model.getSubDtmc(subSys);
 	}
 
     };

src/models/AtomicPropositionsLabeling.h

@@ -283,6 +283,22 @@ public:
 		return this->nameToLabelingMap;
 	}
 
+	/*!
+	 * Adds a state to the labeling.
+	 * Since this operation is quite expensive (resizing of all BitVectors containing the labeling), it should
+	 * only be used in special cases to add one or two states.
+	 * If you want to build a new AtomicPropositionlabeling:
+	 *   - Count the number of states you need.
+	 *   - Then add the labelings using addAtomicProposition() and addAtomicPropositionToState().
+	 * Do NOT use this method for this purpose.
+	 */
+	void addState() {
+		for(uint_fast64_t i = 0; i < apsCurrent; i++) {
+			singleLabelings[i].resize(singleLabelings[i].getSize() + 1);
+		}
+		stateCount++;
+	}
+
 	/*!
 	 * Calculates a hash over all values contained in this Sparse Matrix.
 	 * @return size_t A Hash Value

src/models/Dtmc.h

@@ -121,6 +121,121 @@ public:
 		return AbstractDeterministicModel<T>::getHash();
 	}
 
+	/*!
+	 * Generates a sub-Dtmc of this Dtmc induced by the states specified by the bitvector.
+	 * E.g. a Dtmc that is partial isomorph (on the given states) to this one.
+	 * @param subSysStates A BitVector where all states that should be kept are indicated 
+	 *                     by a set bit of the corresponding index.
+	 *                     Waring: If the vector does not have the correct size, it will be resized.
+	 * @return The sub-Dtmc.
+	 */
+	storm::models::Dtmc<T> getSubDtmc(storm::storage::BitVector& subSysStates) {
+
+
+		// Is there any state in the subsystem?
+		if(subSysStates.getNumberOfSetBits() == 0) {
+			LOG4CPLUS_ERROR(logger, "No states in subsystem!");
+			return storm::models::Dtmc<T>(storm::storage::SparseMatrix<T>(0),
+					  	  	  	  	  	  storm::models::AtomicPropositionsLabeling(this->getStateLabeling(), subSysStates),
+					  	  	  	  	  	  boost::optional<std::vector<T>>(),
+					  	  	  	  	  	  boost::optional<storm::storage::SparseMatrix<T>>(),
+					  	  	  	  	  	  boost::optional<std::vector<std::set<uint_fast64_t>>>());
+		}
+
+		// Does the vector have the right size?
+		if(subSysStates.getSize() != this->getNumberOfStates()) {
+			LOG4CPLUS_INFO(logger, "BitVector has wrong size. Resizing it...");
+			subSysStates.resize(this->getNumberOfStates());
+		}
+
+		// Test if it is a proper subsystem of this Dtmc, i.e. if there is at least one state to be left out.
+		if(subSysStates.getNumberOfSetBits() == subSysStates.getSize()) {
+			LOG4CPLUS_INFO(logger, "All states are kept. This is no proper subsystem.");
+			return storm::models::Dtmc<T>(*this);
+		}
+
+		// 1. Get all necessary information from the old transition matrix
+		storm::storage::SparseMatrix<T> const & origMat = this->getTransitionMatrix();
+		uint_fast64_t const stateCount = origMat.getColumnCount();
+
+		// Iterate over all rows. Count the number of all transitions from the old system to be 
+		// transfered to the new one. Also build a mapping from the state number of the old system 
+		// to the state number of the new system.
+		uint_fast64_t subSysTransitionCount = 0;
+		uint_fast64_t row = 0;
+		uint_fast64_t newRow = 0;
+		std::vector<uint_fast64_t> stateMapping;
+		for(auto iter = origMat.begin(); iter != origMat.end(); ++iter) {
+			if(subSysStates.get(row)){
+				for(auto colIter = iter.begin(); colIter != iter.end(); ++colIter) {
+					if(subSysStates.get(colIter.column())) {
+						subSysTransitionCount++;	
+					} 
+				}
+				stateMapping.push_back(newRow);
+				newRow++;
+			} else {
+				stateMapping.push_back((uint_fast64_t) -1);
+			}
+			row++;
+		}
+
+		// 2. Construct transition matrix
+
+		// Take all states indicated by the vector as well as one additional state as target of 
+		// all transitions that target a state that is not kept.
+		uint_fast64_t const newStateCount = subSysStates.getNumberOfSetBits() + 1;
+		storm::storage::SparseMatrix<T> newMat(newStateCount);
+
+		// The number of transitions of the new Dtmc is the number of transitions transfered 
+		// from the old one plus one transition for each state to the new one.
+		newMat.initialize(subSysTransitionCount + newStateCount);
+
+		// Now fill the matrix.
+		newRow = 0;
+		row = 0;
+		T rest = 0;
+		for(auto iter = origMat.begin(); iter != origMat.end(); ++iter) {
+			if(subSysStates.get(row)){
+				// Transfer transitions
+				for(auto colIter = iter.begin(); colIter != iter.end(); ++colIter) {
+					if(subSysStates.get(colIter.column())) {
+						newMat.addNextValue(newRow, stateMapping[colIter.column()], colIter.value());
+					} else {
+						rest += colIter.value();
+					}
+				}
+
+				// Insert the transition taking care of the remaining outgoing probability.
+				newMat.addNextValue(newRow, newStateCount - 1, rest);
+				rest = (T) 0;
+
+				newRow++;
+			}
+			row++;
+		}
+
+		// Insert last transition: self loop on added state
+		newMat.addNextValue(newStateCount - 1, newStateCount - 1, (T) 1);
+
+		newMat.finalize(false);
+
+		// 3. Take care of the labeling
+		storm::models::AtomicPropositionsLabeling newLabeling = storm::models::AtomicPropositionsLabeling(this->getStateLabeling(), subSysStates);
+		newLabeling.addState();
+		//newLabeling.addAtomicProposition();
+
+		// 4. Make Dtmc from the matrix and return it
+		//TODO: test the labeling, handle optionals.
+		return storm::models::Dtmc<T>(newMat, 
+									  newLabeling,
+									  boost::optional<std::vector<T>>(),
+									  boost::optional<storm::storage::SparseMatrix<T>>(),
+									  boost::optional<std::vector<std::set<uint_fast64_t>>>()
+									  );
+
+	}
+
 private:
 	/*!
 	 *	@brief Perform some sanity checks.

src/storage/BitVector.h

@@ -166,6 +166,7 @@ public:
         uint_fast64_t nextPosition = 0;
         for (auto position : filter) {
             this->set(nextPosition, other.get(position));
+            nextPosition++;
         }
     }
     

src/storm.cpp

@@ -258,37 +258,6 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker<double>
 	}
 }
 
-/*!
- * Checks if a counterexample for the given PRCTL formula can be computed.
- *
- * @param formula The formula to be examined.
- * @param model The model for which the formula is to be examined.
- * @return true iff a counterexample can be computed
- */
-bool checkForCounterExampleGeneration(storm::property::prctl::AbstractPrctlFormula<double> &formula, storm::models::Dtmc<double> &model) {
-	// First check if it is a formula type for which a counterexample can be generated.
-	if (dynamic_cast<storm::property::prctl::AbstractNoBoundOperator<double> const*>(&formula) != nullptr) {
-		LOG4CPLUS_ERROR(logger, "Can not generate a counterexample without a given bound.");
-		return false;
-	} else if (dynamic_cast<storm::property::prctl::AbstractStateFormula<double> const*>(&formula) != nullptr) {
-		storm::property::prctl::AbstractStateFormula<double> const& stateForm = static_cast<storm::property::prctl::AbstractStateFormula<double> const&>(formula);
-
-		// Now check if the model does not satisfy the formula.
-		// That is if there is at least one initial state of the model that does not.
-		storm::storage::BitVector result = stateForm.check(*createPrctlModelChecker(model));
-		if((result & model.getInitialStates()).getNumberOfSetBits() < model.getInitialStates().getNumberOfSetBits()) {
-			return true;
-		} else {
-			LOG4CPLUS_ERROR(logger, "Formula is satisfied. Can not generate counterexample.");
-			return false;
-		}
-
-	} else {
-		LOG4CPLUS_ERROR(logger, "Unexpected kind of formula. Expected either a No Bound or a State formula.");
-		return false;
-	}
-}
-
 /*!
  * Handles the counterexample generation control.
  */
@@ -302,20 +271,17 @@ bool checkForCounterExampleGeneration(storm::property::prctl::AbstractPrctlFormu
 	storm::models::Dtmc<double> model = *parser.getModel<storm::models::Dtmc<double>>();
 	LOG4CPLUS_INFO(logger, "Model is a DTMC.");
 
-	// Test for and get PRCTL formulas.
-	storm::settings::Settings* s = storm::settings::Settings::getInstance();
-
-	if (!s->isSet("prctl")) {
-		LOG4CPLUS_ERROR(logger, "No PRCTL formula file specified.");
-		return;
-	}
-
 	// Get specified PRCTL formulas.
-	std::string const chosenPrctlFile = s->getOptionByLongName("prctl").getArgument(0).getValueAsString();
+	std::string const chosenPrctlFile = storm::settings::Settings::getInstance()->getOptionByLongName("counterExample").getArgument(0).getValueAsString();
 	LOG4CPLUS_INFO(logger, "Parsing prctl file: " << chosenPrctlFile << ".");
 	std::list<storm::property::prctl::AbstractPrctlFormula<double>*> formulaList = storm::parser::PrctlFileParser(chosenPrctlFile);
 
 	// Test for each formula if a counterexample can be generated for it.
+	if(formulaList.size() == 0) {
+		LOG4CPLUS_ERROR(logger, "No PRCTL formula file specified.");
+		return;
+	}
+
 	for (auto formula : formulaList) {
 
 		// First check if it is a formula type for which a counterexample can be generated.
@@ -337,10 +303,10 @@ bool checkForCounterExampleGeneration(storm::property::prctl::AbstractPrctlFormu
 		}
 
 		//Generate counterexample
-		storm::counterexamples::PathBasedSubsystemGenerator<double>::computeCriticalSubsystem(*parser.getModel<storm::models::Dtmc<double>>(), stateForm);
+		storm::models::Dtmc<double> counterExample = storm::counterexamples::PathBasedSubsystemGenerator<double>::computeCriticalSubsystem(*parser.getModel<storm::models::Dtmc<double>>(), stateForm);
 
 		//Output counterexample
-		//TODO: Write output.
+		counterExample.printModelInformationToStream(std::cout);
 
 		delete formula;
 	}

src/utility/StormOptions.cpp

@@ -12,7 +12,7 @@ bool storm::utility::StormOptions::optionsRegistered = storm::settings::Settings
 	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "prctl", "", "Evaluates the PRCTL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("prctlFileName", "The path and name of the File to read PRCTL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
 	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "csl", "", "Evaluates the CSL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("cslFileName", "The path and name of the File to read CSL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
 	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "ltl", "", "Evaluates the LTL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("ltlFileName", "The path and name of the File to read LTL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
-	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "counterExample", "", "Generate a counterexample if given formula is not satisfied").build());
+	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "counterExample", "", "Generates a counterexample for the given formulas if not satisfied by the model").addArgument(storm::settings::ArgumentBuilder::createStringArgument("prctlFileName", "The path and name of the File to read the PRCTL Formulas to be used in \n\t\t\t\t\t\t the couterexample generation from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
 	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "transitionRewards", "", "If specified, the model will have these transition rewards").addArgument(storm::settings::ArgumentBuilder::createStringArgument("transitionRewardsFileName", "The path and name of the File to read the Transition Rewards from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
 	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "stateRewards", "", "If specified, the model will have these state rewards").addArgument(storm::settings::ArgumentBuilder::createStringArgument("stateRewardsFileName", "The path and name of the File to read the State Rewards from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
 	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "fixDeadlocks", "", "Insert Self-Loops for States with no outgoing transitions").build());