Keywords: Compensation, Transformée operationnelle, Annulation de groupe, Édition collaborative

Un cadre flexible pour l'annulation dans l'édition collaborative Résumé : Les systèmes d'édition collaborative fournissent un mécanisme d'annulation qui permet à un utilisateur de corriger ses erreurs ou de visionner des modifications précédentes. Il est difficile de fournir une telle fonctionnalité dans un environnement collaboratif où tous les utilisateurs sont autorisés à retirer les modifications effectuées par n'importe quel autre utilisateur. L'approche des Transformées opérationnelles permet d'assurer la cohérence des données partagées dans les systèmes d'édition collaborative. Toutes les approches existantes proposent une annulation indépendante du type d'application. Nous montrons, dans cet article, que ce type d'annulation peut donner des résultats inattendus pour un utilisateur. Par conséquent, nous proposons un nouveau framework générique et flexible pour l'annulation appelé "Compensation". Notre approche permet de définir une action adaptée pour contrebalancer les effets d'une modification.

Introduction

Collaborative editing systems allow people distributed in time and space to work together on shared documents. The major benefits of collaborative writing include reducing task completion time, reducing errors, getting different viewpoints and skills, and obtaining an accurate document [START_REF] Tammaro | Collaborative Writing Is Hard to Support: A Field Study of Collaborative Writing[END_REF][START_REF] Noël | Empirical study on collaborative writing: What do coauthors do, use, and like?[END_REF].

The undo mechanism has been recognized as an important feature of collaborative editing systems [START_REF] Abowd | Giving undo attention[END_REF][START_REF] Berlage | A framework for shared applications with a replicated architecture[END_REF][START_REF] Prakash | A framework for undoing actions in collaborative systems[END_REF][START_REF] Choudhary | A general multi-user undo/redo model[END_REF][START_REF] Sun | Achieving convergence, causality preservation, and intention preservation in real-time cooperative editing systems[END_REF]. In such systems, the most general model of undo mechanism allows any user to undo any edit operation at any time. Preserving consistency of shared data with the undo feature is a complex issue.

In collaborative editing, the Operational Transformation (OT) [START_REF] Sun | Achieving convergence, causality preservation, and intention preservation in real-time cooperative editing systems[END_REF][START_REF] Ellis | Concurrency control in groupware systems[END_REF] approach is recognized as a suitable approach to maintain consistency of shared documents. This approach has been applied to develop both real-time and asynchronous collaborative editors [?]. This framework considers two main components: the transformation functions, which are specific to an application, and the integration algorithm.

All undo algorithms proposed in the OT framework [START_REF] Ressel | An integrating, transformationoriented approach to concurrency control and undo in group editors[END_REF][START_REF] Ferrié | Concurrent undo operations in collaborative environments using operational transformation[END_REF][START_REF] Sun | Undo as concurrent inverse in group editors[END_REF][START_REF] Sun | Operation Context and Context-based Operational Transformation[END_REF] provide an undo at the integration algorithm level. The main goal is to return to a state on which the undone operation has never been performed. They are based on standard set of operations where the inverse of each operation is already included in this set of operations [START_REF] Sun | Undo as concurrent inverse in group editors[END_REF]. For instance, most of these algorithms are instantiated for operations insert and delete where the inverse of delete is insert and the inverse of insert is delete. This kinds of undo mechanisms has the advantage of not modifying the transformation functions specific to the application. However, through two motivating examples, we show that:

1. introducing undo feature in a collaborative editing systems impacts the definition of the operation set handled by the system, 2. a system undo may not achieve the user's undo intention.

Firstly, we consider a text collaborative editor. A user can produce three kind of modifications: insert a character, delete a character and update character's attributes (face, bold, italic, ...). Let's assume that a character "a" is inserted, put in bold "a" and finally deleted "". Now, a user wants to undo the deletion, the system generates the inverse operation, i.e. an insertion of the character "a". Obviously, the user expects to see the character "a" in bold. Unfortunately, the result is the character "a" which is no more in bold.

From this example, we note that the deletion removes the effects of two modifications: the insertion and the attribute update. Therefore, generating only an insertion to undo a deletion is not sufficient to achieve the expected effect. Undo mechanisms should also update the character attribute. Since existing undo approaches generate only one inverse operation, a solution consists in modifying existing operations 1 . Modifying the operation set implies to modify the transformation functions. Thus, to obtain a complete undo feature, even with an undo defined at the integration algorithm level, the modification of the operations and transformation functions cannot be avoided.

Figure 1: Undo in a graphical editor Secondly, under certain circumstances, the system functionality undo may not achieve the expected undo effect from a user point of view. For instance, we consider a graphical editor (Figure 1) in which the fill color of a circle can be updated. Initially, the circle is black. Now, two users update its color at the same time: user 1 updates it to gray, while user 2 updates it to white. Since the circle could have only one color, the system have to arbitrary choose one color: let's say the color gray. Now, user 1 wants to undo his operation. The system functionality undo generates a state on which only user 2's update was performed. Therefore, the circle turns into white. Depending on the context, this result could be desired. However, if we assume that a user is able to imagine the effect of its undo, user 1 will find this result surprising. Indeed, user 1 has seen the circle black and puts it in gray, so when he undoes his update, his intention is probably to obtain a black circle and not a white one as shown in Figure 1. On another hand, if it's the user 2 who undoes the "put in gray" operation after seeing the circle in white, his intention is probably to obtain a white circle.

This example illustrates that, depending on the context, the undo effect expected by a user could be different than a system undo effect. As a consequence, we claim that an undo framework must allow building any kind of undo effect: the regular one which we call system undo and other undo effects we call user undo. Based of these observations, we claim that an undo feature for an OT collaborative editing system must be designed specifically for an application. Thus, we introduce a novel undo approach, called Compensation, defined at the transformation function level. As suggested in [START_REF] Abowd | Giving undo attention[END_REF], our framework allows designing a user undo as well as a system undo.

In the compensation approach, we generate a new operation to counterbalance the effect of another one. For instance, in the text editor previously defined, we could add an operation "insertFormatted" to compensate the deletion of a bold character. Similarly, in the graphical editor, we can compensate user 1's operation by an operation which updates the circle's color to black.

INRIA

With the compensation approach, we can have the same result obtained in current undo approaches: we can define the compensation effect in a way that it rolls back the modification. Therefore, we can consider that system undo is a particular case of compensation.

The compensation approach brings the followings advantages. There is no specific mechanism required to integrate compensation operations when received on remote sites. The compensation relies only on a simple scheme which can be introduced in all existing OT algorithms. And finally, unlike existing undo approaches, the compensation does not limit the usage of log truncation algorithms [START_REF] Sun | Achieving convergence, causality preservation, and intention preservation in real-time cooperative editing systems[END_REF] defined for approaches without undo feature.

As a proof of concept, we apply the compensation framework to the Tombstone Transformation Functions (TTF) [START_REF] Oster | Tombstone transformation functions for ensuring consistency in collaborative editing systems[END_REF]. Using the compensation, we design two different ways of undoing in the TTF approach: a system undo and a user undo. The correction of the obtained models is proved formally by the automated proof environment VOTE [START_REF] Imine | Vote: Group editors analyzing tool: System description[END_REF].

Based on this approach, we build Graveyard, a collaborative real-time text editor prototype. Graveyard combines a SOCT2 [START_REF] Suleiman | Concurrent operations in a distributed and mobile collaborative environment[END_REF] algorithm that does not provide a native undo feature, with the TTF transformation functions extended with compensation operations. Finally, we obtain a reliable decentralized collaborative editor with an undo mechanism.

In this paper, we present our framework for compensation. We first describe the OT approach and its correctness criteria in the second section. Then, we present the compensation approach and show how it could be applied in section "Compensation approach". This section also deals with correctness issues and finally we show how our approach can be used with main integration algorithms. In the third section, we instantiate the compensation framework with the TTF transformation functions to obtain two different undo mechanisms for linear structures. We presents the Graveyard prototype which implements the approach in the forth section. Finally, we compare our approach with existing undo approaches in the fifth section.

The Operational Transformation (OT) approach

In the OT approach, shared documents are replicated. Each site contains its own copy of the document, and a user is supposed to work at one site. OT approach allows any user to modify at any time his own copy of the document. Therefore, different copies of the same document can be modified in parallel. In the OT model, a modification is represented as an operation. Each site sends all the locally generated operations to the other sites. On these other sites, such operations are seen as remote operations which have to be integrated for execution.

The CCI Model [START_REF] Sun | Achieving convergence, causality preservation, and intention preservation in real-time cooperative editing systems[END_REF] considers an OT system correct if it preserves Causality, Convergence and Intention.

Causality This criterion ensures that all operations ordered by a precedence relation, in the sense of the Lamport's happened-before relation [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF], will be executed in the same order on every copy.

Convergence

The system converges if all copies are identical when the system is idle.

Intention The expected effect of an operation should be observed on all copies.

To ensure these criteria, several integration algorithms were proposed [9, 15, 17, 18, 12, ?]. Causality preservation is mainly achieved by the use of state vectors or a central timestamper.

To ensure convergence, these algorithms use transformation functions to modify remote operations according to local ones. For instance, we consider two sites sharing the same text document (Figure 2). The initial state of the document is "Compnsation". On Site1, a user wants to insert a character 'e' to obtain "Compensation". Concurrently, on Site2, another user wants to insert a 's' at the end of the word. Each site sends its local operation to the other one. If Site1 and Site2 directly execute its remote operation, they do not obtain the same document. On Site1, the character 's' should have been inserted at position 12 instead of 11. In the OT model, a transformation functions T is devised in order to transform remote operations regarding concurrent operations. We call T (op Ins(11, 's )

x x q q q q q q q q q q q q q q q q q q "Compensation" "Compnsations"

Ins(11, 's ) Ins(4, 'e ) "Compensatiosn" "Compensations" Figure 2: Divergence scenario However, defining transformation functions is not sufficient to ensure convergence. In the OT approach, the correctness is based on two standard properties called T P 1 and T P 2. Some algorithms only require T P 1 such as SOCT4 [START_REF] Vidot | Copies convergence in a distributed real-time collaborative environment[END_REF], MOT2 [?] or COT [START_REF] Sun | Operation Context and Context-based Operational Transformation[END_REF], while others require T P 1 and T P 2 such as Adopted [START_REF] Ressel | An integrating, transformationoriented approach to concurrency control and undo in group editors[END_REF], GOTO [START_REF] Sun | Operational transformation in real-time group editors: Issues, algorithms, and achievements[END_REF], SOCT2 [START_REF] Suleiman | Concurrent operations in a distributed and mobile collaborative environment[END_REF].

The transformation property T P 1 defines a state equality. The state obtained by the execution of an operation op 1 on a state S followed by the execution of the operation T (op 2 , op 1 ) should be equal to the state obtained by the execution of op 2 on a state S followed by the execution of T (op 1 , op 2 ) :

T P 1 : S • op 1 • T (op 2 , op 1 ) = S • op 2 • T (op 1 , op 2 )
The property T P 2 ensures that the transformation of an operation against a sequence of operations does not depend on the transformation order of operations in this sequence.

T P 2 : T (op 3 , op 1 • T (op 2 , op 1 )) = T (op 3 , op 2 • T (op 1 , op 2 ))

INRIA

Finally, convergence and causality are not sufficient. For instance, in Figure 2, both sites could reach the state "Compensatiosn". Unfortunately, site2 's intention, which is to add the 's' after the 'n', is no more respected. The transformation functions have to be designed in order to ensure the intention preservation. Although a generic definition for intention has never been formalized, we assume that particular definitions can be expressed and verified for a given transformation functions set.

Compensation approach

The compensation is a generic framework which allows defining how an operation should be counterbalanced. To obtain any kind of effect when the user undoes an operation, we produce a new operation which has the wished effect. This new operation is treated as regular ones when integrated on local and remote sites.

In existing OT undo mechanisms, the undo effect is to return to a state on which the undone operation was never performed. We name such undo a system undo. If we want to obtain such a system undo, we can automatically prove that the operations and the transformation functions designed for such a compensation ensure this effect thanks to a formal property we call TPC.

In contrast to system undo, a user undo allows generating a new state which fits to user's expectation. The correctness of the transformation functions thereby relies on the intention preservation which, unfortunately, cannot be formally defined on a generic purpose. However, this intention preservation should be defined and verified for the considered transformation functions.

Given a set of operations, an instance of the compensation framework is built in three steps. Firstly, define the (possibly new) operations that counterbalance original ones. Secondly, define the transformation function for the new operations, if any. Thirdly, formally verify the properties required by the targeted integration algorithm.

Compensation mechanism

We call C(op) the compensation operation of op, i.e. the operation which counterbalances the effect of op, if op is the last executed operation. C(op) can be either a newly defined operation or an operation from the initial set.

C(op) is not necessary the inverse operation of op even in the case of system undo. For instance, in the text editor introducing example, the operation "insertFormatted" is not the inverse operation of the deletion, nevertheless, after its application, the document is in the state that we should have obtained if the deletion was never performed. In fact, the compensation in this example is a complete system undo.

However, since op may not be the last executed operation, we need to compute an operation C(op) which is defined on the current state. C(op) is the transformation of C(op) according to all operations which have been executed on the local site since the execution of op. Therefore, C(op) is treated as any other newly generated operation (i.e. sent to all remote sites in order to be integrated). To compute C(op) , we use the naive undo algorithm [START_REF] Ferrié | Concurrent undo operations in collaborative environments using operational transformation[END_REF], see Figure 3.

Instantiation

The first step to instantiate the compensation framework is to define all operations C(op).

We need to define each operation C(op) in such a way that S • op • C(op) is a state where the effect of op has been counterbalanced. When the definition of C(op) introduces new operation(s), the following step is to write transformation functions for each new operation(s). These transformation functions are standard transformation functions, and thus must be proven correct according to CCI criteria.

In the OT approach, the correctness is ensured by a set of properties that must be satisfied by the transformation functions. Since compensation operations are integrated as regular operations, we have to demonstrate that the new set of operations and transformation functions respect the standard properties for convergence and intention.

The transformation functions defined for regular and compensation operations have to ensure:

T P 1 and T P 2 (or only T P 1, depending on the integration algorithm) are required for consistency,

The intention preservation: Like regular operations, we have to verify that the effect of a compensation operation will be preserved. In case of system undo, we also need to satisfy a Transformation Property for Compensation2 (T P C). This property ensures that the compensation effect will always

Site1

Site2

C(op) @ @ op o o

C C Seq s s h h h h h h h h h h h h h h h

Seq = T (Seq, op) op = T (op, Seq) G G C(op ) u u C(op) = T (C(op), Seq ) C(op ) = C(T (op, Seq))
Figure 4: Respect of the system undo effect be the same, even if the operation compensated is not the last executed one. This condition is similar to the condition C4 [START_REF] Ferrié | Concurrent undo operations in collaborative environments using operational transformation[END_REF] and the condition IP 3 [START_REF] Sun | Operation Context and Context-based Operational Transformation[END_REF][START_REF] Sun | Undo any operation at any time in group editors[END_REF][START_REF] Sun | Undo as concurrent inverse in group editors[END_REF]. The condition T P C is formally defined as:

T P C : T (C(op), T (seq, op)) = C(T (op, seq))
Figure 4 explains the T P C property. Two sites make concurrent operations. Site1 generates op while site 2 generates a sequence of operations seq. Both sites receive remote operations, transform and integrate them. Now, they are on the same state. Consequently, if they want to compensate the same operation on the same state, they must obviously generate the same operation. Site1 generates C(op) and transforms it against following operations T (seq, op). Site2 compensates the last received operation which is T (op, seq). These two compensation operations are defined on the same state, they compensate the same operation, so the resulting operation must be the same. The verification of this property ensures that whenever an operation is compensated, the compensation effect remains the same.

So, there are properties to verify in order to ensure a correct OT system with compensation. Due to their conciseness, these properties are theoretically easy to prove. However, one of the particularity of the OT approach is the huge numbers of cases to check.

In such conditions, a hand proof is error-prone, and many transformation functions supposed hand-proven finally revealed themselves false (all counter examples can be found in [START_REF] Oster | Tombstone transformation functions for ensuring consistency in collaborative editing systems[END_REF]).

On another hand, each of the cases to check can be easily handled by an automated formal theorem prover. Consequently, we choose to use the proof environment VOTE [START_REF] Imine | Vote: Group editors analyzing tool: System description[END_REF] based on the theorem prover Spike [START_REF] Nieuwenhuis | Rewriting Techniques and Applications, 14th International Conference, RTA 2003[END_REF][START_REF] Stratulat | A general framework to build contextual cover set induction provers[END_REF] which generates all the cases and ensures the verification of all properties.

We have now defined a complete and generic framework to provide compensation in the OT approach. This framework could be applied to many transformation functions and integration algorithm. The following section will discuss about compensation and existing integration algorithms.

Integrating the compensation in existing integration algorithms

In the OT framework, integration algorithms (SOCT2, SOCT4, GOTO, COT, MOT2) are defined for operations (with no assumption about the number or the kind of operations) and need transformation functions to deal with these operations.

The compensation framework extends a set of operations and transformation functions to support a recovery mechanism. We obtain a new set of operations and transformation functions. Consequently, the resulting set can be handled by any existing integration algorithm.

Our framework also requires a compensation algorithm. To compensate an operation op, we generate a compensation operation C(op). The compensation algorithm transforms C(op) against all operations which have been executed after op. For this stage, C(op) is considered as concurrent to all operations after op. Fortunately, the main goal of every integration algorithm is to transform an operation against a set of concurrent operations.

Consequently, any OT integration algorithm can determine the compensation operation. The resulting operation is treated as a normal operation. Thus, the compensation algorithm can be easily integrated in any integration algorithm.

In the following section, we instantiate the compensation approach on the Tombstone Transformation Functions (TTF). The TTF have two particularities: they have non-inversible operations and are the only transformation functions that ensure T P 1 and T P 2 [START_REF] Oster | Tombstone transformation functions for ensuring consistency in collaborative editing systems[END_REF].

Compensation in the TTF approach

In order to illustrate the compensation approach, we choose to apply it on the TTF functions. We present the TTF functions in the following and then, apply the compensation. In the first place, we apply the compensation to build a system undo. This kind of recovery is suitable for patch undo and , especially, for vandalism reverting. In the second place, we propose the compensation as a user undo which fits differently to user's intention.

The Tombstones Transformation Functions

The TTF approach is divided in two parts: the model and the transformation functions. A detailed explanation of the TTF approach and its correctness can be found in [START_REF] Oster | Tombstone transformation functions for ensuring consistency in collaborative editing systems[END_REF].

The main idea of the model is to keep deleted characters as tombstones. The document's view only shows visible characters: tombstones are hidden. Consequently, the model differs from the view. Figure 5 illustrates this. Assume that a document is in a state "abcd". Now, a user deletes the character 'b'. In the TTF model, the character is replaced by a tombstone (i.e. the character with a visibility flag set to false). The view differs from the model as the view only contains "acd" while the model contains "ab /cd". Since tombstones are necessary to achieve consistency, they cannot be removed and thus, the operation "Ins" is not inversible. The TTF transformation functions (Figure 6) can only be used with the TTF model. In other OT approaches, the deletion of a character decreases the position of all the following characters. The TTF model's particularity is that a character's position can only grow. Therefore, transforming an operation against any "Del" operation will never modify it.

INRIA

T( Ins(p1, c1, sid1), Ins(p2, c2, sid2)):

if (p1 < p2) return Ins(p1, c1, sid1) else if (p1 = p2 and sid1 < sid2) return Ins(p1, c1, sid1) else return Ins(p1 + 1, c1, sid1) end T( Ins(p1, c1, sid1),Del(p2, sid2)):

return Ins(p1, c1, sid1) end T( Del(p1, sid1), Ins(p2, c2, sid2)):

if (p1 < p2) return Del(p1, sid1) else return Del(p1 + 1, sid1) end T( Del(p1, sid1), Del(p2, sid2)):

return Del(p1, sid1) end

Compensation as a "system undo"

The first step in applying the compensation framework is to define the compensation operations and their effect.

A system undo returns the system to a state on which the undone operation was never performed. In our context, this definition implies that a character deleted concurrently by N sites should not be visible unless each of these N delete operations are compensated.

To achieve a such behavior, we propose to associate, to each character, a visibility level. This visibility level is an integer. Initially, an inserted character has a visibility level of 1. Each time we compensate an insertion operation, the visibility level of the corresponding character is decreased. Each time we compensate a deletion, we increase the visibility level of this character.

A character is said "visible" and appears in the document's view if its visibility level is at least 1. Similarly, a character is said "invisible" and does not appear in the document's view if its visibility level is less than 1.

We choose to compensate the insertion with an operation "Del(p, sid)" which effect is to decrease the visibility level of the character at position "p". To compensate a deletion, we should increase the visibility level of the character. Since neither the operation "Ins", nor the operation "Del" could provide this effect, we add a new operation "Undel(p, sid)" which effect is to increase the visibility level of the character at position "p". Similarly, the compensation of an operation "Undel" have to decrease the visibility level. Fortunately, the operation "Del" produces this effect and can be used to compensate an operation "Undel".

Site1 "a 1 b 1 c 1 " Site2 "a 1 b 1 c 1 "
Del(0, sid 1 ) The second step is to write transformation functions for all operations. The definition of the transformation functions for the operations "Ins" and "Del" are the same as presented in Figure 6.

4 4 i i i i i i i i i i i i i i compens. A A Del(0, sid 2 ) Õ Õ "a / 0 b 1 c 1 "a / 0 b 1 c 1 U ndel(0, sid 1 ) 4 4 i i i i i i i i i i i i i i Del(0, sid 1 ) "a 1 b 1 c 1 "a / -1 b 1 c 1 Del(0, sid 2 ) U ndel(0, sid 1 ) "a / 0 b 1 c 1 "a / 0 b 1 c 1
As the operations "Del" and "Undel" just influence the fact that a character is visible in the view or not, they do not modify the position of the document's characters stored in the model. Consequently, an operation transformed against any "Undel" (or "Del") operation is not modified.

T( Ins(p1, c1, sid1),Undel(p2, sid2)):

return Ins(p1, c1, sid1) end T( Del(p1, sid1), Undel(p2, sid2)):

return Del(p1, sid1) end T( Undel(p1, sid1), Ins(p2, c2, sid2)):

if (p1 < p2) return Undel(p1, sid1) else return Undel(p1 + 1, sid1) end T( Undel(p1, sid1), Undel(p2, sid2)):

return Undel(p1, sid1) end T( Undel(p1, sid1), Del(p2, sid2)):

return Undel(p1, sid1) end Since these transformation functions are bijective, they can easily be reversed and consequently allow us to apply our approach with integration algorithms as SOCT2, GOTO which require reversible transformation functions.

The last step is to prove the correctness of the previous transformation functions.

Using the proof environment VOTE [START_REF] Imine | Vote: Group editors analyzing tool: System description[END_REF], we have proven that our transformation functions verify the properties T P 1, T P 2 and T P C. The system specification given to the theorem prover Spike3 can be reviewed and tested at the following url: http://graveyard. sf.net/.

Compensation as a "user undo"

The first step in applying the compensation framework is to define the compensation operations and their effect.

In this case, we assume that, when a user compensates a deletion, the expected effect is to see the deleted character even if it has been deleted many times. In other words, user's intention is: "make this character visible".

As a result, an insertion is compensated by an operation "Del(position, id, sid)" which makes the character invisible. A deletion is compensated by making the character visible. Since no operation achieves this effect, we add a new operation "Undel(position, id, sid)".

Compensating an operation "Undel(position, id, sid)" consists in making the character invisible, then we use the operation "Del(position, id, sid)". The field "id" is an integer which indicates whether the operation has an effect or not. If "id" is superior to 0, the operation has no more effect since a concurrent operation has already achieve the expected effect.

Then we define the function C: The second step is to write transformation functions for all operations ( Figure 8 4 ). Figure 9 illustrates the behavior of this user undo. This scenario is similar to Figure 7 and emphasizes the difference between system undo and user undo. Site1 and Site2 generate concurrently an operation to delete the character 'a'. When Site1 cancels his deletion by generating an operation "U ndel(0, 0, sid 1 )", the user at this site expects to see the character 'a'. After integrating remote operations, Site1 and Site2 are in the same state and the user at Site1 sees the expected result.

The last step consists in proving the correctness of our transformation function.

Using the proof environment VOTE [START_REF] Imine | Vote: Group editors analyzing tool: System description[END_REF], we have proven that our transformation functions verify the properties T P 1 and T P 2. The system specification given to the theorem prover Spike can be reviewed and tested at the following url : http://graveyard.sf.net/.

In this approach, we define the following intentions for the operations :

"Ins" The order relationships between characters must be preserved. In [START_REF] Oster | Tombstone transformation functions for ensuring consistency in collaborative editing systems[END_REF], the authors prove that the TTF functions preserve these order relationships. The operations "Del" and "Undel" only modify the visibility of a character, not the position. Therefore, our approach preserves these relationships.

"Del" The intention of the "Del" operation is to obtain the character invisible. From the definition of the execution of "Del", del(p, i, sid) has an effect only if i = 0. When generated by the user, we get i = 0, and the effect is realized. When transformed, T( Ins(p1, c1, sid1), Del(p2, i2, sid2)): return Ins(p1, c1, sid1) end T( Ins(p1, c1, sid1), Undel(p2, i2, sid2)):

return Ins(p1, c1, sid1) end

T( Undel(p1, i1, sid1), Ins(p2, c2, sid2)): if (p1 < p2) return Undel(p1, i1, sid1) else return Undel(p1 + 1, i1, sid1) end T( Del(p1, i1, sid1), Ins(p2, c2, sid2)): if (p1 < p2) return Del(p1, i1, sid1) else return Del(p1 + 1, i1, sid1) end T( Del(p1, i1, sid1), Del(p2, i2, sid2)): if (p1 = p2 and i2 = 0) return Del(p1, i1 + 1, sid1) else return Del(p1, i1, sid1) end T( Del(p1, i1, sid1), Undel(p2, i2, sid2)):
return Del(p1, i1, sid1) end T( Undel(p1, i1, sid1), Undel(p2, i2, sid2)):

if (p1 = p2 and i2 = 0) return Undel(p1, i1 + 1, sid1) else return Undel(p1, i1, sid1) end T( Undel(p1, i1, sid1), Del(p2, i2, sid2)):

return Undel(p1, i1, sid1) end Figure 8: TTF transformation functions with a "user undo" i = 0 remains true except if the del(p, i, sid) operation is transformed against another del(p, 0, sid ), i.e. if the intention is already realized.

"Undel" The intention of the "Undel" operation is to obtain the character visible. Since the definitions of "Del" and "Undel" are the symmetric, the intention of "Undel" is also respected.

Site1

"abc" Site2 "abc" Del(0, 0, sid 1 )

5 5 r r r r r r r r r r r r r r r r compens.
A A Del(0, 0, sid 2 )

Ô Ô Ù Ù Ù Ù Ù Ù Ù Ù Ù Ù Ù Ù Ù Ù Ù Ù Ù Ù Ù Ù Ù Ù Ù Ù Ù "a /bc "a /bc
U ndel(0, 0, sid 1 )

5 5 r r r r r r r r r r r r r r r r Del(0, 1, sid 1 )
"abc "a /bc Del(0, 2, sid 2 ) U ndel(0, 0, sid

"abc "abc Figure 9: User undo

TPC and user undo

In the system undo strategy, we assume that the expected undo effect is to remove an operation from the system. On the contrary, in the user undo strategy, we remove an effect from the document. Thus T P C may contradict user intention in the case of a user undo. An example of this contradiction is show in figure 10 5 . In this example, two users delete concurrently intersecting parts of the document "abc". User1 deletes "ab" while User2 deletes "bc". For User2, the observed effect of User1's operations is only to remove "a"; and if he undoes these operation, he wants only "a" to appear.

For User1, the effect of his actions is obviously to remove "ab"; and if he undoes them, he wants "ab" to appear. So, two user's undo intention of the same operation could lead to two different operations. Thus, T P C contradicts users' intentions in this case.

Implementation

In order to validate our approach, we have built the Graveyard prototype. Graveyard is a real-time collaborative text editor (cf. figure 11). It relies on the SOCT2 algorithm for User1 "abc" User2 "abc" Del(0, 0, s 1 ) Del(1, 0, s 1 )

• So, we wrote the TTF document that extends the Swing text editor abstract document. This document manages invisible characters when inserting and removing characters. This model also forward local operations to the other connected editors through the workspace manager.

2 2 f f f f f f f f f f f f f f compens. ( (
Del(1, 0, s 2 ) Del(2, 0, s 2 ) • || | | | | | | | | | | | | "a /b /c "ab /b / Del(1, 1, s 2 ) Del(2, 0, s 2 ) • Del(0, 0, s 1 ) Del(1, 1, s 1 ) • compens. { { "a /b /c / "a /b /c / U ndel(0, 0, s 1 ) U ndel(1, 0, s 1 ) • U ndel(0, 0, s 1 ) U ndel(1, 1, s 1 ) • "abc / "ab /c /
The workspace manager sends local operations to other sites and handles remote operations reception. When a remote operation is received and is causally ready, this operation is transformed against concurrent operations using the SOCT2 algorithm and TTF transformation functions. The resulting operation is executed on the TTF document. This update is notified to the swing text editor. For managing membership and network broadcast, we use the JGroups8 toolkit. This toolkit allows us to test various broadcast protocols.

The undo feature is accessible in graveyard with traditional keys. By typing 'control-z', the user can undo his operations that are not always the last executed operations. The undo panel at the left (see figure 11) contains all operations integrated on the local site. The user can select any operation and compensate them by clicking on the button "Undo".

The graveyard prototype is available under the GPL license on sourceforge9 .

Related Work

In [START_REF] Ressel | Reducing the problems of group undo[END_REF], the authors present an undo specific to the adOPTed algorithm by adding two functions called "mirror" and "fold". Unfortunately, this solution cannot allow undoing any operation at anytime. Since the adOPTed algorithm requires transformation functions satisfying T P 1 and T P 2, we can use the TTF functions in association with the compensation approach. Therefore, we can instantiate adOPTed and provide an undo for any operation. The ANYUNDO algorithm [START_REF] Sun | Undo as concurrent inverse in group editors[END_REF] is associated with the GOTO integration algorithm. This approach introduces three undo properties called IP 1, IP 2 and IP 3. The property IP 3 is similar to the property T P C. The property IP 1 illustrates the neutrality of do-undo pairs toward the document state while the property IP 2 illustrates the neutrality of do-undo pairs toward transformation functions. The properties IP 2 and IP 3 are enforced by the ANYUNDO algorithm. Therefore, the GOTO-ANYUNDO approach needs transformation functions which satisfy three properties T P 1, T P 2 defined for operation satisfying IP 1. Unfortunately, transformation functions satisfying IP 2 and IP 3 defined for operations satisfying IP 1 have never been published. The TTF approach satisfies T P 1 and T P 2 but is defined for operations which do not satisfy IP 1. However, we can still provide compensation in GOTO. Operations and transformation functions described in this paper can be used in the GOTO integration algorithm to provide either a system undo or a user undo without using the ANYUNDO algorithm.

In [START_REF] Ferrié | Concurrent undo operations in collaborative environments using operational transformation[END_REF], the authors define two properties C3 and C4 which are similar to IP 2 and IP 3. To ensure the verification of these two properties, the authors introduce a specific operation "undo(op)". This approach defines generic transformation functions for this operation "undo(op)" using the proposed transformation functions. The main idea to enforce C4 is to swap the operations and undo the resulting operation. Unfortunately, the authors do not discuss the case of causally dependent operations. This leads to incorrect results.

In the COT approach [START_REF] Sun | Operation Context and Context-based Operational Transformation[END_REF], an undo operation is defined on the generation state of the operation that we want to undo. The state is represented by a "context vector" associated to each sent operation. Unlike state vectors which only capture normal operations , context vectors are designed to capture also undo operations. Unfortunately, context vector's size grows linearly with the number of undone operations. Therefore, the use of context vector limits the number of undo which can be performed during an editing session. One can use the compensation approach with the COT's integration algorithm. This allows obtaining an undo mechanism in the COT approach without using "context vectors".

From a generic point of view, existing undo mechanisms place into the operation log undo operations directly next to original one in order to form do-undo-pairs [START_REF] Ressel | Reducing the problems of group undo[END_REF][START_REF] Sun | Undo as concurrent inverse in group editors[END_REF][START_REF] Ferrié | Concurrent undo operations in collaborative environments using operational transformation[END_REF][START_REF] Sun | Operation Context and Context-based Operational Transformation[END_REF]. This behavior limits the supports of log truncation features. Indeed, if the original operation is dropped, undo operation cannot be integrated. Since compensation operations are treated as do operation, every operation in the log of the local site can be compensated and remotely integrated even if it has been dropped by the other sites.

From a correctness point of view, the existing undo mechanisms rely on some properties that the transformation functions must ensure or that the undo mechanism enforces. These properties are designed to resolve some known undo puzzles. Mechanisms which enforce such properties could break causality, convergence or intentions. However, since compensation operations are integrated as other operations, their correctness rely directly on the CCI criteria:

Causality is ensured by the integration algorithm Convergence is ensured by the respect of TP1 and, if required, TP2.

Intention must be ensured by the execution of the operations and their transformation as well for compensation operation as for standard operation 10 . Unfortunately, OT framework does not provide a generic scheme to show that an operation's intention is respected. This issue must be addressed for each set of operations as we done for the instances of compensation for TTF.

However, compared to undo built at the integration level, the compensation approach has a drawback. The compensation implies an additional development cost on account of the addition of new operations. But, this additional cost cannot be avoided if original operations are not inversible -such as TTF operations -or if the original set of operations is not sufficient to produce a complete undo -such as the "insertFormatted" example. This cost is mostly a property verification cost and can be reduced thanks to automated verification techniques [?].

Finally, compared to the above approaches, the use of the compensation approach brings several improvements: it improves the performances, extends the undo functionality add/or even replaces a non-instantiable undo mechanism. One main characteristic of compensation approach is to realize the undo feature at the transformation functions level. It makes the undo feature independent of the integration algorithm. So the compensation approach can be used with any integration algorithm.

Conclusions

In all existing OT approaches, undo is designed at the integration algorithm level and proposes a system undo. In this paper, we introduced our compensation framework which provides the system undo and, furthermore, a new way to undo called user undo. The user undo allows expressing the user's intention undo [START_REF] Abowd | Giving undo attention[END_REF][START_REF] Garcia-Molina | Sagas[END_REF].

With a little additional design cost -that may not be avoided to build a correct undoour framework allows defining any adequate action to counterbalance the effect of an operation. Since system undo is just one of these possible actions, we claim that the compensation is more generic than existing undo approaches. An important feature of our approach is that the resulting transformation functions remain generic towards integration algorithms. Consequently, we can apply these functions with COT, SOCT2, SOCT4, MOT2, GOTO and adOPTed. We have a complete solution to build correct decentralized text editors with a flexible undo capability and a log truncation feature. The TTF transformation functions with the system undo proposed in this paper has been implemented in the Graveyard collaborative text editor.

In future work, we will integrate the TTF transformation functions with the user undo. Thus, a user study will be settled to determine which undo strategy is the most adequate depending on the context. The major drawback of the compensation as a user undo, which is shared with the OT approach in general, is the lack of a formal definition and generic properties to ensure user's intention. As a result, we will try to obtain a formalization of user's intention.

Figure 3 :

 3 Figure 3: Algorithm of the compensation

Figure 5 :

 5 Figure 5: Model in the TTF approach.

Figure 6 :

 6 Figure 6: TTF transformation functions

Figure 7 :

 7 Figure 7: Visibility level

C

  (op): INRIA IF op = Ins(p, c, sid) THEN C(op) := Del(p, sid) IF op = Del(p, sid) THEN C(op) := U ndel(p, sid) IF op = U ndel(p, sid) THEN C(op) := Del(p, sid)

C

  (op): IF op = Ins(p, c, sid) THEN C(op) := Del(p, 0, sid) IF op = Del(p, i, sid) THEN C(op) := U ndel(p, i, sid) IF op = U ndel(p, i, sid) THEN C(op) := Del(p, i, sid)

Figure 10 :Figure 11 :

 1011 Figure 10: TPC and user undo

Figure 12 :

 12 Figure 12: Graveyard architecture

  1 , op 2 ) the operation op 1 transformed against the operation op 2 .

	Site1	Site2
	"Compnsation"	"Compnsation"
	Ins(4, 'e ) w w w w w w w w w w w w w w w w 8 8 w w

Another solution may consist in generating many operations to undo one, but such a modification introduces consistency issues that have never been addressed.RR n°6516

RR n°6516

We discuss of this property for a user undo is section "Comparing system undo and user undo" INRIA

http://lita.sciences.univ-metz.fr/ ~stratula RR n°6516

Some transformation functions are similar to TTF functions and hence, are not reported on this figure.INRIA

This scenario does not lead to inconsistency, since sites will eventually converge when both set of undelete operation will remotely be integrated.INRIA

http://en.wikipedia.org/wiki/Swing_(Java)

http://www.eclipse.org/

http://www.jgroups.org INRIA

http://graveyard.sf.net RR n°6516

Even with traditional undo properties (IP2/IP3 or C3/C4) or our property TPC, intention preservation is never formally proved to be ensured in any case.INRIA

http://www.inria.fr ISSN 0249-6399