|
\begin{vdm_al}
class Table
instance variables
forks : nat := 0;
guests : set of Philosopher := {};
done : nat := 0
operations
public Table: nat1 ==> Table
Table (noGuests) ==
while forks < noGuests do
( guests := guests union
{new Philosopher(self)};
forks := forks + 1 )
pre noGuests >= 2;
public takeFork: () ==> ()
takeFork () == forks := forks - 1;
public releaseFork: () ==> ()
releaseFork () == forks := forks + 1;
public IamDone: () ==> ()
IamDone () == done := done + 1;
wait: () ==> ()
wait () == skip;
public LetsEat: () ==> ()
LetsEat () ==
( startlist(guests); wait() )
sync
per takeFork => forks > 0;
per wait => done = card guests;
mutex(takeFork,releaseFork);
mutex(IamDone)
end Table
\end{vdm_al}
¤ Dauer der Verarbeitung: 0.3 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
