/*
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.IOException;
import java.io.RandomAccessFile;
import java.util.StringTokenizer;

import edu.hunnu.webjetchecker.config.Config;
import edu.hunnu.webjetchecker.convert.Bpel2RemarkPi;

/**
 * @author ly
 * 
 * TODO To change the template for this generated type comment go to Window -
 * Preferences - Java - Code Style - Code Templates
 */
public class Prover extends PropertyExamine {
    private File file = null;

    public Prover(File file) {
        this.file = file;
    }

    // 將不帶注釋的Pi表達式匹配到帶注釋的Pi表達式
    public String pi2RemarkPi() throws IOException {
        Config config = new Config();
        String path = config.getMwb_path();
        RandomAccessFile ra = new RandomAccessFile(path + "\\proveFault", "r");
        long len = ra.length();
        String str = "";
        for (int i = 0; i < len; i++) {
            str = str + ra.readLine();
        }

        StringTokenizer token = new StringTokenizer(str, ".");
        int num = token.countTokens();
        String[] actions = new String[num];
        for (int i = 0; i < num; i++) {
            actions[i] = token.nextToken();
        }
        String head = actions[0];

        if (head.startsWith("("))
            head = head.substring(1);
        if (head.indexOf("(") > 0) {
            head = head.substring(0, head.indexOf("("));
        } else if (head.indexOf("<") > 0)
            head = head.substring(0, head.indexOf("<"));

        String tail = actions[num - 2];
        if (tail.indexOf("(") > 0)
            tail.substring(0, tail.indexOf("("));
        else if (tail.indexOf("<") > 0)
            tail = tail.substring(0, tail.indexOf("<"));

        Bpel2RemarkPi br = new Bpel2RemarkPi(file);
        String strf = br.getResult();

        for (int i = 0; i < 2; i++) {
            strf = strf.substring(strf.indexOf(")") + 1);
        }

        int posHead = strf.indexOf(head); // posHead是開始的動作在帶匹配的Pi演算的表達式中的位置
        int temp0 = posHead;
        temp0 = positionBackward(strf, temp0, 0); // start結束*的位置
        int temp1 = temp0 - 1;
        temp1 = positionBackward(strf, temp1, 0); // start開始*的位置
        int bsPos = startPos(strf, temp1);

        int posTail = strf.indexOf(tail);
        int temp2 = posTail;
        temp2 = positionForward(strf, temp2, 0); // end開始*的位置
        int temp3 = temp2 + 1;
        temp3 = positionForward(strf, temp3, 0); // end結束*的位置

        int bePos = endPos(strf, temp2);
        int eePos = positionForward(strf, bePos + 1, 0);
        String result = strf.substring(bsPos - 1, eePos + 2);

        return result;
    }

    // positionBackward向后尋找*的位置,
    private static int positionBackward(String str, int i, int j) {
        int cons = i + 1;
        while (!str.substring(i, i + 1).equals("*")) {
            if (i == 0) { // 已經找到字符串頂端,則匹配最后一個找到的*
                i = cons;
                break;
            } else if (str.substring(i, i + 1).equals(".") && j != 0) { // 當遇到字符"."后返回最后匹配的*,第一次匹配時忽略"."
                while (!str.substring(i, i + 1).equals("*")) {
                    i = i + 1;
                }
                return i;

            }
            i = i - 1;
        }
        return i;
    }

    // positionForward向前尋找*的位置,
    private static int positionForward(String str, int i, int j) {
        int cons = i - 1;
        while (!str.substring(i, i + 1).equals("*")) {
            if (i == str.length() - 2) { // 已經找到字符串尾端,則匹配最后一個找到的*
                i = cons;
                break;
            } else if (str.substring(i, i + 1).equals(".") && j != 0) { // 當遇到字符"."后返回倒數第二次匹配的*,第一次匹配時忽略"."
                while (!str.substring(i, i + 1).equals("*")) {
                    i = i - 1;
                }
                i = i - 1;
                while (!str.substring(i, i + 1).equals("*")) {
                    i = i - 1;
                }
                return i;
            }
            i = i + 1;
        }
        return i;
    }

    // 方法startPos,返回(*start*)開始的位置,
    private static int startPos(String str, int pos) {
        int cons = pos; // cons記錄初始的start的*位置
        pos = positionBackward(str, positionBackward(str, pos - 1, 1) - 1, 1);
        if (pos == cons) { // 如果*的位置沒有發生變化，說明此時的start的位置為最終匹配的位置(中間沒有其他的),返回
            return pos;
        } else if ((str.substring(pos + 1, pos + 2)).equals("s")) { // 如果下一個還是start,則繼續往下找,直到滿足條件
            startPos(str, pos);
        } else {
            pos = positionForward(str, positionForward(str, pos + 1, 1) + 1, 1);// 如果下一個是end,則回溯到前面一個start
        }
        return pos;
    }

    // 方法endPos,返回(*end*)開始的位置
    private static int endPos(String str, int pos) {
        int cons = pos;
        pos = positionForward(str, positionForward(str, pos + 1, 1) + 1, 1);
        if (pos == cons) {
            return pos;
        } else if (str.substring(pos + 1, pos + 2).equals("e")) {
            endPos(str, pos);
        } else
            pos = positionBackward(str, positionBackward(str, pos - 1, 1) - 1,
                    1);
        return pos;
    }

    public String getPiFault() throws IOException {
        Config config = new Config();
        String path = config.getMwb_path();
        RandomAccessFile ra = new RandomAccessFile(path + "\\proveFault", "r");
        long len = ra.length();
        String str = "";
        for (int i = 0; i < len; i++) {
            str = str + ra.readLine();
        }
        return str;

    }
}