Aufgabe 5

Spezifizieren Sie einen Round-Robin-Scheduler, der folgende Eigenschaften erfüllt:

• Er verwaltet drei Prozesse der Form FibonacciProcess (siehe TLA^{+}-Modul auf der nächsten Seite). Die Anzahl der Prozesse ändert sich nicht.

• Es gibt eine Prozeßliste, in denen die Prozesse mit ihren Umgebungen (d.h. in TLA^{+}: ihren Variablen) abgelegt sind.

• Der Scheduler benutzt die Aktionen Save und Restore:

Save sorgt für das Ablegen des gerade aktiven Prozesses mit

seiner Umgebung an das Ende der Prozeßliste. Restore aktiviert den Prozeß, der am Kopf der Prozeßliste

steht, inklusive Umgebung.

• Es gibt ein Modul Clock, das nebenläufig eine Variable clock hochzählt.

• Der Scheduler aktiviert nach jeweils 10 Clock-Schritten den nächsten Prozeß in der Liste.

Das Modul Naturals (S. 3) definiert die Menge der natürlichen Zahlen mit den üblichen Rechenoperationen. Es muß (eigentlich …) immer eingebunden werden, wenn mit natürlichen Zahlen gearbeitet wird.

Ein ähnliches Definitionsmodul ist Sequences (S. 3): es definiert einige Operationen für das Rechnen mit Folgen auf der Basis von Tupeln und könnte hier bei der Modellierung der Warteschlange nützlich sein.

module FibonacciProcess

parameters pc, x, y : variable

import Naturals

predicates

Init =^{Δ} \begin{matrix}∧ pc = 1 \\ ∧ x = 1 \\ ∧ y = 1 \end{matrix}

definitions Vars =^{Δ} ⟨pc, x, y ⟩

actions Fib_{x} =^{Δ} ∧ pc = 1 ∧ x′ = x + y ∧ pc′ = 2 ∧ unchanged y

Fib_{y} =^{Δ} ∧ pc = 2 ∧ y′ = x + y ∧ pc′ = 1 ∧ unchanged x

temporal SomeAction =^{Δ} ∨ Fib_{x} ; ∨ Fib_{y}

Spec =^{Δ} ∧ Init ∧ □[SomeAction]_{Vars}

Das Modul Naturals ist bisher nicht geschrieben worden, weil es eine ”etwas größere“ Schreibarbeit ist, die natürlichen Zahlen aus der Mengentheorie heraus zu definieren. Ein ”import Naturals“ stellt aber neben den Zahlen selbst auf jeden Fall folgende Definitionen zur Verfügung:

• die Menge Nat der natürlichen Zahlen (inklusive 0)

• die binären Relationen =, ≠, <, ≤, >, ≥ auf Nat

• die binären Operatoren +, −, ∗, /, mod auf Nat

module Sequences

import Naturals

m..n  =^{Δ} {i ∈ Nat : (m ≤ i) ∧ (i ≤ n)}

Len(s) =^{Δ} choose n : (n ∈ Nat) ∧ ((Domain s) = (1..n))

Head(s) =^{Δ} s[1]

Tail(s) =^{Δ} [i ∈ 1..(Len(s) − 1) ↦ s[i + 1]]

s ∘ t  =^{Δ} [i ∈ 1..(Len(s) + Len(t)) ↦ if i ≤ Len(s) then s[i] else t[i − Len(s)]]

Seq(S) =^{Δ} union {[(1..n) → S] : n ∈ Nat} SelectSeq(s, test( )) =^{Δ} let F [ t : Seq({s[i] : i ∈ (1..Len(s))}) ] =^{Δ} if t = ⟨ ⟩ then ⟨ ⟩ else if test(Head(t)) then ⟨Head(t)⟩ ∘ F [Tail(t)] else F [Tail(t)] in F [s]

SubSeq(s, m, n) =^{Δ} [i ∈ (1..(1 + n − m)) ↦ s[i + m − 1]]