shell.java

UML设计测试工具

        fStepMode = true;
        Log.println("Step mode turned on.");
    }

    /**
     * Undoes the last object manipulation command.
     */
    private void cmdUndo() throws NoSystemException {
        MSystem system = system();
        try {
            system.undoCmd();
        } catch (MSystemException ex) {
            Log.error(ex.getMessage());
        }
    }

    /**
     * Prints commands executed so far.
     */
    private void cmdWrite(String filename) throws NoSystemException {
        MSystem system = system();
        PrintWriter out = null;
        try {
            if (filename == null)
                out = new PrintWriter(System.out);
            else {
                out = new PrintWriter(new BufferedWriter(new FileWriter(
                        filename)));
            }
            out
                    .println("-- Script generated by USE "
                            + Options.RELEASE_VERSION);
            out.println();
            system.writeUSEcmds(out);
        } catch (IOException ex) {
            Log.error(ex.getMessage());
        } finally {
            if (out != null) {
                out.flush();
                if (filename != null)
                    out.close();
            }
        }
    }

    //***********************************************************
    // Generator Commands
    //***********************************************************

    /**
     *  
     */
    private void cmdGenLoadInvariants(String str, MSystem system, boolean doEcho) {
        String filename = str.trim();
        if (filename.length() == 0)
            Log.error("syntax is `load FILE'");
        else
            system.generator().loadInvariants(str.trim(), doEcho);
    }

    /**
     *  
     */
    private void cmdGenUnloadInvariants(String str, MSystem system) {
        StringTokenizer st = new StringTokenizer(str);
        Set names = new TreeSet();
        try {
            while (st.hasMoreTokens())
                names.add(st.nextToken());
            system.generator().unloadInvariants(names);
        } catch (NoSuchElementException e) {
            Log.error("syntax is `unload [invnames]'");
        }
    }

    private void cmdGenPrintLoadedInvariants(MSystem system) {
        system.generator().printLoadedInvariants();
    }

    private void cmdGenResult(String str, MSystem system) {
        str = str.trim();
        try {
            if (str.length() == 0) {
                PrintWriter pw = new PrintWriter(System.out);
                system.generator().printResult(pw);
                pw.flush();
            } else if (str.equals("inv"))
                system.generator().printResultStatistics();
            else if (str.equals("accept"))
                system.generator().acceptResult();
            else
                Log.error("Unknown command `result " + str + "'. Try help.");
        } catch (GNoResultException e) {
            Log.error("No result available.");
        }
    }

    /**
     *  
     */
    private void cmdGenInvariantFlags(String str, MSystem system) {
        // Syntax: gen flags (invariant)* [+d|-d] [+n|-n]
        StringTokenizer st = new StringTokenizer(str);
        Set names = new TreeSet();
        Boolean disabled = null;
        Boolean negated = null;
        boolean error = false;
        boolean optionDetected = false;
        String tok = null;

        try {
            while (st.hasMoreTokens() && !optionDetected) {
                tok = st.nextToken();
                if (tok.startsWith("+") || tok.startsWith("-"))
                    optionDetected = true;
                else
                    names.add(tok);
            }
            while (optionDetected && !error) {
                if (tok.equals("+d") || tok.equals("-d")) {
                    if (disabled != null)
                        error = true;
                    else if (tok.equals("+d"))
                        disabled = Boolean.TRUE;
                    else
                        disabled = Boolean.FALSE;

                } else if (tok.equals("+n") || tok.equals("-n")) {
                    if (negated != null)
                        error = true;
                    else if (tok.equals("+n"))
                        negated = Boolean.TRUE;
                    else
                        negated = Boolean.FALSE;
                } else
                    error = true;
                if (st.hasMoreTokens())
                    tok = st.nextToken();
                else
                    optionDetected = false;
            }
        } catch (NoSuchElementException e) {
            error = true;
        }
        if (error)
            Log.error("syntax is `flags [invnames] ((+d|-d) | (+n|-n))'");
        else if (disabled == null && negated == null)
            system.generator().printInvariantFlags(names);
        else
            system.generator().setInvariantFlags(names, disabled, negated);
    }

    /**
     *  
     */
    private void cmdGenStartProcedure(String str, MSystem system) {
        String filename = null; // the file which contains procedures
        String callstr = null; // the call of the procedure
        Long limit = null; // default: no limit
        boolean printBasics = false; // print flow of control (to understand)
        boolean printDetails = false; // print flow of control in detail
        String printFilename = null; // null-> prints to System.out
        Long randomNr = null; // null-> choose a random number

        StringTokenizer st = new StringTokenizer(str);
        boolean allOptionsFound = false;
        boolean error = false;
        boolean limitOptionFound = false;
        boolean outputOptionFound = false;
        boolean randomOptionFound = false;
        boolean checkStructure = true;
        String message = null;

        try {
            while (!allOptionsFound && !error) {
                String optionOrFilename = st.nextToken();
                if (optionOrFilename.equals("-s")) {
                    if (!checkStructure)
                        error = true;
                    else
                        checkStructure = false;
                } else if (optionOrFilename.equals("-r")) {
                    if (randomOptionFound)
                        error = true;
                    else {
                        try {
                            randomNr = new Long(st.nextToken());
                        } catch (NumberFormatException e) {
                            error = true;
                        }
                        error = error || (randomNr.longValue() <= 0);
                        if (error)
                            message = "the parameter of the -r"
                                    + " option must be a positive number"
                                    + " (< 2^63).";
                    }
                    randomOptionFound = true;
                } else if (optionOrFilename.equals("-l")) {
                    if (limitOptionFound)
                        error = true;
                    else {
                        try {
                            limit = new Long(st.nextToken());
                        } catch (NumberFormatException e) {
                            error = true;
                        }
                        error = error || (limit.longValue() <= 0);
                        if (error)
                            message = "the parameter of the -l"
                                    + " option must be a positive number"
                                    + " (< 2^63).";
                    }
                    limitOptionFound = true;
                } else if (optionOrFilename.equals("-b")
                        || optionOrFilename.equals("-d")
                        || optionOrFilename.equals("-bf")
                        || optionOrFilename.equals("-df")) {
                    // an output option
                    if (outputOptionFound)
                        error = true;
                    else if (optionOrFilename.equals("-b"))
                        printBasics = true;
                    else if (optionOrFilename.equals("-d"))
                        printDetails = true;
                    else if (optionOrFilename.equals("-bf")) {
                        printBasics = true;
                        printFilename = st.nextToken();
                    } else if (optionOrFilename.equals("-df")) {
                        printDetails = true;
                        printFilename = st.nextToken();
                    }
                    outputOptionFound = true;
                } else {
                    // optionOrFilename must be a filename
                    if (optionOrFilename.startsWith("-"))
                        error = true;
                    else {
                        allOptionsFound = true;
                        filename = optionOrFilename;
                        callstr = st.nextToken("");
                    }
                }
            }
        } catch (NoSuchElementException e) {
            error = true;
        }

        if (error) {
            if (message != null)
                Log.error(message);
            else {
                Log.error("syntax is `start [-l <num>][-r <num>]"
                        + "[-b|-d|-bf <FILE>|-df <FILE>] "
                        + "FILE PROCNAME([paramlist])'");
            }
            return;
        }

        //System.out.println(filename);
        //System.out.println(callstr);
        //System.out.println("limit:"+limit);
        //System.out.println("printBasics:"+printBasics);
        //System.out.println("printDetails:"+printDetails);
        //System.out.println("printFilename:"+printFilename);

        system.generator().startProcedure(filename, callstr, limit,
                printFilename, printBasics, printDetails, randomNr,
                checkStructure);

    }

    private MSystem system() throws NoSystemException {
        if (!fSession.hasSystem())
            throw new NoSystemException();
        return fSession.system();
    }

    //***********************************************************
    // Method for deferring Read-Commands
    //***********************************************************
    private String getFirstWordOfFile(String filename) {
        try {
            String result = "";
            BufferedReader bf = new BufferedReader(new FileReader(filename));
            boolean isComment = false;
            boolean noCase = false;
            boolean cont = false;

            for (String line = bf.readLine(); line != null; line = bf
                    .readLine()) {
                line = line.trim();
                while (!noCase) {
                    noCase = true;
                    if (line.startsWith("--")) {
                        noCase = true;
                        cont = true;
                        continue;
                    }
                    if (line.startsWith("/*")) {
                        noCase = false;
                        isComment = true;
                        line = line.substring(line.indexOf("/*") + 2).trim();
                    }
                    if (isComment == true) {
                        noCase = false;
                        int index = line.indexOf("*/");
                        if (index != -1) {
                            line = line.substring(index + 2).trim();
                            isComment = false;
                        }
                        if (index == -1) {
                            noCase = true;
                            cont = true;
                            continue;
                        }
                    }
                }
                if (cont || line.trim().equals("")) {
                    cont = false;
                    noCase = false;
                    continue;
                }
                StringTokenizer st = new StringTokenizer(line);
                result = st.nextToken();
                return result;
            }
        } catch (FileNotFoundException e) {
            // ignored
            Log.println("Error: File `" + filename + "' could not be found!");
            return "ERROR: -1";
        } catch (IOException e) {
            // ignored
        }
        return null;
    }

}