Difference between revisions of "Scenarios for Merging Proofs"

From Event-B
Jump to navigationJump to search
imported>Mathieu
m (New page: 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: # a component ...)
 
imported>Mathieu
m (Add a table describing the envisionned cases)
Line 6: Line 6:
 
# 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)
 +
# a PO [[sequent]]
  
 
== Rodin database implementation ==
 
== Rodin database implementation ==
−
Each component {{ident|compname}} is associated with:
+
Each component {{ident|compname}} is associated with:
 
* a {{file|compname.bpr}} file, which contains the proof trees associated with each PO (1/, 2/ and 3/ before).
 
* a {{file|compname.bpr}} file, which contains the proof trees associated with each PO (1/, 2/ and 3/ before).
 
* 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)
Line 16: Line 17:
 
PO being uniquely identified, it may be enough to consider a merge taking place PO by PO.
 
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.
+
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).
 +
 
 +
{{SimpleHeader}}
 +
!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
  
−
{{TODO|Describe the different scenarios, and the proposed merging actions}}
 
  
 
[[Category:Design proposal]]
 
[[Category:Design proposal]]

Revision as of 09:00, 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)
  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).


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
Retrieved from ‘https://wiki.event-b.org/index.php?title=Scenarios_for_Merging_Proofs&oldid=9262’