Il y a quelque chose que je suis pas sûr de comprendre avec les points de linéarisation fixés. Le problème quand les points sont fixés est qu'il faut aussi deviner la valeur de retour et on dit dans le papier qu'on suppose qu'on connaît cette valeur de retour. Comment faire pour cet exemple ?

La spécification est S = a1 b*

Dans l'implémentation, il y a deux méthodes :

a : la première transition de a est "x == 0? x := 1" (ce qui permet à b de s'exécuter)
ensuite il y a un branchement, la première branche va vers v1 (valeur de retour 1, a1)
la seconde branche va vers v2, mais avec une condition qui n'est pas satisfaite

b : sa seule transition est "x == 1?"

J'ai l'impression que dire qu'on peut deviner les valeurs de retour quand on veut mettre les points de linéarisation est similaire à dire que les méthodes n'ont pas de valeur de retour et qu'on les sépare en plusieurs méthodes (par exemple on divise "a" en a1 et a2). Pour cet exemple, la librairie est linéarisable avec des points de linéarisation fixés (sur la première transition de chaque méthode), mais la librairie {a1,a2,b} ne l'est pas.

----------------------------------------------

Quand tu fais la transformation tu vas redéfinir les points de linearisation. Les points de linearisation de a, b sont pas nécessairement les mêmes avec celles de a1,a2,et b: a1 a le même point de linearisation que a, et a2 a comme point de linearisation qq chose après cette condition qui n'est pas satisfaite. Avec ces points, la librairie est linearisable, n'est-ce pas ?

----------------------------------------------

non je crois qu'elle n'est pas linéarisable même si les points ne sont pas fixés (trace: call(a2) call(b) ret(b))

----------------------------------------------

Je me rappelle que à un certain moment les points de linearisations dépendaient aussi de la valeur de retour. C'est-à-dire, pour chaque methode M, il y avait une fonction
L: Valueurs de retours -> Actions de M. Je me rappelle plus pourquoi on l'a enlevé. Dans ce contexte, ta librairie initiale n'est pas static linearisable parce qu'il y aura un chemin avec deux points de linearisations.

En fait dans ce cas, t'as besoin de points de linearisation conditionnelles (qui dépendent de la valeur de retour) et la bonne réduction vers les points de linearisation fixes serait d'enlever la méthode a2.

Mais, je pense que ta observation est bonne....si on veut faire des points de linearisation conditionnelles sans transformer la librairie on a besoin de plusieurs lineariseurs.

----------------------------------------------

Quand la valeur de retour est 2, le point de linéarisation n'a pas besoin d'être sur la première transition (il peut être sur la deuxième transition de la deuxième branche)

Je crois pas qu'on ait le droit d'enlever a2 car la condition non satisfaite de a2 pourrait être satisfaite plus tard dans la trace et a2 pourrait être accepté par la spécification

Par exemple, si la spécification est (les préfixes de) S = a1 b a2*
La transition de "b" est "x == 1? x := 2"
La première transition de "a" est toujours "x == 0? x := 1"
La première branche de "a" est : "x == 2 ? x := 3"
La seconde branche de "a" est : "x == 3?"

En gros "a2" ne peut s'exécuter seulement si "a1" et "b" se sont exécutés. Pour cet exemple, la librairie {a,b} a des les points de linéarisation fixés (dans "a" : pour la valeur de retour 1, première transition, et pour la valeur de retour 2, seconde transition ; ou alors pour les deux valeurs de retour sur la première transition) mais la librairie {a1,a2,b} n'est pas linéarisable même quand les points de sont pas fixés (toujours la trace call a2 call b ret b)

----------------------------------------------

Oui, mais le chemin qui contient cette 2-eme branche contient deux points de linearisation: le point pour a1 est ce point pour a2.

Ici, pareil, tu aura un chemin avec deux points (le meme points de linearisation pour deux valeurs de retour je le considere comme deux points de linearisations distinctes parce que je regarde le nombre de points dans l'image de la fonction L: Valueurs de retours -> Actions de M)

----------------------------------------------

Ah ok je comprends mieux