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/automata/with_properties/counters.lus
44 44 

  		




  45
  45
  
    

  		




  46
  46
  
    

  		




  47
  
  
    
--@ ensures OK;


  		




  48
  47
  
    
node top (x:bool) returns (OK:bool);


  		




  
  48
  
    
--@ contract guarantees OK;


  		




  49
  49
  
    
var a,b,d:bool;


  		




  50
  50
  
    
    s:int;


  		




  51
  51
  
    
    OK1,OK2,OK3: bool;


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/ccp02.lus
    
  





  1
  1
  
    

  		




  2
  2
  
    

  		




  3
  
  
    
--@ ensures OK;


  		




  4
  3
  
    
node top(onOff: bool; 


  		




  5
  4
  
    
      decelSet: bool; 


  		




  6
  5
  
    
      accelResume: bool; 


  		




  ......




  9
  8
  
    
      carGear: int ; 


  		




  10
  9
  
    
      carSpeed: real; 


  		




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


  		




  
  11
  
    
--@ contract guarantees OK;


  		




  12
  12
  
    
var


  		




  13
  13
  
    
   mode: int ; 


  		




  14
  14
  
    
      cruiseThrottle: real; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/ccp03.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/ccp04.lus
    
  





  1
  1
  
    

  		




  2
  
  
    
--@ ensures OK;


  		




  3
  2
  
    
node top(onOff: bool; 


  		




  4
  3
  
    
      decelSet: bool; 


  		




  5
  4
  
    
      accelResume: bool; 


  		




  ......




  9
  8
  
    
      carSpeed: real; 


  		




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


  		




  11
  10
  
    

  		




  
  11
  
    
--@ contract guarantees OK;


  		




  12
  12
  
    
var


  		




  13
  13
  
    
   mode: int ; 


  		




  14
  14
  
    
      cruiseThrottle: real; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/ccp05.lus
    
  





  1
  1
  
    

  		




  2
  
  
    
--@ ensures OK;


  		




  3
  2
  
    
node top(onOff: bool; 


  		




  4
  3
  
    
      decelSet: bool; 


  		




  5
  4
  
    
      accelResume: bool; 


  		




  ......




  9
  8
  
    
      carSpeed: real; 


  		




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


  		




  11
  10
  
    

  		




  
  11
  
    
--@ contract guarantees OK;


  		




  12
  12
  
    
var


  		




  13
  13
  
    
   mode: int ; 


  		




  14
  14
  
    
      cruiseThrottle: real; 


  		












  

    
      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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/ccp07.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/ccp08.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/ccp09.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/ccp10.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/ccp11.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/ccp12.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/ccp13.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/ccp14.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/ccp15.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/ccp16.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/ccp17.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/ccp18.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/ccp19.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/ccp20.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/ccp21.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/ccp22.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/ccp23.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/ccp24.lus
    
  





  1
  1
  
    

  		




  2
  2
  
    

  		




  3
  
  
    
--@ ensures OK;


  		




  4
  3
  
    
node top(onOff: bool; 


  		




  5
  4
  
    
      decelSet: bool; 


  		




  6
  5
  
    
      accelResume: bool; 


  		




  ......




  9
  8
  
    
      carGear: int ; 


  		




  10
  9
  
    
      carSpeed: real; 


  		




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


  		




  
  11
  
    
--@ contract guarantees OK;


  		




  12
  12
  
    
var


  		




  13
  13
  
    
   mode: int ; 


  		




  14
  14
  
    
      cruiseThrottle: real; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/cruise_controller_01.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/cruise_controller_02.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/cruise_controller_03.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/cruise_controller_04.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/cruise_controller_05.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/cruise_controller_06.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/cruise_controller_07.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/cruise_controller_08.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/cruise_controller_09.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/cruise_controller_10.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/cruise_controller_11.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/cruise_controller_12.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/cruise_controller_13.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/cruise_controller_14.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/cruise_controller_15.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/cruise_controller_16.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; 


  		












  

    
      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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/cruise_controller_18.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/cruise_controller_19.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/cruise_controller_20.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/cruise_controller_21.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/cruise_controller_22.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/cruise_controller_23.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/cruise_controller_24.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; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave01.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		




  ......




  15
  14
  
    
) returns (OK:bool);


  		




  16
  15
  
    

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave02.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		




  ......




  15
  14
  
    
) returns (OK:bool);


  		




  16
  15
  
    

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave03.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		




  ......




  15
  14
  
    
) returns (OK:bool);


  		




  16
  15
  
    

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave04.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		




  ......




  15
  14
  
    
) returns (OK:bool);


  		




  16
  15
  
    

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave05.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		




  ......




  15
  14
  
    
) returns (OK:bool);


  		




  16
  15
  
    

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave06.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		




  ......




  15
  14
  
    
) returns (OK:bool);


  		




  16
  15
  
    

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave07.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		




  ......




  15
  14
  
    
) returns (OK:bool);


  		




  16
  15
  
    

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave08.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		




  ......




  15
  14
  
    
) returns (OK:bool);


  		




  16
  15
  
    

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave09.lus
    
  





  1
  1
  
    

  		




  2
  
  
    
--@ ensures OK;


  		




  3
  2
  
    
node top(KP_START: bool; 


  		




  4
  3
  
    
      KP_CLEAR: bool; 


  		




  5
  4
  
    
      KP_0: bool; 


  		




  ......




  16
  15
  
    
) returns (OK:bool);


  		




  17
  16
  
    

  		




  18
  17
  
    
   


  		




  
  18
  
    
--@ contract guarantees OK;


  		




  19
  19
  
    
var


  		




  20
  20
  
    
   LEFT_DIGIT: int; 


  		




  21
  21
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave10.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		




  ......




  15
  14
  
    
) returns (OK:bool);


  		




  16
  15
  
    

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave11.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		




  ......




  15
  14
  
    
) returns (OK:bool);


  		




  16
  15
  
    

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave12.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		




  ......




  15
  14
  
    
) returns (OK:bool);


  		




  16
  15
  
    

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave13.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		




  ......




  15
  14
  
    
) returns (OK:bool);


  		




  16
  15
  
    

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave14.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		




  ......




  15
  14
  
    
) returns (OK:bool);


  		




  16
  15
  
    

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave15.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		




  ......




  15
  14
  
    
) returns (OK:bool);


  		




  16
  15
  
    

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave16.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		




  ......




  15
  14
  
    
) returns (OK:bool);


  		




  16
  15
  
    

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave17.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		




  ......




  15
  14
  
    
) returns (OK:bool);


  		




  16
  15
  
    

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave18.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		




  ......




  15
  14
  
    
) returns (OK:bool);


  		




  16
  15
  
    

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave19.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		




  ......




  15
  14
  
    
) returns (OK:bool);


  		




  16
  15
  
    

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave20.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		




  ......




  15
  14
  
    
) returns (OK:bool);


  		




  16
  15
  
    

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave21.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		




  ......




  15
  14
  
    
) returns (OK:bool);


  		




  16
  15
  
    

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave22.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		




  ......




  15
  14
  
    
) returns (OK:bool);


  		




  16
  15
  
    

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave23.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		




  ......




  15
  14
  
    
) returns (OK:bool);


  		




  16
  15
  
    

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave24.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		




  ......




  15
  14
  
    
) returns (OK:bool);


  		




  16
  15
  
    

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave25.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		




  ......




  15
  14
  
    
) returns (OK:bool);


  		




  16
  15
  
    

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave27.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		




  ......




  15
  14
  
    
) returns (OK:bool);


  		




  16
  15
  
    

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave28.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		




  ......




  15
  14
  
    
) returns (OK:bool);


  		




  16
  15
  
    

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave30.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		




  ......




  15
  14
  
    
) returns (OK:bool);


  		




  16
  15
  
    

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave31.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		




  ......




  15
  14
  
    
) returns (OK:bool);


  		




  16
  15
  
    

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave32.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		




  ......




  15
  14
  
    
) returns (OK:bool);


  		




  16
  15
  
    

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave33.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		




  ......




  15
  14
  
    
) returns (OK:bool);


  		




  16
  15
  
    

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave34.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		




  ......




  15
  14
  
    
) returns (OK:bool);


  		




  16
  15
  
    

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave35.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		




  ......




  15
  14
  
    
) returns (OK:bool);


  		




  16
  15
  
    

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave36.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		




  ......




  15
  14
  
    
) returns (OK:bool);


  		




  16
  15
  
    

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












  

    
      regression_tests/lustre_files/success/kind_fmcad08/large/microwave37.lus
    
  





  1
  
  
    
--@ ensures OK;


  		




  2
  1
  
    
node top(KP_START: bool; 


  		




  3
  2
  
    
      KP_CLEAR: bool; 


  		




  4
  3
  
    
      KP_0: bool; 


  		








... This diff was truncated because it exceeds the maximum size that can be displayed.



Also available in:  Unified diff