Browse Source

Jani JSONExporter: Fixed export of reward accumulation.

tempestpy_adaptions
TimQu 6 years ago
parent
commit
29e22f6de3
  1. 2
      src/storm/storage/jani/JSONExporter.cpp

2
src/storm/storage/jani/JSONExporter.cpp

@ -167,7 +167,7 @@ namespace storm {
storm::jani::RewardModelInformation info(model, rewardModelName); storm::jani::RewardModelInformation info(model, rewardModelName);
bool steps = rewardAccumulation.isStepsSet() && (info.hasActionRewards() || info.hasTransitionRewards()); bool steps = rewardAccumulation.isStepsSet() && (info.hasActionRewards() || info.hasTransitionRewards());
bool time = rewardAccumulation.isTimeSet() && !model.isDeterministicModel() && info.hasStateRewards();
bool time = rewardAccumulation.isTimeSet() && !model.isDiscreteTimeModel() && info.hasStateRewards();
bool exit = rewardAccumulation.isExitSet() && info.hasStateRewards(); bool exit = rewardAccumulation.isExitSet() && info.hasStateRewards();
return constructRewardAccumulation(storm::logic::RewardAccumulation(steps, time, exit)); return constructRewardAccumulation(storm::logic::RewardAccumulation(steps, time, exit));

Loading…
Cancel
Save