module Light

spec Light
  switch: Boolean;
  
  init event switchOn() 
    post: this.switch' = Boolean[TRUE]; 
   
  event switchOff() 
    pre: this.switch = Boolean[TRUE]; 
    post: this.switch' = Boolean[FALSE];
        
  final event brokenBulb()  
  
  states:      
    (*) -> lightOn: switchOn;   
    lightOn -> lightOff: switchOff;     
    lightOff -> lightOn: switchOn;
    lightOff -> (*): brokenBulb;
        
spec Boolean [TRUE,FALSE]      
       
config OneLight = l1: Light is uninitialized;
    
assert CanBeTurnedOnAndOff = exists l: Light | ((l is initialized => l is lightOn) until l is lightOff);
run CanBeTurnedOnAndOff from OneLight in max 4 steps with infinite trace expect trace; 

assert BulbCanBreak = eventually exists l: Light | l is finalized;
run BulbCanBreak from OneLight in max 4 steps expect trace;