Find the Turing machine that will produce a desired string.

turing.c

#ifdef KLEE
#include <assert.h>
#include <klee/klee.h>
#define PRINTF(...) /* print nothing */
#else
#include <stdio.h>
#define PRINTF(...) printf(__VA_ARGS__)
#endif

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

// A readable representation of the binary move direction.
enum Move { L=0, R=1 };

// This machine state type is defined as bitfield, as we have to shrink the search space for KLEE
//  as much as possible for exceptable runtimes.
//  Also this keeps the logic simple and readable.
typedef struct {
    uint8_t write_symbol;
    uint8_t head_move : 1; // only left or right
    uint8_t next      : 3; // same as for current state
} State;

State machine[10] = {
#ifndef KLEE
    { 1, R, 1 },
    { 4, R, 2 },
    { 3, R, 3 },
    { 3, R, 4 },
    { 2, R, 5 },
    { 5, R, 6 },
    { 0, R, 0 },
#endif
    {0}
};

// This is the alphabet of the turing machine.
//  In this way, there is a well defined search space for KLEE, that does not include symbols we
//  don't care about. e.g. ASCII[1 to 31].
const char     TERMINATOR   = '\0';
const char     ALPHABET[]   = {TERMINATOR, 'H','o','l','e','.'};
const uint32_t ALPHABET_LEN = sizeof(ALPHABET)/sizeof(ALPHABET[0]);

const uint8_t  RESULT_TAPE[]     = {1, 4, 3, 3, 2, 5, 0}; // Hello\0
const uint32_t RESULT_TAPE_LEN   = sizeof(RESULT_TAPE)/sizeof(RESULT_TAPE[0]);
const uint32_t MACHINE_STATE_CNT = sizeof(machine)/sizeof(State);
const uint32_t TAPE_MAX          = 32;


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

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

#ifndef KLEE
void print_tape(const uint8_t * tape, uint32_t size, const char* name) {
    uint32_t i;
    printf("%s:\t", name);
    for(i=0; i<RESULT_TAPE_LEN; ++i) {
        printf("%c", ALPHABET[tape[i]]);
    }
    printf("\n");
}
#endif

int main(int argc, char *argv[])
{
    uint8_t state = 0;
    int32_t head = 0;
    uint8_t tape[TAPE_MAX] = {0};

    PRINTF("alphabet len: %2u\n", ALPHABET_LEN);

#ifdef KLEE
    klee_make_symbolic((void*)machine, sizeof(machine), "machine");
#endif
    do {
        if (head < 0 || head >= TAPE_MAX ) {
            PRINTF("Exit: head %d out of bounds.\n", head);
            break;
        }
        if (state >= MACHINE_STATE_CNT) {
            PRINTF("Exit: state %u out of bounds.\n", state);
            break;
        }

        tape[head] = machine[state].write_symbol;
        PRINTF("State: %2x Head: %u Symbol: %c\n",
            state, head, ALPHABET[machine[state].write_symbol]
        );
        head  += machine[state].head_move == R ? 1 : -1;
        state  = machine[state].next;
    }
    while(0 != state);
    PRINTF("Exit: final state.\n");

#ifdef KLEE
    klee_assert(!same(tape, RESULT_TAPE, RESULT_TAPE_LEN));
#else
    print_tape(tape, RESULT_TAPE_LEN, "tape");
    PRINTF("same: %s\n", same(tape, RESULT_TAPE, RESULT_TAPE_LEN) ? "true" : "false" );
#endif
    return 0;
}

To be fair, this is not* a turing machine at the moment. There is no reading of symbols, only writing. So not* yet exactly what we are look for.

* Well it is somehow, because the reading of zero symbols is optimised out and leafs us with a state machine that describes how to write a string in a given alphabet. It would be different if we do not start from an empty tape, but increases the search Space a lot (for a random initial tape). For this case it boils down to a well known "program": Write some letters from the start to end position on the tape.

A more interesting problem could be to change a sentence, like so:
"I love cookies." -> [magic turing machine] -> "I love coffee"

This could also be fun and is maybe easier to find with KLEE.