---

BUI.java

package edu.ksu.cis.bandera.bui;

/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
 * Bandera, a Java(TM) analysis and transformation toolkit           *
 * Copyright (C) 2000   Robby (robby@cis.ksu.edu)                    *
 * All rights reserved.                                              *
 *                                                                   *
 * This work was done as a project in the SAnToS Laboratory,         *
 * Department of Computing and Information Sciences, Kansas State    *
 * University, USA (http://www.cis.ksu.edu/santos).                  *
 * It is understood that any modification not identified as such is  *
 * not covered by the preceding statement.                           *
 *                                                                   *
 * This work is free software; you can redistribute it and/or        *
 * modify it under the terms of the GNU Library General Public       *
 * License as published by the Free Software Foundation; either      *
 * version 2 of the License, or (at your option) any later version.  *
 *                                                                   *
 * This work 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 *
 * Library General Public License for more details.                  *
 *                                                                   *
 * You should have received a copy of the GNU Library General Public *
 * License along with this toolkit; if not, write to the             *
 * Free Software Foundation, Inc., 59 Temple Place - Suite 330,      *
 * Boston, MA  02111-1307, USA.                                      *
 *                                                                   *
 * Java is a trademark of Sun Microsystems, Inc.                     *
 *                                                                   *
 * To submit a bug report, send a comment, or get the latest news on *
 * this project and other SAnToS projects, please visit the web-site *
 *                http://www.cis.ksu.edu/santos                      *
 * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
import javax.swing.tree.*;
import java.io.*;
import java.util.*;
import java.awt.event.*;
import javax.swing.*;
import edu.ksu.cis.bandera.bui.session.*;
import edu.ksu.cis.bandera.bui.session.datastructure.*;
import edu.ksu.cis.bandera.jjjc.*;
import edu.ksu.cis.bandera.specification.datastructure.*;
import edu.ksu.cis.bandera.specification.assertion.datastructure.*;
import edu.ksu.cis.bandera.specification.predicate.datastructure.*;
import edu.ksu.cis.bandera.abstraction.*;
import edu.ksu.cis.bandera.abstraction.gui.*;
import edu.ksu.cis.bandera.pdgslicer.dependency.*;
public class BUI extends JFrame {
    public static BUI bui;
    public static Sessions sessions = new Sessions();
    public static Property property = new Property();
    public static SessionManager manager;
    static PatternManager patternManager;
    static PredicateBrowser predicateBrowser;
    static AssertionBrowser assertionBrowser;
    public static BUISessionPane sessionPane;
    public static PropertyManager propertyManager;
    static AbstractionLibraryManager abstractionLibraryManager;
    public static TypeGUI typeGUI;
    public static SpinOption spinOption;
    public static IROptions irOptions;
    static DSpinOption dSpinOption;
    static JPFOption jpfOption;
    static boolean doJJJC = true;
    static boolean doSlicer = false;
    static boolean doSLABS = false;
    static boolean doChecker = false;
    public static boolean isExecuting = false;
    public static String originalUserDir = System.getProperty("user.dir");
    private JPanel ivjBUIContentPane = null;
    private JMenuBar ivjBUIJMenuBar = null;
    private JMenuItem ivjExitMenuItem = null;
    private JSeparator ivjJSeparator1 = null;
    private JMenuItem ivjNewMenuItem = null;
    private JMenuItem ivjOpenMenuItem = null;
    private JMenuItem ivjSaveAsMenuItem = null;
    private JMenuItem ivjSaveMenuItem = null;
    private JToolBar ivjBUIToolBar = null;
    private JButton ivjRunToolBarButton = null;
    private JButton ivjJ3CToolBarButton = null;
    private JButton ivjSlicerToolBarButton = null;
    private JButton ivjBircToolBarButton = null;
    private JButton ivjABPSToolBarButton = null;
    private JLabel ivjBanderaLabel = null;
    private JMenuItem ivjPropertyManagerMenuItem = null;
    private JMenu ivjSpecificationMenu = null;
    private JMenuItem ivjAbstractionManagerMenuItem = null;
    private JMenu ivjAbstractionMenu = null;
    private JPanel ivjBottomPanel = null;
    private JMenuItem ivjAboutMenuItem = null;
    private JMenu ivjHelpMenu = null;
    private JSeparator ivjJSeparator2 = null;
    private JButton ivjSeparator1ToolBarButton = null;
    private JMenu ivjSessionMenu = null;
    private JSeparator ivjJSeparator4 = null;
    private JMenuItem ivjManagerMenuItem = null;
    private JMenuItem ivjPatternManagerMenuItem = null;
    private JMenuItem ivjPredicateBrowserMenuItem = null;
    private JMenuItem ivjAssertionBrowserMenuItem = null;
    IvjEventHandler ivjEventHandler = new IvjEventHandler();
    private JButton ivjNewToolBarButton = null;
    private JButton ivjSeparator1ToolBarButton1 = null;
    private JButton ivjOpenToolBarButton = null;
    private JButton ivjSaveAsToolBarButton = null;
    private JButton ivjSaveToolBarButton = null;
    private JButton ivjAssertionToolBarButton = null;
    private JToolBar ivjBUIMiddleToolBar = null;
    private JPanel ivjBUIMiddleToolbarPanel = null;
    private JPanel ivjBUIToolbarPanel = null;
    private JPanel ivjBUITopToolbarPanel = null;
    private JButton ivjPatternToolBarButton = null;
    private JButton ivjPredicateToolBarButton = null;
    private JButton ivjPropertyToolBarButton = null;
    private JButton ivjSeparator1ToolBarButton11 = null;
    private JButton ivjSeparator1ToolBarButton111 = null;
    private JButton ivjSessionToolBarButton = null;
    private JButton ivjDependToolBarButton = null;
    private JButton ivjAbstractionToolBarButton = null;
    private JButton ivjSeparator1ToolBarButton1111 = null;
    private JPanel ivjCheckerPanel = null;
    private JLabel ivjJPFLabel = null;
    private JLabel ivjNuSMVLabel = null;
    private JLabel ivjSpinLabel = null;
    private JMenuItem ivjIRMenuItem = null;
    private JSeparator ivjJSeparator3 = null;
    private JMenuItem ivjAbstractionLibraryManagerMenuItem = null;
    private JSeparator ivjJSeparator5 = null;

class IvjEventHandler implements java.awt.event.ActionListener {
        public void actionPerformed(java.awt.event.ActionEvent e) {
            if (e.getSource() == BUI.this.getExitMenuItem()) 
                connEtoC2();
            if (e.getSource() == BUI.this.getManagerMenuItem()) 
                connEtoC1();
            if (e.getSource() == BUI.this.getJ3CToolBarButton()) 
                connEtoC3();
            if (e.getSource() == BUI.this.getSlicerToolBarButton()) 
                connEtoC4();
            if (e.getSource() == BUI.this.getABPSToolBarButton()) 
                connEtoC5();
            if (e.getSource() == BUI.this.getBircToolBarButton()) 
                connEtoC6();
            if (e.getSource() == BUI.this.getRunToolBarButton()) 
                connEtoC7();
            if (e.getSource() == BUI.this.getPatternManagerMenuItem()) 
                connEtoC8();
            if (e.getSource() == BUI.this.getSaveMenuItem()) 
                connEtoC9();
            if (e.getSource() == BUI.this.getSaveAsMenuItem()) 
                connEtoC10();
            if (e.getSource() == BUI.this.getOpenMenuItem()) 
                connEtoC11();
            if (e.getSource() == BUI.this.getNewMenuItem()) 
                connEtoC12();
            if (e.getSource() == BUI.this.getPredicateBrowserMenuItem()) 
                connEtoC13();
            if (e.getSource() == BUI.this.getPropertyManagerMenuItem()) 
                connEtoC14();
            if (e.getSource() == BUI.this.getAbstractionManagerMenuItem()) 
                connEtoC16();
            if (e.getSource() == BUI.this.getAboutMenuItem()) 
                connEtoC17();
            if (e.getSource() == BUI.this.getAssertionBrowserMenuItem()) 
                connEtoC18();
            if (e.getSource() == BUI.this.getSaveToolBarButton()) 
                connEtoC19();
            if (e.getSource() == BUI.this.getSaveAsToolBarButton()) 
                connEtoC20();
            if (e.getSource() == BUI.this.getOpenToolBarButton()) 
                connEtoC21();
            if (e.getSource() == BUI.this.getNewToolBarButton()) 
                connEtoC22();
            if (e.getSource() == BUI.this.getSessionToolBarButton()) 
                connEtoC23();
            if (e.getSource() == BUI.this.getAssertionToolBarButton()) 
                connEtoC24();
            if (e.getSource() == BUI.this.getPredicateToolBarButton()) 
                connEtoC25();
            if (e.getSource() == BUI.this.getPatternToolBarButton()) 
                connEtoC26();
            if (e.getSource() == BUI.this.getPropertyToolBarButton()) 
                connEtoC27();
            if (e.getSource() == BUI.this.getDependToolBarButton()) 
                connEtoC28();
            if (e.getSource() == BUI.this.getAbstractionToolBarButton()) 
                connEtoC15();
            if (e.getSource() == BUI.this.getIRMenuItem()) 
                connEtoC29();
            if (e.getSource() == BUI.this.getAbstractionLibraryManagerMenuItem()) 
                connEtoC30();
        };
    };
/**
 * BUI constructor comment.
 */
public BUI() {
    super();
    initialize();
}
/**
 * Comment
 */
public void aboutMenuItem_ActionEvents() {
    AboutBox box = new AboutBox();
    box.show();
}
/**
 * Comment
 */
public void aBPSToolBarButton_ActionEvents() {
    Icon temp = getABPSToolBarButton().getPressedIcon();
    getABPSToolBarButton().setPressedIcon(getABPSToolBarButton().getIcon());
    getABPSToolBarButton().setIcon(temp);
    doSLABS = !doSLABS;
    try {
        sessions.getActiveSession().setDoSLABS(doSLABS);
        manager.updateInfo(sessions.getActiveSession());
    } catch (Exception e) {}
}
/**
 * Comment
 */
public void abstractionLibraryManagerMenuItem_ActionEvents() {
    abstractionLibraryManager.setVisible(true);
}
/**
 * Comment
 */
public void abstractionManagerMenuItem_ActionEvents() {
    typeGUI.setVisible(true);
}
/**
 * Comment
 */
public void abstractionToolBarButton_ActionEvents() {
    abstractionManagerMenuItem_ActionEvents();
}
/**
 * Comment
 */
public void assertionBrowserMenuItem_ActionEvents() {
    assertionBrowser.setVisible(true);
}
/**
 * Comment
 */
public void assertionToolBarButton_ActionEvents() {
    assertionBrowserMenuItem_ActionEvents();
}
/**
 * Comment
 */
public void bircToolBarButton_ActionEvents() {
    Icon temp = getBircToolBarButton().getPressedIcon();
    getBircToolBarButton().setPressedIcon(getBircToolBarButton().getIcon());
    getBircToolBarButton().setIcon(temp);
    doChecker = !doChecker;
    try {
        sessions.getActiveSession().setDoChecker(doChecker);
        manager.updateInfo(sessions.getActiveSession());
    } catch (Exception e) {}
}
/**
 * 
 * @param sessions edu.ksu.cis.bandera.bui.session.Sessions
 */
private void changeSessions(Sessions sessions) {
    this.sessions = sessions;
    CompilationManager.reset();
    PredicateSet.reset();
    AssertionSet.reset();

    sessionPane.updateLeftTree();
    
    manager.dispose();
    manager = new SessionManager();
    manager.updateSessionManager();
    manager.setVisible(true);
    /*
    f = patternManager.isVisible();
    patternManager.dispose();
    patternManager.setVisible(f);
    */

    PredicateSet.reset();
    AssertionSet.reset();

    assertionBrowser.updateTree();
    predicateBrowser.updateTree();  
    
    boolean f = propertyManager.isVisible();
    propertyManager.dispose();
    propertyManager.setVisible(f);

    jpfOption.setVisible(false);
    jpfOption.dispose();
    spinOption.setVisible(false);
    typeGUI.setFile(null);
}
/**
 * connEtoC1:  (WizardMenuItem.action. --> BUI.wizardMenuItem_ActionEvents()V)
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private void connEtoC1() {
    try {
        // user code begin {1}
        // user code end
        this.managerMenuItem_ActionEvents();
        // user code begin {2}
        // user code end
    } catch (java.lang.Throwable ivjExc) {
        // user code begin {3}
        // user code end
        handleException(ivjExc);
    }
}
/**
 * connEtoC10:  (SaveAsMenuItem.action. --> BUI.saveAsMenuItem_ActionEvents()V)
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private void connEtoC10() {
    try {
        // user code begin {1}
        // user code end
        this.saveAsMenuItem_ActionEvents();
        // user code begin {2}
        // user code end
    } catch (java.lang.Throwable ivjExc) {
        // user code begin {3}
        // user code end
        handleException(ivjExc);
    }
}
/**
 * connEtoC11:  (OpenMenuItem.action. --> BUI.openMenuItem_ActionEvents()V)
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private void connEtoC11() {
    try {
        // user code begin {1}
        // user code end
        this.openMenuItem_ActionEvents();
        // user code begin {2}
        // user code end
    } catch (java.lang.Throwable ivjExc) {
        // user code begin {3}
        // user code end
        handleException(ivjExc);
    }
}
/**
 * connEtoC12:  (NewMenuItem.action. --> BUI.newMenuItem_ActionEvents()V)
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private void connEtoC12() {
    try {
        // user code begin {1}
        // user code end
        this.newMenuItem_ActionEvents();
        // user code begin {2}
        // user code end
    } catch (java.lang.Throwable ivjExc) {
        // user code begin {3}
        // user code end
        handleException(ivjExc);
    }
}
/**
 * connEtoC13:  (PredicateBrowserMenuItem.action. --> BUI.predicateBrowserMenuItem_ActionEvents()V)
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private void connEtoC13() {
    try {
        // user code begin {1}
        // user code end
        this.predicateBrowserMenuItem_ActionEvents();
        // user code begin {2}
        // user code end
    } catch (java.lang.Throwable ivjExc) {
        // user code begin {3}
        // user code end
        handleException(ivjExc);
    }
}
/**
 * connEtoC14:  (PropertyManagerMenuItem.action. --> BUI.propertyManagerMenuItem_ActionEvents()V)
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private void connEtoC14() {
    try {
        // user code begin {1}
        // user code end
        this.propertyManagerMenuItem_ActionEvents();
        // user code begin {2}
        // user code end
    } catch (java.lang.Throwable ivjExc) {
        // user code begin {3}
        // user code end
        handleException(ivjExc);
    }
}
/**
 * connEtoC15:  (TypeInferenceMenuItem.action. --> BUI.typeInferenceMenuItem_ActionEvents()V)
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private void connEtoC15() {
    try {
        // user code begin {1}
        // user code end
        this.abstractionToolBarButton_ActionEvents();
        // user code begin {2}
        // user code end
    } catch (java.lang.Throwable ivjExc) {
        // user code begin {3}
        // user code end
        handleException(ivjExc);
    }
}
/**
 * connEtoC16:  (AbstractionManagerMenuItem.action. --> BUI.abstractionManagerMenuItem_ActionEvents()V)
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private void connEtoC16() {
    try {
        // user code begin {1}
        // user code end
        this.abstractionManagerMenuItem_ActionEvents();
        // user code begin {2}
        // user code end
    } catch (java.lang.Throwable ivjExc) {
        // user code begin {3}
        // user code end
        handleException(ivjExc);
    }
}
/**
 * connEtoC17:  (AboutMenuItem.action. --> BUI.aboutMenuItem_ActionEvents()V)
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private void connEtoC17() {
    try {
        // user code begin {1}
        // user code end
        this.aboutMenuItem_ActionEvents();
        // user code begin {2}
        // user code end
    } catch (java.lang.Throwable ivjExc) {
        // user code begin {3}
        // user code end
        handleException(ivjExc);
    }
}
/**
 * connEtoC18:  (AssertionBrowserMenuItem.action. --> BUI.assertionBrowserMenuItem_ActionEvents()V)
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private void connEtoC18() {
    try {
        // user code begin {1}
        // user code end
        this.assertionBrowserMenuItem_ActionEvents();
        // user code begin {2}
        // user code end
    } catch (java.lang.Throwable ivjExc) {
        // user code begin {3}
        // user code end
        handleException(ivjExc);
    }
}
/**
 * connEtoC19:  (SaveToolBarButton.action. --> BUI.saveToolBarButton_ActionEvents()V)
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private void connEtoC19() {
    try {
        // user code begin {1}
        // user code end
        this.saveToolBarButton_ActionEvents();
        // user code begin {2}
        // user code end
    } catch (java.lang.Throwable ivjExc) {
        // user code begin {3}
        // user code end
        handleException(ivjExc);
    }
}
/**
 * connEtoC2:  (ExitMenuItem.action. --> BUI.exitMenuItem_ActionEvents()V)
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private void connEtoC2() {
    try {
        // user code begin {1}
        // user code end
        this.exitMenuItem_ActionEvents();
        // user code begin {2}
        // user code end
    } catch (java.lang.Throwable ivjExc) {
        // user code begin {3}
        // user code end
        handleException(ivjExc);
    }
}
/**
 * connEtoC20:  (SaveAsToolBarButton.action. --> BUI.saveAsToolBarButton_ActionEvents()V)
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private void connEtoC20() {
    try {
        // user code begin {1}
        // user code end
        this.saveAsToolBarButton_ActionEvents();
        // user code begin {2}
        // user code end
    } catch (java.lang.Throwable ivjExc) {
        // user code begin {3}
        // user code end
        handleException(ivjExc);
    }
}
/**
 * connEtoC21:  (OpenToolBarButton.action. --> BUI.openToolBarButton_ActionEvents()V)
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private void connEtoC21() {
    try {
        // user code begin {1}
        // user code end
        this.openToolBarButton_ActionEvents();
        // user code begin {2}
        // user code end
    } catch (java.lang.Throwable ivjExc) {
        // user code begin {3}
        // user code end
        handleException(ivjExc);
    }
}
/**
 * connEtoC22:  (NewToolBarButton.action. --> BUI.newToolBarButton_ActionEvents()V)
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private void connEtoC22() {
    try {
        // user code begin {1}
        // user code end
        this.newToolBarButton_ActionEvents();
        // user code begin {2}
        // user code end
    } catch (java.lang.Throwable ivjExc) {
        // user code begin {3}
        // user code end
        handleException(ivjExc);
    }
}
/**
 * connEtoC23:  (SessionToolBarButton.action. --> BUI.sessionToolBarButton_ActionEvents()V)
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private void connEtoC23() {
    try {
        // user code begin {1}
        // user code end
        this.sessionToolBarButton_ActionEvents();
        // user code begin {2}
        // user code end
    } catch (java.lang.Throwable ivjExc) {
        // user code begin {3}
        // user code end
        handleException(ivjExc);
    }
}
/**
 * connEtoC24:  (AssertionToolBarButton.action. --> BUI.assertionToolBarButton_ActionEvents()V)
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private void connEtoC24() {
    try {
        // user code begin {1}
        // user code end
        this.assertionToolBarButton_ActionEvents();
        // user code begin {2}
        // user code end
    } catch (java.lang.Throwable ivjExc) {
        // user code begin {3}
        // user code end
        handleException(ivjExc);
    }
}
/**
 * connEtoC25:  (PredicateToolBarButton.action. --> BUI.predicateToolBarButton_ActionEvents()V)
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private void connEtoC25() {
    try {
        // user code begin {1}
        // user code end
        this.predicateToolBarButton_ActionEvents();
        // user code begin {2}
        // user code end
    } catch (java.lang.Throwable ivjExc) {
        // user code begin {3}
        // user code end
        handleException(ivjExc);
    }
}
/**
 * connEtoC26:  (PatternToolBarButton.action. --> BUI.patternToolBarButton_ActionEvents()V)
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private void connEtoC26() {
    try {
        // user code begin {1}
        // user code end
        this.patternToolBarButton_ActionEvents();
        // user code begin {2}
        // user code end
    } catch (java.lang.Throwable ivjExc) {
        // user code begin {3}
        // user code end
        handleException(ivjExc);
    }
}
/**
 * connEtoC27:  (PropertyToolBarButton.action. --> BUI.propertyToolBarButton_ActionEvents()V)
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private void connEtoC27() {
    try {
        // user code begin {1}
        // user code end
        this.propertyToolBarButton_ActionEvents();
        // user code begin {2}
        // user code end
    } catch (java.lang.Throwable ivjExc) {
        // user code begin {3}
        // user code end
        handleException(ivjExc);
    }
}
/**
 * connEtoC28:  (PDGToolBarButton.action. --> BUI.pDGToolBarButton_ActionEvents()V)
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private void connEtoC28() {
    try {
        // user code begin {1}
        // user code end
        this.dependToolBarButton_ActionEvents();
        // user code begin {2}
        // user code end
    } catch (java.lang.Throwable ivjExc) {
        // user code begin {3}
        // user code end
        handleException(ivjExc);
    }
}
/**
 * connEtoC29:  (IRMenuItem.action. --> BUI.iRMenuItem_ActionEvents()V)
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private void connEtoC29() {
    try {
        // user code begin {1}
        // user code end
        this.iRMenuItem_ActionEvents();
        // user code begin {2}
        // user code end
    } catch (java.lang.Throwable ivjExc) {
        // user code begin {3}
        // user code end
        handleException(ivjExc);
    }
}
/**
 * connEtoC3:  (J3CToolBarButton.action. --> BUI.j3CToolBarButton_ActionEvents()V)
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private void connEtoC3() {
    try {
        // user code begin {1}
        // user code end
        this.j3CToolBarButton_ActionEvents();
        // user code begin {2}
        // user code end
    } catch (java.lang.Throwable ivjExc) {
        // user code begin {3}
        // user code end
        handleException(ivjExc);
    }
}
/**
 * connEtoC30:  (AbstractionLibraryManagerMenuItem.action. --> BUI.abstractionLibraryManagerMenuItem_ActionEvents()V)
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private void connEtoC30() {
    try {
        // user code begin {1}
        // user code end
        this.abstractionLibraryManagerMenuItem_ActionEvents();
        // user code begin {2}
        // user code end
    } catch (java.lang.Throwable ivjExc) {
        // user code begin {3}
        // user code end
        handleException(ivjExc);
    }
}
/**
 * connEtoC4:  (SlicerToolBarButton.action. --> BUI.slicerToolBarButton_ActionEvents()V)
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private void connEtoC4() {
    try {
        // user code begin {1}
        // user code end
        this.slicerToolBarButton_ActionEvents();
        // user code begin {2}
        // user code end
    } catch (java.lang.Throwable ivjExc) {
        // user code begin {3}
        // user code end
        handleException(ivjExc);
    }
}
/**
 * connEtoC5:  (ABPSToolBarButton.action. --> BUI.aBPSToolBarButton_ActionEvents()V)
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private void connEtoC5() {
    try {
        // user code begin {1}
        // user code end
        this.aBPSToolBarButton_ActionEvents();
        // user code begin {2}
        // user code end
    } catch (java.lang.Throwable ivjExc) {
        // user code begin {3}
        // user code end
        handleException(ivjExc);
    }
}
/**
 * connEtoC6:  (BircToolBarButton.action. --> BUI.bircToolBarButton_ActionEvents()V)
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private void connEtoC6() {
    try {
        // user code begin {1}
        // user code end
        this.bircToolBarButton_ActionEvents();
        // user code begin {2}
        // user code end
    } catch (java.lang.Throwable ivjExc) {
        // user code begin {3}
        // user code end
        handleException(ivjExc);
    }
}
/**
 * connEtoC7:  (RunToolBarButton.action. --> BUI.runToolBarButton_ActionEvents()V)
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private void connEtoC7() {
    try {
        // user code begin {1}
        // user code end
        this.runToolBarButton_ActionEvents();
        // user code begin {2}
        // user code end
    } catch (java.lang.Throwable ivjExc) {
        // user code begin {3}
        // user code end
        handleException(ivjExc);
    }
}
/**
 * connEtoC8:  (PatternManagerMenuItem.action. --> BUI.patternManagerMenuItem_ActionEvents()V)
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private void connEtoC8() {
    try {
        // user code begin {1}
        // user code end
        this.patternManagerMenuItem_ActionEvents();
        // user code begin {2}
        // user code end
    } catch (java.lang.Throwable ivjExc) {
        // user code begin {3}
        // user code end
        handleException(ivjExc);
    }
}
/**
 * connEtoC9:  (SaveMenuItem.action. --> BUI.saveMenuItem_ActionEvents()V)
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private void connEtoC9() {
    try {
        // user code begin {1}
        // user code end
        this.saveMenuItem_ActionEvents();
        // user code begin {2}
        // user code end
    } catch (java.lang.Throwable ivjExc) {
        // user code begin {3}
        // user code end
        handleException(ivjExc);
    }
}
/**
 * Comment
 */
public void dependToolBarButton_ActionEvents() {
        if (Dependencies.dependFrame != null)
            Dependencies.dependFrame.dispose();
        
        Dependencies.dependFrame = null;
        Dependencies.dependFrame = new Dependencies();
        Dependencies.dependFrame.show();
     /*else
        if (!Dependencies.dependFrame.isVisible())
            Dependencies.dependFrame.setVisible(true);*/
/*
    Object leftTreeUsrObj = null;
    DefaultMutableTreeNode leftTreeSelectedNode = (DefaultMutableTreeNode) BUI.sessionPane.getLeftTree().getLastSelectedPathComponent();
    if (leftTreeSelectedNode != null)
        leftTreeUsrObj = ((DefaultMutableTreeNode) leftTreeSelectedNode).getUserObject();
    Object rightTreeUsrObj = null;
    Object rightTreeSelectedNode = BUI.sessionPane.getRightTree().getLastSelectedPathComponent();
    if (rightTreeSelectedNode != null)
        rightTreeUsrObj = ((DefaultMutableTreeNode) rightTreeSelectedNode).getUserObject();
    DependencyFrame dependFrame = new DependencyFrame(leftTreeUsrObj, rightTreeUsrObj);
    dependFrame.show();
    */
}
/**
 * Comment
 */
public void exitMenuItem_ActionEvents() {
    System.exit(0);
}
/**
 * Return the AboutMenuItem property value.
 * @return javax.swing.JMenuItem
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JMenuItem getAboutMenuItem() {
    if (ivjAboutMenuItem == null) {
        try {
            ivjAboutMenuItem = new javax.swing.JMenuItem();
            ivjAboutMenuItem.setName("AboutMenuItem");
            ivjAboutMenuItem.setMnemonic('a');
            ivjAboutMenuItem.setText("About");
            ivjAboutMenuItem.setBackground(new java.awt.Color(204,204,255));
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjAboutMenuItem;
}
/**
 * Return the ABPSToolBarButton property value.
 * @return javax.swing.JButton
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JButton getABPSToolBarButton() {
    if (ivjABPSToolBarButton == null) {
        try {
            ivjABPSToolBarButton = new javax.swing.JButton();
            ivjABPSToolBarButton.setName("ABPSToolBarButton");
            ivjABPSToolBarButton.setToolTipText("SLABS");
            ivjABPSToolBarButton.setHorizontalTextPosition(javax.swing.SwingConstants.CENTER);
            ivjABPSToolBarButton.setMargin(new java.awt.Insets(0, 0, 0, 0));
            ivjABPSToolBarButton.setPressedIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/SlabsSelected24.gif")));
            ivjABPSToolBarButton.setMinimumSize(new java.awt.Dimension(65, 50));
            ivjABPSToolBarButton.setBorder(new javax.swing.border.CompoundBorder());
            ivjABPSToolBarButton.setText("  SLABS  ");
            ivjABPSToolBarButton.setBackground(new java.awt.Color(204,204,255));
            ivjABPSToolBarButton.setMaximumSize(new java.awt.Dimension(65, 50));
            ivjABPSToolBarButton.setVerticalTextPosition(javax.swing.SwingConstants.BOTTOM);
            ivjABPSToolBarButton.setIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/Slabs24.gif")));
            ivjABPSToolBarButton.setPreferredSize(new java.awt.Dimension(65, 50));
            ivjABPSToolBarButton.setFont(new java.awt.Font("dialog", 0, 10));
            ivjABPSToolBarButton.setEnabled(true);
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjABPSToolBarButton;
}
/**
 * Return the AbstractionLibraryManagerMenuItem property value.
 * @return javax.swing.JMenuItem
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JMenuItem getAbstractionLibraryManagerMenuItem() {
    if (ivjAbstractionLibraryManagerMenuItem == null) {
        try {
            ivjAbstractionLibraryManagerMenuItem = new javax.swing.JMenuItem();
            ivjAbstractionLibraryManagerMenuItem.setName("AbstractionLibraryManagerMenuItem");
            ivjAbstractionLibraryManagerMenuItem.setMnemonic('a');
            ivjAbstractionLibraryManagerMenuItem.setText("Abstraction Library Manager");
            ivjAbstractionLibraryManagerMenuItem.setBackground(new java.awt.Color(204,204,255));
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjAbstractionLibraryManagerMenuItem;
}
/**
 * Return the AbstractionManagerMenuItem property value.
 * @return javax.swing.JMenuItem
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JMenuItem getAbstractionManagerMenuItem() {
    if (ivjAbstractionManagerMenuItem == null) {
        try {
            ivjAbstractionManagerMenuItem = new javax.swing.JMenuItem();
            ivjAbstractionManagerMenuItem.setName("AbstractionManagerMenuItem");
            ivjAbstractionManagerMenuItem.setMnemonic('t');
            ivjAbstractionManagerMenuItem.setText("Typer");
            ivjAbstractionManagerMenuItem.setBackground(new java.awt.Color(204,204,255));
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjAbstractionManagerMenuItem;
}
/**
 * Return the AbstractionMenu property value.
 * @return javax.swing.JMenu
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JMenu getAbstractionMenu() {
    if (ivjAbstractionMenu == null) {
        try {
            ivjAbstractionMenu = new javax.swing.JMenu();
            ivjAbstractionMenu.setName("AbstractionMenu");
            ivjAbstractionMenu.setMnemonic('a');
            ivjAbstractionMenu.setText("Abstraction");
            ivjAbstractionMenu.setBackground(new java.awt.Color(204,204,255));
            ivjAbstractionMenu.add(getAbstractionLibraryManagerMenuItem());
            ivjAbstractionMenu.add(getJSeparator5());
            ivjAbstractionMenu.add(getAbstractionManagerMenuItem());
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjAbstractionMenu;
}
/**
 * Return the AbstractionToolBarButton property value.
 * @return javax.swing.JButton
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JButton getAbstractionToolBarButton() {
    if (ivjAbstractionToolBarButton == null) {
        try {
            ivjAbstractionToolBarButton = new javax.swing.JButton();
            ivjAbstractionToolBarButton.setName("AbstractionToolBarButton");
            ivjAbstractionToolBarButton.setToolTipText("Type Inference");
            ivjAbstractionToolBarButton.setHorizontalTextPosition(javax.swing.SwingConstants.CENTER);
            ivjAbstractionToolBarButton.setMargin(new java.awt.Insets(0, 0, 0, 0));
            ivjAbstractionToolBarButton.setPressedIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/Abstraction24.gif")));
            ivjAbstractionToolBarButton.setMinimumSize(new java.awt.Dimension(65, 50));
            ivjAbstractionToolBarButton.setBorder(new javax.swing.border.CompoundBorder());
            ivjAbstractionToolBarButton.setText("  Typer   ");
            ivjAbstractionToolBarButton.setBackground(new java.awt.Color(204,204,255));
            ivjAbstractionToolBarButton.setMaximumSize(new java.awt.Dimension(65, 50));
            ivjAbstractionToolBarButton.setVerticalTextPosition(javax.swing.SwingConstants.BOTTOM);
            ivjAbstractionToolBarButton.setIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/Abstraction24.gif")));
            ivjAbstractionToolBarButton.setPreferredSize(new java.awt.Dimension(65, 50));
            ivjAbstractionToolBarButton.setFont(new java.awt.Font("dialog", 0, 10));
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjAbstractionToolBarButton;
}
/**
 * Return the AssertionBrowserMenuItem property value.
 * @return javax.swing.JMenuItem
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JMenuItem getAssertionBrowserMenuItem() {
    if (ivjAssertionBrowserMenuItem == null) {
        try {
            ivjAssertionBrowserMenuItem = new javax.swing.JMenuItem();
            ivjAssertionBrowserMenuItem.setName("AssertionBrowserMenuItem");
            ivjAssertionBrowserMenuItem.setMnemonic('a');
            ivjAssertionBrowserMenuItem.setText("Assertion Browser");
            ivjAssertionBrowserMenuItem.setBackground(new java.awt.Color(204,204,255));
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjAssertionBrowserMenuItem;
}
/**
 * Return the AssertionToolBarButton property value.
 * @return javax.swing.JButton
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JButton getAssertionToolBarButton() {
    if (ivjAssertionToolBarButton == null) {
        try {
            ivjAssertionToolBarButton = new javax.swing.JButton();
            ivjAssertionToolBarButton.setName("AssertionToolBarButton");
            ivjAssertionToolBarButton.setToolTipText("Assertion Browser");
            ivjAssertionToolBarButton.setHorizontalTextPosition(javax.swing.SwingConstants.CENTER);
            ivjAssertionToolBarButton.setMargin(new java.awt.Insets(0, 0, 0, 0));
            ivjAssertionToolBarButton.setPressedIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/Assertion24.gif")));
            ivjAssertionToolBarButton.setMinimumSize(new java.awt.Dimension(65, 50));
            ivjAssertionToolBarButton.setBorder(new javax.swing.border.CompoundBorder());
            ivjAssertionToolBarButton.setText("  Assertion  ");
            ivjAssertionToolBarButton.setBackground(new java.awt.Color(204,204,255));
            ivjAssertionToolBarButton.setMaximumSize(new java.awt.Dimension(65, 50));
            ivjAssertionToolBarButton.setVerticalTextPosition(javax.swing.SwingConstants.BOTTOM);
            ivjAssertionToolBarButton.setIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/Assertion24.gif")));
            ivjAssertionToolBarButton.setPreferredSize(new java.awt.Dimension(65, 50));
            ivjAssertionToolBarButton.setFont(new java.awt.Font("dialog", 0, 10));
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjAssertionToolBarButton;
}
/**
 * Return the JLabel1 property value.
 * @return javax.swing.JLabel
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JLabel getBanderaLabel() {
    if (ivjBanderaLabel == null) {
        try {
            ivjBanderaLabel = new javax.swing.JLabel();
            ivjBanderaLabel.setName("BanderaLabel");
            ivjBanderaLabel.setIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/bandera.gif")));
            ivjBanderaLabel.setFont(new java.awt.Font("serif.bold", 1, 48));
            ivjBanderaLabel.setText("");
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjBanderaLabel;
}
/**
 * Return the BircToolBarButton property value.
 * @return javax.swing.JButton
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JButton getBircToolBarButton() {
    if (ivjBircToolBarButton == null) {
        try {
            ivjBircToolBarButton = new javax.swing.JButton();
            ivjBircToolBarButton.setName("BircToolBarButton");
            ivjBircToolBarButton.setToolTipText("Checker");
            ivjBircToolBarButton.setHorizontalTextPosition(javax.swing.SwingConstants.CENTER);
            ivjBircToolBarButton.setMargin(new java.awt.Insets(0, 0, 0, 0));
            ivjBircToolBarButton.setPressedIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/CheckerSelected24.gif")));
            ivjBircToolBarButton.setMinimumSize(new java.awt.Dimension(65, 50));
            ivjBircToolBarButton.setBorder(new javax.swing.border.CompoundBorder());
            ivjBircToolBarButton.setText("  Checker  ");
            ivjBircToolBarButton.setBackground(new java.awt.Color(204,204,255));
            ivjBircToolBarButton.setMaximumSize(new java.awt.Dimension(65, 50));
            ivjBircToolBarButton.setDisabledIcon(null);
            ivjBircToolBarButton.setVerticalTextPosition(javax.swing.SwingConstants.BOTTOM);
            ivjBircToolBarButton.setIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/Checker24.gif")));
            ivjBircToolBarButton.setPreferredSize(new java.awt.Dimension(65, 50));
            ivjBircToolBarButton.setFont(new java.awt.Font("dialog", 0, 10));
            ivjBircToolBarButton.setEnabled(true);
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjBircToolBarButton;
}
/**
 * Return the JPanel1 property value.
 * @return javax.swing.JPanel
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JPanel getBottomPanel() {
    if (ivjBottomPanel == null) {
        try {
            ivjBottomPanel = new javax.swing.JPanel();
            ivjBottomPanel.setName("BottomPanel");
            ivjBottomPanel.setBorder(new javax.swing.border.EtchedBorder());
            ivjBottomPanel.setLayout(new java.awt.BorderLayout());
            ivjBottomPanel.setBackground(new java.awt.Color(204,204,255));
            getBottomPanel().add(getBanderaLabel(), "East");
            getBottomPanel().add(getCheckerPanel(), "West");
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjBottomPanel;
}
/**
 * Return the BUIContentPane property value.
 * @return javax.swing.JPanel
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JPanel getBUIContentPane() {
    if (ivjBUIContentPane == null) {
        try {
            ivjBUIContentPane = new javax.swing.JPanel();
            ivjBUIContentPane.setName("BUIContentPane");
            ivjBUIContentPane.setBorder(new javax.swing.border.EtchedBorder());
            ivjBUIContentPane.setLayout(new java.awt.BorderLayout());
            ivjBUIContentPane.setBackground(new java.awt.Color(204,204,255));
            ivjBUIContentPane.setVisible(true);
            getBUIContentPane().add(getBottomPanel(), "South");
            getBUIContentPane().add(getBUIToolbarPanel(), "North");
            // user code begin {1}
            getBUIContentPane().add(sessionPane, "Center");
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjBUIContentPane;
}
/**
 * Return the BUIJMenuBar property value.
 * @return javax.swing.JMenuBar
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JMenuBar getBUIJMenuBar() {
    if (ivjBUIJMenuBar == null) {
        try {
            ivjBUIJMenuBar = new javax.swing.JMenuBar();
            ivjBUIJMenuBar.setName("BUIJMenuBar");
            ivjBUIJMenuBar.setBorder(new javax.swing.border.EtchedBorder());
            ivjBUIJMenuBar.setBackground(new java.awt.Color(204,204,255));
            ivjBUIJMenuBar.add(getSessionMenu());
            ivjBUIJMenuBar.add(getSpecificationMenu());
            ivjBUIJMenuBar.add(getAbstractionMenu());
            ivjBUIJMenuBar.add(getHelpMenu());
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjBUIJMenuBar;
}
/**
 * 
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private static void getBuilderData() {
/*V1.1
**start of data**
    D0CB838494G88G88GE503CAA9GGGGGGGGGGGG8CGGGE2F5E9ECE4E5F2A0E4E1F4E16C3D8FDCD4D57ABF6EEE34CB3BD4D4D414D4D4D4D434CBC53B3451A7AAF62316ED2925168ADBAA37285816B6EAE917F6C74502C443C2A523C4C545C4C4C5C5C5C5C5C5C5C5C5C5980101991D51918886C5C57DBD671C7BBC774E3DF71899BEDFF87DDE5F5757576BF1F85E671C67F94EB94F79F34FB977DCC37E2C60096346679B8C63A69A24FF2B46998CE10F0CB3ACCAF9EE8FE25955569C03625FEC20
    2906B74FE441EF8104A57D4B1613E7686E49863E94782C5F59F2E6405FDF99DE1C98F7A988F421A784424E04FC786260FA3665221E4FB8BFFEFBAE7CCE81AA872C81A898A84FB0F3FB01047783BFC57A1B51387186C375C696E77F5A8285BED60A178FE1A5C0E3F91C955B8B25F0DF06B179709B31D1440D03DFE1648FFBAA25F8D159579AFC16CD9CBF1969D248C7AA5DA45256CB3FC5067BF8C1CCB05C194772D8D5FF6258FA0B392F6CC4EFDFD9072D372C5D54E93674184A5A7BECEB56ECBA309D62C4EFE236
    1DD91B4D5301ED4057EDE6587BEBD9F9E4415F05C0951B513E77F6D5C97A5B7EF61B217A55A9AE6D735FAC6C0A58AC5B17F8693759669AA63F0517B7CB178E61250089DB6E5C0E36045620AD1F4FE5F113014FE0E937A07E9C47CB002F86EA5C02B63E3E81ED34DB6FB4E415FFB57E8B97B6F6EF913685EE11ED0CBA75ED76575CA7DE1D4C6AB58142B200F237DAF34A016A013A013E613EF8C56E77703B315D31396B64492E4E0D5D5D1B6C661EDDDDE60B9D7EDE3386C2A4EC1F25232B47ECB088FF3B3036D447
    9EA45F2D4E3E46C8646D10817DA3F07CE8C3602C6F46CF54491B7968876302A49961DB653CF5EFE365B6E69DAB37F840D93A1D2C9CB8BEE9BD43A3364938282BFFF2DFE0FCC32DB5A7FC8716F3C0895A12FB75D50628E37F9977190EAD5DCF4D9C1F3BCB58D03CCB36C514F164972C0C6B81378379G8581C581A56D42B2CE4CDD6E2E0C37F7BAACBD1DA67B7E3E76EED30FE3D31F4D8E3EAE1535F97BE0E52DC7A2DD0F5769C43904AED756D141A363476B150BFF54147199D2F9646D164BC5683E57256E725DDA
    5F18C2F5F80137091A5D228EA7906E4B718685AE6AB60F631C0730D8A0915FB60F6125FBC47CF5A4471F63618ADC4879B31743780AFAEBCE51BEEB0E28DF53D4566F65B6C0DF88D48D5488548F94G945A00F5DCB6F909076D28DED13FA26DDB1327432F255F51E35A5E596BB0F5F6D88E1AFAEC26F63B2557A045C91B4C4A355DA95D073CFDF7000EED16CE68999D362ECE10EEBAE981E76A95F17EB3F9AA0B53E361218D361396D0F0325B00F2BF1D72957C5ACD3D0E835DE61343A2479061D326B01FB8E5BA88
    92C1G7C1D51404A6BDA5E6746425FE39B302C2E7812E1D587E07CB90065F25914AFD95B83673658572C2931F5B0B3CCBDE750C75FD897G3FD608BF8AA888A882A881A88DA86BA0745FC0D620C8205CC3569CB3D0A4D0EE23B5278DA89AA87730B54788948A1486545084F2008A1BA1ADD09CD011916A8DA88E286808B5E7GA889282A451A9388148ED4578A7D83D0C6AB0D970D5896B27EBA5A10722B7F6A76913C2FEE93FE6D5326EE8BD35733BC06819E8F148614E702B1892891E8GA888A88AA889A89328
    309D6C82B2828DG8581C581A581E58295F6C0B81091E8GA888A88AA889A89328508C61C0C6208120A020A820A420CC20C28B04DBF06E70495A7A717AED1515252B3E0255851FD79835F1D8BD32BAF51516550B9E9EA949E4F54F6A5CD5FAD6E75E74EBC84CA758EF56A032A325B02BE4A373AD668F980E7E437EE6BE477C1079D103A4BB4EC55E14447CACD4AA5BD12AF28AEF55CF9F2108477CDEAFCE02A2CE202A0C52A53EC8273E3CA1569ED99B9CB82215932D30CB78D6C015AB5FDAB8080E99526FAA1DB0
    A6F742A0E91738403F11FE59FC6F2BC152EF9CE239AC16FE3F98A44EB469F72974BB57A066A5983E9AE82D7477BC20EF01B6GAD1230659E58318DE8017477C4D558F697E9F294FF4FF291E712626F4D2A30AD526F0AA1169D929B2B58D832CEA7EC3662EFB15EE4FE4546ECA374E37DC001969CF3E226949978D83C4954EB4151F7CF8F8C1C9633BC8209380FFF416A4BF24A52692831F4DB6089235351AB0DFD31DF30F211466523DD869CB31F65B81B27ED060133177004AF268A9CE4A8C7F98CCF6261A60723
    47565E67306C37B89C364EE3F27A315C16DE27A9E02F14571CE9FC5E82F90C85CA243C1E4CE33E0C63EBDDD757093E6E86B6F3104669A77873C8AA444FBA0A7D3D4FDC766CD8C27C951C1743274FED7CDF5623AB12F5AE99B69D2CEF90BA3A6675CBBC6BCFA6CAF80E644B2C9F78C272B9D6062CEDAE12FC0B156DAC4967D89BE5ED1135A956E73176485ABA6BE7D8BBE6ED1279BD6B2BD8DB46B6ACEC380E5BD08979EE8372858A87CA84B29C03B9A5D0BDD0BFD0B0D0ACD09AD00195661AC0D6A0FF20C820E420
    EC9BBC4381B5820D828A850A874AGAABAEE4D29856A868A840ABE0EE5BDE6EE72B839ECBCA907990AF240BEC12FAC968DD2964A3EEC030B3A5A69827FFF64BD093AEEACD65635A775BCD12A67EF5D5475570354B52BE76C33F12CD2536A7F9F14517FADA47A7E93D3DD0FDDBDD375472E7E297AE3570529030FCDBF192AB7B609304B27B29F6ABA5D29986B2E1E4A1E7BBA3ABABBADFC4025A486314677DE834B072D5366B8E4B39F33B8765B4EDA8C063C93EC4C8A634F16A950FFE59E47673053F371B94CFC70
    BAC37D793F0F53DBB78A1FDAB03E6104B4FFBFA1BF07891B2E79120D21963B65A49454662E3ECE0740EF604F2D925EBB01E317FD4E5A4CFECBAFFB6A5DE5696CB3887C12732C9CF6B4F4F559B719FAB675B99CDD1DCB25301FE6FF4E42D86C6D8E4B49258689CFDE404AF6FF372543F65456419F4439C48C1F3909495C585E8B155561F0567770A6E6DB2D455E4DC001151FF552338C6594ADE1ED3028E4CB3F4D010125C2E2D95162456B0BB69D58DEEAD18436EE6401DB18877516ACBC38F0A959F4E9DD8D1735
    4B54E9BAE669F1A96E24F338D662D2A12FEE6696AEEF47724DCEE52791F8DC95C1A3F19959E81D3C134B5CEF37F5D8FA86975B2B0D23113CDC12FB2DF59B173BF1D37D7E41251A54B1B4B2ABA419098B054CCD361E0E41E5362BE3E8E42E10E47EF80BA853FDFD1D030B6CD1C550C8DCC9E55ADA38174B2C072EGA6156E2A3FDBB71AC67EAA127F02C37868FE53A90BCB293D0AC00D2CCA12D5513A11E4ED6C9DD41A9C2C11371A6465772F677276C0DF6AD2DA17A2D06B6D65A86B5CE7D5DC56EE4BE91722BA65
    B02D17CB6DE6C36FC1D19F706C427A8E4B261E2E533D0355080B08DADB295FB83E3AC15281196BF11CF1DB697A71349A168B79636CCD22BDA9FAB8B7AACCAE23EA352C40FCBC73CD3524272B4FF587E8D206EA252D9432EAE608F25F588BE54887B0B765EEF291D12BE1955A3B2E26167C57CD6F250E2115DAA9E4766D2AD3348977D2D5F134F2D7CBFD4D61DAEA9B03CB6DD247507AF63910F9FA5AD6ECA3030B6CD4C550765CB45626746D967997A3371B8250092435165A09ED7FBEE71FF0B3B868C6534ADF0E
    72AF2E5A675C5687175F2D9BCDAB3F8265EF4B5B2D6C5B5DC857092415CDED6F37536A1D7A90F7266B4452CA175A626455422745A4F7F049E6ED9C2D5CD5C2EE766C036AFE49CD0D3A082875C7EA63A59DEB380E6D7BDC769C36FD2EC701CA14D3FB562A36354E565EE36AF15BDB1B5C2550EADDAD561C2A26337932AF4C230300A2CE601A53342FD8B82EB9C98BEB1B3B6CF6B155B7603902236B15678A62CE08F389D9F6EBCE81D01B1D457946182F08D3EE97F1585FA2FC1B4BF02123572827A39462C58109B8
    0D3AF192A0BC0562BC5C2C9747F0521A13FF92EDADF5E3EB23D3F869C9915ECF69DF528D77237026A3FA6141947E0AEEF884059BDB7442E3A9FC0CEEF8920537346A0527D178DFF44333BAB13C2DCDAF3C0042DF538DAF2570F613DEF8B5053F219B5EC06166F63DF0AB057FD5B7FC00420FF668057BD378DB3A61A194EEB56B05C7D2785B3A61F194FE5C22971ECC616F6A0627D3387D28DEF8F697067FCDB73C1042BB0F690517D3785FF543EBA83C5B2A975EC8616F6B065BA93C472697BE0A42BF508D8F20F0
    47F13D70D08A7FD0B7BC2A8B7B357179F9705BEB79214F5259E1E10B68BBADE724FD741C7CAFD5E187CD76BEF9FFFEEABEDBAF30AB565F857E45B47DB507E953581A7B89127F7534CF8DEC1FDD4894EBA461A6A6333B47F692BAED3621A075F9AFEDD776D571E0BFBB5B158E3F595D569C117674CCB6EE30D3D2815DAC4D58F9F8FE2B8878CA2046EE114E5EAD7AB0916F267998AF99788CC53C029F147176AE40F8B5009BFF10638DB8451BD80271C2810FD644CBF60A77B0454B6B316614744871EAFB1471CEAE
    44F87D007BAB6205BB451B7DBD6583708C2002DE912F34D7996FE50A5788F8B7103F94AF44A95E4D0BB0DEA260E9C0F98E912F58210CF72894635581EEF64871FC1C62CDDA0C7142810FD544CBF10A7798454B6B03F2812A6D93710CFD4AF87DE5984F8770A020A8A9DE3CD33C25CBB0DE56A9E87B2764F8D52714717ECA713A8177D5448BF50AF7C3B915B360990AF885271571F6ADA5FF815C88B4F0DA4473F70A7769B20C9783F892D02694AF2F5F29DCA8DEB5600D7DF23CFE27F89716137F819E2D08176C94
    EFD985157399A867B3F23C5AB34AF8EFD2BC8760FEC0E1E7C43CE827F8372C40F8E900E71F1563151CD5465B3F92639981F7A86285B8457BEC95460B85BCD9914FF0CE996F910AD78EF86DB9B91E55A9DED7A5468B82BC82A8611C64FFCE71CAD6E33C0281988B006A87C4BC7300B25EEB94AF9070F020F8A95ED827F8B72E41F83967216DG551C97719A4FCBE7994F33F8CF52194EA5043D4C3177613FFFCE4433EA3B721467CD871E1B22FB1E10D112A4BF6D3C7A8C5F8FB3185C3C8B561C228BB896DCB3CD39
    2F8ACFFCDD9DB63EF2AB756B1B26AB570C8536EDBADB17BDEA6B69F5EC6FB4DB7AF1EC58B51D594A4ED8C930543F9F7E1C1D3D6467DCBB3ACE16595ACF16751DBAD9E6EAF71441131DE34D9A3E44FB50565BE732736EDFBA6FFA73FA261B492C3800E7C92D4DEC1C31836F8394F481470137274FB1E84F25ED8171DDBDF4783003CD5AC5F95E38CCF9BEB648787E38C9AE4AB36202A847048BF2F9E61C7AB6DB58F82F91ED4C3F08B65E41ED2C835E8CB4F0914F4C7AD35CG0A7BA90F9B877CD820CC0A7BFEB349
    9D05F14F8839401B0186C6E15E6FDD344EED5EB71F664FBD8DDD1B3B4C16DA983EB7531645C11B6534814B7CCAA37AE340A834A56F88E2F104DDC5D8560F907B328531AA422EA14CC1D8FEABE2E104DDCB58D8422637A1D678E3442EA72C01308293E2FE045DC0D88CE1B35B914BA4ECB4E19517A0D65801181D301B888BA16CBBB3E2C9045DC2D83E8FE2C596446A883B15B09F42669CC5AC0A305B89CBA72C7898E22517A2F687E1E64266DB918BA26CAE429288AB31A1167B93446EA62C06306F0FA3B6C0583D
    04C590D6FA8231541F200FFEBC33G7B006326D3267E325E53364EE350743732F31CA25D669D687345BFC51FDFEC62E7DF00F7G798109F32C136767CA7DCB88E0C9BF45396FD72714F35FFCDF986F015A00447A02E3BE5BAB16568E247E69955ED78F36E1A43D18D0DFAD498D2B3949507FFD166EF975D45BA7639C3E222F8872157B8C7B02426C86A0E17F6F487E9408D3F499BD7B766A595FF8991663744F583E351B5DA8692C6F598528438E69C3C8475F1B14BA12G4F7F994C15FF06BA9E5AD6843F6EB628
    040E329254D18769FDFE06BAB64E525391C5BA4EFE4E765DBD582D127272BA6909879959BFC7BD96031E1E6A1F231E479633BDFE377BD786BC9FFD5DC25453GB27CC84F475F696909A1BD17D7B3BDEE7734C84F0E6FD1CFA2484873C3BD9D3AF5D36B077EFB7F77DA7F6DECE67565EE73CB681D3088759AC1E6G691D542E763BB888CBA33DFD0B34FA479C18EFE0FB6C1EEC0DE13E1FA27DD91703EFDF0E7A47DB747C5EF1B96AAFAB556ADF3415355B41B651044ED12528539764C5134E76BDFABAB3AE47BACD
    EC7DCE126FFADB8D73D53198F564DE81F33DABD047E755FABA862EC09D97A633BC8C3659A6642710FCFFC89BCB72334F6949B7DC09653627CCDBEE9F5B59FCED10DDB9A9CF3716214EFC10D7F7A56A3C432867ABBE24B3FB09D6670EB9A54CD7BC5C34937A1B16207EC0109DCF7A1BF575E77BE319B656AD603ABC5A3D1372BA259CF595021C86FF54754FB635AEBF888BA7DD5FCDE1F3DB4F377150DF1EA0FDB1A0AB13747D32C32D2F62AA687F2FC2FD168D5FF2FD036C6DD19FF3EAA9757F10BE64AA9AA3B5F9
    E26517F495565F18255A7A3BE3BF2BBFCFB77F047EA54BD0FF9A48AE399A75DFBEC72F0FEB3B9A75DF37CC2B7F7AEFE6CBED51337EB505F4BBC0EE98693EFE2E1E6E31D7E379362E18CBED5E13F1692E6528A783E414DF03FADE285253E33D86757CF663EC295DFB161F668A54B3GB2A2C8CF4591BDBD2924E76C78A25156BD989B3ED801BA8C81B09F88C09DD9EDEA9D5D9096900075F5EA05363E9E58DE4C4A51030DC721BB16F407025CE4527D62C1BD5D8557E27E1E5FB7DF6917EE8AD3689AD8093ACAC10E
    79DA54755B59FA3A02C857267E794ABE4CA3DD652BD0D7B848C9A1DDC59ABFE43A0A2EC3DD3B3AD979F932B9A9740CA5BD95A043FE9D75DF1A36467404101ECBCE4CD374151E79E2E0A56A0A84B9E9246BA71A398B53D5F2BD7A49FFAB35FE72F38BEBEF9E6CE6CA3A772EC65DD5A057F1BD6A7E232E1F04116E4855DA5D4BE716B8775D9E147367EBD0FFB4484EA07DEB3A75466172C0547F439A2D7E7C09B361577536A8167713243386648D84224E9BB563A09B1BA2C86777EB35BA27ADDB6A1CE74F76CA8D74
    DE6BB227F528CFCADD2EC345860AE71F24C075BAD45B576CB9AF83705C9BF09DAAF6BABBBB086BD07BAC9D8ED367B13B4500EBCB27E630BC1D301C117833B318DE3E0FE040B341372FD73F0BD98472AB00EA010CB7E85F63916FCAA671F5156E9B443B1263887FAB47879438280F4EE6FCA75A9742D2EF407782EF1A496A237EC6E8FFC0BEC0C1C0D1B7E29E479538FDBFF6CB7FA06F47069B5579CB8259E9C0D92321CF9C6DAAFFDF9B79BB222355791B43714A516A7C5DCB792B01305051F83E7EDA0D7E5CA068
    3300AA00EA03DC69BF4B659903547AAF6138B5C82DBF1774BBA0ACB18875FF542C56DFF513B5279E488C54FF13AB7DFF63727CEED26B7F086301B72975DFA47DA19016FDB36A8F5064FFB032D33AE9C73CC9B70A52DD67D53AGCAB723451BF42114AE502BF4D1146E6BD6EF5245D33A9B3DCAB71652FD5366CD3A8CCA9764D53A5CDBB05D37A6EF5295D13A1B3DCAD7C169E635FB132E165285FB154EC869E6F7F8132E1B525D66D5BA9FCAB7576CCD3AC0CA9762D53AB0CAB74F62CD3AE8CAF727D76992A85D02
    235E24CB21F421DE254B24F48B0FF913AEAF98535D63D53AE2CA37486ACD3ACACA9766D53ABACA375866CD3AB6CA778B2F52B9A85D12635E247325F461DE258B22F4CBCFF813AE1C52556EE069E200CF8C560EFD29AA4CF0AB5E99F1ABDFD34F3FD5FD77443D9CAF3ED5FD7744F2935EBDD181E10137227E2F662B6D4E3C55D9E741ED4E3C545FE852152978AAD5BAB1F70D1D4866D1BAFB88B8EB154E0D5CF1C8F9EE2481E475838581055F06FB94BBCEE5CB76445E0673378F3EE1EBF1065B2DB905C095C075C0
    8EA0FF20085BF19E57DC20375F66BC0FF33559A63FABAB4AA2EE08E578325BB2CC385DB91D34C76740FC275E0E75B8EA4150EC38C213CEEDC3F108DEBD2696ACB48C3E9F6C74A0E640B310E3CD4AFA2D8259E6A0DF2020905A73627B26ECEDA5A28473D7D1B2347CED5224D3672F7B8E3DB26E1F45ECE06BF43EF7208DA9C33461A337B6545C29E7C31081EDB05EC9731F05C333619ECDBA358D85F76959D04E4B016DD7155F05B654FFBFB49BDAB46954B6246A5AF0E39333012DB1E405228DB90B06E6438CCDBA
    358D51214E69045FBEF7C42FBFCA0438292168371B5A31DDE65D0DF67EE108F63E62564E2A3B754AEA3585EDE8A09BFED2BAB49B82B46954B678695AF0439E34A104ECD833F8E8B654EA5229EDC85235E1FDB55A10CEB63CB7C49BB25D5AD0FA0F1E8D9B4E61DEF84DBDE843DDE5C33361A1CDBA358D833AB6A499319C82480636A5C33321D313CEEDC31C2E8DD7138DE349067C722159B0C713CEEDC3613DFA6D3725CD2F7DD6C05C5AFB317D1619504E36FB514E58A15A7922DBBB83F56D8CB66A59998EF1E348
    4EB7BB504EA432F3E069506C7C19A61D5A4E7CB03DBA5D5106B61406218DAB168D4D064D1AF4EA9B4C3AB6444C4131E900ECF8EF08B6E43A352172BEBD9B1E1D0BB6545F07B65C37FCE8B6BC22C92736A17797FAB6642EC39B0AFF01B618AA06E6C317A61D5A06E4DD9BCE9CC19BB24806E9AB06E643DCCDBA358D913F54EBBB179DD14FAD63A0DE9AD0D6B8361D35EDB827AA8CC7BB1F9D221DC9EE6DCC8C57AB2B49075006B4326147AB07E6033FA61D5A06307B75EC481C0DB6445C0FB62CDCB5B49BEAB46954
    B60CFAC04F06C33C6D30673140875006F706E8C306DB9B9A9E543321ECAE16037DC1DA732B9C1A8DE11AF4EA9BCAA274ECF83489ED280EC09B8E2D9E1A8D96CDBA358D193AB6FCCABE197F905A1037E6E8B6FC27C92736A17EA1BD9BFE6846B1A505ECF8FA08B67C592D8DC53F523361B91A2BD47E8A579416FF4B30EE60C77D8A578FA28B589DB53857D55FE56BF498F01F4B72B5FBBF262B47F64C560958F10EF5F475700BC744FDD73F61E7237DC1E6881040A6ECE0D8A4703104D9B916GFCAAE1B7F01FB17C
    5A1AD370EBAC2B571B8D147FF795FFBB1A076B7EAA393CAF9FD69D228C6F18697A8E1930197AF748BCB0D37F8E194819035FFF96BD53559DB3227C1FB2E25DD57D9A6BE452912C3BFA426CC7306E0C043DC8F557CDF5B74BA857D709626F7BC7206E1E99D69DA24FE1D4DE81D48EE9C6AC2FD04276D2F9C590360A4AAB164AEB14423FAFD37C7D658814572291A82F49D4DE29F259D0F999A291FB40086515CB58BDD4DEC511D8DE9FA84AA8D3717725A3D0DEB70FC0F909F7B8EAA03FEDD48E25C790F390F69FE1
    3E041535A096C458AF898BA72C3C953198426EA7AC1130E5ED08259276A0E10607912BB0A116CF58C304159036329D31AA42FECDD8BDE1159D081989FB1830FE4256189173A36C914202892B32A096C15823044592367EA8E2C904BDC6D89AE15547904B7A8DE20F93D6C058A6ABE22504BDC9D8B5E1B5B6449A887BADE1D642369EC7EC0030278873A72C7684E2A10435727799A201CFA26CD79CCB7B0DF8B697D8C0AB36392CC728AEF91D17GDF75882D7F18583B3435445F4FF9B3712BCD1E3695A6E3E86DF1
    1F47BA863B3B5695FD4B53BDBD1D0D555D6CD0DFAF5FC829B1B9CCD258DB8EF61F1F663E355D261396835EA131E3FE0E94E70B23EBB33BC7CB6CBB644CE077G3A58BFB224BF427798F660F320AF7041C031C0C90F08FBC545BCEF4CA1DC1B2B0A4277D4A61FE5FBE48E607D00C22230CE761CD24FA523A0AC9EE8EC14FE9D08B944A75F381E2FE4956A4FD7BEAFE4734A5E2E3E1E8E0BFACEB235300042645DA836E9460ACE44194953BBCCBD47AC1AB94DEC1EDE0439CA7FFD212BF90F2817898B14753214FCEA
    06C3DDC699D0B6390F42987428FE9989F93FF612371C6A396D62CC7DFA1636157019FF3753FAD98568EA849AG72FF145E8523F57950C7312E9771F3D34940E7G657D8F6D0BB70733B67BBF03372DAAB7610C6AA10E99289F48CF95BFD862A360B796A8C96253245F2C4720BF84AA852AFE4CB9ED43E3DA5D22ACCF14A84B32026A667CAC16A72BCEBAA58D3889E7648FF1C200A2F56246C9D8B27C2683E5C7BB47A9843E9C288628D195E60FF61527D98B15F9DAC1F93A554072B4CAA71D12825C04B38A05B8D1
    C071BAF147CAD8867C66BE8E3E7C38F31C8A60EB010CC05D2AB01F47DD6569CFCEF9DAC9F95A3A0265A9D0A71D12425C04B30A06B889C0A9BAF1B3A5AC6F89EBCEB1D06593022F13FE5B605781648B947404F37A70A7DC6569275FAB73340A72F4CB934BD30CCEBAA5A5AA42D3DD4405A9C0CEBED089D095D07D13F2BC3374F7BF7C7A8185BF69ACA38278D820A420B4D5D8D60C2BBCD5AFD266091D19957DC9CE8B76A785B1581F6C6667AB6A0137820D0A417EE41B66BCD7A0040581C56B6815F5E715AAF52F26
    72DC2FB94F14GF2D200B2871577E869678AF96C6EBFE9EE3EC7ADAF6F376097C0153F9DCC5E8F0B1D64AD25357CEA353CBA1053866498D45E3CB2A7F94BE8ED711CDA1EAF4889828A870A5111A9643D6AACEFB94AFBCDF37EB391E4248299FEB718FD57AFF112D701722E57484B87B9A5C0D5034A5BD96EA4EFA57A56F5342FD27FBB742D5778D9D6DF600301A2FF073E35DCF3B6B19E424682E58C2A7B3F4E3AD721EE9B0D1339CF216EFF35B35DB5409B019CCF216EF7B567867DA0AC98A8622941F4BF3854C9
    F7A516639E4D394ED810138414B628BC7BB2A7F92BD15E53F3D83F1395BBF83FD360A61CD1A9442986EAG322A628FC83CBF7C06GC52A426300CF86CA874AFEDAB59EBE6D4AF767ADD766E9993555BF4DE5F9AA57C927249AB7610C9AA10E9DE894D000AAFE2844C741EFBC50D8D5F88670394F40D888D4710CF3D86DB32E72B456B9CF54DFCCDD4772E454C92724EEB7610CFCA0CEA0D098D034AAFE02442740EFA6D05E6F1D430B012F842A83EAD305B9FE6FAACF0195CEF922BE6BC7D616A7DF1DF4CA8AF293
    4EA89C6244GA582252A629B62841F8F3FA5C0D5F14E6175401B017A017CD4E141F12E72D43742A9CF4BF11E7D15C1EF1E9D81F2E263F01E7D78916CBF1263307F48E9E57DC7419FE06E87D47B876CBF2A5BD899357DE170B2F03889E7648BF102004201E2D47193A5BE95FE8D4F427C61D9677092602B006A014C4F3A57A54AE862CA27B22231604BC3ACCF7DEE6478F920A79862C4G4582A5296227C9FC569F61998128740F2A3DD0609B002CC083FF74B4CF8FBB67E98566E99C6FC77D5D488971C0CFA44409
    83CA86CAD7454F0E97FCA17C16835544BB07B782EF879A8594906FE91ECE2EF24A53CA4C1311772321EE64C4F920A79E620C854A50091B7B1C400A6037822876B967B8C6603B01FC00821F73B4CF33AB1D72348A73341C67A94C0D1CE88F74A4C01C9420CC203C67D57D2444D742EF9DD01BAA5C813CAFD090D078731E66698567BC511C6089716C60C6CE2287FAD2A10E61CF507E01CA7E649C3FCA626B61578C542F8A7783BE98A882A876CF1E66690A55CE7392EACF13F89F1164C6CE1A87FA3292207D831582
    D5A7285688A45E8A3F83C07E2A709060A30162001293BC4D5336B5CE75C4F32DD35D6A39DBBA484CFE411AD37842E0F3B743DA253C65B44FF9D1B327AE87B9B5C00DAE6409352B4AEF591977FE622BB8FF0674BD4777DBCFF6DACEF6F55ABA86DEE063D38A475E82323F006FDC4E5C4056E49D16FEC7748B6CFB36875951D33C77F88333395D54F162D8CFD7DF27996600DC4E75FC0FB66BC5787BC5FCAF777E536CBE2A23BD2613364EE36C138A86FF96EE88EF4231346AC54977245FEE789572445E58EB4C3F81
    93F614315709A5FD577231B685425201045C3F115C22BF8BF99552EF431FD16E8BDC6E13ACFFFFC6395F4C13651E65F2FDA04C7F4FA8F7B7490D126445CB3FE9A4F7A5177B9CD0DEA24A7DC0A177959EDE84E12509A877F1125B18A8645925DF3FC43AABE1A36FD7781A6516CE333451AE6ED8FB024B3C03794CF844B6F37B9F867A4BB844E2B8769C886CA0EC8BFF06FF8C309B887B9D476E866C3704ED636B7A178276BEE1319CB38176B5695D4E1F5B4E00137C410058B39C7BB3243B03526E647BBBEFGFF0E
    30B80E7D89783D046D624FE2CF833F0030E7B9F69EF4FCC2BA76707D1DE3006D22F8719CFB886C1BCD58DE3E3F538758AD1476F90EF5C05AF994EFBF5F5F399230C91437840EDDBAC1D92687787E4E4F813B1F3097B9F6B9E01792F66898362F399390CB64589BC07B89BB4C77F75E863A043017B976A1500304B5737D1D8FD8FA4212B876B1503AAC440E9CC79D6788FB15E3FF9CA76AC4E02DFC4F67FED63F5446CF6DE07B93E64BD1D31F5D31595E55EB5953ADFD32147C79AA3E8744FCB4AC917B0DBFF00C6F
    C4ECB275889F3F3795FDFCAC444BGAAF8891EB5009ADF42F4F1ED7C0E8B1B033FABAD5ACE62FC394FC9DA4552EFBA30FDF3D727031FD76834603C7CF513FADE4E76B87AC1365FCBF84F56711D74AEACE0C9AFE15B7A71EA97EB6CD28EF0DD60011D18577C17F1DE7F4EC1A6338EF8B350404B786D1B339370CE3E4C05379B7CBE1D217B4D6A2AC7A60E8FF8D93475C869173DDB9EFA6A5BEC69AC4BA14D18827132DF01B16595F98CA8D77CAD5EFFFA086F61543CA25EFF1AC6F8AC477B9538A81B2FB84E78B088
    EBCC423D3B237C5D222CB1D0DFE3E8DF1DE32540D791B669B443EA01EFA32C4C01E99D0475B8B02DAFE1FFF2E05A00B1D8A79FACF4F1479A2BF43B2873A9AD6ABAE77B0721A0A3EA8CBE0B7D046EA9CC9803F536042FD1663EEA4DA9862AFA155E9D65EB148D2FEA47D6ABE083BA38A8533F70BD947FD7C5194EA07C830E47AAF0D156CBB94EF843DF40563FE0B9F47077FD7A13E1DCC8C66C990E85819FCD58ACF156817894426E677BF86940673EC67B333CFFAE823E1230578EB02C8EF8BBE10B8FB2EC947081
    04F59D42FA0AA4AC7E9056D38CE1EF73B1A59178B442FE4BF5E43D8EBE7ABAE2DFF09D654057935641B1B3708E426A394D3E40079076B6179789FCACE1EFFE4730A4605388FBE89616DF569B08CDAF52165F06A2AC3FBC0AB771B416DFA1E1FDD4FE65047D71G16D58DE1D3292C2C0475D0D9B9880B253272A56C5D835AF24927F28922F87FEC41F289A72C174AA506304F793BD2094027927612814B45B0164EBE0C5316CB47B8AC17DC0A17C4FED5C0D89D15CBA9E12329DC2A899BF3904B45CC58FAAA17EE42
    2A28DCFC887B39CE39C49C40F28924F841D4AEE1047D144AA51A305B3F43F2C9A06C428AAC1794427E32C2DBAE59AB31DC52A95E6CF5D8AE063FA29639964BA51F30EDD5D8AEA504DD368E4B250E30F756E139B492963E864B45CE58ABEB31ED0DA2ECD615362CEA2B302C82A8DE5BDAAC2BD042AA2B302C22E41B8FE3D945937667A6AC2B31F2DA1D3E494431B4081375A6E277B6E3799590B661901E93A9A6ECAE79DAADE113382F99019FA02C117C4F1F3027487FC2884B21F699CB58F1723F84429EA17FCBF9
    53B37F4B24F80B487F725E22365A00E5DACC588797313F2AFC8B471BA91ABBAA6AA02C8D4871167E731D98D71E6063176FDBE2DC19C4F8BC47C3953898EF9AB84E78D888ABCDC11BDA5AF1FC76A76C36F6AC339042A6F4E0190593F64002E9E3883B4102E993897B1785530EA56C21BD18B603300F77E05A5C3791EB2A473485B2D60DE9CB893B399A53D693765FEACCDBC7D873B9CC5BC658AD67B02D03303892CCBB0A30FB79F3EDG70E104E598D1DEB4E122AFE37292883B69884ACBA66C9714B61D30FF98B1
    ED76BB086D2734796F205F0C566C9115C0D895D07DBB03794D81BE6FB03FA37C63B342CD9C9FD06042EF5E627BED7C1DB9E68F59344304369B5FC56C8A935A5ECD585FCDE87B403BE8FB27E69F589F42C200A25F9D4C764E8EE6CB5C3B6A777C7BB91E742E7ABDFFC3873E671F8AE17529E853F8B35A9EC158D6B37593045DE526FE0230237CB9B68578CC42FE49313C3FD9F30A7EC66337A88B60EB889B475F2FE8843E1BB0AB4786008FA66CD10EC5G9FCB587A333C7F84BE1530AB1B317FB43CC736B4E33FD8
    CC58D15EEFD782DFC758FDBCDEB77023887B127B1E9F70A104859C46FEB1123099DCDE9C7029041D9067EC7F8EFF7F9D31B71A30DFACA66C234358AFD69216495FDD2B833E0D30C9458CF3G6FC7D88F4782010FA26CA90E4583BF1630A05E1E53004FCEC36CADAA2BC242BEB3E2D9D593B60D47EBG5ECAD800A8976003887B18E32140C793D65504E515C058139CCB81BE7BFDAABF2E239078D2428A1A312C2A895B5004E555C058B2DED6D66087885B4E678D7E400792964E31886093891B485777D201B77C83
    31774B98168BFCB1E1FFDC00E5D5C9585F97E0D999897B64BC77A160FD882B61E3DCA87011045D4D31986013885BC6E515C61809E3D99F00AD9F50B8A1FC9778DA425EA33FB292D6CDE555CDD895EFC7BE40879276B0DFC78983BE0630A23EE6928FFCBAE1FD9C4BCE87FFC927799447CA002FA66CB29B16D583E1622EF1D6D67D043D40757A819FCCD883DF030981BE013007B9164CF842E22DD8D6399FA2964F31A2602B89AB66FA9B00B7937665F1AC2BFE425E33E2D97991F6164F8103010F78901F1BF772E7
    86765C9C7BA1BEB7A770F14270910C47C0659FE11F7EBBFE37D76DC75A7E5B88D8378EAE7A6E7B791E284FC76AB50A980EC7FE24DE2378229557A8D2A1AC701FE8FF3FB8D31E81BE11C173F80ED90177A3CC1CB38F86BE0230B10D8C0B86BE11308C9356EBAAE1856DD82FF99FA3361327AD863E1230E7F89FE7845ECE5892B1F7865EDF465A30DEC3889B6072A201CFA4AC1EE32940E792B63B1D661C7FA23FEB24B9A7E1BB78DC379278FA4244BA019178D104FD4A5386G9FCA58753CCF0AGBE0E30ADC6AC17
    E442AC540FE67D9B3151BC3F8540179276BA17D78FFC9BE15BF8DABB70BE04BDCFE3CEA0E1F5DCDE9870F10485F3AC9978B4426228EF484A247223B1270030553C9FAD853E0630E00E55836FA06CC30E79829FC45829B33C0F83BE1A307768BD1384422650D81CC1D89037A5779318ABFC62BCCE56G5FC0D8ADCF5B86FCBFE1E728DC7C887B10E34140C793361D4BCBGFEACE129D4AE99044D20BEB377BFB45671BE338878CA427E4D319A602D045573F1F7GF8FF429672F1B7887888421E23B208A54C4A75A6
    811FC658BDBCDE7EFF41F77F0B58975CB74A012FA56C89AA83A3E1699C6B865E1F30DA2EA384788842D2288CE2897B9779C692E1A7F8FE53004FB65850A7B9168FFCA5E18BF89954815FC6581F79BC4D8E3C8FE1F1B47788A4AC154AA50AB0D1EF71400FA54C1F474B9EE74BA9980758079CAB863E0A305728DC6A897B124BB3836FC318188B86829FCAD8964DBD22889BC73E91CF583FB8B69678CC424433FE76F8DBCE69F844FE4531EA609B88DB427B1CB6607B89BBCD6F097891F6BDBD570793F69FFF660E81
    BE1130F43E2E1489FC6E84448EF39D8540179376A6BD575790164753B6825FCF1819E3FE40879176D7F93D0D307B6575B642B6F33D09402791F68F47B201AF4AC26CF35E47D6GDFCB5883E23E893C1DB0F92EBA0AB0F92E9AC258ACD1C7404791F6D42C3DGEF1808586FB9168BFCB1E1AF103FD492164F655581EFA7CC3455D1407B93B61D7CA50430EC7217C842AE676FB047811FCC580B9CCB87BE6BD372B53E761F87FC89E1FF63792D823E1E30153CAE4D40BB889B4D31D1408782C9E7BA57335F853D8B24
    BBFEDFB3A86F78AD0A1A67720E5FB01041FE23255F606F8BA499CBAA15B2923E7D4738F1AEE4E4C8E933BE3351DE0E5847BA492E89137631FC4B587D901D1653C5ECEB234CF45AD136394B5E55D3322C3C2214530A958B25BDA7710EAC53D589B23B01D81BD55E154C5ED3E19B73E52C9F6461AB1D42D9FE37C861A2BF0B1AF1EF2AE165DD065ACB7EBDCEEFEF0A6FC9C979C812FE6B669598E25F79B6DB646333A33C2C3B97C8FBF5CFFEAF677177CD1E67712BE64CE3FEB666F1231BBC76EA7258BBCE048B7D29
    C6EE1B89ED0BDAA45BD66A05ED8EAA7FBA326D362641EDCBE8D25BB6E63C5236DD42B6AB5A76D029EC5BADDE5876965966C336CD53145BBCA75B36E94A0D6D8B4B360572FB9895DBEEE507EC1D662E531B3BBAFB9D26CEC7EFD94D767D75FB76EFE95D333BF5F39D7CA15D97500A36C411AD7FF57A76AC13FF438425ADCB5B5436AE982F8C6FF08AE73E7B7EC4E57835ED6A3C7CC1728165B732583AE7BA58A41EE142AC6C9922B44716D383E484924FB05DBB3D39371211C8F7E10869FE6D144E11E323E7A4DF45
    5F5AE72616C34C7EA008B3CEAA93011F60F82482974FCCE9FCFF1A6FFFC2D86567B669AE075B97333D53A060A3016201D20032A741B881A44E8D4DDAD0EEF0F3B7E4C3D7F71D6514452E38BAC0744D9F73B1102D33D5CE427EFA939F83793E87E1F7F10C6FFB90F68D1FE35B01771D047573485992788DGBE8CA886A81945874A4B057987D08D109148110BE91E65E95877B75937BA59F7BD59B7C07DA01CFDA3B58CFE59B78F636017FDDBD524797AEC3024C773AC1BABE30EDC6770D2859F231396EDD563B539
    7AF52DC7E1D2DEE59F2A61366A3D1B7A15626FE92A30AFD43E28CE1BA33599B5BE558B9FE7EDF132C1EE77DF9972F8BDBB1FB93B121FA3E067CDD2F3F17CBE5C68FC666C9F2CB9CBB2766D52BFF3D64177EEB3C1C676E41BF48E6B901FD73C82D4811810758C7BAC2514A6130757C0D8BD8B677D45D6FA1FE9E0B276975773B5708860630046CEC65F7A3953593CCC407326083AA9065F4AA95AFA956D74F63E97D3B74526DA473ECFFC9BCE010B763B026E2B35C3D87C94ECA3153CEF2B78826C7C8231CB5A31AD
    359116CC73C94797E87BDF396D4140C781A581E582956659F22A010CC083C0C1C0D1C049F9186EE31E0EFDE7B5DA7AFEAB7F56ABCBA3FDA738C47A3EEF61D49B7FFE2FC8374A98AE1581132B67AF55924EF4962A62A4CBB6F95347A6C9F9D363BC4F122CCC1DF0EDBFFD14ECF7657F6867DF69341B992A766689FDA6359FB54EFCG5BF20E9B99223D1CEDE676B83A3A6C8D366E86E8D252FC633EF239CD3D56BC9DFE2DDDBD3633DD1D8E131DC52B6F6A3509C3DED2DB2179D955D4EC27AB0D6C9E1F13269EFE37
    0F107B74D2D9EE6CA1719DECCBEF2F454CBFD6AAE4A573F1418EF27AC9D6340D45BDE96B341D6CBB395FF656A2457D8B1FD30C05F8E994B763GAB679E76CD6FDE47562E0E3E5EAD1D6C535DE6A94D177CD90E45AD7C92537CF5A733353D2B073F84AE5E0DBFF8904F8E15C23C9A20FEA03FAFA5DF667939153DEEAF499563D9880407135C3FD8395D26FE155D625B21C990AF0562A69D60FBEF36DEEEACAB9091B71DBFD3B2BB723F4238737977DFCE312FGF5B85708C8D3FD907B29E2CAF376A06BB7EDA4571F
    47E90070B60A337078E4D1A7C7ADBDBD96B3379873F70617F58244CD267893EDCC66D1708BE55966665BF28A72B14EA75FB1BBACCEF510BF8B6B20B69F7BDE9F76CA3B64A765AB64F2AD63FDF7A344B367E35FFDB337A5897894A0D1DF9987547515BF8D1E990122293E32D74AF2C7737A2A06703AE9A877FD7E3C588F3C8FE16BF81E42010FA22C086BAF1D8E7D78F44402445EBF705D53B16F338D5A3CD79AB06F4153B16F49AB653CBF39CA36F1A29F9343A1DE946991E70E4AE758F22AE6E05EE3B4F937C258
    G906BEF055C5115325CE3BC6F81909EBC8365DAF85E6300CFA4EC0CB827D5GE3D781E2CFF35F9DG5E1730F09EAF8278E842623E43FC2695E0BEEFD9AD6773749A591E9DFCBF4A7035ADA777EBCC7F9ABF0B62833C7F57184F6EAAF5BE23A0AC1E4521FC6ED9AB4B7D0A6FE9253074A477A5FEE626E8A64C89E7A216D505ED2C11309FB8E6855EC158E55C2631402791E662718A3F01327E86316E43187746EFB06F4B2B643E2F1F77173D963B2543E1B1CBF39D6AC32D14E652BA1E17EF58334CCC27FB5E55A4
    E45471FA0D0178715F208F4EE99D3CBF2C2267322AC2347FC79C2B875ED808E51F2671B1DF888BAA94633830770DF5F259DF43ED090070E812BB167BD8AACBD3686CE3455F5AF24A3FC52C017BD8907021049571F88940A7937666C5AC673C6FF0BEB32F851FAB0A88333560F3C585E14F3460DC287ABB1C3F441AD83F5AGFCBFD090D0B4D0A2053F48433B6199A128CFFC6FBE93428ACF61BC26C9773E98A6C32F4E92A59DCA2C41C55CFE3221D7D7072B711E0DBF6AB93C2B3BEAA6D25D7D144F93593B8F0533
    50979FD9AF57EDA9BF6FD38AE1153330AEAE70F3BC6C7C3A1952A4EE10534C65E75E9D90B60A523C3A877504D11A70EAB94DA57CFCCF940445D21ACB78391D3FG25D39A5F0DF21A120D3C7E0B204D94E19A9F3E77B00679F89126E95BA42779101F6729033046A2ECB7CFEC501F1F3C3C817B8A9F12BF1B7B75DF0182C8FE65E6D97E6FF8F8880405D31ABF53FBABC914A62FC6CEB3A05A8A04E59451FAF09B7AF671EC44BEEAC35F2EA46C901D2B29190DFE534C77E69B0177858AA67C98470B4F43B3B08BA3DF
    7E9B3F0B0C4577E6EE2AC73E120CE005AC2163D3E363A07E688DCDD448F56E93FBF9D93077A5D2E6E3B917EC114BD96C5BE6C0D8569CAC3FCB695CDBB9E1CF5339379A423E27F3EF75F330BC9D9D7C1EAA62AFF0BE034A75530E416E14E2697EB765A05D11B8280E7FEDF90BF2DBE44636BBEA8E162BE12BDC2E71BC5C9F420266E01BBA5F26FD468FE8C3B931946FF7ED4E4F7809DC2E88DBE452FF465F4C6BB991E40CA5B985F3751FEF42374972AE4EF57FFCF363DC9CA37366226C04395A679B5FDAD96E0133
    7A7D47C93E87D88DF26A004458FEE7337B31BD114F8FA2A1CD8C59F03EC97B5C9250249E2753A0FED6310DBF0B0BF4B14D4E655B36DD36FB21D13FFCB7727E2A90641494E39F76A81F67B4G5FD60CB615B58D7EECA276DE191F7AD11A9FB7B9BF1B8472B8D1909ECB3AF2F97EAB6659F22A67A1A676386C40774FC3D9DF4D554E393F1F0B7304D00AB727D85FB7AAF748E5F1D931FB5F88A9C65F08A4592F96EBFDA3EF27AC7741F37A3E71FBBECE25001C74F9689B7F7140B74AF95D1867433347FC342134D96B
    9B1B1B553E918471430158DA0DC8F72F5159B7BED0581DF7C45FB7CA78D8958BF29266537304B87330G66748B5026175D78C6BA79C6A525A9EBF6760D9A6E87D688F7ACC0DD9BB9B69678B442445EE4E18978EB894A5ABEC76B9BEDF3E82ECE715A56697B466F6B6432F8EA1DFB5FF8FD9D4D69C9F661FA2DEF5C3ECB161B3DC45FB70A16B0D901A0A72484FD634D856EFD23004FED729642BCF5A15A10FFC16B9B0BAE202C5A0542B75A60578194CD3E51FC5159B73E2B176D0E3E286F9B09FC0E6E87F2829752
    73912F1B9860634926FEB73EF1B579C6A62509D3759B2F73B8255F433C74FB54A54ED306G9FCE18CD1CB181BE65FB1435DF275FB8CE7DC641A20C97EF55770D0F94E5314A665EB7765950B7CAC8361FCD6B9B4F6E1565365A74FD63B4175588F24C0B50B702ED9E0CA962ECA324C9A29BD22DDA5F18E0D37BC6F6A9789390DB6B9569CE9CF7760DBB7749F6479F57770D94FE7E308264D417E25D7C131FBF34835FDF0AB63DE59D5CB7465950B7C2A84DDA1B33EF6C65F192A0BC19F4ED627A6B96C37F379831EF
    F8BC9F607D97232C2B2A343E91DA053E913D9867FA7586651AFFBC60E3970B79DC867C661639DA732FBD426660C5E56AB57FFD9CAFAFD32F793FEC44B57FEA888BA943796818A338661F3D8431B97CB9171D13AAA46C4996DC73AFDF02367F3A3584FE0D408FG05G4582258265164333B9D0A3D0BFD0F0B926F9062771839F0881AC7B2CB54781148CD4FB4E1AB3963088784DDA8A698768DB972D410A7CB379D3A43D6C1769D016CF3F4417CBFA914FAD77EE1E9C3244B9FE2C0A9FD071525DBBCE36625ABD4E
    1F556B7D382746567315FBEA138D1E5B093A153C7A59DE3D76AFFC744AB67DFE6942FE399DFE54663EDF1AEA42FE29F8A97A7FCE1336DFB2B548F2539B757B25DCB1BF84B9EDCB31DF7A225DFD3F3411BFEB45C31AA432213DD15BAF1DE9C4D9594BC43FD4843F95C0FE54AF3DF65839DFDAFDC036FBEB13FE3F54A24EBA011C46E558AFB47267949F607D1721CD57B48E5EAF5D57087DD29425F92B5139DF7AC41C5F05708C523503675F3A9C465F6508BD4F6385839F369CE5198E6957793C03F29EE38F392F73
    B78EE11DA7116CEF9B35F57E09C26EAF1A756B7CF762BCD905AD2720826B5CE8F4DF67D770B92CAF248928C09B9E50F93EF93AC9DD675190BF21C274BFA25D472A671B750D325DADAE1EEFCEF17D29A0A723824B7C5F5CFF0BD7C07F3582ED6AF0B3CFB9CF7394A3257935EA1E72879E478F4283D7202E8FB9163D5216133F92310F397EEA606BD6222C7AB97AF5BE7D301C47DF4FF1DF674F4F41BA9FA05939BA4F349FAB64DEFEC63F4E6F6067B142C0CE64CA2C73099EBC372C623ED2328A5A6CAA346141435A
    BAFF66303A4E5BA03E039155793F1A1C6B7C39A6596E56E67DBABF4D757B011C40D5D8663771B20F81BE1EEC4AF5D367736539A925E9D35579A9B1B72D0439E9A56A926F9305829FC118F8D7A5997854CA14F52F0BF50C3B1B65BCFE6941336AE2FAD6ADDC0D320F69BC2B7E48A84B2DF6712C5A481FD56BC0CE63EA347DDFBCBF3140A7107C070D5A7A3CCA53068DEB406F011229BE9FD73561370F48B6E5346A57E725F8BF9264D42EC11B5E6575E9863EFB8D5AB449CDFD4E237A8C22B42D2A7A6C936F39C1F8
    A2691A4A73DF3B56165330963139620CAC70FEEBE93D43C5FDBE5EA26771ED8F56253228BE23C876FA1D7A3C21D5167B1E0BF529CFF9FD26021C0C3558065F70208DCF63E5EE2D0236D8A57B3E364ECFEB6ABC9862C7G313922C8F7172A4EFFE8136D4EF551EF97F37DF1A0A7318A4B7CF3712E58BA4843BA5A5BF6D3671B294E2BA84DF9D51DDFA3561BA03CFF9D6ADA4C6BBC8578F4423E67710A565BF2CA57232C29AE4EDAECB749F96C77602C45B534CFE8A459FFE85656796CF6D96ED697E7ADDA78386F87
    F28257E31DDF516A3E4E23797EE05686083F81ED08B9202D73D78E286B3C8A6257EF904F85D2DBBC64DC679FAB6C6EBE24DF673E5CEEAB48F1EC40B27F02BF5384839FC6B6ADF0F3CEE2A31D13C824B467D467A42E62F1322B21FF2AC6DDD3F87EC7816FC7584B626CBF70B155A82B49457C6C398EB90F0FFBB0BFFB0B66E769A4FB364E7C6CEE33AC77E997733357447BA19BE1CE33517BB54690C8933E114E78683473DD1AF61E847153B60AE7C029DD295A790FAC325D2F3B982B4558123D896AE1931679FF44
    7C88783ACDE853A2B76DFC8B3573FECAF3D1554E2F65F1C2A1BC02F4ED90F3154DB0D7590C58D29E2F8DF87BE61495522D5D63F804E3FF848A22F8FF6BF6AE0343C765B2A8F06817C1B9BF139886B2A2C9CE56912D3EEF0E601E4AD80A376B08333E2547E4FD8F38D857FD064BC98799069ABC977CAA3F132C94785A9ABC87FCEC81BBBCFF50F4DCBA813C45ECF3F47570A340G5677F4F5C3F51C9168C1133D4FE29032DE32B29B040C7B964CF3A5E3E33BE3076914E9CF7BF1CB072341F44CC05FFEEE7276EC35
    F83F613386FC3FA16017D79B7A6D7F98B749207FFE0335C62C8B78CA3F09538BB8AE6CDFF61C79FAA404A5GE5G65ED31659483D5ED4132F900FFCF9C3240B2345161B0F5D8CF324F1BE04E8E5AAC27E518DDFEA872D650BC34F363E73CAE9311AEF50869DEEC9DDA3AD9CE77BC54C3F9193708B26E07DFBF2060AD4EEBB2E2CD2C68A8BFEF3BC52C09CDA4FC9147E39538D8ABFB001F67E7FC9204D5EF45B530E779DDED7CBE9842566E427D5C582D3846E5BE144752821F8E143F8D7A31ED9876838F2B723566
    4479D9F37C7C2DB995D761BA57C787BD7DF6901349648F96A7DD91AE6B7F621027BAD8FCF77B3E4AF5A556CE246F85AEF67DED1E87976BFF1B6761457A5F92FCEC312BEF66087027382E5E3E76EE79ED8154756CE2E6DF57E97ED9C829FFDA4057C45819131AED3887BD6A040142453B518D9056368D7B41FB4E3075B8937F228FFBED41443ABBE97CEC349B8C74DD09232CCF58EDB94D6E78E31F7E417B5957B2FF5A83A5018182BFD2424AED3F6914E5E3AFA51152D4AE4E15421C53CC1D4CF46C58EF017C1A20
    372B10629FB9474AE1172953F44C5223521FD0661CE62904BF14457A706D7B543AA737B847DFAE6157FE46EC5A52EFF3E00AB6BBAB33DF76AA5F197103F2E37E4D7E9661D33A878FFF2B4FD53850FB67A9763B209F5FED5AFBD2AE7308A31E3C5BA462F6BA381C13A867C027AC677DAECF6408B634D3F347D244B65156E2D93B5C66EA4DFE92DF03CF5B266E0726F3BC2BD65D8F5D540C7DD081048D54E21FF39B1FD731771D13891BAD4E30ED376594EC27F799DBF19D3F0A30375BF09D3FFEBB7689F7736F248D
    907FA06773FF067D52DA0F3FE946E4F8532F4BFDFB4330FEB7CD54711EF656479C35F7199CECDB065A7C31F61CAB87EC47F9DA9847C2010FGCA5F4E663C7FECAE9AC4C73214F7216B6EA6564FC3DFA0FDD3EBD31F435155A942EEB94E7AB4569FB885D25ACB5631FD8151AFB847107644EB26CA617A69A378373A65666E94EB2994A71F5937E379E69D7BAE4E607A6D368ECB0F1E7EF54B187E0D1B6A776B6B5F7DA98B5FE46B69508F7FF7568C5776611A43E2E65F3EBE67A2927D4521394A7EA269B2EB8E7355
    2A9D50E773701B8E6B05576F20739E46598667779177337F655791B7EF595D3005EDC60AFE62FFFA64FEE2F4EB2B221F40745BCFC2374B1E18CA58675F58GD632308C7E5CE791DF14AB193344E26EDBF22237EFC9072DF7C9BB0CA0169E531276BE5B929BCB5A3BE4470E9D1B17D5149D339D1D33F02124773ADED96F0B873EB3287A279A9BCC7FFAE1CCAAD9392234E8C579C2BA0F431FC79DBDFD96510F1CE8463DBFB314C19010388F35724C820376BE54B271F036E68D8CF55DECEA3FC9BC2C0977192EB808
    EDA5E1873E4F94455F874C5D8973D8202A1DB82E4E6C136DFF5523FEDA5AB3D0247B0D97791E44735D59E7378B7E50C1B7753CE9CFC3431EDDD44F6527E53D4BDB0F8DDBBD6F17CEF12B6BBB3BDFD1DE9E65DB245BF5D6CE7772F7F3546936F6F5BACA6618EDA6FB5731B925C56525C5CB65B2DBB48BFDC5486ABBA74BBA54EA9B16B290BD0B3694A8BF83328DB11E1583774DF2724D061D681BAD5CB77D008F810AA25F5CFADE567128973E795D85B9DD3297F53475221C6E159653B0162B36BC37CE15F5DB3D30
    39AEDFCE771F0B5E79559E0333DFED1AAE4BDA52EA9D267C1B5AFBB5EEA575C5B3E47D7EDE78D466816A6F48273E977DDD9D74F7C0D5F568D3DF9548BA16FA61D36FAA520D7222FE7C0B64F41736348DDF192A4A52BADB56BB60053DADF365F457FB59CF3D711D33BF7D24D816F5635A634312774DD6CB47895D0ECA58E01BA75BD0D56539CF09F3C03C1F2AC31FFA310A77D34007GC511CF35AB6E2A3FE30D67BE35E6011CAEFE2D67E368B7D5B806CA7ACBE4B9B5EB5B07331CB5653BE6212CFB31E765AB7ABB
    453D9CEB8FFB67E7BFBD0CFEA6BDFBB6333952D1133D17BDAF083540FF77A86FBAA93CE3116EBD7C0E796F0ECB28134EF25549F737A4AC6F18A04DAB95F7F47C3525E5D84A96E6500AF2953A7637AA73A44DB5974B36C4F951BF165018DB3A8BFD79A06F9F4D408FG856CC2DF3E32CC56916EC57F5833E4E87D630D0AF71273C624FCA5FB956FAC27B6F8EE2FF5391C6EADAF475BCFAE225F0A67575DFCBD003DAB94C665DF4DBEDBACBD73FE404323A0ACF697BE977D6AABB6C8571B9C8ECBCF27FAA989471965
    EC302A6F3118ED9DA607E5D3CF5769DEB91654660E31B89BFBFB590ECAD727EE1CD9671C571816E1BB5FBD034B976B7FEAA344735D9223FA3D082D254A4F5EB73773F59E3A27E7758A39DCFD0D1E2F97DD4B7BGF66F131033EC25AC676ADE4F65FC3847591EC52B946D5E6C391C9B2B391CAE14D3DCA94B593247F3B9234FF1B91DA8675B55321CB56BBD17737E8667672DCAF1F7D38F4A1D3EC6167BD12B67F25F93F799519DD0B3574AF2B636F9A2C77878AB741ED0BA3501FFA85E759DA56E1C5EED4B495B0D
    ED60E7BB5864E6E3FB2F23C7AC7856595AFBCCBD9ACFC4FB461CF0766395927E705C194EF2B48204AF7F3ECD6D4BECCFC076651F19F8D9B830AC5ED53C93FC09C73EAC727A8B3E1E453EA1D5359B4B62C9453B377B79FBE9F59056C8E551795DE41E072EBE07A65F1B4C4EBE9D35DE366B3497F5FDEF1B331C688D321CAF3DE82B774F75EECDA725DA5663E89E1EB59D36C227FE467F7DC6D9EFF3136763EC1CFCAF57EE9CE77F55444659A8609300D229DEE3B649BAAEBB6C79B89B34D9CE176B11EDA2EEEB13F7
    6BAC63956F6645B60DDC593F2C507B6EE14F4765D7EA65F4E9F33C9B17B74EF51ECFBED26C1D1FCED03CDB767B66E1DAB760AB4D5AF503D7943ABFEF765CD79F2473C6D9FBECCE5F592E823E81483E87FDB5C1712E58D24F6E29636942946FD5C5FA612B131A3D73558445FBD619CDA3DB7EE13BE55D951E7595BC5D1B0A770A66FB692F2767B87B6B476B3C73572F956F70C4AC981E364DF6CE54ED7BFD055EFF1C77242C445A78A29B2E0D7B00CFC66D41FB3BBAAE5079A972612BAE70FB7E6AEDB9B5C046FA74
    61F7946FCBD4F96143CFA85E07B868058F5F6DE5FF7B21627D05BF8DD3FF2BD7A7FFD01C7DDF61057F3E24B8FBDFBE57BB7F7D112A3F35593C735FDC459970CE5B70BCB36E361C56BCB30ED568FD466AF9DF5BCB6F84BA6A51CFEF65BE9D86FC8CD09279699845596FC72D1E7B69C30A335D3F7548B6913740DD592B7CF40C623C76BFC7306C9FD21C21FE4333326769429567CEBB2B3C7353472A50CF453E7CB1836E692757539D5C63E8CFFFAFE24D93E8CF1F304B688E7D7A3D38073F1B1F5D9BA03E11735D81
    38271FEC74F43F5D23FD7F3DFA6F42FD7CFFD4478435CE7E5C72E98B7AFF60DE5C3B5F4931B060A377625E7D4BADC50348F65E3B0FEBE74FE47BAD3D2C52F57647E7CC7A5A60FAFFFDA949F9E596DBCF21F59055E63808F3D7A7DFF34175945DB8933FE276C86BB2BA764C5FBD4DA02F19686F395F714D4C41ECDECA673E97323DFFF1ECCBEFDFFE4978EF861503E70BFEB84F57006467DF1DFD7CBD456AFDFA661FE37762BE7E9C4DBEBF8B4F2070673F538B4F5D074F2FA5A66F7A7EB7BA64761CE49A1E35EE49
    2BB4FD50A30AF358550D1E4FDFEEED4479CB91643BF19F4EDF5EEE44F6613F8F4705990779F9C7601301B27661389021B8CBDD6C517A0AC86727B8FF7C03C7B60B38B10D5E0D8B918ED94F4476112D97BF45D9041BBD4A23C8F73962AC4152E26F4606FF9D724EEF23956786969A4D43D2BE540B297682834F483A7D3DD84F98C74F08F97B51BF1770E744DA605B007A7723FF86A94EB7BC6545FA06C3F116E12397736BGAF6757D3664AFA421BC6367C5FD7687E2D97EB9A7FD06CDD5EB55BBB7FFCFB0EF77EB9
    D33197797CB0158F0D202A727907C277D51E158F774F71345E66CF7ED94E575BE201CF864AA07FFCD731C75A6905FFBE29585FFC47A35BC45CF5DE7A673B0AEFA8440FF079BF29580B75ECCDD1243BC23167B75E4BE7409AAF5758FE2558A7FC28F9F84697E9762699DF2ED06C959E71227FFC1A7CB32F817D731F5CBFEB01EF836AEFC07F3CFA192CA34C8B7FBC2E580FFC5B8B7F2C7252BFEF2A107544B50DEC7977A976867F6EC57FF9CA3107771217EBEC5FF8691FF7AB7679421BBB06297D0A2787759A4E0F
    94FB036B3D704FDF4A7DA779679851FF821F5C401EDD51BF4FAA7689DF7442BF77A97685BF73E2FCEF7252BF4FAA765CD21AC6367C772D13F5FF6405FF56AA7651323C6CBF6FF137C62E724F6EEAD91731F5F856ED6AEB36E95AEE2DE2AF6DB6AF4E2CFCC5E7D6728E20EFEE64E7D6EA01EF836ABF003ED92758CBFB450BB3AB450A3D340987BD774DC6AF4FAC575548FA1E9926B3AEFAE5DF3CC556FB2797E7F266A96E510C70728C60FF3CFCAEEAD46C5BBD53FCF4D84AC6314221A923726D327EFCAF7A4ECB65
    3E137C73C151F7821F8C14C17ED9215823FB460B3EB3D7316F1663C55FE974326F5C2058277B38E9646BE006E27F6E93AF7A4F49FB64F429DE0E6F4FF773B38D4770CC43270A7D38E77ABCBF5330CC1C272133917FD5487905C76BB462BD48B70E3175B1FA07D23CCEAD053DF30C2D2159BAED8E480B6D2C099562FE0858F9CC3C2F7C473DACBC6F20AD2794289E488C54FF905FD5EE34313259582E771E729673B18BBA866ADBFB5C753B211B0E3335D0695DD0162A83EC6D3131F735FAB17DCEF1AFE0174351F5
    1249C7FC6FF136666C686A6620408E9E07C2B374580ED99DA22A049B799DFEF64BD18ECB5F826467E382A0DF2187F1DD7DA1FEA6A68E78E442AAAC783EEF56A14416DAF07D3D00303D9C2B823E7E902E414F6777191B019FA0ECA9478201EFFC945766A3AD2E564DD9DA17EB700304E957661FF329C33D4E2EA43DEF4868113857A1F3A75E6B908536A5GE5B75AF28A9B051D52FD197C7D698A402A9BF15D76324F5919AAE9C50E1DBC12FCBEF981FF6F2D5B52E1BB4A1EB5B1945B444CCDDF981C4FDC49E99F5E
    446B4DE26FE620B41FED646D0B4E77D5AA76F1FD4FF8523E44FBD4D7B98A8D5A7728562C11CF05891FE827F7B46D0D3447C36FE87A9316C35FD78AE9C4BF194A77F86201CFA32CD05C619BE24D097BA57A4E6D4D6E76DC629BBDFFC7B32DD1EFDFA74A2D0E41FC481DCF895F09277B5F728F8B5FA9055FEAA016DFD1C7E7DA58DDA2F653192EBE87265B5102699AA1EEB7D0A0D01814CE78DC8CAF739840628F637E1041D4B4080D1907157BC39FCFE3FD5026835B25BD8D44AF34EB4FD5AFD56C713F506CF95F1F
    4F6F405A8C3DA3FBF91D75E386C3D9BF1EBBCF5DF603A1B5E06EF8569E746E2048EB9276D6B549674E592F748E9F3F231659525D047B85890791ABED263B8A5C5EA711522C679F975D267BCE450BF4579C7476DE88717EF4B97FCEE116D13CBFBD0E70559C4FD360E24F6489BE5767F71AC158A8A366F7459075BF4F650D5568FF0563E99A7DE6521F89E1EDC7D07F38A16A3F194B0BB92256FF9747630F287517137EA4882BEEC17D77D58DCD7F0EF5CCDEC80BDA7FFE0E07372875A7D5217EA888ABEA45FBE26A
    795DCFBE40878345GA5812581E53761FC63E70B58E22B2BFBE36AF8DF40679CBDA6DB27C364EB71904B7599DECE05ED6AFC7D0963A5ED6AFC9929DCABA0AC308D47B3CB8B9FE768BC73E30AF3B1CBCD1E77897FE8F31E8FBEF9C8169363C55F72DBF1BE1E3E959B25B8EFB3265D73FB901E737A7E97D1FE1DFC1FA7D3D32E27B91EEDD2172B21994BB59F427ACD682F11DE5FF7A3749C6077ADA419547ADBB81E22517F9669CF073046F61A3B590656BFEEF01BCE3FFF34DE98DAFEA7DE6467045B55791D427158
    F6F5FE2F3F0079CD00304A8E4CEF3FDB3B7575CFBB4E3FAF5B21567F9D47C3BB547A6F32217E8888ABB06377247C8DB8368F18451CA0GFEC301587CC74479FCBC4609B60B71BF91FED325B8E27C7761E7E832ACB06EDBF07C8FB6968D120FAA0BF27CFF145F1DG637FAE1B59EC47B39BA26C5B966D9C60A145FD2811AD1EFF0B79A745B8A657DBF01CBECCE3F76ED144F2E6A196FB946B6A2E46217966C3EE53697B66FBEE53697B464F7919841FE3EA5F8860387FB135EFFCFB98FDA388428CD64C6F27C36C8B
    EE67ED5BECD56B8F63F837D52DFF857585839016CC7ABF9BE2DF984257F5EAECEA7D77F13C5E26563F3289759BA1AC5AC65FA59E22FEF1B7C471F135FE87474B0F2B75FFC27A2BA0AC78B86A0F98227E3DDCCF5689357EA60E671DD06BFF037497C2582893283FE008E37CC3E26E26517FBFE26E26513FCD1E3B1DE06710D07F4F06187F85BC1FB1F6357EF20E475B557A9F267CA7C1D875C91C977DF92F6BF515D7773ADFD7F9EBAF6BC3AC66E31606B35D9601256EE54FA0DDC70F76DAE87D667D3DF904ED6F45
    FB92C55F362BDDFB3723196EEE8FB9A97A6CA8780D87B2BF024FF1F19D5A6738B7BAB0DD4AC9510F9BBAEDB9791DA21D68470F70B516D240AA995E497A71DA4BE077D28AFDD68B2B33D336DE9B3B85C8483A48E5317030CE1C377D310A2DC3EC62EBCD7526CE0B9D775F4BD9D9CB4FFF6D269E91D63D111F9BBF2A54DF7128155B9B85B263190D3C8E0B6B704CD68AE0C5DDF89F4B44A2F6A84365FDACDB9C9DD68B5E46024FF276BADCABEE6C4235629B39FCFF60C301223BF02D78970AB346B38EFAB28EC963AE
    BDD3A7F6093AC8035F2CEE31E6A54AAF0F3FEBD788D8C9B70E29C5F4DFD2C337F64D4179197A35C5DFE219F6BB95AB1E6B5EB34D209AF365A8D25B4820EFDCD8C1DFF0B70E0F55C7300C923B310CBA79F7B272FEGFB012AFF403A69E941765588187F8FD8B7EF16FD232C9BD6E0EB56083A908F9DD2FD7C064E23467E003AD238CCC38F4CE5004AFB30BE6ED21C47FE552375DC91F794FFA7FDF7D70F035D23A11E1D2E677317DA10ED8672858A860AG0A83CA6EE15F5C443E222FE130E7A811A975B354B5F371
    1B5503D1FE6F60EBCBA590DE85D48FE4866AD745771378E0780DG0A1578A469B78DFE339CD00E8E2D1ED29DCC587E52E1CFEC2F56C92F24868837828DG7983052862C7CAFC9C7CA68325CBFCF61F78AD045FF2201ABE2D1EC69D6CDB6E9B51DF31F7B0ED1DF6DB27E5F31759324D52C979DA491F7F24E78A455F319E5FA3B99492BADE9B819D09878D8AFD725F47C7C077A5A320A3C411277B94FF2F9C815DFBC6C0C77DBAB9CF0795FF3FDEB57C3A7FBD2CBAC4BFFA78006BB9D75B8177F3AE5B817D3D2C2E83
    5A3DAC47817D3D2C338714FBD9A26F718ADFFAC971F77B88547939915061E81673F4DE717727EE77A57E773AE70D000EE6231CA733626F3F0D006ECF7F0F3E33232FE352C5B9CF790A3FEF3AB07C3AFFB582BA3EB9AE6729D87177FD3661577D3BE155A1664811861CE75BE15E92520773EC43B81C7BA675615C37EC9C0B1BFF4A16D38AD4F38A67594B4653BA86E08127D0465971A8A36E944A8865F133CE5BF28A01AACE637CF91A623D3D8BDE5C957128114D1F7743245DCA657673E2CF6608F527871FA336C1
    38834897A888A8DC95BFC6629361B7954850AF78FC693784FE2B006A7B35FA4CBA18303D452339F93FCEFAA579C1F8B0D084D0ACD012AAFE1A44E71D0179B7D0699941D7CB3F8D70EB859AB82355632F03895B274C724476901D74CA0A0470B820E42074B36C3BDE4E718BA53E9CFEEB009AA55EAE7D0E025FG205033DABDD1BA18307DAA3E2EAB7E3ED171775C43435F4E2BC6C0475D0A317581455FEBC7E09CEA98819D77B449F9FAD071F7D553706BBEB082BAFED05459D9455F93C620EC8BC7C047A1C51E5A
    94FF3FBD82E5BBFE84727708E26E9E2378FB57884C310F0E000E450ABADB29787B3191283F44E155A166B8FE6DB8CF0A07B1A47B9C1D35217B662B4F619CE7FC870B5B8F3CBFD068B91CA7CDB263BCA99A308C12315F0CB24A87D0460FF8DCAB7023008287F01E743562DBEE73AD1E4C1344F923E7D7AA4F9B31B3C4FA77DCB28A9F90E3E4420073F9A32173BA8B5D5D4AED9F4D4FBCB29D79675176E4DED6F5401B01864E633E4A77F5C35B472CF41BCEFF9F7387376954A46D256FE276871CD76F634C60F870F9
    75BECEF09D56EB980465DD407A0E2475E787E0E197E8EE5D0A75BD76824D2DDB7979140BB0A7862A3B0875EDED136B7BBF1E5DC743F55472F3077C7B9397317C7FE39CDA79679E99DA79EFF11BCE3F7CDF676B79C19755657FAE47C3AF2A4B5FF1044E98C0D841A8BA6320793607E77D49CF06186EB12F5309FC99F95D8F0CD2675742F15FD16A7C3EC7FE95GE19923F0AF60B6236BB52C3B0D6E57309EB06A2FE1C59A35EBD80F9A7557301EB4AA57308496AB49E5FB913BCDA7C96E33C65687093DC269CAC560
    4539595F733391469FC17F77A3BCCBDB444FD084G9FC1580D9799968BFC92E12107704CED8AE113789D8A39BF3665947F983149FC1F2B68B5EBCEA5E1E67EBED19D70ED04096FA37BG9FC0D82D789EB370110415737D22C41097C758B8AEAF1971048572761FFB89BCF7DD02D8AA472A012FA76C573C8D7B3EEE4DB193A63EC1598F3C9FE1D3B99614EC4D098692589A0E85C31CE80A7713BE06A5C01C84429CF6AC2BE44282B8168E7132FC902BEC4532AAA0AC6BA0FEC32B14308B3C2CCA47D8F36A897B4BA1
    BCE7EFA46C31A3D8D65D04BD4E57BF33A03FBE04ED96E72A812BFF9D73E667189978C00AF78515D598E1393C8C12G0B7641BE61FF8CC36B83635C26536F83A70E9BDA1FF09BDFEBC970D1778977F2BC59C75DA7D40C43BEA195426AAF457CD60E9FDADF36F50869AEFA1DCE642BF08233BF62D2F5FE67F1BC7AD2F5FEFFC1EBCEF190D67E932C73A7C59F81FCA4E18573783B9F402792D6B21B7B7DCFEDB979BFC56C035358960A88BB584F309A600D0475B6E3DB68A64C177B1A8F700104FD467B42A860638833
    F3AC9178B4424437E7D9DB4872C5ECBD478A00AFA74C4A7556GEFA6AC0AE37D407B9216520AEDA10830333C2D06839FC358F53C0FCD84BE1330F7B916F799683D8C31A05E4756G5FC858B96AE34D043D4AB1DF6003897BA7759B91046D643644821FC458B3C25E4FE07E74B3441670BE3690788A4266D19FDBCB58985EEF9801F790B6C714817021041D62D89470F10435D03F11CC1878FEEFBA7059BFC7ECABBF17D788FCB5E123B956G3C0330157CBB4A3E40879116CD6F000492F602E3F1400FA5ECB579D5
    86E12D5C16DCBFDBCE119F15337083609B885B4C7D2A8D78FE42BEB90CE565C758B2B1AEG9FC9D807308578D4424458E3389C6A63F2445EA43FAAA62C1757E5A570F517E31FF3F57B507A58E03769747B58175C26536FF3CE716734364B55FD4EC50E5BAFD777B9599D586774C3D89265F72AF9E8FD652CA126EB74BA1D4857077C19327A8AF5FE7F43713AAB54797DA9BD2FB6C2D85495F836FF27091DA1AA3A5216D3855486548F648794F2A54EC55BDA5905932E4E256C6B6AF23073BE1B59B70FED1D4AA3AA
    688BC715F90C8439F1D78A1FC9065F74ABDDFD172F0157D1363F7A3BFC2D9CAFD460A20FEF72E7D54617C3D800BF56E9BEFF57D47C7D2D626FBB6B06FFBD6331915071BFC3FC46099BE23A09DEFFA7D61A8771E7208CFF4DBC0863D9D7E966C12D6833F99066388A6BF317531962C440D32F9AFC9FC224CBB9A2577D7B0A3F4F9E997EBA3AE684F434374AF9BA2178BB3DE578F5CFEE9DCE9DE24D6475396E3F2F7E49DCDC0FB1DC0D67C5D7717B8C4D36DE7604EC464F86ED27EF046F65734CF208DFC5E96E3F28
    7DA67B8D7CDED1711D75478E61594B302B353EA7E44CE9547FEE7B9ABE970A06F4F1D7635D18AB7973EB55B5361C5AEB646F57EB4F6DDEFD9075BA2E915FE477035FE0204CBCCC772FC34E5F879FD05C1F585A287FFD70535C26C81093F38D5AF4184F4F5218EC3229C0FCC3C6AACB398C45B75ECA82E0FE9700F1FF59BA78775B1F66F39066BFA114E6C21B73775B3F666512G614981E8D7B21F4F54DF8B7378EB69DB40CDCC0E25131BA56569F13A2F4117626DED9A5C97CE0867EF089FFAAD2E5BB51865FA7F
    39FD30F34CC246237C193B60BADBCE71F5E8330967B5G78606B703D1945D417F157093A9C8B3F99C005D3D1F7A93F83D2484866F514F7BD04DF0FF2D37833F7AD708D043D436750230077A36CDA2EBF93786CC044443C309FF89F42D6D0190587E2FF9BBACE6ECB6ED77C3DE65C7077AB7BC7C0471C89F21E96A97E0E98BF7C3A7FB02CBA044F3FDC6C3E5F7C30986BBDA6905B4A12F90337156D7CD9BC9D629BEE40B49BE6EB7B4DACFE9F29E8BF1F77234FF75F602A5FBC592F5FEFDE4A1F5FFDA01D7F8D682F
    C1625966C6DBCE6E0DE843ADCD5AFE73D7CD283772C651566A61578C94D30E693EB3BA771BC90AFBD4AFB16A771B2379335AG48713D91ED3273B69481FCB459F420C93F5FBC496326C23C8C0AFB31F970FE7306E66CB72D23B14D1F1A1D7B4D37F91CC0888F990DF6CD65FDE9FE90BCFF86E13A2B8EEA7B4DD03A07290E625D6741589BCBE3EF9B259B6FE66CAD64FE678F7103A84D03BAE3EF44B159072E2631B777A6D7BE7461A1FD9F1A4C7B50A2C8D7FA9316CB91AF17A060C3EFC29B5AF5465EB354DFA75C
    A4FCA895FE8DB7C33FCDBE741AEA6C75334ABE345545585B42EDAAGB945B723CD62BBE175409BEFC659698774FDA8175717AF448B20382B5D0C3D7BE96C4D3A8553DC5E6A6CC33773B89590DEFD8B5A75D36ED76140C7D13A0DBAE3EFA30DA3A9946F48AC77BE54BF8B53E5D23A87E68D6EC3F1BCCDE930AD27B298536CBA2775A133CD7621D94DD81721412EFC68474D7ABEF4A3AF03A8C8979B0C65524E314ADB41AFEEC59BCE6974C317D3BF54FD2B70A1DF788D824ADA0A69BEECF676212A63328FB5396807
    FAF8BF9481F222EFC51B660B3E85788C32E93B0BFE484463965FE64BA93F8D631EF5538F85D0BF94CCE91ED575C3E3F91CF888CF3A8D6D7A0237373A5BEDB90D3753773DF47A21DB299F72399D67A2E2AEAB7E3ED47177140E619F2B970C000EFF1B65BCE5D9643FAFB78F3F6EBB07D507D8CBEAB0395E57ECB6395F57B41B7477B50F1B347B1ADDA67DFD4DBE7EFDB967FB26FEFD94773F82EF277B232CFCAD75A074F5045DEB437D2FE4422EED47B561F47253A6FEC7D5D18874C9A108D9B8D68FFCB7E1296D6A
    B2E7E906DA4615A1FAEB3193B5FE6B4DBDC0EAD25F8BA4BDA3A8569B6ED77C3DE6D8578524E704E155A16DA573FEACG4A7721AC44EC9C8B836CD2835DA768659D32669386CAFB6162705C315B0B57DD49F77071F3A5FF657BB42CBEE3C370F9534FAE5B73FE6B0859A34A62242CFB77E0F7F3AEABF77A5642EF8E62F9AE439D505E6E4033B9638F617851FD875D954E6F9E8AE5F100926F40FC9F6914F54F736CAE881EEEC5171C6E23416E5BA41BA5FD5DF23A0191ABE7693E36D6B7BE2A3AAB527F8759565143
    F48F37AB1F3076483AFD873B8FF3F93953FD1809CD5A7BBE7CFBE5D9477BC6B69FCFAA3E15D1B8426DEA3462DB999FFB642322DD9D20F615866D2464CEECD7B7513C2C6DCEECD73F67F183018F870A3D935BD540A9D9F7049777741ED6FC2763D7DE342BDB945F5CD8B042657C3C621B9BBDA35CCE6ED1FC0BE31C976D244E291D88ACF71EF7E358984577BCF2E70F6C98D65E0FE3D8B2795C447332BD07C6389E46A8F41F9F2C9ED4ED6D55A6ECEB85F759F26A6F4236B61F3E4762FB97363586FE87C9B47009C0
    E9F7E13EDF3CA06B2E7462FB073F38A827DB6E114DA25D6159F23A3A91ABE721AF5C4B6F057EE80EECEB5C88778B07674A3A3BBC1A5708380F9D54364D3FF879BD6548E2D97728911EDFC6527CB2BB94FDB4D971FD1BD7C6389EA2674B3A2B3D18DF5ECA63E0B56423BF143E65C563E0F8A8FD4B0B4FAFD300B75CED4BA9389B73FD7F82D977CCAF661713974A691E77E29CDC2178364C27A3BC3FBC6E657C7273B25956CDA35CDF3F2E50BD4B233ECFEA47BA636615333CEB1B53945F3719F9EEE45B6696FA2720
    1CFCF41D621BB75F0EF0BDCCD3FC8B27410BF173A19AB72D100F603B31EDFEC26B4F09F7E35BDCA46EAE3B876632C05577E03E27A83E27738FAF6E6AFFDF11EE019763E631625BB6D5A3BCEE5E6B6538F9E825EC6BB3A35CDFAFD1FC4B476A45389969B4EE0AF577E43A7F2B719EF15FD9B77C7AG31BB5EC51CA6AB46893AC75C2795813F31D29C31A61D40577F1281CB3D876F538AEBAFB238DEBFAA38D7F91F56D6FEF6ED13A804BAD33B45AE701CD206EF36DABACED84475D962DB1A57F7A83F25D9FA2F3025
    9EFE453DE61F1DD45FEB46424D905EFFAF5E11E51A4FE4CB5F92B8E4B3BB2C827F7F2ABB9660282AAB2D3603C295ABD85B6214C218E2895FG86894AF786BA29C5450235BAD429C39DF4D2F4DAC618FA49170F418821589AF4AB54E2058D79D0D1D012908249C40884A11854E633F949EE5C5DECF6DF42020C53F36EFD773E4FEE32EFB7E433E466E65FBB771CFB4FBD673CFB4F3D6F5E738A8239AA7C34046B24042F29BDF7D13B47EA841415B0514C9E2BF9E1637D055EAF7AD0D83A507BC5F3AEC63797AD010E
    5349930362BBD2782209C1719DAF723DE84BA02FB4112F5FB6C659DEE7146D9D9BE5BC4563147F3B930D6DBDCD6189094676BEAC62A9CE053C7CC9A296F7C0DBFFG6043A719310B55E163B00616533A30F4216574FE14F1C71750B1E24CA4231C9E267044C9C6B9FDA1620EA6C3DE41E4AE2739BA3B9C827011134D4869E7D15A534CA86D6905A86DE998DBC71D9C949F1642E7CCB64AE90FF8FE66C15E3EA9DCCEB5BABD8D857868A9E664B4A7CAFBDA9A25BD25C7E9CFBF2176B1F50AD1CE93A8BCE50AD1CEC5
    421E16C05E01297C7C6966F66E670CG5812295C4F29EB977B9D27F1BF679B0AFB846E6BA0B92671B23E6D60E58F81D872B4DE46AF9C3C0CB4D146FA0A3BFFBA0CB3109A26F3DFE93F661BF7371A0AC94EF01736E8E33B307167C5BAA60778BE879D9799EF8F51F7E6789E4FBB1D73FB5C4DE19326F3FE6F725233D4F03F9ED2DE12B83357405F5B6087AF99AC3B013F37A9917A7D39A6CEDF12667A584598441C08C19DA7B5EDBA2339DE9103F882E983DA8753E9EDA0D84F1F8502757C10A61E418ADD1C0A0117
    4315812D0335F97945E0B9BCFEB1D88EF7E8EC60C71A6B3DB1304501FD26D81BED0D41F2E8EB8C1643F80D8DCC56DCFF9083FB280BC19D5B5B239BA78B4252059EA7BF8FCBE7CCECBCDCC7472C7DC946F1F2830517A69947491B5B79D8D686F989C95C1F986A086ECC4BDDD1527DAAE2BA56AE977D164266994676F6D3F87E8CE3FB7FA246EE8B645DBC033777D1BB563FE6865361C665B7EFA67B5DB7333798D915EE4E77918527D679ED06DFB9849D63EFEB970DE3B0137117A360FF2570B19AB863FBB49D1771
    BE99728AE6F13E57537D1C6CFA13C33D3E35FD601F09F1B1284367D45B743566BAB3863186778CE89D2CAFFD0E7AE5C3C01FA3E6F1DFEBC591429260FE0600B551339098C3E009004D95F18A168BD8231B41E02EF99F07A5D058FE38BFA6E0FBBB6959D8388F88D82D1717B77CBEEEDFF9549E1361FE99245582DEC0619B613EA0994ACD667031DEAEB3448D556EE53D40F9CA6EA3DF193308BAF2FA418B779D3F3E76EDA96FFEDB757BAFF753F8C4CD50CEC7B25FEB79C2916234F5FAE40613D9CC4F58C07E2AE4
    6E67EF235F17E66BDB4BDD16BE6A4D1F2DDD5F72396937893C36AE7C16A5AB7F962AC74C5FB71B73B0479D7CED01C744DAD6A96055C212A18D1D4D764BB13A0FBAC36FFFBDC76DE28C60A64E666BF2F6EFDFFC2F5471BD6AC31CCF54FB1D9EBA7990F0BF5DABD8D3D725D92B2B7A9772F0263B7E538B8AB2DB2BBB5BE5DC2BC33E574C466FD150BE3FA3D47EC611CF1C2172736E67BAA951FC0FBB2528198C44DA2C82D2D6E215F7C91A6FEC1FF53DCB8CF3BE764DD53F64F336D9DBBADD2D6F9C30949D30149E91
    6B31FFF4213D1D3479E5F6BF464D63CE31B162E5B79F5B76C1DB1B6E676B16C54D3A6FB732587E27FC4E568ADBBB8B6E4F6603959EBEFF9DF9BF1F8FFABDD8E6AA5C2F0634D148502A79EEF739B702587EDE64792264D76A7CEE9756096B2779F3783CF4DC875F8F9D90308F1C9CB6F58E6FEB08A7BADFE3FB14F427A226E3E37AEAAA43B5F30CBE4A73947E529C230F526361FAA4A94EAD2DA93C3D433AC20DC7CBD214EF882484771BE9G4B1C9B8CFF83E087660672D7A7F4E09B4B8CF96715FBC70832143988
    7DF656B5C37E8865BE21D73A67BCC4DC3F28393E66997871FD540056414654C9543E13217DCB6672F1F6070F0E93F03FD6408AFA68587BG74D38FF0D82A1F1EA5007BB281BB6B66E374F981DBC41F178438CF913087BBF8F94B846CF6A767E5350025B9F9F9E982D66F6434E58FF258C18727BDAFE037B9B8ED7303FCDCD95425BFF3117D8922303C77FCF88E44ED8BB85D5D6EFA67D57EED1AF2AA0F29D0C60AA82724C7BF7ED6D3792C017C17844EB3FE6CB73CBE29CD727924D6DAA29F47B6D259B54FF3EEF1
    C1CA1D0763D81B3BD2514D5D73026D11BF0399CACA849CCC3B94783CF96AF32A6C3B68206DF1FA8C6DF9114ABEFF3EF30BE53EB8DFCAE135F05FB01F7721CFD159B05EF2BAB8EF0B668773169506371573D55ED8FD57288ED783BCCD54B76B38DA5FF8872F2FE9C168F3BBFD5567DD2056474A3E2DCC55736BBDFD3CE3BC2CFF07BB2BDC251B667FAF990831983D9171CA1473DB2156DB69B645AF9D07FE60666F7B2F018C5E2674B07FA46A9FAB3F6B84DE33B81385FEED1C491B1F4CCD5FCBC247191C2168A2F3
    219AE7F2DE09BDC359F7DB2972FC36433C0C6F514447141D83A3E3706C0AB5B22632BA5241E5F5ECA137416EE6D5C693ECAADFBB9CDF8E88DF543BB46C5978350373A58B3E06501884ECDC986D560E73090833306FB98B0B81F3450E8ADA8E38E910729741988B298CD283A49724A110C6C2CA04348852CAC8EBA1114570CCC25A876948E29EAFE6568914E5EF71E29487CE93A506737FF107167FDAA82FF93119F7C1CF6856E0E420999A060E0D83C9EE3EC638C940125DFC0D90E12CBD5F3377FEE6E924BD7C19
    25FB6C214FAC0D33871FD91AE08FFDE6E932DDFBE60941126CE88B6DA04F860117ACE01784ECAEAD93E174653F00AF24FCA11C3F7CE77025142F4B94564063BBEAE017945823747BF050E4C7270F532E345339255365E2773F25B8CE0FDF1205BCFEC7F9F4FAED9A3E1F9530CBC29767BB0275F329C32B9F86DB6788467B33C30B371B56F1CBCBEAA9401EA7D9B249D1BEE3AF134DF53ECE2F64132F48E41B669B75B249442F52832632D9436FA35B757304CD63F75F14F7FBC9F7BA492EA259EDB61757E12BA6D9
    BDB6D737D4CB526DFE193CD90BA405C0D2E8C712C2CAD86F355925230DE4CB1B2F3D05224BA43D312A918A21F7DD649B12D3CB364A8E9AD5892CCBA63B55126A7029D1B20E8668C112D7D2D3DF71421F9FC933A205C0DBCF861CD0C90E923A93GB5B5B5A720492F09A6D7D39D2E6AA979A86319F19969A4331AE4B31B2EA619E81850F4EA3755A483EC1A71257D83D1DBACD82C45A2136CFA1753AE79A8AFF94118DBAD96060038D975356595753D21EE81D44CC74C9CE583CDEF385BAC96858331B34EF5FBFA43
    4C31D8A09731DE2B3349326473D8D459545BFAA4B4A17831402C16E41E05DE814ABBA3DD16496BF56053B96DB6D932D478BAAF7B11A20F5B18DAC896FE4F91FF4BDBE0A28BE465FEC4854BD349F2E98DFEE6297E5ED88529D2BC60F5270EGF833DA2DFD48C2E9GD266E2934CD4C5710060D5E8ECD8FC10A222219415670D8B20AF2E94CCCBA82174C617EB31283896AAF1C58B6189D50505D0F79F0CF2CCCB888577C676AAD62720825D5F61265DE7F3DB7840E23F922E25A0533A4AD3C83C9DCD48D26D01E984
    90CAFDBCCB5456AC34F927A48FF4E6AE50A30A8A3BA8CD27E729F53678ECBE0D192A7D64B6E035C3324B1FCA1EEED35D0C0F6C35F73A2D4E9637353B47ED353548D61033EC4530412D42C37AE2E1F332E3692EF752C9D6B559566614DC2D7554C72AA5F9742ED2725BFDCEAF6B13F730DE50E5733497564BBE70350E561257A99E772D30F8E46633DA32D3D3DC1553A5F9542C6D1A2C4F4F5502B0D9499EC9AE04FB562DEE12C929555A248CGCD6032B5014B5684AEDB136232B5014B5644DC36A66C5A0ACB51E7
    13493F437A1D829999BA0F525A916C91175F76780A447FD5662713F468ED9D926BDE33AE63B0CEB944DD33653DE86302AE3F0E3567D8E46D614196F83B0A4D34CBCF0415B79AB97211DC5D7A61621F9EFEB675298B7E8C12DDCD7E06CB537592F8D1AE181C36D65AE45B85F89EC09ED5E40B379386BF1C3442286327BFD9FE790A8B4CA53F6D1C5455AD792166F299EC2325DB069B320BA936DBF63A8ACF5B7C8E99FDB3301ACCE18DCC5765967A3C20CBC4003F1D14BF24328A2A1DF3DE7B67BFEAD6A7E71074AA
    325555E9EB2D02672653D7CD36488E1F64F7F43ADA835E63E534204DB482AD4E34B32038B7C5F331F1D68C26A0187CAAF04F705CB539D5690484FC2410E26258EE95982DA79CB6FCC4A5DFB5A45CAA3BCF64FD6BAD795DDF1E5A5D14CEB6699B85C3A3BC579EFFDB274F8D9CD88C9C70ACD110754E2507C65D7B729734A015D4A6EF2B2EC73B5469AEACEFEBF3FAA4D1GBCABD07C9ED1BC62D88DB8BB82F76C2AF96C159650EFA549F09FBAC47F97517F45783F08C20AA82428980418E66C4874FF467CGB5B03B
    4C0CC2B8AE58D1D82BC0D372EF1EDFBA7609E3E9EB21F5D50A0F86424ED3314EF43BDBA45FF793C76D59B6F255B0540597CD02178B7E1D5B6982A7B13B926C3233BD00F0FFC07BECFDE27E59E24E0D7169AA8D3BA290028C99688E75441B6C917E93A9571C5B836638D5397CBA9497DF86BDFB883585BFC488E6E3DCBB7D5F913109A0150B52FA30C23C68526B73A61DBEBF0EC4B236963FD11DA5618594C40555FF279F5ABC9CA14F1C5777CD712A72B8AC6EF5F927CE17474D4BC519A19835F9B81C04C252A18B
    237A214F8FA2661B73FB50A43FAA1FBF0EFB1D0E536934443CECE0AE476572DEB83988DC2CEAFCBFF4978B7EA6463D4E12821AB5166856A72E97C43F4293F29D8457FCCC972E68B902B9824E38CD4F91D4E42CECC1BFACB1B69CAE09FBDBDC266BBFA271FC202165FE731E0F869DABFCA4C67ED97F38DC99777ADB9508522AF1554A34D52B48D8595331F96E7A41611A3857DBDA34637699693269F1D160E2D56BE2B3EEC74D5F7AF85759A62253D984FE2832E2E85A8F5561E34D693171177B4D67663857E11ECE
    079F1A170DD8CB6752A98CA79D8385563E239FFA0CB52FEF443DAEAD516AD23C5EB0AD9F8385567ECEECF4F9DDF85D9F773ABC94ED5F2A3CF2B25DE7697031666258742D7D6673C85C6B30CC2743A31158B81B8BF361D8431B3816G6B2E680796E34B69693857E3DD343EE9DD65A9533E1F40459A4F4546B70D1A3F063857D933CEE7C7A3709554659FAE1B22305E021186B9E869078E8703DFC75C6B549B38DE4BFCB788A444D68D92330C4807F4DD14A693C33A8E9F95FC0BF730EA9E2EB77E7CB08FEB7EE071
    797DC11310619555DB0345478F87CD8223EF909B99BBE8929A9FA7B6F26F20C9A0718631116903A62119F1A2015903A601149B44C6968C1A0496470984168E1A84D2EF909BF9E450A474D8D889999C598876BDA9A0137B1EB458485893DEF566D4D1C6DDEA0C623B291719D3A6056376C1F6F4064D00906B3ACE291093E5CA15059BE75B680C6A77A1E6D4B249E161550AE4F5B24045DC2C15E8F184EFD214030AB259EF76CCA37237569B22F61C31E4EA53F561109F73B341A1C7C58E57F97B60A90A37057CD01F
    1937059C977978D3AFFC30F31AA9A7B1A89F1EEBCB59BC0A9C4B4FCE6767EE0D675EAC9B583938528D6AB9CDF68670492BE832DE008F5F404F719D3CFA1074F20E2F3CC52EF75BDCAE59667A2A5C53DAE36B31D5DC1171481BF21E6B692BD83E1F63A819AC6F8FD7116F8E8D4D7F81D0CB87888C2DF99DEDEEGG543B81GD0CB818294G94G88G88GE503CAA98C2DF99DEDEEGG543B81G8CGGGGGGGGGGGGGGGGGE2F5E9ECE4E5F2A0E4E1F4E1D0CB8586GGGG81G81GBAGG
    G27EEGGGG
**end of data**/
}
/**
 * Return the BUIMiddleToolBar property value.
 * @return javax.swing.JToolBar
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JToolBar getBUIMiddleToolBar() {
    if (ivjBUIMiddleToolBar == null) {
        try {
            ivjBUIMiddleToolBar = new javax.swing.JToolBar();
            ivjBUIMiddleToolBar.setName("BUIMiddleToolBar");
            ivjBUIMiddleToolBar.setFloatable(false);
            ivjBUIMiddleToolBar.setBackground(new java.awt.Color(204,204,255));
            getBUIMiddleToolBar().add(getSessionToolBarButton(), getSessionToolBarButton().getName());
            getBUIMiddleToolBar().add(getSeparator1ToolBarButton11(), getSeparator1ToolBarButton11().getName());
            getBUIMiddleToolBar().add(getAssertionToolBarButton(), getAssertionToolBarButton().getName());
            getBUIMiddleToolBar().add(getPredicateToolBarButton(), getPredicateToolBarButton().getName());
            ivjBUIMiddleToolBar.add(getPatternToolBarButton());
            getBUIMiddleToolBar().add(getPropertyToolBarButton(), getPropertyToolBarButton().getName());
            getBUIMiddleToolBar().add(getSeparator1ToolBarButton111(), getSeparator1ToolBarButton111().getName());
            getBUIMiddleToolBar().add(getDependToolBarButton(), getDependToolBarButton().getName());
            getBUIMiddleToolBar().add(getSeparator1ToolBarButton1111(), getSeparator1ToolBarButton1111().getName());
            getBUIMiddleToolBar().add(getAbstractionToolBarButton(), getAbstractionToolBarButton().getName());
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjBUIMiddleToolBar;
}
/**
 * Return the BUIMiddleToolbarPanel property value.
 * @return javax.swing.JPanel
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JPanel getBUIMiddleToolbarPanel() {
    if (ivjBUIMiddleToolbarPanel == null) {
        try {
            ivjBUIMiddleToolbarPanel = new javax.swing.JPanel();
            ivjBUIMiddleToolbarPanel.setName("BUIMiddleToolbarPanel");
            ivjBUIMiddleToolbarPanel.setBorder(new javax.swing.border.EtchedBorder());
            ivjBUIMiddleToolbarPanel.setLayout(new java.awt.BorderLayout());
            ivjBUIMiddleToolbarPanel.setBackground(new java.awt.Color(204,204,255));
            getBUIMiddleToolbarPanel().add(getBUIMiddleToolBar(), "Center");
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjBUIMiddleToolbarPanel;
}
/**
 * Return the BUIToolBar property value.
 * @return javax.swing.JToolBar
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JToolBar getBUIToolBar() {
    if (ivjBUIToolBar == null) {
        try {
            ivjBUIToolBar = new javax.swing.JToolBar();
            ivjBUIToolBar.setName("BUIToolBar");
            ivjBUIToolBar.setFloatable(false);
            ivjBUIToolBar.setBackground(new java.awt.Color(204,204,255));
            getBUIToolBar().add(getNewToolBarButton(), getNewToolBarButton().getName());
            getBUIToolBar().add(getOpenToolBarButton(), getOpenToolBarButton().getName());
            getBUIToolBar().add(getSaveAsToolBarButton(), getSaveAsToolBarButton().getName());
            getBUIToolBar().add(getSaveToolBarButton(), getSaveToolBarButton().getName());
            getBUIToolBar().add(getSeparator1ToolBarButton1(), getSeparator1ToolBarButton1().getName());
            ivjBUIToolBar.add(getJ3CToolBarButton());
            ivjBUIToolBar.add(getSlicerToolBarButton());
            ivjBUIToolBar.add(getABPSToolBarButton());
            ivjBUIToolBar.add(getBircToolBarButton());
            getBUIToolBar().add(getSeparator1ToolBarButton(), getSeparator1ToolBarButton().getName());
            getBUIToolBar().add(getRunToolBarButton(), getRunToolBarButton().getName());
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjBUIToolBar;
}
/**
 * Return the BUIToolbarPanel property value.
 * @return javax.swing.JPanel
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JPanel getBUIToolbarPanel() {
    if (ivjBUIToolbarPanel == null) {
        try {
            ivjBUIToolbarPanel = new javax.swing.JPanel();
            ivjBUIToolbarPanel.setName("BUIToolbarPanel");
            ivjBUIToolbarPanel.setLayout(new java.awt.BorderLayout());
            ivjBUIToolbarPanel.setBackground(new java.awt.Color(204,204,255));
            getBUIToolbarPanel().add(getBUITopToolbarPanel(), "North");
            getBUIToolbarPanel().add(getBUIMiddleToolbarPanel(), "South");
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjBUIToolbarPanel;
}
/**
 * Return the BUITopToolbarPanel property value.
 * @return javax.swing.JPanel
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JPanel getBUITopToolbarPanel() {
    if (ivjBUITopToolbarPanel == null) {
        try {
            ivjBUITopToolbarPanel = new javax.swing.JPanel();
            ivjBUITopToolbarPanel.setName("BUITopToolbarPanel");
            ivjBUITopToolbarPanel.setBorder(new javax.swing.border.EtchedBorder());
            ivjBUITopToolbarPanel.setLayout(new java.awt.BorderLayout());
            ivjBUITopToolbarPanel.setBackground(new java.awt.Color(204,204,255));
            getBUITopToolbarPanel().add(getBUIToolBar(), "Center");
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjBUITopToolbarPanel;
}
/**
 * Return the CheckerPanel property value.
 * @return javax.swing.JPanel
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JPanel getCheckerPanel() {
    if (ivjCheckerPanel == null) {
        try {
            ivjCheckerPanel = new javax.swing.JPanel();
            ivjCheckerPanel.setName("CheckerPanel");
            ivjCheckerPanel.setOpaque(true);
            ivjCheckerPanel.setLayout(new java.awt.GridBagLayout());
            ivjCheckerPanel.setBackground(new java.awt.Color(204,204,255));

            java.awt.GridBagConstraints constraintsSpinLabel = new java.awt.GridBagConstraints();
            constraintsSpinLabel.gridx = 0; constraintsSpinLabel.gridy = 0;
            constraintsSpinLabel.insets = new java.awt.Insets(4, 4, 4, 4);
            getCheckerPanel().add(getSpinLabel(), constraintsSpinLabel);

            java.awt.GridBagConstraints constraintsJPFLabel = new java.awt.GridBagConstraints();
            constraintsJPFLabel.gridx = 2; constraintsJPFLabel.gridy = 0;
            constraintsJPFLabel.insets = new java.awt.Insets(4, 4, 4, 4);
            getCheckerPanel().add(getJPFLabel(), constraintsJPFLabel);

            java.awt.GridBagConstraints constraintsNuSMVLabel = new java.awt.GridBagConstraints();
            constraintsNuSMVLabel.gridx = 1; constraintsNuSMVLabel.gridy = 0;
            constraintsNuSMVLabel.insets = new java.awt.Insets(4, 4, 4, 4);
            getCheckerPanel().add(getNuSMVLabel(), constraintsNuSMVLabel);
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjCheckerPanel;
}
/**
 * Return the PDGToolBarButton property value.
 * @return javax.swing.JButton
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
public javax.swing.JButton getDependToolBarButton() {
    if (ivjDependToolBarButton == null) {
        try {
            ivjDependToolBarButton = new javax.swing.JButton();
            ivjDependToolBarButton.setName("DependToolBarButton");
            ivjDependToolBarButton.setToolTipText("Program Dependency Browser");
            ivjDependToolBarButton.setHorizontalTextPosition(javax.swing.SwingConstants.CENTER);
            ivjDependToolBarButton.setMargin(new java.awt.Insets(0, 0, 0, 0));
            ivjDependToolBarButton.setPressedIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/PDG24.gif")));
            ivjDependToolBarButton.setMinimumSize(new java.awt.Dimension(65, 50));
            ivjDependToolBarButton.setBorder(new javax.swing.border.CompoundBorder());
            ivjDependToolBarButton.setText("  PDG  ");
            ivjDependToolBarButton.setBackground(new java.awt.Color(204,204,255));
            ivjDependToolBarButton.setMaximumSize(new java.awt.Dimension(65, 50));
            ivjDependToolBarButton.setVerticalTextPosition(javax.swing.SwingConstants.BOTTOM);
            ivjDependToolBarButton.setIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/PDG24.gif")));
            ivjDependToolBarButton.setPreferredSize(new java.awt.Dimension(65, 50));
            ivjDependToolBarButton.setFont(new java.awt.Font("dialog", 0, 10));
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjDependToolBarButton;
}
/**
 * Return the ExitMenuItem property value.
 * @return javax.swing.JMenuItem
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JMenuItem getExitMenuItem() {
    if (ivjExitMenuItem == null) {
        try {
            ivjExitMenuItem = new javax.swing.JMenuItem();
            ivjExitMenuItem.setName("ExitMenuItem");
            ivjExitMenuItem.setMnemonic('x');
            ivjExitMenuItem.setText("Exit");
            ivjExitMenuItem.setBackground(new java.awt.Color(204,204,255));
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjExitMenuItem;
}
/**
 * Return the HelpMenu property value.
 * @return javax.swing.JMenu
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JMenu getHelpMenu() {
    if (ivjHelpMenu == null) {
        try {
            ivjHelpMenu = new javax.swing.JMenu();
            ivjHelpMenu.setName("HelpMenu");
            ivjHelpMenu.setMnemonic('h');
            ivjHelpMenu.setText("Help");
            ivjHelpMenu.setBackground(new java.awt.Color(204,204,255));
            ivjHelpMenu.add(getAboutMenuItem());
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjHelpMenu;
}
/**
 * Return the IRMenuItem property value.
 * @return javax.swing.JMenuItem
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JMenuItem getIRMenuItem() {
    if (ivjIRMenuItem == null) {
        try {
            ivjIRMenuItem = new javax.swing.JMenuItem();
            ivjIRMenuItem.setName("IRMenuItem");
            ivjIRMenuItem.setMnemonic('g');
            ivjIRMenuItem.setText("General Options");
            ivjIRMenuItem.setBackground(new java.awt.Color(204,204,255));
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjIRMenuItem;
}
/**
 * Return the J3CToolBarButton property value.
 * @return javax.swing.JButton
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JButton getJ3CToolBarButton() {
    if (ivjJ3CToolBarButton == null) {
        try {
            ivjJ3CToolBarButton = new javax.swing.JButton();
            ivjJ3CToolBarButton.setName("J3CToolBarButton");
            ivjJ3CToolBarButton.setToolTipText("JJJC");
            ivjJ3CToolBarButton.setHorizontalTextPosition(javax.swing.SwingConstants.CENTER);
            ivjJ3CToolBarButton.setMargin(new java.awt.Insets(0, 0, 0, 0));
            ivjJ3CToolBarButton.setPressedIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/JJJC24.gif")));
            ivjJ3CToolBarButton.setMinimumSize(new java.awt.Dimension(65, 50));
            ivjJ3CToolBarButton.setRequestFocusEnabled(true);
            ivjJ3CToolBarButton.setBorder(new javax.swing.border.CompoundBorder());
            ivjJ3CToolBarButton.setText("  JJJC  ");
            ivjJ3CToolBarButton.setBackground(new java.awt.Color(204,204,255));
            ivjJ3CToolBarButton.setMaximumSize(new java.awt.Dimension(65, 50));
            ivjJ3CToolBarButton.setDisabledIcon(null);
            ivjJ3CToolBarButton.setVerticalTextPosition(javax.swing.SwingConstants.BOTTOM);
            ivjJ3CToolBarButton.setIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/JJJCSelected24.gif")));
            ivjJ3CToolBarButton.setPreferredSize(new java.awt.Dimension(65, 50));
            ivjJ3CToolBarButton.setFont(new java.awt.Font("dialog", 0, 10));
            ivjJ3CToolBarButton.setEnabled(true);
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjJ3CToolBarButton;
}
/**
 * Return the JLabel2 property value.
 * @return javax.swing.JLabel
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
public javax.swing.JLabel getJPFLabel() {
    if (ivjJPFLabel == null) {
        try {
            ivjJPFLabel = new javax.swing.JLabel();
            ivjJPFLabel.setName("JPFLabel");
            ivjJPFLabel.setIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/JPF2.gif")));
            ivjJPFLabel.setText("");
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjJPFLabel;
}
/**
 * Return the JSeparator1 property value.
 * @return javax.swing.JSeparator
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JSeparator getJSeparator1() {
    if (ivjJSeparator1 == null) {
        try {
            ivjJSeparator1 = new javax.swing.JSeparator();
            ivjJSeparator1.setName("JSeparator1");
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjJSeparator1;
}
/**
 * Return the JSeparator2 property value.
 * @return javax.swing.JSeparator
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JSeparator getJSeparator2() {
    if (ivjJSeparator2 == null) {
        try {
            ivjJSeparator2 = new javax.swing.JSeparator();
            ivjJSeparator2.setName("JSeparator2");
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjJSeparator2;
}
/**
 * Return the JSeparator3 property value.
 * @return javax.swing.JSeparator
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JSeparator getJSeparator3() {
    if (ivjJSeparator3 == null) {
        try {
            ivjJSeparator3 = new javax.swing.JSeparator();
            ivjJSeparator3.setName("JSeparator3");
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjJSeparator3;
}
/**
 * Return the JSeparator4 property value.
 * @return javax.swing.JSeparator
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JSeparator getJSeparator4() {
    if (ivjJSeparator4 == null) {
        try {
            ivjJSeparator4 = new javax.swing.JSeparator();
            ivjJSeparator4.setName("JSeparator4");
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjJSeparator4;
}
/**
 * Return the JSeparator5 property value.
 * @return javax.swing.JSeparator
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JSeparator getJSeparator5() {
    if (ivjJSeparator5 == null) {
        try {
            ivjJSeparator5 = new javax.swing.JSeparator();
            ivjJSeparator5.setName("JSeparator5");
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjJSeparator5;
}
/**
 * Return the CloseMenuItem property value.
 * @return javax.swing.JMenuItem
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JMenuItem getManagerMenuItem() {
    if (ivjManagerMenuItem == null) {
        try {
            ivjManagerMenuItem = new javax.swing.JMenuItem();
            ivjManagerMenuItem.setName("ManagerMenuItem");
            ivjManagerMenuItem.setMnemonic('m');
            ivjManagerMenuItem.setText("Manager");
            ivjManagerMenuItem.setBackground(new java.awt.Color(204,204,255));
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjManagerMenuItem;
}
/**
 * Return the NewMenuItem property value.
 * @return javax.swing.JMenuItem
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JMenuItem getNewMenuItem() {
    if (ivjNewMenuItem == null) {
        try {
            ivjNewMenuItem = new javax.swing.JMenuItem();
            ivjNewMenuItem.setName("NewMenuItem");
            ivjNewMenuItem.setMnemonic('n');
            ivjNewMenuItem.setText("New");
            ivjNewMenuItem.setBackground(new java.awt.Color(204,204,255));
            ivjNewMenuItem.setPressedIcon(null);
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjNewMenuItem;
}
/**
 * Return the NewToolBarButton property value.
 * @return javax.swing.JButton
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JButton getNewToolBarButton() {
    if (ivjNewToolBarButton == null) {
        try {
            ivjNewToolBarButton = new javax.swing.JButton();
            ivjNewToolBarButton.setName("NewToolBarButton");
            ivjNewToolBarButton.setToolTipText("New sessions");
            ivjNewToolBarButton.setHorizontalTextPosition(javax.swing.SwingConstants.CENTER);
            ivjNewToolBarButton.setMargin(new java.awt.Insets(0, 0, 0, 0));
            ivjNewToolBarButton.setPressedIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/New24.gif")));
            ivjNewToolBarButton.setMinimumSize(new java.awt.Dimension(65, 50));
            ivjNewToolBarButton.setBorder(new javax.swing.border.CompoundBorder());
            ivjNewToolBarButton.setText("  New  ");
            ivjNewToolBarButton.setBackground(new java.awt.Color(204,204,255));
            ivjNewToolBarButton.setMaximumSize(new java.awt.Dimension(65, 50));
            ivjNewToolBarButton.setVerticalTextPosition(javax.swing.SwingConstants.BOTTOM);
            ivjNewToolBarButton.setIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/New24.gif")));
            ivjNewToolBarButton.setPreferredSize(new java.awt.Dimension(65, 50));
            ivjNewToolBarButton.setFont(new java.awt.Font("dialog", 0, 10));
            ivjNewToolBarButton.setEnabled(true);
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjNewToolBarButton;
}
/**
 * Return the JLabel3 property value.
 * @return javax.swing.JLabel
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
public javax.swing.JLabel getNuSMVLabel() {
    if (ivjNuSMVLabel == null) {
        try {
            ivjNuSMVLabel = new javax.swing.JLabel();
            ivjNuSMVLabel.setName("NuSMVLabel");
            ivjNuSMVLabel.setIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/NuSMV.gif")));
            ivjNuSMVLabel.setText("");
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjNuSMVLabel;
}
/**
 * Return the OpenMenuItem property value.
 * @return javax.swing.JMenuItem
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JMenuItem getOpenMenuItem() {
    if (ivjOpenMenuItem == null) {
        try {
            ivjOpenMenuItem = new javax.swing.JMenuItem();
            ivjOpenMenuItem.setName("OpenMenuItem");
            ivjOpenMenuItem.setMnemonic('o');
            ivjOpenMenuItem.setText("Open");
            ivjOpenMenuItem.setBackground(new java.awt.Color(204,204,255));
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjOpenMenuItem;
}
/**
 * Return the SlicerToolBarButton2 property value.
 * @return javax.swing.JButton
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JButton getOpenToolBarButton() {
    if (ivjOpenToolBarButton == null) {
        try {
            ivjOpenToolBarButton = new javax.swing.JButton();
            ivjOpenToolBarButton.setName("OpenToolBarButton");
            ivjOpenToolBarButton.setToolTipText("Open sessions");
            ivjOpenToolBarButton.setHorizontalTextPosition(javax.swing.SwingConstants.CENTER);
            ivjOpenToolBarButton.setMargin(new java.awt.Insets(0, 0, 0, 0));
            ivjOpenToolBarButton.setPressedIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/Open24.gif")));
            ivjOpenToolBarButton.setMinimumSize(new java.awt.Dimension(65, 50));
            ivjOpenToolBarButton.setBorder(new javax.swing.border.CompoundBorder());
            ivjOpenToolBarButton.setText("  Open  ");
            ivjOpenToolBarButton.setBackground(new java.awt.Color(204,204,255));
            ivjOpenToolBarButton.setMaximumSize(new java.awt.Dimension(65, 50));
            ivjOpenToolBarButton.setVerticalTextPosition(javax.swing.SwingConstants.BOTTOM);
            ivjOpenToolBarButton.setIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/Open24.gif")));
            ivjOpenToolBarButton.setPreferredSize(new java.awt.Dimension(65, 50));
            ivjOpenToolBarButton.setFont(new java.awt.Font("dialog", 0, 10));
            ivjOpenToolBarButton.setEnabled(true);
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjOpenToolBarButton;
}
/**
 * Return the SpecificationPatternMenuItem property value.
 * @return javax.swing.JMenuItem
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JMenuItem getPatternManagerMenuItem() {
    if (ivjPatternManagerMenuItem == null) {
        try {
            ivjPatternManagerMenuItem = new javax.swing.JMenuItem();
            ivjPatternManagerMenuItem.setName("PatternManagerMenuItem");
            ivjPatternManagerMenuItem.setMnemonic('a');
            ivjPatternManagerMenuItem.setText("Pattern Manager");
            ivjPatternManagerMenuItem.setBackground(new java.awt.Color(204,204,255));
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjPatternManagerMenuItem;
}
/**
 * Return the PatternToolBarButton property value.
 * @return javax.swing.JButton
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JButton getPatternToolBarButton() {
    if (ivjPatternToolBarButton == null) {
        try {
            ivjPatternToolBarButton = new javax.swing.JButton();
            ivjPatternToolBarButton.setName("PatternToolBarButton");
            ivjPatternToolBarButton.setToolTipText("Pattern Manager");
            ivjPatternToolBarButton.setHorizontalTextPosition(javax.swing.SwingConstants.CENTER);
            ivjPatternToolBarButton.setMargin(new java.awt.Insets(0, 0, 0, 0));
            ivjPatternToolBarButton.setPressedIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/Pattern24.gif")));
            ivjPatternToolBarButton.setMinimumSize(new java.awt.Dimension(65, 50));
            ivjPatternToolBarButton.setBorder(new javax.swing.border.CompoundBorder());
            ivjPatternToolBarButton.setText("  Pattern  ");
            ivjPatternToolBarButton.setBackground(new java.awt.Color(204,204,255));
            ivjPatternToolBarButton.setMaximumSize(new java.awt.Dimension(65, 50));
            ivjPatternToolBarButton.setVerticalTextPosition(javax.swing.SwingConstants.BOTTOM);
            ivjPatternToolBarButton.setIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/Pattern24.gif")));
            ivjPatternToolBarButton.setPreferredSize(new java.awt.Dimension(65, 50));
            ivjPatternToolBarButton.setFont(new java.awt.Font("dialog", 0, 10));
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjPatternToolBarButton;
}
/**
 * Return the PropositionMenuItem property value.
 * @return javax.swing.JMenuItem
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JMenuItem getPredicateBrowserMenuItem() {
    if (ivjPredicateBrowserMenuItem == null) {
        try {
            ivjPredicateBrowserMenuItem = new javax.swing.JMenuItem();
            ivjPredicateBrowserMenuItem.setName("PredicateBrowserMenuItem");
            ivjPredicateBrowserMenuItem.setMnemonic('r');
            ivjPredicateBrowserMenuItem.setText("Predicate Browser");
            ivjPredicateBrowserMenuItem.setBackground(new java.awt.Color(204,204,255));
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjPredicateBrowserMenuItem;
}
/**
 * Return the PredicateToolBarButton property value.
 * @return javax.swing.JButton
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JButton getPredicateToolBarButton() {
    if (ivjPredicateToolBarButton == null) {
        try {
            ivjPredicateToolBarButton = new javax.swing.JButton();
            ivjPredicateToolBarButton.setName("PredicateToolBarButton");
            ivjPredicateToolBarButton.setToolTipText("PredicateBrowser");
            ivjPredicateToolBarButton.setHorizontalTextPosition(javax.swing.SwingConstants.CENTER);
            ivjPredicateToolBarButton.setMargin(new java.awt.Insets(0, 0, 0, 0));
            ivjPredicateToolBarButton.setPressedIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/Predicate24.gif")));
            ivjPredicateToolBarButton.setMinimumSize(new java.awt.Dimension(65, 50));
            ivjPredicateToolBarButton.setBorder(new javax.swing.border.CompoundBorder());
            ivjPredicateToolBarButton.setText("  Predicate  ");
            ivjPredicateToolBarButton.setBackground(new java.awt.Color(204,204,255));
            ivjPredicateToolBarButton.setMaximumSize(new java.awt.Dimension(65, 50));
            ivjPredicateToolBarButton.setVerticalTextPosition(javax.swing.SwingConstants.BOTTOM);
            ivjPredicateToolBarButton.setIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/Predicate24.gif")));
            ivjPredicateToolBarButton.setPreferredSize(new java.awt.Dimension(65, 50));
            ivjPredicateToolBarButton.setFont(new java.awt.Font("dialog", 0, 10));
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjPredicateToolBarButton;
}
/**
 * Return the PropertyManagerMenuItem property value.
 * @return javax.swing.JMenuItem
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JMenuItem getPropertyManagerMenuItem() {
    if (ivjPropertyManagerMenuItem == null) {
        try {
            ivjPropertyManagerMenuItem = new javax.swing.JMenuItem();
            ivjPropertyManagerMenuItem.setName("PropertyManagerMenuItem");
            ivjPropertyManagerMenuItem.setMnemonic('p');
            ivjPropertyManagerMenuItem.setText("Property Manager");
            ivjPropertyManagerMenuItem.setBackground(new java.awt.Color(204,204,255));
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjPropertyManagerMenuItem;
}
/**
 * Return the PropertyToolBarButton property value.
 * @return javax.swing.JButton
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JButton getPropertyToolBarButton() {
    if (ivjPropertyToolBarButton == null) {
        try {
            ivjPropertyToolBarButton = new javax.swing.JButton();
            ivjPropertyToolBarButton.setName("PropertyToolBarButton");
            ivjPropertyToolBarButton.setToolTipText("Property Manager");
            ivjPropertyToolBarButton.setHorizontalTextPosition(javax.swing.SwingConstants.CENTER);
            ivjPropertyToolBarButton.setMargin(new java.awt.Insets(0, 0, 0, 0));
            ivjPropertyToolBarButton.setPressedIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/Property24.gif")));
            ivjPropertyToolBarButton.setMinimumSize(new java.awt.Dimension(65, 50));
            ivjPropertyToolBarButton.setBorder(new javax.swing.border.CompoundBorder());
            ivjPropertyToolBarButton.setText("  Property  ");
            ivjPropertyToolBarButton.setBackground(new java.awt.Color(204,204,255));
            ivjPropertyToolBarButton.setMaximumSize(new java.awt.Dimension(65, 50));
            ivjPropertyToolBarButton.setVerticalTextPosition(javax.swing.SwingConstants.BOTTOM);
            ivjPropertyToolBarButton.setIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/Property24.gif")));
            ivjPropertyToolBarButton.setPreferredSize(new java.awt.Dimension(65, 50));
            ivjPropertyToolBarButton.setFont(new java.awt.Font("dialog", 0, 10));
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjPropertyToolBarButton;
}
/**
 * Return the RunToolBarButton property value.
 * @return javax.swing.JButton
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JButton getRunToolBarButton() {
    if (ivjRunToolBarButton == null) {
        try {
            ivjRunToolBarButton = new javax.swing.JButton();
            ivjRunToolBarButton.setName("RunToolBarButton");
            ivjRunToolBarButton.setToolTipText("Run");
            ivjRunToolBarButton.setHorizontalTextPosition(javax.swing.SwingConstants.CENTER);
            ivjRunToolBarButton.setSelected(false);
            ivjRunToolBarButton.setMargin(new java.awt.Insets(0, 0, 0, 0));
            ivjRunToolBarButton.setPressedIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/Run24.gif")));
            ivjRunToolBarButton.setRequestFocusEnabled(false);
            ivjRunToolBarButton.setMinimumSize(new java.awt.Dimension(65, 50));
            ivjRunToolBarButton.setBorder(new javax.swing.border.CompoundBorder());
            ivjRunToolBarButton.setText("  Run  ");
            ivjRunToolBarButton.setBackground(new java.awt.Color(204,204,255));
            ivjRunToolBarButton.setMaximumSize(new java.awt.Dimension(65, 50));
            ivjRunToolBarButton.setVerticalTextPosition(javax.swing.SwingConstants.BOTTOM);
            ivjRunToolBarButton.setIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/Run24.gif")));
            ivjRunToolBarButton.setPreferredSize(new java.awt.Dimension(65, 50));
            ivjRunToolBarButton.setFont(new java.awt.Font("dialog", 0, 10));
            ivjRunToolBarButton.setEnabled(true);
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjRunToolBarButton;
}
/**
 * Return the SaveAsMenuItem property value.
 * @return javax.swing.JMenuItem
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JMenuItem getSaveAsMenuItem() {
    if (ivjSaveAsMenuItem == null) {
        try {
            ivjSaveAsMenuItem = new javax.swing.JMenuItem();
            ivjSaveAsMenuItem.setName("SaveAsMenuItem");
            ivjSaveAsMenuItem.setMnemonic('a');
            ivjSaveAsMenuItem.setText("Save as");
            ivjSaveAsMenuItem.setBackground(new java.awt.Color(204,204,255));
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjSaveAsMenuItem;
}
/**
 * Return the SlicerToolBarButton3 property value.
 * @return javax.swing.JButton
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JButton getSaveAsToolBarButton() {
    if (ivjSaveAsToolBarButton == null) {
        try {
            ivjSaveAsToolBarButton = new javax.swing.JButton();
            ivjSaveAsToolBarButton.setName("SaveAsToolBarButton");
            ivjSaveAsToolBarButton.setToolTipText("Save sessions as...");
            ivjSaveAsToolBarButton.setHorizontalTextPosition(javax.swing.SwingConstants.CENTER);
            ivjSaveAsToolBarButton.setMargin(new java.awt.Insets(0, 0, 0, 0));
            ivjSaveAsToolBarButton.setPressedIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/SaveAs24.gif")));
            ivjSaveAsToolBarButton.setMinimumSize(new java.awt.Dimension(65, 50));
            ivjSaveAsToolBarButton.setBorder(new javax.swing.border.CompoundBorder());
            ivjSaveAsToolBarButton.setText("  Save as  ");
            ivjSaveAsToolBarButton.setBackground(new java.awt.Color(204,204,255));
            ivjSaveAsToolBarButton.setMaximumSize(new java.awt.Dimension(65, 50));
            ivjSaveAsToolBarButton.setVerticalTextPosition(javax.swing.SwingConstants.BOTTOM);
            ivjSaveAsToolBarButton.setIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/SaveAs24.gif")));
            ivjSaveAsToolBarButton.setPreferredSize(new java.awt.Dimension(65, 50));
            ivjSaveAsToolBarButton.setFont(new java.awt.Font("dialog", 0, 10));
            ivjSaveAsToolBarButton.setEnabled(true);
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjSaveAsToolBarButton;
}
/**
 * Return the SaveMenuItem property value.
 * @return javax.swing.JMenuItem
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JMenuItem getSaveMenuItem() {
    if (ivjSaveMenuItem == null) {
        try {
            ivjSaveMenuItem = new javax.swing.JMenuItem();
            ivjSaveMenuItem.setName("SaveMenuItem");
            ivjSaveMenuItem.setMnemonic('s');
            ivjSaveMenuItem.setText("Save");
            ivjSaveMenuItem.setBackground(new java.awt.Color(204,204,255));
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjSaveMenuItem;
}
/**
 * Return the SlicerToolBarButton4 property value.
 * @return javax.swing.JButton
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JButton getSaveToolBarButton() {
    if (ivjSaveToolBarButton == null) {
        try {
            ivjSaveToolBarButton = new javax.swing.JButton();
            ivjSaveToolBarButton.setName("SaveToolBarButton");
            ivjSaveToolBarButton.setToolTipText("Save sessions");
            ivjSaveToolBarButton.setHorizontalTextPosition(javax.swing.SwingConstants.CENTER);
            ivjSaveToolBarButton.setMargin(new java.awt.Insets(0, 0, 0, 0));
            ivjSaveToolBarButton.setPressedIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/Save24.gif")));
            ivjSaveToolBarButton.setMinimumSize(new java.awt.Dimension(65, 50));
            ivjSaveToolBarButton.setBorder(new javax.swing.border.CompoundBorder());
            ivjSaveToolBarButton.setText("  Save  ");
            ivjSaveToolBarButton.setBackground(new java.awt.Color(204,204,255));
            ivjSaveToolBarButton.setMaximumSize(new java.awt.Dimension(65, 50));
            ivjSaveToolBarButton.setVerticalTextPosition(javax.swing.SwingConstants.BOTTOM);
            ivjSaveToolBarButton.setIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/Save24.gif")));
            ivjSaveToolBarButton.setPreferredSize(new java.awt.Dimension(65, 50));
            ivjSaveToolBarButton.setFont(new java.awt.Font("dialog", 0, 10));
            ivjSaveToolBarButton.setEnabled(true);
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjSaveToolBarButton;
}
/**
 * Return the Separator1ToolBarButton property value.
 * @return javax.swing.JButton
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JButton getSeparator1ToolBarButton() {
    if (ivjSeparator1ToolBarButton == null) {
        try {
            ivjSeparator1ToolBarButton = new javax.swing.JButton();
            ivjSeparator1ToolBarButton.setName("Separator1ToolBarButton");
            ivjSeparator1ToolBarButton.setHorizontalTextPosition(javax.swing.SwingConstants.CENTER);
            ivjSeparator1ToolBarButton.setDisabledSelectedIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/separator.gif")));
            ivjSeparator1ToolBarButton.setMargin(new java.awt.Insets(0, 0, 0, 0));
            ivjSeparator1ToolBarButton.setPressedIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/separator.gif")));
            ivjSeparator1ToolBarButton.setMinimumSize(new java.awt.Dimension(20, 50));
            ivjSeparator1ToolBarButton.setBorder(new javax.swing.border.CompoundBorder());
            ivjSeparator1ToolBarButton.setText("");
            ivjSeparator1ToolBarButton.setBackground(new java.awt.Color(204,204,255));
            ivjSeparator1ToolBarButton.setMaximumSize(new java.awt.Dimension(20, 50));
            ivjSeparator1ToolBarButton.setDisabledIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/separator.gif")));
            ivjSeparator1ToolBarButton.setVerticalTextPosition(javax.swing.SwingConstants.BOTTOM);
            ivjSeparator1ToolBarButton.setIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/separator.gif")));
            ivjSeparator1ToolBarButton.setPreferredSize(new java.awt.Dimension(30, 50));
            ivjSeparator1ToolBarButton.setEnabled(false);
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjSeparator1ToolBarButton;
}
/**
 * Return the Separator1ToolBarButton1 property value.
 * @return javax.swing.JButton
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JButton getSeparator1ToolBarButton1() {
    if (ivjSeparator1ToolBarButton1 == null) {
        try {
            ivjSeparator1ToolBarButton1 = new javax.swing.JButton();
            ivjSeparator1ToolBarButton1.setName("Separator1ToolBarButton1");
            ivjSeparator1ToolBarButton1.setHorizontalTextPosition(javax.swing.SwingConstants.CENTER);
            ivjSeparator1ToolBarButton1.setDisabledSelectedIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/separator.gif")));
            ivjSeparator1ToolBarButton1.setMargin(new java.awt.Insets(0, 0, 0, 0));
            ivjSeparator1ToolBarButton1.setPressedIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/separator.gif")));
            ivjSeparator1ToolBarButton1.setMinimumSize(new java.awt.Dimension(20, 50));
            ivjSeparator1ToolBarButton1.setBorder(new javax.swing.border.CompoundBorder());
            ivjSeparator1ToolBarButton1.setText("");
            ivjSeparator1ToolBarButton1.setBackground(new java.awt.Color(204,204,255));
            ivjSeparator1ToolBarButton1.setMaximumSize(new java.awt.Dimension(20, 50));
            ivjSeparator1ToolBarButton1.setDisabledIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/separator.gif")));
            ivjSeparator1ToolBarButton1.setVerticalTextPosition(javax.swing.SwingConstants.BOTTOM);
            ivjSeparator1ToolBarButton1.setIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/separator.gif")));
            ivjSeparator1ToolBarButton1.setPreferredSize(new java.awt.Dimension(30, 50));
            ivjSeparator1ToolBarButton1.setEnabled(false);
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjSeparator1ToolBarButton1;
}
/**
 * Return the Separator1ToolBarButton11 property value.
 * @return javax.swing.JButton
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JButton getSeparator1ToolBarButton11() {
    if (ivjSeparator1ToolBarButton11 == null) {
        try {
            ivjSeparator1ToolBarButton11 = new javax.swing.JButton();
            ivjSeparator1ToolBarButton11.setName("Separator1ToolBarButton11");
            ivjSeparator1ToolBarButton11.setHorizontalTextPosition(javax.swing.SwingConstants.CENTER);
            ivjSeparator1ToolBarButton11.setDisabledSelectedIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/separator.gif")));
            ivjSeparator1ToolBarButton11.setMargin(new java.awt.Insets(0, 0, 0, 0));
            ivjSeparator1ToolBarButton11.setPressedIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/separator.gif")));
            ivjSeparator1ToolBarButton11.setMinimumSize(new java.awt.Dimension(20, 50));
            ivjSeparator1ToolBarButton11.setBorder(new javax.swing.border.CompoundBorder());
            ivjSeparator1ToolBarButton11.setText("");
            ivjSeparator1ToolBarButton11.setBackground(new java.awt.Color(204,204,255));
            ivjSeparator1ToolBarButton11.setMaximumSize(new java.awt.Dimension(20, 50));
            ivjSeparator1ToolBarButton11.setDisabledIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/separator.gif")));
            ivjSeparator1ToolBarButton11.setVerticalTextPosition(javax.swing.SwingConstants.BOTTOM);
            ivjSeparator1ToolBarButton11.setIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/separator.gif")));
            ivjSeparator1ToolBarButton11.setPreferredSize(new java.awt.Dimension(20, 50));
            ivjSeparator1ToolBarButton11.setEnabled(false);
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjSeparator1ToolBarButton11;
}
/**
 * Return the Separator1ToolBarButton111 property value.
 * @return javax.swing.JButton
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JButton getSeparator1ToolBarButton111() {
    if (ivjSeparator1ToolBarButton111 == null) {
        try {
            ivjSeparator1ToolBarButton111 = new javax.swing.JButton();
            ivjSeparator1ToolBarButton111.setName("Separator1ToolBarButton111");
            ivjSeparator1ToolBarButton111.setHorizontalTextPosition(javax.swing.SwingConstants.CENTER);
            ivjSeparator1ToolBarButton111.setDisabledSelectedIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/separator.gif")));
            ivjSeparator1ToolBarButton111.setMargin(new java.awt.Insets(0, 0, 0, 0));
            ivjSeparator1ToolBarButton111.setPressedIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/separator.gif")));
            ivjSeparator1ToolBarButton111.setMinimumSize(new java.awt.Dimension(20, 50));
            ivjSeparator1ToolBarButton111.setBorder(new javax.swing.border.CompoundBorder());
            ivjSeparator1ToolBarButton111.setText("");
            ivjSeparator1ToolBarButton111.setBackground(new java.awt.Color(204,204,255));
            ivjSeparator1ToolBarButton111.setMaximumSize(new java.awt.Dimension(20, 50));
            ivjSeparator1ToolBarButton111.setDisabledIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/separator.gif")));
            ivjSeparator1ToolBarButton111.setVerticalTextPosition(javax.swing.SwingConstants.BOTTOM);
            ivjSeparator1ToolBarButton111.setIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/separator.gif")));
            ivjSeparator1ToolBarButton111.setPreferredSize(new java.awt.Dimension(20, 50));
            ivjSeparator1ToolBarButton111.setEnabled(false);
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjSeparator1ToolBarButton111;
}
/**
 * Return the Separator1ToolBarButton1111 property value.
 * @return javax.swing.JButton
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JButton getSeparator1ToolBarButton1111() {
    if (ivjSeparator1ToolBarButton1111 == null) {
        try {
            ivjSeparator1ToolBarButton1111 = new javax.swing.JButton();
            ivjSeparator1ToolBarButton1111.setName("Separator1ToolBarButton1111");
            ivjSeparator1ToolBarButton1111.setHorizontalTextPosition(javax.swing.SwingConstants.CENTER);
            ivjSeparator1ToolBarButton1111.setDisabledSelectedIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/separator.gif")));
            ivjSeparator1ToolBarButton1111.setMargin(new java.awt.Insets(0, 0, 0, 0));
            ivjSeparator1ToolBarButton1111.setPressedIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/separator.gif")));
            ivjSeparator1ToolBarButton1111.setMinimumSize(new java.awt.Dimension(20, 50));
            ivjSeparator1ToolBarButton1111.setBorder(new javax.swing.border.CompoundBorder());
            ivjSeparator1ToolBarButton1111.setText("");
            ivjSeparator1ToolBarButton1111.setBackground(new java.awt.Color(204,204,255));
            ivjSeparator1ToolBarButton1111.setMaximumSize(new java.awt.Dimension(20, 50));
            ivjSeparator1ToolBarButton1111.setDisabledIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/separator.gif")));
            ivjSeparator1ToolBarButton1111.setVerticalTextPosition(javax.swing.SwingConstants.BOTTOM);
            ivjSeparator1ToolBarButton1111.setIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/separator.gif")));
            ivjSeparator1ToolBarButton1111.setPreferredSize(new java.awt.Dimension(20, 50));
            ivjSeparator1ToolBarButton1111.setEnabled(false);
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjSeparator1ToolBarButton1111;
}
/**
 * Return the JMenu1 property value.
 * @return javax.swing.JMenu
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JMenu getSessionMenu() {
    if (ivjSessionMenu == null) {
        try {
            ivjSessionMenu = new javax.swing.JMenu();
            ivjSessionMenu.setName("SessionMenu");
            ivjSessionMenu.setMnemonic('s');
            ivjSessionMenu.setText("Session");
            ivjSessionMenu.setBackground(new java.awt.Color(204,204,255));
            ivjSessionMenu.setActionCommand("ProjectMenu");
            ivjSessionMenu.add(getNewMenuItem());
            ivjSessionMenu.add(getOpenMenuItem());
            ivjSessionMenu.add(getSaveAsMenuItem());
            ivjSessionMenu.add(getSaveMenuItem());
            ivjSessionMenu.add(getJSeparator4());
            ivjSessionMenu.add(getManagerMenuItem());
            ivjSessionMenu.add(getJSeparator1());
            ivjSessionMenu.add(getIRMenuItem());
            ivjSessionMenu.add(getJSeparator3());
            ivjSessionMenu.add(getExitMenuItem());
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjSessionMenu;
}
/**
 * Return the SessionToolBarButton property value.
 * @return javax.swing.JButton
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JButton getSessionToolBarButton() {
    if (ivjSessionToolBarButton == null) {
        try {
            ivjSessionToolBarButton = new javax.swing.JButton();
            ivjSessionToolBarButton.setName("SessionToolBarButton");
            ivjSessionToolBarButton.setToolTipText("Session Manager");
            ivjSessionToolBarButton.setHorizontalTextPosition(javax.swing.SwingConstants.CENTER);
            ivjSessionToolBarButton.setMargin(new java.awt.Insets(0, 0, 0, 0));
            ivjSessionToolBarButton.setPressedIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/Session24.gif")));
            ivjSessionToolBarButton.setMinimumSize(new java.awt.Dimension(65, 50));
            ivjSessionToolBarButton.setBorder(new javax.swing.border.CompoundBorder());
            ivjSessionToolBarButton.setText("  Session  ");
            ivjSessionToolBarButton.setBackground(new java.awt.Color(204,204,255));
            ivjSessionToolBarButton.setMaximumSize(new java.awt.Dimension(65, 50));
            ivjSessionToolBarButton.setVerticalTextPosition(javax.swing.SwingConstants.BOTTOM);
            ivjSessionToolBarButton.setIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/Session24.gif")));
            ivjSessionToolBarButton.setPreferredSize(new java.awt.Dimension(65, 50));
            ivjSessionToolBarButton.setFont(new java.awt.Font("dialog", 0, 10));
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjSessionToolBarButton;
}
/**
 * Return the SlicerToolBarButton property value.
 * @return javax.swing.JButton
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JButton getSlicerToolBarButton() {
    if (ivjSlicerToolBarButton == null) {
        try {
            ivjSlicerToolBarButton = new javax.swing.JButton();
            ivjSlicerToolBarButton.setName("SlicerToolBarButton");
            ivjSlicerToolBarButton.setToolTipText("Slicer");
            ivjSlicerToolBarButton.setHorizontalTextPosition(javax.swing.SwingConstants.CENTER);
            ivjSlicerToolBarButton.setMargin(new java.awt.Insets(0, 0, 0, 0));
            ivjSlicerToolBarButton.setPressedIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/SlicerSelected24.gif")));
            ivjSlicerToolBarButton.setMinimumSize(new java.awt.Dimension(65, 50));
            ivjSlicerToolBarButton.setBorder(new javax.swing.border.CompoundBorder());
            ivjSlicerToolBarButton.setText("  Slicer  ");
            ivjSlicerToolBarButton.setBackground(new java.awt.Color(204,204,255));
            ivjSlicerToolBarButton.setMaximumSize(new java.awt.Dimension(65, 50));
            ivjSlicerToolBarButton.setVerticalTextPosition(javax.swing.SwingConstants.BOTTOM);
            ivjSlicerToolBarButton.setIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/Slicer24.gif")));
            ivjSlicerToolBarButton.setPreferredSize(new java.awt.Dimension(65, 50));
            ivjSlicerToolBarButton.setFont(new java.awt.Font("dialog", 0, 10));
            ivjSlicerToolBarButton.setEnabled(true);
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjSlicerToolBarButton;
}
/**
 * Return the SpecificationMenu property value.
 * @return javax.swing.JMenu
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private javax.swing.JMenu getSpecificationMenu() {
    if (ivjSpecificationMenu == null) {
        try {
            ivjSpecificationMenu = new javax.swing.JMenu();
            ivjSpecificationMenu.setName("SpecificationMenu");
            ivjSpecificationMenu.setMnemonic('p');
            ivjSpecificationMenu.setText("Property");
            ivjSpecificationMenu.setBackground(new java.awt.Color(204,204,255));
            ivjSpecificationMenu.add(getPatternManagerMenuItem());
            ivjSpecificationMenu.add(getPredicateBrowserMenuItem());
            ivjSpecificationMenu.add(getAssertionBrowserMenuItem());
            ivjSpecificationMenu.add(getJSeparator2());
            ivjSpecificationMenu.add(getPropertyManagerMenuItem());
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjSpecificationMenu;
}
/**
 * Return the JLabel1 property value.
 * @return javax.swing.JLabel
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
public javax.swing.JLabel getSpinLabel() {
    if (ivjSpinLabel == null) {
        try {
            ivjSpinLabel = new javax.swing.JLabel();
            ivjSpinLabel.setName("SpinLabel");
            ivjSpinLabel.setText("JLabel1");
            ivjSpinLabel.setMaximumSize(new java.awt.Dimension(50, 50));
            ivjSpinLabel.setIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/Spin.gif")));
            ivjSpinLabel.setPreferredSize(new java.awt.Dimension(50, 50));
            ivjSpinLabel.setMinimumSize(new java.awt.Dimension(50, 50));
            // user code begin {1}
            // user code end
        } catch (java.lang.Throwable ivjExc) {
            // user code begin {2}
            // user code end
            handleException(ivjExc);
        }
    }
    return ivjSpinLabel;
}
/**
 * Called whenever the part throws an exception.
 * @param exception java.lang.Throwable
 */
private void handleException(java.lang.Throwable exception) {

    /* Uncomment the following lines to print uncaught exceptions to stdout */
    // System.out.println("--------- UNCAUGHT EXCEPTION ---------");
    // exception.printStackTrace(System.out);
}
/**
 * Initializes connections
 * @exception java.lang.Exception The exception description.
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private void initConnections() throws java.lang.Exception {
    // user code begin {1}
    // user code end
    getExitMenuItem().addActionListener(ivjEventHandler);
    getManagerMenuItem().addActionListener(ivjEventHandler);
    getJ3CToolBarButton().addActionListener(ivjEventHandler);
    getSlicerToolBarButton().addActionListener(ivjEventHandler);
    getABPSToolBarButton().addActionListener(ivjEventHandler);
    getBircToolBarButton().addActionListener(ivjEventHandler);
    getRunToolBarButton().addActionListener(ivjEventHandler);
    getPatternManagerMenuItem().addActionListener(ivjEventHandler);
    getSaveMenuItem().addActionListener(ivjEventHandler);
    getSaveAsMenuItem().addActionListener(ivjEventHandler);
    getOpenMenuItem().addActionListener(ivjEventHandler);
    getNewMenuItem().addActionListener(ivjEventHandler);
    getPredicateBrowserMenuItem().addActionListener(ivjEventHandler);
    getPropertyManagerMenuItem().addActionListener(ivjEventHandler);
    getAbstractionManagerMenuItem().addActionListener(ivjEventHandler);
    getAboutMenuItem().addActionListener(ivjEventHandler);
    getAssertionBrowserMenuItem().addActionListener(ivjEventHandler);
    getSaveToolBarButton().addActionListener(ivjEventHandler);
    getSaveAsToolBarButton().addActionListener(ivjEventHandler);
    getOpenToolBarButton().addActionListener(ivjEventHandler);
    getNewToolBarButton().addActionListener(ivjEventHandler);
    getSessionToolBarButton().addActionListener(ivjEventHandler);
    getAssertionToolBarButton().addActionListener(ivjEventHandler);
    getPredicateToolBarButton().addActionListener(ivjEventHandler);
    getPatternToolBarButton().addActionListener(ivjEventHandler);
    getPropertyToolBarButton().addActionListener(ivjEventHandler);
    getDependToolBarButton().addActionListener(ivjEventHandler);
    getAbstractionToolBarButton().addActionListener(ivjEventHandler);
    getIRMenuItem().addActionListener(ivjEventHandler);
    getAbstractionLibraryManagerMenuItem().addActionListener(ivjEventHandler);
}
/**
 * Initialize the class.
 */
/* WARNING: THIS METHOD WILL BE REGENERATED. */
private void initialize() {
    try {
        // user code begin {1}
        IconLibrary.initialize();
        FileChooser.initialize();
        bui = this;
        manager = new SessionManager();
        patternManager = new PatternManager();
        predicateBrowser = new PredicateBrowser();
        assertionBrowser = new AssertionBrowser();
        sessionPane = new BUISessionPane();
        propertyManager = new PropertyManager();
        abstractionLibraryManager = new AbstractionLibraryManager();
        typeGUI = new TypeGUI();
        spinOption = new SpinOption();
        irOptions = new IROptions();
        dSpinOption = new DSpinOption();
        jpfOption = new JPFOption();
        bui.pack();
        manager.pack();
        patternManager.pack();
        predicateBrowser.pack();
        assertionBrowser.pack();
        propertyManager.pack();
        abstractionLibraryManager.pack();
        typeGUI.pack();
        spinOption.pack();
        dSpinOption.pack();
        jpfOption.pack();
        // user code end
        setName("BUI");
        setDefaultCloseOperation(javax.swing.WindowConstants.DISPOSE_ON_CLOSE);
        setJMenuBar(getBUIJMenuBar());
        setSize(760, 460);
        setTitle("Bandera");
        setContentPane(getBUIContentPane());
        initConnections();
    } catch (java.lang.Throwable ivjExc) {
        handleException(ivjExc);
    }
    // user code begin {2}
    // user code end
}
/**
 * Comment
 */
public void iRMenuItem_ActionEvents() {
    irOptions.setVisible(true);
}
/**
 * Comment
 */
public void j3CToolBarButton_ActionEvents() {
    Icon temp = getJ3CToolBarButton().getPressedIcon();
    getJ3CToolBarButton().setPressedIcon(getJ3CToolBarButton().getIcon());
    getJ3CToolBarButton().setIcon(temp);
    doJJJC = !doJJJC;
}
/**
 * main entrypoint - starts the part when it is run as an application
 * @param args java.lang.String[]
 */
public static void main(java.lang.String[] args) {
    try {
        BUI aBUI;
        edu.ksu.cis.bandera.util.Preferences.load(); 
        //edu.ksu.cis.bandera.util.Logger.on();
        aBUI = new BUI();
        aBUI.addWindowListener(new java.awt.event.WindowAdapter() {
            public void windowClosing(java.awt.event.WindowEvent e) {
                //edu.ksu.cis.bandera.util.Logger.off();
                edu.ksu.cis.bandera.util.Preferences.save();
                System.exit(0);
            };
        });
        aBUI.setVisible(true);
    } catch (Throwable exception) {
        System.err.println("Exception occurred in main() of javax.swing.JFrame");
        exception.printStackTrace(System.out);
    }
}
/**
 * Comment
 */
public void managerMenuItem_ActionEvents() {
    manager.pack();
    manager.setVisible(true);
}
/**
 * Comment
 */
public void newMenuItem_ActionEvents() {
    Vector v = sessions.getSessions();
    if ((v.size() > 0) && !sessions.isSaved()){
        switch (JOptionPane.showConfirmDialog(this, "Current sessions are not saved. Do you want to save it now ?", "Confirm", JOptionPane.YES_NO_CANCEL_OPTION, JOptionPane.INFORMATION_MESSAGE)) {
            case JOptionPane.YES_OPTION:
                saveMenuItem_ActionEvents();
                break;
            case JOptionPane.CANCEL_OPTION:
                return;
        }
    }
    changeSessions(new Sessions());
}
/**
 * Comment
 */
public void newToolBarButton_ActionEvents() {
    newMenuItem_ActionEvents();
}
/**
 * Comment
 */
public void openMenuItem_ActionEvents() {
    Vector v = sessions.getSessions();
    if ((v.size() > 0) && !sessions.isSaved()){
        switch (JOptionPane.showConfirmDialog(this, "Current sessions are not saved. Do you want to save it now ?", "Confirm", JOptionPane.YES_NO_CANCEL_OPTION, JOptionPane.INFORMATION_MESSAGE)) {
            case JOptionPane.YES_OPTION:
                saveMenuItem_ActionEvents();
                break;
            case JOptionPane.CANCEL_OPTION:
                return;
        }
    }
    System.setProperty("user.dir", BUI.originalUserDir);
    FileChooser.chooser.setCurrentDirectory(new File(System.getProperty("user.dir")));
    FileChooser.chooser.setSelectedFile(new File(""));
    FileChooser.chooser.setFileFilter(FileChooser.SESSION);
    FileChooser.chooser.setFileSelectionMode(FileChooser.FILES_ONLY);
    
    if (FileChooser.chooser.showOpenDialog(this) == FileChooser.APPROVE_OPTION) {
        try {
            if (FileChooser.chooser.getSelectedFile().isDirectory()) {
                JOptionPane.showMessageDialog(this, "Cannot choose a directory to open a session file", "Information", JOptionPane.INFORMATION_MESSAGE);
                return;
            }
            if (!FileChooser.chooser.getSelectedFile().exists()) {
                JOptionPane.showMessageDialog(this, "Selected file does not exist", "Information", JOptionPane.INFORMATION_MESSAGE);
                return;
            }
            changeSessions(SessionsSaverLoader.load(FileChooser.chooser.getSelectedFile().getCanonicalPath()));
            sessions.setSaved(true);
        } catch (Exception e) {
            JOptionPane.showMessageDialog(this, e.getMessage(), "Error", JOptionPane.ERROR_MESSAGE); 
        }
    }
}
/**
 * 
 * @param filename java.lang.String
 */
public void openMenuItemRoboto(String filename) {
    try {
        changeSessions(SessionsSaverLoader.load(new File(filename).getCanonicalPath()));
    } catch (Exception e) {
        System.out.println("Error: " + e.getMessage());
    }
}
/**
 * Comment
 */
public void openToolBarButton_ActionEvents() {
    openMenuItem_ActionEvents();
}
/**
 * Comment
 */
public void patternManagerMenuItem_ActionEvents() {
    patternManager.setVisible(true);
}
/**
 * Comment
 */
public void patternToolBarButton_ActionEvents() {
    patternManagerMenuItem_ActionEvents();
}
/**
 * Comment
 */
public void predicateBrowserMenuItem_ActionEvents() {
    predicateBrowser.setVisible(true);
}
/**
 * Comment
 */
public void predicateToolBarButton_ActionEvents() {
    predicateBrowserMenuItem_ActionEvents();
}
/**
 * Comment
 */
public void propertyManagerMenuItem_ActionEvents() {
    propertyManager.setVisible(true);
}
/**
 * Comment
 */
public void propertyToolBarButton_ActionEvents() {
    propertyManagerMenuItem_ActionEvents();
}
/**
 * Comment
 */
public void runToolBarButton_ActionEvents() {
    if (isExecuting) {
        JOptionPane.showMessageDialog(this, "Please wait until current execution is finished", "Information", JOptionPane.INFORMATION_MESSAGE);
        return;
    }
    isExecuting = true;
    new Driver().start();
}
/**
 * Comment
 */
public void saveAsMenuItem_ActionEvents() {
    Vector v = sessions.getSessions();
    
    if (v.size() == 0) {
        JOptionPane.showMessageDialog(this, "There is no session to be saved", "Information", JOptionPane.INFORMATION_MESSAGE);
        return;
    }
    
    FileChooser.chooser.setFileFilter(FileChooser.SESSION);
    FileChooser.chooser.setSelectedFile(new File(System.getProperty("user.dir")));
    FileChooser.chooser.setFileSelectionMode(FileChooser.FILES_ONLY);
    FileChooser.chooser.setSelectedFile(new File(""));

    if (FileChooser.chooser.showSaveDialog(this) == FileChooser.APPROVE_OPTION) {
        try {
            if (FileChooser.chooser.getSelectedFile().isDirectory()) {
                JOptionPane.showMessageDialog(this, "Cannot choose a directory to save a session file", "Information", JOptionPane.INFORMATION_MESSAGE);
                return;
            }
            boolean f = true;
            if (FileChooser.chooser.getSelectedFile().exists()) {
                String filename = FileChooser.chooser.getSelectedFile().getCanonicalPath();
                f = JOptionPane.showConfirmDialog(this, "Overwrite " + filename + "?", "Confirm", JOptionPane.YES_NO_OPTION) == JOptionPane.YES_OPTION;
            }
            if (f) {
                String filename = FileChooser.chooser.getSelectedFile().getCanonicalPath();
                sessions.setFilename(filename);
                saveMenuItem_ActionEvents();
                return;
            }
        } catch (Exception e) {
            JOptionPane.showMessageDialog(this, e.getMessage(), "Error", JOptionPane.ERROR_MESSAGE); 
        }
    }
}
/**
 * Comment
 */
public void saveAsToolBarButton_ActionEvents() {
    saveAsMenuItem_ActionEvents();
}
/**
 * Comment
 */
public void saveMenuItem_ActionEvents() {
    Vector v = sessions.getSessions();
    
    if (v.size() == 0) {
        JOptionPane.showMessageDialog(this, "There is no session to be saved", "Information", JOptionPane.INFORMATION_MESSAGE);
        return;
    }
    
    if ("".equals(sessions.getFilename())) {
        saveAsMenuItem_ActionEvents();
        return;
    }

    try {
        SessionsSaverLoader.save(sessions);
    } catch (Exception e) {
        JOptionPane.showMessageDialog(this, e.getMessage(), "Error", JOptionPane.ERROR_MESSAGE);
    }
}
/**
 * Comment
 */
public void saveToolBarButton_ActionEvents() {
    saveMenuItem_ActionEvents();
}
/**
 * Comment
 */
public void sessionToolBarButton_ActionEvents() {
    managerMenuItem_ActionEvents();
}
/**
 * Comment
 */
public void slicerToolBarButton_ActionEvents() {
    Icon temp = getSlicerToolBarButton().getPressedIcon();
    getSlicerToolBarButton().setPressedIcon(getSlicerToolBarButton().getIcon());
    getSlicerToolBarButton().setIcon(temp);
    doSlicer = !doSlicer;
    try {
        sessions.getActiveSession().setDoSlicer(doSlicer);
        manager.updateInfo(sessions.getActiveSession());
    } catch (Exception e) {}
}
}

---