Minor bugfix in sparse matrix method to compute pointwise product.

Remove unnecessary small example files. Add reward files for synchronous leader example. Added test procedures to main (commented out by default) to check all of the three main models (crowds, die, synchronous leader).
12 years ago · 1561843cee
4 changed files with 132 additions and 43 deletions
--- a/src/modelChecker/DtmcPrctlModelChecker.h
+++ b/src/modelChecker/DtmcPrctlModelChecker.h
@ -102,16 +102,24 @@ public:
 		std::cout << std::endl;
 		LOG4CPLUS_INFO(logger, "Model checking formula\t" << stateFormula.toString());
 		std::cout << "Model checking formula:\t" << stateFormula.toString() << std::endl;
-		storm::storage::BitVector* result = stateFormula.check(*this);
-		LOG4CPLUS_INFO(logger, "Result for initial states:");
-		std::cout << "Result for initial states:" << std::endl;
-		for (auto initialState : *this->getModel().getLabeledStates("init")) {
-			LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result->get(initialState) ? "satisfied" : "not satisfied"));
-			std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl;
+		storm::storage::BitVector* result = nullptr;
+		try {
+			result = stateFormula.check(*this);
+			LOG4CPLUS_INFO(logger, "Result for initial states:");
+			std::cout << "Result for initial states:" << std::endl;
+			for (auto initialState : *this->getModel().getLabeledStates("init")) {
+				LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result->get(initialState) ? "satisfied" : "not satisfied"));
+				std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl;
+			}
+			delete result;
+		} catch (std::exception& e) {
+			std::cout << "Error during computation: " << e.what() << "Skipping property." << std::endl;
+			if (result != nullptr) {
+				delete result;
+			}
 		}
 		std::cout << std::endl;
 		storm::utility::printSeparationLine(std::cout);
-		delete result;
 	}

 	/*!
@ -123,16 +131,24 @@ public:
 		std::cout << std::endl;
 		LOG4CPLUS_INFO(logger, "Model checking formula\t" << probabilisticNoBoundsFormula.toString());
 		std::cout << "Model checking formula:\t" << probabilisticNoBoundsFormula.toString() << std::endl;
-		std::vector<Type>* result = checkProbabilisticNoBoundsOperator(probabilisticNoBoundsFormula);
-		LOG4CPLUS_INFO(logger, "Result for initial states:");
-		std::cout << "Result for initial states:" << std::endl;
-		for (auto initialState : *this->getModel().getLabeledStates("init")) {
-			LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (*result)[initialState]);
-			std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl;
+		std::vector<Type>* result = nullptr;
+		try {
+			result = checkProbabilisticNoBoundsOperator(probabilisticNoBoundsFormula);
+			LOG4CPLUS_INFO(logger, "Result for initial states:");
+			std::cout << "Result for initial states:" << std::endl;
+			for (auto initialState : *this->getModel().getLabeledStates("init")) {
+				LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (*result)[initialState]);
+				std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl;
+			}
+			delete result;
+		} catch (std::exception& e) {
+			std::cout << "Error during computation: " << e.what() << " Skipping property." << std::endl;
+			if (result != nullptr) {
+				delete result;
+			}
 		}
 		std::cout << std::endl;
 		storm::utility::printSeparationLine(std::cout);
-		delete result;
 	}

 	/*!
@ -144,16 +160,26 @@ public:
 		std::cout << std::endl;
 		LOG4CPLUS_INFO(logger, "Model checking formula\t" << rewardNoBoundsFormula.toString());
 		std::cout << "Model checking formula:\t" << rewardNoBoundsFormula.toString() << std::endl;
-		std::vector<Type>* result = checkRewardNoBoundsOperator(rewardNoBoundsFormula);
-		LOG4CPLUS_INFO(logger, "Result for initial states:");
-		std::cout << "Result for initial states:" << std::endl;
-		for (auto initialState : *this->getModel().getLabeledStates("init")) {
-			LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (*result)[initialState]);
-			std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl;
+		std::vector<Type>* result = nullptr;
+		try {
+			result = checkRewardNoBoundsOperator(rewardNoBoundsFormula);
+			LOG4CPLUS_INFO(logger, "Result for initial states:");
+			std::cout << "Result for initial states:" << std::endl;
+			for (auto initialState : *this->getModel().getLabeledStates("init")) {
+				LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (*result)[initialState]);
+				std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl;
+			}
+			std::cout << std::endl;
+			storm::utility::printSeparationLine(std::cout);
+			delete result;
+		} catch (std::exception& e) {
+			std::cout << "Error during computation: " << e.what() << " Skipping property." << std::endl;
+			if (result != nullptr) {
+				delete result;
+			}
 		}
 		std::cout << std::endl;
 		storm::utility::printSeparationLine(std::cout);
-		delete result;
 	}

 	/*!
--- a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h
+++ b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h
@ -241,7 +241,7 @@ public:
 	virtual std::vector<Type>* checkReachabilityReward(const storm::formula::ReachabilityReward<Type>& formula) const {
 		// Only compute the result if the model has at least one reward model.
 		if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) {
-			LOG4CPLUS_ERROR(logger, "Missing reward model for formula.");
+			LOG4CPLUS_ERROR(logger, "Missing reward model for formula. Skipping formula");
 			throw storm::exceptions::InvalidArgumentException() << "Missing reward model for formula.";
 		}

--- a/src/storage/SquareSparseMatrix.h
+++ b/src/storage/SquareSparseMatrix.h
@ -107,7 +107,7 @@ public:
 					// use T() to force use of the copy constructor for complex T types
 					valueStorage[i] = T(ssm.valueStorage[i]);
 				}
-				for (uint_fast64_t i = 0; i <= rowCount; ++i) {
+				for (uint_fast64_t i = 0; i < rowCount; ++i) {
 					// use T() to force use of the copy constructor for complex T types
 					diagonalStorage[i] = T(ssm.diagonalStorage[i]);
 				}
@ -843,15 +843,17 @@ public:
 		// Iterate over all elements of the current matrix and either continue with the next element
 		// in case the given matrix does not have a non-zero element at this column position, or
 		// multiply the two entries and add the result to the corresponding position in the vector.
-		uint_fast64_t otherRow = 0;
-		for (uint_fast64_t row = 0; row < rowCount; ++row) {
+		for (uint_fast64_t row = 0; row < rowCount && row < otherMatrix.rowCount; ++row) {
 			(*result)[row] += diagonalStorage[row] * otherMatrix.diagonalStorage[row];
-			for (uint_fast64_t element = otherMatrix.rowIndications[row], nextElement = rowIndications[row]; element < otherMatrix.rowIndications[row + 1]; ++element) {
-				if (otherMatrix.columnIndications[element] < columnIndications[nextElement]) {
+			for (uint_fast64_t element = rowIndications[row], nextOtherElement = otherMatrix.rowIndications[row]; element < rowIndications[row + 1] && nextOtherElement < otherMatrix.rowIndications[row + 1]; ++element) {
+				if (columnIndications[element] < otherMatrix.columnIndications[nextOtherElement]) {
 					continue;
 				} else {
-					(*result)[row] += otherMatrix.valueStorage[element] * valueStorage[nextElement];
-					++nextElement;
+					// If the precondition of this method (i.e. that the given matrix is a submatrix
+					// of the current one) was fulfilled, we know now that the two elements are in
+					// the same column, so we can multiply and add them to the row sum vector.
+					(*result)[row] += otherMatrix.valueStorage[element] * valueStorage[nextOtherElement];
+					++nextOtherElement;
 				}
 			}
 		}
--- a/src/storm.cpp
+++ b/src/storm.cpp
@ -138,25 +138,16 @@ void cleanUp() {
 	}
 }

-/*!
- * Simple testing procedure.
- */
-void testChecking() {
-	storm::settings::Settings* s = storm::settings::instance();
-	storm::parser::DtmcParser dtmcParser(s->getString("trafile"), s->getString("labfile"), s->getString("staterew"), s->getString("transrew"));
-	std::shared_ptr<storm::models::Dtmc<double>> dtmc = dtmcParser.getDtmc();
-
-	dtmc->printModelInformationToStream(std::cout);
-
-	storm::formula::Ap<double>* observe0Greater1Formula = new storm::formula::Ap<double>("one");
-	storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(observe0Greater1Formula);
+void testCheckingDie(storm::models::Dtmc<double>& dtmc) {
+	storm::formula::Ap<double>* oneFormula = new storm::formula::Ap<double>("one");
+	storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(oneFormula);
 	storm::formula::ProbabilisticNoBoundsOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundsOperator<double>(eventuallyFormula);

 	storm::formula::Ap<double>* done = new storm::formula::Ap<double>("done");
 	storm::formula::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(done);
 	storm::formula::RewardNoBoundsOperator<double>* rewardFormula = new storm::formula::RewardNoBoundsOperator<double>(reachabilityRewardFormula);

-	storm::modelChecker::GmmxxDtmcPrctlModelChecker<double>* mc = new storm::modelChecker::GmmxxDtmcPrctlModelChecker<double>(*dtmc);
+	storm::modelChecker::GmmxxDtmcPrctlModelChecker<double>* mc = new storm::modelChecker::GmmxxDtmcPrctlModelChecker<double>(dtmc);
 	mc->check(*probFormula);
 	mc->check(*rewardFormula);

@ -165,6 +156,76 @@ void testChecking() {
 	delete rewardFormula;
 }

+void testCheckingCrowds(storm::models::Dtmc<double>& dtmc) {
+	storm::formula::Ap<double>* observe0Greater1Formula = new storm::formula::Ap<double>("observe0Greater1");
+	storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(observe0Greater1Formula);
+	storm::formula::ProbabilisticNoBoundsOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundsOperator<double>(eventuallyFormula);
+
+	storm::modelChecker::GmmxxDtmcPrctlModelChecker<double>* mc = new storm::modelChecker::GmmxxDtmcPrctlModelChecker<double>(dtmc);
+	mc->check(*probFormula);
+	delete probFormula;
+
+	storm::formula::Ap<double>* observeIGreater1Formula = new storm::formula::Ap<double>("observeIGreater1");
+	eventuallyFormula = new storm::formula::Eventually<double>(observeIGreater1Formula);
+	probFormula = new storm::formula::ProbabilisticNoBoundsOperator<double>(eventuallyFormula);
+
+	mc->check(*probFormula);
+	delete probFormula;
+
+	storm::formula::Ap<double>* observeOnlyTrueSenderFormula = new storm::formula::Ap<double>("observeOnlyTrueSender");
+	eventuallyFormula = new storm::formula::Eventually<double>(observeOnlyTrueSenderFormula);
+	probFormula = new storm::formula::ProbabilisticNoBoundsOperator<double>(eventuallyFormula);
+
+	mc->check(*probFormula);
+	delete probFormula;
+
+	delete mc;
+}
+
+void testCheckingSynchronousLeader(storm::models::Dtmc<double>& dtmc, uint_fast64_t n) {
+	storm::formula::Ap<double>* electedFormula = new storm::formula::Ap<double>("elected");
+	storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(electedFormula);
+	storm::formula::ProbabilisticNoBoundsOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundsOperator<double>(eventuallyFormula);
+
+	storm::modelChecker::GmmxxDtmcPrctlModelChecker<double>* mc = new storm::modelChecker::GmmxxDtmcPrctlModelChecker<double>(dtmc);
+	mc->check(*probFormula);
+	delete probFormula;
+
+	electedFormula = new storm::formula::Ap<double>("elected");
+	storm::formula::BoundedUntil<double>* boundedUntilFormula = new storm::formula::BoundedUntil<double>(new storm::formula::Ap<double>("true"), electedFormula, 1);
+	probFormula = new storm::formula::ProbabilisticNoBoundsOperator<double>(boundedUntilFormula);
+
+	for (uint_fast64_t L = 1; L < 5; ++L) {
+		boundedUntilFormula->setBound(L*(n + 1));
+		mc->check(*probFormula);
+	}
+	delete probFormula;
+
+	electedFormula = new storm::formula::Ap<double>("elected");
+	storm::formula::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(electedFormula);
+	storm::formula::RewardNoBoundsOperator<double>* rewardFormula = new storm::formula::RewardNoBoundsOperator<double>(reachabilityRewardFormula);
+
+	mc->check(*rewardFormula);
+	delete rewardFormula;
+
+	delete mc;
+}
+
+/*!
+ * Simple testing procedure.
+ */
+void testChecking() {
+	storm::settings::Settings* s = storm::settings::instance();
+	storm::parser::DtmcParser dtmcParser(s->getString("trafile"), s->getString("labfile"), s->getString("staterew"), s->getString("transrew"));
+	std::shared_ptr<storm::models::Dtmc<double>> dtmc = dtmcParser.getDtmc();
+
+	dtmc->printModelInformationToStream(std::cout);
+
+	// testCheckingDie(*dtmc);
+	// testCheckingCrowds(*dtmc);
+	// testCheckingSynchronousLeader(*dtmc, 4);
+}
+
 /*!
 * Main entry point.
 */
@ -175,7 +236,7 @@ int main(const int argc, const char* argv[]) {
 	}
 	printHeader(argc, argv);

-	// testChecking();
+	testChecking();

 	cleanUp();
 	return 0;