This repository stores the Coq code of the Pactole
The Pactole Repository: *A Framework for Formal Verification of Robotic Swarm Protocols*.
project (https://pactole.liris.cnrs.fr/), dedicated to formal
verification of mobile robotic swarm protocols in many variants of the
model initially proposed by Suzuki and Yamashita [1] and sometimes
called the "look-compute-move model".
It contains an abstract and parametrized formal model and a few
This repository houses the Coq implementation of the Pactole project (https://pactole.liris.cnrs.fr/), dedicated to formally verifying distributed protocols for mobile robot swarms. It implements multiple variants of the Look-Compute-Move model, originally introduced by Suzuki and Yamashita [1].
case studies. The structure of the repository is described below.
Key Features:
- Provides an abstract, parameterized formal model
- Includes documented case studies (described below)
- Supports various model variants
- Enables rigorous protocol verification
[1] I. Suzuki and M. Yamashita. *Distributed Anonymous Mobile Robots: Formation of Geometric Patterns*. SIAM Journal of Computing, 28(4):1347–1363, 1999.
# Support
# Support
Pactole was financially supported by the following projects:
Pactole was financially supported by the following projects:
-[Pactole](https://pactole.liris.cnrs.fr/) started as
-[Pactole](https://pactole.liris.cnrs.fr/) started as the
Digiteo Project #2009-38HD.
Digiteo Project #2009-38HD.
-[SAPPORO](https://sapporo.liris.cnrs.fr/) funded by the French
-[SAPPORO](https://sapporo.liris.cnrs.fr/) funded by the French
National Research Agency (ANR) under the reference 2019-CE25-0005
National Research Agency (ANR) under the reference 2019-CE25-0005
[1] I. Suzuki and M. Yamashita. Distributed Anonymous Mobile Robots: Formation
of Geometric Patterns. SIAM Journal of Computing, 28(4):1347–1363, 1999.
# Overall Structure
# Overall Structure
-*Setting.v*: All you need to setup a working framework. A good starting point.
-*Setting.v*: All you need to setup a working framework. A good starting point.
-*Util/*: Extension to the Coq standard library that are not specific to Pactole.
-*Util/*: Extension to the Coq standard library not specific to Pactole.
-*Core/*: The core of the Pactole framework, implementing the Look/Compute/Move cycle.
-*Core/*: The core of the Pactole framework, implementing the Look/Compute/Move cycle.
-*Spaces/*: Spaces in which robots evolve.
-*Spaces/*: Spaces where robots evolve.
-*Observations/*: Types of robot views of the configuration.
-*Observations/*: Types of robot views on the configuration.
-*Models/*: Additional properties of some models.
-*Models/*: Additional properties of some models.
-*CaseStudies/* : Case studies.
-*CaseStudies/* : Case studies.
...
@@ -35,19 +37,19 @@ Pactole was financially supported by the following projects:
...
@@ -35,19 +37,19 @@ Pactole was financially supported by the following projects:
The directory `CaseStudies` contains the following case
The directory `CaseStudies` contains the following case
studies. Each case study (say `casestudy.v`) has a companion file
studies. Each case study (say `casestudy.v`) has a companion file
called `casestudy_Assuptions.v`the only purpose of which is to call `Print
called `casestudy_Assuptions.v`whose only purpose is to call `Print
Assumption` on the main theorem(s) of the case study.
Assumption` on the main theorem(s) of the case study.
This command is not included in the case study itself to allow for
This command is not included in the case study itself to allow for
fast compilation.
fast compilation.
Here is a list of the current case studies:
Here is a list of the current case studies:
-[Convergence/](Casestudy/Convergence):
-[Convergence/](Casestudy/Convergence): convergency results on different protocols.