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.