Wie unterscheidet dieser FSP beide USER-Pfade?

Question

RESOURCE = (acquire->continue->RESOURCE). 
USER = (acquire->use->continue->USER). 
||RESOURCE_SHARE = (a:USER || b:USER || {a,b}::RESOURCE). 

Wie funktioniert die gemeinsame Aktion continue zwischen a.USER und a.RESOURCE sicherzustellen, dass der a.USER Pfad nicht mit dem b.USER Pfad nicht verflechten? Zum Beispiel erlaube ich der LTSA die folgende Spur nicht, und ich verstehe nicht warum nicht.

a.acquire->b.acquire->a.use->b.use->... 

Diese Verwirrung folgt aus dem Vergleich mit der folgenden FSP/LTSA. Entfernen Sie die continue Aktion in beiden Prozessen und wir sind links mit:

RESOURCE = (acquire->RESOURCE). 
USER = (acquire->use->USER). 
||RESOURCE_SHARE = (a:USER || b:USER || {a,b}::RESOURCE). 

Diese FSP/LTSA DOES plötzlich für die USER Pfade erlauben verflochtenen zu werden, da wir die folgende Spur durchführen können:

Anscheinend hinzufügen fortfahren zwingt die USER Pfade getrennte Wege zu gehen. Warum allerdings?

Quelle: Die erste FSP stammt aus dem Buch "Concurrency" von Jeff Magee und Jeff Kramer.

Answer 1

Ich schickte eine Mail an meinen Lehrer, um mir zu helfen. Ich werde ihn paraphrasieren:

Es gibt drei Prozesse, zwei Präfixe a und b der USER und {a, b} :: RESOURCE. Die Aktion "acquire" von a.USER und b.USER führt mit {a, b} .acquire aus {a, b} :: RESOURCE zusammen. Dies geschieht auch für {a, b} .fortsetzen.

Daher sind im ersten Zustand zwei mögliche Spuren aktiviert: a.acquire OR b.acquire. Angenommen, die Aktion a.acquire wird gewählt. Ein Übergang tritt auf und a.USER wird nur die Aktion a.use aktiviert haben, während {a, b} :: RESOURCE zwei Optionen aktiviert hat: {a, b} .continue.

Da a.continue in a.USER noch nicht aktiviert ist, kann a.continue in {a, b} :: RESOURCE nicht auftreten. Die einzige verbleibende Aktion besteht darin, dass eine Aktion auftritt. In der Zwischenzeit befindet sich b.USER in der noch im ersten Zustand und kann b.acquire nicht ausführen, da {a, b} :: RESOURCE nur {a, b} .continue aktiviert ist.

Nach dem a.use-Übergang ist a.USER nun für die gemeinsame Aktion a.continue bereit. Sobald dies geschieht, sind alle drei Prozesse zurück in den Anfangszustand .