Package owl.run
This package (and it's sub-packages) contains a flexible infrastructure for executing various
translation chains and obtaining these translation chains from the command line. Executions are
modeled as a pipeline, starting with an input parser (e.g., an
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:
- A central coordinator (e.g.,
stream
) takes care of orchestrating the whole execution. It receives anabstract 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.
- To obtain input, the coordinator is given a
reader
which will submit all parsed inputs to a callback. - For each received input, all
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. - Eventually, once all transformers have been called for a particular input, the resulting
object is given to the
output writer
. This object takes care of serializing the final result on the provided output stream.
TransformerSettings settings = ImmutableTransformerSettings.builder()
.key("ltl2nba")
.optionsDirect(new Options()
.addOption("f", "fast", false, "Turn on ludicrous speed!"))
.transformerSettingsParser(settings -> {
boolean fast = settings.hasOption("fast");
return environment -> (input, context) ->
LTL2NBA.apply((LabelledFormula) input, fast, environment);
})
.build();
These settings now only have to be added to the
registry
to be usable with the extended command line
syntax. Also, a dedicated main
method can be created by delegating to the
partial configuration parser
.-
Interface Summary 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 Summary Class Description DefaultCli Pipeline PipelineRunner Helper class to execute a specific pipeline with created input and output streams.RunUtil ServerCli ServerRunner -
Exception Summary Exception Description PipelineException