From 3184ba1611a3fc8aaf74728754ab912d001a5496 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 1 Dec 2020 14:51:55 +0100
Subject: [PATCH] Jani: Correctly parse the input-enable field. Throw an error
 in the sparse model builder, as these are not supported right now.

---
 src/storm-parsers/parser/JaniParser.cpp        | 8 +++++++-
 src/storm/generator/JaniNextStateGenerator.cpp | 2 ++
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp
index 06d99c4d2..ce071ff10 100644
--- a/src/storm-parsers/parser/JaniParser.cpp
+++ b/src/storm-parsers/parser/JaniParser.cpp
@@ -1573,7 +1573,13 @@ namespace storm {
         template <typename ValueType>
         std::shared_ptr<storm::jani::Composition> JaniParser<ValueType>::parseComposition(Json const &compositionStructure) {
             if(compositionStructure.count("automaton")) {
-                return std::shared_ptr<storm::jani::AutomatonComposition>(new storm::jani::AutomatonComposition(compositionStructure.at("automaton").template get<std::string>()));
+                std::set<std::string> inputEnabledActions;
+                if (compositionStructure.count("input-enable")) {
+                    for (auto const& actionDecl : compositionStructure.at("input-enable")) {
+                        inputEnabledActions.insert(actionDecl.template get<std::string>());
+                    }
+                }
+                return std::shared_ptr<storm::jani::AutomatonComposition>(new storm::jani::AutomatonComposition(compositionStructure.at("automaton").template get<std::string>(), inputEnabledActions));
             }
             
             STORM_LOG_THROW(compositionStructure.count("elements") == 1, storm::exceptions::InvalidJaniException, "Elements of a composition must be given, got " << compositionStructure.dump());
diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp
index df9530494..4710dd432 100644
--- a/src/storm/generator/JaniNextStateGenerator.cpp
+++ b/src/storm/generator/JaniNextStateGenerator.cpp
@@ -1183,6 +1183,8 @@ namespace storm {
                 uint64_t automatonIndex = 0;
                 for (auto const& composition : parallelComposition.getSubcompositions()) {
                     STORM_LOG_THROW(composition->isAutomatonComposition(), storm::exceptions::WrongFormatException, "Expected flat parallel composition.");
+                    STORM_LOG_THROW(composition->asAutomatonComposition().getInputEnabledActions().empty(), storm::exceptions::NotSupportedException, "Input-enabled actions are not supported right now.");
+
                     this->parallelAutomata.push_back(this->model.getAutomaton(composition->asAutomatonComposition().getAutomatonName()));
                 
                     // Add edges with silent action.