pw.close();            }            if (resultPw != null )                resultPw.flush();        }    }    private void setInvFlags( GFlaggedInvariant inv,                              Boolean disabled,                              Boolean negated) {        if (disabled!=null)            inv.setDisabled( disabled.booleanValue() );        if (negated!=null)            inv.setNegated( negated.booleanValue() );    }    private List flaggedInvariants( Set names ) {        // if names==null all flaggedInvariants will be returned.        List invs = new ArrayList();        if (names.isEmpty())            invs = new ArrayList(fGModel.flaggedInvariants());        else {            Iterator it = names.iterator();            while (it.hasNext()) {                String name = (String) it.next();                GFlaggedInvariant inv = fGModel.getFlaggedInvariant(name);                if (inv != null)                    invs.add(inv);                else                    Log.error("Invariant `" + name + "' does not exist. " +                               "Ignoring `" + name + "'.");            }        }        return invs;    }    public List flaggedInvariants() {        List invs = new ArrayList( fGModel.flaggedInvariants() );        return invs;        }    public GFlaggedInvariant flaggedInvariant (String name) {        GFlaggedInvariant inv = null;        inv = fGModel.getFlaggedInvariant(name);        if (inv == null) {            Log.error("Invariant `" + name + "' does not exist. " +                      "Ignoring `" + name + "'.");        }        return inv;    }      public void setInvariantFlags( Set names,                                   Boolean disabled,                                   Boolean negated ) {        Iterator it = flaggedInvariants(names).iterator();        while (it.hasNext())            setInvFlags((GFlaggedInvariant) it.next(), disabled, negated);    }    public void printInvariantFlags( Set names ) {        boolean found = false;        if (!names.isEmpty())            System.out.println(                               "Listing only invariants given as parameter...");            List flInvs = flaggedInvariants(names);        System.out.println("- disabled class invariants:");        Iterator disIt = flInvs.iterator();        while (disIt.hasNext()) {            GFlaggedInvariant flaggedInv = (GFlaggedInvariant) disIt.next();            if (flaggedInv.disabled()) {                System.out.println(flaggedInv.classInvariant().toString()+" "                                   + (flaggedInv.negated() ? "(negated)" : "" ));                found = true;            }        }        if (!found)            System.out.println("(none)");        found = false;        System.out.println("- enabled class invariants:");        Iterator enIt = flInvs.iterator();        while (enIt.hasNext()) {            GFlaggedInvariant flaggedInv = (GFlaggedInvariant) enIt.next();            if (!flaggedInv.disabled()) {                System.out.println(flaggedInv.classInvariant().toString()+" "                                   + (flaggedInv.negated() ? "(negated)" : "" ));                found = true;            }        }        if (!found)            System.out.println("(none)");    }        public void printResult(PrintWriter pw) throws GNoResultException {        pw.println("Random number generator was "                    + "initialized with " + lastResult().randomNr() + ".");        pw.println("Checked " + lastResult().collector().numberOfCheckedStates() + " snapshots.");        if (lastResult().collector().limit() != Long.MAX_VALUE)            pw.println("Limit was set to " + lastResult().collector().limit() + "." );        if (!lastResult().collector().validStateFound() )            pw.println("Result: No valid state found.");        else {            pw.println("Result: Valid state found.");            pw.println("Commands to produce the valid state:");            Iterator it = lastResult().collector().commands().iterator();            while (it.hasNext())                pw.println( ((MCmd) it.next()).getUSEcmd() );            if (lastResult().collector().commands().isEmpty())                pw.println("(none)");        }    }        public void printResultStatistics() throws GNoResultException {        PrintWriter pw = new PrintWriter(System.out);        lastResult().checker().printStatistics(pw);        pw.flush();    }        public void acceptResult() throws GNoResultException {        if (!lastResult().collector().validStateFound() )            System.out.println("No commands available.");        else {            try {                Iterator it = lastResult().collector().commands().iterator();                while (it.hasNext())                    fSystem.executeCmd((MCmd) it.next());                System.out.println(                                   "Generated result (system state) accepted.");            } catch (MSystemException e) {                Log.error(e.getMessage());            }        }    }    public void loadInvariants( String filename, boolean doEcho ) {        Collection addedInvs = null;        try {            addedInvs = USECompiler.compileAndAddInvariants(                                                            fGModel,                                                            new BufferedReader(new FileReader(filename)),                                                            filename,                                                            new PrintWriter(System.err) );        } catch (FileNotFoundException e) {            Log.error( e.getMessage() );        }        if (addedInvs != null && doEcho) {            System.out.println("Added invariants:");            Iterator it = addedInvs.iterator();            while (it.hasNext())                System.out.println( ((MClassInvariant) it.next()).toString() );            if (addedInvs.isEmpty())                System.out.println("(none)");        }    }    public void unloadInvariants(Set pNames) {        Set names = new TreeSet(pNames);        if (names.isEmpty()) {            Iterator invIt = fGModel.loadedClassInvariants().iterator();            while (invIt.hasNext()) {                MClassInvariant inv = (MClassInvariant) invIt.next();                names.add( inv.cls().name() + "::" + inv.name() );            }        }            Iterator nameIt = names.iterator();        while (nameIt.hasNext()) {            String name = (String) nameIt.next();            if (fGModel.removeClassInvariant(name) == null )                Log.error("Invariant `" + name + "' does not exist or is " +                          "an invariant of the original model. Ignoring.");        }    }        public void printLoadedInvariants() {        MMVisitor v = new MMPrintVisitor(new PrintWriter(System.out, true));        Collection loadedInvs = fGModel.loadedClassInvariants();        Iterator it = loadedInvs.iterator();        while (it.hasNext())            ((MClassInvariant) it.next()).processWithVisitor(v);        if (loadedInvs.isEmpty())            System.out.println("(no loaded invariants)");    }    private GResult lastResult() throws GNoResultException {        if (fLastResult==null)            throw new GNoResultException();        else            return fLastResult;    }        public boolean hasResult() {        return fLastResult != null;    }    public MSystem system() {        return fSystem;    }}