Browse Source

minor fix for Long run average rewards for Markov automata

tempestpy_adaptions
TimQu 7 years ago
parent
commit
75e4c229cb
  1. 2
      src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
  2. 1
      src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp

2
src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp

@ -34,7 +34,7 @@ namespace storm {
template<typename SparseMarkovAutomatonModelType>
bool SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
storm::logic::Formula const& formula = checkTask.getFormula();
if(formula.isInFragment(storm::logic::csl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setReachabilityRewardFormulasAllowed(true).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true))) {
if(formula.isInFragment(storm::logic::csl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageRewardFormulasAllowed(true))) {
return true;
} else {
// Check whether we consider a multi-objective formula

1
src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp

@ -247,7 +247,6 @@ namespace storm {
stateRewardWeights[markovianState] = storm::utility::one<ValueType>() / exitRateVector[markovianState];
}
std::vector<ValueType> totalRewardVector = rewardModel.getTotalActionRewardVector(transitionMatrix, stateRewardWeights);
RewardModelType scaledRewardModel(boost::none, std::move(totalRewardVector));
return computeLongRunAverageRewards(dir, transitionMatrix, backwardTransitions, exitRateVector, markovianStates, totalRewardVector, minMaxLinearEquationSolverFactory);
}

Loading…
Cancel
Save