/*
Copyright (C) 1989, 1991 Free Software Foundation, Inc.  
51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA

author: Yuan yongfu  lijin   liyong   lib 511,the College of Mathematics and Computer Science,HuNan Normal University,China

Everyone is permitted to copy and distribute verbatim copies
of this license document, but changing it is not allowed.

*/
package edu.hunnu.webjetchecker.propertytest;

import java.io.File;
import java.io.FileNotFoundException;
import java.io.IOException;
import java.io.RandomAccessFile;
import java.util.StringTokenizer;

import edu.hunnu.webjetchecker.MyFile;
import edu.hunnu.webjetchecker.config.Config;
import edu.hunnu.webjetchecker.convert.Bpel2Pi;
import edu.hunnu.webjetchecker.convert.Bpel2RemarkPi;
import edu.hunnu.webjetchecker.convert.Remark_Pi2Bpel;
import edu.hunnu.webjetchecker.convert.pi2RemarkPi;

public class Bisimulation extends PropertyExamine {

    private String specPi = null;

    private String appliPi = null;

    private File specFile = null;

    private File appliFile = null;

    public Bisimulation() {

    }

    public Bisimulation(File specFile, File appliFile) { // 該構(gòu)造函數(shù)對(duì)傳入的兩個(gè)文件進(jìn)行相應(yīng)的轉(zhuǎn)化，表示成Pi表達(dá)式。

        try { // 先判斷規(guī)范文件屬于哪種類型：bpel ? pi表達(dá)式？
            RandomAccessFile tempFile = new RandomAccessFile(specFile, "r");
            try {// 根據(jù)選擇的文件的前若干個(gè)字符判斷該規(guī)范文件是否bpel或pi表達(dá)式，并對(duì)相應(yīng)的標(biāo)志進(jìn)行更新
                if (tempFile.readLine().indexOf("agent") == -1)
                    ((MyFile) specFile).setFileIsBpel(true);
                else
                    ((MyFile) specFile).setFileIsPi(true);

                tempFile.close();

            } catch (IOException e1) {
                // TODO Auto-generated catch block
                e1.printStackTrace();
            }
        } catch (FileNotFoundException e0) {
            e0.printStackTrace();
        }

        try {
            RandomAccessFile tempFile = new RandomAccessFile(specFile, "r");
            try {
                if (((MyFile) specFile).getFileIsBpel()) {// 如果該文件是Bpel，則分別將該文件的帶注釋的Pi演算表達(dá)式和不帶注釋的Pi表達(dá)式存入其對(duì)象中
                    ((MyFile) specFile).setRemarkPi(new Bpel2RemarkPi(specFile)
                            .getResult());
                    ((MyFile) specFile).setBarePi(new Bpel2Pi(specFile)
                            .getResult());
                } else {
                    String str = "";
                    tempFile.seek(0);
                    String s = "";
                    s = tempFile.readLine();
                    while (s != null) {
                        str += s;
                        s = tempFile.readLine();
                    }
                    ((MyFile) specFile).setBarePi(str);// 如果該文件是Pi表達(dá)式，則將該文件的作為整個(gè)表達(dá)式存入其中
                }
            } catch (IOException e1) {
                // TODO Auto-generated catch block
                e1.printStackTrace();
            }
            try {
                tempFile.close();
            } catch (IOException e2) {
                // TODO Auto-generated catch block
                e2.printStackTrace();
            }
        } catch (FileNotFoundException e0) {
            e0.printStackTrace();
        }

        // 將實(shí)施文件的帶注釋Pi表達(dá)式和不帶注釋的Pi表達(dá)式分別存入其對(duì)應(yīng)的文件對(duì)象中
        ((MyFile) appliFile).setRemarkPi(new Bpel2RemarkPi(appliFile)
                .getResult().replace('P', 'Q'));
        ((MyFile) appliFile).setBarePi(new Bpel2Pi(appliFile).getResult()
                .replace('P', 'Q'));

        // 分別將規(guī)范和實(shí)施文件的不帶注釋的Pi表達(dá)式格式化顯示到工具界面的相應(yīng)位置上！
        final String pi_expression_Spec = ((MyFile) specFile).getBarePi(); // 取得規(guī)范文件的不帶注釋的Pi表達(dá)式
        String strTemp = "";

        int noTemp = pi_expression_Spec.length();
        for (int i = 0; i < (noTemp / 200); i++) {
            for (int j = i * 200; j < (i + 1) * 200; j++) {
                strTemp += pi_expression_Spec.substring(j, j + 1);
            }
            strTemp = strTemp + "\n";
        }
        if (noTemp / 200 * 200 != noTemp) {
            for (int i = (noTemp / 200) * 200; i < noTemp; i++) {
                strTemp += pi_expression_Spec.substring(i, i + 1);
            }
        }
        setSpecPi(strTemp);

        final String pi_expression_Appl = ((MyFile) appliFile).getBarePi(); // 獲得實(shí)施文件不帶注釋的Pi表達(dá)式

        strTemp = "";
        noTemp = pi_expression_Appl.length();
        for (int i = 0; i < (noTemp / 200); i++) {
            for (int j = i * 200; j < (i + 1) * 200; j++) {
                strTemp += pi_expression_Appl.substring(j, j + 1);
            }
            strTemp = strTemp + "\n";
        }
        if (noTemp / 200 * 200 != noTemp) {
            for (int i = (noTemp / 200) * 200; i < noTemp; i++) {
                strTemp += pi_expression_Appl.substring(i, i + 1);
            }
        }

        setAppliPi(strTemp);

        this.specFile = specFile;
        this.appliFile = appliFile;

    }

    public int execute() {
        /***********************************************************************
         * 返回0表示該互模擬結(jié)果為兩個(gè)文件不互模擬 返回1，表示該互模擬結(jié)果為兩個(gè)文件互模擬 返回2，表示互模擬檢驗(yàn)出錯(cuò)
         * 返回3，表示在執(zhí)行互模擬過(guò)程中，將BPEL文件轉(zhuǎn)化為Pi演算時(shí)出錯(cuò)，未將Pi表達(dá)式及相關(guān)命令寫(xiě)入到sml目錄下的commands.txt中
         * 返回4，表明捕獲讀寫(xiě)異常 返回5，表示進(jìn)程P,Q至少有一個(gè)為空 返回6，表示詞法有誤
         */
        String expSpec = ((MyFile) specFile).getBarePi();
        String expAppli = ((MyFile) appliFile).getBarePi();

        String command = "";
        command = expSpec + "\n";
        command += expAppli + "\n";
        command += "eq P Q" + "\n";

        if (command.equals(""))
            return 3;// 返回3，表示在執(zhí)行互模擬過(guò)程中，將BPEL文件轉(zhuǎn)化為Pi演算時(shí)出錯(cuò)，未將Pi表達(dá)式及相關(guān)命令寫(xiě)入到sml目錄下的commands.txt中
        else { // 執(zhí)行互模擬檢驗(yàn)
            this.propertyTest(command);
            String str = null;
            //
            // 通過(guò)配置文件找到mwb的位置
            //
            Config config = new Config();
            String path = config.getMwb_path();
            File file = new File(path + "\\bisimulation");
            try {
                str = this.readLine(file); // vcbvbvcbvbvbvcbvbvbvcbvcbvcbvcbvcbvcbvc
            } catch (IOException e1) {
                // TODO Auto-generated catch block
                e1.printStackTrace();
                return 4; // 返回4，表明捕獲讀寫(xiě)異常
            }
            if (str == null)
                return 2; // 返回2，表示互模擬檢驗(yàn)出錯(cuò)
            else if (str.trim().equalsIgnoreCase("bisimulation")) {
                return 1; // 表示該互模擬結(jié)果為兩個(gè)文件互模擬
            } else {
                StringTokenizer stringTokenizer = new StringTokenizer(str, "&");
                int tokenCount = stringTokenizer.countTokens();
                String tempP = "", tempQ = "";
                if (tokenCount == 3) {
                    tempP = stringTokenizer.nextToken();
                    tempQ = stringTokenizer.nextToken();
                    if (!tempP.equals("") && !tempQ.equals("")) {

                        tempP = handleStr(tempP);
                        tempQ = handleStr(tempQ);
                        if (((MyFile) specFile).getFileIsBpel()) {
                            pi2RemarkPi p2r_p = new pi2RemarkPi(tempP, specFile);
                            String p_RemarkPi = p2r_p.getResult();

                            Remark_Pi2Bpel rp = new Remark_Pi2Bpel(specFile);
                            rp.pi2Bpel(p_RemarkPi, 0);
                        }

                        tempQ = tempQ.replace('Q', 'P');
                        pi2RemarkPi p2r_q = new pi2RemarkPi(tempQ, appliFile);
                        String q_RemarkPi = p2r_q.getResult();
                        Remark_Pi2Bpel rq = new Remark_Pi2Bpel(appliFile);
                        rq.pi2Bpel(q_RemarkPi, 0);

                        return 0;// 表示該互模擬結(jié)果為兩個(gè)文件不互模擬
                    } else
                        return 5;// 表示進(jìn)程P,Q至少有一個(gè)為空

                }
                return 6;// 詞法有誤

            }
        }
    }

    public void setSpecPi(String str) {
        this.specPi = str;
    }

    public void setAppliPi(String str) {
        this.appliPi = str;
    }

    public String getSpecPi() {
        return this.specPi;
    }

    public String getAppliPi() {
        return this.appliPi;
    }

    public String readLine(File file) throws IOException {
        String str = "";
        RandomAccessFile ra = new RandomAccessFile(file, "r");
        str = ra.readLine();
        return str;
    }

    public String handleStr(String str) {
        int length = str.length();
        int begin, end;
        // first, remove the restrict names (\,\,\,...)
        if (str.indexOf("(\\") > -1) {
            begin = str.indexOf("(\\");
            end = str.indexOf(")", begin);
            str = str.substring(0, begin) + str.substring(end + 1, length);
        }

        // second,remove the free names (^,^,^...)
        length = str.length();
        if (str.indexOf("(^") > -1) {
            begin = str.indexOf("(^");
            end = str.indexOf(")", begin);
            str = str.substring(0, begin) + str.substring(end + 1, length);
        }

        return str;
    }

}