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

[[_TOC_]]

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](/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](/wp-content/uploads/media/research/cool/artifact.zip).**


8
9
10
## Installation 

### Prebuilt Binaries
11

Merlin's avatar
Merlin committed
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
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).
  Run it e.g. `cool-static sat CL <<< '<{1 2}> C & [{1 2}] ~C'`
- All the additional binaries of the project are available as nix-bundles (basically a wrapper like an AppImage to make the executables portable by including their dynamic dependencies) as [job artefacts](https://git8.cs.fau.de/software/cool/-/jobs/artifacts/master/browse?job=nix-bundle).
  Not that the wrapping adds about 200ms of thartup time so **don't use the bundles for benchmarking of fast things where the additional 200ms would be significant**.
- Dynamically linked executables without dependencies are also available [in the artefacts](https://git8.cs.fau.de/software/cool/-/jobs/artifacts/master/browse/dynamic?job=build).
  Run it e.g. `coalg.exe sat CL <<< '<{1 2}> C & [{1 2}] ~C'`.
  Note that these are Linux executables despite the Windows looking `.exe` suffix.

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)
- [Bundles](https://git8.cs.fau.de/software/cool/-/jobs/artifacts/pgsolver/browse?job=nix-bundle)
- [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)
- [Bundles](https://git8.cs.fau.de/software/cool/-/jobs/artifacts/modcheck/browse?job=nix-bundle)
- [Dynamically linked executables](https://git8.cs.fau.de/software/cool/-/jobs/artifacts/modcheck/browse/dynamic?job=build).
42

Merlin's avatar
Merlin committed
43
44
45
46
### 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
47
48
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`

49
50
51
52
53
### 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
54
Runtime dependencies:
55
56
  - readline
  - minisat (at least minisat 2)
Merlin's avatar
Merlin committed
57
58
59
  - m4 
  - zlib 
  - ncurses (for the debugger)
60

Merlin's avatar
Merlin committed
61
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.
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77

### Building from Source

To build the cool executable
```
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
78
79
80
81
82
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.
83

Merlin's avatar
Merlin committed
84
#### Building from source in one script
85
86
87
88
89
90
91

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
92
./ci/ocaml-setup.sh
93
94
95
96
97
98
dune build @all
```

## Usage

To see a longer list of example formulas, just run the testsuite:
Merlin's avatar
Merlin committed
99
```
100
  dune exec cool-testsuite
Merlin's avatar
Merlin committed
101
```
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
### 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
118
119
120
121
122
./coalg.exe sat CL  <<< '<{ 1 2 }> C & [{ 1 2 }] ~C'
# or via the static executable
./cool-static sat CL  <<< '<{ 1 2 }> C & [{ 1 2 }] ~C'
# or via docker
echo '<{1 2}> C & [{1 2}] ~C' | docker run -i cs8service/cool:master sat CL
123
124
```

125
126
127
128
129
130
131
132
133
134
## Experimental Results 

**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/_media/research:cool:benchmarks.zip)**

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/_media/research:cool:comparison_CTL.zip)

## Literature 

- A system description of COOL ([COOL --- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions](https://www8.cs.fau.de/_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/).
- 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/).