COLA has been built on top of SPOT and inspired by Seminator.
Complementing UNBA (Under construction): the slice-based algorithm
Divide and conquer approach for determinization and complementaton of nondeterministic Büchi automata
Containment checking based on the determinization and complementation above
./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
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 !
Input an NBA from "filename", and run ./cola --algo=cola filename, then you will get an equivalent deterministic automaton on standard output!
To output the result to a file, use ./cola --algo=cola filename -o out_filename
To output a deterministic Parity automaton, use ./cola --algo=cola filename
To output a deterministic Rabin automaton, use ./cola --algo=cola filename --rabin
To output a complement automaton, use ./cola --algo=cola filename --complement
Complementation using decomposition: ./cola --algo=comp [options] filename
Options:
--merge-iwa- Merge all IWA SCCs--merge-det- Merge all deterministic SCCs--tgba- Outputs a TGBA with two colours--iw-sim- Simulation on IWA SCCs--det-sim- Simulation on DET SCCs--scc-compl- Complementation for each SCC separately--scc-high- SCC compl with high postprocessing before intersection--no-sat- No saturation of accepting states/transitions