ggenerator.java

UML设计测试工具

/*
 * This is source code of the Snapshot Generator, an extension for USE
 * to generate (valid) system states of UML models.
 * Copyright (C) 2001 Joern Bohling, University of Bremen
 *
 * About USE:
 *   USE - UML based specification environment
 *   Copyright (C) 1999,2000,2001 Mark Richters, University of Bremen
 *
 * This program is free software; you can redistribute it and/or
 * modify it under the terms of the GNU General Public License as
 * published by the Free Software Foundation; either version 2 of the
 * License, or (at your option) any later version.
 *
 * This program is distributed in the hope that it will be useful, but
 * WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 * General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with this program; if not, write to the Free Software
 * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
 */

package org.tzi.use.gen.tool;

import org.tzi.use.uml.mm.MClassInvariant;
import org.tzi.use.uml.mm.MMVisitor;
import org.tzi.use.uml.mm.MMPrintVisitor;
import org.tzi.use.gen.model.GModel;
import org.tzi.use.gen.assl.statics.GProcedure;
import org.tzi.use.gen.assl.dynamics.GEvalProcedure;
import org.tzi.use.gen.assl.dynamics.GEvaluationException;
import org.tzi.use.gen.model.GFlaggedInvariant;
import org.tzi.use.parser.USECompiler;
import org.tzi.use.uml.sys.MCmd;
import org.tzi.use.uml.sys.MSystem;
import org.tzi.use.uml.sys.MSystemException;
import org.tzi.use.util.Log;
import org.tzi.use.config.Options;
import java.util.Set;
import java.util.TreeSet;
import java.util.List;
import java.util.ArrayList;
import java.util.Iterator;
import java.util.Collection;
import java.util.Random;
import java.io.*;


/**
 * Provides operations called by the <code>GGeneratorShell</code>.
 * Knows the modified <code>GModel</code>, the current <code>MSystem</code>
 * and the last <code>GResult</code>.
 * @author  Joern Bohling
 */
public class GGenerator {
    private GModel fGModel;
    private MSystem fSystem;
    private GResult fLastResult;

    public GGenerator( MSystem system ) {
        fSystem = system;
        fGModel = new GModel(system.model());
        fLastResult = null;
    }

    private void internalError(GEvaluationException e, long randomNr) {
        String nl = Options.LINE_SEPARATOR;
        try {
            PrintWriter pw
                = new PrintWriter(new FileWriter("generator_error.txt"));
            pw.println("Program version: " + Options.RELEASE_VERSION);
            pw.println("Project version: " + Options.PROJECT_VERSION);
            pw.println("Stack trace: ");
            e.printStackTrace(pw);
            pw.close();
            System.err.println("THE GENERATOR HAS AN INTERNAL ERROR." + nl +
                               "PLEASE SEND THE FILE `generator_error.txt'"+nl+
                               "TO [e-mail].");
            System.err.println("The random number generator was " 
                               + "initialized with " + randomNr + ".");
        } catch (IOException ioException) {
            System.err.println("THE GENERATOR HAS AN INTERNAL ERROR." + nl +
                               "PLEASE SEND THE FOLLOWING INFORMATION "+nl+
                               "TO [e-mail].");
            System.err.println("Program version: " + Options.RELEASE_VERSION);
            System.err.println("Project version: " + Options.PROJECT_VERSION);
            System.err.println("Stack trace: ");
            e.printStackTrace();
        }
    }

    public void startProcedure( String filename,
                                String callstr,
                                Long limit,
                                String printFilename,
                                boolean printBasics,
                                boolean printDetails,
                                Long randomNr,
                                boolean checkStructure ) {
        fLastResult = null;

        if (randomNr == null)
            randomNr = new Long( (new Random()).nextInt(10000) );
        if (limit == null)
            limit = new Long( Long.MAX_VALUE );

        List procedures = null;
        GProcedureCall call = null;
        PrintWriter pw = null;
        PrintWriter resultPw = null;

        try {
            Log.verbose("Compiling procedures from " + filename + ".");
            procedures=USECompiler.compileProcedures(
                                                     fSystem.model(),
                                                     new BufferedReader(new FileReader(filename)),
                                                     filename,
                                                     new PrintWriter(System.err) );
            if (procedures!=null) {
                Log.verbose("Compiling `" + callstr + "'.");
                call = USECompiler.compileProcedureCall(fSystem.model(),
                                                        fSystem.state(),
                                                        new StringReader(callstr),
                                                        "<input>",
                                                        new PrintWriter(System.err)
                                                        );
            }
            if (call!=null && procedures!=null) {
                GProcedure proc = call.findMatching( procedures );
                if (proc == null)
                    Log.error( call.signatureString()
                               + " not found in " + filename );
                else {
                    resultPw = new PrintWriter(System.out);
                    if (printFilename==null)
                        pw = resultPw;
                    else
                        pw = new PrintWriter(
                                             new BufferedWriter(new FileWriter(printFilename)));

                    GCollectorImpl collector = new GCollectorImpl();
                    collector.setLimit(limit.longValue());
                    if (printBasics || printDetails)
                        collector.setBasicPrintWriter(pw);
                    if (printDetails)
                        collector.setDetailPrintWriter(pw);

                    GChecker checker = new GChecker(fGModel, checkStructure);

                    Log.verbose(proc.toString() + " started...");

                    try {
                        GEvalProcedure evalproc = new GEvalProcedure( proc );
                        evalproc.eval(call.evaluateParams(fSystem.state()),
                                      fSystem.state(),
                                      collector,
                                      checker,
                                      randomNr.longValue());
                        fLastResult = new GResult( collector,
                                                   checker,
                                                   randomNr.longValue());
                        if (collector.existsInvalidMessage())
                            pw.println("There were errors." + (
                                                               (!printBasics && !printDetails)
                                                               ?
                                                               " Use the -b or -d option to get "+
                                                               "further information."
                                                               :
                                                               " See output " + 
                                                               ( printFilename!=null ? "("+printFilename+") " : "" ) +
                                                               "for details."
                                                               ) );
                        try {
                            if (Log.isVerbose())
                                printResult(resultPw);
                        } catch (GNoResultException e) {
                            throw new RuntimeException(
                                                       "Although the generator computed a result, it"
                                                       + "is not available for printing." );
                        }                  
                    } catch (GEvaluationException e) {
                        internalError(e, randomNr.longValue());
                        Log.error("The system state may be changed in use.");
                    } catch (StackOverflowError ex) {
                        Log.error("Evaluation aborted because of a stack " +
                                  "overflow error. Maybe there were too many "+
                                  "elements in a sequence of a for-loop.");
                        Log.error("The system state may be changed in use.");
                    }
                }
            }
        } catch (FileNotFoundException e) {
            Log.error( e.getMessage() );
        } catch (IOException e) {
            Log.error( e.getMessage() );
        } finally {
            if (pw != null ) {
                pw.flush();
                if (printFilename != null )