Project

General

Profile

« Previous | Next » 

Revision 2d37a1e1

Added by Pierre-Loïc Garoche over 6 years ago

Renaminig lustre contracts from ensures to guarantees
Will require the latest cocospec branch to compile (before it is integrated in the unstable/master branches)

View differences:

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

  		




  2
  2
  
    

  		




  3
  
  
    
--@ ensures OK;


  		




  4
  3
  
    
node top(onOff: bool; 


  		




  5
  4
  
    
      decelSet: bool; 


  		




  6
  5
  
    
      accelResume: bool; 


  		




  ......




  10
  9
  
    
      carSpeed: real; 


  		




  11
  10
  
    
      validInputs: bool) returns (OK: bool);


  		




  12
  11
  
    

  		




  
  12
  
    
--@ contract guarantees OK;


  		




  13
  13
  
    
var


  		




  14
  14
  
    
   mode: int ; 


  		




  15
  15
  
    
      cruiseThrottle: real; 


  		












Also available in:  Unified diff