# COOL-benchmarks

## Dependencies

   The benchmarks need some external dependencies to be available in the path:

   - [hyperfine](https://github.com/sharkdp/hyperfine) is used to take the measurements.
   - [TATL](https://atila.ibisc.univ-evry.fr/tableau_ATL_star/bin/tatl_star.tar.gz) needs to be available when comparing to TATL.
   - [FaCT++](https://bitbucket.org/dtsarkov/factplusplus) needs to be available when comparing to FaCT++.
     Additionally our scripts require the two wrapper scripts `factSetup.sh` and `factWrapper.sh` to be available in the PATH.
   - [Python 3](https://www.python.org/downloads/) is used for some post processing scripts for combining CSV files with measurements.

## Overview
     
   We have multiple benchmarking scripts to run individual comparisons.
   
### Comparing to FaCT++

    These experiments compare the performance of COOL and FaCT++, the input (extension `.fact` and `.cool`) and output files (extension `.out`) of tested formulae are generated and saved in the working directory.

    `cardiGML.sh`   - a series of satisfiable cardinality formulae
    `uncardiGML.sh` - a series of unsatisfiable cardinality formulae

### Comparing to TATL

    `benchSatAtlCoolTatl.sh` - the 42 example formulae from the TATL paper
    `nestedTATL.sh` - seris of nested modalities based on formulae from the TATL paper
    
### Comparing COOL algorithms

    `treeGML.sh`       - a series of graded tree formulae 
    `parityGML.sh`     - a series of satisfiable parity formulae
    `parityNegGML.sh`  - a series of unsatisfiable parity formulae
    `rabin.sh`         - a series of rabin formulae
    `earlyGML.sh`      - a series of early formulae
    `streettK.sh`      - a series of streett formulae for K
    `streettGML.sh`    - a series of streett fotmulae for GML
