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.");