# Blatt 6

Hazard: $$v.D = Ruptured$$

### DCCA:

#### Überprüfung

##### Einelementige

* fs: :heavy_check_mark:
* ft: :heavy_check_mark:
* fk1: :heavy_check_mark:
* fk2: :x:
* fs1: :heavy_check_mark:

##### ZweiElementige

* {fs, ft}: :x:
* {fs, fk1}: :x:
* {fs, fs1}: :x:
* {ft, fk1}: :heavy_check_mark:
* {ft, fs1}: :heavy_check_mark:
* {fk1, fs1}: :heavy_check_mark:

#### Minimal Critial Sets

* {fk2}: :x:
* {fs, ft}: :x:
* {fs, fk1}: :x:
* {fs, fs1}: :x:

## Quantitative Analyse

\begin{align*}
P(fs1) &= 3 \cdot 10^{-5} \\
P(fk1) &= 3 \cdot 10^{-5} \\
P(fk2) &= 3 \cdot 10^{-5} \\
P(ft) &= 1 \cdot 10^{-4} \\
P(fs) &= 1 \cdot 10^{-4} \\
\\
P(HAZARD)&= P(fk2) + P(fs) * (P(ft) + P(fk1) + P(fs1)) \\
&= 3\cdot 10^{-5} + 10^{-4} (10^{-4} + 3\cdot 10^{-5} + 3\cdot 10^{-5}) \\
&= 3,0016 \cdot 10^{-5}
\end{align*}

## Aufgabe 13
Siehe `drucktank.prism`

## Aufgabe 14
Ergebnisse von PRISM für Property `P=? [F "hazard_ruptured" ]`:

Jacobi: 1632 iterations in 4014.64 seconds (average 2.458577, setup 2.24)

Value in the initial state: 0.9999584762419129

Time for model checking: 4015.56 seconds.

Result: 0.9999584762419129 (value in the initial state)

Das Ergebnis ist also: Zu fast 100% tritt irgendwann der Hazard ein.
Dies liegt daran, dass die Fehler bei jedem Übergang zu einer bestimmten Wahrscheinlichkeit eintreten können; im Gegensatz dazu wird bei der DCCA vor dem Prüfen bestimmt, ob ein Fehler $F$ überhaupt eintreten kann oder nicht und falls hier der Hazard eintritt wird dies nur einmal mit der Fehlerwahrscheinlichkeit $p_F$ gewertet.
In PRISM kann jeder Fehler beliebig häufig vorkommen, sodass die Wahrscheinlichkeit gegen 1 konvergiert.

* Indeterministischer Übergang von Start zu Closed
* Floating Point Ungenauigkeiten
* Wahrscheinlichkeit, dass irgendwann ein Fehler auftritt
* Wir wollen eigentlich die Wahrscheinlichkeit in einem Durchlauf