This repository stores the Coq code of the Pactole project, dedicated to formal verification of mobile robotic swarm protocols.
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
-
CasesStudies/
- Convergence/: Convergence of robots in the 2D Euclidean plane
- Gathering/: Gathering in R or R² for various models
- Exploration/: Exploration of a ring with stop
- LifeLine/: Life line connection in the 2D Euclidean plane
Fast Compiling when developing
During development you can benefit from coq's "vos/vok" generation to speed up compilation. The only specificity of Pactole concerns compilation of the files named xxx_Assumptions.v. This files print the sets of assumptions used in the proofs of final lemmas in Case studies. Compiling these files for vos/vok target would raise errors. We provide adapted targets:
configure
coq_makefile -f _CoqProject -o Makefile
See below for faster compilation.
build (slow)
make
Be aware this may take more than 10mn to compile due to some case studies. You may want to comment them in the _CoqProject file before the configure step above if you are not interested in these case studies. Another solution is to follow the fast compilation recipes below.
Doing this once a week when developing is good practice. This is the only way to make a really safe compilation including all xxx_Assumption.v. You should always do this once in a while to make sure some universe constraints aren't failing and to check if you did not miss any remaining axiom.
But during the development process this makes the compilation when switching between files too slow. Hence the following less safe compilation processes:
build (slow, almost safe, but very parallelisable)
make [-j] vok
or better when developing
make [-j] vok-nocheck
Doing this once a day when developing is good practice.
build (Very fast, unsafe)
make [-j] vos
or better when developing
make [-j] vos-nocheck
This should be your prefered way of compiling when developing. It is much faster. It is unsafe but in most situations no bad surprise are to be expected.
You should do real compilations from time to time as explained above.
proofgeneral
For easy use of this feature (vos) you can use the auto compilation feature of proofgeneral. menu:
menu: Coq / Auto Compilation / Compile Before Require and then: Coq / Auto Compilation / vos compilation
Now you can transparently script in any buffer, all needed file will be compiled quickly. Don't forget to make a big fat "make" from time to time.