diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index b570bf50c..91fbb17e0 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -639,6 +639,7 @@ namespace storm { } predicates.back().push_back(initialExpression.changeManager(expressionManager).substitute(lastSubstitution)); + return std::make_pair(predicates, stepVariableToCopiedVariableMap); } @@ -649,11 +650,13 @@ namespace storm { boost::optional predicates; // Create solver and interpolation groups. + auto assertionStart = std::chrono::high_resolution_clock::now(); storm::solver::MathsatSmtSolver interpolatingSolver(interpolationManager, storm::solver::MathsatSmtSolver::Options(true, false, true)); uint64_t stepCounter = 0; auto traceIt = trace.rbegin(); auto traceIte = trace.rend(); for (; traceIt != traceIte; ++traceIt) { + auto iterationStart = std::chrono::high_resolution_clock::now(); auto const& step = *traceIt; interpolatingSolver.push(); @@ -661,15 +664,13 @@ namespace storm { for (auto const& predicate : step) { interpolatingSolver.add(predicate); } - storm::solver::SmtSolver::CheckResult result = interpolatingSolver.check(); - // If the result already became unsatisfiable - if (result == storm::solver::SmtSolver::CheckResult::Unsat) { - STORM_LOG_TRACE("Trace formula became unsatisfiable after step " << stepCounter << "."); - break; - } + auto iterationEnd = std::chrono::high_resolution_clock::now(); + STORM_LOG_TRACE("Asserting step of trace formula took " << std::chrono::duration_cast(iterationEnd - iterationStart).count() << "ms."); ++stepCounter; } + auto assertionEnd = std::chrono::high_resolution_clock::now(); + STORM_LOG_TRACE("Asserting trace formula until unsatisfiability took " << std::chrono::duration_cast(assertionEnd - assertionStart).count() << "ms."); // Now encode the trace as an SMT problem. storm::solver::SmtSolver::CheckResult result = interpolatingSolver.check(); @@ -691,7 +692,12 @@ namespace storm { STORM_LOG_TRACE("Trace formula is satisfiable, not using interpolation."); } auto end = std::chrono::high_resolution_clock::now(); - STORM_LOG_TRACE("Deriving predicates using interpolation from witness of size " << trace.size() << " took " << std::chrono::duration_cast(end - start).count() << "ms."); + + if (predicates) { + STORM_LOG_TRACE("Deriving predicates using interpolation from witness of size " << trace.size() << " took " << std::chrono::duration_cast(end - start).count() << "ms."); + } else { + STORM_LOG_TRACE("Tried deriving predicates using interpolation but failed in " << std::chrono::duration_cast(end - start).count() << "ms."); + } return predicates; } @@ -712,8 +718,11 @@ namespace storm { std::shared_ptr interpolationManager = abstractionInformation.getExpressionManager().clone(); // Build the trace of the most probable path in terms of which predicates hold in each step. + auto start = std::chrono::high_resolution_clock::now(); std::pair>, std::map> traceAndVariableSubstitution = buildTrace(*interpolationManager, game, symbolicMostProbablePathsResult.spanningTree, symbolicPivotStateResult.pivotState); - + auto end = std::chrono::high_resolution_clock::now(); + STORM_LOG_DEBUG("Building the trace and variable substitution for interpolation from symbolic most-probable paths result took " << std::chrono::duration_cast(end - start).count() << "ms."); + return storm::abstraction::derivePredicatesFromInterpolation(*interpolationManager, abstractionInformation, traceAndVariableSubstitution.first, traceAndVariableSubstitution.second); } @@ -725,8 +734,11 @@ namespace storm { std::shared_ptr interpolationManager = abstractionInformation.getExpressionManager().clone(); // Build the trace of the most probable path in terms of which predicates hold in each step. + auto start = std::chrono::high_resolution_clock::now(); std::pair>, std::map> traceAndVariableSubstitution = buildTrace(*interpolationManager, game, pivotStateResult, odd); - + auto end = std::chrono::high_resolution_clock::now(); + STORM_LOG_DEBUG("Building the trace and variable substitution for interpolation from explicit most-probable paths result took " << std::chrono::duration_cast(end - start).count() << "ms."); + return storm::abstraction::derivePredicatesFromInterpolation(*interpolationManager, abstractionInformation, traceAndVariableSubstitution.first, traceAndVariableSubstitution.second); } @@ -856,8 +868,6 @@ namespace storm { bool foundPivotState = false; ValueType pivotStateDeviation = storm::utility::zero(); auto const& player2Grouping = transitionMatrix.getRowGroupIndices(); - - uint64_t pivotStates = 0; while (!dijkstraQueue.empty()) { auto distanceStatePair = *dijkstraQueue.begin(); @@ -961,8 +971,6 @@ namespace storm { } } - std::cout << "found " << pivotStates << " pivots" << std::endl; - if (foundPivotState) { return result; } diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp index 507cde01a..091c3fe6d 100644 --- a/src/storm/builder/DdJaniModelBuilder.cpp +++ b/src/storm/builder/DdJaniModelBuilder.cpp @@ -1275,7 +1275,7 @@ namespace storm { // Finally treat the transient assignments. std::map> transientEdgeAssignments; if (!this->transientVariables.empty()) { - performTransientAssignments(edge.getAssignments().getTransientAssignments(), [this, &transientEdgeAssignments, &guard, &sourceLocationAndGuard] (storm::jani::Assignment const& assignment) { + performTransientAssignments(edge.getAssignments().getTransientAssignments(), [this, &transientEdgeAssignments, &sourceLocationAndGuard] (storm::jani::Assignment const& assignment) { transientEdgeAssignments[assignment.getExpressionVariable()] = sourceLocationAndGuard * this->variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression()); } ); } diff --git a/src/storm/modelchecker/exploration/SparseExplorationModelChecker.cpp b/src/storm/modelchecker/exploration/SparseExplorationModelChecker.cpp index c5dc5e036..73e880662 100644 --- a/src/storm/modelchecker/exploration/SparseExplorationModelChecker.cpp +++ b/src/storm/modelchecker/exploration/SparseExplorationModelChecker.cpp @@ -341,7 +341,7 @@ namespace storm { }); } else if (explorationInformation.useProbabilityHeuristic()) { std::transform(row.begin(), row.end(), probabilities.begin(), - [&bounds, &explorationInformation] (storm::storage::MatrixEntry const& entry) { + [] (storm::storage::MatrixEntry const& entry) { return entry.getValue(); }); } diff --git a/src/storm/solver/stateelimination/DynamicStatePriorityQueue.h b/src/storm/solver/stateelimination/DynamicStatePriorityQueue.h index 0ac38769d..4065ee265 100644 --- a/src/storm/solver/stateelimination/DynamicStatePriorityQueue.h +++ b/src/storm/solver/stateelimination/DynamicStatePriorityQueue.h @@ -17,7 +17,7 @@ namespace storm { namespace stateelimination { struct PriorityComparator { - bool operator()(std::pair const& first, std::pair const& second) { + bool operator()(std::pair const& first, std::pair const& second) const { return (first.second < second.second) || (first.second == second.second && first.first < second.first) ; } }; diff --git a/src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp b/src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp index 2a73744cf..6cbd57f09 100644 --- a/src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp @@ -419,7 +419,7 @@ namespace storm { // the sorting is over. Otherwise, this interferes with the data used in the sorting process. storm::storage::sparse::state_type originalBlockIndex = block.getBeginIndex(); auto split = this->partition.splitBlock(block, - [&weakStateLabels,&block,originalBlockIndex,this] (storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) { + [&weakStateLabels,originalBlockIndex,this] (storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) { return weakStateLabels[this->partition.getPosition(state1) - originalBlockIndex] < weakStateLabels[this->partition.getPosition(state2) - originalBlockIndex]; }, [this, &splitterQueue, &block] (bisimulation::Block& newBlock) { diff --git a/src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp b/src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp index 473ae556a..019ec40c2 100644 --- a/src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp +++ b/src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp @@ -367,7 +367,7 @@ namespace storm { bool result = quotientDistributionsLess(state1, state2); return result; }, - [this, &block, &splitterQueue, &newBlocks] (Block& newBlock) { + [&newBlocks] (Block& newBlock) { newBlocks.push_back(&newBlock); }); diff --git a/src/storm/storage/jani/ParallelComposition.cpp b/src/storm/storage/jani/ParallelComposition.cpp index d81db1d91..0d439e0ce 100644 --- a/src/storm/storage/jani/ParallelComposition.cpp +++ b/src/storm/storage/jani/ParallelComposition.cpp @@ -116,7 +116,7 @@ namespace storm { return !(vector1 == vector2); } - bool SynchronizationVectorLexicographicalLess::operator()(SynchronizationVector const& vector1, SynchronizationVector const& vector2) { + bool SynchronizationVectorLexicographicalLess::operator()(SynchronizationVector const& vector1, SynchronizationVector const& vector2) const { STORM_LOG_THROW(vector1.size() == vector2.size(), storm::exceptions::WrongFormatException, "Cannot compare synchronization vectors of different size."); for (uint64_t i = 0; i < vector1.size(); ++i) { if (vector1.getInput(i) < vector2.getInput(i)) { diff --git a/src/storm/storage/jani/ParallelComposition.h b/src/storm/storage/jani/ParallelComposition.h index c3d41717c..381ace5f8 100644 --- a/src/storm/storage/jani/ParallelComposition.h +++ b/src/storm/storage/jani/ParallelComposition.h @@ -62,7 +62,7 @@ namespace storm { bool operator!=(SynchronizationVector const& vector1, SynchronizationVector const& vector2); struct SynchronizationVectorLexicographicalLess { - bool operator()(SynchronizationVector const& vector1, SynchronizationVector const& vector2); + bool operator()(SynchronizationVector const& vector1, SynchronizationVector const& vector2) const; }; std::ostream& operator<<(std::ostream& stream, SynchronizationVector const& synchronizationVector);