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

...
 
Commits (8)
image: gitlab.lrz.de:5005/i7/owl:ba23e343
image: gitlab.lrz.de:5005/i7/owl:986b7109
before_script:
- chmod +x gradlew
......@@ -22,7 +22,6 @@ Build:
paths:
- $GRADLE
script:
- apt-get update && apt-get install -y --no-install-recommends build-essential zlib1g-dev # TODO: Remove this after Docker update
- ./gradlew distZip
- unzip -d build/unzipped build/distributions/*.zip
- mv build/unzipped/owl-*/bin build
......
# 2020.XX (unreleased)
# 2020.06
Modules:
......@@ -57,7 +57,7 @@ API:
possible by major performance improvements in the EquivalenceClass
implementation.
* Addition of the `BooleanOperations` utility class that provides Boolean
* Addition of the `BooleanOperations` utility class providing Boolean
operations (complementation, union, and intersection) on automata.
* Addition of utility classes for determinization of NCW and minimisation
......@@ -75,7 +75,8 @@ Bugfixes:
* Fixed several bugs affecting the LD(G)BA, D(G)RA, and DPA constructions.
The translations based on the LICS'18 Master theorem and its predecessors
have been affected.
have been affected. Thanks to Julian Brunner for reporting one of the
issues.
* Fixed a bug in the `UpwardClosedSet` class: sets that were subsumed by other
sets have not been removed in all circumstances.
......
......@@ -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.
......@@ -28,7 +28,6 @@ plugins {
// Languages
apply plugin: 'antlr'
apply plugin: 'c'
apply plugin: 'java'
// Static Analysis
......@@ -40,7 +39,7 @@ apply plugin: 'application'
apply plugin: 'idea'
project.group = 'de.tum.in'
project.version = '20.XX-development'
project.version = '20.06'
project.archivesBaseName = 'owl'
project.mainClassName = 'owl.run.DefaultCli'
......@@ -58,7 +57,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 +304,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.
FROM ubuntu:focal
FROM ubuntu:latest
MAINTAINER Salomon Sickert
......@@ -35,16 +35,16 @@ RUN gu install native-image
## Download, verify, unpack, compile, and install
RUN wget -q https://www.lrde.epita.fr/dload/spot/spot-2.8.7.tar.gz \
&& echo 'bdbeb4454f0244b6b77e1b04458558ab62471aaa21918e104602e6da99969c1f spot-2.8.7.tar.gz' | sha256sum --check \
&& tar -zxvf spot-2.8.7.tar.gz \
&& rm spot-2.8.7.tar.gz \
&& cd spot-2.8.7 \
RUN wget -q https://www.lrde.epita.fr/dload/spot/spot-2.9.3.tar.gz \
&& echo '02a348272329d4931905a586f7197b518ac6fa411aeeea2acac55d6d490ecd1e spot-2.9.3.tar.gz' | sha256sum --check \
&& tar -zxvf spot-2.9.3.tar.gz \
&& rm spot-2.9.3.tar.gz \
&& cd spot-2.9.3 \
&& ./configure --disable-python --enable-max-accsets=1024 \
&& make -j 4 \
&& make install \
&& cd .. \
&& rm -rf spot-2.8.7
&& rm -rf spot-2.9.3
ENV LD_LIBRARY_PATH=/usr/local/lib/
......
# How to update the docker build environment.
0. Update Dockerfile
1. Execute `git log` and get the 8 first characters of the hash sum.
2. `sudo docker pull ubuntu:latest`
3. `sudo docker build -t gitlab.lrz.de:5005/i7/owl:[hash sum] .`
4. `sudo docker push gitlab.lrz.de:5005/i7/owl:[hash sum]`
5. Update `.gitlab-ci.yml`
......@@ -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
......@@ -25,7 +25,7 @@ public class OwlVersion {
// Fall-back strings if MANIFEST cannot be accessed correctly.
private static final String MAIN_NAME = "owl";
private static final String VERSION = "20.XX-development";
private static final String VERSION = "20.06";
private OwlVersion() {}
......