README.md 7.44 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
15
16
17
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:
- Docker images unter `cs8service/cool` tagged with the branch they were published from i.e. `cs8service/cool:master` would give you the latest release candidate of COOL.
  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`
- A prebuilt static binary of the latest release candidate is available as [`cool-static`](https://git8.cs.fau.de/software/cool/-/jobs/artifacts/master/file/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
27
28
29
30
31
32
33
34
35

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`
- [`cool-static`](https://git8.cs.fau.de/software/cool/-/jobs/artifacts/pgsolver/file/cool-static?job=nix-build)
- [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`
- [`cool-static`](https://git8.cs.fau.de/software/cool/-/jobs/artifacts/modcheck/file/cool-static?job=nix-build)
- [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/).