This is an umbrella library for dealing with (omega) automata in rust. It contains the following subpackages:
automata
introduces the basic types for dealing with transition systems and words. It also contains combinators for manipulating transition systemshoars
implements a parser for the HOA format for representing omega automataautomata-learning
deals with the inference of automata, defines both passive and active automaton learning schemes and implements some algorithmsbin
contains a command line interface to some of the functionality provided in the other packages
In essence, an automaton consists of a transition system (TS) together with an acceptance component. A TS is simply a finite collection of states (the set of all states is denoted
The implementation of TS is generic over the alphabet, which can either be simple (i.e. it is just a collection of individual symbols/chars as given implemented in the CharAlphabet
struct) or propositional (meaning the alphabet consists of a collection of atomic propositions). Similar to other libraries dealing with (omega) automata, we distinguish between edges and transitions in a TS. Specifically, an edge is determined by its origin/target state, the color it emits and a guard, which is of the expression type that the alphabet determines. A transition on the other hand is a concretization of an edge, where the guard is a single symbol (also determined by the alphabet). For simple alphabets, expressions and symbols coincide, whereas for propositional alphabets, expressions are formulas (represented as BDDs) over the atomic propositions and symbols are satisfying valuations of expressions.
The most important trait is TransitionSystem
, which provides access to the indices of all states and is capable of returning iterators over the outgoing edges of a state. It also provides a lot of combinators, which allow manipulation of the TS. For example map_state_color
consumes the TS and relabels the colors on the states through applying a given function. Most combinators consume self
, returning a new TS, which is mainly to avoid unneccessary cloning of the underlying data structures. If the original TS should continue to exist, call as_ref
or simply use a reference to the TS.
As each combinator returns an object which again implements TransitionSystem
, these can easily be chained together without too much overhead. While this is convenient, the applied manipulations are computed on-demand, which may lead to considerable overhead. To circumvent this, it can be beneficial to collect
the resulting TS into a structure, which then explicitly does all the necessary computations and avoids recomputation at a later point. There are also variants collect_with_initial
/collect_ts
, which either take the designated ininital state into account or collect into a specific representation of the TS.
The crate defines some basic building blocks of TS which can easily be manipulated (see Sproutable
), these are
NTS
/DTS
(the latter is just a thin wrapper around the former). These store edges in a vector, a state contains a pointer to the first edge in this collection and each edge contains pointers to the previous/next one.BTS
which stores transitions in an efficient HashMap
Further traits that are of importance are
Pointed
which picks one designated initial state, this is important for deterministic automataDeterministic
, a marker trait that disambiguates between nondeterministic and deterministic TS. AsTransitionSystem
only provides iterators over the outgoing edges, it can be used to deal with nondeterministic TS, that have multiple overlapping edges. By implementingDeterministic
, we guarantee, that there is always a single unique outgoing transition for each state.Sproutable
enables growing a TS state by state and edge/transition by edge/transition. Naturally, this is only implemented for the basic building blocks, i.e.BTS
,DTS
andNTS
.
We can profile the benchmark code with cargo bench --bench forc_paper -- --profile-time 20
where 20
is the time for which the benchmarks will be run. A flamegraph will be generated and placed in target/criterion/forc_paper/profile/flamegraph.csv
.
To ensure code quality, the main
branch should only be modified via pull requests.
The CI is configured that any pull request will run through a set of checks and tests.
Specifically, the formatting is tested, then clippy is run and finally all tests will be run.
To avoid unnecessary runs of the CI, these steps can be run locally before every commit.
This can be done through the check
script included in the base of the repository.