PEREDUR repairs unrealisable reactive specifications using a genetic algorithm.
A reactive specification is unrealisable when no implementation can satisfy it against every environment — the specification is at fault, not the code. Tools like ltlsynt will say so, but not what to change. PEREDUR searches for the repairs: edits to the specification that make it realisable while staying as close as possible to what was originally written.
Inputs are either FRETISH requirements as JSON, or basic TLSF — the Temporal Logic Synthesis Format used by the reactive-synthesis community.
Build, then repair one of the bundled examples (building from source covers the non-Nix route):
$ nix develop
$ cmake --workflow --preset release
$ ./build-release/realize examples/lily02/spec.tlsf
UNREALIZABLE
$ mkdir -p out
$ ./build-release/peredur --input examples/lily02/spec.tlsf --output-dir out --seed 42
Realizable specifications: 11 (3 maximal), written to out/
Done in 4.12sThat writes the 3 maximal repairs to out/, each repair_N.tlsf paired with a repair_N.fitness.json holding its score. Expect a few seconds on 20 threads; the seed fixes the repairs, not the runtime, which swings with how the external solvers get scheduled.
The container image is the alternative to nix develop: it carries the binaries, the solvers and these examples, so docker run --rm benmandrew/peredur:latest realize /opt/peredur/share/peredur/examples/lily02/spec.tlsf needs no toolchain on the host.
The example is a grant arbiter that must answer every request within three ticks, never grant twice in a row, and withhold grants after a cancel until a go arrives. Nothing forces go to ever arrive, so a cancelled request can be neither granted nor refused — and the specification cannot be implemented. All three repairs rewrite that third guarantee, which is also the one mucs identifies as the minimal unrealisable core. The TLSF guide walks through this run in full.
| Command | Purpose |
|---|---|
peredur --input <spec> --output-dir <dir> |
repair an unrealisable specification |
realize <spec>... |
report whether a specification is realisable |
ltl <spec>... |
print the LTL formulae a specification translates to |
compare --repairs <dir> --ideals <dir> |
compare repairs against known-ideal ones |
mucs <spec.tlsf> |
extract a minimal unrealisable core from a TLSF spec |
maximal <dir-or-file>... |
report which specifications of a set are maximal under the implication order |
A <spec> is either a FRETISH .json or a .tlsf file.
Run any command with --help for full option descriptions.
PEREDUR evolves a population of candidate specifications over several generations, keeping those that are realisable and close to the original.
- Seed a population of specifications, each mutated slightly from the input.
- Score each candidate on three weighted components: semantic similarity (bounded model counting of satisfying traces), realisability status, and syntactic similarity.
- Evolve through rounds of selection, crossover, mutation, and filtering.
- Collect the realisable survivors, keep the genuine weakenings of the original and, of those, only the maximal ones under implication, then write each to the output directory.
Model counting uses Ganak over the transition matrices of SPOT-generated automata. Satisfiability and realisability queries use black and ltlsynt respectively.
The full documentation is published at benmandrew.com/docs/peredur.
| Building from source | Nix and non-Nix builds, dependencies, presets, tests |
| Docker | building and running the container image |
| Virtual machine | building a VirtualBox appliance from the image |
| Architecture | algorithm flow, key types, module layout |
| Configuration | tuning via TOML, fitness weights, selection schemes |
| TLSF specifications | TLSF mode and a worked repair |
| API reference | the include/ headers |
| Experiment scripts | parameter sweeps and result analysis |