Find the Turing machine that will produce a desired string.

turing.c

#ifdef KLEE
#include <klee/klee.h>
#include <assert.h>
#endif

#ifndef KLEE
#include <string.h>
#include <stdio.h>
#endif

#include <stdint.h>
#include <stdbool.h>

#define TRANS_SIZE ((uint8_t)5u)
#define MACHINE_MAX_TRANS ((uint32_t)6u)
#define MACHINE_MAX_DESC ((uint32_t)(MACHINE_MAX_TRANS * TRANS_SIZE))

char machine[MACHINE_MAX_DESC] =
#ifdef KLEE 
{0}
#else
{
    1, 0, 'H', 'R', 2,
    6, 0, '.', 'R', 0,
    5, 0, 'o', 'R', 6,
    3, 0, 'l', 'R', 4,
    4, 0, 'l', 'R', 5,
    2, 0, 'e', 'R', 3,
}
#endif
;

#define TAPE_MAX ((uint32_t)32)
char tape[TAPE_MAX] = {0};

bool same(const char * a, const char * b, uint32_t size)
{
    uint32_t i;

    for (i = 0u; i < size; ++i) {
        if (a[i] != b[i]) {
            return false;
        }
    }
    return true;
}

int main(int argc, char *argv[])
{
    uint32_t i, j;
    uint8_t state;
    int32_t head = 0;

#ifdef KLEE
    klee_make_symbolic(machine, MACHINE_MAX_DESC, "machine");
#endif
    state = machine[0];

    while (true) {
#ifndef KLEE
        printf("State: %2x Head: %u Symbol: %2x Tape: %s\n", state, head, tape[head], tape);
#endif
        if (head < 0 || head >= TAPE_MAX ) {
#ifndef KLEE
            printf("Exit: head %d out of bounds.\n", head);
#endif
            break;
        }

        for(i = 0u; i <= MACHINE_MAX_DESC - 5 && machine[i]; i += TRANS_SIZE) {
            if (state == machine[i]
                && tape[head] == machine[i + 1u]) 
            {
                break;
            }
        }
    
        if (i > MACHINE_MAX_DESC - 5 || !machine[i]) {
#ifndef KLEE
            printf("Exit: no applicable transitions.\n");
#endif
            break;
        }

        tape[head] = 
            machine[i + 2u];

        if ('L' == machine[i + 3u]) {
            --head;
        } else if ('R' == machine[i + 3u]) {
            ++head;
        } else {
#ifndef KLEE
            printf("Exit: no applicable transitions.\n");
#endif
          return 1;  
        }
        state = machine[i + 4u];

        if (!state) {
#ifndef KLEE
            printf("Exit: final state.\n");
#endif
            break;
        }
    }
#ifndef KLEE
    printf("Tape: %s\n", tape);
#endif

#ifdef KLEE
    klee_assert(!same(tape, "Forty-two", 10));
#endif
    return 0;
}

Hi, I have done some changes to improve the performance on a KLEE run.
You will find it on my fork https://gist.github.com/PeterHahlweg/d2009f1c48f90dc037614772b09916e7
Let me know what you think about it. 🙂

Hey @PeterHahlweg, will check it ASAP, thanks a lot! 👍

Thanks @PeterHahlweg, looks very good, I would create a repo as discussed and then maybe you can make a PR to it when you have time? I'll put in the code as I have it... which is already a bit improved by having seen your code, but I don't have everything in. Cheers again!