Commit caaf71e5 authored by Thorsten Wißmann's avatar Thorsten Wißmann 🐧
Browse files

More documentation mentioning literature

parent 632f9f24
# Installing CoPaR
## Downloading Binaries
You can directly download the [latest binaries for
linux](https://git8.cs.fau.de/software/copar/-/jobs/artifacts/master/download?job=test).
## Build from source
In order to compile it from source
stack build
Enabling the flag `benchmark-generators` also build generators and helper
executables used to create various benchmark suites that have been used in
different publications. To build with that flag, use the command `stack build
--flag copar:benchmark-generators`.
## Running
To partition states of a coalgebra specification, use the command
stack exec -- copar refine FILENAME
Examples for input files are in the directory `examples/`.
Command line syntax is described in `copar --help` and the input
file syntax in `copar help`.
## API documentation
The documentation for the internal API can be built and opened in the
default browser with:
stack haddock --open copar
This can help to understand the code structure.
# CoPaR, the `Co`algebraic `Pa`rtition `R`efiner # CoPaR, the `Co`algebraic `Pa`rtition `R`efiner
Copar implements a generic partition refinement algorithm with a fast run-time.
The genericity of copar covers the minimization of
## Building - 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).
stack build The algorithm runs in *O(m log n)* on a system with *n* states and *m*
transitions and has been developed in a series of publications, see the [Literature](doc/literature.md) file.
Alternatively, you can directly download the [latest binaries for For installation, see the [INSTALL.md](Install.md) file.
linux](https://git8.cs.fau.de/software/copar/-/jobs/artifacts/master/download?job=test).
Enabling the flag `benchmark-generators` also build generators and helper ## Usage
executables used to create various benchmark suites that have been used in The core partition-refinement algorithm can be called by
different publications. To build with that flag, use the command `stack build
--flag copar:benchmark-generators`.
## Running ./copar refine FILENAME
To partition states of a coalgebra specification, use the command
stack exec -- copar refine FILENAME
Examples for input files are in the directory `examples/`. Examples for input files are in the directory `examples/`.
Command line syntax is described in `copar --help` and the input Command line syntax is described in `copar --help` and the input
...@@ -31,12 +30,3 @@ Extensive benchmarks of CoPaR on different input files can be found at ...@@ -31,12 +30,3 @@ Extensive benchmarks of CoPaR on different input files can be found at
Micro-Benchmarks for internal data structures and routines are available in the Micro-Benchmarks for internal data structures and routines are available in the
`bench/` directory and can be executed with `stack bench`. `bench/` directory and can be executed with `stack bench`.
## API documentation
The documentation for the internal API can be built and opened in the
default browser with:
stack haddock --open copar
This can help to understand the code structure.
# Literature
Coalgebraic Partition refinement:
- Generic Partition Refinement and Weighted Tree Automata (Hans-Peter Deifel, Stefan Milius, Lutz Schröder, Thorsten Wißmann) In: Formal Methods – The Next 30 Years, pp. 280–297 [DOI: 10.1007/978-3-030-30942-8_18]
- Hans-Peter Deifel, Master's Thesis, 2019
- Efficient and Modular Coalgebraic Partition Refinement (Thorsten Wißmann, Ulrich Dorsch, Stefan Milius, Lutz Schröder) In: Logical Methods in Computer Science, Volume 16, Issue 1 [DOI: 10.23638/LMCS-16(1:8)2020]
- Conference version of the above journal article: Efficient Coalgebraic Partition Refinement (Ulrich Dorsch, Stefan Milius, Lutz Schröder, Thorsten Wißmann) In: Proc. 28th International Conference on Concurrency Theory (CONCUR 2017) [DOI: 10.4230/LIPIcs.CONCUR.2017.32]
On Reachability:
- A Coalgebraic View on Reachability (Thorsten Wißmann, Stefan Milius, Shin-ya Katsumata, Jérémy Dubut) In: Commentationes Mathematicae Universitatis Carolinae, 60, 4, pp. 605-638
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment