Evaluation of the VoxMinX toolchain for spatial model checking via model minimisation
This repository provides setup and execution instructions for the validation of the VoxMinX toolchain. The workflow uses GraphLogicA and mCRL2 for conversion/minimization and VoxLogicA for model checking. The environment is containerized to keep runs reproducible.
This repository contains the source code for the validation of the toolchain VoxMinX for the paper:
Title: Spatial Model Checking of Images via Minimised Models and Branching Bisimilarity
Authors: Vincenzo Ciancia, Jan Friso Groote, Diego Latella, Mieke Massink and Erik P. de Vink
This file will be updated when the paper appears online and will contain a link to it.
This archive has been designed for, and tested on, ubuntu 26.04. It is expected to work, possibly with minor changes, on other linux distributions, and it should be possible to port it to macos and windows, although we did not do this yet.
This archive contains a .devcontainer folder that can be used with visual studio code, or just the Dockerfile can be used with docker or podman directly.
If you don't want to run python directly and don't have podman or docker installed, one quick way to do this is using an optional support tool called podman-minimal see https://vincenzoml.github.io/podman-minimal/ , a script that will install podman if you don't have it (on windows, linux and macos) and run any command using the Dockerfile included in the current directory or a .devcontainer directory, with correct permissions for the current working directory, in userspace.
Using podman-minimal you can write from the main folder VoxMinX-Validation:
podman-minimal python3 scripts/runTestsVLX.py
and it takes care of everything.
As a result you get a table like the one below with values for each selected example present in the folder test-images-try:
| label | conversionimg2aut | convWIOfull | pixels | transitions | autSizeH | min_computation | minWIO | statesMin | transitionsMin | convertBack | modelCheckingFull | modelCheckingMin | speedupMC |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| maze-128 | 0.20 | 0.39 | 16.00 K | 142.50 K | 2.47 MiB | 0.01 | 0.08 | 7 | 21 | 0.20 | 0.27 | 0.27 | 1.01 |
| maze-256 | 0.21 | 0.27 | 64.00 K | 573.00 K | 10.35 MiB | 0.04 | 0.28 | 7 | 21 | 0.24 | 0.27 | 0.27 | 1.01 |
Note that the values obtained may differ due to the use of a different machine configuration. To see more results, just copy other test images from the folder test-images to the folder test-images-try and run the above command again. Note that the largest images may require more memory than available on your machine or may take a very long time to process. Timings may also vary slightly in various runs.
Meaning of the column labels used in the above table:
label: label of the example
conversionimg2aut: conversion time of the image into its encoding
convWIOfull: Same as above, but including time for IO
pixels: number of pixels in the image
transitions: number of transitions in the image
autSizeH: size of the encoded LTS
min_computation: time needed to compute the minimal model
minWIO: same but including time for IO
statesMin: number of states of the minimal model
transitionsMin: number of transitions of the minimal model
convertBack: time needed to convert the model checking result back to the input image
modelCheckingFull: model checking time of the full image using VoxLogicA
modelCheckingMin: model checking time of the minimal model using GraphLogicA
speedupMC: speedup in the model checking time for the minimal model w.r.t. the model checking time for the full image
If you prefer plain Docker:
docker build --progress=plain .
docker run --rm $(docker build -q .)
For interactive debugging inside the container:
docker run -it --rm $(docker build -q .) bash
python3 ./scripts/runTestsVLX.py
On ubuntu, one needs to install python3 and python3-pip and to create a venv in order to avoid conflicts with the system's package manager.
sudo apt install python3 python3-pip python3-venv
python3 -m venv .venv
source .venv/bin/activate
after which the python prerequisites pandas and pillow can be installed using
pip3 install pandas pillow
If all images are tested then the test may take about 30 minutes to finish on an Intel Core-i9 machine from 2019. Ram usage is high (the test machine has 32gb).
To run the tests from the repository root:
python3 ./runTestsVLX.py
This file runs the VoxMinX application on the images that are in the folder test-images-try. In the repository this folder contains only the smallest maze image. More images can be found in the folder test-images. To run the application on further images, just copy (or move) the ones of interest to the folder test-image-try and run the tests again as shown above.
See the comments in runTests.py or the paper to see what the tests are doing.
The results are the files "rawdata_new.csv" (raw data from experiments) and "results-table_new.csv" (table massaged to be included in latex; note that the labels are not exactly the same as those in the paper but they should be clear nevertheless.). These files can be found in the folder experiments/stats and will be overwritten with every execution of python3 ./runTestsVLX.py
-
Rebuild without cache:
docker build --no-cache --progress=plain .
-
Run interactively and execute the script manually:
docker run -it --rm $(docker build -q .) bash python3 ./scripts/runTestsVLX.py
- The script mostly prints phase-level messages; large images may take time per phase.
- You can monitor execution using tools such as
htop.
Boost Software License - Version 1.0 - August 17th, 2003
Permission is hereby granted, free of charge, to any person or organization obtaining a copy of the software and accompanying documentation covered by this license (the "Software") to use, reproduce, display, distribute, execute, and transmit the Software, and to prepare derivative works of the Software, and to permit third-parties to whom the Software is furnished to do so, all subject to the following:
The copyright notices in the Software and this entire statement, including the above license grant, this restriction and the following disclaimer, must be included in all copies of the Software, in whole or in part, and all derivative works of the Software, unless such copies or derivative works are solely in the form of machine-executable object code generated by a source language processor.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE, TITLE AND NON-INFRINGEMENT. IN NO EVENT SHALL THE COPYRIGHT HOLDERS OR ANYONE DISTRIBUTING THE SOFTWARE BE LIABLE FOR ANY DAMAGES OR OTHER LIABILITY, WHETHER IN CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
Copyright 2018 Vincenzo Ciancia.
Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License.
A copy of the license is available in the file "Apache_License.txt". You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License.