ArdaandClaude Opus 5.5
0728acd99a
- gen_aspirin.py generates aspirin.sax (playable) and aspirin_solver.sax (30-move shuffle, then one inverse move per second) from stock kits - build.py compiles with sedonac and packages simulator backup zips - verify_logic.py models the Sedona scan engine to test both apps offline - viewer/OxViewer.java shows the headless simulator's screen live over SOX Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
351 lines
12 KiB
Python
351 lines
12 KiB
Python
"""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")
|
|
|
|
|
|
if __name__ == "__main__":
|
|
import sys
|
|
main_solver() if "--solver" in sys.argv else main()
|