View source for Scenarios for Team-based Development

''See also the [[Talk:Scenarios for Team-based Development|associated talk page]] for discussion about this topic.''

== Objective ==

Rodin is currently a stand-alone tool.  Attempts to use it in a team environment by simply putting a code repository underneath it (e.g. Subversion) failed, as this makes handling of conflicts awkward at best.  It was decided to take a step back and to first figure out what is needed in the first place, before deciding on how to solve the problem.

== Approach ==

* Identify scenarios (users and tool developers through brainstorming)

* While identifying scenarios, collect requirements that must hold true for all scenarios

* Share the scenarios with the industry partners to validate and improve them (and to find missing scenarios)

* Decide on the scenario(s) that will be implemented for Rodin

* Design a subsystem for Rodin that will realize the selected scenario(s) and implement it

== Scenarios ==

; (S-1) Only one person at a time works on an Event-B Project: While it is important not to corrupt data through concurrent edits, in this scenario it is sufficient if access for editing is granted only one user at a time.

; (S-2) Multiple users work concurrently on an Event-B Project: In this scenario, it is expected that several users need concurrent write-access to the project.  It is acceptable if individual elements of the system must be locked, or if individual elements need to be merged in case of conflict.

; (S-3) A History of changes on an Event-B Project is maintained and accessible: In this scenario, the users don't care much about the team aspect, but require access to a change history.

; (S-4) A project is exchanged between two sites (e.g. customer and supplier), where each party has a clear responsibility: In this scenario it is expected that each party can modify only a certain part of the model, and it is expected that a merge must be performed on a regular basis.

== Requirements for all Scenarios ==

; (R-1) If a change in the machine or context has an impact on proofs, the proofs are either updated or invalidated.

; (R-2) The impact of editing on the rest of the system shall be as small as possible.: This could mean, for instance that if we change an invariant, that not the whole prooftree of a proof is invalidated, but only a subtree.

== Some general thoughts ==

* There are two common types of repositories: Those following a lock-edit-unlock cycle (MS SourceSafe, Perforce) and those following an update-edit-merge cycle (Subversion, CVS).  These two approaches are not compatible.  The question of which approach to use will appear sooner than later.

* The granularity of the Event-B-models for the purpose of team-based development has to be decided at some point.  As we noted earlier, the current file structure clearly does not have the right granularity.

* With a text editor, it would be possible to for example store the textual representations of the models in subversion. This would in principle enable concurrent editing: updating the Rodin XML models in case of an svn update would not be much different from when a user locally modifies a text file. This still leaves open the issue of how to enable multiple users to work on proofs a the same time. If every proof is represented by a single file, one could for example put those files as binary files within subversion. (Note: this means that individual proofs cannot be merged; if two users have modified the same proof one would have to choose one of the two versions.) There are, however, still issues with how to manage the individual proof files in case of changes to the model (renaming of some files, deletion of others and additions).

== Proposal for a solution ==

Here is the picture of a technical solution relying on subversion, a textual representation of models, the two-way translator between Rodin XML files and text files (part of a text editor), and an extension of the Rodin POG where proofs for POs are stored in individual XML files.
[[Image:SubversionProposal.svg]]

[[Category:Design proposal]]