Browse Source

DdJaniModelBuilder: Fixed canHandle

tempestpy_adaptions
Tim Quatmann 5 years ago
parent
commit
bb3f7c52fd
  1. 2
      src/storm/builder/DdJaniModelBuilder.cpp
  2. 1
      src/storm/generator/JaniNextStateGenerator.cpp

2
src/storm/builder/DdJaniModelBuilder.cpp

@ -95,7 +95,7 @@ namespace storm {
auto compositionInfo = storm::jani::CompositionInformationVisitor(model, model.getSystemComposition()).getInformation();
// Every automaton has to occur exactly once.
if (compositionInfo.getAutomatonToMultiplicityMap().size() == model.getNumberOfAutomata()) {
if (compositionInfo.getAutomatonToMultiplicityMap().size() != model.getNumberOfAutomata()) {
STORM_LOG_INFO("Symbolic engine can not build Jani model since the system composition does not list each automaton exactly once.");
return false;
}

1
src/storm/generator/JaniNextStateGenerator.cpp

@ -135,6 +135,7 @@ namespace storm {
features.remove(storm::jani::ModelFeature::Functions); // can be substituted
features.remove(storm::jani::ModelFeature::StateExitRewards);
if (!features.empty()) {
STORM_LOG_INFO("The model can not be build as it contains these unsupported features: " << features.toString());
return false;
}
// There probably are more cases where the model is unsupported. However, checking these is more involved.

Loading…
Cancel
Save