I always think of finite state automata, but these adventure games with all the different inventory and actions can be remarkably hard to model.
For instance, if you don't model that the player can drop an object after finding it, you can't guarantee that they'll have it when they need it. So, using the original post's game, Alice needs the red key to get to the red room (final goal). Let's say it was in the west room, also with the green key, where Alice begins the game. She grabs the green key, goes east, hands it to Bob who heads west. Now Alice cannot move. This particular game is solvable because Bob can grab the red key and take it to Alice, but not every game permits this recovery action. Supposing it only had the one player character, and the keys were consumable (as happens in some games). She has no way to return.
The dependency chart only shows that she can solve the puzzle, not that she can always solve the puzzle (that there exists a path, not for all paths), until it gets a lot more detail than a hand-drawn graph is likely to get.
One of the more notorious dungeons in the series is the Water Temple in Ocarina of Time, which contained a sequence that would allow the player to use a small key for an optional area that, critically, did not refund the small key. This allowed the player to become permanently stuck, unable to advance through the dungeon and complete the game.
It looks like the dungeon is set up with a few carefully designed chokepoints using the water level mechanics to stop players from going too far down the wrong path:
Unfortunately, the author also claims there is an alternate way to ruin your game in the water temple that they'll cover in a follow-up article, but that article doesn't exist.
This was a problem in the original Monkey Island: you could throw some leaflets in a fire, but you needed them in order to convince a local tribe to give you a key.
I would like to know more about how this works:
> The formal verification tool effectively runs this function with all possible seed values and checks if the assert() is violated in any of the cases. But it uses a more much efficient method to accomplish this than running the function
2^32 (approximately 4 billion) times.
Or are the "prove_" functions some sort of DSL that don't actually get executed as ordinary C code?
What was the point of publishing this information in such a non-functional format? Is this an example of minimalism taken too far (not even an anchor tag for the twitter link) or is this some publishing standard I'm not aware of?
I feel like the document could have benefited a great deal from some simple font color styling. I guess in its current format it can easily be copy-pasted somewhere else and still look exactly as it does?
Apart from the links not working, that's as functional as it gets for conveying text-based information. All the rest is fluff and the bytes to information ratio gets very bad, very fast (e.g. several MB to read a 1000 word CNN.com article).
Although the question make me fell a little old. How young are you buddy, for this is a plain old textfile -- used to be a very very common way to convey information. Last generation's GitHub readme.md files so to speak.
In fact, if one wants to know more about the phenomenon of textfiles, and read some classic stuff along the way: http://www.textfiles.com/directory.html
25, so I grew up reading most of my content on wikipedia or forum posts, which is about the level of markup I mean (minus the ridiculously huge banner signatures that people were so fond of on invision forums ;) )
You make it sound like this is a big publication I worked weeks on. :) It's not. It's a toy project I wrote Saturday.
As far as "publishing" goes: I sent a tweet about it in the hopes someone might find it interesting. And now it's trending on Hacker News! Woohoo! ^_^
The link is just a deep link into my SVN repo, directly to the README file.
For the record, my weekend project this Easter was to watch the first season of The Expanse...
/That's/ a non-functional format. Given the choice of everyone being time.com or everyone being like this website, I'd happily return to the days of amazing ascii art.
It's a shame mobile browsers are so dysfunctional that they struggle to cope with plain text or minimally marked up HTML, but the blame lies with the browsers, not the content.
With no zoom the linebeaks are uncomfortable (which is ok, because EOL is difficult) http://imgur.com/9QulRkn
Zoom shows combination of uncomfortable linebreaks and horizontal scrolling: https://imgur.com/ti7gGMV
Reader mode does reflow the lines, but prevents zoom. (Also destroys ASCII diagrams).
None of these combinations are good.
To adjust this settings users need to go to settings and adjust text size and then to accessibility and adjust text size.
I'm not making a judgement call, I'm trying to learn.
Articles or links can be submitted by anyone not necessarily content authors.
Further I think a lot of people here (myself) included are quite happy with plain-text (it loads fast, it works well with various font/screen sizes) - note also that the README is in fact markdown formatted, so feel free to open it in your reader of choice.
Is it? How do you see that? Or is that a different link?
Why doesn't my browser render markdown?
A stronger example of the problem is, I think, some of the text from 4AM documenting their ongoing reverse-engineering efforts, for example: https://ia600509.us.archive.org/6/items/Muppetville4amCrack/...
The 40col text might be "retro", but it also makes lines wrap so soon that my eyes get tired reading it. (And yet—unlike e.g. an RFC file—I can't just plop it into a Markdown parser or what-have-you to get reflowable lines of HTML out, because 1. it's not really in any particular format, and 2. the alternating "prose text", "formatted console interaction", and "formatted ASM listing with long prose comments beside them" sections aren't demarcated or delimited in any particular way.)
When your text becomes sufficiently "simple", it can actually become an accessibility problem.
Actual point: Dear gods that 4am crack is awful to read, and I'd actually prefer github angry fruit salad in spite of mostly hating the latter.
So, yeah, there are virtues to simplification, but it can still be overdone - and while the article we're commenting on was great to me, it probably overdid it slightly - and the link you provide is an unintentional reductio ad absurdum of the approach.
(long comment written because I expected to disagree with you until I clicked and went aaaaaaaaaaaaaaaaaa)
Here's a blog post I've always found interesting about Markdown, from Joe Armstrong: http://joearms.github.io/2016/03/21/Why-Markdown-Sucks.html
Plain text documents don't solve the problem he's talking about, but they at least mitigate it somewhat -- WYSIWYG is preferable to a changing pseudo-standard mangling an author's intent, in my opinion.
It could have been worse, they could have published it some binary format!
Maybe some CSS to font-color the code to make it more readable? I like that in my IDE and I doubt it would cost much.
Maybe in-document anchor tags to allow linking to certain sections?
Vehemently opposed to your other suggestions. But I'm weird and cranky, and very much miss the days of most of computing being done in plain text. It's really the first and only universal data format/API.
The place to make plaintext pretty (if you care) is in the user's editor of choice where they can customize to their hearts content.
I do know I'm in the very tiny minority with this opinion though.
Remember when the internet was just plain text and ASCII art? Pepperidge Farm remembers.
Or are you talking about the way way back? I wasn't around for that.
Why is that up to the document and not the user agent? The user agent can be configured so that all documents like nice and uniform.
I'm thinking that would be a great way to naturally practice reading comprehension since it forces you to think about what you read.
I played these, and also Zork, Enchanter, and so forth, around that age, with my father doing most of the typing, and loved them. As I got older we moved into more (read: extremely) challenging titles like Witness and Deadline.
Of possible interest:
Edit: Looks like you're better off buying them used off eBay.
Sometimes romance and adventure are combined, such as in "Escape from Fire Island!" , also from the "Date with Destiny" series.
Maybe not the best for young readers, though, as it is not aimed at younger readers:
It was supposed to be a nice, relaxing
weekend—with a little swimming, a lot of
cocktails, and more hot bods than a year’s
subscription to Men’s Health magazine. But when a
vat of radioactive waste washes onto the beach,
strange things start happening—and now an army of
zombie drag queens is storming the coast! Can you
save Fire Island before it’s too late? Or will you
perish at the hands of a thousand shrieking divas?
It all depends on the choices YOU make.
If you run toward the nearest ferry terminal, turn
to page 44. If you flirt with the cute twink, turn
to page 55. If you throw caution to the wind and
join the nearest circuit party, turn to page 80.
Now, if you built a game isomorphic to a traveling salesman problem, or other exponential problem, then the model checker might have a problem with that. But so would a human; such a game would get extremely tedious. So, I'd venture as far as "this should scale to adventure games that humans enjoy playing".
I did some work on formally modeling game mechanics in answer-set programming  for a prototyping system a few years ago , and in my case model size rather than complexity was almost always the bottleneck. And the biggest model-size culprit was just numerical stuff. If you have a game with a lot of numerical state variables (e.g. health of units), you get big explosions in the size of the state space, which even when the queries are trivial, end up taking the solver longer just to construct the space than solving complex problems in smaller state spaces does. By contrast very discrete-type games (that don't involve a lot of numerical status meters) worked great, even if they have a complex logical structure and you have complex questions to ask about their possibility space. However if you do have a numerically heavy game, SMT solvers can handle that too (the "modulo" part of satisfiability modulo theories can factor out things like the "theory of integers"). In my case I used ASP, specifically the Potassco suite , because imo the modeling language is friendlier, especially for incremental modeling, and I was more interested in investigating expressivity than scaling at the time.
 Some papers: http://www.kmjn.org/publications/Mechanics_AIIDE08-abstract...., http://www.kmjn.org/publications/Playtesting_AIIDE09-abstrac..., http://www.kmjn.org/publications/Ludocore_CIG10-abstract.htm...
I'm not sure that premise holds. Admittedly it's a different genre, but a lot of puzzle games are in exponential/NP-Hard/NP-Complete spaces. Tetris is an obvious example as a simple reduction of the packing problem. Humans very much enjoy playing those.
Even just restricting it to the genre of "adventure games", I'd be hesitant to say that there can't be games with very complex state spaces that humans enjoy playing. Maybe especially with "adventure games" where if the story and writing are interesting enough players will put up with a very wide variety of puzzles and exploration styles.
And is unwinnable.
I'm talking about adventure-style games that have a defined solution and way to "win", and the complexity of computing that solution. In that regard, games that require a full backtracking search and aren't amenable to shortcuts tend to become tedious.
As an example, it's entirely possible to build an adventure game puzzle equivalent to an arbitrary SAT problem.
I'm really not sure about this one. Consider for example a savefile in an Angband-variant and whether a character can leave the dungeon alive (that's easy to define formally '@' on tile '>' with at 1 free turn seq and hp > 0), but I imagine the backtracking is going to be a very expensive computation...
The only tricky bit is you want to avoid modelling the exact pixel location of every object / player if at all possible, but need to make sure your simplifications don't end up hiding some unsolvable corners.
And you could render the room unreachable if you did things in the wrong sequence.
If it gets to conditional / puzzle evaluation that starts to get Turing Complete, then it will hit the halting problem, which I believe is thought to be noncomputable for nontrivial graphs / code.
I imagine it's harder to find an active one now, but even a "dead" one that's still online should be somewhat playable. Just harder to learn and advance without other players.
In the example (simple) game in the post, a player character may be able to pass into the red room and "win", but perhaps there's no condition for returning and the game only terminates when both make it to their individual rooms. If the other character lacks the keys to move through the green and blue doors, then they will be stuck and the game won't terminate. This is easy to guard against in a small game (small state space, easy to manually or mentally compute), but in larger games it's almost trivially easy to cause these sorts of dead-end states. Consider the puzzles of Sokoban, where pushing a block onto certain walls or a corner prevent further progress and require a restart. Now, that's part of the game in that case, but perhaps a designer wants to prevent (in their puzzles) this sort of situation from occurring. This sort of analysis of the game model (states and actions) will help them prevent it.
It is especially important because of how frustrating the resulting loss is; it does not even have the dignity that you get from killing Vivec in Morrowind, where the game informs you "sorry, this game just became unwinnable." You just wander around after doing a bunch of actions that made sense at the time, not realizing that your brother Ralph was twisted up in some crazy voodoo plot. "Yes, Alice, I see that you have pains in your arm that you think come from some voodoo doll, I don't see how that has any relevance to anything though: I've searched this whole damn city and there are no voodoo dolls anywhere." Until later "Oh wait... there was that one alley on the other side of the mob lair, it looked empty at the time but what if that's where Ralph is now?"
See http://ifwiki.org/index.php/Cruelty_scale . Not only do they have dead-ends, but sometimes you don't realize you've hit one until long after you do the thing that set you down the unwinnable path.
It gets worse -- there are a bunch of tools you go by throughout the game. If you fail to pick up any of them, that one will be the one you need to open one of the final doors.
It's a nasty little game, really.
I guess if I were doing it again nowadays I'd be going for a tool-assisted... umm... speedrun isn't really right here, so win-at-all-run.
Getting rid of dead ends makes some of these games feel like they are on rails. If you try enough combos of everything, eventually you'll progress.
I think its important that there is no state were you just get stuck, you should at least have a game over sequence, so that you know you have done something wrong.
...classic Infocom games had plenty of dead-ends :)
Some do by accident, for example if you can proceed to the next location in the game without an object you need to solve the challenge in it and without the ability to return to the previous one.
... no "dead ends". I.e. all player actions will result in a state in which the game is still winnable
- then, yes, fairly common, although not always intentionally.
A dead lock occurs when a state is reached and there is no way to exit the state. In complex state machines it is important insure they are 'deadlock free.' Sometimes people use a timeout to recover from a locked state machine, sometimes the system needs to be re-powered.
An adventure game is simply a state machine (or a collection of interlocked state machines). So proving the proving the game has no deadlocks will also prove that the state machine has no deadlocks.