LTL parser
), followed by multiple transformers (e.g. an
LTL to DPA translation
), and an output writer
at the end (e.g. a HOA printer
). To allow for high
flexibility, various other concepts accompany this central model. In general, the structure is
as follows:
stream
) takes care of orchestrating
the whole execution. It receives an abstract specification
of the involved modules. After setting up relevant I/O operations and instantiating the pipeline
from the specification, the coordinator takes care of executing the process. Since input may
arrive asynchronously, a coordinator might decide to delegate one thread to input parsing and
another to processing the input. Similarly, it might delegate each task to a separate thread (or
even machine) to transparently achieve parallelism even for translations that don't inherently
make use of it. For example, a non-trivial coordinator would be a server that is waiting for
connections and starts a pipeline for each accepted connection, or processes multiple file input
output pairs.
N.B.: If some parts of the pipeline access a globally shared resource, e.g., some static variable, these accesses have to be synchronized or the coordinators have to take care of only running one process in total.
reader
which
will submit all parsed inputs to a callback.
transformers
are called in
order, mutating the input to the desired output. This is usually done by translation or
optimization constructions, but another possible instances are debugging objects which return
the given object untouched and just output various statistics.output writer
. This object takes
care of serializing the final result on the provided output stream.Interface | Description |
---|---|
Environment |
The environment makes global configuration available to all parts of the pipeline.
|
PipelineExecutionContext |
Holds information about an execution originating from a particular input.
|
Class | Description |
---|---|
DefaultCli | |
NullExecutionContext | |
Pipeline | |
PipelineRunner |
Helper class to execute a specific pipeline with created input and output streams.
|
RunUtil | |
ServerCli | |
ServerRunner |