Merge branch 'master' into gathering-bivalent

.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

CREDIT.md

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

DEV.md

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

INSTALL.md

 
 # 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

README.md

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

codemeta.json

+{
+    "@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"
+}