diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp index 92512f6e8..0fd243fcd 100644 --- a/src/storm/builder/DdJaniModelBuilder.cpp +++ b/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; } diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index 606c420bc..d3e6e81b8 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/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.