Project

General

Profile

Revision 65f71d05

View differences:

test/src/kind_fmcad08/large/ccp01.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/ccp02.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/ccp03.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/ccp04.lus
1 1

  
2
--@ ensures OK;
2 3
node top(onOff: bool; 
3 4
      decelSet: bool; 
4 5
      accelResume: bool; 
test/src/kind_fmcad08/large/ccp05.lus
1 1

  
2
--@ ensures OK;
2 3
node top(onOff: bool; 
3 4
      decelSet: bool; 
4 5
      accelResume: bool; 
test/src/kind_fmcad08/large/ccp06.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/ccp07.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/ccp08.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/ccp09.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/ccp10.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/ccp11.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/ccp12.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/ccp13.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/ccp14.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/ccp15.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/ccp16.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/ccp17.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/ccp18.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/ccp19.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/ccp20.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/ccp21.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/ccp22.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/ccp23.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/ccp24.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/cruise_controller_01.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/cruise_controller_02.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/cruise_controller_03.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/cruise_controller_04.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/cruise_controller_05.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/cruise_controller_06.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/cruise_controller_07.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/cruise_controller_08.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/cruise_controller_09.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/cruise_controller_10.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/cruise_controller_11.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/cruise_controller_12.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/cruise_controller_13.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/cruise_controller_14.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/cruise_controller_15.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/cruise_controller_16.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/cruise_controller_17.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/cruise_controller_18.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/cruise_controller_19.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/cruise_controller_20.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/cruise_controller_21.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/cruise_controller_22.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/cruise_controller_23.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/cruise_controller_24.lus
1 1

  
2 2

  
3
--@ ensures OK;
3 4
node top(onOff: bool; 
4 5
      decelSet: bool; 
5 6
      accelResume: bool; 
test/src/kind_fmcad08/large/microwave01.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave02.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave03.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave04.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave05.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave06.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave07.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave08.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave09.lus
1 1

  
2
--@ ensures OK;
2 3
node top(KP_START: bool; 
3 4
      KP_CLEAR: bool; 
4 5
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave10.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave11.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave12.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave13.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave14.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave15.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave16.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave17.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave18.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave19.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave20.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave21.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave22.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave23.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave24.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave25.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave26.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave27.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave28.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave29.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave30.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave31.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave32.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave33.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave34.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave35.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave36.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave37.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave38.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave39.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/microwave40.lus
1
--@ ensures OK;
1 2
node top(KP_START: bool; 
2 3
      KP_CLEAR: bool; 
3 4
      KP_0: bool; 
test/src/kind_fmcad08/large/steam_boiler_no_arr1.lus
756 756

  
757 757
 
758 758

  
759
--@ ensures OK;
759 760
node top( 
760 761
  stop, 
761 762
  steam_boiler_waiting, 
test/src/kind_fmcad08/large/steam_boiler_no_arr1_e4_23904_e4_2384.lus
624 624
  (b2,b3)=
625 625
    SteamOutput(op_mode,steam_defect,steam_repaired); 
626 626
tel
627
--@ ensures OK;
627 628
node top( 
628 629
  stop, 
629 630
  steam_boiler_waiting, 
test/src/kind_fmcad08/large/steam_boiler_no_arr2.lus
751 751
tel
752 752

  
753 753

  
754
--@ ensures OK;
754 755
node top(
755 756
  steam_boiler_waiting,physical_units_ready,stop_request:bool; 
756 757
  steam,level_defect,steam_defect:int; 
test/src/kind_fmcad08/large/steam_boiler_no_arr2_e1_17214_e5_18600.lus
621 621
  (b2,b3)=
622 622
    SteamOutput(op_mode,steam_defect,steam_repaired); 
623 623
tel
624
--@ ensures OK;
624 625
node top(
625 626
  steam_boiler_waiting,physical_units_ready,stop_request:bool; 
626 627
  steam,level_defect,steam_defect:int; 
test/src/kind_fmcad08/large/steam_boiler_no_arr2_e3_514_e4_11150.lus
622 622
  (b2,b3)=
623 623
    SteamOutput(op_mode,steam_defect,steam_repaired); 
624 624
tel
625
--@ ensures OK;
625 626
node top(
626 627
  steam_boiler_waiting,physical_units_ready,stop_request:bool; 
627 628
  steam,level_defect,steam_defect:int; 
test/src/kind_fmcad08/large/steam_boiler_no_arr2_e6_3003_e4_15091.lus
622 622
  (b2,b3)=
623 623
    SteamOutput(op_mode,steam_defect,steam_repaired); 
624 624
tel
625
--@ ensures OK;
625 626
node top(
626 627
  steam_boiler_waiting,physical_units_ready,stop_request:bool; 
627 628
  steam,level_defect,steam_defect:int; 
test/src/kind_fmcad08/large/steam_boiler_no_arr2_e7_12307.lus
622 622
  (b2,b3)=
623 623
    SteamOutput(op_mode,steam_defect,steam_repaired); 
624 624
tel
625
--@ ensures OK;
625 626
node top(
626 627
  steam_boiler_waiting,physical_units_ready,stop_request:bool; 
627 628
  steam,level_defect,steam_defect:int; 
test/src/kind_fmcad08/large/steam_boiler_no_arr2_e8_21449_e5_18210.lus
622 622
  (b2,b3)=
623 623
    SteamOutput(op_mode,steam_defect,steam_repaired); 
624 624
tel
625
--@ ensures OK;
625 626
node top(
626 627
  steam_boiler_waiting,physical_units_ready,stop_request:bool; 
627 628
  steam,level_defect,steam_defect:int; 
test/src/kind_fmcad08/memory1/DRAGON_1.lus
92 92
   pre invalid;
93 93
tel
94 94

  
95
--@ ensures OK;
95 96
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
96 97
         init_invalid : int ) returns ( OK : bool );
97 98
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_10.lus
93 93
tel
94 94

  
95 95
-- Not provable with luke-bitvec
96
--@ ensures OK;
96 97
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
97 98
             init_invalid : int ) returns ( OK : bool );
98 99
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_10_e1_3587_e3_2749.lus
81 81
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
82 82
   pre invalid;
83 83
tel
84
--@ ensures OK;
84 85
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
85 86
             init_invalid : int ) returns ( OK : bool );
86 87
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_10_e1_3587_e7_872.lus
81 81
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
82 82
   pre invalid;
83 83
tel
84
--@ ensures OK;
84 85
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
85 86
             init_invalid : int ) returns ( OK : bool );
86 87
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_10_e1_998.lus
81 81
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
82 82
   pre invalid;
83 83
tel
84
--@ ensures OK;
84 85
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
85 86
             init_invalid : int ) returns ( OK : bool );
86 87
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_10_e2_2785_e3_1744.lus
81 81
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
82 82
   pre invalid;
83 83
tel
84
--@ ensures OK;
84 85
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
85 86
             init_invalid : int ) returns ( OK : bool );
86 87
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_10_e2_402.lus
81 81
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
82 82
   pre invalid;
83 83
tel
84
--@ ensures OK;
84 85
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
85 86
             init_invalid : int ) returns ( OK : bool );
86 87
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_10_e3_144_e5_2046.lus
81 81
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
82 82
   pre invalid;
83 83
tel
84
--@ ensures OK;
84 85
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
85 86
             init_invalid : int ) returns ( OK : bool );
86 87
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_10_e3_144_e7_523.lus
81 81
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
82 82
   pre invalid;
83 83
tel
84
--@ ensures OK;
84 85
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
85 86
             init_invalid : int ) returns ( OK : bool );
86 87
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_10_e3_3429.lus
81 81
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
82 82
   pre invalid;
83 83
tel
84
--@ ensures OK;
84 85
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
85 86
             init_invalid : int ) returns ( OK : bool );
86 87
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_10_e7_3861_e2_1020.lus
81 81
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
82 82
   pre invalid;
83 83
tel
84
--@ ensures OK;
84 85
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
85 86
             init_invalid : int ) returns ( OK : bool );
86 87
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_10_e7_3861_e7_2180.lus
81 81
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
82 82
   pre invalid;
83 83
tel
84
--@ ensures OK;
84 85
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
85 86
             init_invalid : int ) returns ( OK : bool );
86 87
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_11.lus
101 101
tel
102 102

  
103 103
-- Not provable?
104
--@ ensures OK;
104 105
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
105 106
             init_invalid : int ) returns ( OK : bool );
106 107
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_11_e1_2450.lus
85 85
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
86 86
   pre invalid;
87 87
tel
88
--@ ensures OK;
88 89
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
89 90
             init_invalid : int ) returns ( OK : bool );
90 91
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_11_e1_2450_e1_5887.lus
85 85
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
86 86
   pre invalid;
87 87
tel
88
--@ ensures OK;
88 89
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
89 90
             init_invalid : int ) returns ( OK : bool );
90 91
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_11_e1_2450_e2_1483.lus
85 85
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
86 86
   pre invalid;
87 87
tel
88
--@ ensures OK;
88 89
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
89 90
             init_invalid : int ) returns ( OK : bool );
90 91
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_11_e1_2450_e3_2330.lus
85 85
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
86 86
   pre invalid;
87 87
tel
88
--@ ensures OK;
88 89
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
89 90
             init_invalid : int ) returns ( OK : bool );
90 91
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_11_e1_2450_e7_5791.lus
85 85
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
86 86
   pre invalid;
87 87
tel
88
--@ ensures OK;
88 89
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
89 90
             init_invalid : int ) returns ( OK : bool );
90 91
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_11_e2_1678_e1_3565.lus
85 85
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
86 86
   pre invalid;
87 87
tel
88
--@ ensures OK;
88 89
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
89 90
             init_invalid : int ) returns ( OK : bool );
90 91
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_11_e2_5396_e3_282.lus
85 85
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
86 86
   pre invalid;
87 87
tel
88
--@ ensures OK;
88 89
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
89 90
             init_invalid : int ) returns ( OK : bool );
90 91
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_11_e3_382_e1_505.lus
85 85
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
86 86
   pre invalid;
87 87
tel
88
--@ ensures OK;
88 89
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
89 90
             init_invalid : int ) returns ( OK : bool );
90 91
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_11_e3_382_e4_4421.lus
85 85
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
86 86
   pre invalid;
87 87
tel
88
--@ ensures OK;
88 89
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
89 90
             init_invalid : int ) returns ( OK : bool );
90 91
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_12.lus
101 101
tel
102 102

  
103 103
-- Only provable in nbac
104
--@ ensures OK;
104 105
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
105 106
             init_invalid : int ) returns ( OK : bool );
106 107
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_12_e1_4640_e7_128.lus
85 85
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
86 86
   pre invalid;
87 87
tel
88
--@ ensures OK;
88 89
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
89 90
             init_invalid : int ) returns ( OK : bool );
90 91
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_12_e2_1618.lus
85 85
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
86 86
   pre invalid;
87 87
tel
88
--@ ensures OK;
88 89
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
89 90
             init_invalid : int ) returns ( OK : bool );
90 91
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_12_e2_1618_e1_6030.lus
85 85
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
86 86
   pre invalid;
87 87
tel
88
--@ ensures OK;
88 89
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
89 90
             init_invalid : int ) returns ( OK : bool );
90 91
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_12_e2_1618_e2_138.lus
85 85
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
86 86
   pre invalid;
87 87
tel
88
--@ ensures OK;
88 89
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
89 90
             init_invalid : int ) returns ( OK : bool );
90 91
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_12_e2_1618_e3_2012.lus
85 85
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
86 86
   pre invalid;
87 87
tel
88
--@ ensures OK;
88 89
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
89 90
             init_invalid : int ) returns ( OK : bool );
90 91
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_12_e2_1618_e7_4732.lus
85 85
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
86 86
   pre invalid;
87 87
tel
88
--@ ensures OK;
88 89
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
89 90
             init_invalid : int ) returns ( OK : bool );
90 91
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_13.lus
101 101
tel
102 102

  
103 103
-- Only provable in nbac
104
--@ ensures OK;
104 105
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
105 106
             init_invalid : int ) returns ( OK : bool );
106 107
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_13_e3_1418_e3_2761.lus
85 85
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
86 86
   pre invalid;
87 87
tel
88
--@ ensures OK;
88 89
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
89 90
             init_invalid : int ) returns ( OK : bool );
90 91
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_13_e7_2336.lus
85 85
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
86 86
   pre invalid;
87 87
tel
88
--@ ensures OK;
88 89
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
89 90
             init_invalid : int ) returns ( OK : bool );
90 91
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_13_e7_2336_e1_541.lus
85 85
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
86 86
   pre invalid;
87 87
tel
88
--@ ensures OK;
88 89
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
89 90
             init_invalid : int ) returns ( OK : bool );
90 91
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_13_e7_2336_e2_1255.lus
85 85
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
86 86
   pre invalid;
87 87
tel
88
--@ ensures OK;
88 89
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
89 90
             init_invalid : int ) returns ( OK : bool );
90 91
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_13_e7_2336_e3_3117.lus
85 85
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
86 86
   pre invalid;
87 87
tel
88
--@ ensures OK;
88 89
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
89 90
             init_invalid : int ) returns ( OK : bool );
90 91
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_13_e7_2336_e7_685.lus
85 85
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
86 86
   pre invalid;
87 87
tel
88
--@ ensures OK;
88 89
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
89 90
             init_invalid : int ) returns ( OK : bool );
90 91
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_14.lus
101 101
tel
102 102

  
103 103
-- Not provable?
104
--@ ensures OK;
104 105
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
105 106
             init_invalid : int ) returns ( OK : bool );
106 107
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_14_e1_5710.lus
85 85
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
86 86
   pre invalid;
87 87
tel
88
--@ ensures OK;
88 89
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
89 90
             init_invalid : int ) returns ( OK : bool );
90 91
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_14_e2_3606.lus
85 85
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
86 86
   pre invalid;
87 87
tel
88
--@ ensures OK;
88 89
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
89 90
             init_invalid : int ) returns ( OK : bool );
90 91
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_14_e3_1259_e1_5798.lus
85 85
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
86 86
   pre invalid;
87 87
tel
88
--@ ensures OK;
88 89
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
89 90
             init_invalid : int ) returns ( OK : bool );
90 91
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_14_e3_5120.lus
85 85
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
86 86
   pre invalid;
87 87
tel
88
--@ ensures OK;
88 89
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
89 90
             init_invalid : int ) returns ( OK : bool );
90 91
    var exclusive, shared, shared_dirty, dirty, invalid : int;
test/src/kind_fmcad08/memory1/DRAGON_14_e7_3162.lus
85 85
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
86 86
   pre invalid;
87 87
tel
88
--@ ensures OK;
88 89
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
89 90
             init_invalid : int ) returns ( OK : bool );
90 91
    var exclusive, shared, shared_dirty, dirty, invalid : int;
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff