README.md 7.46 KB
Newer Older
Merlin's avatar
Merlin committed
1
# COOL - The **Co**algebraic **O**ntology **L**ogic Reasoner
2
3
4

[[_TOC_]]

Merlin's avatar
Merlin committed
5
COOL is a generic reasoner for modal, hybrid and fixpoint logics, developed jointly at FAU Erlangen-Nürnberg and the Australian National University ([Dirk Pattinson](http://users.cecs.anu.edu.au/~dpattinson/)); it can be instantiated to any modal, hybrid or alternation-free fixpoint logic admitting an axiomatization in terms of so-called rank-1 rules or axioms. Current instantiations include multimodal K (i.e. the description logic ALC), serial monotone neighborhood logic (the next-step logic of game logic GL), and coalition logic (the next-step logic of alternating temporal logic ATL). COOL currently supports global assumptions, i.e. general TBoxes, nominals, satisfaction operators; the latter features are similar in expressivity to Boolean ABoxes. COOL implements two global caching algorithms as separate reasoner cores: the global caching algorithm described in [this paper](http://link.springer.com/chapter/10.1007/978-3-642-14203-1_5) (also available [here](https://www8.cs.fau.de/wp-content/uploads/staff/schroeder/papers/hyGlobalCaching.pdf)) and the global caching algorithm for alternation-free fixpoint logics described in [this paper](http://drops.dagstuhl.de/opus/volltexte/2016/6172/pdf/LIPIcs-CONCUR-2016-34.pdf); the latter reasoner core decides the alternation-free mu-calculi over all supported logics (including in particular CTL, ATL and the star-nesting free fragment of GL). **Recently, the fixpoint core has been extended with support for aconjunctive mu-calculi via permutation games, as described [here](https://arxiv.org/pdf/1710.08996.pdf); an archive containing according binaries, a formula generator and benchmarking scripts is available [here](https://www8.cs.fau.de/wp-content/uploads/media/research/cool/artifact.zip).**
6
7


8
9
10
## Installation 

### Prebuilt Binaries
11

Merlin's avatar
Merlin committed
12
13
14
Visit the [release page](https://git8.cs.fau.de/software/cool/-/releases) to get released versions of COOL.

We provide multiple options to get your hands on an up to date COOL executables:
Merlin's avatar
Merlin committed
15
- Docker images on Dockerhub as `cs8service/cool` tagged with the branch they were published from i.e. `cs8service/cool:master` would give you the latest release candidate of COOL.
Merlin's avatar
Merlin committed
16
  You could e.g. use it to check coalition logic formulas `echo '<{1 2}> C & [{1 2}] ~C' | docker run -i cs8service/cool:master sat CL`
Merlin's avatar
Merlin committed
17
- A prebuilt static binary of the latest release candidate is available as [`cool-static`](https://git8.cs.fau.de/software/cool/-/jobs/artifacts/master/browse/cool-static?job=nix-build).
Merlin's avatar
Merlin committed
18
19
  Run it e.g. `coalg sat CL <<< '<{1 2}> C & [{1 2}] ~C'`
- Dynamically linked executables without included dependencies are also available [in the artefacts](https://git8.cs.fau.de/software/cool/-/jobs/artifacts/master/browse/dynamic?job=build).
Merlin's avatar
Merlin committed
20
21
22
23
24
25
26

There are additional features yet to be merged so use at your own risk:

#### Aconjunctive mu-Calculi

The current master can only work with **alternation free** mu-calculi so if you want to work with **aconjunctive** mu-calculi you should look into [the `pgsolver` branch](https://git8.cs.fau.de/software/cool/-/tree/pgsolver) and the related artefacts: 
- Docker images unter `cs8service/cool:pgsolver`
Merlin's avatar
Merlin committed
27
- [`cool-static`](https://git8.cs.fau.de/software/cool/-/jobs/artifacts/pgsolver/browse/cool-static?job=nix-build)
Merlin's avatar
Merlin committed
28
29
30
31
32
33
- [Dynamically linked executables](https://git8.cs.fau.de/software/cool/-/jobs/artifacts/pgsolver/browse/dynamic?job=build).
 
#### Modelchecking

If you want to do modelchecking you should look into [the `modcheck` branch](https://git8.cs.fau.de/software/cool/-/tree/modcheck) and the related artefacts: 
- Docker images unter `cs8service/cool:modcheck`
Merlin's avatar
Merlin committed
34
- [`cool-static`](https://git8.cs.fau.de/software/cool/-/jobs/artifacts/modcheck/browse/cool-static?job=nix-build)
Merlin's avatar
Merlin committed
35
- [Dynamically linked executables](https://git8.cs.fau.de/software/cool/-/jobs/artifacts/modcheck/browse/dynamic?job=build).
36

Merlin's avatar
Merlin committed
37
38
39
40
### Nix

We also provide batteries included build infrastructure using `nix`. See [the respective documentation](./nix/) on how to use `nix` to develop or compile COOL.

Merlin's avatar
Merlin committed
41
42
You could compile and intall COOL and all it's dependencies using `nix` by running `nix-env -f https://git8.cs.fau.de/software/cool/-/archive/master/cool-master.tar.gz -iA cool`

43
44
45
46
47
### Dependencies

Install ocaml include files, minisat include files. Place them in the include
directory (e.g. `/usr/include`, `/usr/lib/ocaml`, or `.`).

Merlin's avatar
Merlin committed
48
Runtime dependencies:
49
50
  - readline
  - minisat (at least minisat 2)
Merlin's avatar
Merlin committed
51
52
  - m4 
  - zlib 
53
  - ncurses (for the debugger and the repl-example)
54

Merlin's avatar
Merlin committed
55
On Debian, Ubuntu or other `apt` based Linux distrubutions you can use [the setup script](./ci/apt-setup.sh) and [the OCaml setup script](./ci/ocaml-setup.sh) to install the required dependencies.
56
57
58

### Building from Source

Merlin's avatar
Merlin committed
59
To build the cool executables
60
61
62
63
64
65
66
67
68
69
70
71
```
dune build
```
Run it with
```
dune exec cool
```
To build everything just run
```
dune build @all
```
If you want the executables statically linked, then run the build with
Merlin's avatar
Merlin committed
72
73
74
75
76
the flag `--profile=static` i.e.
```
dune build --profile=static
```
Note that static linking also requires the dependencies to be statically available which might **not** be included in your operating system packages.
77

Merlin's avatar
Merlin committed
78
#### Building from source in one script
79
80
81
82
83
84
85

Install the packaged dependencies (see above). Install minisat, e.g. manually
via git:
```bash
git clone https://git8.cs.fau.de/software/cool
cd cool
./ci/apt-setup.sh
Merlin's avatar
Merlin committed
86
./ci/ocaml-setup.sh
87
88
89
90
91
92
dune build @all
```

## Usage

To see a longer list of example formulas, just run the testsuite:
Merlin's avatar
Merlin committed
93
```
94
  dune exec cool-testsuite
Merlin's avatar
Merlin committed
95
```
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
### Coalition Logic

Some formulas are

```
[{1}] C & [{ 2 }] ~C
[{1}] C & <{ 2 }> ~C
[{1}] C & <{ 1 2 }> ~C
<{ 1 2 }> C & <{ 1 2 3 4 5 6 7 8 9 10 }> ~C
<{ 1 2 }> C & <{ 1 2 3 4 5 6 7 8 9 }> ~C
<{ 1 2 }> C & <{ 1 2 }> ~C
<{ 1 2 }> C & [{ 1 2 }] ~C
```

So call for example:
```bash
Merlin's avatar
Merlin committed
112
./coalg sat CL  <<< '<{ 1 2 }> C & [{ 1 2 }] ~C'
Merlin's avatar
Merlin committed
113
114
# or via docker
echo '<{1 2}> C & [{1 2}] ~C' | docker run -i cs8service/cool:master sat CL
115
116
```

117
118
## Experimental Results 

Merlin's avatar
Merlin committed
119
**Recent benchmarking results that compare [MLSolver](https://github.com/tcsprojects/mlsolver) with the permutation game solving core of COOL for aconjunctive formulas can be found in this file: [benchmarks.zip](https://www8.cs.fau.de/wp-content/uploads/media/research/cool/benchmarks.zip)**
120

Merlin's avatar
Merlin committed
121
We also compare the runtimes of three variants of the CTL-instantiation of the alternation-free fixpoint-reasoning core of COOL (with different frequencies of intermediate propagation -- *always*, *never* and *adaptive*) with TreeTab and GMUL on various series of CTL formulas; for descriptions of the benchmark formulas and the provers TreeTab and GMUL, see *An Experimental Comparison of Theorem Provers for CTL*, R. Goré, J. Thomson and F. Widmann, TIME 2011. More benchmarking results can be found in this file: [comparison_ctl.zip](https://www8.cs.fau.de/wp-content/uploads/media/research/cool/comparison_ctl.zip)
122
123
124

## Literature 

Merlin's avatar
Merlin committed
125
- A system description of COOL ([COOL --- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions](https://www8.cs.fau.de/wp-content/uploads/media/research/papers/cool.pdf), D. Gorin, D. Pattinson, L. Schröder, F. Widmann and T. Wißmann) has been published at [IJCAR 2014](http://cs.nyu.edu/ijcar2014/).
126
- A paper on global caching for alternation-free fixpoint logics ([Global Caching for the Alternation-free µ-Calculus](http://drops.dagstuhl.de/opus/volltexte/2016/6172/pdf/LIPIcs-CONCUR-2016-34.pdf), D. Hausmann, L. Schröder and C. Egger) has been published at [CONCUR 2016](https://www.concur2016.ulaval.ca/no_cache/home/).