Alte Klausuren?

mister_tt
Kernelcompilierer
Kernelcompilierer
Beiträge: 502
Registriert: 29. Sep 2008 15:54

Re: Alte Klausuren?

Beitrag von mister_tt »

Also ich schreib jetzt einfach mal meine ganz Lösung hier rein...

Aufgabe 1
1. Der Wertebereich \(S := \{ l, r \} x P(M) x P(M) x \mathbb N\) ist für die Modellierung der Zustände angemessen. Das Tupel \((d, L, R, n) \in S\) modelliert, dass
- sich die Taschenlampe auf der Seite, die durch das Symbol \(d\) modelliert wird, befindet,
- sich die Personen, die durch die Symbole in der Menge \(L\) bzw. \(R\) auf der linken bzw. rechten Seite befinden,
- n die verstrichene Zeit in Minuten seit Beginn der Brückenüberquerung angibt.

2. \(S_0 = \{ (l, \{ 5, 10, 20, 25 \}), \{ \}, 0 \}\)

3. \(P := \{ (d, L, R, n) \in \{ l, r \} x P(M) x P(M) x \mathbb N | (L \cup R) = \{ 5, 10, 20, 25 \} \wedge (L \cap R = \emptyset) \}\)

4. \(E := \{ überquere(d, P) | s \in \{ l, r \} \wedge P \in P(M) \}\), wobei \(überquere(d, P)\) modelliert, dass die Personen, die durch die Symbole in der Menge \(P\) modelliert werden, die Brücke in die Richtung, die durch das Symbol \(d\) modelliert wird, überqueren.

5. \(\rightarrow := \{ ((l, L, R, n), überquere(r, P), (r, L', R', n')) \in S x E x S | (L' = L \backslash P) \wedge (R' = R \cup P) \wedge (n' = max(P)) \wedge (|P| \leq 2) \wedge (|P| > 0) \}\)
\(\cup \{ ((r, L, R, n), überquere(l, P), (l, L', R', n')) \in S x E x S | (L' = L \cup P) \wedge (R' = R \backslash P) \wedge (n' = max(P)) \wedge (|P| \leq 2) \wedge (|P| > 0) \}\)

Aufgabe 2
1. \((r \exists f) \frac{<b[X \mapsto n], \sigma> \Downarrow false}{<\exists X.b, \sigma, Z> \Rightarrow false} Z = (n), n \in \mathbb N\)

2. \((r \forall f) \frac{<b[X \mapsto n], \sigma> \Downarrow false}{<\forall X.b, \sigma, Z> \Rightarrow false} Z = (z_1, ..., z_n), n \in \mathbb N\)
\((r \forall) \frac{<b[X \mapsto z_1], \sigma> \Downarrow true ~ ~ ~ <\forall X.b, \sigma, Z'> \Rightarrow w}{<\forall X.b, \sigma, Z> \Rightarrow w} Z = (z_1, ..., z_n), Z' = (z_2, ..., z_n) n \in \mathbb N\)
\((r \forall t) \frac{<b[X \mapsto n], \sigma> \Downarrow true}{<\forall X.b, \sigma, Z> \Rightarrow true} Z = (n), n \in \mathbb N\)
Zuletzt geändert von mister_tt am 9. Mär 2010 15:24, insgesamt 2-mal geändert.

Benutzeravatar
C0RNi666
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 114
Registriert: 8. Jan 2008 12:51

Re: Alte Klausuren?

Beitrag von C0RNi666 »

Habe meinen Beitrag nochmal editiert...
Win32: Reboot!
Unix: Be root!

Radze
Erstie
Erstie
Beiträge: 21
Registriert: 10. Okt 2008 10:14

Re: Alte Klausuren?

Beitrag von Radze »

OK so siehts dann besser aus.
Wobei du den Hinweis noch umsetzen könntest. Es geht wirklich mit nur 2 Regeln. Kleiner Tip: Wenn alle bis auf das letzte Element der Liste b erfüllen. Wie komme ich dann an das Gesamtergebnis?

Benutzeravatar
C0RNi666
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 114
Registriert: 8. Jan 2008 12:51

Re: Alte Klausuren?

Beitrag von C0RNi666 »

@mister_tt, meine Lösung sieht ähnlich aus wie deine. Eventuell kannst du dir bei geeigneter Modellierung den Parameter d in dem Ereignis überquere(d, P) sparen.

Dann noch eine andere Variante..
\((rA)~\frac{ <AX.b, \sigma, (z_1, ..., z_{n-1})>\Rightarrow ~ true ~~<b[X \rightarrow z_{n}], ~ \sigma> \Downarrow true~~}{<AX.b, ~ \sigma>, ~ Z> \Rightarrow true>}~Z = (z_1, ..., z_n) n \epsilon \mathbb N\)

\((rAf) \frac{<EX.b, ~ \sigma>, ~ Z> \Rightarrow ~ false>}{<AX.b, ~ \sigma>, ~ Z> \Rightarrow false>} ~ Z = (z_1, ..., z_n) n \epsilon \mathbb N\)

Idee: Ist vielleicht die Variable \(\omega\) überflüssig?

Thx @ Radze!
Win32: Reboot!
Unix: Be root!

Antworten

Zurück zu „Archiv“