law assist_too_early

minebender-game@1.0.0.0 · LAWS.bend:492

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/game.bend as G

492# LAW: "Pressing the assist when some cell is provably safe loses, and shows
493# a provably safe cell; the knowledge is unchanged."
494law assist_too_early:
495  for w: Nat
496  for h: Nat
497  for layout: T.Grid(Bool)
498  for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
499  for g: G.Game
500  for r: Reachable(w, h, layout, g)
501  for playing: {G.status(g) == T.Playing{} : T.Status}
502  for q: T.Pos
503  for option: ProvablySafe(G.knowledge(g), q)
504  for k: Nat
505  exs p: T.Pos
506  ProvablySafe(G.knowledge(g), p) &
507  {G.status(G.step(g, T.Assist{k})) == T.Lost{T.AssistTooEarly{p}} : T.Status} &
508  {G.knowledge(G.step(g, T.Assist{k})) == G.knowledge(g) : T.Knowledge}