Quelle  TimeBug.vdmpp

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] ==> ()