Linear Bounded Automata enumeration program

The enumeration program was written in C++.

Dependencies

It uses libtbb and C++17 for_each for parallelization.

To install libtbb:

sudo apt install libtbb-dev

The program can be compiled with g++:

g++ -O3 -std=c++17 -o [EXECUTABLE_FILE] [PATH_TO_CPP] -ltbb

Usage

The program contains a series of define directives. The reason is that we optimized the simulation procedured using BITSET, that require to have its size known at compilation time. So if you desire to change the number of states, or tape size, you will need to adjust in the source file, and recompile it. These directives are:

• N_STATES: number of states for LBA
• OUTPUT_CAP: maximum tape size to consider (this means only strings with up to this size will be produced)
• STATE_BITS: amount of bits required to codify N_STATES (should BE ceiling of log base 2 of N_STATES)
• POS_BITS: amount of bits required to codify OUTPUT_CAP (should BE ceiling of log base 2 of OUTPUT_CAP)

Once it was compiled, as "LBA_ENUM", for instance, it can be executed with:

./LBA_ENUM

Root transitions will be enumerated and paralellized for enumeration. Each parallel call will generate a file with its partial results. The program creates a dist directory in the same path where the executable resides, and the partial results files will be within.

You can also run in sharded mode:

./LBA_ENUM [SHARD_NUMBER]

(for more information on the root transitions and sharding, see LINK)