Scenarios for Merging Proofs

From Event-B
Revision as of 10:05, 3 October 2008 by imported>Mathieu (→‎Merging scenarios)
Jump to navigationJump to search

This page is a first tentative to describe the scenario that a merge tool will have to face.

Proof structure

With respect to the merging objective, a proof is made of:

  1. a component name,
  2. a unique identifier inside that component, which is same as the PO identifier,
  3. a proof tree, either manual or automatic,
  4. a proof status (PO discharged or not by the proof tree)
  5. a PO sequent

Rodin database implementation

Each component

compname

is associated with:

  • a
    compname.bpr
    file, which contains the proof trees associated with each PO (1/, 2/ and 3/ before).
  • a
    compname.bps
    file, which contains the proof status associated with each PO (2/, 5/ and 3/ - discharged or not, manual or automatic)
  • a
    compname.bpo
    file, which contains the PO (1/ and 2/ + PO content).

Merging scenarios

PO being uniquely identified, it may be enough to consider a merge taking place PO by PO.

In the following we call L the local database/user/branch, O the other database/user/branch and A the database which reflects the common state from which L and O have departed (A, for ancestor). We also consider L and O as being symmetrical (and thus we won't describe symmetrical scenarios).

The table hereafter described the envisioned use case.

A st L st O st A ma L ma O ma PO L PO O PR L PR O Actions
1 - nok nok - - - =A /=A - - get PR O (O model has changed)
2 nok nok nok - - - =A =A /=A =A get PR L (L has perhaps tried a demo)
3 nok nok nok - - - =A =A /=A /=A ask user (both PR changed)
4 nok nok nok - - - =A =A =A =A get PR L (or O, no difference)
5 nok ok nok - - - - - - - get PR L
6 nok ok ok - - - =A /=A - - get PR O, (O model has changed)
7 nok ok ok - - - =A =A - - ask user (both demo are ok)
8 nok ok ok - - - =A =A - - ask user (both model have changed)
9 ok nok nok - - - =A =A /=A - get PR A (model has not changed and was proved)
10 ok nok nok - - - =A =A =A =A get PR A (model has not changed and was proved)
11 ok ok nok - - - =A =A - - get PR L (no model has changed)
12 ok ok nok - ma au =A /=A - - get PR L (O model has changed but L had a manual proof)
13 ok ok nok - au ma =A /=A - - get PR O (O model has changed and has a manual proof)
14 ok ok nok - ma ma =A /=A - /=A get PR O (O model has changed and has a new manual proof)
15 ok ok nok - ma ma =A /=A - =A get PR O (O model has changed)
16 ok ok nok - au au =A /=A - - get PR O (O model has changed)
17 ok ok nok - ma au /=A /=A - - get PR L (both model changed but L had a manual proof)
18 ok ok nok - ma ma /=A /=A - - ask user (both model changed with manual proof)
19 ok ok nok - au au /=A /=A - - ask user (both model changed with manual proof)
X st: (ok,nok) proof status for X (A,O or L)
X ma: (manual, automatic) manual status for X (A,O or L)
PO X: po changes for X compare to others user/branch
PR X: proof change for X, compared to others user/branch

User interactions

When asked, the user should be able to compare...

VCS interactions

External Links