Traces (P||Q)

save_jeff
Neuling
Neuling
Beiträge: 8
Registriert: 24. Nov 2016 10:50

Traces (P||Q)

Beitrag von save_jeff » 7. Mär 2017 16:54

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
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 124
Registriert: 11. Sep 2015 10:57

Re: Traces (P||Q)

Beitrag von Markus Tasch » 7. Mär 2017 17:47

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.
Markus Tasch, M.Sc.
Modeling and Analysis of Information Systems
Department of Computer Science, TU Darmstadt
http://www.mais.informatik.tu-darmstadt.de

save_jeff
Neuling
Neuling
Beiträge: 8
Registriert: 24. Nov 2016 10:50

Re: Traces (P||Q)

Beitrag von save_jeff » 7. Mär 2017 17:57

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
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 124
Registriert: 11. Sep 2015 10:57

Re: Traces (P||Q)

Beitrag von Markus Tasch » 7. Mär 2017 19:53

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.
Markus Tasch, M.Sc.
Modeling and Analysis of Information Systems
Department of Computer Science, TU Darmstadt
http://www.mais.informatik.tu-darmstadt.de

save_jeff
Neuling
Neuling
Beiträge: 8
Registriert: 24. Nov 2016 10:50

Re: Traces (P||Q)

Beitrag von save_jeff » 8. Mär 2017 07:52

okay danke ;]

Antworten

Zurück zu „Archiv“