Seite 1 von 1

Traces (P||Q)

Verfasst: 7. Mär 2017 16:54
von 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)}

Re: Traces (P||Q)

Verfasst: 7. Mär 2017 17:47
von 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.

Re: Traces (P||Q)

Verfasst: 7. Mär 2017 17:57
von 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

Re: Traces (P||Q)

Verfasst: 7. Mär 2017 19:53
von 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.

Re: Traces (P||Q)

Verfasst: 8. Mär 2017 07:52
von save_jeff
okay danke ;]