COLA: a determinization, complementation and containment checking library for Büchi automata

COLA has been built on top of SPOT and inspired by Seminator.

List of algorithms

TBA

Requirements

• Spot

./configure --enable-max-accsets=128

One can set the maximal number of colors for an automaton when configuring Spot with --enable-max-accsets=INT

make && make install

Compilation

Please run the following steps to compile COLA after cloning this repo:

autoreconf -i

./configure [--with-spot=where/spot/is/installed]

make

Then you will get an executable file named cola !

Determinization

Input an NBA from "filename", and run ./cola --determinize=cola filename --simulation --stutter --use-scc, then you will get an equivalent deterministic automaton on standard output!

To output the result to a file, use ./cola --determinize=cola filename -o out_filename --simulation --stutter --use-scc

To output a deterministic Parity automaton, use ./cola --determinize=cola filename --parity --acd --simulation --stutter --use-scc

To output a deterministic Rabin automaton, use ./cola --determinize=cola filename --rabin --simulation --stutter --use-scc

To output a complement automaton, use ./cola --determinize=cola filename --parity --acd --complement --simulation --stutter --use-scc