Merge branch 'vapontegarcia-master-patch-75068' into 'master'

Update README.md

See merge request xurbain/pactole-dev!7

README.md

 # Content
 
-This repository stores the Coq code of the Pactole
-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".
+The Pactole Repository: *A Framework for Formal Verification of Robotic Swarm Protocols*.
 
-It contains an abstract and parametrized formal model and a few
-case studies. The structure of the repository is described 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
 
 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.
 - [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 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.
-- *Spaces/*: Spaces in which robots evolve.
-- *Observations/*: Types of robot views of the configuration.
+- *Spaces/*: Spaces where robots evolve.
+- *Observations/*: Types of robot views on the configuration.
 - *Models/*: Additional properties of some models.
 - *CaseStudies/* : Case studies.
 
@@ -35,19 +37,19 @@ Pactole was financially supported by the following projects:
 
 The directory `CaseStudies` contains the following case
 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. 
 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 real 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.
 
@@ -63,7 +65,7 @@ Here is a list of the current case studies:
   - [InR/](CaseStudies/Gathering/InR) case studies for the gathering
     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
@@ -71,36 +73,38 @@ Here is a list of the current case studies:
   - [InR2/](CaseStudies/Gathering/InR2) case studies for the gathering
     on the Euclidean plane
     - [Peleg.v](CaseStudies/Gathering/InR2/Peleg.v):
-      Gathering in FSYNC and non rigid moves with weak mutliplicity detection, 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.
+      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 no 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):
-      SSYNC Gathering in  R²  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 a single robot is no enough.
+    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–
+ 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)
+
    02:36, 2022.