Crate hoars

This crate provides a parser for the HOA format.

Modules

input

output

Structs

AcceptanceSignature

An acceptance signature is a vector of acceptance set identifiers, it is associated with an edge.

AliasName

Aliases are also named by a string.

Body

Represents the body of a HOA automaton. In essence, this is just a vector of States.

Edge

Represents an edge in a HOA automaton. It contains the crate::LabelExpression, the StateConjunction and the AcceptanceSignature of the edge.

Header

Represents the header of a HOA file, consists of a set of HeaderItems.

HoaAutomaton

Represents a parsed HOA automaton. It consists of a the version string, a Header and a Body. The header contains all the information about the automaton (e.g. the number of states, the acceptance condition, aliases etc.) and the body contains the actual transitions.

HoaBool

Represents a boolean value in the HOA format.

Label

Newtype wrapper around a crate::LabelExpression, implements Deref.

State

Represents a state in a HOA automaton. It contains the Id of the state, an optional comment and a list of outgoing edges.

StateConjunction

Represents a conjunction over states of a HOA automaton, this is mostly used as the initial state of the automaton.

Enums

AbstractLabelExpression

AcceptanceAtom

An acceptance atom can be used to build an acceptance condition, each atom is either a positive or a negative acceptance set identifier.

AcceptanceCondition

An acceptance condition is a positive boolean expression over AcceptanceAtoms.

AcceptanceInfo

Used to give additional (human-readable) and optional information about the acceptance condition, more information can be obtained in the HOA docs.

AcceptanceName

Represents the name of a type of acceptance condition.

FromHoaError

Represents the different types of error that can be encountered when parsing a HoaAutomaton.

HeaderItem

Represents a header item in a HOA file, for more information on each element, see the HOA format specification. The multiplicity of each element is given in parenthesis.

LabelExpression

Property

Represents properties of an automaton. For more information see the documentation of the HOA format.

Constants

MAX_APS

Functions

build_vars

first_automaton_split_position

parse_hoa_automata

Type Aliases

Aliases

Stores information on aliases, it holds a vector of pairs of alias names and label expression. This can be used to unalias an automaton.

AtomicProposition

An atomic proposition is named by a string.

HoaAcceptance

Represents an acceptance condition as it is encoded in a HOA automaton.

Id

The type of identifier used for states.