From 9cf3d6af5d16e4d6147c16056dabe039ecbb8e4e Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 9 Aug 2021 17:10:44 +0200
Subject: [PATCH] Adding debug output and file I/O checks whenever parsing a
 HOA automaton from a file.

---
 src/storm/automata/DeterministicAutomaton.cpp | 18 +++++++++++++++---
 src/storm/logic/HOAPathFormula.cpp            |  2 --
 2 files changed, 15 insertions(+), 5 deletions(-)

diff --git a/src/storm/automata/DeterministicAutomaton.cpp b/src/storm/automata/DeterministicAutomaton.cpp
index 62ae6c043..c19f55dbe 100644
--- a/src/storm/automata/DeterministicAutomaton.cpp
+++ b/src/storm/automata/DeterministicAutomaton.cpp
@@ -1,10 +1,15 @@
 #include "storm/automata/DeterministicAutomaton.h"
-#include "storm/automata/AcceptanceCondition.h"
-#include "storm/automata/HOAConsumerDA.h"
+
 #include "cpphoafparser/parser/hoa_parser.hh"
 #include "cpphoafparser/parser/hoa_parser_helper.hh"
 #include "cpphoafparser/consumer/hoa_intermediate_check_validity.hh"
 
+#include "storm/automata/AcceptanceCondition.h"
+#include "storm/automata/HOAConsumerDA.h"
+#include "storm/utility/macros.h"
+
+#include "storm/exceptions/FileIoException.h"
+
 namespace storm {
     namespace automata {
         DeterministicAutomaton::DeterministicAutomaton(APSet apSet, std::size_t numberOfStates, std::size_t initialState, AcceptanceCondition::ptr acceptance)
@@ -93,7 +98,14 @@ namespace storm {
 
         DeterministicAutomaton::ptr DeterministicAutomaton::parseFromFile(const std::string& filename) {
             std::ifstream in(filename);
-            return parse(in);
+            STORM_LOG_THROW(in.good(), storm::exceptions::FileIoException, "Can not open '" << filename << "' for reading.");
+            auto da = parse(in);
+            
+            STORM_LOG_INFO("Deterministic automaton from HOA file '" << filename << "' has "
+                    << da->getNumberOfStates() << " states, "
+                    << da->getAPSet().size() << " atomic propositions and "
+                    << *da->getAcceptance()->getAcceptanceExpression() << " as acceptance condition.");
+            return da;
         }
 
     }
diff --git a/src/storm/logic/HOAPathFormula.cpp b/src/storm/logic/HOAPathFormula.cpp
index b5dc17d27..39a0f60c9 100644
--- a/src/storm/logic/HOAPathFormula.cpp
+++ b/src/storm/logic/HOAPathFormula.cpp
@@ -6,7 +6,6 @@
 #include "storm/exceptions/ExpressionEvaluationException.h"
 #include "storm/exceptions/IllegalArgumentException.h"
 #include "storm/exceptions/InvalidPropertyException.h"
-#include "storm/exceptions/FileIoException.h"
 
 namespace storm {
     namespace logic {
@@ -71,7 +70,6 @@ namespace storm {
 
         storm::automata::DeterministicAutomaton::ptr HOAPathFormula::readAutomaton() const {
             std::ifstream in(automatonFile);
-            STORM_LOG_THROW(in.good(), storm::exceptions::FileIoException, "Can not open '" << automatonFile << "' for reading.");
             storm::automata::DeterministicAutomaton::ptr automaton = storm::automata::DeterministicAutomaton::parse(in);
             for (auto& ap : automaton->getAPSet().getAPs()) {
                 STORM_LOG_THROW(apToFormulaMap.find(ap) != apToFormulaMap.end(), storm::exceptions::ExpressionEvaluationException, "For '" << automatonFile << "' HOA automaton, expression for atomic proposition '" << ap << "' is missing.");