Algebraic Specification Of Pt Nets

30
Signatur Algebren Erweiterterung Ende P/T-Netze algebraisch spezifiziert Alexander Rein, Helko Glathe 01.11.2006 Alexander Rein, Helko Glathe P/T-Netze algebraisch spezifiziert

Transcript of Algebraic Specification Of Pt Nets

Page 1: 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

Page 2: Algebraic Specification Of Pt Nets

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

Page 3: Algebraic Specification Of Pt Nets

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

Page 4: Algebraic Specification Of Pt Nets

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

Page 5: Algebraic Specification Of Pt Nets

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

Page 6: Algebraic Specification Of Pt Nets

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

Page 7: Algebraic Specification Of Pt Nets

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

Page 8: Algebraic Specification Of Pt Nets

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

Page 9: Algebraic Specification Of Pt Nets

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

Page 10: Algebraic Specification Of Pt Nets

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

Page 11: Algebraic Specification Of Pt Nets

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

Page 12: Algebraic Specification Of Pt Nets

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

Page 13: Algebraic Specification Of Pt Nets

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

Page 14: Algebraic Specification Of Pt Nets

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

Page 15: Algebraic Specification Of Pt Nets

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

Page 16: Algebraic Specification Of Pt Nets

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

Page 17: Algebraic Specification Of Pt Nets

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

Page 18: Algebraic Specification Of Pt Nets

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

Page 19: Algebraic Specification Of Pt Nets

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

Page 20: Algebraic Specification Of Pt Nets

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

Page 21: Algebraic Specification Of Pt Nets

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

Page 22: Algebraic Specification Of Pt Nets

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

Page 23: Algebraic Specification Of Pt Nets

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

Page 24: Algebraic Specification Of Pt Nets

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

Page 25: Algebraic Specification Of Pt Nets

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

Page 26: Algebraic Specification Of Pt Nets

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

Page 27: Algebraic Specification Of Pt Nets

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

Page 28: Algebraic Specification Of Pt Nets

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

Page 29: Algebraic Specification Of Pt Nets

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

Page 30: Algebraic Specification Of Pt Nets

SignaturAlgebren

ErweiterterungEnde

Wir bedanken uns fur Eure Aufmerksamkeit.

Alexander Rein, Helko Glathe P/T-Netze algebraisch spezifiziert