heuristic_grouping.pl

benchmark_group(invariant,'scheduler_err.mch','SchedulerErr').

benchmark_group(invariant,'Simpson_Four_Slot_CSP.mch','Simpson4Slot').

benchmark_group(invariant,'Peterson_err.mch','Peterson_err').

benchmark_group(invariant,'CarlaTravelAgencyErr.mch','TravelAgency').

benchmark_group(invariant,'M21_err3_mch.eventb','SecureBldg_M21_err3').

benchmark_group(invariant,'m2_err.ref','Abrial_Press_m2_err').

benchmark_group(invariant,'m_partner_behaviour.eventb','SAP_M_Partner').

benchmark_group(invariant,'pkeyprot.mch','Needham-Schroeder').

benchmark_group(invariant,'dfcheck_houseset_simpler.mch','HousesetSimpler').

benchmark_group(invariant,'NastyCoin.mch','NastyCoin').

benchmark_group(invariant,'BreadthFirstTest.mch','BFTest').

benchmark_group(invariant,'DepthFirstTest.mch','DFTest1').

benchmark_group(invariant,'DepthFirstTest2.mch','DFTest2').

benchmark_group(deadlock,'earley_3_v3.mch','Abrial_Earley3_v3').

benchmark_group(deadlock,'earley_3_v5.mch','Abrial_Earley3_v5').

benchmark_group(deadlock,'earley_4_v3.mch','Abrial_Earley4_v3').

benchmark_group(deadlock,'axl3_deadlock.mch','Alstom_axl3').

benchmark_group(deadlock,'exemple7.mch','Alstom_ex7').

benchmark_group(deadlock,'CrsCtl_m2.eventb','Bosch_CrsCtl').

benchmark_group(deadlock,'mchoreography.eventb','SAP_MChoreography').

benchmark_group(deadlock,'Dining_With_Protocol_in_B.mch','DiningPhil').

benchmark_group(deadlock,'cxcc0.eventb','CXCC0').

benchmark_group(goal,'RussianPostalPuzzle.mch','RussianPostal').

benchmark_group(goal,'TrainTorchPuzzle.mch','TrainTorch').

benchmark_group(goal,'BlocksWorldGeneric.mch','BlocksWorld').

benchmark_group(goal,'Farmer.mch','Farmer').

benchmark_group(goal,'Hanoi.mch','Hanoi').

benchmark_group(goal,'Puzzle8_difficult.mch','Puzzle8').

benchmark_group(goal,'RushHour.mch','RushHour').

benchmark_group(goal,'m13.ref','Abrial_Press_m13').

benchmark_group(goal,'m1.ref','Abrial_Queue_m1').

benchmark_group(goal,'Router.mch','SystemOnChip_Router').

benchmark_group(goal,'Wegenetz.mch','Wegenetz').

benchmark_group(noerror,'scheduler1.ref','Scheduler1').

benchmark_group(noerror,'Cruise_finite1.mch','Volvo_Cruise').

benchmark_group(noerror,'USB_4Endpoints.mch','USB4').

benchmark_group(noerror,'nota.mch','Nokia_Nota').

benchmark_group(noerror,'HuffmanM_mch.eventb','Huffman').

benchmark_group(noerror,'cont3.ref','Cansell_Contention').

benchmark_group(noerror,'ModeleGS_R1.ref','Demoney_GS_R1').

benchmark_group(noerror,'Router1.mch','SystemOnChip_Router').

benchmark_group(noerror,'mondex_m2.eventb','Mondex_m2').

benchmark_group(noerror,'mondex_m3.eventb','Mondex_m3').

benchmark_group(noerror,'siemens_mch_0.eventb','Siemens_ATP0').

benchmark_group(noerror,'obsw_M001.eventb','SSF_obsw1').

benchmark_group(noerror,'elevator12.eventb','ETH_Elevator12').

benchmark_group(noerror,'EchoAlg.mch','Echo').

Determinacy Checker

Determinacy Checker:

* Non-determinate: user:benchmark_group/3 (clause 1)
* Indexing cannot distinguish this from clause 2.
* Non-determinate: user:benchmark_group/3 (clause 2)
* Indexing cannot distinguish this from clause 3.
* Non-determinate: user:benchmark_group/3 (clause 3)
* Indexing cannot distinguish this from clause 4.
* Non-determinate: user:benchmark_group/3 (clause 4)
* Indexing cannot distinguish this from clause 5.
* Non-determinate: user:benchmark_group/3 (clause 5)
* Indexing cannot distinguish this from clause 6.
* Non-determinate: user:benchmark_group/3 (clause 6)
* Indexing cannot distinguish this from clause 7.
* Non-determinate: user:benchmark_group/3 (clause 7)
* Indexing cannot distinguish this from clause 8.
* Non-determinate: user:benchmark_group/3 (clause 8)
* Indexing cannot distinguish this from clause 9.
* Non-determinate: user:benchmark_group/3 (clause 9)
* Indexing cannot distinguish this from clause 10.
* Non-determinate: user:benchmark_group/3 (clause 10)
* Indexing cannot distinguish this from clause 11.
* Non-determinate: user:benchmark_group/3 (clause 11)
* Indexing cannot distinguish this from clause 12.
* Non-determinate: user:benchmark_group/3 (clause 12)
* Indexing cannot distinguish this from clause 13.
* Non-determinate: user:benchmark_group/3 (clause 14)
* Indexing cannot distinguish this from clause 15.
* Non-determinate: user:benchmark_group/3 (clause 15)
* Indexing cannot distinguish this from clause 16.
* Non-determinate: user:benchmark_group/3 (clause 16)
* Indexing cannot distinguish this from clause 17.
* Non-determinate: user:benchmark_group/3 (clause 17)
* Indexing cannot distinguish this from clause 18.
* Non-determinate: user:benchmark_group/3 (clause 18)
* Indexing cannot distinguish this from clause 19.
* Non-determinate: user:benchmark_group/3 (clause 19)
* Indexing cannot distinguish this from clause 20.
* Non-determinate: user:benchmark_group/3 (clause 20)
* Indexing cannot distinguish this from clause 21.
* Non-determinate: user:benchmark_group/3 (clause 21)
* Indexing cannot distinguish this from clause 22.
* Non-determinate: user:benchmark_group/3 (clause 23)
* Indexing cannot distinguish this from clause 24.
* Non-determinate: user:benchmark_group/3 (clause 24)
* Indexing cannot distinguish this from clause 25.
* Non-determinate: user:benchmark_group/3 (clause 25)
* Indexing cannot distinguish this from clause 26.
* Non-determinate: user:benchmark_group/3 (clause 26)
* Indexing cannot distinguish this from clause 27.
* Non-determinate: user:benchmark_group/3 (clause 27)
* Indexing cannot distinguish this from clause 28.
* Non-determinate: user:benchmark_group/3 (clause 28)
* Indexing cannot distinguish this from clause 29.
* Non-determinate: user:benchmark_group/3 (clause 29)
* Indexing cannot distinguish this from clause 30.
* Non-determinate: user:benchmark_group/3 (clause 30)
* Indexing cannot distinguish this from clause 31.
* Non-determinate: user:benchmark_group/3 (clause 31)
* Indexing cannot distinguish this from clause 32.
* Non-determinate: user:benchmark_group/3 (clause 32)
* Indexing cannot distinguish this from clause 33.
* Non-determinate: user:benchmark_group/3 (clause 34)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: user:benchmark_group/3 (clause 35)
* Indexing cannot distinguish this from clause 36.
* Non-determinate: user:benchmark_group/3 (clause 36)
* Indexing cannot distinguish this from clause 37.
* Non-determinate: user:benchmark_group/3 (clause 37)
* Indexing cannot distinguish this from clause 38.
* Non-determinate: user:benchmark_group/3 (clause 38)
* Indexing cannot distinguish this from clause 39.
* Non-determinate: user:benchmark_group/3 (clause 39)
* Indexing cannot distinguish this from clause 40.
* Non-determinate: user:benchmark_group/3 (clause 40)
* Indexing cannot distinguish this from clause 41.
* Non-determinate: user:benchmark_group/3 (clause 41)
* Indexing cannot distinguish this from clause 42.
* Non-determinate: user:benchmark_group/3 (clause 42)
* Indexing cannot distinguish this from clause 43.
* Non-determinate: user:benchmark_group/3 (clause 43)
* Indexing cannot distinguish this from clause 44.
* Non-determinate: user:benchmark_group/3 (clause 44)
* Indexing cannot distinguish this from clause 45.
* Non-determinate: user:benchmark_group/3 (clause 45)
* Indexing cannot distinguish this from clause 46.
* Non-determinate: user:benchmark_group/3 (clause 46)
* Indexing cannot distinguish this from clause 47.