From 344d87608ba37d7c60a9ac0c86ee04773487d197 Mon Sep 17 00:00:00 2001
From: XU <xavier.urbain@liris.cnrs.fr>
Date: Thu, 5 Dec 2024 16:33:40 +0100
Subject: [PATCH] omfg proofread plz
---
README.md | 44 ++++++++++++++++++++++----------------------
codemeta.json | 6 +++---
2 files changed, 25 insertions(+), 25 deletions(-)
diff --git a/README.md b/README.md
index 9f9cb416..7b6fd626 100644
--- a/README.md
+++ b/README.md
@@ -1,21 +1,21 @@
# Content
This repository stores the Coq code of the Pactole
-(https://pactole.liris.cnrs.fr/) project, dedicated to formal
+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".
-It contains a very abstract and parametrized formal model and a lot of
-case studies. The structure of the repository is describe below.
+It contains an abstract and parametrized formal model and a few
+case studies. The structure of the repository is described below.
# Support
-It was financially supported by the following projects:
+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
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
@@ -24,30 +24,30 @@ It was financially supported by the following projects:
# 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 that are 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.
+- *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(s) 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` the only purpose of which 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):
- [Algorithm_noB.v](CaseStudies/Convergence/Algorithm_noB.v):
- Convergence without byzantine robots on the euclidean plane.
+ 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 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.
@@ -80,8 +80,8 @@ Here is a list of the current case studies:
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):
diff --git a/codemeta.json b/codemeta.json
index ecffdeeb..de545b51 100644
--- a/codemeta.json
+++ b/codemeta.json
@@ -44,13 +44,13 @@
},
{
"@type": "Person",
- "@id": "https://orcid.org/XXX",
+ "@id": "https://orcid.org/0000-0001-7442-2538",
"givenName": "Xavier",
"familyName": "Urbain",
- "email": "???",
+ "email": "Xavier.Urbain@univ-lyon1.fr",
"affiliation": {
"@type": "Organization",
- "name": "Université???"
+ "name": "Université Claude Bernard Lyon 1"
}
}
{
--
GitLab