Browse Source

All model builders support state-exit rewards

tempestpy_adaptions
TimQu 6 years ago
parent
commit
c95ca4ed15
  1. 1
      src/storm/builder/DdJaniModelBuilder.cpp
  2. 1
      src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
  3. 1
      src/storm/generator/JaniNextStateGenerator.cpp

1
src/storm/builder/DdJaniModelBuilder.cpp

@ -1988,6 +1988,7 @@ namespace storm {
STORM_LOG_THROW(!model.usesAssignmentLevels(), storm::exceptions::WrongFormatException, "The symbolic JANI model builder currently does not support assignment levels.");
auto features = model.getModelFeatures();
features.remove(storm::jani::ModelFeature::DerivedOperators);
features.remove(storm::jani::ModelFeature::StateExitRewards);
STORM_LOG_THROW(features.empty(), storm::exceptions::InvalidSettingsException, "The dd jani model builder does not support the following model feature(s): " << features.toString() << ".");
storm::jani::Model preparedModel = model;

1
src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp

@ -149,6 +149,7 @@ namespace storm {
#endif
auto features = model.getModelFeatures();
features.remove(storm::jani::ModelFeature::DerivedOperators);
features.remove(storm::jani::ModelFeature::StateExitRewards);
STORM_LOG_THROW(features.empty(), storm::exceptions::InvalidArgumentException, "The jit model builder does not support the following model feature(s): " << features.toString() << ".");
//STORM_LOG_THROW(!model.reusesActionsInComposition(), storm::exceptions::InvalidArgumentException, "The jit JANI model builder currently does not support reusing actions in parallel composition");

1
src/storm/generator/JaniNextStateGenerator.cpp

@ -44,6 +44,7 @@ namespace storm {
auto features = model.getModelFeatures();
features.remove(storm::jani::ModelFeature::DerivedOperators);
features.remove(storm::jani::ModelFeature::StateExitRewards);
// Eliminate arrays if necessary.
if (features.hasArrays()) {
arrayEliminatorData = this->model.eliminateArrays(true);

Loading…
Cancel
Save