TassUserFrame.java

package edu.udel.cis.vsl.tass.gui.impl;

import java.awt.BorderLayout;
import java.awt.Color;
import java.awt.FlowLayout;
import java.awt.Toolkit;
import java.awt.event.ActionEvent;
import java.awt.event.ActionListener;
import java.io.File;
import java.io.PrintWriter;
import java.io.StringWriter;

import javax.swing.BorderFactory;
import javax.swing.JButton;
import javax.swing.JFrame;
import javax.swing.JLabel;
import javax.swing.JMenu;
import javax.swing.JMenuBar;
import javax.swing.JMenuItem;
import javax.swing.JOptionPane;
import javax.swing.JPanel;
import javax.swing.JScrollPane;
import javax.swing.JTextArea;
import javax.swing.filechooser.FileFilter;

import edu.udel.cis.vsl.tass.config.RunConfiguration;
import edu.udel.cis.vsl.tass.gui.IF.TassUserFrameIF;
import edu.udel.cis.vsl.tass.ui.Runner;

public class TassUserFrame extends JFrame implements TassUserFrameIF,
		ActionListener {

	// Version number.
	private static final String VERSION = "v1.0";

	// Name of the software.
	private static final String NAME = "Toolkit for Accurate Scientific Software ";

	// Frame size
	static int frameWidth = 0;
	static int frameHeight = 0;

	// Content panel for the frame
	private JPanel contentPanel = null;

	// Menu bar for the frame
	private JMenuBar menuBar = null;

	// "View" menu item
	private JMenu menuView = null;
	private JMenuItem viewModel = null;
	private JMenuItem viewTrace = null;

	// "Help" menu
	private JMenu menuHelp = null;
	private JMenuItem showUsage = null;
	private JMenuItem support = null;

	// "About" menu
	private JMenu menuAbout = null;
	private JMenuItem aboutTass = null;

	// Text area
	private JTextArea displayArea = null;
	private JScrollPane displayPane = null;

	// "Verify" button
	private JButton verifyButton = null;
	private final String verifyToolTip = "Verify a single program.";

	// "Compare" button
	private JButton compareButton = null;
	private final String compareToolTip = "Compare functional equivalence of two programs.";

	// "Extract" button
	private JButton extractButton = null;
	private final String extractToolTip = "Extract model from source code.";

	// "Stop" button
	private JButton stopButton = null;
	private final String stopToolTip = "Stop verification.";

	private JPanel buttonPanel = null;

	// Status bar
	private JLabel statusLabel = null;
	private JPanel statusPanel = null;

	private JPanel lowerPanel = null;

	// Dialogs
	private VerifyDialog verifyDialog = null;
	private CompareDialog compareDialog = null;
	private ExtractDialog extractDialog = null;

	public static final long serialVersionUID = 0;

	private static final String tassDescription = "The Toolkit for Accurate Scientific Software (TASS) \nis developed "
			+ "and maintained by the Verified Software Laboratory \n at Computer and Information Science Department, \nUniversity of Delaware, Newark DE, USA";

	private static final String tassUsage = "Verify button: run TASS in verify mode for a single program.\n"
			+ "Compare button: run TASS in compare mode for a pair of programs.\n"
			+ "Extract button: extract a model from the source program.\n"
			+ "Stop button: stop TASS from running. Only become clickable after verify or compare or extract begins.";

	private static final String supportDescription = "Detailed usage about TASS on command line and \n"
			+ "with GUI as well as the description of its input language and IR model\n"
			+ "can be found on http://vsl.cis.udel.edu/tass";

	private static RunConfiguration configuration = null;

	private StringWriter sout = null;
	private PrintWriter out = null;

	// Indicate whether the option dialog normally closes.
	private static boolean optionsSet = false;

	public TassUserFrame() {

		initializeComponents();

	}

	public static void setConfiguration(RunConfiguration config) {
		configuration = config;
	}

	public static void optionsSet() {
		TassUserFrame.optionsSet = true;
	}

	// Set the title and layout of the frame.
	private void initializeComponents() {

		Toolkit config = this.getToolkit();
		setTitle(NAME + VERSION);
		frameWidth = config.getScreenSize().width / 2;
		frameHeight = config.getScreenSize().height / 2;
		setSize(frameWidth, frameHeight);
		setDefaultCloseOperation(EXIT_ON_CLOSE);

		this.contentPanel = new JPanel();
		this.contentPanel.setLayout(new BorderLayout());
		this.contentPanel.setBorder(BorderFactory.createEmptyBorder(20, 20, 2,
				20));
		this.add(this.contentPanel);

		// Add the menu bar to the frame
		setUpMenus();

		// Add text area to the frame
		setUpTextArea();

		// Add a group of command buttons
		setUpButtons();

		// Add status bar
		setUpStatusBar();

		this.lowerPanel = new JPanel();
		this.lowerPanel.setLayout(new BorderLayout());
		this.lowerPanel.add(this.buttonPanel, BorderLayout.CENTER);
		this.lowerPanel.add(this.statusPanel, BorderLayout.SOUTH);
		this.contentPanel.add(this.lowerPanel, BorderLayout.SOUTH);
		setVisible(true);
	}

	// Set up the menu bar and menu items.
	private void setUpMenus() {

		this.menuBar = new JMenuBar();

		// Create the "View" menu.
		this.menuView = new JMenu("View");

		// "View Model" menu item
		this.viewModel = new JMenuItem("View Model");
		this.viewModel.setEnabled(false);
		this.menuView.add(this.viewModel);

		// "View Trace" menu item
		this.viewTrace = new JMenuItem("View Trace");
		this.viewTrace.setEnabled(false);
		this.menuView.add(this.viewTrace);

		this.menuBar.add(this.menuView);

		// Create the "Help" menu.
		this.menuHelp = new JMenu("Help");

		// "Show Usage" menu item
		this.showUsage = new JMenuItem("Show Usage");
		this.menuHelp.add(this.showUsage);
		this.showUsage.addActionListener(this);

		// "Support" menu item
		this.support = new JMenuItem("Support");
		this.menuHelp.add(this.support);
		this.support.addActionListener(this);

		this.menuBar.add(this.menuHelp);

		// Create the "About" menu.
		this.menuAbout = new JMenu("About");

		// "About TASS" menu item
		this.aboutTass = new JMenuItem("About TASS");
		this.menuAbout.add(this.aboutTass);
		this.aboutTass.addActionListener(this);

		this.menuBar.add(this.menuAbout);

		this.setJMenuBar(this.menuBar);
	}

	private void setUpTextArea() {

		this.displayPane = new JScrollPane();

		// Text area
		this.displayArea = new JTextArea();
		this.displayArea.setLineWrap(true);
		this.displayArea.setEnabled(false);
		this.displayArea.setWrapStyleWord(true);
		this.displayArea.setBorder(BorderFactory.createEtchedBorder());
		this.displayArea.setDisabledTextColor(Color.BLACK);
		// Add the text area to the scroll pane
		this.displayPane.getViewport().add(this.displayArea);
		this.contentPanel.add(this.displayPane, BorderLayout.CENTER);
	}

	private void setUpButtons() {

		// "Verify" button
		this.verifyButton = new JButton("Verify");
		this.verifyButton.setToolTipText(this.verifyToolTip);
		this.verifyButton.addActionListener(new ActionListener() {
			public void actionPerformed(ActionEvent event) {
				if (verifyDialog == null) {
					verifyDialog = new VerifyDialog();
				} else {
					verifyDialog.setVisible(true);
				}
				if (TassUserFrame.optionsSet) {
					sout = new StringWriter();
					out = new PrintWriter(sout);
					TassUserFrame.configuration.setOut(out);
					Runner runner = new Runner(TassUserFrame.configuration);
					try {
						runner.run();
					} catch (Exception e) {
						e.printStackTrace();
						displayArea.setText(e.getMessage());
						TassUserFrame.optionsSet = false;
						return;
					}
					displayArea.setText(sout.toString());
					TassUserFrame.optionsSet = false;
				}
			}
		});

		// "Compare" button
		this.compareButton = new JButton("Compare");
		this.compareButton.setToolTipText(this.compareToolTip);
		this.compareButton.addActionListener(new ActionListener() {
			public void actionPerformed(ActionEvent event) {
				if (compareDialog == null) {
					compareDialog = new CompareDialog();
				} else {
					compareDialog.setVisible(true);
				}
				if (TassUserFrame.optionsSet) {
					sout = new StringWriter();
					out = new PrintWriter(sout);
					TassUserFrame.configuration.setOut(out);
					Runner runner = new Runner(TassUserFrame.configuration);
					try {
						runner.run();
					} catch (Exception e) {
						e.printStackTrace();
						displayArea.setText(e.getMessage());
						TassUserFrame.optionsSet = false;
						return;
					}
					displayArea.setText(sout.toString());
					TassUserFrame.optionsSet = false;
				}
			}
		});

		// "Extract" button
		this.extractButton = new JButton("Extract");
		this.extractButton.setToolTipText(this.extractToolTip);
		this.extractButton.addActionListener(new ActionListener() {
			public void actionPerformed(ActionEvent event) {
				if (extractDialog == null) {
					extractDialog = new ExtractDialog();
				} else {
					extractDialog.setVisible(true);
				}
				if (TassUserFrame.optionsSet) {
					sout = new StringWriter();
					out = new PrintWriter(sout);
					TassUserFrame.configuration.setOut(out);
					Runner runner = new Runner(TassUserFrame.configuration);
					try {
						runner.run();
					} catch (Exception e) {
						e.printStackTrace();
						displayArea.setText(e.getMessage());
						TassUserFrame.optionsSet = false;
						return;
					}
					displayArea.setText(sout.toString());
					TassUserFrame.optionsSet = false;
				}
			}
		});

		// "Stop" button
		this.stopButton = new JButton("Stop");
		this.stopButton.setEnabled(false);
		this.stopButton.setToolTipText(this.stopToolTip);
		this.extractButton.addActionListener(this);

		this.buttonPanel = new JPanel();
		this.buttonPanel.setLayout(new FlowLayout());
		this.buttonPanel
				.setBorder(BorderFactory.createTitledBorder("Commands"));

		this.buttonPanel.add(this.verifyButton);
		this.buttonPanel.add(this.compareButton);
		this.buttonPanel.add(this.extractButton);
		this.buttonPanel.add(this.stopButton);
	}

	private void setUpStatusBar() {

		this.statusLabel = new JLabel("Ready");

		this.statusPanel = new JPanel();
		this.statusPanel.setBorder(BorderFactory.createEtchedBorder());
		this.statusPanel.setLayout(new FlowLayout(FlowLayout.LEFT));
		this.statusPanel.add(this.statusLabel);
	}

	public void actionPerformed(ActionEvent event) {
		Object source = event.getSource();
		if (source.equals(this.aboutTass)) {
			JOptionPane.showMessageDialog(this, TassUserFrame.tassDescription,
					"About TASS", JOptionPane.INFORMATION_MESSAGE);
		} else if (source.equals(this.showUsage)) {
			this.displayArea.setText("");
			this.displayArea.setText(TassUserFrame.tassUsage);
		} else if (source.equals(this.support)) {
			JOptionPane.showMessageDialog(this,
					TassUserFrame.supportDescription, "Support",
					JOptionPane.INFORMATION_MESSAGE);
		}
	}

	public static void main(String args[]) {

		new TassUserFrame();
	}
}

class SourceFilter extends FileFilter {

	// Accept all directories and .mmp files.
	public boolean accept(File f) {
		if (f.isDirectory()) {
			return true;
		}

		String extension = this.getExtension(f);
		if (extension != null) {
			if (extension.equals("mmp")) {
				return true;
			} else {
				return false;
			}
		}

		return false;
	}

	// The description of this filter
	public String getDescription() {
		return "MiniMP source files";
	}

	public String getExtension(File f) {
		String ext = null;
		String s = f.getName();
		int i = s.lastIndexOf('.');

		if (i > 0 && i < s.length() - 1) {
			ext = s.substring(i + 1).toLowerCase();
		}
		return ext;
	}
}