(DA) Automata classes: DeterministicAutomaton, APSet, HOAConsumer, AcceptanceCondition

Adapted from ltl2dstar.

src/storm/automata/APSet.cpp

@@ -0,0 +1,65 @@
+
+#include "storm/automata/APSet.h"
+
+#include <string>
+#include <exception>
+
+namespace storm {
+    namespace automata {
+
+        APSet::APSet() {
+            // intentionally left blank
+        }
+
+        unsigned int APSet::size() const {
+            return index_to_ap.size();
+        }
+
+        std::size_t APSet::alphabetSize() const {
+            return 1L << size();
+        }
+
+        void APSet::add(const std::string& ap) {
+            if (size() >= MAX_APS)
+                throw std::runtime_error("Set of atomic proposition size is limited to " + std::to_string(MAX_APS));
+
+            unsigned int index = size();
+            bool fresh = ap_to_index.insert(std::make_pair(ap, index)).second;
+            if (!fresh)
+                throw std::runtime_error("Duplicate atomic proposition '" + ap + "' in APSet");
+            index_to_ap.push_back(ap);
+        }
+
+        unsigned int APSet::getIndex(const std::string& ap) const {
+            // throws out_of_range if ap is not in the set
+            return ap_to_index.at(ap);
+        }
+
+        const std::string& APSet::getAP(unsigned int index) const {
+            // throws out_of_range if index is out of range
+            return index_to_ap.at(index);
+        }
+
+        const std::vector<std::string>& APSet::getAPs() const {
+            return index_to_ap;
+        }
+
+
+        bool APSet::contains(const std::string& ap) const {
+            return ap_to_index.find(ap) != ap_to_index.end();
+        }
+
+        APSet::alphabet_element APSet::elementAllFalse() const {
+            return 0;
+        }
+
+        APSet::alphabet_element APSet::elementAddAP(alphabet_element element, unsigned int ap) const {
+            if (ap >= size()) {
+                throw std::runtime_error("AP out of range");
+            }
+
+            return element | (1ul << ap);
+        }
+
+    }
+}

src/storm/automata/APSet.h

@@ -0,0 +1,33 @@
+#pragma once
+
+#include <vector>
+#include <map>
+#include <string>
+
+namespace storm {
+    namespace automata {
+        class APSet {
+        public:
+            // TODO: uint32
+            typedef std::size_t alphabet_element;
+
+            APSet();
+
+            unsigned int size() const;
+            std::size_t alphabetSize() const;
+            void add(const std::string& ap);
+            unsigned int getIndex(const std::string& ap) const;
+            bool contains(const std::string& ap) const;
+            const std::string& getAP(unsigned int index) const;
+            const std::vector<std::string>& getAPs() const;
+
+            alphabet_element elementAllFalse() const;
+            alphabet_element elementAddAP(alphabet_element element, unsigned int ap) const;
+
+            const unsigned int MAX_APS = 32;
+        private:
+            std::map<std::string, unsigned int> ap_to_index;
+            std::vector<std::string> index_to_ap;
+        };
+    }
+}

src/storm/automata/AcceptanceCondition.cpp

@@ -0,0 +1,100 @@
+#include "AcceptanceCondition.h"
+
+namespace storm {
+namespace automata {
+
+AcceptanceCondition::AcceptanceCondition(std::size_t numberOfStates, unsigned int numberOfAcceptanceSets, acceptance_expr::ptr acceptance)
+    : numberOfStates(numberOfStates), numberOfAcceptanceSets(numberOfAcceptanceSets), acceptance(acceptance) {
+
+    // initialize acceptance sets
+    for (unsigned int i = 0; i < numberOfAcceptanceSets; i++) {
+        acceptanceSets.push_back(storm::storage::BitVector(numberOfStates));
+    }
+}
+
+unsigned int AcceptanceCondition::getNumberOfAcceptanceSets() const {
+    return numberOfAcceptanceSets;
+}
+
+
+storm::storage::BitVector& AcceptanceCondition::getAcceptanceSet(unsigned int index) {
+    return acceptanceSets.at(index);
+}
+
+const storm::storage::BitVector& AcceptanceCondition::getAcceptanceSet(unsigned int index) const {
+    return acceptanceSets.at(index);
+}
+
+AcceptanceCondition::acceptance_expr::ptr AcceptanceCondition::getAcceptanceExpression() const {
+    return acceptance;
+}
+
+
+bool AcceptanceCondition::isAccepting(const storm::storage::StateBlock& scc) const {
+    return isAccepting(scc, acceptance);
+}
+
+bool AcceptanceCondition::isAccepting(const storm::storage::StateBlock& scc, acceptance_expr::ptr expr) const {
+    switch (expr->getType()) {
+    case acceptance_expr::EXP_AND:
+        return isAccepting(scc, expr->getLeft()) && isAccepting(scc, expr->getRight());
+    case acceptance_expr::EXP_OR:
+        return isAccepting(scc, expr->getLeft()) && isAccepting(scc, expr->getRight());
+    case acceptance_expr::EXP_NOT:
+        return !isAccepting(scc, expr->getLeft());
+    case acceptance_expr::EXP_TRUE:
+        return true;
+    case acceptance_expr::EXP_FALSE:
+        return false;
+    case acceptance_expr::EXP_ATOM: {
+        const cpphoafparser::AtomAcceptance& atom = expr->getAtom();
+        const storm::storage::BitVector& acceptanceSet = acceptanceSets.at(atom.getAcceptanceSet());
+        bool negated = atom.isNegated();
+        bool rv;
+        switch (atom.getType()) {
+        case cpphoafparser::AtomAcceptance::TEMPORAL_INF:
+            rv = false;
+            for (auto& state : scc) {
+                if (acceptanceSet.get(state)) {
+                    rv = true;
+                    break;
+                }
+            }
+            break;
+        case cpphoafparser::AtomAcceptance::TEMPORAL_FIN:
+            rv = true;
+            for (auto& state : scc) {
+                if (acceptanceSet.get(state)) {
+                    rv = false;
+                    break;
+                }
+            }
+            break;
+        }
+
+        return (negated ? !rv : rv);
+    }
+    }
+
+    throw std::runtime_error("Missing case statement");
+}
+
+AcceptanceCondition::ptr AcceptanceCondition::lift(std::size_t productNumberOfStates, std::function<std::size_t (std::size_t)> mapping) const {
+    AcceptanceCondition::ptr lifted(new AcceptanceCondition(productNumberOfStates, numberOfAcceptanceSets, acceptance));
+    for (unsigned int i = 0; i < numberOfAcceptanceSets; i++) {
+        const storm::storage::BitVector& set = getAcceptanceSet(i);
+        storm::storage::BitVector& liftedSet = lifted->getAcceptanceSet(i);
+
+        for (std::size_t prodState = 0; prodState < productNumberOfStates; prodState++) {
+            if (set.get(mapping(prodState))) {
+                liftedSet.set(prodState);
+            }
+        }
+    }
+
+    return lifted;
+}
+
+
+}
+}

src/storm/automata/AcceptanceCondition.h

@@ -0,0 +1,36 @@
+#pragma once
+
+#include <functional>
+#include <vector>
+#include <memory>
+#include "storm/storage/BitVector.h"
+#include "storm/storage/StateBlock.h"
+#include "cpphoafparser/consumer/hoa_consumer.hh"
+
+namespace storm {
+    namespace automata {
+        class AcceptanceCondition {
+        public:
+            typedef std::shared_ptr<AcceptanceCondition> ptr;
+            typedef cpphoafparser::HOAConsumer::acceptance_expr acceptance_expr;
+
+            AcceptanceCondition(std::size_t numberOfStates, unsigned int numberOfAcceptanceSets, acceptance_expr::ptr acceptance);
+            bool isAccepting(const storm::storage::StateBlock& scc) const ;
+
+            unsigned int getNumberOfAcceptanceSets() const;
+            storm::storage::BitVector& getAcceptanceSet(unsigned int index);
+            const storm::storage::BitVector& getAcceptanceSet(unsigned int index) const;
+
+            acceptance_expr::ptr getAcceptanceExpression() const;
+
+            AcceptanceCondition::ptr lift(std::size_t productNumberOfStates, std::function<std::size_t (std::size_t)> mapping) const;
+        private:
+            bool isAccepting(const storm::storage::StateBlock& scc, acceptance_expr::ptr expr) const;
+
+            std::size_t numberOfStates;
+            unsigned int numberOfAcceptanceSets;
+            acceptance_expr::ptr acceptance;
+            std::vector<storm::storage::BitVector> acceptanceSets;
+        };
+    }
+}

src/storm/automata/DeterministicAutomaton.cpp

@@ -0,0 +1,103 @@
+#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"
+
+namespace storm {
+    namespace automata {
+        DeterministicAutomaton::DeterministicAutomaton(APSet apSet, std::size_t numberOfStates, std::size_t initialState, AcceptanceCondition::ptr acceptance)
+                : apSet(apSet), numberOfStates(numberOfStates), initialState(initialState), acceptance(acceptance) {
+            // TODO: this could overflow, add check?
+            edgesPerState = apSet.alphabetSize();
+            numberOfEdges = numberOfStates * edgesPerState;
+            successors.resize(numberOfEdges);
+        }
+
+        std::size_t DeterministicAutomaton::getInitialState() const {
+            return initialState;
+        }
+
+        const APSet& DeterministicAutomaton::getAPSet() const {
+            return apSet;
+        }
+
+        std::size_t DeterministicAutomaton::getSuccessor(std::size_t from, APSet::alphabet_element label) const {
+            std::size_t index = from * edgesPerState + label;
+            return successors.at(index);
+        }
+
+        void DeterministicAutomaton::setSuccessor(std::size_t from, APSet::alphabet_element label, std::size_t successor) {
+            std::size_t index = from * edgesPerState + label;
+            successors.at(index) = successor;
+        }
+
+        std::size_t DeterministicAutomaton::getNumberOfStates() const {
+            return numberOfStates;
+        }
+
+        std::size_t DeterministicAutomaton::getNumberOfEdgesPerState() const {
+            return edgesPerState;
+        }
+
+        AcceptanceCondition::ptr DeterministicAutomaton::getAcceptance() const {
+            return acceptance;
+        }
+
+
+        void DeterministicAutomaton::printHOA(std::ostream& out) const {
+            out << "HOA: v1\n";
+
+            out << "States: " << numberOfStates << "\n";
+
+            out << "Start: " << initialState << "\n";
+
+            out << "AP: " << apSet.size();
+            for (unsigned int i = 0; i < apSet.size(); i++) {
+                out << " " << cpphoafparser::HOAParserHelper::quote(apSet.getAP(i));
+            }
+            out << "\n";
+
+            out << "Acceptance: " << acceptance->getNumberOfAcceptanceSets() << " " << *acceptance->getAcceptanceExpression() << "\n";
+
+            out << "--BODY--" << "\n";
+
+            for (std::size_t s = 0; s < getNumberOfStates(); s++) {
+                out << "State: " << s;
+                out << " {";
+                bool first = true;
+                for (unsigned int i = 0; i < acceptance->getNumberOfAcceptanceSets(); i++) {
+                    if (acceptance->getAcceptanceSet(i).get(s)) {
+                        if (!first)
+                            out << " ";
+                        first = false;
+                        out << i;
+                    }
+                }
+                out << "}\n";
+                for (std::size_t label = 0; label < getNumberOfEdgesPerState(); label++) {
+                    out << getSuccessor(s, label) << "\n";
+                }
+            }
+        }
+
+
+        DeterministicAutomaton::ptr DeterministicAutomaton::parse(std::istream& in) {
+            HOAConsumerDA::ptr consumer(new HOAConsumerDA());
+            cpphoafparser::HOAIntermediateCheckValidity::ptr validator(new cpphoafparser::HOAIntermediateCheckValidity(consumer));
+            cpphoafparser::HOAParser::parse(in, validator);
+
+            return consumer->getDA();
+        }
+
+        DeterministicAutomaton::ptr DeterministicAutomaton::parseFromFile(const std::string& filename) {
+            std::ifstream in(filename);
+            return parse(in);
+        }
+
+    }
+}
+
+
+

src/storm/automata/DeterministicAutomaton.h

@@ -0,0 +1,46 @@
+#pragma once
+
+#include <iostream>
+#include <memory>
+#include "storm/automata/APSet.h"
+
+
+namespace storm {
+    namespace automata {
+        // fwd
+        class AcceptanceCondition;
+
+        class DeterministicAutomaton {
+        public:
+            typedef std::shared_ptr<DeterministicAutomaton> ptr;
+
+            DeterministicAutomaton(APSet apSet, std::size_t numberOfStates, std::size_t initialState, std::shared_ptr<AcceptanceCondition> acceptance);
+
+            const APSet& getAPSet() const;
+
+            std::size_t getInitialState() const;
+
+            std::size_t getSuccessor(std::size_t from, APSet::alphabet_element label) const;
+            void setSuccessor(std::size_t from, APSet::alphabet_element label, std::size_t successor);
+
+            std::size_t getNumberOfStates() const;
+            std::size_t getNumberOfEdgesPerState() const;
+
+            std::shared_ptr<AcceptanceCondition> getAcceptance() const;
+
+            void printHOA(std::ostream& out) const;
+
+            static DeterministicAutomaton::ptr parse(std::istream& in);
+            static DeterministicAutomaton::ptr parseFromFile(const std::string& filename);
+
+        private:
+            APSet apSet;
+            std::size_t numberOfStates;
+            std::size_t initialState;
+            std::size_t numberOfEdges;
+            std::size_t edgesPerState;
+	    std::shared_ptr<AcceptanceCondition> acceptance;
+            std::vector<std::size_t> successors;
+        };
+    }
+}

src/storm/automata/HOAConsumerDA.h

@@ -0,0 +1,237 @@
+#pragma once
+
+#include "storm/automata/APSet.h"
+#include "storm/automata/DeterministicAutomaton.h"
+#include "storm/automata/HOAConsumerDAHeader.h"
+#include "storm/exceptions/OutOfRangeException.h"
+#include "storm/exceptions/InvalidOperationException.h"
+#include "storm/storage/BitVector.h"
+#include "storm/storage/SparseMatrix.h"
+#include "storm/storage/expressions/ExpressionManager.h"
+#include "storm/solver/SmtSolver.h"
+#include "storm/utility/solver.h"
+
+#include "cpphoafparser/consumer/hoa_consumer.hh"
+#include "cpphoafparser/util/implicit_edge_helper.hh"
+
+#include <boost/optional.hpp>
+#include <exception>
+
+namespace storm {
+namespace automata {
+
+class HOAConsumerDA : public HOAConsumerDAHeader {
+private:
+    AcceptanceCondition::ptr acceptance;
+
+    DeterministicAutomaton::ptr da;
+    cpphoafparser::ImplicitEdgeHelper *helper = nullptr;
+
+    std::shared_ptr<storm::expressions::ExpressionManager> expressionManager;
+    std::vector<storm::expressions::Variable> apVariables;
+    std::unique_ptr<storm::solver::SmtSolver> solver;
+
+    storm::storage::BitVector seenEdges;
+
+public:
+    typedef std::shared_ptr<HOAConsumerDA> ptr;
+
+    HOAConsumerDA() : seenEdges(0) {
+        expressionManager.reset(new storm::expressions::ExpressionManager());
+        storm::utility::solver::SmtSolverFactory factory;
+        solver = factory.create(*expressionManager);
+    }
+
+    ~HOAConsumerDA() {
+        delete helper;
+    }
+
+    DeterministicAutomaton::ptr getDA() {
+        return da;
+    }
+
+  /**
+   * Called by the parser to notify that the BODY of the automaton has started [mandatory, once].
+   */
+  virtual void notifyBodyStart() {
+      if (!header.numberOfStates) {
+          throw std::runtime_error("Parsing deterministic HOA automaton: Missing number-of-states header");
+      }
+
+      acceptance = header.getAcceptanceCondition();
+      da.reset(new DeterministicAutomaton(header.apSet, *header.numberOfStates, *header.startState, acceptance));
+
+      helper = new cpphoafparser::ImplicitEdgeHelper(header.apSet.size());
+
+      seenEdges.resize(*header.numberOfStates * helper->getEdgesPerState());
+
+      for (const std::string& ap : header.apSet.getAPs()) {
+          apVariables.push_back(expressionManager->declareBooleanVariable(ap));
+      }
+  }
+
+  /**
+   * Called by the parser for each "State: ..." item [multiple].
+   * @param id the identifier for this state
+   * @param info an optional string providing additional information about the state (empty pointer if not provided)
+   * @param labelExpr an optional boolean expression over labels (state-labeled) (empty pointer if not provided)
+   * @param accSignature an optional list of acceptance set indizes (state-labeled acceptance) (empty pointer if not provided)
+   */
+  virtual void addState(unsigned int id, std::shared_ptr<std::string> info, label_expr::ptr labelExpr, std::shared_ptr<int_list> accSignature) {
+      if (accSignature) {
+          for (unsigned int accSet : *accSignature) {
+              acceptance->getAcceptanceSet(accSet).set(id);
+          }
+      }
+
+      if (labelExpr) {
+          throw std::runtime_error("Parsing deterministic HOA automaton: State-labeled automata not supported");
+      }
+
+      helper->startOfState(id);
+  }
+
+  /**
+   * Called by the parser for each implicit edge definition [multiple], i.e.,
+   * where the edge label is deduced from the index of the edge.
+   *
+   * If the edges are provided in implicit form, after every `addState()` there should be 2^|AP| calls to
+   * `addEdgeImplicit`. The corresponding boolean expression over labels / BitSet
+   * can be obtained by calling BooleanExpression.fromImplicit(i-1) for the i-th call of this function per state.
+   *
+   * @param stateId the index of the 'from' state
+   * @param conjSuccessors a list of successor state indizes, interpreted as a conjunction
+   * @param accSignature an optional list of acceptance set indizes (transition-labeled acceptance) (empty pointer if not provided)
+   */
+  virtual void addEdgeImplicit(unsigned int stateId, const int_list& conjSuccessors, std::shared_ptr<int_list> accSignature) {
+      std::size_t edgeIndex = helper->nextImplicitEdge();
+
+      if (conjSuccessors.size() != 1) {
+          throw std::runtime_error("Parsing deterministic HOA automaton: Does not support alternation (conjunction of successor states)");
+      }
+
+      if (accSignature) {
+          throw std::runtime_error("Parsing deterministic HOA automaton: Does not support transition-based acceptance");
+      }
+
+      da->setSuccessor(stateId, edgeIndex, conjSuccessors.at(0));
+      markEdgeAsSeen(stateId, edgeIndex);
+  }
+
+  /**
+   * Called by the parser for each explicit edge definition [optional, multiple], i.e.,
+   * where the label is either specified for the edge or as a state-label.
+   * <br/>
+   * @param stateId the index of the 'from' state
+   * @param labelExpr a boolean expression over labels (empty pointer if none provided, only in case of state-labeled states)
+   * @param conjSuccessors a list of successors state indizes, interpreted as a conjunction
+   * @param accSignature an optional list of acceptance set indizes (transition-labeled acceptance) (empty pointer if none provided)
+   */
+  virtual void addEdgeWithLabel(unsigned int stateId, label_expr::ptr labelExpr, const int_list& conjSuccessors, std::shared_ptr<int_list> accSignature) {
+      if (conjSuccessors.size() != 1) {
+          throw std::runtime_error("Parsing deterministic HOA automaton: Does not support alternation (conjunction of successor states)");
+      }
+
+      if (accSignature) {
+          throw std::runtime_error("Parsing deterministic HOA automaton: Does not support transition-based acceptance");
+      }
+
+      std::size_t successor = conjSuccessors.at(0);
+
+      solver->reset();
+      solver->add(labelToStormExpression(labelExpr));
+
+      solver->allSat(apVariables,
+          [this, stateId, successor] (storm::expressions::SimpleValuation& valuation) {
+          // construct edge index from valuation
+          APSet::alphabet_element edgeIndex = header.apSet.elementAllFalse();
+          for (std::size_t i = 0; i < apVariables.size(); i++) {
+              if (valuation.getBooleanValue(apVariables[i])) {
+                  edgeIndex = header.apSet.elementAddAP(edgeIndex, i);
+              }
+          }
+
+          // require: edge already exists -> same successor
+          STORM_LOG_THROW(!alreadyHaveEdge(stateId, edgeIndex) || da->getSuccessor(stateId, edgeIndex) == successor,
+                          storm::exceptions::InvalidOperationException, "HOA automaton: multiple definitions of successor for state " << stateId << " and edge " << edgeIndex);
+
+          // std::cout << stateId << " -(" << edgeIndex << ")-> " << successor << std::endl;
+          da->setSuccessor(stateId, edgeIndex, successor);
+          markEdgeAsSeen(stateId, edgeIndex);
+
+          // continue with next valuation
+          return true;
+      });
+  }
+
+  /**
+   * Called by the parser to notify the consumer that the definition for state `stateId`
+   * has ended [multiple].
+   */
+  virtual void notifyEndOfState(unsigned int stateId) {
+      helper->endOfState();
+  }
+
+  /**
+   * Called by the parser to notify the consumer that the automata definition has ended [mandatory, once].
+   */
+  virtual void notifyEnd() {
+      // require that we have seen all edges, i.e., that the automaton is complete
+      STORM_LOG_THROW(seenEdges.full(),
+                      storm::exceptions::InvalidOperationException, "HOA automaton has mismatch in number of edges, not complete?");
+  }
+
+  /**
+   * Called by the parser to notify the consumer that an "ABORT" message has been encountered
+   * (at any time, indicating error, the automaton should be discarded).
+   */
+  virtual void notifyAbort() {
+      throw std::runtime_error("Parsing deterministic automaton: Automaton is incomplete (abort)");
+  }
+
+
+  /**
+   * Is called whenever a condition is encountered that merits a (non-fatal) warning.
+   * The consumer is free to handle this situation as it wishes.
+   */
+  virtual void notifyWarning(const std::string& warning) {
+      // IGNORE
+      (void)warning;
+  }
+
+private:
+  storm::expressions::Expression labelToStormExpression(label_expr::ptr labelExpr) {
+      switch (labelExpr->getType()) {
+      case label_expr::EXP_AND:
+          return labelToStormExpression(labelExpr->getLeft()) && labelToStormExpression(labelExpr->getRight());
+      case label_expr::EXP_OR:
+          return labelToStormExpression(labelExpr->getLeft()) || labelToStormExpression(labelExpr->getRight());
+      case label_expr::EXP_NOT:
+          return !labelToStormExpression(labelExpr->getLeft());
+      case label_expr::EXP_TRUE:
+          return expressionManager->boolean(true);
+      case label_expr::EXP_FALSE:
+          return expressionManager->boolean(false);
+      case label_expr::EXP_ATOM: {
+          unsigned int apIndex = labelExpr->getAtom().getAPIndex();
+          STORM_LOG_THROW(apIndex < apVariables.size(),
+                          storm::exceptions::OutOfRangeException, "HOA automaton refers to non-existing atomic proposition");
+          return apVariables.at(apIndex).getExpression();
+      }
+      }
+      throw std::runtime_error("Unknown label expression operator");
+  }
+
+  bool alreadyHaveEdge(std::size_t stateId, std::size_t edgeIndex) {
+      return seenEdges.get(stateId * helper->getEdgesPerState() + edgeIndex);
+  }
+
+  void markEdgeAsSeen(std::size_t stateId, std::size_t edgeIndex) {
+      seenEdges.set(stateId * helper->getEdgesPerState() + edgeIndex);
+  }
+
+};
+
+}
+}
+

src/storm/automata/HOAConsumerDAHeader.h

@@ -0,0 +1,217 @@
+#pragma once
+
+#include "storm/automata/APSet.h"
+#include "storm/automata/DeterministicAutomaton.h"
+#include "storm/automata/HOAHeader.h"
+#include "storm/storage/BitVector.h"
+#include "storm/storage/SparseMatrix.h"
+#include "cpphoafparser/consumer/hoa_consumer.hh"
+#include "cpphoafparser/util/implicit_edge_helper.hh"
+
+#include <boost/optional.hpp>
+#include <exception>
+
+namespace storm {
+namespace automata {
+
+class HOAConsumerDAHeader : public cpphoafparser::HOAConsumer {
+protected:
+    HOAHeader header;
+
+public:
+    typedef std::shared_ptr<HOAConsumerDAHeader> ptr;
+
+    struct header_parsing_done : public std::exception {};
+
+    HOAHeader& getHeader() {
+        return header;
+    }
+
+    virtual bool parserResolvesAliases() {
+        return true;
+    }
+
+    /** Called by the parser for the "HOA: version" item [mandatory, once]. */
+    virtual void notifyHeaderStart(const std::string& version) {
+        // TODO: Check version
+    }
+
+    /** Called by the parser for the "States: int(numberOfStates)" item [optional, once]. */
+    virtual void setNumberOfStates(unsigned int numberOfStates) {
+        header.numberOfStates = numberOfStates;
+    }
+
+  /**
+   * Called by the parser for each "Start: state-conj" item [optional, multiple].
+   * @param stateConjunction a list of state indizes, interpreted as a conjunction
+   **/
+  virtual void addStartStates(const int_list& stateConjunction) {
+      if (header.startState) {
+          throw std::runtime_error("Parsing deterministic HOA automaton: Nondeterministic choice of  start states not supported");
+      }
+      if (stateConjunction.size() != 1) {
+          throw std::runtime_error("Parsing deterministic HOA automaton: Conjunctive choice of  start states not supported");
+      }
+      header.startState = stateConjunction.at(0);
+  }
+
+  /**
+   * Called by the parser for the "AP: ap-def" item [optional, once].
+   * @param aps the list of atomic propositions
+   */
+  virtual void setAPs(const std::vector<std::string>& aps) {
+      for (const std::string& ap : aps) {
+          header.apSet.add(ap);
+      }
+  }
+
+  /**
+   * Called by the parser for the "Acceptance: acceptance-def" item [mandatory, once].
+   * @param numberOfSets the number of acceptance sets used to tag state / transition acceptance
+   * @param accExpr a boolean expression over acceptance atoms
+   **/
+  virtual void setAcceptanceCondition(unsigned int numberOfSets, acceptance_expr::ptr accExpr) {
+      header.numberOfAcceptanceSets = numberOfSets;
+      header.acceptance_expression = accExpr;
+  }
+
+  /**
+   * Called by the parser for each "acc-name: ..." item [optional, multiple].
+   * @param name the provided name
+   * @param extraInfo the additional information for this item
+   * */
+  virtual void provideAcceptanceName(const std::string& name, const std::vector<cpphoafparser::IntOrString>& extraInfo) {
+      header.accName = name;
+      header.accNameExtraInfo = extraInfo;
+  }
+
+  /**
+   * Called by the parser for each "Alias: alias-def" item [optional, multiple].
+   * Will be called no matter the return value of `parserResolvesAliases()`.
+   *
+   *  @param name the alias name (without @)
+   *  @param labelExpr a boolean expression over labels
+   **/
+  virtual void addAlias(const std::string& name, label_expr::ptr labelExpr) {
+      // IGNORE
+      (void)name;
+      (void)labelExpr;
+  }
+
+  /**
+   * Called by the parser for the "name: ..." item [optional, once].
+   **/
+  virtual void setName(const std::string& name) {
+      // IGNORE
+  }
+
+  /**
+   * Called by the parser for the "tool: ..." item [optional, once].
+   * @param name the tool name
+   * @param version the tool version (option, empty pointer if not provided)
+   **/
+  virtual void setTool(const std::string& name, std::shared_ptr<std::string> version) {
+      // IGNORE
+  }
+
+  /**
+   * Called by the parser for the "properties: ..." item [optional, multiple].
+   * @param properties a list of properties
+   */
+  virtual void addProperties(const std::vector<std::string>& properties) {
+      // TODO: check supported
+  }
+
+  /**
+   * Called by the parser for each unknown header item [optional, multiple].
+   * @param name the name of the header (without ':')
+   * @param content a list of extra information provided by the header
+   */
+  virtual void addMiscHeader(const std::string& name, const std::vector<cpphoafparser::IntOrString>& content) {
+      // TODO: Check semantic headers
+  }
+
+  /**
+   * Called by the parser to notify that the BODY of the automaton has started [mandatory, once].
+   */
+  virtual void notifyBodyStart() {
+      throw header_parsing_done();
+  }
+
+  /**
+   * Called by the parser for each "State: ..." item [multiple].
+   * @param id the identifier for this state
+   * @param info an optional string providing additional information about the state (empty pointer if not provided)
+   * @param labelExpr an optional boolean expression over labels (state-labeled) (empty pointer if not provided)
+   * @param accSignature an optional list of acceptance set indizes (state-labeled acceptance) (empty pointer if not provided)
+   */
+  virtual void addState(unsigned int id, std::shared_ptr<std::string> info, label_expr::ptr labelExpr, std::shared_ptr<int_list> accSignature) {
+      // IGNORE
+  }
+
+  /**
+   * Called by the parser for each implicit edge definition [multiple], i.e.,
+   * where the edge label is deduced from the index of the edge.
+   *
+   * If the edges are provided in implicit form, after every `addState()` there should be 2^|AP| calls to
+   * `addEdgeImplicit`. The corresponding boolean expression over labels / BitSet
+   * can be obtained by calling BooleanExpression.fromImplicit(i-1) for the i-th call of this function per state.
+   *
+   * @param stateId the index of the 'from' state
+   * @param conjSuccessors a list of successor state indizes, interpreted as a conjunction
+   * @param accSignature an optional list of acceptance set indizes (transition-labeled acceptance) (empty pointer if not provided)
+   */
+  virtual void addEdgeImplicit(unsigned int stateId, const int_list& conjSuccessors, std::shared_ptr<int_list> accSignature) {
+      // IGNORE
+  }
+
+  /**
+   * Called by the parser for each explicit edge definition [optional, multiple], i.e.,
+   * where the label is either specified for the edge or as a state-label.
+   * <br/>
+   * @param stateId the index of the 'from' state
+   * @param labelExpr a boolean expression over labels (empty pointer if none provided, only in case of state-labeled states)
+   * @param conjSuccessors a list of successors state indizes, interpreted as a conjunction
+   * @param accSignature an optional list of acceptance set indizes (transition-labeled acceptance) (empty pointer if none provided)
+   */
+  virtual void addEdgeWithLabel(unsigned int stateId, label_expr::ptr labelExpr, const int_list& conjSuccessors, std::shared_ptr<int_list> accSignature) {
+      // IGNORE
+  }
+
+  /**
+   * Called by the parser to notify the consumer that the definition for state `stateId`
+   * has ended [multiple].
+   */
+  virtual void notifyEndOfState(unsigned int stateId) {
+      // IGNORE
+  }
+
+  /**
+   * Called by the parser to notify the consumer that the automata definition has ended [mandatory, once].
+   */
+  virtual void notifyEnd() {
+  }
+
+  /**
+   * Called by the parser to notify the consumer that an "ABORT" message has been encountered
+   * (at any time, indicating error, the automaton should be discarded).
+   */
+  virtual void notifyAbort() {
+      throw std::runtime_error("Parsing deterministic automaton: Automaton is incomplete (abort)");
+  }
+
+
+  /**
+   * Is called whenever a condition is encountered that merits a (non-fatal) warning.
+   * The consumer is free to handle this situation as it wishes.
+   */
+  virtual void notifyWarning(const std::string& warning) {
+      // IGNORE
+      (void)warning;
+  }
+
+};
+
+}
+}
+

src/storm/automata/HOAHeader.h

@@ -0,0 +1,26 @@
+#pragma once
+
+#include "storm/automata/APSet.h"
+#include "cpphoafparser/consumer/hoa_consumer.hh"
+#include <boost/optional.hpp>
+
+namespace storm {
+    namespace automata {
+        class HOAHeader {
+        public:
+            boost::optional<unsigned int> startState;
+            boost::optional<unsigned int> numberOfStates;
+            APSet apSet;
+
+            boost::optional<unsigned int> numberOfAcceptanceSets;
+            cpphoafparser::HOAConsumer::acceptance_expr::ptr acceptance_expression;
+            boost::optional<std::string> accName;
+            boost::optional<std::vector<cpphoafparser::IntOrString>> accNameExtraInfo;
+
+            AcceptanceCondition::ptr getAcceptanceCondition() {
+                return AcceptanceCondition::ptr(new AcceptanceCondition(*numberOfStates, *numberOfAcceptanceSets, acceptance_expression));
+            }
+
+        };
+    }
+}