@EverythingIsNonnullByDefault

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 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.

  • 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.
For convenience, several default implementations are also provided. These should be suitable for most cases and may serve as starting point for custom implementations. Note that the provided implementations may satisfy stricter conditions than the ones imposed by the general design. Refer to each interface for the actual method contracts. The command-line parser is completely pluggable and written without explicitly referencing any of our implementations. New modules can be added by simply specifying a name, the set of options, and a way to obtain a configured instance based on some options. For example, the module ltl2nba with a --fast flag can be specified as follows
 
 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.