package verifier;
import java.io.*;
import java.util.*;
/************************************
*
* This class verifies the combination proof of bad small components.
*
* It proves the following statement:
* Every breakpoint graph containing bad small components
* whose total size is >= 8 cycles has an (11,8) sequence.
*
* The bad small components are:
* Unoriented Interleaving pair: [3](0 4 2)[3](1 5 3)
* Unoriented Necklace of size 4: [3](1 5 3)[3](4 8 6)[3](7 11 9)[3](10 2 0)
* Twisted Necklace of size 4: [3](5 0 7)[3](2 6 4)[3](3 10 8)[3](9 1 11)
* Unoriented Necklace of size 5: [3](3 7 5)[3](0 4 2)[3](6 10 8)[3](9 13 11)[3](12 1 14)
* Unoriented Necklace of size 6: [3](13 17 15)[3](10 14 12)[3](7 11 9)[3](16 2 0)[3](1 5 3)[3](4 8 6)
*
* The verification procedes as follows:
* 1. FOR EACH of the bad small components
* VERIFY(comp, proof_file_for_comp)
*
* 2. VERIFY(configuration conf)
* IF conf has >= 8 cycles
* give sorting for conf IF NO SORTING EXISTS ERROR
* ELSE
* FOR EACH position i in the conf
* FOR EACH bad small comp
* VERIFY(conf addComponent comp to position i, proof_file)
*/
public class VerifyCOMBINATIONProof extends BaseClass {
private static Configuration BADSMALLCOMPS[] = new Configuration[5];
public static void main(String args[]){
try {
Configuration necklace_6 = new Configuration("[3](13 17 15)[3](10 14 12)[3](7 11 9)[3](16 2 0)[3](1 5 3)[3](4 8 6)");
BADSMALLCOMPS[0] = necklace_6;
Configuration necklace_5 = new Configuration("[3](3 7 5)[3](0 4 2)[3](6 10 8)[3](9 13 11)[3](12 1 14)");
BADSMALLCOMPS[1] = necklace_5;
Configuration necklace_4 = new Configuration("[3](1 5 3)[3](4 8 6)[3](7 11 9)[3](10 2 0)");
BADSMALLCOMPS[2] = necklace_4;
Configuration twistedneck_4 = new Configuration("[3](5 0 7)[3](2 6 4)[3](3 10 8)[3](9 1 11)");
BADSMALLCOMPS[3] = twistedneck_4;
Configuration interleaving_pair = new Configuration("[3](0 4 2)[3](1 5 3)");
BADSMALLCOMPS[4] = interleaving_pair;
if ( ! VERIFY(necklace_6,"[3](0_16_2)[3](1_5_3)[3](4_8_6)[3](7_11_9)[3](10_14_12)[3](13_17_15).html") )
System.exit(1);
if ( ! VERIFY(necklace_5, "[3](0_4_2)[3](1_14_12)[3](3_7_5)[3](6_10_8)[3](9_13_11).html") )
System.exit(1);
if ( ! VERIFY(necklace_4, "[3](0_10_2)[3](1_5_3)[3](4_8_6)[3](7_11_9).html") )
System.exit(1);
if ( ! VERIFY(twistedneck_4, "[3](0_7_5)[3](1_11_9)[3](2_6_4)[3](3_10_8).html") )
System.exit(1);
if ( ! VERIFY(interleaving_pair, "[3](0_4_2)[3](1_5_3).html") )
System.exit(1);
}
catch(IOException exc){
exc.printStackTrace();
}
System.out.println();
System.out.println("proof verified");
System.out.println("checkedFiles: " + checkedFiles.size());
}
// The file names of the files that have been verified
// with respect to the configuration inside the file.
private static HashSet checkedFiles = new HashSet();
/************************************
* VERIFY FILE
* Verify that the file is a correct sorting file
* or extension file.
*/
static int filesVerfied = 0;
private static boolean VERIFY(Configuration conf, String fileName) throws IOException{
DEBUG("VERIFYING " + fileName);
BufferedReader in
= new BufferedReader(new FileReader("comb_files/"+fileName));
//The first three lines of all files are:
//
//[3](1_5_3)[3](4_8_6)[3](7_11_9).jpeg)
//Configuration numBE = 12 numOCy = 4 hVal = 1251911397
//[3](1 5 3)[3](4 8 6)[3](7 11 9)[3](10 2 0)
in.readLine();//skip the header
in.readLine();//skip the image line
in.readLine();//skip the conf info
Configuration readConf = new Configuration(in.readLine());
//check that the read configuration is the same as the one we are verifying
if ( !readConf.equals(conf) ){
stackTrace();
printERR("The read configuration is not the same as the one that should be in this file");
printERR("readConf: " + readConf);
printERR("inputConf: " + conf);
return false;
}
//If the file already has been check (we can follow a link to this file many times)
if ( checkedFiles.contains(fileName) ){
in.close();
return true;
}
checkedFiles.add(fileName);
// There are three types of files and the rest of the lines in the file are as follows:
//1. Extension files that look like:
//
// EXTENSIONS
//2. Sorting files that look like:
//
// SORTING
//3. File with subset of components that have >= 8 components look like this:
//
// SUBSET EXISTS
in.readLine();
String l = in.readLine();
boolean correct;
if ( l.indexOf("SORTING") != -1 )
correct = verifySortingFile(conf, in,fileName);
else if ( l.indexOf("EXTENSIONS") != -1 )
correct = verifyExtensionFile(conf, in, fileName);
else if ( l.indexOf("SUBSET") != -1 )
correct = verifySubcompExistsFile(conf,in,fileName);
else {
stackTrace();
printERR(" unexpected line: " + l );
correct = false;
}
in.close();
if ( ! correct ){
printERR("There was an error in the file");
printERR(fileName);
}
else{
filesVerfied++;
System.out.print("files verified = " + filesVerfied +"\r");
System.out.flush();
}
return correct;
}
/**********************************
* VERIFY SORTING FILE
* This method is called from VERIFY()
* Some lines have allready been read.
* So the file looks like this:
* Configuration numBE = 30 numOCy = 10 hVal = 34904901
* [3](24 28 26)[3](27 1 29)[3](0 4 2)[3](3 25 23)[3](18 ....
* 0: a = 0 b = 2 c = 5 move_type = 0
* Configuration numBE = 9 numOCy = 3 hVal = 461256
* [3](4 7 2)[3](0 5 3)[3](1 8 6)
* 1: a = 2 b = 4 c = 7 move_type = 2
* Configuration numBE = 9 numOCy = 5 hVal = 1617691
* [1](2)[3](0 3 6)[3](1 8 4)[1](7)[1](5)
* 2: a = 0 b = 3 c = 6 move_type = 2
* Configuration numBE = 9 numOCy = 7 hVal = 656848
* [1](5)[1](0)[3](4 8 1)[1](7)[1](2)[1](6)[1](3)
* 3: a = 1 b = 4 c = 8 move_type = 2
* Configuration numBE = 9 numOCy = 9 hVal = 1888127
* [1](2)[1](0)[1](1)[1](4)[1](6)[1](3)[1](7)[1](8)[1](5)
*
*/
private static boolean verifySortingFile(Configuration conf, BufferedReader in, String fileName) throws IOException{
DEBUG("sorting file: " + fileName);
//skip until first transposition
in.readLine();
in.readLine();
// START VERIFYING THE SORTING
Configuration currentConf = new Configuration(conf);
int num2moves = 0;
int num0moves = 0;
while ( true ){
//0: a = 0 b = 2 c = 5 move_type = 0
String transLine = in.readLine(); // the transposition
DEBUG(transLine);
if ( transLine.indexOf("