HOAConsumerDA.h

Go to the documentation of this file.

#pragma once
 
#include "storm/automata/APSet.h"
#include "storm/automata/DeterministicAutomaton.h"
#include "storm/automata/HOAConsumerDAHeader.h"
#include "storm/exceptions/InvalidOperationException.h"
#include "storm/exceptions/OutOfRangeException.h"
#include "storm/solver/SmtSolver.h"
#include "storm/storage/BitVector.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/storage/expressions/ExpressionManager.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;
    }
 
    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));
        }
    }
 
    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);
    }
 
    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);
    }
 
    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 << '\n';
            da->setSuccessor(stateId, edgeIndex, successor);
            markEdgeAsSeen(stateId, edgeIndex);
 
            // continue with next valuation
            return true;
        });
    }
 
    virtual void notifyEndOfState(unsigned int /*stateId*/) {
        helper->endOfState();
    }
 
    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?");
    }
 
    virtual void notifyAbort() {
        throw std::runtime_error("Parsing deterministic automaton: Automaton is incomplete (abort)");
    }
 
    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);
    }
};
 
}  // namespace automata
}  // namespace storm