bisimulation.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.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) { // 该构造函数对传入的两个文件进行相应的转化，表示成Pi表达式。

        try { // 先判断规范文件属于哪种类型：bpel ? pi表达式？
            RandomAccessFile tempFile = new RandomAccessFile(specFile, "r");
            try {// 根据选择的文件的前若干个字符判断该规范文件是否bpel或pi表达式，并对相应的标志进行更新
                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演算表达式和不带注释的Pi表达式存入其对象中
                    ((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表达式，则将该文件的作为整个表达式存入其中
                }
            } 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();
        }

        // 将实施文件的带注释Pi表达式和不带注释的Pi表达式分别存入其对应的文件对象中
        ((MyFile) appliFile).setRemarkPi(new Bpel2RemarkPi(appliFile)
                .getResult().replace('P', 'Q'));
        ((MyFile) appliFile).setBarePi(new Bpel2Pi(appliFile).getResult()
                .replace('P', 'Q'));

        // 分别将规范和实施文件的不带注释的Pi表达式格式化显示到工具界面的相应位置上！
        final String pi_expression_Spec = ((MyFile) specFile).getBarePi(); // 取得规范文件的不带注释的Pi表达式
        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(); // 获得实施文件不带注释的Pi表达式

        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表示该互模拟结果为两个文件不互模拟 返回1，表示该互模拟结果为两个文件互模拟 返回2，表示互模拟检验出错
         * 返回3，表示在执行互模拟过程中，将BPEL文件转化为Pi演算时出错，未将Pi表达式及相关命令写入到sml目录下的commands.txt中
         * 返回4，表明捕获读写异常 返回5，表示进程P,Q至少有一个为空 返回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，表示在执行互模拟过程中，将BPEL文件转化为Pi演算时出错，未将Pi表达式及相关命令写入到sml目录下的commands.txt中
        else { // 执行互模拟检验
            this.propertyTest(command);
            String str = null;
            //
            // 通过配置文件找到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，表明捕获读写异常
            }
            if (str == null)
                return 2; // 返回2，表示互模拟检验出错
            else if (str.trim().equalsIgnoreCase("bisimulation")) {
                return 1; // 表示该互模拟结果为两个文件互模拟
            } 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;// 表示该互模拟结果为两个文件不互模拟
                    } else
                        return 5;// 表示进程P,Q至少有一个为空

                }
                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;
    }

}