HOAConsumerDAHeader.h

Go to the documentation of this file.

#pragma once
 
#include "cpphoafparser/consumer/hoa_consumer.hh"
#include "cpphoafparser/util/implicit_edge_helper.hh"
#include "storm/automata/APSet.h"
#include "storm/automata/DeterministicAutomaton.h"
#include "storm/automata/HOAHeader.h"
#include "storm/exceptions/NotSupportedException.h"
#include "storm/exceptions/WrongFormatException.h"
#include "storm/storage/BitVector.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/utility/macros.h"
 
#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;
    }

    virtual void notifyHeaderStart(const std::string& /*version*/) {
        // TODO: Check version
    }

    virtual void setNumberOfStates(unsigned int numberOfStates) {
        header.numberOfStates = numberOfStates;
    }

    virtual void addStartStates(const int_list& stateConjunction) {
        STORM_LOG_THROW(!header.startState, storm::exceptions::NotSupportedException,
                        "Parsing deterministic HOA automaton: Nondeterministic choice of start states not supported.");
        STORM_LOG_THROW(stateConjunction.size() == 1, storm::exceptions::NotSupportedException,
                        "Parsing deterministic HOA automaton: Conjunctive choice of start states not supported.");
        header.startState = stateConjunction.at(0);
    }

    virtual void setAPs(const std::vector<std::string>& aps) {
        for (const std::string& ap : aps) {
            header.apSet.add(ap);
        }
    }

    virtual void setAcceptanceCondition(unsigned int numberOfSets, acceptance_expr::ptr accExpr) {
        header.numberOfAcceptanceSets = numberOfSets;
        header.acceptance_expression = accExpr;
    }

    virtual void provideAcceptanceName(const std::string& name, const std::vector<cpphoafparser::IntOrString>& extraInfo) {
        header.accName = name;
        header.accNameExtraInfo = extraInfo;
    }

    virtual void addAlias(const std::string& name, label_expr::ptr labelExpr) {
        // IGNORE
        (void)name;
        (void)labelExpr;
    }

    virtual void setName(const std::string& /*name*/) {
        // IGNORE
    }

    virtual void setTool(const std::string& /*name*/, std::shared_ptr<std::string> /*version*/) {
        // IGNORE
    }

    virtual void addProperties(const std::vector<std::string>& /*properties*/) {
        // TODO: check supported
    }

    virtual void addMiscHeader(const std::string& /*name*/, const std::vector<cpphoafparser::IntOrString>& /*content*/) {
        // TODO: Check semantic headers
    }

    virtual void notifyBodyStart() {
        throw header_parsing_done();
    }

    virtual void addState(unsigned int /*id*/, std::shared_ptr<std::string> /*info*/, label_expr::ptr /*labelExpr*/,
                          std::shared_ptr<int_list> /*accSignature*/) {
        // IGNORE
    }

    virtual void addEdgeImplicit(unsigned int /*stateId*/, const int_list& /*conjSuccessors*/, std::shared_ptr<int_list> /*accSignature*/) {
        // IGNORE
    }

    virtual void addEdgeWithLabel(unsigned int /*stateId*/, label_expr::ptr /*labelExpr*/, const int_list& /*conjSuccessors*/,
                                  std::shared_ptr<int_list> /*accSignature*/) {
        // IGNORE
    }

    virtual void notifyEndOfState(unsigned int /*stateId*/) {
        // IGNORE
    }

    virtual void notifyEnd() {}

    virtual void notifyAbort() {
        STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing deterministic automaton: Automaton is incomplete (abort).");
    }

    virtual void notifyWarning(const std::string& warning) {
        // IGNORE
        (void)warning;
    }
};
 
}  // namespace automata
}  // namespace storm