Browse Source

fix in bounded reachability computation with Markov automata

Former-commit-id: fe2b399778
tempestpy_adaptions
TimQu 9 years ago
parent
commit
c672f7aea2
  1. 2
      src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp

2
src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp

@ -72,7 +72,7 @@ namespace storm {
std::vector<ValueType> bMarkovian(markovianNonGoalStates.getNumberOfSetBits()); std::vector<ValueType> bMarkovian(markovianNonGoalStates.getNumberOfSetBits());
// Compute the two fixed right-hand side vectors, one for Markovian states and one for the probabilistic ones. // Compute the two fixed right-hand side vectors, one for Markovian states and one for the probabilistic ones.
std::vector<ValueType> bProbabilisticFixed = transitionMatrix.getConstrainedRowSumVector(probabilisticNonGoalStates, goalStates);
std::vector<ValueType> bProbabilisticFixed = transitionMatrix.getConstrainedRowGroupSumVector(probabilisticNonGoalStates, goalStates);
std::vector<ValueType> bMarkovianFixed; std::vector<ValueType> bMarkovianFixed;
bMarkovianFixed.reserve(markovianNonGoalStates.getNumberOfSetBits()); bMarkovianFixed.reserve(markovianNonGoalStates.getNumberOfSetBits());
for (auto state : markovianNonGoalStates) { for (auto state : markovianNonGoalStates) {

Loading…
Cancel
Save