Forward segment TM decider

_fwdseg.py

from bbconv import *
from collections import deque

# Machine, N - segment length, s - initial state, p in [0..N) - initial position, t - tape state encoded as an integer
# returns (p, t) - final position and tape state
# OR None if machine loops
def segrun(M, N, s, p, t, limit=999999999):
    seen = set()
    while 0 <= p < N:
        #print(": " + bin(t)[2:].zfill(N)[::-1])
        #print("- " + " "*p + "^")
        # Detect loops
        key = ((t << 4 | s) << 8) | p
        if key in seen: return None, limit
        seen.add(key)

        limit -= 1
        if limit <= 0: return None, limit
        # Perform forward transition
        w, d, s = M[s][(t>>p)&1]
        if s < 0: return (p, t), limit # Halt
        if w:
            t |= 1<<p
        else:
            t &= ~(1 << p)
        if d:
            p += 1
        else:
            p += -1
    return (p, t), limit # Ran off the segment

# M - machine, N - segment length
# returns whether the machine halts, or None if it can't decide
def fwddecide(M, N, limit=999999999):
    # compute set of states going left / right
    rs = set()
    ls = set()
    for t in (t for r in M for t in r):
        if t[2]<0: continue
        if t[1]: rs.add(t[2])
        else: ls.add(t[2])

    #print(ls, rs)

    unseenhalts = set(range(N))

    queue = deque()

    seenl = {0}
    seenr = {0}
    for i in range(N):
        queue.append((0, i, 0))
    for s in rs - {0}:
        queue.append((s, 0, 0))
    for s in ls - {0}:
        queue.append((s, N-1, 0))

    while queue:
        s, p, t = queue.pop()
        assert 0 <= p < N
        res, limit = segrun(M, N, s, p, t, limit)
        if limit <= 0: return None, 0
        #print("res =", res)
        if res is None: continue # looped
        p, t = res
        if 0 <= p < N:
            if p in unseenhalts:
                #print("Found halt at position %d" % p)
                unseenhalts.remove(p)
                if not unseenhalts: break
            continue # halted
        # ran off the tape
        if p < 0: # left edge
            if t in seenl: continue # already reached this position
            seenl.add(t)
            for s in rs:
                queue.append((s, 0, t))
        else: # right edge
            if t in seenr: continue # already reached this position
            seenr.add(t)
            for s in ls:
                queue.append((s, N-1, t))

    print("left nodes:", len(seenl))
    print("right nodes:", len(seenr))

    if unseenhalts:
        print("Machine does not halt in positions %r" % unseenhalts)
        print(":NONHALTING:")
        return False, limit
    else:
        print("Machine halted in all reachable positions")
        print(":UNDECIDED:")
        return None, limit

import multiprocessing, ctypes, sys
#counter = multiprocessing.Value(ctypes.c_int32)

def rdecide(i):
    M = read_short(i)[0]
    limit = 5000000
    for s in range(1, 64):
        r, limit = fwddecide(M, s, limit=limit)
        if r is False:
#            with counter:
#                counter.value += 1
            if s > 10:
                sys.stdout.write("machine %d proven at N=%d\n" % (i, s))
                sys.stdout.flush()
            return s, limit
        if limit is 0:
#            with counter:
#                counter.value += 1
#                sys.stdout.write("machine %d bailed at N=%d\n" % (i, s))
#                sys.stdout.flush()
            return -s, 0
#    with counter:
#        counter.value += 1
#        sys.stdout.write("machine %d bailed late\n" % i)
#        sys.stdout.flush()
    return -64, limit

undset = struct.unpack(">"+"I"*(len(undecided)//4), undecided)[::]
with multiprocessing.Pool(15) as pl:
    resset = pl.map(rdecide, undset, 256)
#for m in undset:
#    print(m)
#    print(rdecide(m))

#print("Reading from file")
#with open("resset5M.bin","rb") as f: resset = struct.unpack(">"+"i"*len(undset), f.read())
#with open("resset200k.bin","rb") as f: resset200k = struct.unpack(">"+"i"*len(undset), f.read())

import collections
rescnt = collections.Counter(resset)

print("===== OVERALL STATS =====")
print("%d nonhalting machines" % sum(v for k,v in rescnt.items() if k > 0))
for k,v in sorted(i for i in rescnt.items() if i[0] > 0):
    print("- %d decided with N=%d" % (v, k))
print("%d undecided machines" % sum(v for k,v in rescnt.items() if k < 0))
for k,v in sorted(i for i in rescnt.items() if i[0] < 0)[::-1]:
    print("- %d bailed at N=%d" % (v, -k))

#with open("resset5M.bin", "wb") as f: f.write(struct.pack(">"+"i"*len(resset), *resset))
#import os
#os.system("chmod -w resset5M.bin")

#h3, h5, h7, n = 0, 0, 0, 0
#for i in range(len(undecided)//4):
#    m = struct.unpack_from(">I", undecided, 4*i)[0]
#    M = read_short(m)[0]
#    print(m, "...", end="\r")
#    #print("Machine %9d: %s" % (m, "_".join(s.replace(" ","").replace("!","Z") for s in rustr(M))))
#    if fwddecide(M, 3) is False:
#        #print("Decided witn N=3")
#        h3 += 1
#        continue
#    if fwddecide(M, 5) is False:
#        #print("Decided witn N=5")
#        h5 += 1
#        continue
#    if fwddecide(M, 7) is False:
#        #print("Decided witn N=7")
#        h7 += 1
#        continue
#    #print("Undecided :(")
#    n += 1
#print()
#print("===== OVERALL STATS =====")
#print("%d nonhalting machines" % (h3 + h5 + h7))
#print("- %d decided with N=3" % h3)
#print("- %d decided with N=5" % h5)
#print("- %d decided with N=7" % h7)
#print("%d undecided machines" % n)

bbconv.py

import struct
import mmap
import sys

def find(l, x):
    if x in l: return l.index(x)
    return -1

permuteback = [0, 1, 2, 4, 3, 5, 6, 7, 12, 18, 13, 19, 8, 10, 14, 20, 16, 22, 9, 11, 15, 21, 17, 23]
def rupermute(rules, n):
    m = list(range(2,len(rules)))
    pidx = [0,1] # 1RB assumed
    inv = []
    for i in range(1,len(m)+1):
        n, k = divmod(n, i)
        inv.append(k)
    while m:
        pidx.append(m.pop(inv.pop()))
    #print(pidx)
    fixup = lambda r: (
        (r[0][0], r[0][1], find(pidx, r[0][2])),
        (r[1][0], r[1][1], find(pidx, r[1][2])))
    newrules = [fixup(rules[i]) for i in pidx]
    return newrules

def ruswap(rules, a, b):
    pidx = list(range(len(rules)))
    pidx[a] = b
    pidx[b] = a
    fixup = lambda r: (
        (r[0][0], r[0][1], find(pidx, r[0][2])),
        (r[1][0], r[1][1], find(pidx, r[1][2])))
    newrules = [fixup(rules[i]) for i in pidx]
    return newrules

# Defines lexical order on rules
def rulekey(rules):
    ts = [t for r in rules for t in r]
    ts.pop(0) # first transition is fixed, don't bother comparing
    return [t[2] for t in ts] + [b for t in ts for b in [t[0], t[1]]]

def runorm(ru):
    # Skip initial tape shuffling before writing 1
    while not ru[0][0][0]:
        s=ru[0][0][2].index(True)
        if s == 0: return [((False, True, [True, False]), (True, True, [False, True]))] # 0RA1RH
        ru = ruswap(ru, 0, s)
    # Rule is now 1?? ??? ...
    # Mirror rule to always go right first
    if not ru[0][0][1]:
        ru = [tuple((t[0], not t[1], t[2]) if t[2]>=0 else (1, True, -1) for t in r) for r in ru]
    # Rule is now 1R? ??? ...
    if ru[0][0][2] != 1:
        s=ru[0][0][2]
        if s == 0: return [((True, True, 0), (True, True, -1))] # 1RA1RH
        if s > 1:
            ru = ruswap(ru, 1, s)
    # Rule is now 1RB ??? ...
    assert ru[0][0][0]
    assert ru[0][0][1]
    assert ru[0][0][2] == 1
    for t in (t for r in ru for t in r):
        if t[2] == -1:
            assert t[0] == 1 and t[1] == True, t
    # Choose smallest permutation to achieve canonical lexical normal form (as defined by rulekey)
    N = [1,1,2,6,24,120,720][len(ru)-2]
    mi = 0
    mp = ru
    mk = rulekey(ru)
    for i in range(1, N):
        p = rupermute(ru, i)
        k = rulekey(p)
        assert rupermute(p, permuteback[i]) == ru
        if k < mk:
            mi = i
            mp = p
            mk = k
    return mp, mi

def ruleparse(s, norm=True, partial=False):
    assert not (partial and norm)
    s=s.replace(" ","")
    s=s.replace("_","")
    assert len(s)%6 == 0
    N = len(s)//6
    ru = []
    for i in range(0, len(s), 6):
        if not partial:
            w0, d0, s0 = ord(s[i+0]) - ord("0"), s[i+1].upper() != "L", ord(s[i+2])-ord("A")
            w1, d1, s1 = ord(s[i+3]) - ord("0"), s[i+4].upper() != "L", ord(s[i+5])-ord("A")
            if not (0 <= s0 < N): s0 = -1
            if not (0 <= s1 < N): s1 = -1
            ru.append(((w0, d0, s0), (w1, d1, s1)))
        else:
            w0, d0, s0 = [0, 1, None]["01".find(s[i+0])], [False, True, None]["LR".find(s[i+1].upper())], ord(s[i+2])-ord("A")
            w1, d1, s1 = [0, 1, None]["01".find(s[i+3])], [False, True, None]["LR".find(s[i+4].upper())], ord(s[i+5])-ord("A")
            if not (0 <= s0 <= N): s0 = None if s[i+2] not in "!HXZ" else -1
            if not (0 <= s1 <= N): s1 = None if s[i+5] not in "!HXZ" else -1
            ru.append(((w0, d0, (s0 if s0 is not None else None)), (w1, d1, (s1 if s1 is not None else None))))
    if norm:
        ru, _ = runorm(ru)
    return ru

def rustr(rules, ass=None):
    c = lambda s, x: s[x] if x is not None else "?"
    l = lambda i: chr(ord("A")+i) if 0 <= i < len(rules) else "Z?"[i == None]
    return [" ".join([c("01", w) + c("LR", d) + l(s) for (w, d, s) in r]) for r in rules]

# --- #

def read_wide(i=-1, data=None):
    if data is None: data = widedata
    b = struct.unpack_from("B"*30, widedata, i*30+30)
    return runorm([
        (([0, 1][b[i  ]], [True, False][b[i+1]], b[i+2]-1) if b[i+2] else (1, True, -1),
         ([0, 1][b[i+3]], [True, False][b[i+4]], b[i+5]-1) if b[i+5] else (1, True, -1)) for i in range(0, 30, 6)
    ])

def read_short(i=-1, data=None):
    if data is None: data = shortdata
    st, pk = struct.unpack_from("<II", data, i*8+8)
    return ([
        (((pk>>(4*i  )) & 1, bool((pk>>(4*i+1)) & 1), [0,1,2,3,4,5,6,-1][(st>>(i*6  ))&7]),
         ((pk>>(4*i+2)) & 1, bool((pk>>(4*i+3)) & 1), [0,1,2,3,4,5,6,-1][(st>>(i*6+3))&7])) for i in range(5)
    ], pk >> 20)

def write_short(rules, n, data=None, pos=-1):
    st, pk = 0, 0
    for i, (r0, r1) in enumerate(rules):
        st |= (r0[2]&7) << (6*i)
        st |= (r1[2]&7) << (6*i+3)
        pk |= r0[0] << (4*i)
        pk |= int(r0[1]) << (4*i+1)
        pk |= r1[0] << (4*i+2)
        pk |= int(r1[1]) << (4*i+3)
    pk |= n << 20
    if data is None:
        a = bytearray(8)
        struct.pack_into("<II", a, 0, st, pk)
        return a
    else:
        struct.pack_into("<II", data, pos*8+8, st, pk)

with open("all_5_states_undecided_machines_with_global_header", "rb") as widedbfile:
    widedata = mmap.mmap(widedbfile.fileno(), 0, access=mmap.ACCESS_READ)
if __name__ == "main" and sys.argv[1:] == "convert":
    nmach = struct.unpack_from(">I", widedata, 8)[0]

    import sys
    shortdata = bytearray(8)
    struct.pack_into("<I", shortdata, 0, nmach)
    for i in range(nmach):
        if i % 50000 == 0:
            print(" %d / %d " % (i, nmach), end="\r")
            sys.stdout.flush()
        ru, n = read_wide(i)
        shortdata += write_short(ru, n)
    print("\nDone!")

    with open("seeddb_short_norm.bin", "rb") as f: f.write(shortdata)

with open("seeddb_short_norm.bin", "rb") as shortdbfile:
    shortdata = mmap.mmap(shortdbfile.fileno(), 0, access=mmap.ACCESS_READ)

with open("bb5_undecided_index", "rb") as f:
    undecided = mmap.mmap(f.fileno(), 0, access=mmap.ACCESS_READ)

out-200k.log

===== OVERALL STATS =====
1023776 nonhalting machines
- 256178 decided with N=2
- 332650 decided with N=3
- 197300 decided with N=4
- 104703 decided with N=5
- 54503 decided with N=6
- 30751 decided with N=7
- 18844 decided with N=8
- 11409 decided with N=9
- 6775 decided with N=10
- 4090 decided with N=11
- 2457 decided with N=12
- 1603 decided with N=13
- 866 decided with N=14
- 591 decided with N=15
- 354 decided with N=16
- 320 decided with N=17
- 150 decided with N=18
- 69 decided with N=19
- 60 decided with N=20
- 37 decided with N=21
- 33 decided with N=22
- 11 decided with N=23
- 10 decided with N=24
- 3 decided with N=25
- 5 decided with N=26
- 1 decided with N=27
- 3 decided with N=28
514836 undecided machines
- 189 bailed at N=9
- 1758 bailed at N=10
- 2546 bailed at N=11
- 6651 bailed at N=12
- 31764 bailed at N=13
- 81579 bailed at N=14
- 65780 bailed at N=15
- 31929 bailed at N=16
- 20972 bailed at N=17
- 18692 bailed at N=18
- 12640 bailed at N=19
- 8471 bailed at N=20
- 5907 bailed at N=21
- 3939 bailed at N=22
- 3410 bailed at N=23
- 2896 bailed at N=24
- 2603 bailed at N=25
- 2607 bailed at N=26
- 2521 bailed at N=27
- 2948 bailed at N=28
- 3481 bailed at N=29
- 3838 bailed at N=30
- 4243 bailed at N=31
- 5155 bailed at N=32
- 5622 bailed at N=33
- 5823 bailed at N=34
- 6675 bailed at N=35
- 7404 bailed at N=36
- 7718 bailed at N=37
- 7103 bailed at N=38
- 7076 bailed at N=39
- 6949 bailed at N=40
- 6182 bailed at N=41
- 6121 bailed at N=42
- 6874 bailed at N=43
- 6493 bailed at N=44
- 6116 bailed at N=45
- 5372 bailed at N=46
- 5763 bailed at N=47
- 5277 bailed at N=48
- 4890 bailed at N=49
- 8449 bailed at N=50
- 4230 bailed at N=51
- 4164 bailed at N=52
- 5338 bailed at N=53
- 10050 bailed at N=54
- 6051 bailed at N=55
- 2602 bailed at N=56
- 2957 bailed at N=57
- 1979 bailed at N=58
- 3274 bailed at N=59
- 6923 bailed at N=60
- 6552 bailed at N=61
- 2202 bailed at N=62
- 2206 bailed at N=63
- 13882 bailed at N=64
9916.70user 4.99system 9:56.16elapsed 1664%CPU (0avgtext+0avgdata 261552maxresident)k
8inputs+12024outputs (0major+653059minor)pagefaults 0swaps

out-5M.log

===== OVERALL STATS =====
1024265 nonhalting machines
- 256178 decided with N=2
- 332650 decided with N=3
- 197300 decided with N=4
- 104703 decided with N=5
- 54503 decided with N=6
- 30751 decided with N=7
- 18844 decided with N=8
- 11409 decided with N=9
- 6780 decided with N=10
- 4092 decided with N=11
- 2469 decided with N=12
- 1627 decided with N=13
- 934 decided with N=14
- 626 decided with N=15
- 391 decided with N=16
- 349 decided with N=17
- 200 decided with N=18
- 97 decided with N=19
- 110 decided with N=20
- 76 decided with N=21
- 58 decided with N=22
- 34 decided with N=23
- 19 decided with N=24
- 15 decided with N=25
- 15 decided with N=26
- 3 decided with N=27
- 14 decided with N=28
- 7 decided with N=29
- 5 decided with N=30
- 4 decided with N=31
- 1 decided with N=32
- 1 decided with N=37
514347 undecided machines
- 10 bailed at N=11
- 1151 bailed at N=12
- 2157 bailed at N=13
- 1822 bailed at N=14
- 2134 bailed at N=15
- 4100 bailed at N=16
- 11689 bailed at N=17
- 44878 bailed at N=18
- 77568 bailed at N=19
- 45239 bailed at N=20
- 19562 bailed at N=21
- 11498 bailed at N=22
- 10335 bailed at N=23
- 12316 bailed at N=24
- 12359 bailed at N=25
- 9130 bailed at N=26
- 7089 bailed at N=27
- 4462 bailed at N=28
- 3053 bailed at N=29
- 2553 bailed at N=30
- 2451 bailed at N=31
- 2330 bailed at N=32
- 1672 bailed at N=33
- 1251 bailed at N=34
- 1033 bailed at N=35
- 985 bailed at N=36
- 1032 bailed at N=37
- 844 bailed at N=38
- 728 bailed at N=39
- 577 bailed at N=40
- 448 bailed at N=41
- 357 bailed at N=42
- 392 bailed at N=43
- 338 bailed at N=44
- 294 bailed at N=45
- 295 bailed at N=46
- 312 bailed at N=47
- 264 bailed at N=48
- 286 bailed at N=49
- 266 bailed at N=50
- 297 bailed at N=51
- 320 bailed at N=52
- 358 bailed at N=53
- 363 bailed at N=54
- 348 bailed at N=55
- 389 bailed at N=56
- 396 bailed at N=57
- 494 bailed at N=58
- 561 bailed at N=59
- 581 bailed at N=60
- 630 bailed at N=61
- 655 bailed at N=62
- 743 bailed at N=63
- 208952 bailed at N=64
201112.22user 137.30system 4:11:39elapsed 1332%CPU (0avgtext+0avgdata 621704maxresident)k
1489176inputs+12024outputs (8329major+34152729minor)pagefaults 0swaps