Scenarios for Merging Proofs: Difference between revisions

From Event-B
Jump to navigationJump to search
← Older editNewer edit →
imported>Mathieu
mNo edit summary
imported>Mathieu
m Simple scenarios (need database evolution)
Line 5: Line 5:
# a unique identifier inside that component, which is same as the [[PO]] identifier,
# a unique identifier inside that component, which is same as the [[PO]] identifier,
# a proof tree, either manual or automatic,
# a proof tree, either manual or automatic,
# a proof status (PO discharged or not by the proof tree)
# a proof status (PO discharged or not by the proof tree, in fact implemented with a ''confidence'' value: 1000 => proved, 500 => review, <500 => unproved)
# a PO [[sequent]]
# a PO [[sequent]]


Line 13: Line 13:
* a {{file|compname.bps}} file, which contains the proof status associated with each PO (2/, 5/ and 3/ - discharged or not, manual or automatic)
* a {{file|compname.bps}} file, which contains the proof status associated with each PO (2/, 5/ and 3/ - discharged or not, manual or automatic)
* a {{file|compname.bpo}} file, which contains the PO (1/ and 2/ + PO content).
* a {{file|compname.bpo}} file, which contains the PO (1/ and 2/ + PO content).
== Proof reuse ==
Rodin is able, actually with a bit of work, to provide a ''reuse'' mechanism. This mechanism would allow to check, without replaying, that a proof tree will cleanly discharge a PO.
Having this mechanism at hand is very useful, as it allows the person doing the merge to take its decision without knowing the content of the old {{file|.bps}} and {{file|.bpo}} files. Only the {{file|.bpr}} files and the {{file|.bpo}} obtains after having merged the model are used.


== Merging scenarios ==
== 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).
=== Simple scenarios (need database evolution) ===
=== Simple scenarios (need database evolution) ===
While discussing about the merge topic, it appears that another wanted and related feature is [[multi-proof database]], where the {{file|compname.bpr}} file contains not only the current proof (called ''main proof''), but also all the proof that weere once used to proof the po.
While discussing about the merge topic, it appears that another wanted and related feature is [[multi-proof database]], where the {{file|compname.bpr}} file contains not only the current proof (called ''main proof''), but also all the proof trees that were once used to proof the PO (the set of those proof tree is called ''proof history'').
 
Once both ''multi-proof database'' and ''proof reuse'' are implemented, the merge process for the proofs may be the following one:
# [[Requirements for merging models|merge the model]] (machines and context)
# the new ''proof history'' is made of the union of ''proof histories'' from ''O'' and ''L' plus one of ''O'' or ''L'' ''main proof''
# the other ''main proof'' becomes the new ''main proof''
Those steps are totally automatic.
 
Then the person doing the merge may review the proof that do not replay, and see if one of the history proof tree may help (steps which may also be automated with the help of ''proof reuse'' feature.


=== Complicated scenarios ===
=== Complicated scenarios ===
''Those scenarios are kept for reference''
''Those scenarios are kept for reference''
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.
The table hereafter described the envisioned use case.

Revision as of 12:19, 3 October 2008

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, in fact implemented with a confidence value: 1000 => proved, 500 => review, <500 => unproved)
  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).

Proof reuse

Rodin is able, actually with a bit of work, to provide a reuse mechanism. This mechanism would allow to check, without replaying, that a proof tree will cleanly discharge a PO.

Having this mechanism at hand is very useful, as it allows the person doing the merge to take its decision without knowing the content of the old

.bps

and

.bpo

files. Only the

.bpr

files and the

.bpo

obtains after having merged the model are used.

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).

Simple scenarios (need database evolution)

While discussing about the merge topic, it appears that another wanted and related feature is multi-proof database, where the

compname.bpr

file contains not only the current proof (called main proof), but also all the proof trees that were once used to proof the PO (the set of those proof tree is called proof history).

Once both multi-proof database and proof reuse are implemented, the merge process for the proofs may be the following one:

  1. merge the model (machines and context)
  2. the new proof history is made of the union of proof histories from O and L' plus one of O or L main proof
  3. the other main proof becomes the new main proof

Those steps are totally automatic.

Then the person doing the merge may review the proof that do not replay, and see if one of the history proof tree may help (steps which may also be automated with the help of proof reuse feature.

Complicated scenarios

Those scenarios are kept for reference


The table hereafter described the envisioned use case.

n° 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

Retrieved from ‘https://wiki.event-b.org/index.php?title=Scenarios_for_Merging_Proofs&oldid=9267’