Detailing case studies in REDAME.

README.md

@@ -42,28 +42,54 @@ compilation of the case study.
 
 Here is a list of the current case studies:
 
-- Convergence/: Convergence of robots in the 2D Euclidean plane
-  - [Algorithm_noB.v](CaseStudies/Convergence/Algorithm_noB.v)
-  - Impossibility_2G_1B.v
-- Gathering/: Gathering in R or R² for various models
-  - Impossibility.v: 
-  - Definitions.v: Common definitions about the gathering problem
-  - WithMultiplicity.v
-  - InR/ case studies for the gathering on the enclidean line
-    - Impossibility.v
-    - Algorithm.v
-  - InR2/ case studies for the gathering on the enclidean plane
-    - Peleg.v
-    - Viglietta.v
-    - FSyncFlexNoMultAlgorithm.v
-    - Algorithm.v
-    - Algorithm_Assumptions.v
-- Exploration/: Exploration of a ring with stop
-  - ImpossibilityKDividesN.v
-  - ExplorationDefs.v
-  - Tower.v
-- LifeLine/: Life line connection in the 2D Euclidean plane
-  - Algorithm.v
+- [Convergence/](Casestudy/Convergence):
+  - [Algorithm_noB.v](CaseStudies/Convergence/Algorithm_noB.v):
+    Convergence without byzantine robots on the euclidean plane.
+    
+  - [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 Results for Byzantine-Tolerant Mobile Robots. SSS
+    2013.
+
+- [Gathering/](CaseStudies/Gathering): Gathering in R or R² for
+  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.
+  - [WithMultiplicity.v](CaseStudies/Gathering/WithMultiplicity.v):
+    Common definition on gathering when robot enjoy strong
+    multiplicity detection.
+  - [InR/](CaseStudies/Gathering/InR) case studies for the gathering
+    on the enclidean line
+    - [Impossibility.v](CaseStudies/Gathering/InR/Impossibility.v):
+      Impossibility of gathering on the line in SSYNC.
+    - [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
+    - [Peleg.v](CaseStudies/Gathering/InR2/Peleg.v):
+      Formalization of a protocol for gathering with lights due to Peleg.
+    - [Viglietta.v](CaseStudies/Gathering/InR2/Viglietta.v):
+      Formalization of a protocol for gathering with lights due to Viglietta.
+    - [FSyncFlexNoMultAlgorithm.v](CaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v):
+      Gathering in FSYNC and non rigid moves with weak mutliplicity detection.
+    - [Algorithm.v](CaseStudies/Gathering/InR2/Algorithm.v):
+      Gathering in R2 in SSYNC with strong multiplicity detection, from
+      non bivalent configurations.
+- [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.
+  - [ExplorationDefs.v](CaseStudies/Exploration/ExplorationDefs.v):
+    Common definitions on exploration.
+  - [Tower.v](CaseStudies/Exploration/Tower.v):
+    ???
+- [LifeLine/](CaseStudies/LifeLine): Life line connection in the 2D Euclidean plane
+  - [Algorithm.v](CaseStudies/LifeLineAlgorithm.v):
+    Connection maintenance protocol on R2.
 
 #  Other Related Ressources