From de0dd71679ccfff4027595773225b565d49a8245 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Mon, 24 Aug 2020 22:24:54 +0200 Subject: [PATCH] (DA) Automata classes: DeterministicAutomaton, APSet, HOAConsumer, AcceptanceCondition Adapted from ltl2dstar. --- src/storm/automata/APSet.cpp | 65 +++++ src/storm/automata/APSet.h | 33 +++ src/storm/automata/AcceptanceCondition.cpp | 100 ++++++++ src/storm/automata/AcceptanceCondition.h | 36 +++ src/storm/automata/DeterministicAutomaton.cpp | 103 ++++++++ src/storm/automata/DeterministicAutomaton.h | 46 ++++ src/storm/automata/HOAConsumerDA.h | 237 ++++++++++++++++++ src/storm/automata/HOAConsumerDAHeader.h | 217 ++++++++++++++++ src/storm/automata/HOAHeader.h | 26 ++ 9 files changed, 863 insertions(+) create mode 100644 src/storm/automata/APSet.cpp create mode 100644 src/storm/automata/APSet.h create mode 100644 src/storm/automata/AcceptanceCondition.cpp create mode 100644 src/storm/automata/AcceptanceCondition.h create mode 100644 src/storm/automata/DeterministicAutomaton.cpp create mode 100644 src/storm/automata/DeterministicAutomaton.h create mode 100644 src/storm/automata/HOAConsumerDA.h create mode 100644 src/storm/automata/HOAConsumerDAHeader.h create mode 100644 src/storm/automata/HOAHeader.h diff --git a/src/storm/automata/APSet.cpp b/src/storm/automata/APSet.cpp new file mode 100644 index 000000000..937207215 --- /dev/null +++ b/src/storm/automata/APSet.cpp @@ -0,0 +1,65 @@ + +#include "storm/automata/APSet.h" + +#include +#include + +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& 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); + } + + } +} diff --git a/src/storm/automata/APSet.h b/src/storm/automata/APSet.h new file mode 100644 index 000000000..b56733685 --- /dev/null +++ b/src/storm/automata/APSet.h @@ -0,0 +1,33 @@ +#pragma once + +#include +#include +#include + +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& 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 ap_to_index; + std::vector index_to_ap; + }; + } +} diff --git a/src/storm/automata/AcceptanceCondition.cpp b/src/storm/automata/AcceptanceCondition.cpp new file mode 100644 index 000000000..4f0a7a02a --- /dev/null +++ b/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 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; +} + + +} +} diff --git a/src/storm/automata/AcceptanceCondition.h b/src/storm/automata/AcceptanceCondition.h new file mode 100644 index 000000000..7f1b993c8 --- /dev/null +++ b/src/storm/automata/AcceptanceCondition.h @@ -0,0 +1,36 @@ +#pragma once + +#include +#include +#include +#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 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 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 acceptanceSets; + }; + } +} diff --git a/src/storm/automata/DeterministicAutomaton.cpp b/src/storm/automata/DeterministicAutomaton.cpp new file mode 100644 index 000000000..62ae6c043 --- /dev/null +++ b/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); + } + + } +} + + + diff --git a/src/storm/automata/DeterministicAutomaton.h b/src/storm/automata/DeterministicAutomaton.h new file mode 100644 index 000000000..940ae77de --- /dev/null +++ b/src/storm/automata/DeterministicAutomaton.h @@ -0,0 +1,46 @@ +#pragma once + +#include +#include +#include "storm/automata/APSet.h" + + +namespace storm { + namespace automata { + // fwd + class AcceptanceCondition; + + class DeterministicAutomaton { + public: + typedef std::shared_ptr ptr; + + DeterministicAutomaton(APSet apSet, std::size_t numberOfStates, std::size_t initialState, std::shared_ptr 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 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 acceptance; + std::vector successors; + }; + } +} diff --git a/src/storm/automata/HOAConsumerDA.h b/src/storm/automata/HOAConsumerDA.h new file mode 100644 index 000000000..4a2215a8c --- /dev/null +++ b/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 +#include + +namespace storm { +namespace automata { + +class HOAConsumerDA : public HOAConsumerDAHeader { +private: + AcceptanceCondition::ptr acceptance; + + DeterministicAutomaton::ptr da; + cpphoafparser::ImplicitEdgeHelper *helper = nullptr; + + std::shared_ptr expressionManager; + std::vector apVariables; + std::unique_ptr solver; + + storm::storage::BitVector seenEdges; + +public: + typedef std::shared_ptr 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 info, label_expr::ptr labelExpr, std::shared_ptr 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 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. + *
+ * @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 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); + } + +}; + +} +} + diff --git a/src/storm/automata/HOAConsumerDAHeader.h b/src/storm/automata/HOAConsumerDAHeader.h new file mode 100644 index 000000000..4d12c0082 --- /dev/null +++ b/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 +#include + +namespace storm { +namespace automata { + +class HOAConsumerDAHeader : public cpphoafparser::HOAConsumer { +protected: + HOAHeader header; + +public: + typedef std::shared_ptr 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& 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& 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 version) { + // IGNORE + } + + /** + * Called by the parser for the "properties: ..." item [optional, multiple]. + * @param properties a list of properties + */ + virtual void addProperties(const std::vector& 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& 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 info, label_expr::ptr labelExpr, std::shared_ptr 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 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. + *
+ * @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 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; + } + +}; + +} +} + diff --git a/src/storm/automata/HOAHeader.h b/src/storm/automata/HOAHeader.h new file mode 100644 index 000000000..1eb7e33af --- /dev/null +++ b/src/storm/automata/HOAHeader.h @@ -0,0 +1,26 @@ +#pragma once + +#include "storm/automata/APSet.h" +#include "cpphoafparser/consumer/hoa_consumer.hh" +#include + +namespace storm { + namespace automata { + class HOAHeader { + public: + boost::optional startState; + boost::optional numberOfStates; + APSet apSet; + + boost::optional numberOfAcceptanceSets; + cpphoafparser::HOAConsumer::acceptance_expr::ptr acceptance_expression; + boost::optional accName; + boost::optional> accNameExtraInfo; + + AcceptanceCondition::ptr getAcceptanceCondition() { + return AcceptanceCondition::ptr(new AcceptanceCondition(*numberOfStates, *numberOfAcceptanceSets, acceptance_expression)); + } + + }; + } +}