README.md 1.27 KB
Newer Older
1
# CoPaR, the `Co`algebraic `Pa`rtition `R`efiner
Hans-Peter Deifel's avatar
Hans-Peter Deifel committed
2

3
4
Copar implements a generic partition refinement algorithm with a fast run-time.
The genericity of copar covers the minimization of
Hans-Peter Deifel's avatar
Hans-Peter Deifel committed
5

6
7
8
9
  - Transition Systems (under strong bisimilarity)
  - (Tree) Automata (under tree isomorphism)
  - Markov Chains, and other weighed systems (under weighed bisimilarity)
  - and *combinations* thereof (under derived bismilarity notions, e.g. backwards bisimilarity for weighted tree automata).
Hans-Peter Deifel's avatar
Hans-Peter Deifel committed
10

11
The algorithm runs in *O(m log n)* on a system with *n* states and *m*
Thorsten Wißmann's avatar
Thorsten Wißmann committed
12
transitions and has been developed in a series of publications, see the [literature file](doc/literature.md).
13

14
## Usage
Thorsten Wißmann's avatar
Thorsten Wißmann committed
15
16
Installation instructions can be found in the [install file](INSTALL.md).

17
The core partition-refinement algorithm can be called by
Hans-Peter Deifel's avatar
Hans-Peter Deifel committed
18

19
    ./copar refine FILENAME
Hans-Peter Deifel's avatar
Hans-Peter Deifel committed
20

Hans-Peter Deifel's avatar
Hans-Peter Deifel committed
21
Examples for input files are in the directory `examples/`.
22

Thorsten Wißmann's avatar
Thorsten Wißmann committed
23
24
Command line syntax is described in `copar --help` and the input
file syntax in `copar help`.
25

26
27
28
## Benchmarks

Extensive benchmarks of CoPaR on different input files can be found at
29
[git8.cs.fau.de/software/copar-benchmarks](https://git8.cs.fau.de/software/copar-benchmarks).
30
31
32

Micro-Benchmarks for internal data structures and routines are available in the
`bench/` directory and can be executed with `stack bench`.