diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 33aa9257065ea614d3ab0f8e15423353ca9bc135..76c4705980764522d6945b9936461785b520c17c 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -18,8 +18,11 @@ stages:
- make -j "$NJOBS"
# - make install
-coq:8.15:
+coq:8.18:
extends: .build
-coq:8.16:
+coq:8.19:
+ extends: .build
+
+coq:8.20:
extends: .build
diff --git a/CREDIT.md b/CREDIT.md
new file mode 100644
index 0000000000000000000000000000000000000000..57547d1e0e3a6cd7e0b62766deab654787674acc
--- /dev/null
+++ b/CREDIT.md
@@ -0,0 +1,9 @@
+The following people have contributed to the development of the Pactole library during the indicated periods of time:
+
+- Cédric Auger (2013)
+- Thibaut Balabonski (2016-2017)
+- Sebastien Bouchard (2021- now)
+- Pierre Courtieu (2013- now)
+- Robin Pelle (2016-2020)
+- Lionel Rieg (2014- now)
+- Xavier Urbain (2013-now)
diff --git a/DEV.md b/DEV.md
index 9597e8b9db1f558fefbd28d14538788f8d384d46..e98361944ba8f01bba64aa5e30b29e9237a96627 100644
--- a/DEV.md
+++ b/DEV.md
@@ -1,13 +1,25 @@
-# Contributing
+The fundamental principle is that the MASTER branch must remain
+compilable at all times and should never contain incomplete
+developments.
-The golden rule is that **MASTER SHOULD COMPILE AT ALL TIME** and does not
-contain in-progress developments.
+Development work on the master branch must be avoided. Instead, each
+feature or topic should have its own dedicated branch. Developers
+should create new branches as needed, and all work—including
+collaborative efforts—should occur within these topic-specific
+branches.
-More precisely, development never happens on master: each topic should have
-its own branch (feel free to create one if needed) and work happens there,
-even when several people are involved.
+Before merging changes into master, ensure that your code:
-Once a set of changes (e.g. a new case study) is complete and polished enough
-(comments, adequate identation, no use of generated hypothesis names, etc.),
-you may merge it to master by squashing its commits into meaningful pieces
-(only a few, usually one may be enough) or submit a pull request.
+- Is complete and thoroughly tested
+- Contains clear and comprehensive comments
+- Features proper indentation
+- Uses descriptive hypothesis names rather than auto-generated ones
+- Meets all project quality standards
+
+When your changes are ready (such as a completed case study), you have
+two options:
+
+1. Submit a pull request for review
+2. Merge directly into master after squashing your commits into
+ meaningful, well-organized units (typically one or a few commits
+ that clearly represent the changes)
diff --git a/INSTALL.md b/INSTALL.md
index 1d7367e4b0694976bd6ebbc2c51f603f6dacffaf..019e84bebbcb17e3af866b9e7948b969ff03ddaa 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -1,7 +1,7 @@
# Requirements
-- Coq 8.19 or 8.20 (including the executable `coqc`, `codep`, `coq_makefile`)
+- Coq 8.19 or 8.20 (including the executable `coqc`, `coqdep`, `coq_makefile`)
- GNU `make`
# Configuration
diff --git a/README.md b/README.md
index 0b2dc291d766b0c890439a36830a2cb4b55dca36..e3235e789692ee6eb7d42bdd1b39947702fd26d9 100644
--- a/README.md
+++ b/README.md
@@ -1,54 +1,55 @@
# Content
-This repository stores the Coq code of the Pactole
-(https://pactole.liris.cnrs.fr/) project, 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".
+The Pactole Repository: *A Framework for Formal Verification of Robotic Swarm Protocols*.
-It contains a very abstract and parametrized formal model and a lot of
-case studies. The structure of the repository is describe below.
+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].
+
+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
-It was financially supported by the following propject:
+Pactole was financially supported by the following projects:
-- [The Pactole project](https://pactole.liris.cnrs.fr/) started as
+- [Pactole](https://pactole.liris.cnrs.fr/) started as the
Digiteo Project #2009-38HD.
-- [SAPPORO](https://sapporo.liris.cnrs.fr/) is funded by the French
+- [SAPPORO](https://sapporo.liris.cnrs.fr/) funded by the French
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
- *Setting.v*: All you need to setup a working framework. A good starting point.
-- *Util/*: Extension the to the Coq standard library that are not specific to Pactole
-- *Core/*: The core the the Pactole framework, implementing the Look/Compute/Move cycle
-- *Spaces/*: Spaces in which robots evolve
-- *Observations/*: Types of robot views of the configuration
-- *Models/*: Additional properties of some models
-- *CaseStudies/* : Case studies
+- *Util/*: Extension to the Coq standard library not specific to Pactole.
+- *Core/*: The core of the Pactole framework, implementing the Look/Compute/Move cycle.
+- *Spaces/*: Spaces where robots evolve.
+- *Observations/*: Types of robot views on the configuration.
+- *Models/*: Additional properties of some models.
+- *CaseStudies/* : Case studies.
# Case Studies
-The directory `CaseStudies` contains the following the following case
+The directory `CaseStudies` contains the following case
studies. Each case study (say `casestudy.v`) has a companion file
-called `casestudy_Assuptions.v` whose only purpose is to call `Print
-Assumption` on the main theorem of the case study. The reason why this
-command is not included in the case study itself is for allowing fast
-compilation of the case study.
+called `casestudy_Assuptions.v` whose only purpose is to call `Print
+Assumption` on the main theorem(s) of the case study.
+This command is not included in the case study itself to allow for
+fast compilation.
Here is a list of the current case studies:
-- [Convergence/](Casestudy/Convergence):
+- [Convergence/](Casestudy/Convergence): convergency results on different protocols.
- [Algorithm_noB.v](CaseStudies/Convergence/Algorithm_noB.v):
- Convergence without byzantine robots on the euclidean plane.
-
+ Convergence on the Euclidean plane without Byzantine robots.
- [Impossibility_2G_1B.v](CaseStudies/Convergence/Impossibility_2G_1B.v):
- Impossibility of convergence on the line when 1/3 of robots are
- byzantine. Auger, Bouzid, Courtieu, Tixeuil, Urbain. Certified
+ *Impossibility of convergence on the real line when 1/3 of robots are
+ Byzantine.* Auger, Bouzid, Courtieu, Tixeuil, Urbain. Certified
Impossibility Results for Byzantine-Tolerant Mobile Robots. SSS
2013.
@@ -56,45 +57,52 @@ Here is a list of the current case studies:
various models
- [Impossibility.v](CaseStudies/Gathering/Impossibility.v):
Impossibility of gathering in SSYNC.
- - [Definitions.v](CaseStudies/Gathering/Definitions.v): Common
- definitions about the gathering problem.
+ - [Definitions.v](CaseStudies/Gathering/Definitions.v):
+ Common definitions about the gathering problem.
- [WithMultiplicity.v](CaseStudies/Gathering/WithMultiplicity.v):
- Common definition on gathering when robot enjoy strong
+ Common definition on gathering when robots enjoy strong
multiplicity detection.
- [InR/](CaseStudies/Gathering/InR) case studies for the gathering
- on the enclidean line
+ on the Euclidean line
- [Impossibility.v](CaseStudies/Gathering/InR/Impossibility.v):
- Impossibility of gathering on the line in SSYNC.
+ *Impossibility of gathering on the line in SSYNC.*
+ Courtieu, Rieg, Tixeuil, Urbain. Impossibility of gathering, a certification. IPL 115.
- [Algorithm.v](CaseStudies/Gathering/InR/Algorithm.v): Gathering
one the line in SSYNC with strong multiplicity detection, from
non bivalent configurations.
- [InR2/](CaseStudies/Gathering/InR2) case studies for the gathering
- on the enclidean plane
+ on the Euclidean plane
- [Peleg.v](CaseStudies/Gathering/InR2/Peleg.v):
- Formalization of a protocol for gathering with lights due to Peleg.
+ *Gathering in FSYNC and non rigid moves with weak mutliplicity detection, due to Peleg.*
+ Cohen, Peleg. Convergence Properties of the Gravitational Algorithm in Asynchronous Robot Systems. SIAM Journal of Computing, 34(6):1516–1528, 2005.
- [Viglietta.v](CaseStudies/Gathering/InR2/Viglietta.v):
Formalization of a protocol for gathering with lights due to Viglietta.
+ Viglietta. *Rendezvous of two robots with visible bits.* ALGOSENSORS 2013.
- [FSyncFlexNoMultAlgorithm.v](CaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v):
- Gathering in FSYNC and non rigid moves with weak mutliplicity detection.
+ *Gathering in FSYNC and non rigid moves with no mutliplicity detection.*
+ Balabonski, Delga, Rieg, Tixeuil, Urbain. Synchronous Gathering Without Multiplicity Detection: A Certified Algorithm. Theory Comput. Syst. 63(2): 200-218 (2019)
- [Algorithm.v](CaseStudies/Gathering/InR2/Algorithm.v):
- Gathering in R2 in SSYNC with strong multiplicity detection, from
- non bivalent configurations.
+ *SSYNC Gathering in R² with strong multiplicity detection, from
+ non-bivalent configurations.*
+ Courtieu, Rieg, Tixeuil, Urbain. Certified Universal Gathering in R² for Oblivious Mobile Robots. DISC 2016.
- [Exploration/](CaseStudies/Exploration): Exploration of a ring with stop
- [ImpossibilityKDividesN.v](CaseStudies/Exploration/ImpossibilityKDividesN.v):
- Impossibility of exploration of a ring when the number of robots
- divides the number of nodes.
+ *Impossibility of exploration of a ring when the number of robots
+ divides the number of nodes.*
+ Balabonski, Pelle, Rieg, Tixeuil. A Foundational Framework for Certified Impossibility Results with Mobile Robots on Graphs. ICDCN 2018.
- [ExplorationDefs.v](CaseStudies/Exploration/ExplorationDefs.v):
Common definitions on exploration.
- [Tower.v](CaseStudies/Exploration/Tower.v):
- ???
+ Exploration with stop on a ring requires forming a tower, in particular one single robot is no enough.
- [LifeLine/](CaseStudies/LifeLine): Life line connection in the 2D Euclidean plane
- [Algorithm.v](CaseStudies/LifeLineAlgorithm.v):
- Connection maintenance protocol on R2.
+ *Connection maintenance protocol on R2.*
+ Balabonski, Courtieu, Pelle, Rieg, Tixeuil, Urbain. Computer Aided Formal Design of Swarm Robotics Algorithms. SSS 2021.
# Other Related Ressources
A general description of the Pactole library and its use:
- Courtieu, L. Rieg, S. Tixeuil, and X. Urbain. Swarms of Mobile Robots: Towards
- Versatility with Safety. Leibniz Transactions on Embedded Systems, 8(2):02:1–
- 02:36, 2022.
+ Courtieu, Rieg, Tixeuil, and Urbain. *Swarms of Mobile Robots: Towards
+ Versatility with Safety.* Leibniz Transactions on Embedded Systems (LITES), 8(2):02:1–
+ 02:36, 2022. [link](https://doi.org/10.4230/LITES.8.2.2)
diff --git a/codemeta.json b/codemeta.json
new file mode 100644
index 0000000000000000000000000000000000000000..d6ace5d8e2dd34759b9a802fc172a18d720d908a
--- /dev/null
+++ b/codemeta.json
@@ -0,0 +1,57 @@
+{
+ "@context": "https://w3id.org/codemeta/3.0",
+ "type": "SoftwareSourceCode",
+ "applicationCategory": "Coq library dedicated to formal verification of mobile robotic swarm distributed protocols",
+ "author": [
+ {
+ "id": "https://orcid.org/0000-0001-8789-9781",
+ "type": "Person",
+ "affiliation": {
+ "type": "Organization",
+ "name": "Conservatoire National des Arts et Métiers"
+ },
+ "email": "Pierre.Courtieu@lecnam.net",
+ "familyName": "Courtieu",
+ "givenName": "Pierre"
+ },
+ {
+ "id": "https://orcid.org/0000-0001-7442-2538",
+ "type": "Person",
+ "affiliation": {
+ "type": "Organization",
+ "name": "Université Claude Bernard Lyon 1"
+ },
+ "email": "Xavier.Urbain@univ-lyon1.fr",
+ "familyName": "Urbain",
+ "givenName": "Xavier"
+ },
+ {
+ "id": "_:author_3",
+ "type": "Person",
+ "affiliation": {
+ "type": "Organization",
+ "name": "Verimag, Grenoble INP -- UGA"
+ },
+ "email": "lionel.rieg@univ-grenoble-alpes.fr",
+ "familyName": "Rieg",
+ "givenName": "Lionel"
+ }
+ ],
+ "codeRepository": "https://gitlab.liris.cnrs.fr/pactole/coq-pactole",
+ "description": "A Coq library dedicated to formally verifying distributed protocols for mobile robot swarms. The library implements various extensions of the Look-Compute-Move model, first proposed by Suzuki and Yamashita, providing a robust framework for protocol verification in different theoretical settings. ",
+ "keywords": [
+ "distributed systems",
+ "deductive verification",
+ "formal proof",
+ "robotic swarms"
+ ],
+ "license": "https://spdx.org/licenses/LGPL-3.0",
+ "name": "Pactole",
+ "programmingLanguage": "Coq/Rocq",
+ "relatedLink": "https://pactole.liris.cnrs.fr/",
+ "runtimePlatform": "Coq-8.20",
+ "version": "2.1",
+ "developmentStatus": "active",
+ "funding": "Digiteo Project #2009-38HD, ANR Project 2019-CE25-0005",
+ "referencePublication": "https://doi.org/10.4230/LITES.8.2.2"
+}