Improve the architecture of the B model
The purpose of this merge request is to improve the architecture of the B model and to make it simple to add the AddNode service.
It also contains various fixes for issues found while inspecting the model.
The Read and Write service are still not provable, but this can be treated in another merge request devoted specifically to each service.
Closes #931 (closed), #951 (closed), #953 (closed) and #954 (closed)
Edited by Vincent Monfort