Skip to content

Improve the architecture of the B model

Laurent Voisin requested to merge lvo/953 into master

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

Merge request reports