From bb3f7c52fdeef2937c2ad4899c66cec52660789f Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 18 Feb 2020 15:27:40 +0100
Subject: [PATCH] DdJaniModelBuilder: Fixed canHandle

---
 src/storm/builder/DdJaniModelBuilder.cpp       | 2 +-
 src/storm/generator/JaniNextStateGenerator.cpp | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

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.