prover.java

这是我们参加06年全国开源软件的竞赛作品

/*
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;

    }
}