Merge branch 'master' into public

README.md

@@ -62,6 +62,9 @@ Here is a list of the current case studies:
   - [WithMultiplicity.v](CaseStudies/Gathering/WithMultiplicity.v):
     Common definition on gathering when robots enjoy strong
     multiplicity detection.
+  - [WithMultiplicityLight.v](CaseStudies/Gathering/WithMultiplicityLight.v):
+    Common definition on gathering when robots enjoy strong
+    multiplicity detection and lights.
   - [InR/](CaseStudies/Gathering/InR) case studies for the gathering
     on the Euclidean line
     - [Impossibility.v](CaseStudies/Gathering/InR/Impossibility.v):
@@ -85,6 +88,11 @@ Here is a list of the current case studies:
       *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.
+    - [Algorithm_withLight](CaseStudies/Gathering/InR2/Algorithm_withLight.v):
+      *Deterministic Color-optimal Self-stabilizing Semi-synchronous
+      Gathering: a Certified Algorithm*. Bonnet, François, Bramas,
+      Quentin, Courtieu, Pierre, Défago, Xavier, Rieg, Lionel,
+      Tixeuil, Sebastien, Urbain, Xavier.
 - [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