|
BarrierReached : () ==> ()
BarrierReached() ==
(
while (card dom wakeUpMap = barrierCount) do
(
currentTime := currentTime + stepLength;
let threadSet : set of nat = {th | th in set dom wakeUpMap
& wakeUpMap(th) <> nil and wakeUpMap(th) <= currentTime }
in
(debugSet := threadSet;
for all t in set threadSet
do
wakeUpMap := {t} <-: wakeUpMap;
);
);
)
post forall x in set rng wakeUpMap & x = nil or x > currentTime;
AddToWakeUpMap : nat * [nat] ==> ()
¤ Dauer der Verarbeitung: 0.12 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.
|
