This repository groups experiments being performed about applying CATLib to spatial problems, e.g., synthesising a strategy enforcing spatial properties on a topological graph.
This software has been developed for to the publication "An Experimental Toolchain for Strategy Synthesis with Spatial Properties", by Davide Basile, Maurice H. ter Beek & Vincenzo Ciancia, published in the Proceeding of the 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, Adaptation and Learning. ISoLA 2022, Rhodes, Greece, October 22–30, 2022, Part III, https://doi.org/10.1007/978-3-031-19759-8_10
The latest release contains the jars for reproducing the experiments of STTT SI Isola 2022 (file maze-0.0.2-SNAPSHOT-jar-with-dependencies.jar).
The Python script named CATLogicA.py is available in the root of the repository.
For reproducing the experiments described in our paper submitted to STTT Special Issue of ISOLA2022 follow the instructions below.
Download a VoxLogicA release:
https://github.com/vincenzoml/VoxLogicA/releases
In the main folder of the cloned repository (CATLib_PngConverter) create a directory VoxLogicA/binaries and unzip the archive there. The tool is now ready to be used.
For reproducing the whole toolchain the script CATLogica.py is used.
OpenJDK11 or a compatible version is required, python>3 is also required.
It suffices to clone the repository, download the released jar in the same folder as CATLogica.py, and run the command:
python3.X ./CATLogicA.py -experiment N -specification filename.imgql -imagePath pathToImg/originalImage.png
where N is the experiment id, filename.imgql is the specification and originalImage.png is the image to analyse.
Then the commands to be run are:
python3.X ./CATLogicA.py -experiment 1 -specification specification.imgql -imagePath pathToImg/maze.png
python3.X ./CATLogicA.py -experiment 2 -specification specification.imgql -imagePath pathToImg/maze.png
python3.X ./CATLogicA.py -experiment 3 -specification railwaySpecification.imgql -imagePath pathToImg/trainExample.png
The resources (including png images) are located inside the folder /src/main/java/io/github/contractautomata/maze/twoagentsproblem/resources/.
If you are interested in solely reproducing the part of the experiments related to CATLib, OpenJDK11 or a compatible version is required (python is not required).
Download the latest jar release, and launch it with:
java -jar maze-0.0.2-SNAPSHOT-jar-with-dependencies.jar
and follow the instructions. The executable class is located under src/main/java/it/github/contractautomata/maze/twoagentsproblem/AppMazeTwoAgents_STTT_SI_ISOLA2022.java.
The executable jar is equipped with an option to use the set-up of the experiments described in the paper.
The previous release contains the jar for reproducing the experiments of Isola 2022 (file maze-0.0.1-SNAPSHOT-jar-with-dependencies.jar). For reproducing the experiments of CATLib described in our paper accepted at ISOLA2022, download the previous (May 2022) jar release, and launch it with:
java -jar maze-0.0.1-SNAPSHOT-jar-with-dependencies.jar
and follow the instructions. The executable class is located under src/main/java/it/github/contractautomata/maze/twoagentsproblem/AppMazeTwoAgents_ISOLA2022.java.
The release also contains the log of reproduction of the jar with the various options.
OpenJDK11 or a compatible version is required.
For running VoxLogicA, first copy the png images generated from the previous step into
src/test/java/io/github/contractautomata/maze/resources/twoagentsimages/png
Then download VoxLogicA 1.0 from here:
https://github.com/vincenzoml/VoxLogicA/releases/tag/v1.0-experimental
and unzip it into src/main/python/io.github.contractautomata.maze/VoxLogicA/binaries (create the directory VoxLogicA/binaries if it does not exist). Then run the python script src/main/python/io.github.contractautomata.maze/orchestrate.py which generates a file called cache.json. A copy of this file is shipped in the root directory of the aforementioned jar file, with path experiment2.json and can be replaced.
A video demo created using this repository is available at https://youtu.be/08_iok6R9sw. Each frame of the video has been generated by executing the code in AppVideoComposition.java and by incrementing the bound of the call to the composition method.
All frames are stored in the folder src/test/ ... /resources/video.
The JSONConverter for importing graphs of VoxLogicA encoding bitmap images has been moved into this repository. A PngConverter is also available for directly importing png images as automata, by-passing the JSon representation.