diff --git a/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp b/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp index fa68468ec..84507912e 100644 --- a/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp +++ b/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp @@ -251,11 +251,17 @@ namespace storm { // More than one component std::vector 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::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 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::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()))); } diff --git a/src/storm.cpp b/src/storm.cpp index cd1ec951c..c95fd1338 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -20,6 +20,7 @@ #include #include #include +#include #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(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(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 std::list*> 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(endTime - startTime).count() << "ms." << std::endl; } } }