Database Reference
In-Depth Information
Wahrend der Ausfuhrung des Algorithmus - und nur dann! - kann es vorkom-
men, dass ein Knoten den Status
Label
(n)=
unknown
erhalt. So kann z.B. ein
out
-Knoten einer nicht-fundiert gultigen Begrundung (s. obige Definition 7.19) das
Label
unknown
haben.
Nun haben wir das notige Repertoire an Begriffen bereitgestellt, das gebraucht
wird, um den Algorithmus eines TM-Verfahrens zu formalisieren. Dieser wird jedes
Mal angestoßen, wenn eine neue Begrundung der Menge
hinzugefugt wird und da-
mit eventuelle Statuswechsel von Knoten notwendig werden. Der TM-Algorithmus
sucht, ausgehend von einem gegebenen zulassigen Modell, ein neues zulassiges Mo-
dell bzgl. der erweiterten Menge an Begrundungen.
Der Einfachheit und Ubersichtlichkeit halber werden wir das Hinzufugen eines
Elementes zu einer Menge durch eine +-Operation beschreiben.
Label
(n) bezeichnet
den Status eines Knotens n,also
in
,
out
oder
unknown
. Kommentarzeilen werden
durch ein % eingeleitet.
J
Algorithmus JTMS-Verfahren
Eingabe:
Ein TM-Netzwerk
T
=(N,
J
);
ein zulassiges Modell M bzgl.
T
;
eine neue Begrundung J
0
=
I
0
|
O
0
→
n
0
.
Ausgabe:
Ein zulassiges Modell
1
M
bzgl. des TM-Netzwerks
T
=(N,
);
(evtl. die Angabe aller vorgenommenen Statuswechsel von Knoten).
J∪{
J
0
}
1.
% Hinzufugen von J
0
, aktualisieren von Cons(n)
J
:=
J
+ J
0
;
J
(n
0
):=
J
(n
0
)+J
0
;
for
n
O
0
do
Cons(n):=Cons(n)+n
0
;
if
Label
(n
0
)=
in
then
HALT.
if
J
0
ungultig in M
then
Supp(n
0
):=Supp(n
0
)+n
; HALT.
(wobei n
out
-Knoten aus I
0
oder
in
-Knoten aus O
0
)
∈
I
0
∪
% Uberprufe ACons(n
0
)
if
ACons(n
0
)=
2.
∅
then
Label
(n
0
):=
in
;
Supp(n
0
):=I
0
∪
O
0
;
SJ(n
0
):=J
0
;
fuge n
0
als großtes Element an M an: M := M + n
0
; HALT.
3.
% Es gilt
Label
(n
0
)=
out
% J
0
ist gultig in M
% ACons(n
0
)
∅
L := ACons
∗
(n
0
)+n
0
;
=
1
Fur bestimmte pathologische TM-Netzwerke mit sog.
odd loops
kann es passieren, dass der
Algorithmus nicht terminiert oder ein nicht zulassiges Modell als Ergebnis liefert (vgl. Seite 219).
