README.md 1.51 KB
Newer Older
1 2
# Invariants Tool

Christian Müller's avatar
Christian Müller committed
3 4
This is NIWO, an implementation for automatic verification of multi-agent workflows.
It can be used to verify and infer universal invariants for workflows as well as directly solve non-omitting workflows.
5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23

## Prerequisites

The tool is built to be run by the JVM.
It needs an installed Z3 SMT Solver on the machine. There are bindings included for version 4.5.1, which can be replaced by specifying an additional classpath entry containing the new bindings.

## Usage

It can be called with `java -jar invariants.jar [--causal] [--elimChoice] FILE`
It will then try to parse the FILE to a workflow specification, build an equality invariant for a single relation (namely the one mentioned as TARGET in the specification) and try to infer the strongest universal invariant that implies this invariant.

When finished, all intermediate proving steps will be documented in the `results` folder and can be visualized by using the included `renderpngs.sh` script.

## Timings

The given implementation may differ from the time indicated in the paper for various reasons.
This release version will always build the invariant for just the target relation, instead of the conjunction over all relations.
The numbers in the paper have been produced by comparing the sum of all separate runtimes for all possible target relations with the invariant that is a conjunction for all target relations, choosing the minimum.
Also, depending on the workflow, the `elimChoice` configuration variable may improve runtimes significantly in some cases.