Project

General

Profile

Revision 2d37a1e1 regression_tests/lustre_files/success/kind_fmcad08/large/cruise_controller_17.lus

View differences:

regression_tests/lustre_files/success/kind_fmcad08/large/cruise_controller_17.lus
1 1 

  		




  2
  2
  
    

  		




  3
  
  
    
--@ ensures OK;


  		




  4
  3
  
    
node top(onOff: bool; 


  		




  5
  4
  
    
      decelSet: bool; 


  		




  6
  5
  
    
      accelResume: bool; 


  		




  ......




  11
  10
  
    
      validInputs: bool)


  		




  12
  11
  
    
   returns (OK:bool);


  		




  13
  12
  
    

  		




  
  13
  
    
--@ contract guarantees OK;


  		




  14
  14
  
    
var


  		




  15
  15
  
    
mode: int; 


  		




  16
  16
  
    
      cruiseThrottle: real; 


  		












Also available in:  Unified diff