sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Working towards reachability reward properties for parametric DTMCs. 

Former-commit-id: addf59ca34
tempestpy_adaptions
dehnert 10 years ago
parent
edfbfaa924
commit
3a18d60925
3 changed files with 91 additions and 139 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 207
      src/modelchecker/reachability/SparseSccModelChecker.cpp
  2. 15
      src/modelchecker/reachability/SparseSccModelChecker.h
  3. 8
      src/stormParametric.cpp

207
src/modelchecker/reachability/SparseSccModelChecker.cpp
View File

@ -17,7 +17,7 @@ namespace storm {
namespace reachability {
template<typename ValueType>
ValueType SparseSccModelChecker<ValueType>::computeReachabilityProbability(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional<std::vector<std::size_t>> const& statePriorities) {
ValueType SparseSccModelChecker<ValueType>::computeReachabilityValue(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional<std::vector<ValueType>>& stateRewards, boost::optional<std::vector<std::size_t>> const& statePriorities) {
std::chrono::high_resolution_clock::time_point totalTimeStart = std::chrono::high_resolution_clock::now();
std::chrono::high_resolution_clock::time_point conversionStart = std::chrono::high_resolution_clock::now();
@ -45,7 +45,7 @@ namespace storm {
STORM_PRINT_AND_LOG("Eliminating " << states.size() << " states using the state elimination technique." << std::endl);
for (auto const& state : states) {
eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions);
eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions, stateRewards);
}
STORM_PRINT_AND_LOG("Eliminated " << states.size() << " states." << std::endl);
} else if (storm::settings::parametricSettings().getEliminationMethod() == storm::settings::modules::ParametricSettings::EliminationMethod::Hybrid) {
@ -53,13 +53,13 @@ namespace storm {
storm::utility::ConstantsComparator<ValueType> comparator;
std::vector<storm::storage::sparse::state_type> entryStateQueue;
STORM_PRINT_AND_LOG("Eliminating " << subsystem.size() << " states using the hybrid elimination technique." << std::endl);
maximalDepth = treatScc(flexibleMatrix, oneStepProbabilities, initialStates, subsystem, transitionMatrix, flexibleBackwardTransitions, false, 0, storm::settings::parametricSettings().getMaximalSccSize(), entryStateQueue, comparator, statePriorities);
maximalDepth = treatScc(flexibleMatrix, oneStepProbabilities, initialStates, subsystem, transitionMatrix, flexibleBackwardTransitions, false, 0, storm::settings::parametricSettings().getMaximalSccSize(), entryStateQueue, comparator, stateRewards, statePriorities);
// If the entry states were to be eliminated last, we need to do so now.
STORM_LOG_DEBUG("Eliminating " << entryStateQueue.size() << " entry states as a last step.");
if (storm::settings::parametricSettings().isEliminateEntryStatesLastSet()) {
for (auto const& state : entryStateQueue) {
eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions);
eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions, stateRewards);
}
}
STORM_PRINT_AND_LOG("Eliminated " << subsystem.size() << " states." << std::endl);
@ -67,7 +67,7 @@ namespace storm {
// Finally eliminate initial state.
STORM_PRINT_AND_LOG("Eliminating initial state " << *initialStates.begin() << "." << std::endl);
eliminateState(flexibleMatrix, oneStepProbabilities, *initialStates.begin(), flexibleBackwardTransitions);
eliminateState(flexibleMatrix, oneStepProbabilities, *initialStates.begin(), flexibleBackwardTransitions, stateRewards);
// Make sure that we have eliminated all transitions from the initial state.
STORM_LOG_ASSERT(flexibleMatrix.getRow(*initialStates.begin()).empty(), "The transitions of the initial states are non-empty.");
@ -101,38 +101,59 @@ namespace storm {
return storm::utility::simplify(oneStepProbabilities[*initialStates.begin()]);
}
// template<typename ValueType>
// ValueType SparseSccModelChecker<ValueType>::computeReachabilityReward(storm::models::Dtmc<ValueType> const& dtmc, std::shared_ptr<storm::properties::prctl::Ap<double>> const& phiFormula, std::shared_ptr<storm::properties::prctl::Ap<double>> const& psiFormula) {
// // Now retrieve the appropriate bitvectors from the atomic propositions.
// storm::storage::BitVector phiStates = phiFormula->getAp() != "true" ? dtmc.getLabeledStates(phiFormula->getAp()) : storm::storage::BitVector(dtmc.getNumberOfStates(), true);
// storm::storage::BitVector psiStates = dtmc.getLabeledStates(psiFormula->getAp());
//
// // Do some sanity checks to establish some required properties.
// STORM_LOG_THROW(!dtmc.hasTransitionRewards(), storm::exceptions::IllegalArgumentException, "Input model does have transition-based rewards, which are currently unsupported.");
// STORM_LOG_THROW(dtmc.hasStateRewards(), storm::exceptions::IllegalArgumentException, "Input model does not have a state-based reward model.");
// STORM_LOG_THROW(dtmc.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state.");
//
// // Then, compute the subset of states that has a reachability reward less than infinity.
// storm::storage::BitVector trueStates(dtmc.getNumberOfStates(), true);
// storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(dtmc.getBackwardTransitions(), trueStates, psiStates);
// infinityStates.complement();
// storm::storage::BitVector maybeStates = ~psiStates & ~infinityStates;
//
// // If the initial state is known to have 0 reward or an infinite reward value, we can directly return the result.
// STORM_LOG_THROW(dtmc.getInitialStates().isDisjointFrom(infinityStates), storm::exceptions::IllegalArgumentException, "Initial state has infinite reward.");
// if (!dtmc.getInitialStates().isDisjointFrom(psiStates)) {
// STORM_LOG_DEBUG("The reward of all initial states was found in a preprocessing step.");
// return storm::utility::constantZero<ValueType>();
// }
//
// // Determine the set of states that is reachable from the initial state without jumping over a target state.
// storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(dtmc.getTransitionMatrix(), dtmc.getInitialStates(), maybeStates, psiStates);
//
// // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state).
// maybeStates &= reachableStates;
//
//
// }
template<typename ValueType>
ValueType SparseSccModelChecker<ValueType>::computeReachabilityReward(storm::models::Dtmc<ValueType> const& dtmc, std::shared_ptr<storm::properties::prctl::Ap<double>> const& phiFormula, std::shared_ptr<storm::properties::prctl::Ap<double>> const& psiFormula) {
// Now retrieve the appropriate bitvectors from the atomic propositions.
storm::storage::BitVector phiStates = phiFormula->getAp() != "true" ? dtmc.getLabeledStates(phiFormula->getAp()) : storm::storage::BitVector(dtmc.getNumberOfStates(), true);
storm::storage::BitVector psiStates = dtmc.getLabeledStates(psiFormula->getAp());
// Do some sanity checks to establish some required properties.
STORM_LOG_THROW(!dtmc.hasTransitionRewards(), storm::exceptions::IllegalArgumentException, "Input model does have transition-based rewards, which are currently unsupported.");
STORM_LOG_THROW(dtmc.hasStateRewards(), storm::exceptions::IllegalArgumentException, "Input model does not have a state-based reward model.");
STORM_LOG_THROW(dtmc.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state.");
// Then, compute the subset of states that has a reachability reward less than infinity.
storm::storage::BitVector trueStates(dtmc.getNumberOfStates(), true);
storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(dtmc.getBackwardTransitions(), trueStates, psiStates);
infinityStates.complement();
storm::storage::BitVector maybeStates = ~psiStates & ~infinityStates;
// If the initial state is known to have 0 reward or an infinite reward value, we can directly return the result.
STORM_LOG_THROW(dtmc.getInitialStates().isDisjointFrom(infinityStates), storm::exceptions::IllegalArgumentException, "Initial state has infinite reward.");
if (!dtmc.getInitialStates().isDisjointFrom(psiStates)) {
STORM_LOG_DEBUG("The reward of all initial states was found in a preprocessing step.");
return storm::utility::constantZero<ValueType>();
}
// Determine the set of states that is reachable from the initial state without jumping over a target state.
storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(dtmc.getTransitionMatrix(), dtmc.getInitialStates(), maybeStates, psiStates);
// Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state).
maybeStates &= reachableStates;
// Create a vector for the probabilities to go to a state with probability 1 in one step.
std::vector<ValueType> oneStepProbabilities = dtmc.getTransitionMatrix().getConstrainedRowSumVector(maybeStates, psiStates);
// Create a vector that holds the one-step rewards.
std::vector<ValueType> oneStepRewards = std::vector<ValueType>(maybeStates.getNumberOfSetBits(), storm::utility::zero<ValueType>());
// Project the state reward vector to all maybe-states.
boost::optional<std::vector<ValueType>> stateRewards(maybeStates.getNumberOfSetBits());
storm::utility::vector::selectVectorValues(stateRewards.get(), maybeStates, dtmc.getStateRewardVector());
// Determine the set of initial states of the sub-DTMC.
storm::storage::BitVector newInitialStates = dtmc.getInitialStates() % maybeStates;
// We then build the submatrix that only has the transitions of the maybe states.
storm::storage::SparseMatrix<ValueType> submatrix = dtmc.getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates);
storm::storage::SparseMatrix<ValueType> submatrixTransposed = submatrix.transpose();
// Before starting the model checking process, we assign priorities to states so we can use them to
// impose ordering constraints later.
std::vector<std::size_t> statePriorities = getStatePriorities(submatrix, submatrixTransposed, newInitialStates, oneStepProbabilities);
return computeReachabilityValue(submatrix, oneStepRewards, submatrixTransposed, newInitialStates, phiStates, psiStates, stateRewards, statePriorities);
}
template<typename ValueType>
ValueType SparseSccModelChecker<ValueType>::computeReachabilityProbability(storm::models::Dtmc<ValueType> const& dtmc, std::shared_ptr<storm::properties::prctl::Ap<double>> const& phiFormula, std::shared_ptr<storm::properties::prctl::Ap<double>> const& psiFormula) {
@ -173,8 +194,16 @@ namespace storm {
// Before starting the model checking process, we assign priorities to states so we can use them to
// impose ordering constraints later.
std::vector<std::size_t> statePriorities(submatrix.getRowCount());
std::vector<std::size_t> states(submatrix.getRowCount());
std::vector<std::size_t> statePriorities = getStatePriorities(submatrix, submatrixTransposed, newInitialStates, oneStepProbabilities);
boost::optional<std::vector<ValueType>> missingStateRewards;
return computeReachabilityValue(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, phiStates, psiStates, missingStateRewards, statePriorities);
}
template<typename ValueType>
std::vector<std::size_t> SparseSccModelChecker<ValueType>::getStatePriorities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector<ValueType> const& oneStepProbabilities) {
std::vector<std::size_t> statePriorities(transitionMatrix.getRowCount());
std::vector<std::size_t> states(transitionMatrix.getRowCount());
for (std::size_t index = 0; index < states.size(); ++index) {
states[index] = index;
}
@ -183,19 +212,19 @@ namespace storm {
} else {
std::vector<std::size_t> distances;
if (storm::settings::parametricSettings().getEliminationOrder() == storm::settings::modules::ParametricSettings::EliminationOrder::Forward || storm::settings::parametricSettings().getEliminationOrder() == storm::settings::modules::ParametricSettings::EliminationOrder::ForwardReversed) {
distances = storm::utility::graph::getDistances(submatrix, newInitialStates);
distances = storm::utility::graph::getDistances(transitionMatrix, initialStates);
} else if (storm::settings::parametricSettings().getEliminationOrder() == storm::settings::modules::ParametricSettings::EliminationOrder::Backward || storm::settings::parametricSettings().getEliminationOrder() == storm::settings::modules::ParametricSettings::EliminationOrder::BackwardReversed) {
// Since the target states were eliminated from the matrix already, we construct a replacement by
// treating all states that have some non-zero probability to go to a target state in one step.
storm::utility::ConstantsComparator<ValueType> comparator;
storm::storage::BitVector pseudoTargetStates(submatrix.getRowCount());
storm::storage::BitVector pseudoTargetStates(transitionMatrix.getRowCount());
for (std::size_t index = 0; index < oneStepProbabilities.size(); ++index) {
if (!comparator.isZero(oneStepProbabilities[index])) {
pseudoTargetStates.set(index);
}
}
distances = storm::utility::graph::getDistances(submatrixTransposed, pseudoTargetStates);
distances = storm::utility::graph::getDistances(transitionMatrixTransposed, pseudoTargetStates);
} else {
STORM_LOG_ASSERT(false, "Illegal sorting order selected.");
}
@ -214,7 +243,7 @@ namespace storm {
statePriorities[states[index]] = index;
}
return computeReachabilityProbability(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, phiStates, psiStates, statePriorities);
return statePriorities;
}
template<typename ValueType>
@ -232,7 +261,7 @@ namespace storm {
}
template<typename ValueType>
uint_fast64_t SparseSccModelChecker<ValueType>::treatScc(FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, FlexibleSparseMatrix<ValueType>& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector<storm::storage::sparse::state_type>& entryStateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator, boost::optional<std::vector<std::size_t>> const& statePriorities) {
uint_fast64_t SparseSccModelChecker<ValueType>::treatScc(FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, FlexibleSparseMatrix<ValueType>& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector<storm::storage::sparse::state_type>& entryStateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator, boost::optional<std::vector<ValueType>>& stateRewards, boost::optional<std::vector<std::size_t>> const& statePriorities) {
uint_fast64_t maximalDepth = level;
// If the SCCs are large enough, we try to split them further.
@ -264,7 +293,7 @@ namespace storm {
STORM_LOG_DEBUG("Eliminating " << trivialSccs.size() << " trivial SCCs.");
for (auto const& stateIndexPair : trivialSccs) {
eliminateState(matrix, oneStepProbabilities, stateIndexPair.first, backwardTransitions);
eliminateState(matrix, oneStepProbabilities, stateIndexPair.first, backwardTransitions, stateRewards);
remainingSccs.set(stateIndexPair.second, false);
}
STORM_LOG_DEBUG("Eliminated all trivial SCCs.");
@ -288,7 +317,7 @@ namespace storm {
}
// Recursively descend in SCC-hierarchy.
uint_fast64_t depth = treatScc(matrix, oneStepProbabilities, entryStates, newSccAsBitVector, forwardTransitions, backwardTransitions, !storm::settings::parametricSettings().isEliminateEntryStatesLastSet(), level + 1, maximalSccSize, entryStateQueue, comparator, statePriorities);
uint_fast64_t depth = treatScc(matrix, oneStepProbabilities, entryStates, newSccAsBitVector, forwardTransitions, backwardTransitions, !storm::settings::parametricSettings().isEliminateEntryStatesLastSet(), level + 1, maximalSccSize, entryStateQueue, comparator, stateRewards, statePriorities);
maximalDepth = std::max(maximalDepth, depth);
}
@ -307,7 +336,7 @@ namespace storm {
// Eliminate the remaining states that do not have a self-loop (in the current, i.e. modified)
// transition probability matrix.
for (auto const& state : states) {
eliminateState(matrix, oneStepProbabilities, state, backwardTransitions);
eliminateState(matrix, oneStepProbabilities, state, backwardTransitions, stateRewards);
}
STORM_LOG_DEBUG("Eliminated all states of SCC.");
@ -317,7 +346,7 @@ namespace storm {
if (eliminateEntryStates) {
STORM_LOG_DEBUG("Finally, eliminating/adding entry states.");
for (auto state : entryStates) {
eliminateState(matrix, oneStepProbabilities, state, backwardTransitions);
eliminateState(matrix, oneStepProbabilities, state, backwardTransitions, stateRewards);
}
STORM_LOG_DEBUG("Eliminated/added entry states.");
} else {
@ -335,7 +364,7 @@ namespace storm {
}
template<typename ValueType>
void SparseSccModelChecker<ValueType>::eliminateState(FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix<ValueType>& backwardTransitions) {
void SparseSccModelChecker<ValueType>::eliminateState(FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix<ValueType>& backwardTransitions, boost::optional<std::vector<ValueType>>& stateRewards) {
auto eliminationStart = std::chrono::high_resolution_clock::now();
++counter;
@ -513,86 +542,6 @@ namespace storm {
auto eliminationTime = eliminationEnd - eliminationStart;
}
template <typename ValueType>
bool SparseSccModelChecker<ValueType>::eliminateStateInPlace(storm::storage::SparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, storm::storage::SparseMatrix<ValueType>& backwardTransitions) {
typename storm::storage::SparseMatrix<ValueType>::iterator forwardElement = matrix.getRow(state).begin();
typename storm::storage::SparseMatrix<ValueType>::iterator backwardElement = backwardTransitions.getRow(state).begin();
if (forwardElement->getValue() != storm::utility::constantOne<ValueType>() || backwardElement->getValue() != storm::utility::constantOne<ValueType>()) {
return false;
}
std::cout << "eliminating " << state << std::endl;
std::cout << "fwd element: " << *forwardElement << " and bwd element: " << *backwardElement << std::endl;
// Find the element of the predecessor that moves to the state that we want to eliminate.
typename storm::storage::SparseMatrix<ValueType>::rows forwardRow = matrix.getRow(backwardElement->getColumn());
typename storm::storage::SparseMatrix<ValueType>::iterator multiplyElement = std::find_if(forwardRow.begin(), forwardRow.end(), [&](storm::storage::MatrixEntry<typename storm::storage::SparseMatrix<ValueType>::index_type, typename storm::storage::SparseMatrix<ValueType>::value_type> const& a) { return a.getColumn() == state; });
std::cout << "before fwd: " << std::endl;
for (auto element : matrix.getRow(backwardElement->getColumn())) {
std::cout << element << ", " << std::endl;
}
// Modify the forward probability entry of the predecessor.
multiplyElement->setValue(multiplyElement->getValue() * forwardElement->getValue());
multiplyElement->setColumn(forwardElement->getColumn());
// Modify the one-step probability for the predecessor if necessary.
if (oneStepProbabilities[state] != storm::utility::constantZero<ValueType>()) {
oneStepProbabilities[backwardElement->getColumn()] += multiplyElement->getValue() * oneStepProbabilities[state];
}
// If the forward entry is not at the right position, we need to move it there.
if (multiplyElement != forwardRow.begin() && multiplyElement->getColumn() < (multiplyElement - 1)->getColumn()) {
while (multiplyElement != forwardRow.begin() && multiplyElement->getColumn() < (multiplyElement - 1)->getColumn()) {
std::swap(*multiplyElement, *(multiplyElement - 1));
--multiplyElement;
}
} else if ((multiplyElement + 1) != forwardRow.end() && multiplyElement->getColumn() > (multiplyElement + 1)->getColumn()) {
while ((multiplyElement + 1) != forwardRow.end() && multiplyElement->getColumn() > (multiplyElement + 1)->getColumn()) {
std::swap(*multiplyElement, *(multiplyElement + 1));
++multiplyElement;
}
}
std::cout << "after fwd: " << std::endl;
for (auto element : matrix.getRow(backwardElement->getColumn())) {
std::cout << element << ", " << std::endl;
}
// Find the backward element of the successor that moves to the state that we want to eliminate.
typename storm::storage::SparseMatrix<ValueType>::rows backwardRow = backwardTransitions.getRow(forwardElement->getColumn());
typename storm::storage::SparseMatrix<ValueType>::iterator backwardEntry = std::find_if(backwardRow.begin(), backwardRow.end(), [&](storm::storage::MatrixEntry<typename storm::storage::SparseMatrix<ValueType>::index_type, typename storm::storage::SparseMatrix<ValueType>::value_type> const& a) { return a.getColumn() == state; });
std::cout << "before bwd" << std::endl;
for (auto element : backwardTransitions.getRow(forwardElement->getColumn())) {
std::cout << element << ", " << std::endl;
}
// Modify the predecessor list of the successor and add the predecessor of the state we eliminate.
backwardEntry->setColumn(backwardElement->getColumn());
// If the backward entry is not at the right position, we need to move it there.
if (backwardEntry != backwardRow.begin() && backwardEntry->getColumn() < (backwardEntry - 1)->getColumn()) {
while (backwardEntry != backwardRow.begin() && backwardEntry->getColumn() < (backwardEntry - 1)->getColumn()) {
std::swap(*backwardEntry, *(backwardEntry - 1));
--backwardEntry;
}
} else if ((backwardEntry + 1) != backwardRow.end() && backwardEntry->getColumn() > (backwardEntry + 1)->getColumn()) {
while ((backwardEntry + 1) != backwardRow.end() && backwardEntry->getColumn() > (backwardEntry + 1)->getColumn()) {
std::swap(*backwardEntry, *(backwardEntry + 1));
++backwardEntry;
}
}
std::cout << "after bwd" << std::endl;
for (auto element : backwardTransitions.getRow(forwardElement->getColumn())) {
std::cout << element << ", " << std::endl;
}
return true;
}
template<typename ValueType>
FlexibleSparseMatrix<ValueType>::FlexibleSparseMatrix(index_type rows) : data(rows) {
// Intentionally left empty.

15
src/modelchecker/reachability/SparseSccModelChecker.h
View File

@ -38,15 +38,18 @@ namespace storm {
class SparseSccModelChecker {
public:
static ValueType computeReachabilityProbability(storm::models::Dtmc<ValueType> const& dtmc, std::shared_ptr<storm::properties::prctl::Ap<double>> const& phiFormula, std::shared_ptr<storm::properties::prctl::Ap<double>> const& psiFormula);
// static ValueType computeReachabilityReward(storm::models::Dtmc<ValueType> const& dtmc, std::shared_ptr<storm::properties::prctl::Ap<double>> const& phiFormula, std::shared_ptr<storm::properties::prctl::Ap<double>> const& psiFormula);
static ValueType computeReachabilityProbability(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional<std::vector<std::size_t>> const& statePriorities = {});
static ValueType computeReachabilityReward(storm::models::Dtmc<ValueType> const& dtmc, std::shared_ptr<storm::properties::prctl::Ap<double>> const& phiFormula, std::shared_ptr<storm::properties::prctl::Ap<double>> const& psiFormula);
private:
static uint_fast64_t treatScc(FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, FlexibleSparseMatrix<ValueType>& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector<storm::storage::sparse::state_type>& entryStateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator, boost::optional<std::vector<std::size_t>> const& distances = {});
static ValueType computeReachabilityValue(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional<std::vector<ValueType>>& stateRewards, boost::optional<std::vector<std::size_t>> const& statePriorities = {});
static uint_fast64_t treatScc(FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, FlexibleSparseMatrix<ValueType>& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector<storm::storage::sparse::state_type>& entryStateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator, boost::optional<std::vector<ValueType>>& stateRewards, boost::optional<std::vector<std::size_t>> const& statePriorities = {});
static FlexibleSparseMatrix<ValueType> getFlexibleSparseMatrix(storm::storage::SparseMatrix<ValueType> const& matrix, bool setAllValuesToOne = false);
static void eliminateState(FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix<ValueType>& backwardTransitions);
static bool eliminateStateInPlace(storm::storage::SparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, storm::storage::SparseMatrix<ValueType>& backwardTransitions);
static void eliminateState(FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix<ValueType>& backwardTransitions, boost::optional<std::vector<ValueType>>& stateRewards);
static std::vector<std::size_t> getStatePriorities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector<ValueType> const& oneStepProbabilities);
};
} // namespace reachability

8
src/stormParametric.cpp
View File

@ -157,7 +157,7 @@ int main(const int argc, const char** argv) {
std::shared_ptr<storm::properties::prctl::PrctlFilter<double>> filterFormula = storm::parser::PrctlParser::parsePrctlFormula(storm::settings::generalSettings().getPctlProperty());
std::cout << "Checking formula " << *filterFormula << std::endl;
bool keepRewards = false;
bool checkRewards = false;
std::shared_ptr<storm::properties::prctl::Ap<double>> phiStateFormulaApFormula = nullptr;
std::shared_ptr<storm::properties::prctl::Ap<double>> psiStateFormulaApFormula = nullptr;
@ -180,7 +180,7 @@ int main(const int argc, const char** argv) {
STORM_LOG_THROW(reachabilityRewardFormula, storm::exceptions::InvalidPropertyException, "Illegal formula " << *filterFormula << " for parametric model checking. Note that only unbounded reachability properties (probabilities/rewards) are admitted.");
phiStateFormula = std::shared_ptr<storm::properties::prctl::Ap<double>>(new storm::properties::prctl::Ap<double>("true"));
psiStateFormula = reachabilityRewardFormula->getChild();
keepRewards = true;
checkRewards = true;
}
}
@ -192,7 +192,7 @@ int main(const int argc, const char** argv) {
// Perform bisimulation minimization if requested.
if (storm::settings::generalSettings().isBisimulationSet()) {
storm::storage::DeterministicModelBisimulationDecomposition<storm::RationalFunction> bisimulationDecomposition(*dtmc, phiStateFormulaApFormula->getAp(), psiStateFormulaApFormula->getAp(), keepRewards, storm::settings::bisimulationSettings().isWeakBisimulationSet(), false, true);
storm::storage::DeterministicModelBisimulationDecomposition<storm::RationalFunction> bisimulationDecomposition(*dtmc, phiStateFormulaApFormula->getAp(), psiStateFormulaApFormula->getAp(), checkRewards, storm::settings::bisimulationSettings().isWeakBisimulationSet(), false, true);
dtmc = bisimulationDecomposition.getQuotient()->as<storm::models::Dtmc<storm::RationalFunction>>();
dtmc->printModelInformationToStream(std::cout);
@ -204,7 +204,7 @@ int main(const int argc, const char** argv) {
storm::modelchecker::reachability::SparseSccModelChecker<storm::RationalFunction> modelchecker;
storm::RationalFunction valueFunction = modelchecker.computeReachabilityProbability(*dtmc, phiStateFormulaApFormula, psiStateFormulaApFormula);
storm::RationalFunction valueFunction = checkRewards ? modelchecker.computeReachabilityReward(*dtmc, phiStateFormulaApFormula, psiStateFormulaApFormula) : modelchecker.computeReachabilityProbability(*dtmc, phiStateFormulaApFormula, psiStateFormulaApFormula);
// STORM_PRINT_AND_LOG(std::endl << "Result: (" << carl::computePolynomial(valueFunction.nominator()) << ") / (" << carl::computePolynomial(valueFunction.denominator()) << ")" << std::endl);
// STORM_PRINT_AND_LOG(std::endl << "Result: (" << valueFunction.nominator() << ") / (" << valueFunction.denominator() << ")" << std::endl);
STORM_PRINT_AND_LOG(std::endl << "Result: " << valueFunction << std::endl);

Write Preview
Loading…
Cancel
Save