11.08., 9:00 - 11:00: Due to updates GitLab will be unavailable for some minutes between 09:00 and 11:00.

...
 
Commits (3)
......@@ -2,12 +2,13 @@
A tool collection and library for <b>O</b>mega-<b>w</b>ords, ω-automata and <b>L</b>inear Temporal Logic (LTL). Batteries included.
Functionality (e.g., translations, simplifiers) is available through command-line tools and a Java and C-API. Details on how to use Owl are given in the [usage instructions](doc/USAGE.md). If you want to contribute to Owl, read the [contribution guidelines](CONTRIBUTING.md) which are mandatory if you want your changes to be merged into the main branch.
Read the javadoc of the respective packages of the infrastructure you plan to use, e.g., `owl.automaton`. It contains links to the relevant classes and typical use cases.
Functionality (e.g., translations, simplifiers) is available through command-line tools and a Java and C-API. Details on how to use Owl are given in the [usage instructions](doc/USAGE.md). If you want to contribute to Owl, read the [contribution guidelines](CONTRIBUTING.md) which are mandatory if you want your changes to be merged into the main branch. Read the javadoc of the respective packages of the infrastructure you plan to use, e.g., `owl.automaton`. It contains links to the relevant classes and typical use cases.
For further information see the official [website](https://owl.model.in.tum.de/).
## Prerequisites
## Building
### Prerequisites
Building the project from the repository requires [GraalVM 20.1: JDK 11](https://www.graalvm.org/), a C build environment with the `glibc` and `zlib` header files installed, and [pandoc](https://pandoc.org/). On Ubuntu the required dependencies can be installed via the following commands:
......@@ -30,8 +31,6 @@ JAVA_HOME=/opt/graalvm-ce-java11-20.1.0/
If GraalVM (native-image) is not available, the project can also be built with a reduced set of features on any JDK that supports at least Java 11. See below for instructions.
## Building
### GraalVM
The standard distribution can be obtained with:
......
# Owl
A tool collection and library for <b>O</b>mega-<b>w</b>ords, ω-automata and <b>L</b>inear Temporal Logic (LTL). Batteries included.
Functionality (e.g., translations, simplifiers) is available through command-line tools and a Java and C-API. Details on how to use Owl are given in the [usage instructions](doc/USAGE.md). For further information see the official [website](https://owl.model.in.tum.de/).
## Content
The distribution contains the following:
* `bin` - Startup scripts for the contained tools, which are described in [usage instructions](doc/USAGE.md). `owl-native` is a pre-compiled version of `owl` for linux-amd64 with faster startup time compared to `owl`. All other tools require an installed [Java runtime environment capable of running Java 11](http://jdk.java.net/).
* `clib` - Owl pre-compiled for linux-amd64 as a C library.
* `doc` - Additional documentation.
* `jars` - Owl packaged as a Java library.
* `lib` - Libraries used by Owl.
......@@ -58,7 +58,6 @@ tasks.withType(JavaCompile) {
// options.errorprone.disableWarningsInGeneratedCode = true
}
def buildMarkdown = !project.hasProperty("disable-pandoc")
def buildOwlNative = !project.hasProperty("disable-native")
def includeJar = !project.hasProperty("exclude-jar")
......@@ -306,8 +305,6 @@ javadoc {
// ---------------- Distributions ----------------
// Configure the distribution to include basic documentation.
// Javadoc is excluded and can be built from source release,
// that is generated from the release tag.
distributions {
main {
......
......@@ -55,7 +55,7 @@ __Global options:__
* `-i INPUT`: Pass `INPUT` as input to the tool
* `-I FILE`: Pass the contents of `FILE` to the tool
* `-O FILE`: Write the output to `FILE`
See the [format descriptions](FORMATS.md) for a description of accepted inputs. Additionally, as soon as an unmatched argument is encountered, this and all following arguments will be interpreted as input. For example, `ltl2dpa "F G a"` is equivalent to `ltl2dpa -i "F G a"`.
## Extended command line syntax
......@@ -116,50 +116,11 @@ For example, translation can be delegated to Rabinizer 3.1 by
% owl ltl --- simplify-ltl --- ltl2aut-ext --tool "run-rabinizer.sh %f" --- minimize-aut --- hoa
```
The real strength of this framework comes from its flexibility.
The command-line parser is completely pluggable and written without explicitly referencing any implementation.
In order to add a new algorithm, one simply has to provide a name (as, e.g., `ltl2nba`), an optional set of command line options and a way of obtaining the configured translator from the parsed options.
For example, to add a new construction called `ltl2nba` with a `--fast` flag, the whole description necessary is as follows:
```java
public static final TransformerParser CLI_SETTINGS = ImmutableTransformerParser.builder()
.key("ltl2nba")
.description("Translates LTL to NBA really fast")
.optionsDirect(new Options()
.addOption("f", "fast", false, "Turn on fast mode"))
.parser(settings -> {
boolean fast = settings.hasOption("fast");
return environment -> (input, context) ->
LTL2NBA.apply((LabelledFormula) input, fast, environment)
.build();
```
After registering these settings with a one-line call, the tool can now be used exactly as `ltl2dpa` before.
Additionally, the tool is automatically integrated into the `--help` output of `Owl`, without requiring further interaction from the developer.
Parsers and serializers can be registered with the same kind of specification.
### Advanced Usage
Some advanced features are:
* Dedicated tools can easily be created by delegating to the generic framework.
For example, `ltl2ldba` is created by the following snippet. This automatically sets up command line argument processing, input / output parsing, help printing, etc.
```java
public static void main(String... args) {
PartialConfigurationParser.run(args, PartialModuleConfiguration.builder("ltl2ldba")
.reader(InputReaders.LTL)
.addTransformer(Transformers.LTL_SIMPLIFIER)
.addTransformer(LTL2LDBACliParser.INSTANCE)
.writer(OutputWriters.HOA)
.build());
}
```
### Server Mode
* The *server mode* listens on a given address and port for incoming TCP connections.
Each of these connections then is handled as a separate pair of input source / output sink, i.e. the specified input parser reads from each connection and the resulting outputs are written back to the client, all completely transparent to the translation modules.
For example, a `ltl2dpa` server is started by writing
`% owl-server ltl --- simplify-ltl --- ltl2dpa --- hoa`
Sending input is as easy as `nc localhost 5050` and starting to type.
We also provide a small C utility `owl-client` dedicated to this purpose for users without access to `netcat`.
This allows easy usage as a fast back-end server, since the JVM does not have to start for each input.
The *server mode* listens on a given address and port for incoming TCP connections.
Each of these connections then is handled as a separate pair of input source / output sink, i.e. the specified input parser reads from each connection and the resulting outputs are written back to the client, all completely transparent to the translation modules.
For example, a `ltl2dpa` server is started by writing
`% owl-server ltl --- simplify-ltl --- ltl2dpa --- hoa`
Sending input is as easy as `nc localhost 5050` and starting to type.
This allows easy usage as a fast back-end server, since the JVM does not have to start for each input.
......@@ -8,7 +8,7 @@ IFS=$'\n\t'
# shellcheck source=./vars.sh
source "$(dirname "$0")/vars.sh"
files=("README.md" "CONTRIBUTING.md" "CHANGELOG.md" "doc/"*)
files=("README_DISTRIBUTION.md" "CONTRIBUTING.md" "CHANGELOG.md" "doc/"*)
destination="$1"
for file_path in "${files[@]}"; do
......@@ -20,6 +20,6 @@ for file_path in "${files[@]}"; do
destination_path="$destination/${file_path%.md}.html"
mkdir -p $(dirname "${destination_path}")
pandoc --standalone -f markdown_github -t html5 -o "$destination_path" "$source_path"
pandoc --standalone -f gfm -t html5 -o "$destination_path" "$source_path"
sed -i -- 's/[.]md/.html/g' "$destination_path"
done