Traces (P||Q)

[save_jeff]

Hi,

Ich bin unsicher was folgender Begriff für traces induziert:

P = ((x->STOP) || (y->STOP))

Meine Antwort wäre:
traces(P) = {(), (x), (y)}
- Da nach Definition alle t erlaubt sind mit: (t projiziert auf das Alphabet) Element von Prozesse P und Q.
-> t = (x) t projiziert auf Alphabet von Q ist () -> das ist Element von Q
-> t = (y) analog

das Schachbrett Beispiel und ein paar andere Aufgaben die ich gesehen suggerieren aber dass nur traces erlaubt sind die in sowohl P als auch Q liegen
traces(P) = {()}

Sonst würde das RULE beim Schachbrett kein Sinn machen, da zwar BRETT und RULE synchronisieren aber nicht (nach RULE) unerlaubte Bewegungen aus dem Trace löscht


Auch Lösung 13.5b) suggeriert dass traces(P||Q) = { t | t element traces(P) und t element traces(Q)}

[Markus Tasch]

Abhängig davon wie der Index bei den beiden \(STOP\) aussieht ist das Ergebnis unterschiedlich:

Für den Beispiel gilt, wenn \(STOP_{\{x\}}\) und \(STOP_{\{y\}}\):

\(traces(P) = \{(), (x), (y), (x,y), (y,x)\}\)


Für den Beispiel gilt, wenn \(STOP_{\{x,y\}}\) und \(STOP_{\{x,y\}}\):
\(traces(P) = \{()\}\)




EDIT: Im zweiten Beispiel war die Menge leider falsch.

[save_jeff]

Also wenn

alpha(P) nicht disjunkt alpha(Q) -> traces(P || Q) = nur traces die in traces(Q) und traces(P)
alpha(P) disjunkt alpha(Q) -> alle nebenläufigen prozesse mit syncronisierung bei gleichen ereignissen

[Markus Tasch]

Die Erklärung wirkt irgendwie falsch:

Also:
Angenommen \(\alpha(P)\cap \alpha(Q)=\emptyset\), dann entspricht \(traces(P || Q)\) allen Interleavings der Spuren von \(P\) und \(Q\). Synchronization tritt keine auf, da keine Ereignisse geteilt sind.

Angenommen \(\neg \alpha(P)\cap \alpha(Q)=\emptyset\), dann entspricht \(traces(P || Q)\) allen Spuren, die projiziert nach \(\alpha(P)\) eine Spur von \(P\) sind und gleichzeitig projoziert nach \(\alpha(Q)\) eine Spur von \(Q\) sind.

[save_jeff]

okay danke ;]