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/storage/BitVector.h"
#include "storm/storage/SparseMatrix.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) {
        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);
    }
 
    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() {
        throw std::runtime_error("Parsing deterministic automaton: Automaton is incomplete (abort)");
    }
 
    virtual void notifyWarning(const std::string& warning) {
        // IGNORE
        (void)warning;
    }
};
 
}  // namespace automata
}  // namespace storm