Browse Source

fixed issue when checking whether transition rewards can be lifted

main
TimQu 6 years ago
parent
commit
0434d9f83a
  1. 2
      src/storm-cli-utilities/model-handling.h
  2. 14
      src/storm/logic/LiftableTransitionRewardsVisitor.cpp

2
src/storm-cli-utilities/model-handling.h

@ -220,7 +220,7 @@ namespace storm {
template <typename ValueType>
std::shared_ptr<storm::models::ModelBase> buildModelSparse(SymbolicInput const& input, storm::settings::modules::BuildSettings const& buildSettings) {
storm::builder::BuilderOptions options(createFormulasToRespect(input.properties));
storm::builder::BuilderOptions options(createFormulasToRespect(input.properties), input.model.get());
options.setBuildChoiceLabels(buildSettings.isBuildChoiceLabelsSet());
options.setBuildStateValuations(buildSettings.isBuildStateValuationsSet());
if (storm::settings::manager().hasModule(storm::settings::modules::CounterexampleGeneratorSettings::moduleName)) {

14
src/storm/logic/LiftableTransitionRewardsVisitor.cpp

@ -120,14 +120,14 @@ namespace storm {
}
bool LiftableTransitionRewardsVisitor::rewardModelHasTransitionRewards(std::string const& rewardModelName) const {
if (symbolicModelDescription.isJaniModel()) {
return storm::jani::RewardModelInformation(symbolicModelDescription.asJaniModel(), rewardModelName).hasTransitionRewards();
} else if (symbolicModelDescription.isPrismProgram()) {
return symbolicModelDescription.asPrismProgram().getRewardModel(rewardModelName).hasTransitionRewards();
} else {
// No model given
return false;
if (symbolicModelDescription.hasModel()) {
if (symbolicModelDescription.isJaniModel()) {
return storm::jani::RewardModelInformation(symbolicModelDescription.asJaniModel(), rewardModelName).hasTransitionRewards();
} else if (symbolicModelDescription.isPrismProgram()) {
return symbolicModelDescription.asPrismProgram().getRewardModel(rewardModelName).hasTransitionRewards();
}
}
return false;
}
}
}
Loading…
Cancel
Save