Push Back Operation

Compensation using the mechanism concept.

The inout declaration

An inout field can unilaterally change to a safe value. Only one participating bundle per field has the capability to write a non-safe value.

   pebble sw1 = tup://128.232.10.22:4000/keypad#switch1;
   pebble digit = tup://128.232.10.22:4000/display#Digit22;

   input sw1 : { off : on };
   inout digit: { off : 0..9 };

   digit := (sw1==on) ? 1:off;  // Cannot push back as sw1 is not inout

The compiler creates new executable rules that reverse the operation of every assignment, operator and function. Compile-time error if not obvious.

   inout out1 { true: false };
   inout out2 { false: true };


   out1 : = A == B;    // Select either A or B where safe values of expression
                       // to be pushed on encompass the full range of the other.
 
   out2 : = C == D;    

   out3 : = (E) ? R : F;  // Chooses either R or F for all pushbacks. May need to push
                          // on E as well.

Fuse Statement

   //   digit := (sw1==on) ? 1:off;  // Would not compile

   fuse F1;
   {   digit := (sw1==on) ? 1:off;   } fuse F1;

   // Other code can be triggered when the fuse blows
   forever 
   {
      wait F1; sleep_secs(5);  F1 := false; 
   }