Safe and Live Assertions

Library fragment

def bundle __std_lib()
{
  input __local_timer#time_now
   #(hours : {0..23},
     minutes : {0..59},
     seconds : { 0..59},
     cseconds : { 0..99 }
    );

  fun sleep_secs(t)
  {
    local until : { 0..59 };
	until := (__local_timer#time_now#second + t);
	wait(__local_timer#time_now#second FQGT until);
  }

  ...
}  

A door unlock example

def bundle ButtonLock()
{
  input v#keys#button : { false:true};
  output v#locks#unlocked : { false:true };
  forever {
    wait (button);
    unlocked := true;
    sleep_secs(5);
    unlocked := false;
    wait (!button);
    }
  local locked := !unlocked;
  live unlocked, locked;
}

Incompatible Bundle

def bundle B2()
{
  pebble lock = tup://128.232.1.45/v;
  input d#q : bool; 

  r#keys#button := lock#locks#unlocked && d#q;

}  

The lock would become deadlocked and hence bundle B2 cannot be loaded.