aspirin/verify_logic.py

"""Offline check of aspirin.sax logic: models the Sedona scan (children first, then
propagate links into a component, then execute) for the component types the app uses."""
import random
import xml.etree.ElementTree as ET

SCAN_MS = 100


class C:
    def __init__(self, typ, props):
        self.typ = typ.split("::")[1]
        self.v = {}
        self.kids = []
        self.links_to = []
        self.state = {}
        for k, val in props.items():
            if val in ("true", "false"):
                self.v[k] = val == "true"
            else:
                try:
                    self.v[k] = float(val)
                except ValueError:
                    self.v[k] = val

    def g(self, k, d=0.0):
        return self.v.get(k, d)

    def start(self):
        if self.typ == "Count":
            self.v["out"] = self.g("preset", 0)
            self.state["last"] = False
        if self.typ in ("OneShot", "DlyOn"):
            self.state["last"] = False
            self.state["end"] = 0
        if self.typ == "SRLatch":
            self.state["ls"] = self.state["lr"] = False

    def execute(self, now):
        g, v, t = self.g, self.v, self.typ
        if t in ("Add2", "Add4"):
            v["out"] = g("in1") + g("in2") + g("in3") + g("in4")
        elif t == "Sub2":
            v["out"] = g("in1") - g("in2")
        elif t == "Mul2":
            v["out"] = g("in1") * g("in2")
        elif t == "Reset":
            i, a, b, c, d = g("in"), g("inMin"), g("inMax"), g("outMin"), g("outMax")
            v["out"] = c if i <= a else d if i >= b else (d - c) / (b - a) * (i - a) + c
        elif t == "Linearize":
            xs = [g(f"x{i}") for i in range(10)]
            ys = [g(f"y{i}") for i in range(10)]
            out = float("nan")
            i = g("in")
            for k in range(9):
                lo_ok = i >= xs[0] if k == 0 else i > xs[k]
                if lo_ok and i <= xs[k + 1]:
                    m = (ys[k + 1] - ys[k]) / (xs[k + 1] - xs[k])
                    out = m * i + (ys[k] - m * xs[k])
            v["out"] = out
        elif t == "InRange":
            v["out"] = g("lowLimit") <= g("in") <= g("highLimit")
        elif t == "Cmpr":
            v["xey"] = g("x") == g("y")
        elif t == "And2":
            v["out"] = bool(g("in1", False) and g("in2", False))
        elif t == "And4":
            v["out"] = all(g(f"in{k}", False) for k in range(1, 5))
        elif t in ("Or2", "Or4"):
            v["out"] = any(g(f"in{k}", False) for k in range(1, 5))
        elif t == "Not":
            v["out"] = not g("in", False)
        elif t == "OneShot":
            i = g("in", False)
            if i and not self.state["last"]:
                if not g("out", False):
                    self.state["end"] = now + g("pulseWidth") * 1000
            v["out"] = self.state["end"] > now
            self.state["last"] = i
        elif t == "ADemux2":
            if g("s1", False):
                v["out2"] = g("in")
            else:
                v["out1"] = g("in")
        elif t == "SRLatch":
            if g("s", False) and not self.state["ls"]:
                v["out"] = True
            if g("r", False) and not self.state["lr"]:
                v["out"] = False
            self.state["ls"], self.state["lr"] = g("s", False), g("r", False)
        elif t == "ASW":
            v["out"] = g("in2") if g("s1", False) else g("in1")
        elif t == "TickTock":
            half = 500 / g("ticksPerSec", 1)
            v["out"] = (now // half) % 2 == 0
        elif t == "DlyOn":
            i = g("in", False)
            if i and not self.state["last"]:
                self.state["end"] = now + g("delayTime") * 1000
            if not i:
                self.state["end"] = 0
                v["out"] = False
            else:
                v["out"] = self.state["end"] < now
                if v["out"]:
                    self.state["end"] = 0
            self.state["last"] = i
        elif t == "F2I":
            v["out"] = float(int(g("in")))
        elif t == "I2F":
            v["out"] = g("in")
        elif t == "Count":
            if not g("enable", False):
                return
            c = g("out")
            if g("in", False) and not self.state["last"]:
                c += 1
            if g("r", False):
                c = g("preset", 0)
            v["out"] = c
            self.state["last"] = g("in", False)


def load(path):
    root = ET.parse(path).getroot()
    paths = {}
    order = []

    def walk(el, prefix):
        comps = []
        for ce in el.findall("comp"):
            props = {p.get("name"): p.get("val") for p in ce.findall("prop")}
            c = C(ce.get("type"), props)
            p = f"{prefix}/{ce.get('name')}"
            paths[p] = c
            c.kids = walk(ce, p)
            comps.append(c)
        return comps

    tops = walk(root.find("app"), "")
    for le in root.find("links").findall("link"):
        fp, fs = le.get("from").rsplit(".", 1)
        tp, ts = le.get("to").rsplit(".", 1)
        paths[tp].links_to.append((paths[fp], fs, ts))
    return tops, paths


def run_scan(tops, now):
    def ex(c):
        for k in c.kids:
            ex(k)
        for src, fs, ts in c.links_to:
            c.v[ts] = src.v.get(fs, 0.0)
        c.execute(now)
    for t in tops:
        ex(t)


def board(paths):
    grid = [["  ."] * 4 for _ in range(4)]
    for t in range(1, 16):
        w = paths[f"/ox/Game/Tile{t:02d}"]
        col = int((w.g("x") - 40) // 105)
        row = int((w.g("y") - 40) // 105)
        grid[row][col] = f"{t:3d}"
    return grid


def main_solver():
    """aspirin_solver.sax: exact-length shuffle, then one inverse move per second until solved."""
    tops, paths = load("aspirin_solver.sax")
    for c in paths.values():
        c.start()
    now = 0
    goal = [["  1", "  2", "  3", "  4"], ["  5", "  6", "  7", "  8"],
            ["  9", " 10", " 11", " 12"], [" 13", " 14", " 15", "  ."]]
    snapshots, solve_times = [], []
    last = board(paths)
    shuffle_done_at = None
    for _ in range(1200):                        # 120 s
        now += SCAN_MS + random.randint(-3, 3)
        run_scan(tops, now)
        b = board(paths)
        shuffling = paths["/logic/glob/Shuf"].g("out", False)
        if b != last and not shuffling and shuffle_done_at is not None:
            solve_times.append(now)
        if not shuffling and shuffle_done_at is None and now > 1000:
            shuffle_done_at = now
            snapshots.append(b)
            print("after shuffle:")
            print("\n".join(" ".join(r) for r in b))
            assert b != goal, "shuffle left board solved"
        last = b
        if shuffle_done_at and paths["/logic/post/Solved"].g("out", False):
            break
    assert paths["/logic/post/Solved"].g("out", False), "auto solver did not finish"
    assert board(paths) == goal
    gaps = [b - a for a, b in zip(solve_times, solve_times[1:])]
    print(f"solved with {len(solve_times)} moves, first move {solve_times[0]-shuffle_done_at} ms "
          f"after shuffle, gaps {min(gaps)}-{max(gaps)} ms, moves label "
          f"{paths['/logic/post/CntF'].g('out')}")
    assert len(solve_times) == 30 and min(gaps) >= 900
    assert paths["/logic/stkReg/Empty"].g("out", False)
    # SHUFFLE again
    paths["/ox/Game/Shuffle"].v["touch"] = True
    for _ in range(3):
        now += SCAN_MS
        run_scan(tops, now)
    paths["/ox/Game/Shuffle"].v["touch"] = False
    for _ in range(600):
        now += SCAN_MS
        run_scan(tops, now)
        if paths["/logic/post/Solved"].g("out", False) and not paths["/logic/glob/Shuf"].g("out", False):
            break
    assert board(paths) == goal and paths["/logic/post/Solved"].g("out", False)
    print("second shuffle + auto solve OK")


def main():
    tops, paths = load("aspirin.sax")
    for c in paths.values():
        c.start()
    now = 0

    def step(n=1):
        nonlocal now
        for _ in range(n):
            now += SCAN_MS + random.randint(-3, 3)
            run_scan(tops, now)

    def check_perm():
        cells = [tuple(r) for r in board(paths)]
        flat = [x for r in cells for x in r]
        nums = sorted(int(x) for x in flat if x.strip() != ".")
        assert nums == list(range(1, 16)), cells

    step(120)  # boot shuffle (10 s) + settle
    check_perm()
    g = board(paths)
    print("after shuffle:")
    print("\n".join(" ".join(r) for r in g))
    solved = paths["/logic/post/Solved"].g("out", False)
    print("solved flag:", solved, "moves:", paths["/logic/post/CntF"].g("out"))
    assert not solved

    def press(t):
        paths[f"/ox/Game/Tile{t:02d}"].v["touch"] = True
        step(2)
        paths[f"/ox/Game/Tile{t:02d}"].v["touch"] = False
        step(2)

    # solve by replaying moves with a simple BFS-free strategy: random legal presses until solved is
    # impractical, so instead verify mechanics: invalid press does nothing, valid press swaps.
    def blank():
        g = board(paths)
        for r in range(4):
            for c in range(4):
                if g[r][c].strip() == ".":
                    return r, c

    def tile_at(r, c):
        return int(board(paths)[r][c])

    br, bc = blank()
    # pick a non-adjacent tile
    far = next((r, c) for r in range(4) for c in range(4)
               if abs(r - br) + abs(c - bc) >= 2)
    before = board(paths)
    press(tile_at(*far))
    assert board(paths) == before, "non-adjacent tile moved"
    moves0 = paths["/logic/post/CntF"].g("out")
    # adjacent press
    nr, nc = (br, bc - 1) if bc > 0 else (br, bc + 1)
    t = tile_at(nr, nc)
    press(t)
    assert blank() == (nr, nc) and tile_at(br, bc) == t, "valid move failed"
    assert paths["/logic/post/CntF"].g("out") == moves0 + 1
    # holding the finger must not oscillate
    paths[f"/ox/Game/Tile{t:02d}"].v["touch"] = True
    step(10)
    paths[f"/ox/Game/Tile{t:02d}"].v["touch"] = False
    step(2)
    assert blank() == (br, bc), "hold did not move exactly once"
    check_perm()

    # solve: undo using a solver on the current board (IDA* is overkill; use reverse of
    # a fresh scramble instead): press SHUFFLE-free path -> brute force with BFS on small scramble
    # Easier: drive tiles to solved using a known-solvable sequence from Python solver.
    from collections import deque

    def state():
        g = board(paths)
        return tuple(0 if x.strip() == "." else int(x) for r in g for x in r)

    goal = tuple(list(range(1, 16)) + [0])
    # A* with manhattan heuristic
    import heapq

    def h(s):
        d = 0
        for i, v in enumerate(s):
            if v:
                d += abs(i // 4 - (v - 1) // 4) + abs(i % 4 - (v - 1) % 4)
        return d

    s0 = state()
    pq = [(h(s0), 0, s0, [])]
    seen = {s0: 0}
    path = None
    while pq:
        f, gc, s, p = heapq.heappop(pq)
        if s == goal:
            path = p
            break
        z = s.index(0)
        for dz in (-1, 1, -4, 4):
            n = z + dz
            if n < 0 or n > 15 or (dz in (-1, 1) and n // 4 != z // 4):
                continue
            l = list(s)
            l[z], l[n] = l[n], l[z]
            ns = tuple(l)
            if seen.get(ns, 1e9) > gc + 1:
                seen[ns] = gc + 1
                heapq.heappush(pq, (gc + 1 + 1.5 * h(ns), gc + 1, ns, p + [s[n]]))
        if len(seen) > 2_000_000:
            break
    assert path is not None, "solver gave up"
    print("solving in", len(path), "presses")
    for t in path:
        press(t)
    step(25)
    print("\n".join(" ".join(r) for r in board(paths)))
    assert state() == goal
    assert paths["/logic/post/Solved"].g("out", False), "solved flag not set"
    print("SOLVED flag OK, moves:", paths["/logic/post/CntF"].g("out"))

    # SHUFFLE button re-scrambles and clears the flag/counter
    paths["/ox/Game/Shuffle"].v["touch"] = True
    step(2)
    paths["/ox/Game/Shuffle"].v["touch"] = False
    step(120)
    check_perm()
    assert state() != goal and not paths["/logic/post/Solved"].g("out", False)
    assert paths["/logic/post/CntF"].g("out") == 0
    print("re-shuffle OK")


def astar(s0):
    """Weighted A* on a 16-tuple (0 = blank); returns the list of cell indices to press."""
    import heapq
    goal = tuple(list(range(1, 16)) + [0])

    def h(s):
        return sum(abs(i // 4 - (v - 1) // 4) + abs(i % 4 - (v - 1) % 4)
                   for i, v in enumerate(s) if v)

    pq = [(h(s0), 0, s0, [])]
    seen = {s0: 0}
    while pq:
        _, gc, s, p = heapq.heappop(pq)
        if s == goal:
            return p
        z = s.index(0)
        for dz in (-1, 1, -4, 4):
            n = z + dz
            if n < 0 or n > 15 or (dz in (-1, 1) and n // 4 != z // 4):
                continue
            l = list(s)
            l[z], l[n] = l[n], l[z]
            ns = tuple(l)
            if seen.get(ns, 1e9) > gc + 1:
                seen[ns] = gc + 1
                heapq.heappush(pq, (gc + 1 + 1.5 * h(ns), gc + 1, ns, p + [n]))
        if len(seen) > 2_000_000:
            return None


def main_v2():
    """aspirinV2.sax: fixed cells, numbers shown via each cell's `in`, empty cell recoloured."""
    tops, paths = load("aspirinV2.sax")
    for c in paths.values():
        c.start()
    now = 0
    goal = tuple(list(range(1, 16)) + [0])
    cell = [paths[f"/ox/Game/Cell{i:02d}"] for i in range(1, 17)]

    def step(n=1):
        nonlocal now
        for _ in range(n):
            now += SCAN_MS + random.randint(-3, 3)
            run_scan(tops, now)

    def state():
        return tuple(int(c.g("in")) for c in cell)

    def check():
        s = state()
        assert sorted(s) == list(range(16)), s
        for v, c in zip(s, cell):          # empty cell = board colour, numbers on white
            assert int(c.g("backgroundColor")) == (0x31A6 if v == 0 else 0xFFFF), (s, v)

    def show():
        s = state()
        return "\n".join(" ".join(f"{v:3d}" if v else "  ." for v in s[r * 4:r * 4 + 4])
                         for r in range(4))

    def solved():
        return paths["/logic/post/Solved"].g("out", False)

    def moves():
        return paths["/logic/post/CntF"].g("out")

    def press(k):
        cell[k].v["touch"] = True
        step(2)
        cell[k].v["touch"] = False
        step(2)

    step(3)
    assert state() == goal, "boot did not load the solved board: %s" % (state(),)
    step(120)
    check()
    print("after shuffle:\n" + show())
    assert state() != goal and not solved() and moves() == 0

    z = state().index(0)
    far = next(k for k in range(16) if abs(k // 4 - z // 4) + abs(k % 4 - z % 4) >= 2)
    before = state()
    press(far)
    assert state() == before, "non-adjacent cell moved"
    press(z)
    assert state() == before, "pressing the empty cell changed the board"
    n = z - 1 if z % 4 else z + 1
    v = before[n]
    press(n)
    s = state()
    assert s[n] == 0 and s[z] == v and moves() == 1, "valid move failed"
    cell[z].v["touch"] = True              # hold: exactly one move back
    step(10)
    cell[z].v["touch"] = False
    step(2)
    assert state() == before and moves() == 2, "hold did not move exactly once"
    check()

    path = astar(state())
    assert path is not None, "solver gave up"
    print("solving in", len(path), "presses")
    for k in path:
        press(k)
    step(5)
    print(show())
    check()
    assert state() == goal and solved(), "solved flag not set"
    print("SOLVED flag OK, moves:", moves())

    paths["/ox/Game/Shuffle"].v["touch"] = True
    step(2)
    paths["/ox/Game/Shuffle"].v["touch"] = False
    step(120)
    check()
    assert state() != goal and not solved() and moves() == 0
    print("re-shuffle OK")


if __name__ == "__main__":
    import sys
    if "--solver" in sys.argv:
        main_solver()
    elif "--v2" in sys.argv:
        main_v2()
    else:
        main()