Created
February 11, 2021 23:03
-
-
Save Mr-Slippery/81705ec02204831998c24d1e26b4dc17 to your computer and use it in GitHub Desktop.
Find the Turing machine that will produce a desired string.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#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; | |
} |
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!
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Hey @PeterHahlweg, will check it ASAP, thanks a lot! 👍