As a companion to the submission of the article Guarded Lists in Bach: Expressiveness and Efficiency Issues, this page describes how to launch a campain of tests.
A zip file is provided by the following link.
It contains
Please upload this file and decompress it in a directory of your
choice. In the following, we will refer to this directory as your_test_dir.
Tests are performed by launching the Bach animator. To that end, open
a terminal and go to the directory your_test_dir. Then launch the
animator by typing the command
java -jar anemone-coordination23.jar
As the animator uses Processing, please make sure to use java version 1.8.
If things go well, you should obtain the blue window of the following figure.
Main window
The next step is to introduce the program. As announced above, two versions are given. On the one hand, the file rush_hour_with_GL.bach contains the coding of the Rush Hour puzzle using the guarded list construct. On the other hand, the file rush_hour_without_GL contains the coding without the guarded list construct. In both cases, the games being tested are coded at the end of the program. Moreover the program is written in a declarative way, which allows to code other case tests by analogy.
In practice, to introduce the program, click on the New Definition(s) bottom in the main window. This will open a purple windows similar to the following one
New Definition Window
Then open the program of your choice in your favorite editor and copy
the whole program in the first box (by erasing first the text Enter
the description(s). Finally, click on submit. You should obtain a
result similar to the one of the following figure.
New Definition Window after parsing the program
An initialisation needs to be operated before model-checking. First the scene to draw images should be initialised. This is obtained by clicking on the New Interactive Agent button of the main (blue) window. By doing so a window similar to the following one should appear:
The interactive Agent
Enter InitScene in the first box, as shown in the above figure,
and press on submit. This will allow you to click on the InitScene
button and then on the draw_scene button to generate a grey window
displaying the board of the Rush Hour game, as seen in the following
window
The Scene Window
We are now ready to place vehicles. As many steps will be required, we
shall use a so-called autonomous agent. To that end, click on the
button New Autonomous Agent in the (blue) main window. Then,
assuming we will play game number 1, enter Init_game_1 in the
first (white) box. Click on the Submit button and press
run. Wait that the agent in place of Here will displayed the
current agent terminates its execution. The following figure shows
the situatioin just before pressing Submit.
The Autonomous Agent Window
We are now in a position to perform the model checking. To that end,
click on the New Model Checker of the main (blue) windows. A
figure similar to the following one should appear
The Model Checker Window
Insert the agent to be model-checked in the first box, namely
Real_game_1. Then insert Reach (#out=1) in the second
box. Click on the Submit buttons. We are now ready to perform the
model-checking. Just click on the button Model checked and
wait. When the model checker has finished the message Status of the
model checking will change. The time needed for the model checking
can be read in the terminal from which the jar file was launched (see section
Launching the software above).
A solution can be viewed by clicking the Simulate trace
button. The model checker guarantees that the contents of the store
has not changed from the start of the model checker. However images
have moved. To appreciate the solution, we need first to reset the
places of the images. This is obtained by launching a new Autonomous
Agent and by computing the Reset_game_1 procedure. When this is
done, click on the Simulate trace and look at the movements of the
vehicles. They illustrate a solution.
