From 18f314d7c660f1619ac074ce0893e8dc32ff6de5 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 29 Jan 2015 18:19:09 +0100 Subject: [PATCH] Some more bugfixes. Damn you, clang on Mac OS! Former-commit-id: 86a7230a6183e910460bf3b3f7c7a29a077c0982 --- src/counterexamples/SMTMinimalCommandSetGenerator.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index fcb0aff94..1300b6efc 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -1693,7 +1693,7 @@ namespace storm { storm::models::Mdp subMdp = labeledMdp.restrictChoiceLabels(commandSet); storm::modelchecker::SparseMdpPrctlModelChecker modelchecker(subMdp); LOG4CPLUS_DEBUG(logger, "Invoking model checker."); - std::vector result = modelchecker.computeUntilProbabilitiesHelper(false, phiStates, psiStates, false) + std::vector result = modelchecker.computeUntilProbabilitiesHelper(false, phiStates, psiStates, false); LOG4CPLUS_DEBUG(logger, "Computed model checking results."); totalModelCheckingTime += std::chrono::high_resolution_clock::now() - modelCheckingClock; @@ -1786,10 +1786,10 @@ namespace storm { std::unique_ptr subResult = modelchecker.check(eventuallyFormula.getSubformula()); - storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult.asExplicitQualitativeCheckResult(); + storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult->asExplicitQualitativeCheckResult(); phiStates = storm::storage::BitVector(labeledMdp.getNumberOfStates(), true); - psiStates = subResult->getTruthValuesVector(); + psiStates = subQualitativeResult.getTruthValuesVector(); } // Delegate the actual computation work to the function of equal name.