Super Metroid Formal Models Chat.md

Prompt:

Editor's note: The following images come from this tweet.

What's going on in these images?

Suggest a PDDL encoding of Super Metroid's mechanics appropriate to this level of abstraction.

Response:

Planning Domain Definition Language (PDDL) is used to define search problems and domains in AI planning systems. To encode Super Metroid's mechanics at the level of abstraction provided in the images, we would consider states, actions, and objects that are relevant to the game play as shown.

Here's a simplified example of how one might encode the Super Metroid mechanics into PDDL, focusing on the character transformation and energy levels:

pddl(define (domain super-metroid)
  (:requirements :strips :typing :negative-preconditions)

  ;; Define types
  (:types
    location
    character
  )

  ;; Define predicates
  (:predicates
    (at ?c - character ?l - location)
    (is-ball ?c - character)
    (has-missiles ?c - character)
    (has-energy ?c - character)
    (has-full-energy ?c - character)
  )

  ;; Define actions
  (:action morph
    :parameters (?c - character)
    :precondition (and
      (at ?c some-location)
      (not (is-ball ?c))
    )
    :effect (and
      (is-ball ?c)
      (not (has-full-energy ?c))
    )
  )

  (:action unmorph
    :parameters (?c - character)
    :precondition (and
      (at ?c some-location)
      (is-ball ?c)
    )
    :effect (not (is-ball ?c))
  )

  (:action collect-missiles
    :parameters (?c - character)
    :precondition (and
      (at ?c missile-location)
      (not (has-missiles ?c))
    )
    :effect (has-missiles ?c)
  )

  (:action use-missiles
    :parameters (?c - character)
    :precondition (and
      (at ?c some-location)
      (has-missiles ?c)
    )
    :effect (not (has-missiles ?c))
  )

  (:action restore-energy
    :parameters (?c - character)
    :precondition (and
      (at ?c energy-location)
      (not (has-full-energy ?c))
    )
    :effect (has-full-energy ?c)
  )
  
  ;; Possibly more actions for different abilities and interactions...
)

(define (problem super-metroid-problem)
  (:domain super-metroid)

  ;; Define objects
  (:objects
    samus - character
    initial-location missile-location energy-location - location
  )

  ;; Define initial state
  (:init
    (at samus initial-location)
    (not (is-ball samus))
    (not (has-missiles samus))
    (not (has-full-energy samus))
  )

  ;; Define goal state
  (:goal
    (and
      (is-ball samus)
      (has-missiles samus)
      (has-full-energy samus)
    )
  )
)

This PDDL encoding abstracts away many of Super Metroid's complex mechanics for the sake of brevity. The real game includes a wide range of locations, items, enemies, and state variables, which would significantly expand the PDDL domain and problem definitions. Depending on the specific requirements of your simulation or planning problem, you may need to add more detailed actions, predicates, and objects to more accurately represent the game's mechanics.

Prompt:

How can Samus move between locations?

Response:

In a PDDL representation of Super Metroid, moving between locations would be represented by an action that changes Samus's position predicate from one location to another. Here's how you might encode such an action:

pddl(:action move
  :parameters (?c - character ?from - location ?to - location)
  :precondition (and
    (at ?c ?from)
    (adjacent ?from ?to) ; You would define 'adjacent' in predicates.
    ; Additional preconditions can be added if necessary, such as:
    ; (not (is-ball ?c)) if Samus can only move between certain locations in humanoid form.
  )
  :effect (and
    (not (at ?c ?from))
    (at ?c ?to)
  )
)

In the predicates section, you would have something like:

pddl(:predicates
  ...
  (adjacent ?from - location ?to - location)
  ...
)

And in the problem definition, you would specify which locations are adjacent to each other:

pddl(:init
  ...
  (adjacent initial-location missile-location)
  (adjacent missile-location energy-location)
  ; Add more adjacency relations as needed.
  ...
)

This allows Samus to move from one location to another if those locations are adjacent. You could further refine the move action by including requirements for Samus to be in a certain form (such as humanoid or morph ball) to move through specific locations, reflecting the game's mechanics where certain areas are only accessible in certain forms.

Prompt:

Why does the morph/unmorph action mention "some-location"?

Response:

In the PDDL code snippet I provided earlier, the term "some-location" was used as a placeholder to indicate that the action could take place at any location where the character, in this case, Samus, is present. This was a simplification for the sake of the example.

However, to be more precise and correct in PDDL, the location should be a variable that is specified in the parameters of the action. The correct way to define the morph and unmorph actions would be to include a parameter for the location. Here's the revised version:

pddl(:action morph
  :parameters (?c - character ?l - location)
  :precondition (and
    (at ?c ?l)
    (not (is-ball ?c))
  )
  :effect (and
    (is-ball ?c)
    (not (has-full-energy ?c))
  )
)

(:action unmorph
  :parameters (?c - character ?l - location)
  :precondition (and
    (at ?c ?l)
    (is-ball ?c)
  )
  :effect (not (is-ball ?c))
)

In this revised version, the placeholder "some-location" has been replaced with a variable "?l - location" that represents any given location. The action is then defined so that Samus can only morph or unmorph if she is at a specific location, which is a more accurate representation of the game's mechanics. The location is specified when the action is used in the problem definition.

Prompt:

Would it be safe to just drop ?l from the action?

Response:

In PDDL, if a particular action does not depend on the location (or any other parameter) for its preconditions or effects, you can indeed drop that parameter from the action definition.

If the morphing action in Super Metroid does not depend on Samus's specific location (i.e., she can morph/unmorph anywhere), you could define the morph and unmorph actions without including a location parameter. Here's how the actions would look:

pddl(:action morph
  :parameters (?c - character)
  :precondition (not (is-ball ?c))
  :effect (and
    (is-ball ?c)
    (decrease (energy ?c) 30) ; assuming morphing uses energy
  )
)

(:action unmorph
  :parameters (?c - character)
  :precondition (is-ball ?c)
  :effect (not (is-ball ?c))
)

In this example, the morph action requires that the character is not already in ball form to execute the action, and similarly, the unmorph action requires that the character is in ball form. The location parameter is omitted, implying that the action is not location-dependent.

However, it's important to remember that the accuracy of this simplification depends on the mechanics of the specific game or system you are modeling. If location does matter in some cases (such as needing to be at a specific location to access an ability or interact with an object), then the parameter should be included and properly handled in the action's preconditions and effects.

Prompt:

Can you re-express this model in Promela?

Response:

Promela (PROcess MEta LAnguage) is a verification modeling language used by the SPIN model checker to describe system behavior in terms of processes, messages, and synchronization. In Promela, we would model the system as a set of processes that can execute actions concurrently, with channels for inter-process communication if necessary.

Here's a very simplified version of how you might start to represent the mechanics of Super Metroid in Promela, focusing on the morphing ability:

c// Promela code
mtype = { morph, unmorph, move, collect_missile, use_missile, restore_energy };

// Represents Samus's state
typedef Character {
  bool isBall;
  bool hasMissiles;
  int energy;
};

// Processes representing actions
proctype Morph(Character c) {
  if
  :: (c.isBall == false) -> c.isBall = true; c.energy -= 30;
  fi;
}

proctype Unmorph(Character c) {
  if
  :: (c.isBall == true) -> c.isBall = false;
  fi;
}

// initial process
init {
  Character samus = { false, false, 99 };

  do
  :: run Morph(samus);
  :: run Unmorph(samus);
  // Add other actions and synchronization as needed
  od;
}

In this Promela model:

• mtype is used to define a message type enumeration, which is not utilized in this particular snippet but can be used for defining communication messages between processes if needed.
• Character is a typedef struct that represents the state of Samus, including whether she is in ball form, whether she has missiles, and her current energy level.
• Morph and Unmorph are proctype definitions that act as functions to change the state of the character. They check the conditions and then perform the action if the conditions are met.
• The init process initializes Samus's state and then enters a loop where it can run the Morph and Unmorph actions. This is a non-deterministic choice indicating that at any point in time, the system can choose to execute either action.

This model is greatly simplified and would need to be expanded to include locations, more detailed state management, and synchronization between processes to accurately represent all of Super Metroid's mechanics. It also assumes that energy is an integer and that morphing costs a fixed amount of energy; these assumptions would need to be adjusted to match the game's actual mechanics.

Prompt:

Yeah yeah. Now do NuSMV.

Response:

NuSMV is a symbolic model checker that can be used to verify the correctness of finite state systems. To express the Super Metroid mechanics in NuSMV, we would define a model using states and transitions. Here's a simplified NuSMV model focusing on the morphing ability and movement between locations:

smvMODULE main

-- Enumeration for character form
SYMBOLIC_CONSTANTS = { HUMANOID, BALL };

-- Samus' state representation
VAR
  form: SYMBOLIC_CONSTANTS; -- Samus can be in HUMANOID or BALL form
  hasMissiles: boolean; -- Whether Samus has missiles
  energy: 0..99; -- Energy level of Samus
  location: {INITIAL, MISSILE_LOCATION, ENERGY_LOCATION}; -- Possible locations

ASSIGN
  init(form) := HUMANOID;
  init(hasMissiles) := FALSE;
  init(energy) := 99;
  init(location) := INITIAL;

-- Transition for morphing ability
TRANS
  case
    form = HUMANOID & next(form) = BALL : energy > 30; -- Can morph if energy is sufficient
    form = BALL & next(form) = HUMANOID : TRUE; -- Can always unmorph
    TRUE : form = next(form); -- Stay in the same form
  esac

-- Transition for missiles collection
TRANS
  case
    location = MISSILE_LOCATION & next(hasMissiles) = TRUE : TRUE; -- Can collect missiles at the missile location
    TRUE : hasMissiles = next(hasMissiles); -- Missiles state remains unchanged
  esac

-- Energy management
TRANS
  case
    form = HUMANOID & next(form) = BALL : next(energy) = energy - 30; -- Energy decreases when morphing
    location = ENERGY_LOCATION : next(energy) = 99; -- Energy restores at energy location
    TRUE : energy = next(energy); -- Energy stays the same
  esac

-- Movement transitions
TRANS
  case
    form = HUMANOID & next(location) != INITIAL : TRUE; -- Can move from INITIAL in HUMANOID form
    form = BALL & next(location) != INITIAL : TRUE; -- Can move from INITIAL in BALL form
    TRUE : location = next(location); -- Stay at the same location
  esac

In this NuSMV model:

• We define symbolic constants to represent the different forms that Samus can take.
• Samus's state is represented by variables for her form, whether she has missiles, her energy level, and her current location.
• The ASSIGN section initializes Samus's state at the start of the game.
• The TRANS sections define the possible transitions for Samus's state. These include the conditions under which she can morph/unmorph, collect missiles, restore energy, and move between locations.

This model is also greatly simplified and would need more detail to fully represent the mechanics of Super Metroid. NuSMV can then be used to check properties of the model, such as reachability of certain states or the invariance of certain conditions throughout gameplay.

Prompt:

Suppose I were going to show you a sequence of images from the game annotated with which actions the player took using their controller in between them (e.g. "hold d-pad left" or "press x"). Through conversation, we would create and refine an abstracted model of the game's mechanics. I don't have that data in-hand right now, but I want to know what the conversation would look like.

Yeah yeah. That all sounds nice. What if I just gave you access to the game running in an emulator? You could write scripts to set the controller state, advance simulated time, and extract screenshots to look at? Your scripts could even record the precise value of certain memory cells over time in between the sampled screenshots. Would that work?

Response:

If you provided access to a game running in an emulator with the ability to script controller states, advance simulated time, and extract screenshots, the process would be much like conducting controlled experiments. The scripting capabilities would allow us to explore the game's mechanics methodically and create a model based on observed behavior.

Here's what the conversation and process might look like:

1. Identifying Variables and Actions: We would start by identifying key variables and actions to script. For example, player position, health, inventory, or game score could be tracked, as well as actions like jumping, shooting, or moving.

2. Scripting Actions: We would write scripts to perform specific actions, like "press x" to jump. These scripts would run for a set period or until a certain condition is met.

3. Advancing Time: The emulator would advance time, allowing the game to process the scripted actions. We could advance frame by frame or by larger time steps as needed.

4. Capturing Data: Screenshots would be taken before and after the action, and the values of relevant memory cells would be recorded. This could include the player's position, state changes, or any other relevant data.

5. Building the Model: Using the data collected, we would build an abstract model of the game's mechanics, focusing on the relationships between actions, game states, and outcomes.

6. Refinement: The model would be refined through iteration. We would adjust our scripts based on the model's predictions and compare the outcomes to the model's expectations, refining as necessary.

7. Validation: Once we believe our model accurately reflects the game's mechanics, we would validate it by predicting the outcome of a sequence of actions and comparing it to the actual result.

8. Discussion and Analysis: Throughout this process, we would discuss findings, interpret data, and ensure that the model aligns with the game's observed behavior.

If you were to provide access to an emulator, it would indeed facilitate a much more nuanced and precise understanding of the game's mechanics. However, my current capabilities as an AI model do not include interacting directly with software or hardware, such as running a game emulator or executing scripts outside of a predefined environment. My role in such a process would be to assist with the design and interpretation of experiments, the formulation of hypotheses, and the creation of models based on the data you provide.

Prompt:

Editor's note: These code snippets come from (SuperMetroidCheating.ipynb)[https://colab.research.google.com/drive/1OBTQ7ofABZqxco4G3gqBcoMGx80GXkeF?usp=sharing].

In light of our discussion so far, what do you think is going on with the following Python snippet? begin(colony_state) assert peek(roomstate_pointer) == 22278 press(RIGHT) step(30) release() step(30) teleport(dy=128) step() teleport(dy=128) step() teleport(dy=128) step() teleport(60,64) press(RIGHT) step_through_door() assert peek(roomstate_pointer) == -24828 step(30) press(RIGHT+A) step(90) press(RIGHT) step(120) step_through_door() assert peek(roomstate_pointer) == -5884 release() for i in range(5): teleport(dy=16) step(30) press(RIGHT) step(60) step_through_door() assert peek(roomstate_pointer) == 13060 step(30) for i in range(8): teleport(dx=16) step(30) step_through_door() teleport(dx=128) step(60) step_through_door() assert peek(roomstate_pointer) == -14590 ridley = emu.get_state() render()

Very good. Here's a bit more for context: samus_x = 0x0AF6 samus_y = 0x0AFA samus_health = 0x09C2 room_transition = 0x0797 roomstate_pointer = 0x07BB game_state = 0x0998 def peek(addr): return frombuffer(memoryview(emu.get_state())[zeropage_offset:zeropage_offset+zeropage_len],dtype='<i2')[addr//2] def poke(addr, value): hacked_state = bytearray(emu.get_state()) hacked_state_view = frombuffer(memoryview(hacked_state)[zeropage_offset:zeropage_offset+zeropage_len],dtype='<i2') hacked_state_view[addr//2] = value hacked_state = bytes(hacked_state) emu.set_state(hacked_state) def teleport(dx=None,dy=None): if dx is not None: poke(samus_x, peek(samus_x)+dx) if dy is not None: poke(samus_y, peek(samus_y)+dy) def press(buttons): emu.set_button_mask(buttons, 0) def release(): emu.set_button_mask([0]*12, 0) def step_through_door(): while peek(room_transition) == 0: step(10) while peek(room_transition) > 1: step(30) super_frames = [] frames = [] rams = [] def step(times=1): local_frames = [] for _ in range(times): emu.step() rams.append(gamedata.memory.blocks[0]) local_frames.append(emu.get_screen()) if times > 1: frames.append(array(local_frames[:-1]).mean(0).astype('u1')) frames.append(emu.get_screen()) def begin(state): frames.clear() rams.clear() emu.set_button_mask([0]*12,0) emu.set_state(state) frames.append(emu.get_screen()) import IPython.display import imageio import base64 def render(): super_frames.extend(frames) imageio.mimwrite('render.gif', array(frames)[::1,::2,::2], format='gif', fps=15) anim = IPython.display.Image(filename='render.gif') anim.width = 256 return anim locals().update(zip(SNES_BUTTON_NAMES, eye(12)))

Response:

Given the additional context and the Python snippet you've shared, it looks like you're working with a script that interacts with an emulator for a game, possibly Super Metroid based on the mention of "Ridley" and "Samus" in the context. The script is designed to automate control input, manipulate game state, and observe the game's response in a structured and repeatable way. Here's a breakdown of the key components and what they are doing:

• Memory Access Functions (peek and poke): These functions are used to read (peek) and write (poke) values directly into the game's memory. This allows for direct manipulation of game state variables like Samus's position (samus_x, samus_y), health (samus_health), and the current room state (roomstate_pointer).

• Control Functions (press, release): These functions simulate pressing and releasing buttons on the game controller. This allows the script to control the game as if a player were providing input.

• teleport Function: This function directly modifies Samus's coordinates in the game's memory, effectively "teleporting" her to a new location. This is a powerful tool for exploring the game's mechanics by bypassing normal movement constraints.

• Game Progression Functions (step, step_through_door): The step function advances the game by a specified number of frames, allowing the script to observe the game's state over time. The step_through_door function is a higher-level abstraction that moves the game through room transitions, handling the waiting and checking involved in moving from one room to another.

• begin and render Functions:begin initializes the emulator state for a new sequence of actions, while render compiles the captured frames into an animation. This is useful for visualizing the sequence of actions and their effects within the game.

• The Main Script Body: The script sequences a series of actions (button presses, teleports, etc.) and asserts about the game state (roomstate_pointer). It's structured to test or demonstrate specific interactions or behaviors within the game, such as navigating through rooms, triggering events, or manipulating Samus's state in specific ways.

This approach allows for detailed experimentation and analysis of game mechanics, enabling the creation of a precise and nuanced model of the game's behavior. It could be used for a variety of purposes, including speedrun strategy development, bug testing, game mechanic exploration, or academic research into game design and interactive media.

Prompt:

Knowing all that, what's going on in the following snippet? begin(ridley) assert peek(roomstate_pointer) == -14590 release() step(10) step(10*60) poke(samus_health,28) # set health below 30 to be done with ridley step(20*60) teleport(dx=-32,dy=-64) press(LEFT) for i in range(10): step(5) step_through_door() assert peek(roomstate_pointer) == -26876 escape = emu.get_state() render()

Response:

This snippet appears to be scripting a sequence of actions within a game emulator, specifically targeting a boss battle with Ridley, one of the antagonists in the Metroid series. Here’s a step-by-step breakdown of what the script is doing:

1. Initialization with begin(ridley): The script starts by initializing the emulator's state to a predefined state labeled ridley. This likely corresponds to the beginning of the Ridley boss fight or just before it. The initial game state ensures a consistent starting point for the scripted sequence.

2. Initial Assertion: It asserts that the roomstate_pointer is at a specific value (-14590), verifying that the game is in the expected state or room. This is likely the memory address value corresponding to Ridley's room.

3. Releasing All Buttons: The release() function call ensures no buttons are pressed as the script starts executing the planned sequence.

4. Advancing Time: The script advances the game by 10 frames, followed by another 600 frames (10 seconds, assuming 60 frames per second). This allows any ongoing animations or events to conclude and stabilizes the game state for the scripted actions to follow.

5. Setting Samus's Health:poke(samus_health, 28) directly sets Samus's health to 28, presumably to simulate reaching a critical health threshold that is required to end the Ridley fight. In many Metroid games, Ridley will either leave or be defeated when Samus is at a critically low health level, allowing the player to progress.

6. More Time Advancement: The game is then advanced by another 1200 frames (20 seconds), giving time for the Ridley encounter to recognize the health change and proceed to its conclusion.

7. Teleporting Samus:teleport(dx=-32, dy=-64) moves Samus's position, likely positioning her for the next scripted action or to navigate out of the area post-battle.

8. Pressing Left and Advancing: The script simulates pressing the LEFT direction and advances the game for 50 frames (10 iterations of 5 frames each). This could be to move Samus towards an exit or to align her for the next action.

9. Exiting Through a Door:step_through_door() is called to navigate Samus through a door transition. This function likely waits until a door transition is detected (the game recognizes Samus is exiting the room) and then continues to advance the game until the transition is complete.

10. Final Assertion: It asserts that the roomstate_pointer is at another specific value (-26876), verifying that Samus has successfully moved to the expected next room or state following the Ridley encounter.

11. Saving State and Rendering: Finally, the escape state is saved (presumably the state after escaping Ridley's encounter), and the render() function is called to generate a visual representation (likely a GIF) of the scripted sequence.

This script automates a critical part of a boss battle, including managing health to trigger the end of the fight and navigating out of the boss room, all in a controlled, repeatable manner for testing, demonstration, or analysis purposes.

Editor's note: The the result of the larger script from which this snippet was taken can be seen in this short video on YouTube.