Unverified Commit c0e838a7 authored by Merlin's avatar Merlin 💧
Browse files

Inline installation documentation into README

parent 23a92364
Pipeline #10858 waiting for manual action with stages
in 4 minutes and 21 seconds
// -*- mode: adoc; fill-column: 80; -*-
cool solver installation notes
==============================
Dependencies
------------
Install ocaml include files, minisat include files. Place them in the include
directory (e.g. /usr/include, /usr/lib/ocaml, or .).
Dependencies:
- dune
- ocamlfind (package called ocaml-findlib)
- ocamlgraph (package ocaml-ocamlgraph)
- readline
- minisat (at least minisat 2)
On Debian or Ubuntu, install the following packages:
- git
- build-essential
- dune
- libocamlgraph-ocaml-dev
- libreadline-dev
- minisat
Build
-----
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
the flag `--profile=static`.
Verbose manual installation tutorial of the git version
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Install the packaged dependencies (see above). Install minisat, e.g. manually
via git:
git clone TODO
make config prefix=/usr/local
sudo make install
Clone the cool git repository via
TODO
cd cool
And build
dune build @all
Installation
------------
Not possible yet.
Examples
--------
To see a longer list of example formulas, just run the testsuite:
dune exec cool-testsuite
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:
./coalg sat CL <<< '<{ 1 2 }> C & [{ 1 2 }] ~C'
// vim: ft=asciidoc tw=80
......@@ -5,7 +5,9 @@
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).**
## Downloads
## Installation
### Prebuilt Binaries
Alternatively, here is a [tarball](/wp-content/uploads/media/research/cool/cool-src-2014-02-01.tar.gz) of a snapshot. The sources of the global caching solver for [alternation-free](https://git8.cs.fau.de/software/cool) and **aconjunctive** mu-calculi can currently be found in separate branches of the repository. There also are
......@@ -13,6 +15,80 @@ Alternatively, here is a [tarball](/wp-content/uploads/media/research/cool/cool-
- a 64 bit linux build of COOL including the alternation-free fixpoint solving core [cool-afmu-2016-05-24.tgz](/wp-content/uploads/media/research/cool/cool-afmu-2016-05-24.tgz) (2016-05-24).
- a 64 bit linux build of COOL **including the aconjunctive fixpoint solving core** [cool-x86-64-2017-11-07.zip](/wp-content/uploads/media/research/cool/cool-bin-x86_64.tar.gz/cool-x86-64-2017-11-07.zip) (2017-11-07).
### Dependencies
Install ocaml include files, minisat include files. Place them in the include
directory (e.g. `/usr/include`, `/usr/lib/ocaml`, or `.`).
Dependencies:
- dune
- ocamlfind (package called ocaml-findlib)
- ocamlgraph (package ocaml-ocamlgraph)
- readline
- minisat (at least minisat 2)
On Debian or Ubuntu, install the following packages:
- git
- build-essential
- dune
- libocamlgraph-ocaml-dev
- libreadline-dev
- minisat
### 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
the flag `--profile=static`.
#### Verbose manual installation tutorial of the git version
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
dune build @all
```
## Usage
To see a longer list of example formulas, just run the testsuite:
dune exec cool-testsuite
### 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
./coalg sat CL <<< '<{ 1 2 }> C & [{ 1 2 }] ~C'
```
## 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)**
......
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