/* * 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 joebo@informatik.uni-bremen.de.");            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 joebo@informatik.uni-bremen.de.");            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 )