Simple animation with ProB
A simple Robot-Maze animation in ProB
A comprehensive article can be located on the ProB official website but I will share a few pointers to those of you who don't fancy engrossing yourselves with an an overwhelming amount of information before actually getting your hands dirty (this is how I personally prefer to learn :P)
A coursework for the undergraduate degree I am follow was the driving force that tingled my inquisitive nature to experiment and successfully animate a B specification although the animation was not mandatory (Which is also why I will not share the code I created, just so I don't get caught for plagiarism). So let me walkthrough the process that let to the completion of the task.
Just for the record, as mentioned above, all you need to know is available on the ProB website but here is the unorthodox methodology I followed:
The assignment specification was to implement a maze that exposed a few interface methods that allowed a robot to make it's way from the start (cell 1,1) to the end (cell 1,5) by avoiding internal walls that obstructed the path of the robot. The valid moves it was allowed to make were North (move a cell up), South (move a cell down), East (move a cell to the right), West (move a cell to the left) and Teleport (jump to a valid cell).
Of course, as the primary step, before bogging into the animation, was to write the B Machine specification implement the robot navigation logic.
Once that was complete I checked out the animation logic of the NQueens.mch example file that was located in the examples > GraphicalAnimation directory of the Prob root directory.
Here is what I found there (at least all that was of any use):
ANIMATION_FUNCTION_DEFAULT == ( {r,c,i|r:1..n & c:1..n & i=(r+c) mod 2 } );
ANIMATION_FUNCTION == ( {r,c,i|c:1..n & r=queens(c) & i=2+((r+c) mod 2) } );
ANIMATION_IMG0 == "images/sm_empty_box.gif";
ANIMATION_IMG1 == "images/sm_gray_box.gif";
ANIMATION_IMG2 == "images/sm_queen_white.gif";
ANIMATION_IMG3 == "images/sm_queen_black.gif";
This is all that was required to handle the entire animation!
Stunning Right? That was my initial reaction as well...
Let's try to understand this logic to comprehend how the animation takes place.
As interpreted above there are two functions, ANIMATION_FUNCTION_DEFAULT which represents the initial state of the images that collectively form the UI/animation.
Second is the ANIMATION_FUNCTION that governs the logic to switch the images as the machine's data changed over time so as to illustrate logic as the program flowed.
Both these methods contain 3 variables, r,c & i
- r : the number of horizontal images/grid cells
- c : the number of vertical images/grid cells
- i : the image to be placed on each of the cells
- i=(r+c) mod 2, meaning that the image value alternated between 0 and 1. Hence representing a chess board like checked grid of cells
- when i=0, the image that will be displayed -> ANIMATION_IMG0 thus ANIMATION_IMG1 when i=1
- i=(r+c) mod 2, meaning that the image value alternated between 0 and 1. Hence representing a chess board like checked grid of cells
Once I realised this, all I had to do was replace r & c with the number of horizontal and vertical cell required for the maze respectively and i with the location of the robot...
... and voila!
Leave a comment below if you have any questions or if there's anything you'd like to share...
Cheers!
