1. 5
  1.  

  2. 1

    Cool stuff! I’ve been playing with a similar idea. There’s this thing call Alttprandomizer, which takes the Zelda: A Link to the Past ROM and shuffles the contents of the chests. So where you should have gotten a few bombs, you might instead get the master sword, or a single rupee. What makes this interesting is that some of the chests require you to have certain items to reach them. For example, you might need the hookshot to cross a gap, or the moon pearl to survive in the dark world. How do you guarantee your randomizer doesn’t make the game unwinnable?

    One way you can do it is by, for each chest, listing the items that can unlock it:

    \* This is a TLA+ spec
    ShuffledItems \in Items -> Chests
    RequiredItems == [Chests -> SUBSET Items] \* A bit handwavy here
    Reachable(chest) == 
      \/ RequiredItems[chest] = {} 
      \/ \A item \in RequiredItems[chest]: Reachable(ShuffledItems[item])
    
    NoUnreachable == \A chest \in Chests: Reachable(chest)
    

    Bit of handwaving here (sometimes you can unlock a chest in several different ways, and the syntax isn’t exact), but then you can validate that, for a given randomization algorithm, NoUnreachable holds.

    Of course it’s going to be slow as molasses due to combinatorial explosion. TLA+ isn’t that good at atemporal problems. I think Alloy would be ideal here, but I don’t know it anywhere close to well enough to try mocking it out.