In formal methods, this is called a "reachability" property: is it always possible to reach state Y? In this case, "In Neko Atsume, is it always possible to have cat food." So yes, a real thing formal method can help with! - ThreadSky

hillelwayne.com • 40 days ago

In formal methods, this is called a "reachability" property: is it always possible to reach state Y? In this case, "In Neko Atsume, is it always possible to have cat food."

So yes, a real thing formal method can help with!

Reposted from Fatih Altinok

If you spend too much money then you can’t buy cat food, for this there’s a free option so you don’t get locked out of the game and restart.

The devs probably foresaw this but it’s entirely possible to ship with that bug. Do you think formal verification can help in scenarios like this?

Comments

hillelwayne.com•40 days ago

Here's a more "serious" real-world example: once @mat4nier.bsky.social couldn't shut down his computer. We'd say that in Macs, "graceful shutdown" does not satisfy reachability. While most of the time you can reach it just fine, there are SOME cases where it's impossible.

hillelwayne.com•40 days ago

Of course, you can analyze videogames this way, too! This article by Evan Miller is about avoiding "dead man walking" scenarios in adventure games, states where "you've won the game" is impossible. He does it with markov chains, but links an FM paper https://www.evanmiller.org/adventure-games-and-eigenvalues.html

hillelwayne.com•40 days ago

Not all formal methods can verify reachability. One of the most popular specification languages, TLA+, can't do it. It can only prove the strictly stronger property of "liveness": state Y is not just possible, but *guaranteed* to happen. It's stronger because liveness implies reachability.

hillelwayne.com•40 days ago

Consider the statement "if you haven't gotten a game over, the game is always winnable." That's reachability. But there's no guarantee you actually REACH it— you can get bored and stop playing.

But "you always will win the game" implies that winning is always reachable... since you always reach it!

hillelwayne.com•40 days ago

Does this make liveness "better" than reachability? No. Because there are lots of cases where we know for sure that liveness is false, but still want to verify reachability. Graceful shutdown is a good example. It should always be *possible*, but we also should let people run servers indefinitely.

hillelwayne.com•40 days ago

PS: even if a speclang can't express reachability, you can still verify it by finding a different property that implies it. Here I prove a game is winnable by arguing that certain initial conditions guarantee reachability, and verifying those conditions hold

https://www.hillelwayne.com/alloy-randomizer/

fatih.6nok.org•40 days ago

Thanks! “Can’t shut down” is a great example and liveness vs reachability is mind bending.

Since TLA+ can’t prove reachability I’m curious if there are other tools that can?

lorisdanto.bsky.social•40 days ago

Chris Martens worked/works on this type of things

Comments

Posting Rules

Reply