Keywords: Compensation, Transformation Operationnal, Group undo, Collaborative Editing Compensation, Transformée operationnelle, Annulation de groupe, Édition collaborative Compensation in Collaborative C2.4 [COMPUTER-COMMUNICATION NETWORKS]: Distributed Systems ; H5.3 [INFORMATION INTERFACES Algorithms, Verification, Reliability CSCW, Collaborative editing, undo, compensation, Operational Transformation

Compensation 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 totalement décentralisé 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. Nous présentons, dans cet article, une nouvelle approche pour l'annulation dans le contexte des transformées opérationnelles. Notre approche est basée sur la notion de compensation utilisée dans les bases de données. Dans cette approche, les opérations de compensation annulent sémantiquement les effets des autres opérations. Notre mécanisme de compensation est moins contraignant que les autres approches pour l'annulation. Notre approche est également génerique du fait qu'elle peut être utilisée en association avec n'importe quel algorithme de transformation opérationnelle.

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 co-authors do, use, and like?[END_REF].

Undo/Redo has been recognized as an important feature of collaborative editing systems [START_REF] Abowd | Giving undo attention[END_REF][START_REF] Sun | Achieving convergence, causality preservation, and intention preservation in real-time cooperative editing systems[END_REF][START_REF] Choudhary | A general multi-user undo/redo model[END_REF][START_REF] Prakash | A framework for undoing actions in collaborative systems[END_REF][START_REF] Berlage | A framework for shared applications with a replicated architecture[END_REF]. In collaborative 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.

All undo algorithms proposed in the OT framework [START_REF] Ressel | An integrating, transformation-oriented 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 | Consistency maintenance in real-time collaborative graphics editing systems[END_REF][START_REF] Sun | Operation Context and Context-based Operational Transformation[END_REF] provide an undo feature as a rollback of previous modifications. Such approaches assume there is an inverse operation, associated to each operation affecting the document, that makes the document return syntactically to a previous state. This kind of recovery, sometimes called backward error recovery, is not always possible. For instance, when a bookkeeper validates an operation, he cannot cancel this operation. If he makes a mistake, he has to compensate his operation by generating a new operation that semantically undoes the previous one. The resulting state is not equal to initial state. This concept is well known in the database community as forward error recovery or compensation [START_REF] Garcia-Molina | Sagas[END_REF]. The main idea of our own approach is to execute an adequate compensating modification instead of rolling back the erroneous modification. This choice have two main advantages.

• In essence, the compensation approach includes the rollback approaches. As we can define the compensating effect in a way that it rolls back the modification, we can consider that backward recovery is a particular case of compensation. In addition, this approach can provide a recovery mechanism even in a system which does not allow rollback of modifications.

• Since compensation is a forward error recovery, the compensation operations are treated as any other newly produced operations. There is no specific mechanism required to handle such operations when received on remote sites. This simple scheme can be introduced in all existing OT algorithms including GOTO [START_REF] Sun | Consistency maintenance in real-time collaborative graphics editing systems[END_REF], COT [START_REF] Sun | Operation Context and Context-based Operational Transformation[END_REF], adOPTed [START_REF] Ressel | Reducing the problems of group undo[END_REF]. It can provide undo capabilities even to algorithms that do not provide this feature natively as SOCT2 [START_REF] Suleiman | Concurrent operations in a distributed and mobile collaborative environment[END_REF], and SOCT4 [START_REF] Vidot | Copies convergence in a distributed real-time collaborative environment[END_REF].

As a proof of concept, we applied the compensation framework to the Tombstone Transformation Functions (TTF) [START_REF] Oster | Tombstone transformation functions for ensuring consistency in collaborative editing systems[END_REF] which handles non inversible operations. The correction of the obtained model 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 the Graveyard real-time editor prototype. Graveyard com-

RR n°6160

bines a SOCT2 algorithm that does not provide a native undo feature, with TTF transformation functions extended with compensation operations. Finally, we obtain a reliable fullydecentralized collaborative editor with an undo mechanism.

qIn this paper, we detail our framework for compensation. We first describe the OT approach and its correctness criteria in Section 2.

We then present the algorithm generating compensation operations and the properties required on the transformation functions in Section 3.

We show that our approach can be integrated in well-known OT integration algorithms in Section 3.2. We also show how this framework is applied on the tombstone transformation functions approach including the proof of required properties and an implementation in Section 4. Finally, we compare our approach with existing backward recovery approaches in Section 5.

THE 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 that have to be integrated for execution.

In the Ressel Model [START_REF] Ressel | An integrating, transformation-oriented approach to concurrency control and undo in group editors[END_REF], the system is correct if it preserve Causality and Convergence.

Description Considering two operations op1 and op2, operation op1 is said to precede op2 if and only if op2 is generated on a copy after op1 was executed on this copy. Subsequently, op2 may depend on effects of execution of op1. Causality preservation 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. Two operations op1 and op2 that are not related by a precedence relation (neither op1 precedes op2, nor op2 precedes op1) are said to be concurrent.

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

For example, we consider two sites sharing the same text document (Figure 1). x x 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" However, defining a transformation function is not sufficient to ensure convergence. In the OT approach, the correctness is based on two standard properties T P1, T P2. Some algorithms only requires T P1 such as SOCT4 [?] or COT [START_REF] Sun | Operation Context and Context-based Operational Transformation[END_REF],

INRIA

Compensation in Collaborative Editing others require T P1 and T P2 such as Adopted [START_REF] Ressel | An integrating, transformation-oriented 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 P1 defines a state equality. The state obtained by the execution of an operation op1 on the initial state S followed by the execution of the operation T (op2, op1) should be equal to the state obtained by the execution of op2 on the initial state S followed by the execution of T (op1, op2) :

T P1 : S • op1 • T (op2, op1) = S • op2 • T (op1, op2)
The property T P2 ensures that the transformation of an operation against a sequence of operation does not depend on the transformation order of the operation in the sequence.

T P2 : T (op3, op1 • T (op2, op1)) = T (op3, op2 • T (op1, op2))

COMPENSATION APPROACH

Existing undo methods for OT enforce the document to return to a previous state after the execution of an undo operation. The compensation approach do not require the system returns to a previous state but only to a state semantically equal to a previous state. However, in some cases, this semantically equal state can be syntactically equal to the previous state.

We call C(op) the operation which compensates op. The execution of the operation C(op) undoes, from a semantic point of view, the effect of the operation op. C(op) is not necessary the inverse operation of op but it is defined in order to compensate op just after the execution of 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 semantically undone.

On Figure 2, a site generates two operations op1 and op2. Now, it wants to compensate the last executed operation which is here op2. Using a function C, we determine the operation op3 = C(op2) which compensate op2. For this example, we chose C(Ins(p, c)) = Del(p).

Site1

"bd" We define the effect of compensating operations on the state obtained after the execution of the operation to be compensated. To compensate an operation op just after its execution, we generate an operation C(op). The operation C(op) will compensate the operation op if op is the last executed operation.

op1 = Ins(1, c ) "bcd" op2 = Ins(0, a ) "abcd" op3 = C(op2) = Del(0) "bcd"
In order to compensate any operation, and not only the last executed operation, we have to transform the compensation operation. On Figure 3, the initial state of the document is "bd". First we add a 'c' between 'b' and 'd'. Then, we add a 'a' at the beginning of the document. Now we want to compensate the operation op1 which is not the last executed operation. The compensation of the insertion of a 'c' is obviously the deletion of this character. Unfortunately, the direct execution of the operation C(op1) deletes the characters 'b'.

Indeed, the operation C(op1) does not take account of the effect of the operation op2 executed after op1. We need to compute an oper-

RR n°6160

Weiss, Urso and Molli Site1 "bd"

op1 = Ins(1, c ) "bcd" op2 = Ins(0, a ) "abcd" op3 = C(op1) = Del(1)
"acd" 1. First, we determine the operation C(op) which compensates op. C(op) should have compensated op if op was the last operation executed on the current site.

2. We use the forward transformation functions in order to transform C(op) with all operations which have already been executed on this site. The resulting operation is called C(op) . C(op) is defined on the current state and will be send to other sites where it will be integrated as any other operation.

This algorithm is known as the naive algorithm for undo [START_REF] Ferrié | Concurrent undo operations in collaborative environments using operational transformation[END_REF].

We need to ensure that the effect of C(op) is the same as C(op) if op was the last executed operation. In OT approach, correctness is ensured by a set of properties that must be satisfied by the transformation functions. Since integration algorithms make no distinction between compensating operations and other operations, compensating operations have also to satisfy the correctness properties.

Correctness of the compensation approach

The compensation approach does not depend of the integration algorithm. It is defined at the transformation functions level. In order to be correct, the transformation functions defined for regular and compensation operations have to ensure:

• at least T P1 or T P1 and T P2 if T P2 is required.

• T Pc to ensure the respect of compensation. These property ensures that the compensation effect will always 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]Undo as concurrent inverse in group editors[END_REF].

The compensation effect is defined on the state obtained by the execution of the compensated operation. This effect should be preserved if the operation we want to compensate is not the last. The property

INRIA Compensation in Collaborative Editing Site1 Site2 C(op) A A op o o C C W W W W W W W W W W W W W W W W W W
Seq s s g g g g g g g g g g g g g g g g g T PC expresses that the effect defined on a state will not be modified by concurrent operation. The condition T pc is formally defined as:

Seq = T (Seq, op) op = T (op, Seq) G G C(op ) r r C(op) = T (C(op), Seq ) C(op ) = C(T (op, Seq)
T PC : T (C(op), T (seq, op)) = C(T (op, seq))
Figure 5 explains the T Pc 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 generate C(op) and transform it through following operations T (seq, op). Site2 compensate the last received operation which is T (op, seq). These two compensating operations are defined on the same state, they compensate the same operation, so they 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 three -or two -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 | Proving correctness of transformation functions in collaborative editing systems[END_REF]).

On an other hand, each of the cases to check can be easily handle by a 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 generate all the cases and ensure the verification of all properties. If property are violated, the environment return the found counter-example as a scenario. Such scenario are very useful to correct the problematic transformation function. If the theorem prover succeeds, the obtained proof is theoretically indisputable. But this proof is based on a hand-written specification. Thus, a claim that a system is automatically proved must be associated with the specification for careful reading.

Of course, the usage of the VOTE environment in particular is not mandatory to validate the properties, and this verification can be done by any other suitable formal method or either by a hand-proof if the system designer is enough confident.

RR n°6160

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 algorithm

In the OT framework, integration algorithm (SOCT2, SOCT4, GOTO, COT) are defined for operations (with no assumption about the number or the kind of operation) 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 to obtain a new set of operations and transformation functions. Consequently, the resulting set can easily be used with existing integration algorithm.

Our framework also requires a compensation algorithm. To compensate an operation op, we generate a compensating operation C(op).

The compensation algorithm transforms C(op) with 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 algorithms is to transform an operation against a set of concurrent operations. For instance :

• In the adOPTed [START_REF] Ressel | Reducing the problems of group undo[END_REF] algorithm, we can call the Translate Request method with arguments C(op) and the state vector of op to obtain C(op) . We then need to remove C(op) and its transformed versions from the model and send C(op) with the current state vector incremented as for a new operation.

• In the SOCT4 [START_REF] Vidot | Copies convergence in a distributed real-time collaborative environment[END_REF] algorithm, since the history of each site is ordered using a continuous global order, we just have to call the Transpose Forward method on C(op) and all the operations following op in the history to obtain C(op) .

• In the COT [START_REF] Sun | Operation Context and Context-based Operational Transformation[END_REF] algorithm, we can call, as the authors do for their undo mechanism, the COT-DO method with arguments C(op), with the same "context vector" as op, and the current document state.

On the other hand, we do not have to include C(op) in the context vector of op and we send C(op) with the context vector of a new operation.

Consequently, any OT integration algorithms can determine the compensating operation. The resulting operation is treated as a normal operation. Thus, we can use the compensation algorithm with any integration algorithm.

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

COMPENSATION IN THE TTF APPROACH

The compensation approach could be applied to the same functions as the undo approach and for transformation functions defined on operations which are not inversible. In order to illustrate the compensation approach, we choose to apply it on the TTF functions. In the TTF approach, the operation "Ins" is not inversible and consequently, the traditional undo approaches could not be used.

To apply the compensation to a transformation function, we first need to define compensating operations. For each operation, we define an operation which compensate its effect. A compensating operation does not necessary exist in the initial set of operation. Using the definition of compensating operation, we can easily write the function C.

INRIA

Compensation in Collaborative Editing

Afterward, we write the transformation functions for all operations. Finally, we must prove that our transformation functions verify the properties T P1, T P2 and T PC .

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 and tombstones are hidden. Consequently, the model differs from the view. Figure 6 illustrates this. Assume that a document is in a state "abcd". Now, 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 7) can only be used with the TTF model. These functions are defined for two kind of operations: an operation "Ins(p, c, sid)" which inserts a character and an operation "Del(p, sid)" which deletes a character. Parameters of an insertion are the position p, the character c and the site identifier sid. Parameters of a deletion are the position p and the site identifier sid. Operations are computed according the model. Consequently, on Figure 6, on state "ab /cd", to delete the character 'c' which has the position 3 in the model, the generated operation is "Del(3, sid)".

In other OT approaches, the deletion of a character decreases the position of all following characters. transforming an operation with any operations "Del" will never modify it.

Defining compensating operations

As the TTF approach is defined for two operations: "Ins(p, c, sid)" and "Del(p, sid)", we need to find two operations to compensate them. The compensating effect required is to obtain that visible characters are the same (Figure 8).

Fortunately, it is obvious that there is no difference between compensating an insertion and deleting a character. So we can use the operation "Del" for compensating "Ins" since it has the desired effect which is removing the character in the user's view. If we use the operation "Ins" to compensate an operation "Del", the transformation functions do not satisfy the property T PC as shown in (Figure 9). This scenario was obtained with the proof environment VOTE.

RR n°6160

Site1

"a" Site2 "a" op1 = Del(0, a , sid1)

A A R R R R R R R R R R R R R R R R R R R R R R R R compens. 6 6 op2 = Ins(0, b , sid2)
u u l l l l l l l l l l l l l l l l l l l l l l l l "a /" "ba"

op 2 = Ins(0, b , sid2) op 1 = Del(1, a , sid1) compens.

{ {

"ba /" "ba /" C(Del(0, sid1)) = Ins(0, a , sid1) C(op 1 ) = Ins(1, a , sid1)

"aba /" "baa /"

Figure 9: T PC counter-example

Two sites share the same document "a" (Figure 9). Site1 deletes the character 'a' while Site2 inserts a character 'b' before the 'a'. After the execution of remote operations, each site owns the same document "ba /". As they are in the same state, they must generate the same compensating operation to compensate the same operation. Site2 compensates op 1 which is the last executed operation. Site1 compensates op1. Consequently, it generates the operation "Ins(0, a , sid1)" and, according to the compensation algorithm, transform it with the operation op2. As sid1 < sid2, the resulting operation is "Ins(0, a , sid1)" which is not the same operation as the operation obtained by site 2. Consequently, the transformation functions do no verify the property T PC1 .

Compensating the operation "Del" with the operation "Ins" inserts a new character in spite of the existing tombstone for this character. Thus, we define a new operation "Undel(position, sid)" to compensate the operation "Del". This operation replace the tombstone of a deleted character by the original character. This operation "Undel" allows to build transformation function which satisfy T PC and to reuse tombstones.

The function C(op) links normal operations to compensating operations. As we have defined compensating operations, we can now write the function C(op). Finally, we can write the transformation functions for all operations. The definition of the transformation functions for the operations "Ins" and "Del" are the same as presented in 7.

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 with any "Undel" (or "Del") operations is not modified. Since the transformation functions are bijective, they can easily be reversed (Figure 10) and consequently allow us to apply our approach with integration algorithms as SOCT2, GOTO which require reversible transformation functions.

Correction of the approach

In the TTF approach, the transformation functions are written in order to satisfy the property T P2. The property T P1 is defined by a state equality, then we have to define the effect of the operation "Undel" on the state. If the effect of "Undel" is simply to make the character visible, the property T P1 is violated (see Figure 11)

To ensure T P1, we define the effect of "Undel" replacing the visibility flag associated to characters by a visibility level. This visibility level is an integer. Initially, a character inserted have a visibility level of 1. Each time an operation deletes this character, its visibility level is decreased. Each time an operation undeletes this character, we increase its visibility level. A character is said "visible" and appears in the document's view if its visibility level is at least 1. And a character is said "invisible" and RR n°6160

does not appear in the document's view if its visibility level is less than 1.

Site1 "a1b1c1" Site2 "a1b1c1" Del(0, sid1) Figure 12, we assume that two sites share the same document containing a string "abc". We assume that the visibility level associated to each characters is 1. Site1 and Site2 generate concurrently an operation to delete the character "a". The visibility level is decreased on both sites. As the visibility level is less than 1, the character is not visible. When site2 receives site1's operation, site2 decreases the visibility level associated to the character "a". Site1 cancels his deletion by generating an operation "U ndel(0, sid1)". The execution of this operation increases the visibility level and the character 'a' is now visible. After integrating remote operations, site1 and site2 are in the same state and the visibility level associated to each characters is the same on both sites. This behavior is similar to the undo effect defined in [START_REF] Ressel | Reducing the problems of group undo[END_REF].

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 P1, T P2 and T PC . The system specification given to the theorem prover Spike can be reviewed and tested at the follow-ing url : http://potiron.loria.fr/projects/ graveyard.

Implementation

Figure 13: Graveyard real-time editor

In order to validate our approach, we have built the Graveyard prototype. Graveyard is a realtime collaborative text editor (cf. figure 13).

It relies on the SOCT2 algorithm for integrating concurrent operations. SOCT2 does not provide natively undo capabilities. We used the TTF transformation functions with related compensation operations to obtain a real-time collaborative with undo feature. The general architecture of graveyard is described in figure 14 For this implementation, we used SOCT2 but we can replace SOCT2 by SOCT4, adOPTed or GOTO and obtain the same result.

The TTF transformation functions require to change the data model of the editor. Fortunately, the Model-View-Controller architecture of the Java Swing Framework2 offers this functionality. Programmers can plug-in their own data model into the abstract document model 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 others connected editors through the workspace manager.

The workspace manager send local operations to others sites and handle reception of remote operations. When a remote operation is received and is causally ready, this operation is 3 http://www.eclipse.org/ transformed with concurrent operations using the SOCT2 algorithm and TTF transformation. 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 the the JGroups4 toolkit. This toolkit allow 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 operation executed. The undo panel (see figure 13) contains all operations executed on the local site. The user can select any operations and compensate them by clicking on the button "undo".

The graveyard prototype is available under GPL at http://potiron.loria.fr/projects/graveyard.

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 to undo any operation at anytime. Since the adOPTed algorithm requires transformation function satisfying T P1 and T P2, 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 | Consistency maintenance in real-time collaborative graphics editing systems[END_REF] is associated with the GOTO integration algorithm. This approach introduce three undo properties called IP 1, IP 2 and IP 3. The property IP 3 is similar to the property T PC . 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 P1, T P2 and IP 1.

Unfortunately, transformation functions satisfying these five properties have never been published. TTF functions satisfy T P1 and T P2 but not IP 1 but we still can provide compensation in GOTO. Operations and transformation functions described in this paper can be used in the GOTO integration algorithm to provide an 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.

For example, the transformation of an operation undo(op1) with an operation op2 is defined Figure 15 explains this transformation function. The main idea is to swap the operations op1 and op2 and undo the resulting operation op 1 . Unfortunately, the authors do not discuss the case of causally dependent operations.

In Figure 15, the operation op2 is causally dependent of the operation op1. The result is "Del(-1)" which is incorrect. These operations cannot be swapped. In addition, the inverse transformation of an undo operation cannot be determined without reordering the history buffer. This reordering is costly and depends on the history size. In the compensation approach, even compensating operations are operations and, consequently, the transformation of compensating operations does not have an additional cost.

In the COT approach [START_REF] Sun | Operation Context and Context-based Operational Transformation[END_REF], there is a specific undo mechanism. Undo operation are treated as "do" (i.e. normal) operations since the transformation path for an operation is chosen using "context vectors" that contains information about undone and redone operations. The COT's algorithm enforces the properties T P2, IP 2 and IP 3 using a continuous total order on operations and the "context vectors". Thus, the COT do/undo approach can use transfor-

Figure 1 :

 1 Figure 1: Divergence scenario

Figure 2 :

 2 Figure 2: Compensation of a last executed operation

Figure 3 :

 3 Figure 3: Wrong compensation of a nonlast executed operation

Figure 4 :

 4 Figure 4: Algorithm of the compensation

Figure 5 :

 5 Figure 5: Respect of the compensation effect

Figure 6 :

 6 Figure 6: Model in the TTF approach.

Figure 7 :

 7 Figure 7: TTF transformation functions

Figure 8 :

 8 Figure 8: Compensating the operation Ins.

C

  (op): 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)

Figure 10 :Figure 11 :

 1011 Figure 10: Reverse transformation functions TTF with compensation

1 Figure 12 :

 112 Figure 12: Visibility level

Figure 14 :

 14 Figure 14: Graveyard architecture

9 op 2 =op 1 =TFigure 15 :

 92115 Figure 15: Transformation of an operation undo

  T( Ins(p 1 , c 1 , sid 1 ), Ins(p 2 , c 2 , sid 2 ) ): if (p 1 < p 2 ) return Ins(p 1 , c 1 , sid 1 ) else if (p 1 = p 2 and sid 1 < sid 2 ) return Ins(p 1 , c 1 , sid 1 ) else return Ins(p 1 + 1, c 1 , sid 1 ) end T( Ins(p 1 , c 1 , sid 1 ),Del(p 2 , sid 2 )): return Ins(p 1 , c 1 , sid 1 ) end T( Del(p 1 , sid 1 ), Ins(p 2 , c 2 , sid 2 )): if (p 1 < p 2 ) return Del(p 1 , sid 1 ) else return Del(p 1 + 1, sid 1 ) end T( Del(p 1 , sid 1 ), Del(p 2 , sid 2 )): return Del(p 1 , sid 1 ) end

  T( Ins(p 1 , c 1 , sid 1 ),Undel(p 2 , sid 2 )): return Ins(p 1 , c 1 , sid 1 ) end T( Del(p 1 , sid 1 ), Undel(p 2 , sid 2 )): return Del(p 1 , sid 1 ) end T( Undel(p 1 , sid 1 ), Ins(p 2 , c 2 , sid 2 )): if (p 1 < p 2 ) then return Undel(p 1 , sid 1 ) else return Undel(p 1 + 1, sid 1 ) end T( Undel(p 1 , sid 1 ), Undel(p 2 , sid 2 )): return Undel(p 1 , sid 1 ) end T( Undel(p 1 , sid 1 ), Del(p 2 , sid 2 )): return Undel(p 1 , sid 1 ) end

  T -1 ( Ins(p 1 , c 1 , sid 1 ), Undel(p 2 , sid 2 )):return Ins(p 1 , c 1 , sid 1 ): end T -1 ( Undel(p 1 , sid 1 ), Ins(p 2 , c 2 , sid 2 )): if (p 1 < p 2 ) then return Undel(p 1 , sid 1 ) else return Undel(p 1 -1, sid 1 ) end T -1 ( Del(p 1 , sid 1 ), Undel(p 2 , sid 2 )): return Del(p 1 , c 1 , v 1 , sid 1 ) end T -1 ( Undel(p 1 , sid 1 ), Del(p 2 , sid 2 )): return Undel(p 1 , sid 1 ) end T -1 ( Undel(p 1 , sid 1 ), Undel(p 2 , sid 2 )): return Undel(p 1 , sid 1 ) end

Consistency is not violated by the scenario even if the sites do not share the same state. Indeed, when local compensation operations will be sent and integrated, the sites will finally share the state "abaa /".

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

http://www.jgroups.org RR n°6160

Using TTF functions, COT will no longer requires such a total order. However, don't have the T P2 property to check can be interesting.In future works, we will implement existing integration algorithm in the Graveyard prototype. Thus, we will be able to benchmark all integration algorithms.

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

Compensation in Collaborative Editing mation functions which only satisfy the property T P1 5 . One can use the compensation approach with the COT's integration algorithm. This allows to obtain and undo mechanism with transformation functions only satisfying T P1 but without using "context vectors" which space complexity is higher than "state vectors" usually used in OT approaches.

Finally, in the above approaches, the use of the compensation approach brings several improvements: it improves the performances, extends the undo functionality or even replaces a non-instanciable undo mechanism. The main characteristic of compensation approach is to realize the undo feature at the transformation function level. It makes the undo feature independent of the integration algorithm. So the compensation approach can be used with any integration algorithm. The approach of Vidot [START_REF] Ferrié | Concurrent undo operations in collaborative environments using operational transformation[END_REF] propose the same idea with a generic undo operation. Unfortunately, all cases are not handled with the generic undo operation.

CONCLUSIONS

In all existing OT approaches, undo is designed as a backward error recovery. In this paper, we introduced our compensation mechanism designed as a forward error recovery [START_REF] Abowd | Giving undo attention[END_REF][START_REF] Garcia-Molina | Sagas[END_REF]. The compensation approach is more generic than the undo approach: we can apply compensation to all transformation functions even if some operations have no inverse. 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, GOTO and adOPTed. We have a complete solution to build fully-decentralized text editors with undo capabilities. The compensation approach proposed in this paper has been implemented in the Graveyard collaborative text editor based on the tombstone transformation approach.


Yiqing Yang

Qiang Liu

Songmei Yuan
email: yuansm@buaa.edu.cn

Jokin Munoa
email: jmunoa@ideko.es

Three dimensional chatter stability prediction based on the exponential cutting force model

Keywords: milling, chatter stability, three dimensional, exponential force model

Chatter stability prediction is widely used to avoid chatter which restricts the machining quality and productivity. A lot of works have been done to predict the stability chart fast and accurately. However, most of them are based on the linear force model, and the chatter stability limits is formulated as independent on the feedrate, which does not conform to the reality well. This paper intends to investigate the chatter stability prediction based on the exponential force model, which is linearized by the Taylor equation when calculating the directional coefficients. Meanwhile, the stability model is extended to the three dimensional, which is especially applicable for the ballend mills, bull-nose end mills and inserted cutter where chatter may be brought up in Z direction. Simulation results show that the exponential force model agrees with the measurements as well as the linear force model in the cutting force prediction, and it is able to demonstrate the effect of the feedrate on the stability limit.

INTRODUCTION

Machining chatter causes poor product quality and reduces the industry productivity. A lot of works have been done to predict and avoid it, based on the chatter stability prediction. One of the most common methods is zero-order solution [Altintas, 2000]. It is fast and high accuracy except for some cases like highly interrupted milling [START_REF] Altintas | Chatter stability of milling in frequency and discrete time domain[END_REF]. Later, G. Stepan improved the stability simulation accuracy of these cases by proposing the semi-discretization method [START_REF] Insperger | Semi-discretization method for delayed systems[END_REF]][Dombovari et al, 2012].

So far, most of the chatter stability prediction works are based on a linear cutting force model, where the cutting coefficients are treated as constants. One problem related with the linear cutting force model is that the stability lobes are independent on the feedrate. However, chatter occurrence is found to be related with the feedrate in reality [START_REF] Faassen | Prediction of regenerative chatter by modeling and analysis of high-speed milling[END_REF]. Other available cutting force models have been investigated in the literature [START_REF] Faassen | Prediction of regenerative chatter by modeling and analysis of high-speed milling[END_REF]] and [Budak, 2006], and exponential force model is the major one. Therefore, it is employed to calculate the stability lobes in this paper.

Munoa investigated the chatter stability prediction of face milling based on the exponential force model with an application to the single degree of freedom system [START_REF] Munoa | Stability study of the milling process using an exponential force model in frequency domain[END_REF]. However, chatter may be brought up by the modes in the Z direction when using ball-end mills, bull-nose end mills and inserted cutters. Altintas has proposed a three dimensional model to calculate the stability based on the linear force model [Altintas, 2001], considering the X/Y/Z machine tool compliance. Campa applied a three-dimensional dynamic model to calculate the stability lobes of low rigidity parts with a corner radius tool [START_REF] Campa | Selection of cutting conditions for a stable milling of flexible parts with bull-nose end mills[END_REF]. Based on their work, the three dimensional stability is extended to the exponential force model.

This paper is organized as follows: basic chatter theory is introduced first, and the chatter stability prediction based on the exponential force model is formulated. The simulation results are compared with the linear force model and classic 2D chatter stability model. The results are concluded in the end.

BASIC THEORY OF THREE DIMENSIONAL CHATTER.

Regenerative chatter is the most common type of chatter, as a result of the previous and current vibration waves printed on the workpiece caused by the machine tool flexibility. A detailed explanation can be found in the literature [Altintas, 2000].

    ) ( sin ) sin( ) ( 0 , j j j j j g c h            
c is the preset feedrate,  j,0 ,  j is the previous and current vibration waves of cutter. g( j ) is a step function determining whether the tool is in or out cut.

The first term c sin( j ) sinκ is a static component and does not contribute to the chatter, therefore it is neglected. The dynamic chip thickness can be written as

    ) ( cos sin ) cos( ) sin( ) ( j j j j d g z y x h               (1)
where, △x=x(t)-x(t-T), △y=y(t)-y(t-T) , △z=z(t)-z(t-T). T is the tooth passing period. By projecting the cutting force into the Cartesian coordinate system, the X/Y/Z components are obtained as,

                                     a t r z y x dF dF dF dF dF dF            sin 0 cos cos cos sin cos sin sin cos cos sin sin (2)
The total cutting force can be calculated by summing the force components acting on each tooth.

CHATTER STABILITY PREDICTION BASED ON THE EXPONENTIAL FORCE MODEL

The cutting coefficients are expressed as an exponential function of the chip thickness h for the exponential force model. Such as,

                   r r ac p r tc q r rc ae re te h K K h K K h K K K K K 0
Then, the cutting force can be expressed as

                          r a p q r t a t r h K h h K a K F F F 1 1 1
Where, p, q, r are the index number of chip thickness in the tangential, radial and axial direction. The exponential function can be formulated in a variety of equivalent ways Particularly, it can be defined by the power series according to the Taylor equation. Let h=h e +h d . h e is the stationary solution, and h d is the dynamic component. Then h 1-p =(h e +h d ) 1-p =h e 1-p +(1-p)h e -p h d +O(h e ) Neglecting the stationary component h e 1-p and higher order polynomials O(h e ) for the simplification of calculation, the cutting force acting on tooth j in the radial, tangential and axial direction is,

  ) ( cos sin cos sin sin 1 ) 1 ( ) 1 ( ) 1 ( j a r r d p d q d T a t r g z y x x K K h r h p h q aK F F F                                                          (3)
Combining Eq.( 2) -Eq.( 3), it can be obtained as,

                          z y x A aK F F F T z y x (4)
[A] is the directional coefficient factor matrix, which is a periodical function of tooth passing period. By using the Zero-order solution, the average term of [A] is kept, and Eq.( 4) can be rewritten as

     ) ( 2 ) ( t aK N t F T     (5)
Therefore, the elements in [α] are all constants which are relied on the entry and exit angles. They are formulated as follows, After obtaining the directional factor, the formulation to calculate the eigenvalues and stability lobes are straightforward and can be referenced with bibliography [Altintas, 2001]. 4. STABILITY LOBES.

                                                                                                                  ex st ex st ex st ex st ex st ex st ex st ex st ex st q r r a E q r r a E q r r a E p q r r a E p q r r a E p q r r a E p q r r a E p q r r a E p q r r a E c K q c K r c K q c K r c K q c K r c p c K q c K r c p c K q c K r c p c K q c K r c p c K q c K r c p c K q c K r c p c K q c K r                                                                                                                                                                                                                                  sin sin

Dynamic Chip Thickness:

Cutting tests are performed on a three axial milling machine by machining Aluminium to identify the cutting coefficients (Fig. 2). The tool diameter is 12mm, and the teeth number is 2. The immersion angle κ = π/4. The cutting force is measured by Kistler 9257B. Cutting coefficients based on the linear and exponential cutting force models are both identified. See Table 1. 0.3323 mm q-p q 0.4637 --K a 0.0560 mm r-p r 0.4882 --

Fig. 2: Tests for the cutting coefficients identification

The cutting force under a series of cutting conditions are predicted and compared with the experiment measurements after identifying the cutting coefficients (Fig. 3). It can be seen that both the force models fits the experiments well and are capable of modelling the milling process. Next, three dimensional chatter stability is predicted. Firstly, the two dimensional and three dimensional chatter stability models are compared based on the exponential force model. It can be seen that the three dimensional model reaches higher stability limit after introducing the mode in Z direction (Fig. 4). Specially when κ= π/2, the Z component in Eq.( 1) is null, and the proposed three dimensional chatter stability model can be reduced to the two dimensional case.

Next, the feedrate effect on the stability is able to be demonstrated on the exponential force model. After implementing more simulations with different feedrate per tooth c in Eq.( 6) (i.e. c=0.1, 0.2, 0.3), it is found that the minimum stability increases slightly as the feedrate increases. Besides, the three dimensional stability model based on the exponential force model is compared with the linear force model proposed by [Altintas, 2001]. In this case, the acquired stability lobes of linear force model are closer with the exponential force model using higher feedrate c (Fig. 5).

CONCLUSIONS

The chatter stability based on the exponential force model is proposed while the flexibility in X/Y/Z direction is considered. Simulation results show that the exponential force model can predict the cutting force as well as the linear force model, and it is able to predict the stability considering the effect of feedrate. Further experiments will be conducted to verify the three dimensional chatter stability based on the exponential force model. And the effect of neglecting the higher harmonics during the linearizing process of the exponential force model will be investigated.

Fig. 1 :

 1 Fig. 1: Dynamic model of the cutting tool.

Fig. 1

 1 Fig.1 illustrates a bull-nose end mill. The machine tool vibrates during the machining because of the flexibility of the structure, which cause the fluctuation of the chip thickness h. As the existence of the lead angle κ, h is affected by the vibration in Z direction. The chip thickness can be expressed as

Fig. 3 :

 3 Fig. 3: Cutting force comparison: measurement (solid line), exponential force model (dashed), linear force model (dashdot). Slot milling. Tool diameter D=12mm, teeth number N=2, κ= π/4. (a) n=4000rpm, F=800mm/min, a p =1mm; (b) n=4000rpm, F=1200mm/min, a p =1.5mm

Fig. 4 :

 4 Fig. 4: Comparison of two dimensional and three dimensional chatter stability based on the exponential force model. Half immersion, up milling. Tool diameter D=12mm, N=2, κ= π/4.

Fig. 5 :

 5 Fig. 5: Chatter stability comparison between three dimensional exponential (different feedrate) and linear force model. Half immersion, up milling. Tool diameter D=12mm, N=2, κ=π/4.

Table 1

 1 Identified cutting coefficients for the linear and exponential force model

	Linear force model
	K tc	812.6	N/mm 2	K te	15.91	N/mm
	K rc	0.4177	--	K re	21.04	N/mm
	K ac	0.1194	--	K ae	2.74	N/mm
	Exponential force model
	K t	581.6	N/mm 2-p	p	0.2278	--
	K r

ACKNOWLEDGEMENTS

This work is sponsored by the Significant Science and Technology Special Program of Machine tools (2010ZX04014-052, 2010ZX04014-017, 2011ZX04016-021) and the Fundamental Research Funds for the Central Universities (YWF-11-03-H-017).