Added timing for PRCTL formula checking.

Replaced std::sort with std::inplace_merge, saving another factor 2.


Former-commit-id: 961c31bb68

src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp

@@ -251,11 +251,17 @@ namespace storm {
 								// More than one component
 								std::vector<uint_fast64_t> tempGroups;
 								tempGroups.reserve(neededReserveSize);
-								for (size_t j = startIndex; j < i; ++j) {
+
+								// Copy the first group to make inplace_merge possible
+								storm::storage::StateBlock const& scc_first = sccDecomposition[topologicalSort[startIndex]];
+								tempGroups.insert(tempGroups.cend(), scc_first.cbegin(), scc_first.cend());
+
+								for (size_t j = startIndex + 1; j < i; ++j) {
 									storm::storage::StateBlock const& scc = sccDecomposition[topologicalSort[j]];
+									std::vector<uint_fast64_t>::iterator const middleIterator = tempGroups.end();
 									tempGroups.insert(tempGroups.cend(), scc.cbegin(), scc.cend());
+									std::inplace_merge(tempGroups.begin(), middleIterator, tempGroups.end());
 								}
-								std::sort(tempGroups.begin(), tempGroups.end());
 
 								result.push_back(std::make_pair(true, storm::storage::StateBlock(boost::container::ordered_unique_range, tempGroups.cbegin(), tempGroups.cend())));
 							} else {
@@ -287,11 +293,17 @@ namespace storm {
 						// More than one component
 						std::vector<uint_fast64_t> tempGroups;
 						tempGroups.reserve(neededReserveSize);
-						for (size_t j = startIndex; j < topologicalSortSize; ++j) {
+						
+						// Copy the first group to make inplace_merge possible
+						storm::storage::StateBlock const& scc_first = sccDecomposition[topologicalSort[startIndex]];
+						tempGroups.insert(tempGroups.cend(), scc_first.cbegin(), scc_first.cend());
+
+						for (size_t j = startIndex + 1; j < topologicalSort.size(); ++j) {
 							storm::storage::StateBlock const& scc = sccDecomposition[topologicalSort[j]];
+							std::vector<uint_fast64_t>::iterator const middleIterator = tempGroups.end();
 							tempGroups.insert(tempGroups.cend(), scc.cbegin(), scc.cend());
+							std::inplace_merge(tempGroups.begin(), middleIterator, tempGroups.end());
 						}
-						std::sort(tempGroups.begin(), tempGroups.end());
 
 						result.push_back(std::make_pair(true, storm::storage::StateBlock(boost::container::ordered_unique_range, tempGroups.cbegin(), tempGroups.cend())));
 					}

src/storm.cpp

@@ -20,6 +20,7 @@
 #include <climits>
 #include <sstream>
 #include <vector>
+#include <chrono>
 
 #include "storm-config.h"
 #include "src/models/Dtmc.h"
@@ -114,14 +115,14 @@ void printUsage() {
 	ULARGE_INTEGER uLargeInteger;
 	uLargeInteger.LowPart = ftKernel.dwLowDateTime;
 	uLargeInteger.HighPart = ftKernel.dwHighDateTime;
-	double kernelTime = uLargeInteger.QuadPart / 10000.0; // 100 ns Resolution to milliseconds
+	double kernelTime = static_cast<double>(uLargeInteger.QuadPart) / 10000.0; // 100 ns Resolution to milliseconds
 	uLargeInteger.LowPart = ftUser.dwLowDateTime;
 	uLargeInteger.HighPart = ftUser.dwHighDateTime;
-	double userTime = uLargeInteger.QuadPart / 10000.0;
+	double userTime = static_cast<double>(uLargeInteger.QuadPart) / 10000.0;
 
 	std::cout << "CPU Time: " << std::endl;
-	std::cout << "\tKernel Time: " << std::setprecision(3) << kernelTime << std::endl;
-	std::cout << "\tUser Time: " << std::setprecision(3) << userTime << std::endl;
+	std::cout << "\tKernel Time: " << std::setprecision(5) << kernelTime << std::endl;
+	std::cout << "\tUser Time: " << std::setprecision(5) << userTime << std::endl;
 #endif
 }
 
@@ -315,8 +316,11 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker<double>
 		std::list<storm::property::prctl::AbstractPrctlFormula<double>*> formulaList = storm::parser::PrctlFileParser(chosenPrctlFile);
         
         for (auto formula : formulaList) {
+			std::chrono::high_resolution_clock::time_point startTime = std::chrono::high_resolution_clock::now();
         	modelchecker.check(*formula);
             delete formula;
+			std::chrono::high_resolution_clock::time_point endTime = std::chrono::high_resolution_clock::now();
+			std::cout << "Checking the formula took " << std::chrono::duration_cast<std::chrono::milliseconds>(endTime - startTime).count() << "ms." << std::endl;
         }
 	}
 }