Algebraic Specification Of Pt Nets
-
Upload
helko-glathe -
Category
Technology
-
view
342 -
download
2
Transcript of Algebraic Specification Of Pt Nets
SignaturAlgebren
ErweiterterungEnde
P/T-Netze algebraisch spezifiziert
Alexander Rein, Helko Glathe
01.11.2006
Alexander Rein, Helko Glathe P/T-Netze algebraisch spezifiziert
SignaturAlgebren
ErweiterterungEnde
Inhaltsverzeichnis
1 Signatur
2 AlgebrenAlgebra PT1Algebra PT2Homomorphismus Algebra PT1 → Algebra PT2Algebra PT3Homomorphismus Algebra PT1 → Algebra PT3
3 ErweiterterungErweiterte SignaturAlgebra zur erweiterten Signatur
Alexander Rein, Helko Glathe P/T-Netze algebraisch spezifiziert
SignaturAlgebren
ErweiterterungEnde
Unsere Signatur fur ein Petrinetz
Σ-P/T Netz:
sorts: natStelleTransitionKanteVorKanteNach
opns: getKapazitat: Stelle → natgetGewichtVor: KanteVor → natgetGewichtNach: KanteNach → natgetToken: Stelle → nattargetVor: KanteVor → TransitiontargetNach: KanteNach → StellesourceVor: KanteVor → StellesourceNach: KanteNach → Transition
Alexander Rein, Helko Glathe P/T-Netze algebraisch spezifiziert
SignaturAlgebren
ErweiterterungEnde
Alg PT1Alg PT2Homo Alg PT1→ Alg PT2Alg PT3Homo Alg PT1→ Alg PT3
Petrinetz zur gesuchten Algebra PT1
s1 k=2
s2 k=1 s3 k=1
t1
t2 t3
e1 w=2
f1 f2e3
f4
e2
f3
Alexander Rein, Helko Glathe P/T-Netze algebraisch spezifiziert
SignaturAlgebren
ErweiterterungEnde
Alg PT1Alg PT2Homo Alg PT1→ Alg PT2Alg PT3Homo Alg PT1→ Alg PT3
Sorten
PT1nat = NPT1Stelle = {s1,s2,s3}PT1Transition = {t1,t2,t3}PT1KanteVor = {e1,e2,e3}PT1KanteNach = {f1,f2,f3,f4}
Alexander Rein, Helko Glathe P/T-Netze algebraisch spezifiziert
SignaturAlgebren
ErweiterterungEnde
Alg PT1Alg PT2Homo Alg PT1→ Alg PT2Alg PT3Homo Alg PT1→ Alg PT3
Operationen
getKapazitatPT1(x) =
(2, | x=s1
1, | sonst
getGewichtVorPT1(x) =
(2, | x=e1
1, | sonst
getGewichtNachPT1(x) = 1
getTokenPT1(x) =
(2, | x=s1
0, | sonst
Alexander Rein, Helko Glathe P/T-Netze algebraisch spezifiziert
SignaturAlgebren
ErweiterterungEnde
Alg PT1Alg PT2Homo Alg PT1→ Alg PT2Alg PT3Homo Alg PT1→ Alg PT3
Operationen
targetVorPT1(x) =
8><>:t1, | x=e1
t2, | x=e2
t3, | x=e3
targetNachPT1(x) =
8><>:s2, | x=f1
s3, | x=f2
s1, | sonst
sourceVorPT1(x) =
8><>:s1, | x=e1
s2, | x=e2
s3, | x=e3
sourceNachPT1(x) =
8>>><>>>:t1, | x=f1
t1, | x=f2
t2, | x=f3
t3, | x=f4
Alexander Rein, Helko Glathe P/T-Netze algebraisch spezifiziert
SignaturAlgebren
ErweiterterungEnde
Alg PT1Alg PT2Homo Alg PT1→ Alg PT2Alg PT3Homo Alg PT1→ Alg PT3
Petrinetz zur gesuchten Algebra PT2
g1 k=4
g2 k=2 g3 k=2
u1
u2 u3
h1 w=4
i1 w=2 i2 w=2h3 w=2
i4 w=2
h2 w=2
i3 w=2
g4 k=1u5 u6
u4
h6 h7
i5
h5h4
i6 i7
Alexander Rein, Helko Glathe P/T-Netze algebraisch spezifiziert
SignaturAlgebren
ErweiterterungEnde
Alg PT1Alg PT2Homo Alg PT1→ Alg PT2Alg PT3Homo Alg PT1→ Alg PT3
Sorten
PT2nat = NPT2Stelle = {g1,g2,g3,g4}PT2Transition = {u1,u2,u3,u4,u5,u6}PT2KanteVor = {h1,h2,h3,h4,h5,h6,h7}PT2KanteNach = {i1,i2,i3,i4,i5,i6,i7}
Alexander Rein, Helko Glathe P/T-Netze algebraisch spezifiziert
SignaturAlgebren
ErweiterterungEnde
Alg PT1Alg PT2Homo Alg PT1→ Alg PT2Alg PT3Homo Alg PT1→ Alg PT3
Operationen
getKapazitatPT2(x) =
8><>:4, | x=g1
2, | (x=g2)∨(x=g3)
1, | sonst
getGewichtVorPT2(x) =
8><>:4, | x=h1
2, | (x=h2)∨(x=h3)
1, | sonst
getGewichtNachPT2(x) =
(2, | (x=i1)∨(x=i2)∨(x=i3)∨(x=i4)
1, | sonst
getTokenPT2(x) =
(4, | x=g1
0, | sonst
Alexander Rein, Helko Glathe P/T-Netze algebraisch spezifiziert
SignaturAlgebren
ErweiterterungEnde
Alg PT1Alg PT2Homo Alg PT1→ Alg PT2Alg PT3Homo Alg PT1→ Alg PT3
Operationen
targetVorPT2(x) =
8>>>>>>>>>><>>>>>>>>>>:
u1, | x=h1
u2, | x=h2
u3, | x=h3
u4, | x=h4
u4, | x=h5
u5, | x=h6
u6, | x=h7
targetNachPT2(x) =
8>>>>>>>>>><>>>>>>>>>>:
g2, | x=i1
g3, | x=i2
g1, | x=i3
g1, | x=i4
g4, | x=i5
g2, | x=i6
g3, | x=i7
Alexander Rein, Helko Glathe P/T-Netze algebraisch spezifiziert
SignaturAlgebren
ErweiterterungEnde
Alg PT1Alg PT2Homo Alg PT1→ Alg PT2Alg PT3Homo Alg PT1→ Alg PT3
Operationen
sourceVorPT2(x) =
8>>>>>>>>>><>>>>>>>>>>:
g1, | x=h1
g2, | x=h2
g3, | x=h3
g2, | x=h4
g3, | x=h5
g4, | x=h6
g4, | x=h7
sourceNachPT2(x) =
8>>>>>>>>>><>>>>>>>>>>:
u1, | x=i1
u1, | x=i2
u2, | x=i3
u3, | x=i4
u4, | x=i5
u5, | x=i6
u6, | x=i7
Alexander Rein, Helko Glathe P/T-Netze algebraisch spezifiziert
SignaturAlgebren
ErweiterterungEnde
Alg PT1Alg PT2Homo Alg PT1→ Alg PT2Alg PT3Homo Alg PT1→ Alg PT3
Allgemein
Definition
Homomorphismus h: PT1 → PT2h=(hs:PT1s → PT2s)sεS mit hs(fPT1(x))=fPT2(hs(x))Definition ist vereinfacht und gilt nur fur einelementige Operationen!
Alexander Rein, Helko Glathe P/T-Netze algebraisch spezifiziert
SignaturAlgebren
ErweiterterungEnde
Alg PT1Alg PT2Homo Alg PT1→ Alg PT2Alg PT3Homo Alg PT1→ Alg PT3
Suche nach Homomorphismus Algebra PT1 → Algebra PT2
g1 k=4
g2 k=2 g3 k=2
u1
u2 u3
h1 w=4
i1 w=2 i2 w=2h3 w=2
i4 w=2
h2 w=2
i3 w=2
g4 k=1u5 u6
u4
h6 h7
i5
h5h4
i6 i7
s1 k=2
s2 k=1 s3 k=1
t1
t2 t3
e1 w=2
f1 f2e3
f4
e2
f3
Alexander Rein, Helko Glathe P/T-Netze algebraisch spezifiziert
SignaturAlgebren
ErweiterterungEnde
Alg PT1Alg PT2Homo Alg PT1→ Alg PT2Alg PT3Homo Alg PT1→ Alg PT3
Konkret
hnat(x) = x∗2
hStelle(x) =
8><>:g1, | x=s1
g2, | x=s2
g3, | x=s3
hTransition(x) =
8><>:u1, | x=t1
u2, | x=t2
u3, | x=t3
hKanteVor(x) =
8><>:h1, | x=e1
h2, | x=e2
h3, | x=e3
hKanteNach(x) =
8>>><>>>:i1, | x=f1
i2, | x=f2
i3, | x=f3
i4, | x=f4
Alexander Rein, Helko Glathe P/T-Netze algebraisch spezifiziert
SignaturAlgebren
ErweiterterungEnde
Alg PT1Alg PT2Homo Alg PT1→ Alg PT2Alg PT3Homo Alg PT1→ Alg PT3
Beweisansatz von h
Beweis.
sourceVor: KanteVor → StellehStelle(sourceVorPT1(x)) = sourceVorPT2(hKanteVor(x)) , x ε KanteVorPT1
x sourceVorPT1(x) hStelle(sourceVorPT1(x)) sourceVorPT2(hKanteVor(x)) hKanteVor(x) x
e1 s1 g1 = g1 h1 e1e2 s2 g2 = g2 h2 e2e3 s3 g3 = g3 h3 e3
Analog fur sourceNach, targetVor, targetNach!
hnat(getKapazitatPT1(x)) = getKapazitatPT2(hStelle(x)) , x ε StellePT1
x getKapazitatPT1(x) hnat(getKapazitatPT1(x)) getKapazitatPT2(hStelle(x)) hStelle(x) x
s1 2 4 = 4 g1 s1sonst 1 2 = 2 g2 ∨ g3 sonst
Analog fur getGewichtVor, getGewichtNach und getToken!
Homomorphismus ist injektiv, aber nicht surjektiv!
Alexander Rein, Helko Glathe P/T-Netze algebraisch spezifiziert
SignaturAlgebren
ErweiterterungEnde
Alg PT1Alg PT2Homo Alg PT1→ Alg PT2Alg PT3Homo Alg PT1→ Alg PT3
Petrinetz zur gesuchten Algebra PT3
g1 k=2
g2 k=1
u1
u2
h1 w=2
i1h2
i2
Alexander Rein, Helko Glathe P/T-Netze algebraisch spezifiziert
SignaturAlgebren
ErweiterterungEnde
Alg PT1Alg PT2Homo Alg PT1→ Alg PT2Alg PT3Homo Alg PT1→ Alg PT3
Sorten
PT3nat = NPT3Stelle = {g1,g2}PT3Transition = {u1,u2}PT3KanteVor = {h1,h2}PT3KanteNach = {i1,i2}
Alexander Rein, Helko Glathe P/T-Netze algebraisch spezifiziert
SignaturAlgebren
ErweiterterungEnde
Alg PT1Alg PT2Homo Alg PT1→ Alg PT2Alg PT3Homo Alg PT1→ Alg PT3
Operationen
getKapazitatPT3(x) =
(2, | x=g1
1, | x=g2
getGewichtVorPT3(x) =
(2, | x=h1
1, | x=h2
getGewichtNachPT3(x) = 1
getTokenPT3(x) =
(2, | x=g1
0, | sonst
Alexander Rein, Helko Glathe P/T-Netze algebraisch spezifiziert
SignaturAlgebren
ErweiterterungEnde
Alg PT1Alg PT2Homo Alg PT1→ Alg PT2Alg PT3Homo Alg PT1→ Alg PT3
Operationen
targetVorPT3(x) =
(u1, | x=h1
u2, | x=h2
targetNachPT3(x) =
(g2, | x=i1
g1, | x=i2
sourceVorPT3(x) =
(g1, | x=h1
g2, | x=h2
sourceNachPT3(x) =
(u1, | x=i1
u2, | x=i2
Alexander Rein, Helko Glathe P/T-Netze algebraisch spezifiziert
SignaturAlgebren
ErweiterterungEnde
Alg PT1Alg PT2Homo Alg PT1→ Alg PT2Alg PT3Homo Alg PT1→ Alg PT3
Suche nach Homomorphismus Algebra PT1 → Algebra PT3
g1 k=2
g2 k=1
u1
u2
h1 w=2
i1h2
i2
s1 k=2
s2 k=1 s3 k=1
t1
t2 t3
e1 w=2
f1 f2e3
f4
e2
f3
Alexander Rein, Helko Glathe P/T-Netze algebraisch spezifiziert
SignaturAlgebren
ErweiterterungEnde
Alg PT1Alg PT2Homo Alg PT1→ Alg PT2Alg PT3Homo Alg PT1→ Alg PT3
Konkret
hnat(x) = x
hStelle(x) =
(g1, | x=s1
g2, | sonst
hTransition(x) =
(u1, | x=t1
u2, | sonst
hKanteVor(x) =
(h1, | x=e1
h2, | sonst
hKanteNach(x) =
(i1, | (x=f1)∨(x=f2)
i2, | sonst
Alexander Rein, Helko Glathe P/T-Netze algebraisch spezifiziert
SignaturAlgebren
ErweiterterungEnde
Alg PT1Alg PT2Homo Alg PT1→ Alg PT2Alg PT3Homo Alg PT1→ Alg PT3
Beweisansatz von h
Beweis.
sourceVor: KanteVor → StellehStelle(sourceVorPT1(x)) = sourceVorPT3(hKanteVor(x)) , x ε KanteVorPT1
x sourceVorPT1(x) hStelle(sourceVorPT1(x)) sourceVorPT3(hKanteVor(x)) hKanteVor(x) x
e1 s1 g1 = g1 h1 e1e2 s2 g2 = g2 h2 e2e3 s3 g2 = g2 h2 e3
Analog fur sourceNach, targetVor, targetNach!
hnat(getKapazitatPT1(x)) = getKapazitatPT3(hStelle(x)) , x ε StellePT1
x getKapazitatPT1(x) hnat(getKapazitatPT1(x)) getKapazitatPT3(hStelle(x)) hStelle(x) x
s1 2 2 = 2 g1 s1sonst 1 1 = 1 g2 sonst
Analog fur getGewichtVor, getGewichtNach und getToken!
Homomorphismus ist surjektiv aber nicht injektiv! Jedoch bewahrt dieserHomomorphismus NICHT das Schaltverhalten!
Alexander Rein, Helko Glathe P/T-Netze algebraisch spezifiziert
SignaturAlgebren
ErweiterterungEnde
Erw. SignaturErw. Alg
Suche nach einer Signatur, die auch das Schalten ermoglicht
Σ-P/T Netz Enhanced:
sorts: natStelleTransitionKanteVorKanteNachMarkierung
opns: getKapazitat: Stelle → natgetGewichtVor: KanteVor → natgetGewichtNach: KanteNach → natgetToken: Stelle Markierung → nattargetVor: KanteVor → TransitiontargetNach: KanteNach → StellesourceVor: KanteVor → StellesourceNach: KanteNach → Transitionschalte: Transition Markierung → MarkierunginiMarkierung: → Markierung
Alexander Rein, Helko Glathe P/T-Netze algebraisch spezifiziert
SignaturAlgebren
ErweiterterungEnde
Erw. SignaturErw. Alg
Petrinetz zur gesuchten Algebra PT1Enhanced
1 k=2
2 k=1 3 k=1
t1
t2 t3
e1 w=2
f1 f2e3
f4
e2
f3
Alexander Rein, Helko Glathe P/T-Netze algebraisch spezifiziert
SignaturAlgebren
ErweiterterungEnde
Erw. SignaturErw. Alg
Sorten
PT1Enhancednat = NPT1EnhancedStelle = {1,2,3} ⊆ NPT1EnhancedTransition = {t1,t2,t3}PT1EnhancedKanteVor = {e1,e2,e3}PT1EnhancedKanteNach = {f1,f2,f3,f4}PT1EnhancedMarkierung = (N ◦ N ◦ N) Wort der Lange 3!
Alexander Rein, Helko Glathe P/T-Netze algebraisch spezifiziert
SignaturAlgebren
ErweiterterungEnde
Erw. SignaturErw. Alg
Operationen
getKapazitatPT1Enhanced(x) =
(2, | x=s1
1, | sonst
getGewichtVorPT1Enhanced(x) =
(2, | x=e1
1, | sonst
getGewichtNachPT1Enhanced(x) = 1
getTokenPT1Enhanced(s,m) = ms (Buchstabe s des Wortes m)
Alexander Rein, Helko Glathe P/T-Netze algebraisch spezifiziert
SignaturAlgebren
ErweiterterungEnde
Erw. SignaturErw. Alg
Operationen
targetVorPT1Enhanced(x) =
8><>:t1, | x=e1
t2, | x=e2
t3, | x=e3
targetNachPT1Enhanced(x) =
8><>:s2, | x=f1
s3, | x=f2
s1, | sonst
sourceVorPT1Enhanced(x) =
8><>:s1, | x=e1
s2, | x=e2
s3, | x=e3
sourceNachPT1Enhanced(x) =
8>>><>>>:t1, | x=f1
t1, | x=f2
t2, | x=f3
t3, | x=f4
Alexander Rein, Helko Glathe P/T-Netze algebraisch spezifiziert
SignaturAlgebren
ErweiterterungEnde
Erw. SignaturErw. Alg
Operationen
iniMarkierungPT1Enhanced = 200
schaltePT1Enhanced(t,m) =
8>>>>>>>>>>>>>>>>><>>>>>>>>>>>>>>>>>:
(m1 − 2, m2 + 1, m3 + 1), | (t = t1) ∧ (m1 = 2)∧| (m2 = 0) ∧ (m3 = 0)
(m1 + 1, m2 − 1, m3), | (t = t2) ∧ (m2 = 1)∧| (m1 < 2)
(m1 + 1, m2, m3 − 1), | (t = t3) ∧ (m3 = 1)∧| (m1 < 2)
m, | sonst
Anmerkung: Man kann evtl. nicht feststellen, ob t geschaltet hat oder nicht!
Alexander Rein, Helko Glathe P/T-Netze algebraisch spezifiziert
SignaturAlgebren
ErweiterterungEnde
Wir bedanken uns fur Eure Aufmerksamkeit.
Alexander Rein, Helko Glathe P/T-Netze algebraisch spezifiziert