diff --git a/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp b/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp index 4cd5a37d4..830113f77 100644 --- a/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp +++ b/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp @@ -19,6 +19,7 @@ namespace storm { std::unique_ptr SparseDtmcInstantiationModelChecker::check(storm::utility::parametric::Valuation const& valuation) { STORM_LOG_THROW(this->currentCheckTask, storm::exceptions::InvalidStateException, "Checking has been invoked but no property has been specified before."); auto const& instantiatedModel = modelInstantiator.instantiate(valuation); + STORM_LOG_ASSERT(instantiatedModel.getTransitionMatrix().isProbabilistic(), "Instantiated matrix is not probabilistic!"); storm::modelchecker::SparseDtmcPrctlModelChecker> modelChecker(instantiatedModel); // Check if there are some optimizations implemented for the specified property @@ -28,7 +29,6 @@ namespace storm { return modelChecker.check(*this->currentCheckTask); } } - template std::unique_ptr SparseDtmcInstantiationModelChecker::checkWithHint(storm::modelchecker::SparseDtmcPrctlModelChecker>& modelchecker) { diff --git a/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp b/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp index 0e3fd482e..675218d71 100644 --- a/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp +++ b/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp @@ -20,6 +20,7 @@ namespace storm { std::unique_ptr SparseMdpInstantiationModelChecker::check(storm::utility::parametric::Valuation const& valuation) { STORM_LOG_THROW(this->currentCheckTask, storm::exceptions::InvalidStateException, "Checking has been invoked but no property has been specified before."); auto const& instantiatedModel = modelInstantiator.instantiate(valuation); + STORM_LOG_ASSERT(instantiatedModel.getTransitionMatrix().isProbabilistic(), "Instantiated matrix is not probabilistic!"); storm::modelchecker::SparseMdpPrctlModelChecker> modelChecker(instantiatedModel); // Check if there are some optimizations implemented for the specified property @@ -57,7 +58,7 @@ namespace storm { std::unique_ptr qualitativeResult = quantitativeResult->template asExplicitQuantitativeCheckResult().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs()); storm::storage::Scheduler& scheduler = quantitativeResult->template asExplicitQuantitativeCheckResult().getScheduler(); this->currentCheckTask->setHint(ExplicitModelCheckerHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult().getValueVector()), - std::move(dynamic_cast(scheduler)))); + std::move(dynamic_cast(scheduler)))); return qualitativeResult; } } diff --git a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp index bb862cd0a..227aea2eb 100644 --- a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp +++ b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp @@ -101,7 +101,7 @@ namespace storm { // if there are maybestates, create the parameterLifter if (!maybeStates.empty()) { // Create the vector of one-step probabilities to go to target states. - std::vector b = this->parametricModel.getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getRowCount(), true), psiStates); + std::vector b = this->parametricModel.getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getRowCount(), true), statesWithProbability01.second); parameterLifter = std::make_unique>(this->parametricModel.getTransitionMatrix(), b, this->parametricModel.getTransitionMatrix().getRowIndicesOfRowGroups(maybeStates), maybeStates); computePlayer1Matrix(); @@ -204,10 +204,10 @@ namespace storm { // Set up the solver auto solver = solverFactory->create(player1Matrix, parameterLifter->getMatrix()); - solver->setTrackScheduler(true); if(lowerResultBound) solver->setLowerBound(lowerResultBound.get()); if(upperResultBound) solver->setUpperBound(upperResultBound.get()); if(applyPreviousResultAsHint) { + solver->setTrackScheduler(true); x.resize(maybeStates.getNumberOfSetBits(), storm::utility::zero()); if(storm::solver::minimize(dirForParameters) && minSched && player1Sched) solver->setSchedulerHint(std::move(player1Sched.get()), std::move(minSched.get())); if(storm::solver::maximize(dirForParameters) && maxSched && player1Sched) solver->setSchedulerHint(std::move(player1Sched.get()), std::move(maxSched.get())); @@ -221,12 +221,14 @@ namespace storm { solver->repeatedMultiply(this->currentCheckTask->getOptimizationDirection(), dirForParameters, x, ¶meterLifter->getVector(), *stepBound); } else { solver->solveGame(this->currentCheckTask->getOptimizationDirection(), dirForParameters, x, parameterLifter->getVector()); - if(storm::solver::minimize(dirForParameters)) { - minSched = solver->getPlayer2Scheduler(); - } else { - maxSched = solver->getPlayer2Scheduler(); + if(applyPreviousResultAsHint) { + if(storm::solver::minimize(dirForParameters)) { + minSched = solver->getPlayer2Scheduler(); + } else { + maxSched = solver->getPlayer2Scheduler(); + } + player1Sched = solver->getPlayer1Scheduler(); } - player1Sched = solver->getPlayer1Scheduler(); } // Get the result for the complete model (including maybestates) diff --git a/src/storm/transformer/GoalStateMerger.cpp b/src/storm/transformer/GoalStateMerger.cpp index f7f7de439..5238404b9 100644 --- a/src/storm/transformer/GoalStateMerger.cpp +++ b/src/storm/transformer/GoalStateMerger.cpp @@ -77,9 +77,9 @@ namespace storm { bool sinkStateRequired = !originalModel.getInitialStates().isDisjointFrom(sinkStates); for( auto state : maybeStates) { resNumActions += origMatrix.getRowGroupSize(state); - bool hasTransitionToTarget(false), hasTransitionToSink(false); auto const& endOfRowGroup = origMatrix.getRowGroupIndices()[state+1]; for (uint_fast64_t row = origMatrix.getRowGroupIndices()[state]; row < endOfRowGroup; ++row) { + bool hasTransitionToTarget(false), hasTransitionToSink(false); for (auto const& entry : origMatrix.getRow(row)) { if(maybeStates.get(entry.getColumn())) { ++resNumTransitions; @@ -120,8 +120,6 @@ namespace storm { } - - template storm::storage::SparseMatrix GoalStateMerger::buildTransitionMatrix(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, boost::optional const& newTargetState, boost::optionalconst& newSinkState, storm::storage::SparseMatrixBuilder& builder) { @@ -138,9 +136,9 @@ namespace storm { uint_fast64_t currRow = 0; for (auto state : maybeStates) { builder.newRowGroup(currRow); - boost::optional targetProbability, sinkProbability; auto const& endOfRowGroup = origMatrix.getRowGroupIndices()[state+1]; for (uint_fast64_t row = origMatrix.getRowGroupIndices()[state]; row < endOfRowGroup; ++row) { + boost::optional targetProbability, sinkProbability; for (auto const& entry : origMatrix.getRow(row)) { if(maybeStates.get(entry.getColumn())) { builder.addNextValue(currRow, oldToNewIndexMap[entry.getColumn()], entry.getValue());