|
@ -156,7 +156,7 @@ namespace storm { |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
template<typename ValueType, bool Nondeterministic> |
|
|
template<typename ValueType, bool Nondeterministic> |
|
|
std::vector<ValueType> SparseLTLHelper<ValueType, Nondeterministic>::computeDAProductProbabilities(Environment const& env, storm::automata::DeterministicAutomaton const& da, std::map<std::string, storm::storage::BitVector>& apSatSets, bool qualitative) { |
|
|
|
|
|
|
|
|
std::vector<ValueType> SparseLTLHelper<ValueType, Nondeterministic>::computeDAProductProbabilities(Environment const& env, storm::automata::DeterministicAutomaton const& da, std::map<std::string, storm::storage::BitVector>& apSatSets) { |
|
|
const storm::automata::APSet& apSet = da.getAPSet(); |
|
|
const storm::automata::APSet& apSet = da.getAPSet(); |
|
|
|
|
|
|
|
|
std::vector<storm::storage::BitVector> apLabels; |
|
|
std::vector<storm::storage::BitVector> apLabels; |
|
@ -210,12 +210,12 @@ namespace storm { |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
if (acceptingStates.empty()) { |
|
|
if (acceptingStates.empty()) { |
|
|
STORM_LOG_INFO("No acceptingStates states, skipping probability computation."); |
|
|
|
|
|
|
|
|
STORM_LOG_INFO("No accepting states, skipping probability computation."); |
|
|
std::vector<ValueType> numericResult(this->_numberOfStates, storm::utility::zero<ValueType>()); |
|
|
std::vector<ValueType> numericResult(this->_numberOfStates, storm::utility::zero<ValueType>()); |
|
|
return numericResult; |
|
|
return numericResult; |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
STORM_LOG_INFO("Computing probabilities for reaching acceptingStates components..."); |
|
|
|
|
|
|
|
|
STORM_LOG_INFO("Computing probabilities for reaching accepting components..."); |
|
|
|
|
|
|
|
|
storm::storage::BitVector bvTrue(product->getProductModel().getNumberOfStates(), true); |
|
|
storm::storage::BitVector bvTrue(product->getProductModel().getNumberOfStates(), true); |
|
|
storm::storage::BitVector soiProduct(product->getStatesOfInterest()); |
|
|
storm::storage::BitVector soiProduct(product->getStatesOfInterest()); |
|
@ -231,6 +231,7 @@ namespace storm { |
|
|
|
|
|
|
|
|
std::vector<ValueType> prodNumericResult; |
|
|
std::vector<ValueType> prodNumericResult; |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
if (Nondeterministic) { |
|
|
if (Nondeterministic) { |
|
|
prodNumericResult = std::move(storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(env, |
|
|
prodNumericResult = std::move(storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(env, |
|
|
std::move(solveGoalProduct), |
|
|
std::move(solveGoalProduct), |
|
@ -238,7 +239,7 @@ namespace storm { |
|
|
product->getProductModel().getBackwardTransitions(), |
|
|
product->getProductModel().getBackwardTransitions(), |
|
|
bvTrue, |
|
|
bvTrue, |
|
|
acceptingStates, |
|
|
acceptingStates, |
|
|
qualitative, |
|
|
|
|
|
|
|
|
this->isQualitativeSet(), |
|
|
false // no schedulers (at the moment)
|
|
|
false // no schedulers (at the moment)
|
|
|
).values); |
|
|
).values); |
|
|
|
|
|
|
|
@ -249,7 +250,7 @@ namespace storm { |
|
|
product->getProductModel().getBackwardTransitions(), |
|
|
product->getProductModel().getBackwardTransitions(), |
|
|
bvTrue, |
|
|
bvTrue, |
|
|
acceptingStates, |
|
|
acceptingStates, |
|
|
qualitative); |
|
|
|
|
|
|
|
|
this->isQualitativeSet()); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
std::vector<ValueType> numericResult = product->projectToOriginalModel(this->_numberOfStates, prodNumericResult); |
|
|
std::vector<ValueType> numericResult = product->projectToOriginalModel(this->_numberOfStates, prodNumericResult); |
|
@ -281,7 +282,7 @@ namespace storm { |
|
|
<< *da->getAcceptance()->getAcceptanceExpression() << " as acceptance condition."); |
|
|
<< *da->getAcceptance()->getAcceptanceExpression() << " as acceptance condition."); |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
std::vector<ValueType> numericResult = computeDAProductProbabilities(env, *da, apSatSets, this->isQualitativeSet()); |
|
|
|
|
|
|
|
|
std::vector<ValueType> numericResult = computeDAProductProbabilities(env, *da, apSatSets); |
|
|
|
|
|
|
|
|
if(Nondeterministic && this->getOptimizationDirection()==OptimizationDirection::Minimize) { |
|
|
if(Nondeterministic && this->getOptimizationDirection()==OptimizationDirection::Minimize) { |
|
|
// compute 1-Pmax[!fomula]
|
|
|
// compute 1-Pmax[!fomula]
|
|
|