ExtICE_23 documentation

Guarded lists in Bach

Contents

Guarded lists in Bach

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.

Setup

A zip file is provided by the following link.

It contains

  • a jar file, named anemone-coordination23.jar
  • two files, rush_hour_with_GL.bach and rush_hour_without_GL
  • a directory Images containing images

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.

Launching the software

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.

alternate text

Main window

Reading the program

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

alternate text

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.

alternate text

New Definition Window after parsing the program

Initialising the model-checker

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:

alternate text

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

alternate text

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.

alternate text

The Autonomous Agent Window

Model-checking

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

alternate text

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).

Viewing a solution

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.

Contents