{"id":96,"date":"2018-09-17T22:23:38","date_gmt":"2018-09-17T22:23:38","guid":{"rendered":"http:\/\/www.mbarsinai.com\/blog\/?p=96"},"modified":"2018-09-17T22:23:38","modified_gmt":"2018-09-17T22:23:38","slug":"the-curious-case-of-the-maze-walker-and-the-cows-tail","status":"publish","type":"post","link":"https:\/\/www.mbarsinai.com\/blog\/2018\/09\/17\/the-curious-case-of-the-maze-walker-and-the-cows-tail\/","title":{"rendered":"The Curious Case of the Maze Walker and the Cow’s Tail"},"content":{"rendered":"

The Backslash Incident<\/h2>\n

I guess it\u2019s never a good time to find out your code has bugs. But there are exceptionally bad times to do so. A middle of a live demo is one such example. Immediately after said demo, when you\u2019ve invited the attendees to take your code for a spin, is not too good either.<\/p>\n

Case in point: I had the honor of presenting BPjs<\/a> at a seminar at Harvard School of Engineering and Applied Sciences (SEAS). BPjs is a tool suite for running and verifying programs written in JavaScript, using the Behavioral Programming<\/a> programming paradigm. In short (very very very short): It\u2019s a paradigm that focuses on how the system should behave, rather than on how its implemented (e.g.\u00a0objects, functions, or procedures). Because behavioral programs (“b-programs” for short) can be verified against a set of formal specification, BPjs allows writing verified systems in JavaScript. Which is, admittedly, weird. But in a good way.<\/p>\n

As part of the above mentioned demo, I\u2019ve created VisualRunningExamples<\/a>, an application that allows playing with a behavioral program for a maze walker. Users can load and modify the walker’s behavioral model and formal specification, and then run or verify it, using a friendly GUI. It also serves as an example of how to build a program around a BPjs model.<\/p>\n

\"\"<\/a>

VisualRunningExamples – Maze solution obtained by formal verification of the maze and walker model.<\/p><\/div>\n

One fun part of VisualRunningExample\u2019s UI is the selection of the maze the walker would roam in. My favorite maze has a cow (created using cowsay<\/code>, of course<\/a>). During the presentation I let the walker walk around the cow a bit, and I thought I saw it demonstrating a bad behavior – it seemed like it was going through a wall. I’m not an expert in maze walking, but I assume maze walkers should not do that.<\/p>\n

Immediately after the presentation, I looked into this in more depth. It seemed like the walker was moving diagonally. Which it should never do, since no part of the program requests such a move. It ostensibly went from point X to point Y:<\/p>\n

_______\r\n<BP(moo) >     @@@@@@@@@   t\r\n-------\r\n        \\Y<\/strong>  ^__^    @@@@@@@@\r\n@ @@@@@ X<\/strong>\\  (oo)_______\r\ns           (__)~~~~~~~)\\\/\\\r\n@ @@@@@        ||----w~|\r\n               ||     ||<\/code><\/pre>\n
Was this really happening? Using VisualRunningExamples<\/em>, I\u2019ve added the following b-threads, and verified the program against it. The idea behind this code is that whenever the maze walker gets into a cell, a set of b-threads that look for diagonal entries is\u00a0spawned. These b-threads blow the program up if they detect a diagonal mode. Pretty neat pattern, I think (reminiscent of LSC\u2019s symbolic charts used to forbid events):<\/p>\n
bp.registerBThread(\"no-diagonal\", function(){\r\n    while (true) {\r\n      var crd=getCoords(bp.sync({waitFor:anyEntrance}).name);\r\n    \tnoEntryNextMove(crd.col-1, crd.row-1);\r\n    \tnoEntryNextMove(crd.col-1, crd.row+1);\r\n    \tnoEntryNextMove(crd.col+1, crd.row-1);\r\n    \tnoEntryNextMove(crd.col+1, crd.row-+1);\r\n    }\r\n});\r\n\r\nfunction noEntryNextMove(col, row){\r\n    bp.registerBThread(\"nenv(\" + col + \",\" + row + \")\", function(){\r\n        var evt = bp.sync({waitFor:anyEntrance});\r\n        var newCoords = getCoords(evt.name);\r\n        bp.ASSERT( newCoords.col !== col || newCoords.row !== row, \"Diagonal Movement detected\");\r\n    });\r\n}\r\n<\/pre>\n
Verification did not find anything wrong, yet that parallel movement is happening, live, in front of my eyes. So, verification is broken too. Highly embarrassing, given that I just presented the tools at Harvard SEAS\u2019 SPYS group. Time to do some runtime verification.<\/p>\n
Runtime verification really boils down to adding these b-threads to the b-program (\u201cmodel\u201d), and running it. Easily done, and we know the runtime works. So, yay, next time mr. maze walker wants to do a diagonal jump, one of these b-threads will catch it red-handed. With an evil grin, I click the Run<\/code> button.<\/p>\n
Nothing. The walker does diagonal jumps like a boss. But only between points X<\/code> and Y<\/code>. Luckily, VisualRunningExamples<\/em>\u2019s UI is fun to play with, so I change the \\<\/code> to *<\/code>.<\/p>\n
No more parallel jumps, which never really happened. Good news: BPjs\u2019 verification works. As does its runtime.<\/p>\n
What Went Wrong<\/h3>\n
What really happened was that when creating the source Javascript b-program, the Java layer was copying the maze into an array of strings, verbatim. This meant that \\<\/code> was really an escaped space, which translates to a single space in JavaScript:<\/p>\n
jjs$ var s = \"\\ \"\r\njjs$ \"|\" + s + \"|\"\r\n| |\r\njjs$\r\n<\/pre>\n
The Java UI, on the other hand, displayed the backslash in the maze monitor table. In short: the JavaScript b-program saw a space there, whereas Java saw a backslash. The ostensible diagonal jumps were just the maze walker going from X<\/code> to Y<\/code> through an empty cell, that was marked by the Java layer as a\u00a0\\<\/code> cell.<\/p>\n
Lessons Learned<\/h3>\n