Alte Klausuren?

[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\)

[C0RNi666]

Habe meinen Beitrag nochmal editiert...

[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?

[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!