Project

General

Profile

Revision 2d37a1e1

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