From 0a8ace99ebe9f48b35409b62f34d6a5a117a03aa Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 18 Dec 2013 22:57:49 +0000 Subject: [PATCH] Code tidy. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7720 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- .../model/GUIMultiModelTree.java | 8155 ++++++++--------- 1 file changed, 3902 insertions(+), 4253 deletions(-) diff --git a/prism/src/userinterface/model/GUIMultiModelTree.java b/prism/src/userinterface/model/GUIMultiModelTree.java index a50f6a3b..defb2749 100644 --- a/prism/src/userinterface/model/GUIMultiModelTree.java +++ b/prism/src/userinterface/model/GUIMultiModelTree.java @@ -27,4266 +27,3915 @@ package userinterface.model; -import java.util.*; -import java.awt.*; -import java.awt.event.*; -import javax.swing.*; -import javax.swing.tree.*; -import javax.swing.event.*; - -import userinterface.*; +import java.awt.BorderLayout; +import java.awt.Color; +import java.awt.Component; +import java.awt.Rectangle; +import java.awt.event.ActionEvent; +import java.awt.event.ActionListener; +import java.awt.event.KeyEvent; +import java.awt.event.MouseEvent; +import java.awt.event.MouseListener; +import java.util.ArrayList; +import java.util.EventObject; +import java.util.Vector; + +import javax.swing.AbstractAction; +import javax.swing.Action; +import javax.swing.ButtonGroup; +import javax.swing.ImageIcon; +import javax.swing.JComboBox; +import javax.swing.JOptionPane; +import javax.swing.JPanel; +import javax.swing.JPopupMenu; +import javax.swing.JRadioButton; +import javax.swing.JScrollPane; +import javax.swing.JTextField; +import javax.swing.JTree; +import javax.swing.ToolTipManager; +import javax.swing.event.CellEditorListener; +import javax.swing.event.ChangeEvent; +import javax.swing.tree.DefaultMutableTreeNode; +import javax.swing.tree.DefaultTreeCellEditor; +import javax.swing.tree.DefaultTreeCellRenderer; +import javax.swing.tree.DefaultTreeModel; +import javax.swing.tree.TreeCellEditor; +import javax.swing.tree.TreeNode; +import javax.swing.tree.TreePath; + +import parser.ast.ConstantList; +import parser.ast.Declaration; +import parser.ast.DeclarationInt; +import parser.ast.Expression; +import parser.ast.ExpressionIdent; +import parser.ast.Module; +import parser.ast.ModulesFile; +import parser.type.Type; +import parser.type.TypeBool; +import parser.type.TypeClock; +import parser.type.TypeDouble; +import parser.type.TypeInt; +import prism.ModelType; +import prism.PrismException; +import userinterface.GUIPrism; +import userinterface.model.computation.LoadGraphicModelThread; +import userinterface.model.graphicModel.Decision; import userinterface.model.graphicModel.GUIGraphicModelEditor; -import userinterface.model.graphicModel.*; -import userinterface.model.computation.*; -import parser.ast.*; -import parser.type.*; -import prism.*; +import userinterface.model.graphicModel.ModuleModel; +import userinterface.model.graphicModel.ProbTransition; +import userinterface.model.graphicModel.State; +import userinterface.model.graphicModel.Transition; +@SuppressWarnings("serial") public class GUIMultiModelTree extends JPanel implements MouseListener { - //Constants - public static final int TREE_SYNCHRONIZED_GOOD = 0; - public static final int TREE_SYNCHRONIZED_BAD = 1; - public static final int TREE_NOT_SYNCHRONIZED = 2; - - //Attributes - private GUIMultiModelHandler handler; - private GUIGraphicModelEditor graphicEditor; - private boolean editable; - - //Graphical elements - private JTree tree; - private JPopupMenu moduleCollectionPopup; - private Action addModule; - private JPopupMenu declarationCollectionPopup; - private Action addBooleanGlobal, addIntegerGlobal; - private JPopupMenu constantsCollectionPopup; - private Action addBooleanConstant, addDoubleConstant, addIntegerConstant; - private JPopupMenu modulePopup; - private Action renameModule, removeModule, addBoolean, addInteger; - private JPopupMenu declarationPopup; - private Action renameDeclaration, removeDeclaration; - private JPopupMenu expressionPopup; - private Action editExpression; - private JPopupMenu modelTypePopup; - private JRadioButton non, pro, sto; - - //Tree listener - private EventListenerList listenerList = new EventListenerList(); - - //Tree nodes - private DefaultTreeModel theModel; - private ModelRootNode root; - private ModelTypeNode modelType; - private ModuleCollectionNode modules; - private DeclarationCollectionNode declarations; - private ConstantCollectionNode constants; - - private ArrayList editableModules; - private ArrayList editableDeclarations; - private ArrayList editableConstants; - - private ImageIcon animIcon; - private boolean isParsing; - private IconThread parseThread; - - private PrismTreeNode lastPopNode; - - //State - private int parseSynchState; - - public GUIMultiModelTree(GUIMultiModelHandler handler, boolean editable) - { - this.handler = handler; - this.editable = editable; - graphicEditor = null; - root = new ModelRootNode(); - theModel = new DefaultTreeModel(root); - newTree(editable); - initComponents(); - animIcon = GUIPrism.getIconFromImage("smallClockAnim1.png"); - isParsing = false; - tree.addMouseListener(this); - - tree.setEditable(true); - - JTextArea area = new JTextArea(); - ToolTipManager.sharedInstance().registerComponent(tree); - } - - public GUIMultiModelTree(GUIMultiModelHandler handler) - { - this(handler, false); - } - - static int modCounter = 1; - public void a_addModule() - { - ModuleNode newNode = new ModuleNode("newModule"+modCounter, true); - try - { - newNode.addVariable(new StateVarNode(newNode)); - } - catch(prism.PrismException e) - { - //canny get here - } - editableModules.add(newNode); - modules.addModule(newNode); - int index = modules.getIndex(newNode); - theModel.nodesWereInserted(modules, new int[] - {index}); - modCounter++; - if(this.graphicEditor != null) graphicEditor.addNewModule(newNode); - if(graphicEditor != null) graphicEditor.setModified(); - - } - - public ModuleNode a_requestNewModule(String name) - { - ModuleNode newNode = new ModuleNode(name, true); - try - { - newNode.addVariable(new StateVarNode(newNode)); - } - catch(prism.PrismException e) - { - //canny get here - } - editableModules.add(newNode); - modules.addModule(newNode); - int index = modules.getIndex(newNode); - theModel.nodesWereInserted(modules, new int[] - {index}); - modCounter++; - if(this.graphicEditor != null) graphicEditor.addNewModule(newNode); - if(graphicEditor != null) graphicEditor.setModified(); - return newNode; - } - - static int globCounter = 1; - public void a_addIntegerGlobal() - { - try - { - Expression init = handler.getGUIPlugin().getPrism().parseSingleExpressionString("0"); - Expression min = handler.getGUIPlugin().getPrism().parseSingleExpressionString("0"); - Expression max = handler.getGUIPlugin().getPrism().parseSingleExpressionString("0"); - - GlobalNode newNode = new GlobalNode("g"+globCounter, init, min, max, true); - editableDeclarations.add(newNode); - declarations.addDeclaration(newNode); - int index = declarations.getIndex(newNode); - theModel.nodesWereInserted(declarations, new int[] - {index}); - globCounter++; - if(graphicEditor != null) graphicEditor.setModified(); - } - catch(Exception e) - { - System.err.println("UNEXPECTED ERROR: "+e.getMessage()); - e.printStackTrace(); - //This should never happen - } - - handler.hasModified(true); - } - - public void a_addIntegerGlobal(String name, String mins, String maxs, String inits) throws PrismException - { - try - { - Expression init = handler.getGUIPlugin().getPrism().parseSingleExpressionString(inits); - Expression min = handler.getGUIPlugin().getPrism().parseSingleExpressionString(mins); - Expression max = handler.getGUIPlugin().getPrism().parseSingleExpressionString(maxs); - - GlobalNode newNode = new GlobalNode(name, init, min, max, true); - editableDeclarations.add(newNode); - declarations.addDeclaration(newNode); - int index = declarations.getIndex(newNode); - theModel.nodesWereInserted(declarations, new int[] - {index}); - globCounter++; - if(graphicEditor != null) graphicEditor.setModified(); - } - catch(Exception e) - { - throw new PrismException("Global integer "+name+" has invalid parameter"); - } - - handler.hasModified(true); - } - - public void a_addBooleanGlobal() - { - try - { - Expression init = handler.getGUIPlugin().getPrism().parseSingleExpressionString("false"); - - GlobalBoolNode newNode = new GlobalBoolNode("g"+globCounter, init, true); - editableDeclarations.add(newNode); - declarations.addDeclaration(newNode); - int index = declarations.getIndex(newNode); - theModel.nodesWereInserted(declarations, new int[] - {index}); - globCounter++; - if(graphicEditor != null) graphicEditor.setModified(); - } - catch(Exception e) - { - System.err.println("UNEXPECTED ERROR: "+e.getMessage()); - e.printStackTrace(); - //This should never happen - } - handler.hasModified(true); - } - - public void a_addBooleanGlobal(String name, String inits) throws PrismException - { - try - { - Expression init = handler.getGUIPlugin().getPrism().parseSingleExpressionString(inits); - - GlobalBoolNode newNode = new GlobalBoolNode(name, init, true); - editableDeclarations.add(newNode); - declarations.addDeclaration(newNode); - int index = declarations.getIndex(newNode); - theModel.nodesWereInserted(declarations, new int[] - {index}); - globCounter++; - if(graphicEditor != null) graphicEditor.setModified(); - } - catch(Exception e) - { - throw new PrismException("Global boolean "+name+" has invalid parameter"); - } - handler.hasModified(true); - } - - static int consCount = 1; - public void a_addIntegerConstant() - { - try - { - Expression value = handler.getGUIPlugin().getPrism().parseSingleExpressionString("0"); - IntegerConstantNode newNode = new IntegerConstantNode("c"+consCount, value, true); - editableConstants.add(newNode); - constants.addConstant(newNode); - int index = constants.getIndex(newNode); - theModel.nodesWereInserted(constants, new int[] - {index}); - consCount++; - if(graphicEditor != null) graphicEditor.setModified(); - } - catch(Exception e) - { - System.err.println("UNEXPECTED ERROR: "+e.getMessage()); - e.printStackTrace(); - } - handler.hasModified(true); - } - - public void a_addIntegerConstant(String name, String val) throws PrismException - { - try - { - Expression value; - if(val == null) - value = null; - else - value = handler.getGUIPlugin().getPrism().parseSingleExpressionString(val); - IntegerConstantNode newNode = new IntegerConstantNode(name, value, true); - editableConstants.add(newNode); - constants.addConstant(newNode); - int index = constants.getIndex(newNode); - theModel.nodesWereInserted(constants, new int[] - {index}); - consCount++; - if(graphicEditor != null) graphicEditor.setModified(); - } - catch(Exception e) - { - throw new PrismException("Constant integer "+name+" has invalid parameter"); - } - handler.hasModified(true); - } - - public void a_addBooleanConstant() - { - try - { - Expression value = handler.getGUIPlugin().getPrism().parseSingleExpressionString("false"); - BoolConstantNode newNode = new BoolConstantNode("c"+consCount, value, true); - editableConstants.add(newNode); - constants.addConstant(newNode); - int index = constants.getIndex(newNode); - theModel.nodesWereInserted(constants, new int[] - {index}); - consCount++; - if(graphicEditor != null) graphicEditor.setModified(); - } - catch(Exception e) - { - System.err.println("UNEXPECTED ERROR: "+e.getMessage()); - e.printStackTrace(); - } - handler.hasModified(true); - } - - public void a_addBooleanConstant(String name, String val) throws PrismException - { - try - { - Expression value; - if(val == null) - value = null; - else - value = handler.getGUIPlugin().getPrism().parseSingleExpressionString(val); - BoolConstantNode newNode = new BoolConstantNode(name, value, true); - editableConstants.add(newNode); - constants.addConstant(newNode); - int index = constants.getIndex(newNode); - theModel.nodesWereInserted(constants, new int[] - {index}); - consCount++; - if(graphicEditor != null) graphicEditor.setModified(); - } - catch(Exception e) - { - throw new PrismException("Constant boolean "+name+" has invalid parameter"); - } - handler.hasModified(true); - } - - public void a_addDoubleConstant() - { - try - { - Expression value = handler.getGUIPlugin().getPrism().parseSingleExpressionString("0.0"); - DoubleConstantNode newNode = new DoubleConstantNode("c"+consCount, value, true); - editableConstants.add(newNode); - constants.addConstant(newNode); - int index = constants.getIndex(newNode); - theModel.nodesWereInserted(constants, new int[] - {index}); - consCount++; - if(graphicEditor != null) graphicEditor.setModified(); - } - catch(Exception e) - { - System.err.println("UNEXPECTED ERROR: "+e.getMessage()); - e.printStackTrace(); - } - handler.hasModified(true); - } - - public void a_addDoubleConstant(String name, String val) throws PrismException - { - try - { - Expression value; - if(val == null) - value = null; - else - value = handler.getGUIPlugin().getPrism().parseSingleExpressionString(val); - DoubleConstantNode newNode = new DoubleConstantNode(name, value, true); - editableConstants.add(newNode); - constants.addConstant(newNode); - int index = constants.getIndex(newNode); - theModel.nodesWereInserted(constants, new int[] - {index}); - consCount++; - if(graphicEditor != null) graphicEditor.setModified(); - } - catch(Exception e) - { - throw new PrismException("Constant double "+name+" has invalid parameter"); - } - handler.hasModified(true); - } - - public void a_removeModule(ModuleNode m) - { - int index = modules.getIndex(m); - editableModules.remove(m); - modules.remove(m); - theModel.nodesWereRemoved(modules, new int[] - {index}, new Object[] - {m}); - if(graphicEditor != null) graphicEditor.removeModule(m); - else - { - //System.out.println("graphic editor is null"); - } - if(graphicEditor != null) graphicEditor.setModified(); - else - { - //System.out.println("graphic editor is null"); - } - handler.hasModified(true); - } - - public void a_renameModule(ModuleNode m) - { - - String s = JOptionPane.showInputDialog("New module name:", m.getName()); - if(s == null) return; - - try - { - Expression exp = handler.getGUIPlugin().getPrism().parseSingleExpressionString(s); - if(exp instanceof ExpressionIdent) - { - m.setName(s); - theModel.nodeChanged(m); - theModel.nodeStructureChanged(m); - if(this.graphicEditor != null) - { - graphicEditor.notifyChangeTo(m); - } - } - else - { - handler.getGUIPlugin().error("Invalid module name"); - } - } - catch(PrismException exx) - { - handler.getGUIPlugin().error("Invalid module name"); - } - - - - handler.hasModified(true); - } - - public void a_renameDeclaration(DeclarationNode d) - { - String type = ""; - if(d instanceof BoolNode || d instanceof VarNode) - type = " variable"; - else if(d instanceof GlobalNode || d instanceof GlobalBoolNode) - type = " global"; - else if(d instanceof ConstantNode) - type = " constant"; - - String s = JOptionPane.showInputDialog("New"+type+" name:", d.getName()); - if(s == null) return; - - try - { - Expression exp = handler.getGUIPlugin().getPrism().parseSingleExpressionString(s); - if(exp instanceof ExpressionIdent) - { - d.setName(s); - theModel.nodeChanged(d); - theModel.nodeStructureChanged(d); - } - else - { - handler.getGUIPlugin().error("Invalid declaration name"); - } - } - catch(PrismException exx) - { - handler.getGUIPlugin().error("Invalid module name"); - } - - - handler.hasModified(true); - } - - public void a_removeVariable(DeclarationNode d, ModuleNode m) - { - int index = m.getIndex(d); - m.remove(d); - theModel.nodesWereRemoved(m, new int[] - {index}, new Object[] - {d}); - if(graphicEditor != null) graphicEditor.setModified(); - handler.hasModified(true); - } - - public void a_removeGlobal(DeclarationNode d) - { - int index = declarations.getIndex(d); - editableDeclarations.remove(d); - declarations.remove(d); - theModel.nodesWereRemoved(declarations, new int[] - {index}, new Object[] - {d}); - if(graphicEditor != null) graphicEditor.setModified(); - handler.hasModified(true); - } - - public void a_removeConstant(ConstantNode c) - { - int index = constants.getIndex(c); - editableConstants.remove(c); - constants.remove(c); - theModel.nodesWereRemoved(constants, new int[] - {index}, new Object[] - {c}); - if(graphicEditor != null) graphicEditor.setModified(); - handler.hasModified(true); - } - - - public void a_addLocalBoolean(ModuleNode m, LoadGraphicModelThread.BooleanVariable var) throws PrismException - { - try - { - Expression init; - if(var != null) - init = handler.getGUIPlugin().getPrism().parseSingleExpressionString(var.init); - else init = handler.getGUIPlugin().getPrism().parseSingleExpressionString("false"); - - BoolNode newNode = new BoolNode(var.name, init, true); - m.add(newNode); - int index = m.getIndex(newNode); - theModel.nodesWereInserted(m, new int[] - {index}); - varCount++; - if(graphicEditor != null) graphicEditor.setModified(); - } - catch(Exception e) - { - throw new PrismException("Local boolean "+var.name+" has an invalid parameter"); - } - handler.hasModified(true); - } - - static int varCount = 1; - public void a_addLocalBoolean(ModuleNode m) - { - try - { - Expression init = handler.getGUIPlugin().getPrism().parseSingleExpressionString("false"); - - BoolNode newNode = new BoolNode("v"+varCount, init, true); - m.add(newNode); - int index = m.getIndex(newNode); - theModel.nodesWereInserted(m, new int[] - {index}); - varCount++; - if(graphicEditor != null) graphicEditor.setModified(); - } - catch(Exception e) - { - System.err.println("UNEXPECTED ERROR: "+e.getMessage()); - e.printStackTrace(); - //This should never happen - } - handler.hasModified(true); - } - - public void a_addLocalInteger(ModuleNode m, LoadGraphicModelThread.IntegerVariable var) throws PrismException - { - try - { - Expression init; - if(var.init == null) - init = handler.getGUIPlugin().getPrism().parseSingleExpressionString("0"); - else - init = handler.getGUIPlugin().getPrism().parseSingleExpressionString(var.init); - Expression min = handler.getGUIPlugin().getPrism().parseSingleExpressionString(var.min); - Expression max = handler.getGUIPlugin().getPrism().parseSingleExpressionString(var.max); - - VarNode newNode = new VarNode(var.name, init, min, max, true); - m.addVariable(newNode); - int index = m.getIndex(newNode); - theModel.nodesWereInserted(m, new int[] - {index}); - varCount++; - if(graphicEditor != null) graphicEditor.setModified(); - } - catch(Exception e) - { - throw new PrismException("Local integer "+var.name+" has an invalid parameter"); - } - handler.hasModified(true); - } - - public void a_addLocalInteger(ModuleNode m) - { - try - { - Expression init = handler.getGUIPlugin().getPrism().parseSingleExpressionString("0"); - Expression min = handler.getGUIPlugin().getPrism().parseSingleExpressionString("0"); - Expression max = handler.getGUIPlugin().getPrism().parseSingleExpressionString("0"); - - VarNode newNode = new VarNode("v"+varCount, init, min, max, true); - m.addVariable(newNode); - int index = m.getIndex(newNode); - theModel.nodesWereInserted(m, new int[] - {index}); - varCount++; - if(graphicEditor != null) graphicEditor.setModified(); - } - catch(Exception e) - { - System.err.println("UNEXPECTED ERROR: "+e.getMessage()); - e.printStackTrace(); - //This should never happen - } - handler.hasModified(true); - } - - public void a_editExpression(ExpressionNode en) - { - String defa; - if(en.getValue() == null) defa = "?"; - else defa = en.getValue().toString(); - String s = JOptionPane.showInputDialog("New Expression:", defa); - if(s == null) return; - try - { - if(s.equals("")) - { - en.setValue(null); - } - else - { - Expression exp = handler.getGUIPlugin().getPrism().parseSingleExpressionString(s); - en.setValue(exp); - } - theModel.nodeChanged(en); - } - catch(Exception e) - { - handler.getGUIPlugin().error("Syntax error in expression:\n"+s); - } - - handler.hasModified(true); - } - - public void a_setModelType(ModelType type) - { - modelType.setModelType(type); - handler.hasModified(true); - } - - public int getParseSynchState() - { - return parseSynchState; - } - - public void setGraphicModelEditor(GUIGraphicModelEditor graphicEditor) - { - this.graphicEditor = graphicEditor; - } - - public void startParsing() - { - isParsing = true; - if(parseThread != null) parseThread.interrupt(); - parseThread = new IconThread(0); - parseThread.start(); - } - - public void stopParsing() - { - isParsing = false; - if(parseThread != null) parseThread.interrupt(); - tree.repaint(); - } - - public void newTree() - { this.newTree(false); } - - public void newTree(boolean editable) - { - this.editable = editable; - root.removeAllChildren(); - parseSynchState = TREE_NOT_SYNCHRONIZED; - { - root.setUserObject("Model: " + handler.getShortActiveFileName()); - modelType = new ModelTypeNode("", editable); - root.add(modelType); - if(editable) - { - modules = new GUIMultiModelTree.ModuleCollectionNode(); - declarations = new GUIMultiModelTree.DeclarationCollectionNode(); - constants = new GUIMultiModelTree.ConstantCollectionNode(); - root.add(modules); - root.add(declarations); - root.add(constants); - theModel.nodeStructureChanged(root); - } - else - { - modules = new ModuleCollectionNode(); - declarations = new DeclarationCollectionNode(); - constants = new ConstantCollectionNode(); - theModel.nodeStructureChanged(root); - } - } - editableModules = new ArrayList(); - editableDeclarations = new ArrayList(); - editableConstants = new ArrayList(); - - modCounter = 1; - } - - public void update(ModulesFile parsedModel) - { - parseSynchState = (parsedModel==null) ? TREE_NOT_SYNCHRONIZED : TREE_SYNCHRONIZED_GOOD; - if(editable) updateEditable(parsedModel); - else updateUnEditable(parsedModel); - } - - private void updateUnEditable(ModulesFile parsedModel) - { - String fn = handler.getShortActiveFileName(); - if(!root.getUserObject().equals(fn)) - { - root.setUserObject("Model: " + fn); - theModel.nodeChanged(root); - } - - if(parsedModel != null) - { - String tp = parsedModel.getTypeString(); - if(!modelType.getValue().equals(tp)) - { - modelType.setUserObject(tp); - theModel.nodeChanged(modelType); - } - - //MODULES - - //If there is no module tree, but we need to have modules, add the tre - if(root.getIndex(modules) == -1 && parsedModel.getNumModules() > 0) - { - root.add(modules); - theModel.nodesWereInserted(root, new int[] - {root.getIndex(modules)}); - } - //If there is a module tree, but no modules, remove the module tree - else if(root.getIndex(modules) != -1 && parsedModel.getNumModules() == 0) - { - int index = root.getIndex(modules); - root.remove(modules); - theModel.nodesWereRemoved(root, new int[] - {index}, new Object[] - {modules}); - } - - /* Create 2 ArrayLists. One of Modules in the tree and one of modules - * not in the tree. */ - ArrayList inTree = new ArrayList(); - ArrayList notInTree = new ArrayList(); - - for(int i = 0; i < parsedModel.getNumModules(); i++) - { - Module aMod = parsedModel.getModule(i); - if(moduleIsMember(aMod)) inTree.add(aMod); - else notInTree.add(aMod); - } - - //make sure modules in the tree are valid - for(int i = 0; i < inTree.size(); i++) - { - Module inTreeMod = (Module)inTree.get(i); - int treeIndex = getModuleTreeIndexOf(inTreeMod); //should not be -1 - ModuleNode inTreeNode = (ModuleNode)modules.getChildAt(treeIndex); - - /* Check its variables getting variables which are already there - * and putting them in varInTree, and getting variables which - * are not there and putting them in varNotInTree*/ - ArrayList varInTree = new ArrayList(); - ArrayList varNotInTree = new ArrayList(); - - for(int j = 0; j < inTreeMod.getNumDeclarations(); j++) - { - Declaration d = inTreeMod.getDeclaration(j); - if(variableIsMember(d, inTreeNode)) varInTree.add(d); - else varNotInTree.add(d); - } - - //make sure variables in this module tree are valid - for(int j = 0; j < varInTree.size(); j++) - { - Declaration inTreeDec = (Declaration)varInTree.get(j); - int decIndex = getVarTreeIndexOf(inTreeDec, inTreeNode); - DeclarationNode dNode = (DeclarationNode)inTreeNode.getChildAt(decIndex); - if(dNode instanceof VarNode) - { - VarNode vNode = (VarNode)dNode; - DeclarationInt dt = (DeclarationInt)inTreeDec.getDeclType(); - vNode.setInitial(parsedModel.getSystemDefn() == null ? inTreeDec.getStartOrDefault() : null); - vNode.setMin(dt.getLow()); - vNode.setMax(dt.getHigh()); - theModel.nodesChanged(vNode, new int [] - {0,1,2}); - } - else if(dNode instanceof BoolNode) - { - BoolNode bNode = (BoolNode)dNode; - bNode.setInitial(parsedModel.getSystemDefn() == null ? inTreeDec.getStartOrDefault() : null); - theModel.nodesChanged(bNode, new int[] - {0}); - } - - } - //add variable in varNotInTree to the tree - int[] cIndices = new int[varNotInTree.size()]; - for(int j = 0; j < varNotInTree.size(); j++) - { - Declaration notTreeDec = (Declaration)varNotInTree.get(j); - if(notTreeDec.getType() instanceof TypeInt) - { - if (notTreeDec.getDeclType() instanceof DeclarationInt) { + //Constants + public static final int TREE_SYNCHRONIZED_GOOD = 0; + public static final int TREE_SYNCHRONIZED_BAD = 1; + public static final int TREE_NOT_SYNCHRONIZED = 2; + + //Attributes + private GUIMultiModelHandler handler; + private GUIGraphicModelEditor graphicEditor; + private boolean editable; + + //Graphical elements + private JTree tree; + private JPopupMenu moduleCollectionPopup; + private Action addModule; + private JPopupMenu declarationCollectionPopup; + private Action addBooleanGlobal, addIntegerGlobal; + private JPopupMenu constantsCollectionPopup; + private Action addBooleanConstant, addDoubleConstant, addIntegerConstant; + private JPopupMenu modulePopup; + private Action renameModule, removeModule, addBoolean, addInteger; + private JPopupMenu declarationPopup; + private Action renameDeclaration, removeDeclaration; + private JPopupMenu expressionPopup; + private Action editExpression; + private JPopupMenu modelTypePopup; + private JRadioButton non, pro, sto; + + //Tree nodes + private DefaultTreeModel theModel; + private ModelRootNode root; + private ModelTypeNode modelType; + private ModuleCollectionNode modules; + private DeclarationCollectionNode declarations; + private ConstantCollectionNode constants; + + private ArrayList editableModules; + private ArrayList editableDeclarations; + private ArrayList editableConstants; + + private ImageIcon animIcon; + private boolean isParsing; + private IconThread parseThread; + + private PrismTreeNode lastPopNode; + + //State + private int parseSynchState; + + public GUIMultiModelTree(GUIMultiModelHandler handler, boolean editable) + { + this.handler = handler; + this.editable = editable; + graphicEditor = null; + root = new ModelRootNode(); + theModel = new DefaultTreeModel(root); + newTree(editable); + initComponents(); + animIcon = GUIPrism.getIconFromImage("smallClockAnim1.png"); + isParsing = false; + tree.addMouseListener(this); + tree.setEditable(true); + ToolTipManager.sharedInstance().registerComponent(tree); + } + + public GUIMultiModelTree(GUIMultiModelHandler handler) + { + this(handler, false); + } + + static int modCounter = 1; + + public void a_addModule() + { + ModuleNode newNode = new ModuleNode("newModule" + modCounter, true); + newNode.addVariable(new StateVarNode(newNode)); + editableModules.add(newNode); + modules.addModule(newNode); + int index = modules.getIndex(newNode); + theModel.nodesWereInserted(modules, new int[] { index }); + modCounter++; + if (this.graphicEditor != null) + graphicEditor.addNewModule(newNode); + if (graphicEditor != null) + graphicEditor.setModified(); + } + + public ModuleNode a_requestNewModule(String name) + { + ModuleNode newNode = new ModuleNode(name, true); + newNode.addVariable(new StateVarNode(newNode)); + editableModules.add(newNode); + modules.addModule(newNode); + int index = modules.getIndex(newNode); + theModel.nodesWereInserted(modules, new int[] { index }); + modCounter++; + if (this.graphicEditor != null) + graphicEditor.addNewModule(newNode); + if (graphicEditor != null) + graphicEditor.setModified(); + return newNode; + } + + static int globCounter = 1; + + public void a_addIntegerGlobal() + { + try { + Expression init = handler.getGUIPlugin().getPrism().parseSingleExpressionString("0"); + Expression min = handler.getGUIPlugin().getPrism().parseSingleExpressionString("0"); + Expression max = handler.getGUIPlugin().getPrism().parseSingleExpressionString("0"); + + GlobalNode newNode = new GlobalNode("g" + globCounter, init, min, max, true); + editableDeclarations.add(newNode); + declarations.addDeclaration(newNode); + int index = declarations.getIndex(newNode); + theModel.nodesWereInserted(declarations, new int[] { index }); + globCounter++; + if (graphicEditor != null) + graphicEditor.setModified(); + } catch (Exception e) { + System.err.println("UNEXPECTED ERROR: " + e.getMessage()); + e.printStackTrace(); + //This should never happen + } + + handler.hasModified(true); + } + + public void a_addIntegerGlobal(String name, String mins, String maxs, String inits) throws PrismException + { + try { + Expression init = handler.getGUIPlugin().getPrism().parseSingleExpressionString(inits); + Expression min = handler.getGUIPlugin().getPrism().parseSingleExpressionString(mins); + Expression max = handler.getGUIPlugin().getPrism().parseSingleExpressionString(maxs); + + GlobalNode newNode = new GlobalNode(name, init, min, max, true); + editableDeclarations.add(newNode); + declarations.addDeclaration(newNode); + int index = declarations.getIndex(newNode); + theModel.nodesWereInserted(declarations, new int[] { index }); + globCounter++; + if (graphicEditor != null) + graphicEditor.setModified(); + } catch (Exception e) { + throw new PrismException("Global integer " + name + " has invalid parameter"); + } + + handler.hasModified(true); + } + + public void a_addBooleanGlobal() + { + try { + Expression init = handler.getGUIPlugin().getPrism().parseSingleExpressionString("false"); + GlobalBoolNode newNode = new GlobalBoolNode("g" + globCounter, init, true); + editableDeclarations.add(newNode); + declarations.addDeclaration(newNode); + int index = declarations.getIndex(newNode); + theModel.nodesWereInserted(declarations, new int[] { index }); + globCounter++; + if (graphicEditor != null) + graphicEditor.setModified(); + } catch (Exception e) { + System.err.println("UNEXPECTED ERROR: " + e.getMessage()); + e.printStackTrace(); + //This should never happen + } + handler.hasModified(true); + } + + public void a_addBooleanGlobal(String name, String inits) throws PrismException + { + try { + Expression init = handler.getGUIPlugin().getPrism().parseSingleExpressionString(inits); + GlobalBoolNode newNode = new GlobalBoolNode(name, init, true); + editableDeclarations.add(newNode); + declarations.addDeclaration(newNode); + int index = declarations.getIndex(newNode); + theModel.nodesWereInserted(declarations, new int[] { index }); + globCounter++; + if (graphicEditor != null) + graphicEditor.setModified(); + } catch (Exception e) { + throw new PrismException("Global boolean " + name + " has invalid parameter"); + } + handler.hasModified(true); + } + + static int consCount = 1; + + public void a_addIntegerConstant() + { + try { + Expression value = handler.getGUIPlugin().getPrism().parseSingleExpressionString("0"); + IntegerConstantNode newNode = new IntegerConstantNode("c" + consCount, value, true); + editableConstants.add(newNode); + constants.addConstant(newNode); + int index = constants.getIndex(newNode); + theModel.nodesWereInserted(constants, new int[] { index }); + consCount++; + if (graphicEditor != null) + graphicEditor.setModified(); + } catch (Exception e) { + System.err.println("UNEXPECTED ERROR: " + e.getMessage()); + e.printStackTrace(); + } + handler.hasModified(true); + } + + public void a_addIntegerConstant(String name, String val) throws PrismException + { + try { + Expression value; + if (val == null) + value = null; + else + value = handler.getGUIPlugin().getPrism().parseSingleExpressionString(val); + IntegerConstantNode newNode = new IntegerConstantNode(name, value, true); + editableConstants.add(newNode); + constants.addConstant(newNode); + int index = constants.getIndex(newNode); + theModel.nodesWereInserted(constants, new int[] { index }); + consCount++; + if (graphicEditor != null) + graphicEditor.setModified(); + } catch (Exception e) { + throw new PrismException("Constant integer " + name + " has invalid parameter"); + } + handler.hasModified(true); + } + + public void a_addBooleanConstant() + { + try { + Expression value = handler.getGUIPlugin().getPrism().parseSingleExpressionString("false"); + BoolConstantNode newNode = new BoolConstantNode("c" + consCount, value, true); + editableConstants.add(newNode); + constants.addConstant(newNode); + int index = constants.getIndex(newNode); + theModel.nodesWereInserted(constants, new int[] { index }); + consCount++; + if (graphicEditor != null) + graphicEditor.setModified(); + } catch (Exception e) { + System.err.println("UNEXPECTED ERROR: " + e.getMessage()); + e.printStackTrace(); + } + handler.hasModified(true); + } + + public void a_addBooleanConstant(String name, String val) throws PrismException + { + try { + Expression value; + if (val == null) + value = null; + else + value = handler.getGUIPlugin().getPrism().parseSingleExpressionString(val); + BoolConstantNode newNode = new BoolConstantNode(name, value, true); + editableConstants.add(newNode); + constants.addConstant(newNode); + int index = constants.getIndex(newNode); + theModel.nodesWereInserted(constants, new int[] { index }); + consCount++; + if (graphicEditor != null) + graphicEditor.setModified(); + } catch (Exception e) { + throw new PrismException("Constant boolean " + name + " has invalid parameter"); + } + handler.hasModified(true); + } + + public void a_addDoubleConstant() + { + try { + Expression value = handler.getGUIPlugin().getPrism().parseSingleExpressionString("0.0"); + DoubleConstantNode newNode = new DoubleConstantNode("c" + consCount, value, true); + editableConstants.add(newNode); + constants.addConstant(newNode); + int index = constants.getIndex(newNode); + theModel.nodesWereInserted(constants, new int[] { index }); + consCount++; + if (graphicEditor != null) + graphicEditor.setModified(); + } catch (Exception e) { + System.err.println("UNEXPECTED ERROR: " + e.getMessage()); + e.printStackTrace(); + } + handler.hasModified(true); + } + + public void a_addDoubleConstant(String name, String val) throws PrismException + { + try { + Expression value; + if (val == null) + value = null; + else + value = handler.getGUIPlugin().getPrism().parseSingleExpressionString(val); + DoubleConstantNode newNode = new DoubleConstantNode(name, value, true); + editableConstants.add(newNode); + constants.addConstant(newNode); + int index = constants.getIndex(newNode); + theModel.nodesWereInserted(constants, new int[] { index }); + consCount++; + if (graphicEditor != null) + graphicEditor.setModified(); + } catch (Exception e) { + throw new PrismException("Constant double " + name + " has invalid parameter"); + } + handler.hasModified(true); + } + + public void a_removeModule(ModuleNode m) + { + int index = modules.getIndex(m); + editableModules.remove(m); + modules.remove(m); + theModel.nodesWereRemoved(modules, new int[] { index }, new Object[] { m }); + if (graphicEditor != null) + graphicEditor.removeModule(m); + else { + //System.out.println("graphic editor is null"); + } + if (graphicEditor != null) + graphicEditor.setModified(); + else { + //System.out.println("graphic editor is null"); + } + handler.hasModified(true); + } + + public void a_renameModule(ModuleNode m) + { + + String s = JOptionPane.showInputDialog("New module name:", m.getName()); + if (s == null) + return; + + try { + Expression exp = handler.getGUIPlugin().getPrism().parseSingleExpressionString(s); + if (exp instanceof ExpressionIdent) { + m.setName(s); + theModel.nodeChanged(m); + theModel.nodeStructureChanged(m); + if (this.graphicEditor != null) { + graphicEditor.notifyChangeTo(m); + } + } else { + handler.getGUIPlugin().error("Invalid module name"); + } + } catch (PrismException exx) { + handler.getGUIPlugin().error("Invalid module name"); + } + + handler.hasModified(true); + } + + public void a_renameDeclaration(DeclarationNode d) + { + String type = ""; + if (d instanceof BoolNode || d instanceof VarNode) + type = " variable"; + else if (d instanceof GlobalNode || d instanceof GlobalBoolNode) + type = " global"; + else if (d instanceof ConstantNode) + type = " constant"; + + String s = JOptionPane.showInputDialog("New" + type + " name:", d.getName()); + if (s == null) + return; + + try { + Expression exp = handler.getGUIPlugin().getPrism().parseSingleExpressionString(s); + if (exp instanceof ExpressionIdent) { + d.setName(s); + theModel.nodeChanged(d); + theModel.nodeStructureChanged(d); + } else { + handler.getGUIPlugin().error("Invalid declaration name"); + } + } catch (PrismException exx) { + handler.getGUIPlugin().error("Invalid module name"); + } + + handler.hasModified(true); + } + + public void a_removeVariable(DeclarationNode d, ModuleNode m) + { + int index = m.getIndex(d); + m.remove(d); + theModel.nodesWereRemoved(m, new int[] { index }, new Object[] { d }); + if (graphicEditor != null) + graphicEditor.setModified(); + handler.hasModified(true); + } + + public void a_removeGlobal(DeclarationNode d) + { + int index = declarations.getIndex(d); + editableDeclarations.remove(d); + declarations.remove(d); + theModel.nodesWereRemoved(declarations, new int[] { index }, new Object[] { d }); + if (graphicEditor != null) + graphicEditor.setModified(); + handler.hasModified(true); + } + + public void a_removeConstant(ConstantNode c) + { + int index = constants.getIndex(c); + editableConstants.remove(c); + constants.remove(c); + theModel.nodesWereRemoved(constants, new int[] { index }, new Object[] { c }); + if (graphicEditor != null) + graphicEditor.setModified(); + handler.hasModified(true); + } + + public void a_addLocalBoolean(ModuleNode m, LoadGraphicModelThread.BooleanVariable var) throws PrismException + { + try { + Expression init; + if (var != null) + init = handler.getGUIPlugin().getPrism().parseSingleExpressionString(var.init); + else + init = handler.getGUIPlugin().getPrism().parseSingleExpressionString("false"); + + BoolNode newNode = new BoolNode(var.name, init, true); + m.add(newNode); + int index = m.getIndex(newNode); + theModel.nodesWereInserted(m, new int[] { index }); + varCount++; + if (graphicEditor != null) + graphicEditor.setModified(); + } catch (Exception e) { + throw new PrismException("Local boolean " + var.name + " has an invalid parameter"); + } + handler.hasModified(true); + } + + static int varCount = 1; + + public void a_addLocalBoolean(ModuleNode m) + { + try { + Expression init = handler.getGUIPlugin().getPrism().parseSingleExpressionString("false"); + + BoolNode newNode = new BoolNode("v" + varCount, init, true); + m.add(newNode); + int index = m.getIndex(newNode); + theModel.nodesWereInserted(m, new int[] { index }); + varCount++; + if (graphicEditor != null) + graphicEditor.setModified(); + } catch (Exception e) { + System.err.println("UNEXPECTED ERROR: " + e.getMessage()); + e.printStackTrace(); + //This should never happen + } + handler.hasModified(true); + } + + public void a_addLocalInteger(ModuleNode m, LoadGraphicModelThread.IntegerVariable var) throws PrismException + { + try { + Expression init; + if (var.init == null) + init = handler.getGUIPlugin().getPrism().parseSingleExpressionString("0"); + else + init = handler.getGUIPlugin().getPrism().parseSingleExpressionString(var.init); + Expression min = handler.getGUIPlugin().getPrism().parseSingleExpressionString(var.min); + Expression max = handler.getGUIPlugin().getPrism().parseSingleExpressionString(var.max); + + VarNode newNode = new VarNode(var.name, init, min, max, true); + m.addVariable(newNode); + int index = m.getIndex(newNode); + theModel.nodesWereInserted(m, new int[] { index }); + varCount++; + if (graphicEditor != null) + graphicEditor.setModified(); + } catch (Exception e) { + throw new PrismException("Local integer " + var.name + " has an invalid parameter"); + } + handler.hasModified(true); + } + + public void a_addLocalInteger(ModuleNode m) + { + try { + Expression init = handler.getGUIPlugin().getPrism().parseSingleExpressionString("0"); + Expression min = handler.getGUIPlugin().getPrism().parseSingleExpressionString("0"); + Expression max = handler.getGUIPlugin().getPrism().parseSingleExpressionString("0"); + + VarNode newNode = new VarNode("v" + varCount, init, min, max, true); + m.addVariable(newNode); + int index = m.getIndex(newNode); + theModel.nodesWereInserted(m, new int[] { index }); + varCount++; + if (graphicEditor != null) + graphicEditor.setModified(); + } catch (Exception e) { + System.err.println("UNEXPECTED ERROR: " + e.getMessage()); + e.printStackTrace(); + //This should never happen + } + handler.hasModified(true); + } + + public void a_editExpression(ExpressionNode en) + { + String defa; + if (en.getValue() == null) + defa = "?"; + else + defa = en.getValue().toString(); + String s = JOptionPane.showInputDialog("New Expression:", defa); + if (s == null) + return; + try { + if (s.equals("")) { + en.setValue(null); + } else { + Expression exp = handler.getGUIPlugin().getPrism().parseSingleExpressionString(s); + en.setValue(exp); + } + theModel.nodeChanged(en); + } catch (Exception e) { + handler.getGUIPlugin().error("Syntax error in expression:\n" + s); + } + + handler.hasModified(true); + } + + public void a_setModelType(ModelType type) + { + modelType.setModelType(type); + handler.hasModified(true); + } + + public int getParseSynchState() + { + return parseSynchState; + } + + public void setGraphicModelEditor(GUIGraphicModelEditor graphicEditor) + { + this.graphicEditor = graphicEditor; + } + + public void startParsing() + { + isParsing = true; + if (parseThread != null) + parseThread.interrupt(); + parseThread = new IconThread(0); + parseThread.start(); + } + + public void stopParsing() + { + isParsing = false; + if (parseThread != null) + parseThread.interrupt(); + tree.repaint(); + } + + public void newTree() + { + this.newTree(false); + } + + public void newTree(boolean editable) + { + this.editable = editable; + root.removeAllChildren(); + parseSynchState = TREE_NOT_SYNCHRONIZED; + { + root.setUserObject("Model: " + handler.getShortActiveFileName()); + modelType = new ModelTypeNode("", editable); + root.add(modelType); + if (editable) { + modules = new GUIMultiModelTree.ModuleCollectionNode(); + declarations = new GUIMultiModelTree.DeclarationCollectionNode(); + constants = new GUIMultiModelTree.ConstantCollectionNode(); + root.add(modules); + root.add(declarations); + root.add(constants); + theModel.nodeStructureChanged(root); + } else { + modules = new ModuleCollectionNode(); + declarations = new DeclarationCollectionNode(); + constants = new ConstantCollectionNode(); + theModel.nodeStructureChanged(root); + } + } + editableModules = new ArrayList(); + editableDeclarations = new ArrayList(); + editableConstants = new ArrayList(); + + modCounter = 1; + } + + public void update(ModulesFile parsedModel) + { + parseSynchState = (parsedModel == null) ? TREE_NOT_SYNCHRONIZED : TREE_SYNCHRONIZED_GOOD; + if (editable) + updateEditable(parsedModel); + else + updateUnEditable(parsedModel); + } + + private void updateUnEditable(ModulesFile parsedModel) + { + String fn = handler.getShortActiveFileName(); + if (!root.getUserObject().equals(fn)) { + root.setUserObject("Model: " + fn); + theModel.nodeChanged(root); + } + + if (parsedModel != null) { + String tp = parsedModel.getTypeString(); + if (!modelType.getValue().equals(tp)) { + modelType.setUserObject(tp); + theModel.nodeChanged(modelType); + } + + //MODULES + + //If there is no module tree, but we need to have modules, add the tree + if (root.getIndex(modules) == -1 && parsedModel.getNumModules() > 0) { + root.add(modules); + theModel.nodesWereInserted(root, new int[] { root.getIndex(modules) }); + } + //If there is a module tree, but no modules, remove the module tree + else if (root.getIndex(modules) != -1 && parsedModel.getNumModules() == 0) { + int index = root.getIndex(modules); + root.remove(modules); + theModel.nodesWereRemoved(root, new int[] { index }, new Object[] { modules }); + } + + //Create 2 ArrayLists: one of Modules in the tree and one of modules not in the tree + ArrayList inTree = new ArrayList(); + ArrayList notInTree = new ArrayList(); + + for (int i = 0; i < parsedModel.getNumModules(); i++) { + Module aMod = parsedModel.getModule(i); + if (moduleIsMember(aMod)) + inTree.add(aMod); + else + notInTree.add(aMod); + } + + //make sure modules in the tree are valid + for (int i = 0; i < inTree.size(); i++) { + Module inTreeMod = inTree.get(i); + int treeIndex = getModuleTreeIndexOf(inTreeMod); //should not be -1 + ModuleNode inTreeNode = (ModuleNode) modules.getChildAt(treeIndex); + + /* Check its variables getting variables which are already there + * and putting them in varInTree, and getting variables which + * are not there and putting them in varNotInTree*/ + ArrayList varInTree = new ArrayList(); + ArrayList varNotInTree = new ArrayList(); + + for (int j = 0; j < inTreeMod.getNumDeclarations(); j++) { + Declaration d = inTreeMod.getDeclaration(j); + if (variableIsMember(d, inTreeNode)) + varInTree.add(d); + else + varNotInTree.add(d); + } + + //make sure variables in this module tree are valid + for (int j = 0; j < varInTree.size(); j++) { + Declaration inTreeDec = varInTree.get(j); + int decIndex = getVarTreeIndexOf(inTreeDec, inTreeNode); + DeclarationNode dNode = (DeclarationNode) inTreeNode.getChildAt(decIndex); + if (dNode instanceof VarNode) { + VarNode vNode = (VarNode) dNode; + DeclarationInt dt = (DeclarationInt) inTreeDec.getDeclType(); + vNode.setInitial(parsedModel.getSystemDefn() == null ? inTreeDec.getStartOrDefault() : null); + vNode.setMin(dt.getLow()); + vNode.setMax(dt.getHigh()); + theModel.nodesChanged(vNode, new int[] { 0, 1, 2 }); + } else if (dNode instanceof BoolNode) { + BoolNode bNode = (BoolNode) dNode; + bNode.setInitial(parsedModel.getSystemDefn() == null ? inTreeDec.getStartOrDefault() : null); + theModel.nodesChanged(bNode, new int[] { 0 }); + } + + } + //add variable in varNotInTree to the tree + int[] cIndices = new int[varNotInTree.size()]; + for (int j = 0; j < varNotInTree.size(); j++) { + Declaration notTreeDec = varNotInTree.get(j); + if (notTreeDec.getType() instanceof TypeInt) { + if (notTreeDec.getDeclType() instanceof DeclarationInt) { DeclarationInt declInt = (DeclarationInt) notTreeDec.getDeclType(); - VarNode newVariable = new VarNode(notTreeDec.getName(), parsedModel.getSystemDefn() == null ? notTreeDec.getStartOrDefault() : null, declInt.getLow(), declInt.getHigh(), false); + VarNode newVariable = new VarNode(notTreeDec.getName(), + parsedModel.getSystemDefn() == null ? notTreeDec.getStartOrDefault() : null, declInt.getLow(), declInt.getHigh(), false); inTreeNode.add(newVariable); cIndices[j] = getVarTreeIndexOf(notTreeDec, inTreeNode); - } else { - VarNode newVariable = new VarNode(notTreeDec.getName(), parsedModel.getSystemDefn() == null ? notTreeDec.getStartOrDefault() : null, null, null, false); + } else { + VarNode newVariable = new VarNode(notTreeDec.getName(), + parsedModel.getSystemDefn() == null ? notTreeDec.getStartOrDefault() : null, null, null, false); inTreeNode.add(newVariable); cIndices[j] = getVarTreeIndexOf(notTreeDec, inTreeNode); - } - } - else if(notTreeDec.getType() instanceof TypeBool) - { - BoolNode newVariable = new BoolNode(notTreeDec.getName(), parsedModel.getSystemDefn() == null ? notTreeDec.getStartOrDefault() : null, false); - inTreeNode.add(newVariable); - cIndices[j] = getVarTreeIndexOf(notTreeDec, inTreeNode); - } - else if(notTreeDec.getType() instanceof TypeClock) - { - VarNode newVariable = new VarNode(notTreeDec.getName(), parsedModel.getSystemDefn() == null ? notTreeDec.getStartOrDefault() : null, Expression.Int(0), null, false); - inTreeNode.add(newVariable); - cIndices[j] = getVarTreeIndexOf(notTreeDec, inTreeNode); - } - } - theModel.nodesWereInserted(inTreeNode, cIndices); - - /* remove variables which are in the tree but not in varInTree or - * varNotInTree */ - ArrayList removeNodes = new ArrayList(); - for(int j = 0; j < inTreeNode.getChildCount(); j++) - { - DeclarationNode vNode = (DeclarationNode)inTreeNode.getChildAt(j); - if(!variableExists(vNode, varInTree, varNotInTree)) - { - removeNodes.add(vNode); - } - } - Object[] remObj = new Object[removeNodes.size()]; - int[] remInd = new int[removeNodes.size()]; - for(int j = 0; j < removeNodes.size(); j++) - { - DeclarationNode vNode = (DeclarationNode)removeNodes.get(j); - int index = inTreeNode.getIndex(vNode); - remObj[j] = vNode; - remInd[j] = index; - } - //remove nodes backwards - for(int j =removeNodes.size()-1; j >= 0; j--) - { - inTreeNode.remove(remInd[j]); - } - theModel.nodesWereRemoved(inTreeNode, remInd, remObj); - } - - //add modules which are not in the tree - for(int i = 0; i < notInTree.size(); i++) - { - Module aMod = (Module)notInTree.get(i); - ModuleNode newNode = new ModuleNode(aMod.getName(),false); - //add variables to this - for(int j = 0; j < aMod.getNumDeclarations(); j++) - { - Declaration aDec = aMod.getDeclaration(j); - - if(aDec.getType() instanceof TypeInt) - { - if (aDec.getDeclType() instanceof DeclarationInt) { - DeclarationInt declInt = (DeclarationInt)aDec.getDeclType(); - VarNode newVariable = new VarNode(aDec.getName(), parsedModel.getSystemDefn() == null ? aDec.getStartOrDefault() : null, declInt.getLow(), declInt.getHigh(), false); - newNode.add(newVariable); - } else { - VarNode newVariable = new VarNode(aDec.getName(), parsedModel.getSystemDefn() == null ? aDec.getStartOrDefault() : null, null, null, false); - newNode.add(newVariable); - } - } - else if(aDec.getType() instanceof TypeBool) - { - BoolNode newVariable = new BoolNode(aDec.getName(), parsedModel.getSystemDefn() == null ? aDec.getStartOrDefault() : null, false); - newNode.add(newVariable); - } - if(aDec.getType() instanceof TypeClock) - { - VarNode newVariable = new VarNode(aDec.getName(), parsedModel.getSystemDefn() == null ? aDec.getStartOrDefault() : null, Expression.Int(0), null, false); - newNode.add(newVariable); - } - } - modules.addModule(newNode); - int index = modules.getIndex(newNode); - theModel.nodesWereInserted(modules, new int[] - {index}); - } - //remove modules from the tree which are not in either inTree or notInTree - ArrayList removeNodes = new ArrayList(); - for(int i = 0; i < modules.getChildCount(); i++) - { - ModuleNode mNode = (ModuleNode)modules.getChildAt(i); - if(!moduleExists(mNode, inTree, notInTree)) - { - removeNodes.add(mNode); - } - } - Object[] remObj = new Object[removeNodes.size()]; - int[] remInd = new int[removeNodes.size()]; - for(int i = 0; i < removeNodes.size(); i++) - { - ModuleNode mNode = (ModuleNode)removeNodes.get(i); - int index = modules.getIndex(mNode); - remObj[i] = mNode; - remInd[i] = index; - } - //remove nodes backwards - for(int i =removeNodes.size()-1; i >= 0; i--) - { - modules.remove(remInd[i]); - } - theModel.nodesWereRemoved(modules, remInd, remObj); - - //DECLARATIONS - - //If there is no declaration tree, but we need to have declarations, add the tre - if(root.getIndex(declarations) == -1 && parsedModel.getNumGlobals() > 0) - { - root.add(declarations); - theModel.nodesWereInserted(root, new int[] - {root.getIndex(declarations)}); - } - //If there is a module tree, but no modules, remove the module tree - else if(root.getIndex(declarations) != -1 && parsedModel.getNumGlobals() == 0) - { - int index = root.getIndex(declarations); - root.remove(declarations); - theModel.nodesWereRemoved(root, new int[] - {index}, new Object[] - {declarations}); - } - - /* Create 2 ArrayLists. One of Declarations in the tree and one of declarations - * not in the tree. */ - ArrayList decInTree = new ArrayList(); - ArrayList decNotInTree = new ArrayList(); - - for(int i = 0; i < parsedModel.getNumGlobals(); i++) - { - Declaration d = parsedModel.getGlobal(i); - if(declarationIsMember(d)) decInTree.add(d); - else decNotInTree.add(d); - } - //make sure declarations in this declaration tree are valid - for(int i = 0; i < decInTree.size(); i++) - { - Declaration inTreeDec = (Declaration)decInTree.get(i); - int decIndex = getIndexOfDec(inTreeDec); - DeclarationNode dNode = (DeclarationNode)declarations.getChildAt(decIndex); - if(dNode instanceof GlobalNode) - { - GlobalNode vNode = (GlobalNode)declarations.getChildAt(decIndex); - DeclarationInt declInt = (DeclarationInt)inTreeDec.getDeclType(); - vNode.setInitial(parsedModel.getSystemDefn() == null ? inTreeDec.getStartOrDefault() : null); - vNode.setMin(declInt.getLow()); - vNode.setMax(declInt.getHigh()); - theModel.nodesChanged(vNode, new int [] - {0,1,2}); - } - else if(dNode instanceof BoolNode) - { - BoolNode bNode = (BoolNode)dNode; - bNode.setInitial(parsedModel.getSystemDefn() == null ? inTreeDec.getStartOrDefault() : null); - theModel.nodesChanged(bNode, new int[] - {0}); - } - - } - - //add declarations in decNotInTree to the tree - int[] cIndices = new int[decNotInTree.size()]; - for(int i = 0; i < decNotInTree.size(); i++) - { - Declaration notTreeDec = (Declaration)decNotInTree.get(i); - if(notTreeDec.getType() instanceof TypeInt) - { - DeclarationInt declInt = (DeclarationInt)notTreeDec.getDeclType(); - GlobalNode newVariable = new GlobalNode(notTreeDec.getName(), parsedModel.getSystemDefn() == null ? notTreeDec.getStartOrDefault() : null, declInt.getLow(), declInt.getHigh(), false); - declarations.add(newVariable); - cIndices[i] = getIndexOfDec(notTreeDec); - } - else if(notTreeDec.getType() instanceof TypeBool) - { - BoolNode newVariable = new BoolNode(notTreeDec.getName(), parsedModel.getSystemDefn() == null ? notTreeDec.getStartOrDefault() : null, false); - declarations.add(newVariable); - cIndices[i] = getIndexOfDec(notTreeDec); - } - } - theModel.nodesWereInserted(declarations, cIndices); - - - /* remove declarations which are in the tree but not in decInTree or - * decNotInTree */ - removeNodes = new ArrayList(); - for(int i = 0; i < declarations.getChildCount(); i++) - { - DeclarationNode vNode = (DeclarationNode)declarations.getChildAt(i); - if(!declarationExists(vNode, decInTree, decNotInTree)) - { - removeNodes.add(vNode); - } - } - remObj = new Object[removeNodes.size()]; - remInd = new int[removeNodes.size()]; - for(int i = 0; i < removeNodes.size(); i++) - { - DeclarationNode vNode = (DeclarationNode)removeNodes.get(i); - int index = declarations.getIndex(vNode); - remObj[i] = vNode; - remInd[i] = index; - } - //remove nodes backwards - for(int i =removeNodes.size()-1; i >= 0; i--) - { - declarations.remove(remInd[i]); - } - theModel.nodesWereRemoved(declarations, remInd, remObj); - - - - - - - - //CONSTANTS - - ConstantList csts = parsedModel.getConstantList(); - //If there is no constant tree, but we need to have constant, add the tre - if(root.getIndex(constants) == -1 && csts.size() > 0) - { - root.add(constants); - theModel.nodesWereInserted(root, new int[] - {root.getIndex(constants)}); - } - //If there is a constant tree, but no constants, remove the module tree - else if(root.getIndex(constants) != -1 && csts.size() == 0) - { - int index = root.getIndex(constants); - root.remove(constants); - theModel.nodesWereRemoved(root, new int[] - {index}, new Object[] - {constants}); - } - - /* Create 2 ArrayLists. One of Constants in the tree and one of constants - * not in the tree. */ - ArrayList conInTree = new ArrayList(); - ArrayList conNotInTree = new ArrayList(); - - for(int i = 0; i < csts.size(); i++) - { - String name = csts.getConstantName(i); - Expression expr = csts.getConstant(i); - Type type = csts.getConstantType(i); - ConstantNode cn; - if (type instanceof TypeBool) { - cn = new BoolConstantNode(name, expr, false); - } else if (type instanceof TypeDouble) { - cn = new DoubleConstantNode(name, expr, false); - } else { - cn = new IntegerConstantNode(name, expr, false); - } - if(constantIsMember(cn)) conInTree.add(cn); - else conNotInTree.add(cn); - } - - //make sure constants in this declaration tree are valid - for(int i = 0; i < conInTree.size(); i++) - { - ConstantNode inTreeCon = (ConstantNode)conInTree.get(i); - int conIndex = getIndexOfCon(inTreeCon); - ConstantNode cNode = (ConstantNode)constants.getChildAt(conIndex); - if(cNode instanceof IntegerConstantNode) - { - IntegerConstantNode iNode = (IntegerConstantNode)cNode; - - iNode.setName(inTreeCon.getName()); - iNode.setValue(inTreeCon.getValue()); - theModel.nodesChanged(iNode, new int [] - {0}); - } - else if(cNode instanceof BoolConstantNode) - { - BoolConstantNode bNode = (BoolConstantNode)cNode; - - bNode.setName(inTreeCon.getName()); - bNode.setValue(inTreeCon.getValue()); - theModel.nodesChanged(bNode, new int [] - {0}); - } - else if(cNode instanceof DoubleConstantNode) - { - DoubleConstantNode dNode = (DoubleConstantNode)cNode; - - dNode.setName(inTreeCon.getName()); - dNode.setValue(inTreeCon.getValue()); - theModel.nodesChanged(dNode, new int [] - {0}); - } - - } - - //add declarations in decNotInTree to the tree - cIndices = new int[conNotInTree.size()]; - for(int i = 0; i < conNotInTree.size(); i++) - { - ConstantNode notTreeCon = (ConstantNode)conNotInTree.get(i); - constants.add(notTreeCon); - cIndices[i] = getIndexOfCon(notTreeCon); - } - theModel.nodesWereInserted(constants, cIndices); - - - /* remove declarations which are in the tree but not in decInTree or - * decNotInTree */ - removeNodes = new ArrayList(); - for(int i = 0; i < constants.getChildCount(); i++) - { - ConstantNode cNode = (ConstantNode)constants.getChildAt(i); - if(!constantExists(cNode, conInTree, conNotInTree)) - { - removeNodes.add(cNode); - } - } - remObj = new Object[removeNodes.size()]; - remInd = new int[removeNodes.size()]; - for(int i = 0; i < removeNodes.size(); i++) - { - ConstantNode vNode = (ConstantNode)removeNodes.get(i); - int index = constants.getIndex(vNode); - remObj[i] = vNode; - remInd[i] = index; - } - //remove nodes backwards - for(int i =removeNodes.size()-1; i >= 0; i--) - { - constants.remove(remInd[i]); - } - theModel.nodesWereRemoved(constants, remInd, remObj); - - } - else - { - String tp = ""; - if(!modelType.getValue().equals(tp)) - { - modelType.setUserObject(tp); - theModel.nodeChanged(modelType); - } - } - - if(tree !=null) tree.repaint(); - } - - public boolean moduleExists(ModuleNode mNode, ArrayList inTree, ArrayList outTree) - { - for(int i = 0; i < inTree.size(); i++) - { - Module m = (Module)inTree.get(i); - if(mNode.getName().equals(m.getName())) - { - return true; - } - } - for(int i = 0; i < outTree.size(); i++) - { - Module m = (Module)outTree.get(i); - if(mNode.getName().equals(m.getName())) - { - return true; - } - } - return false; - } - public boolean variableExists(DeclarationNode vNode, ArrayList inTree, ArrayList outTree) - { - for(int i = 0; i < inTree.size(); i++) - { - Declaration d = (Declaration)inTree.get(i); - if(vNode.getName().equals(d.getName())) - { - return true; - } - } - for(int i = 0; i < outTree.size(); i++) - { - Declaration d = (Declaration)outTree.get(i); - if(vNode.getName().equals(d.getName())) - { - return true; - } - } - return false; - } - - public boolean declarationExists(DeclarationNode vNode, ArrayList inTree, ArrayList outTree) - { - for(int i = 0; i < inTree.size(); i++) - { - Declaration d = (Declaration)inTree.get(i); - if(vNode.getName().equals(d.getName())) - { - return true; - } - } - for(int i = 0; i < outTree.size(); i++) - { - Declaration d = (Declaration)outTree.get(i); - if(vNode.getName().equals(d.getName())) - { - return true; - } - } - return false; - } - - public boolean constantExists(ConstantNode cNode, ArrayList inTree, ArrayList outTree) - { - for(int i = 0; i < inTree.size(); i++) - { - ConstantNode c = (ConstantNode)inTree.get(i); - if(c.equals(cNode)) return true; - } - - for(int i = 0; i < outTree.size(); i++) - { - ConstantNode c = (ConstantNode)outTree.get(i); - if(c.equals(cNode)) return true; - } - return false; - } - - - public boolean moduleIsMember(Module aMod) - { - boolean member = false; - for(int i = 0; i < modules.getChildCount(); i++) - { - ModuleNode node = (ModuleNode)modules.getChildAt(i); - if(node.getName().equals(aMod.getName())) - { - member = true; - break; - } - } - return member; - } - - public boolean declarationIsMember(Declaration d) - { - boolean member = false; - for(int i = 0; i < declarations.getChildCount(); i++) - { - DeclarationNode dec = (DeclarationNode)declarations.getChildAt(i); - if(dec.getName().equals(d.getName())) //check same name - { - if(dec instanceof GlobalBoolNode && d.getType() instanceof TypeBool) //check type equality - { - member = true; - break; - } - if(dec instanceof GlobalNode && d.getType() instanceof TypeInt) - { - member = true; - break; - } - } - } - return member; - } - - public boolean constantIsMember(ConstantNode n) - { - boolean member = false; - for(int i = 0; i < constants.getChildCount(); i++) - { - ConstantNode inC = (ConstantNode)constants.getChildAt(i); - if(inC.equals(n)) - { - member = true; - break; - } - } - return member; - } - - public boolean variableIsMember(Declaration d, ModuleNode node) - { - boolean member = false; - for(int i = 0; i < node.getChildCount(); i++) - { - DeclarationNode dec = (DeclarationNode)node.getChildAt(i); - if(dec.getName().equals(d.getName())) //check same name - { - if(dec instanceof BoolNode && d.getType() instanceof TypeBool) //check type equality - { - member = true; - break; - } - if(dec instanceof VarNode && d.getType() instanceof TypeInt) - { - member = true; - break; - } - } - } - return member; - } - - public int getVarTreeIndexOf(Declaration d, ModuleNode node) - { - int member = -1; - for(int i = 0; i < node.getChildCount(); i++) - { - DeclarationNode vNode = (DeclarationNode)node.getChildAt(i); - if(vNode.getName().equals(d.getName())) - { - member = i; - break; - } - } - return member; - } - - public int getModuleTreeIndexOf(Module aMod) - { - int member = -1; - for(int i = 0; i < modules.getChildCount(); i++) - { - ModuleNode node = (ModuleNode)modules.getChildAt(i); - if(node.getName().equals(aMod.getName())) - { - member = i; - break; - } - } - return member; - } - - public int getIndexOfDec(Declaration d) - { - int member = -1; - for(int i = 0; i < declarations.getChildCount(); i++) - { - DeclarationNode dec = (DeclarationNode)declarations.getChildAt(i); - if(dec.getName().equals(d.getName())) - { - member = i; - break; - } - } - return member; - } - - public int getIndexOfCon(ConstantNode cn) - { - int member = -1; - - for(int i = 0; i < constants.getChildCount(); i++) - { - ConstantNode cc = (ConstantNode)constants.getChildAt(i); - if(cc.equals(cn)) - { - member = i; - break; - } - } - return member; - } - - private void updateEditable(ModulesFile parsedModel) - { - String fn = handler.getShortActiveFileName(); - if(!root.getUserObject().equals(fn)) - { - root.setUserObject("Model: " + fn); - theModel.nodeChanged(root); - } - - if(parsedModel != null) - { - if(!modelType.getValue().equals(parsedModel.getType().toString())) - { - modelType.setModelType(parsedModel.getModelType()); - } - - //MODULES - - //If there is no module tree, but we need to have modules, add the tre - if(root.getIndex(modules) == -1 && parsedModel.getNumModules() > 0) - { - root.add(modules); - theModel.nodesWereInserted(root, new int[] - {root.getIndex(modules)}); - } - - - /* Create 2 ArrayLists. One of Modules in the tree and one of modules - * not in the tree. */ - ArrayList inTree = new ArrayList(); - ArrayList notInTree = new ArrayList(); - - for(int i = 0; i < parsedModel.getNumModules(); i++) - { - Module aMod = parsedModel.getModule(i); - if(moduleIsMember(aMod)) inTree.add(aMod); - else notInTree.add(aMod); - } - - //make sure modules in the tree are valid - for(int i = 0; i < inTree.size(); i++) - { - Module inTreeMod = (Module)inTree.get(i); - int treeIndex = getModuleTreeIndexOf(inTreeMod); //should not be -1 - ModuleNode inTreeNode = (ModuleNode)modules.getChildAt(treeIndex); - - /* Check its variables getting variables which are already there - * and putting them in varInTree, and getting variables which - * are not there and putting them in varNotInTree*/ - ArrayList varInTree = new ArrayList(); - ArrayList varNotInTree = new ArrayList(); - - for(int j = 0; j < inTreeMod.getNumDeclarations(); j++) - { - Declaration d = inTreeMod.getDeclaration(j); - if(variableIsMember(d, inTreeNode)) varInTree.add(d); - else varNotInTree.add(d); - } - - //make sure variables in this module tree are valid - for(int j = 0; j < varInTree.size(); j++) - { - Declaration inTreeDec = (Declaration)varInTree.get(j); - int decIndex = getVarTreeIndexOf(inTreeDec, inTreeNode); - DeclarationNode dNode = (DeclarationNode)inTreeNode.getChildAt(decIndex); - if(dNode instanceof VarNode) - { - VarNode vNode = (VarNode)dNode; - DeclarationInt declInt = (DeclarationInt)inTreeDec.getDeclType(); - vNode.setInitial(parsedModel.getSystemDefn() == null ? inTreeDec.getStartOrDefault() : null); - vNode.setMin(declInt.getLow()); - vNode.setMax(declInt.getHigh()); - theModel.nodesChanged(vNode, new int [] - {0,1,2}); - } - else if(dNode instanceof BoolNode) - { - BoolNode bNode = (BoolNode)dNode; - bNode.setInitial(parsedModel.getSystemDefn() == null ? inTreeDec.getStartOrDefault() : null); - theModel.nodesChanged(bNode, new int[] - {0}); - } - - } - //add variable in varNotInTree to the tree - int[] cIndices = new int[varNotInTree.size()]; - for(int j = 0; j < varNotInTree.size(); j++) - { - Declaration notTreeDec = (Declaration)varNotInTree.get(j); - if(notTreeDec.getType() instanceof TypeInt) - { - DeclarationInt declInt = (DeclarationInt)notTreeDec.getDeclType(); - VarNode newVariable = new VarNode(notTreeDec.getName(), parsedModel.getSystemDefn() == null ? notTreeDec.getStartOrDefault() : null, declInt.getLow(), declInt.getHigh(), false); - inTreeNode.add(newVariable); - cIndices[j] = getVarTreeIndexOf(notTreeDec, inTreeNode); - } - else if(notTreeDec.getType() instanceof TypeBool) - { - BoolNode newVariable = new BoolNode(notTreeDec.getName(), parsedModel.getSystemDefn() == null ? notTreeDec.getStartOrDefault() : null, false); - inTreeNode.add(newVariable); - cIndices[j] = getVarTreeIndexOf(notTreeDec, inTreeNode); - } - } - theModel.nodesWereInserted(inTreeNode, cIndices); - - /* remove variables which are in the tree but not in varInTree or - * varNotInTree */ - ArrayList removeNodes = new ArrayList(); - for(int j = 0; j < inTreeNode.getChildCount(); j++) - { - DeclarationNode vNode = (DeclarationNode)inTreeNode.getChildAt(j); - if(!variableExists(vNode, varInTree, varNotInTree)) - { - removeNodes.add(vNode); - } - } - Object[] remObj = new Object[removeNodes.size()]; - int[] remInd = new int[removeNodes.size()]; - for(int j = 0; j < removeNodes.size(); j++) - { - DeclarationNode vNode = (DeclarationNode)removeNodes.get(j); - int index = inTreeNode.getIndex(vNode); - remObj[j] = vNode; - remInd[j] = index; - } - //remove nodes backwards - for(int j =removeNodes.size()-1; j >= 0; j--) - { - inTreeNode.remove(remInd[j]); - } - theModel.nodesWereRemoved(inTreeNode, remInd, remObj); - } - - //add modules which are not in the tree - for(int i = 0; i < notInTree.size(); i++) - { - Module aMod = (Module)notInTree.get(i); - ModuleNode newNode = new ModuleNode(aMod.getName(),false); - //add variables to this - for(int j = 0; j < aMod.getNumDeclarations(); j++) - { - Declaration aDec = aMod.getDeclaration(j); - - if(aDec.getType() instanceof TypeInt) - { - DeclarationInt declInt = (DeclarationInt)aDec.getDeclType(); - VarNode newVariable = new VarNode(aDec.getName(), parsedModel.getSystemDefn() == null ? aDec.getStartOrDefault() : null, declInt.getLow(), declInt.getHigh(), false); - newNode.add(newVariable); - } - else if(aDec.getType() instanceof TypeBool) - { - BoolNode newVariable = new BoolNode(aDec.getName(), parsedModel.getSystemDefn() == null ? aDec.getStartOrDefault() : null, false); - newNode.add(newVariable); - } - } - modules.addModule(newNode); - int index = modules.getIndex(newNode); - theModel.nodesWereInserted(modules, new int[] - {index}); - } - //remove modules from the tree which are not in either inTree or notInTree - ArrayList removeNodes = new ArrayList(); - for(int i = 0; i < modules.getChildCount(); i++) - { - ModuleNode mNode = (ModuleNode)modules.getChildAt(i); - if(!mNode.isEditable() && !moduleExists(mNode, inTree, notInTree)) - { - removeNodes.add(mNode); - } - } - Object[] remObj = new Object[removeNodes.size()]; - int[] remInd = new int[removeNodes.size()]; - for(int i = 0; i < removeNodes.size(); i++) - { - ModuleNode mNode = (ModuleNode)removeNodes.get(i); - int index = modules.getIndex(mNode); - remObj[i] = mNode; - remInd[i] = index; - } - //remove nodes backwards - for(int i =removeNodes.size()-1; i >= 0; i--) - { - modules.remove(remInd[i]); - } - theModel.nodesWereRemoved(modules, remInd, remObj); - - //DECLARATIONS - - //If there is no declaration tree, but we need to have declarations, add the tre - if(root.getIndex(declarations) == -1 && parsedModel.getNumGlobals() > 0) - { - root.add(declarations); - theModel.nodesWereInserted(root, new int[] - {root.getIndex(declarations)}); - } - - /* Create 2 ArrayLists. One of Declarations in the tree and one of declarations - * not in the tree. */ - ArrayList decInTree = new ArrayList(); - ArrayList decNotInTree = new ArrayList(); - - for(int i = 0; i < parsedModel.getNumGlobals(); i++) - { - Declaration d = parsedModel.getGlobal(i); - if(declarationIsMember(d)) decInTree.add(d); - else decNotInTree.add(d); - } - - //make sure declarations in this declaration tree are valid - for(int i = 0; i < decInTree.size(); i++) - { - Declaration inTreeDec = (Declaration)decInTree.get(i); - int decIndex = getIndexOfDec(inTreeDec); - DeclarationNode dNode = (DeclarationNode)declarations.getChildAt(decIndex); - if(dNode instanceof GlobalNode) - { - GlobalNode vNode = (GlobalNode)declarations.getChildAt(decIndex); - DeclarationInt declInt = (DeclarationInt)inTreeDec.getDeclType(); - vNode.setInitial(parsedModel.getSystemDefn() == null ? inTreeDec.getStartOrDefault() : null); - vNode.setMin(declInt.getLow()); - vNode.setMax(declInt.getHigh()); - theModel.nodesChanged(vNode, new int [] - {0,1,2}); - } - else if(dNode instanceof GlobalBoolNode) - { - GlobalBoolNode bNode = (GlobalBoolNode)dNode; - bNode.setInitial(parsedModel.getSystemDefn() == null ? inTreeDec.getStartOrDefault() : null); - theModel.nodesChanged(bNode, new int[] - {0}); - } - - } - - //add declarations in decNotInTree to the tree - int[] cIndices = new int[decNotInTree.size()]; - for(int i = 0; i < decNotInTree.size(); i++) - { - Declaration notTreeDec = (Declaration)decNotInTree.get(i); - if(notTreeDec.getType() instanceof TypeInt) - { - DeclarationInt declInt = (DeclarationInt)notTreeDec.getDeclType(); - GlobalNode newVariable = new GlobalNode(notTreeDec.getName(), parsedModel.getSystemDefn() == null ? notTreeDec.getStartOrDefault() : null, declInt.getLow(), declInt.getHigh(), false); - declarations.add(newVariable); - cIndices[i] = getIndexOfDec(notTreeDec); - } - else if(notTreeDec.getType() instanceof TypeBool) - { - GlobalBoolNode newVariable = new GlobalBoolNode(notTreeDec.getName(), parsedModel.getSystemDefn() == null ? notTreeDec.getStartOrDefault() : null, false); - declarations.add(newVariable); - cIndices[i] = getIndexOfDec(notTreeDec); - } - } - theModel.nodesWereInserted(declarations, cIndices); - - - /* remove declarations which are in the tree but not in decInTree or - * decNotInTree */ - removeNodes = new ArrayList(); - for(int i = 0; i < declarations.getChildCount(); i++) - { - DeclarationNode vNode = (DeclarationNode)declarations.getChildAt(i); - if(!vNode.isEditable() && !declarationExists(vNode, decInTree, decNotInTree)) - { - removeNodes.add(vNode); - } - } - remObj = new Object[removeNodes.size()]; - remInd = new int[removeNodes.size()]; - for(int i = 0; i < removeNodes.size(); i++) - { - DeclarationNode vNode = (DeclarationNode)removeNodes.get(i); - int index = declarations.getIndex(vNode); - remObj[i] = vNode; - remInd[i] = index; - } - //remove nodes backwards - for(int i =removeNodes.size()-1; i >= 0; i--) - { - declarations.remove(remInd[i]); - } - theModel.nodesWereRemoved(declarations, remInd, remObj); - - - - - - - - //CONSTANTS - - ConstantList csts = parsedModel.getConstantList(); - //If there is no constant tree, but we need to have constant, add the tre - if(root.getIndex(constants) == -1 && csts.size() > 0) - { - root.add(constants); - theModel.nodesWereInserted(root, new int[] - {root.getIndex(constants)}); - } - - /* Create 2 ArrayLists. One of Constants in the tree and one of constants - * not in the tree. */ - ArrayList conInTree = new ArrayList(); - ArrayList conNotInTree = new ArrayList(); - - for(int i = 0; i < csts.size(); i++) - { - String name = csts.getConstantName(i); - Expression expr = csts.getConstant(i); - Type type = csts.getConstantType(i); - ConstantNode cn; - if (type instanceof TypeBool) { - cn = new BoolConstantNode(name, expr, false); - } else if (type instanceof TypeDouble) { - cn = new DoubleConstantNode(name, expr, false); - } else { - cn = new IntegerConstantNode(name, expr, false); - } - if(constantIsMember(cn)) conInTree.add(cn); - else conNotInTree.add(cn); - } - - //make sure constants in this declaration tree are valid - for(int i = 0; i < conInTree.size(); i++) - { - ConstantNode inTreeCon = (ConstantNode)conInTree.get(i); - int conIndex = getIndexOfCon(inTreeCon); - ConstantNode cNode = (ConstantNode)constants.getChildAt(conIndex); - if(cNode instanceof IntegerConstantNode) - { - IntegerConstantNode iNode = (IntegerConstantNode)cNode; - - iNode.setName(inTreeCon.getName()); - iNode.setValue(inTreeCon.getValue()); - theModel.nodesChanged(iNode, new int [] - {0}); - } - else if(cNode instanceof BoolConstantNode) - { - BoolConstantNode bNode = (BoolConstantNode)cNode; - - bNode.setName(inTreeCon.getName()); - bNode.setValue(inTreeCon.getValue()); - theModel.nodesChanged(bNode, new int [] - {0}); - } - else if(cNode instanceof DoubleConstantNode) - { - DoubleConstantNode dNode = (DoubleConstantNode)cNode; - - dNode.setName(inTreeCon.getName()); - dNode.setValue(inTreeCon.getValue()); - theModel.nodesChanged(dNode, new int [] - {0}); - } - - } - - //add declarations in decNotInTree to the tree - cIndices = new int[conNotInTree.size()]; - for(int i = 0; i < conNotInTree.size(); i++) - { - ConstantNode notTreeCon = (ConstantNode)conNotInTree.get(i); - constants.add(notTreeCon); - cIndices[i] = getIndexOfCon(notTreeCon); - } - theModel.nodesWereInserted(constants, cIndices); - - - /* remove declarations which are in the tree but not in decInTree or - * decNotInTree */ - removeNodes = new ArrayList(); - for(int i = 0; i < constants.getChildCount(); i++) - { - ConstantNode cNode = (ConstantNode)constants.getChildAt(i); - if(!cNode.isEditable() && !constantExists(cNode, conInTree, conNotInTree)) - { - removeNodes.add(cNode); - } - } - remObj = new Object[removeNodes.size()]; - remInd = new int[removeNodes.size()]; - for(int i = 0; i < removeNodes.size(); i++) - { - ConstantNode vNode = (ConstantNode)removeNodes.get(i); - int index = constants.getIndex(vNode); - remObj[i] = vNode; - remInd[i] = index; - } - //remove nodes backwards - for(int i =removeNodes.size()-1; i >= 0; i--) - { - constants.remove(remInd[i]); - } - theModel.nodesWereRemoved(constants, remInd, remObj); - - } - else - { - /*String tp = ""; - if(!modelType.getValue().equals(tp)) - { - modelType.setUserObject(tp); - theModel.nodeChanged(modelType); - }*/ - } - - if(tree != null) tree.repaint(); - } - - public void lastParseFailed() - { - parseSynchState = TREE_SYNCHRONIZED_BAD; - tree.repaint(); - } - - public void makeNotUpToDate() - { - parseSynchState = TREE_NOT_SYNCHRONIZED; - tree.repaint(); - } - - private void initComponents() - { - tree = new JTree(theModel) - { - public String getToolTipText(MouseEvent event) - { - String ret = null; - TreePath selectedPath = tree.getPathForLocation(event.getX(), event.getY()); - if(selectedPath != null) - { - //if(selectedPath.getLastPathComponent() instanceof ModelRootNode) - if(parseSynchState == TREE_SYNCHRONIZED_BAD) return handler.getParseErrorMessage(); - else if(parseSynchState == TREE_SYNCHRONIZED_GOOD) return "Model parsed successfully"; - else return "Model not parsed"; - } - - return ret; - } - - public boolean isPathEditable(TreePath path) - { - Object c = path.getLastPathComponent(); - if(c instanceof ValueNode) - { - ValueNode v = (ValueNode)c; - return v.isEditable(); - } - return false; - } - - }; - PrismNodeRenderer prnr = new PrismNodeRenderer(); - tree.setCellRenderer(prnr); - /*JComboBox typeCombo = new JComboBox(new Object[] - {"Probabilistic", "Non-deterministic", "Stochastic"}); - typeCombo.setFont(tree.getFont()); - typeCombo.setBackground(tree.getBackground()); - ValueNodeCellEditor cellEdit = new ValueNodeCellEditor(new JTextField(), typeCombo); - tree.setCellEditor(new DefaultTreeCellEditor(tree, prnr, cellEdit));*/ - tree.setEditable(true); - tree.setCellEditor(new GUIMultiModelTree.ModelTreeCellEditor(tree, prnr)); - - setLayout(new BorderLayout()); - JScrollPane scr = new JScrollPane(); - scr.setViewportView(tree); - add(scr, BorderLayout.CENTER); - - moduleCollectionPopup = new JPopupMenu(); - addModule = new AbstractAction() - { - public void actionPerformed(ActionEvent e) - { - a_addModule(); - } - }; - addModule.putValue(Action.LONG_DESCRIPTION, "Adds an editable module to the tree"); - addModule.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_A)); - addModule.putValue(Action.NAME, "Add Module"); - moduleCollectionPopup.add(addModule); - - declarationCollectionPopup = new JPopupMenu(); - addIntegerGlobal = new AbstractAction() - { - public void actionPerformed(ActionEvent e) - { - a_addIntegerGlobal(); - } - }; - addIntegerGlobal.putValue(Action.NAME, "Add Global Integer"); - addBooleanGlobal = new AbstractAction() - { - public void actionPerformed(ActionEvent e) - { - a_addBooleanGlobal(); - } - }; - addBooleanGlobal.putValue(Action.NAME, "Add Global Boolean"); - declarationCollectionPopup.add(addIntegerGlobal); - declarationCollectionPopup.add(addBooleanGlobal); - - constantsCollectionPopup = new JPopupMenu(); - addIntegerConstant = new AbstractAction() - { - public void actionPerformed(ActionEvent e) - { - a_addIntegerConstant(); - } - }; - addIntegerConstant.putValue(Action.NAME, "Add Integer Constant"); - addBooleanConstant = new AbstractAction() - { - public void actionPerformed(ActionEvent e) - { - a_addBooleanConstant(); - } - }; - addBooleanConstant.putValue(Action.NAME, "Add Boolean Constant"); - addDoubleConstant = new AbstractAction() - { - public void actionPerformed(ActionEvent e) - { - a_addDoubleConstant(); - } - }; - addDoubleConstant.putValue(Action.NAME, "Add Double Constant"); - constantsCollectionPopup.add(addIntegerConstant); - constantsCollectionPopup.add(addBooleanConstant); - constantsCollectionPopup.add(addDoubleConstant); - - modulePopup = new JPopupMenu(); - removeModule = new AbstractAction() - { - public void actionPerformed(ActionEvent e) - { - if(lastPopNode != null && lastPopNode instanceof ModuleNode) - { - a_removeModule((ModuleNode)lastPopNode); - lastPopNode = null; - } - } - }; - removeModule.putValue(Action.NAME, "Remove"); - addBoolean = new AbstractAction() - { - public void actionPerformed(ActionEvent e) - { - if(lastPopNode != null && lastPopNode instanceof ModuleNode) - { - a_addLocalBoolean((ModuleNode)lastPopNode); - lastPopNode = null; - } - - } - }; - addBoolean.putValue(Action.NAME, "Add Boolean Variable"); - addInteger = new AbstractAction() - { - public void actionPerformed(ActionEvent e) - { - if(lastPopNode != null && lastPopNode instanceof ModuleNode) - { - a_addLocalInteger((ModuleNode)lastPopNode); - lastPopNode = null; - } - } - }; - addInteger.putValue(Action.NAME, "Add Integer Variable"); - renameModule = new AbstractAction() - { - public void actionPerformed(ActionEvent e) - { - if(lastPopNode != null && lastPopNode instanceof ModuleNode) - { - a_renameModule((ModuleNode)lastPopNode); - lastPopNode = null; - } - } - }; - renameModule.putValue(Action.NAME, "Rename"); - modulePopup.add(renameModule); - modulePopup.add(removeModule); - //modulePopup.add(new JSplitter()); - modulePopup.add(addInteger); - modulePopup.add(addBoolean); - - declarationPopup = new JPopupMenu(); - removeDeclaration = new AbstractAction() - { - public void actionPerformed(ActionEvent e) - { - if(lastPopNode != null) - { - if(lastPopNode instanceof BoolNode || lastPopNode instanceof VarNode) - { - ModuleNode m = whichModule((DeclarationNode)lastPopNode); - if(m != null) a_removeVariable((DeclarationNode)lastPopNode, m); - } - else if(lastPopNode instanceof GlobalNode || lastPopNode instanceof GlobalBoolNode) - { - a_removeGlobal((DeclarationNode)lastPopNode); - } - else if(lastPopNode instanceof ConstantNode) - { - a_removeConstant((ConstantNode)lastPopNode); - } - } - } - }; - removeDeclaration.putValue(Action.NAME, "Remove"); - declarationPopup.add(removeDeclaration); - - renameDeclaration = new AbstractAction() - { - public void actionPerformed(ActionEvent e) - { - if(lastPopNode != null) - { - a_renameDeclaration((DeclarationNode)lastPopNode); - } - } - }; - renameDeclaration.putValue(Action.NAME, "Rename"); - declarationPopup.add(renameDeclaration); - - expressionPopup = new JPopupMenu(); - - editExpression = new AbstractAction() - { - public void actionPerformed(ActionEvent e) - { - if(lastPopNode !=null) - { - a_editExpression((ExpressionNode)lastPopNode); - } - } - }; - editExpression.putValue(Action.NAME, "Edit"); - expressionPopup.add(editExpression); - - - modelTypePopup = new JPopupMenu(); - - non = new JRadioButton("Non-deterministic (mdp)"); - pro = new JRadioButton("Probabilistic (dtmc)"); - sto = new JRadioButton("Stochastic (ctmc)"); - - ButtonGroup gro = new ButtonGroup(); - gro.add(non); - gro.add(pro); - gro.add(sto); - - non.setSelected(true); - - modelTypePopup.add(non); - modelTypePopup.add(pro); - modelTypePopup.add(sto); - - non.addActionListener(new ActionListener() - { - public void actionPerformed(ActionEvent e) - { - if(non.isSelected())a_setModelType(ModelType.MDP); - modelTypePopup.setVisible(false); - } - }); - - pro.addActionListener(new ActionListener() - { - public void actionPerformed(ActionEvent e) - { - if(pro.isSelected())a_setModelType(ModelType.DTMC); - modelTypePopup.setVisible(false); - } - }); - - sto.addActionListener(new ActionListener() - { - public void actionPerformed(ActionEvent e) - { - if(sto.isSelected())a_setModelType(ModelType.CTMC); - modelTypePopup.setVisible(false); - } - }); - } - - public ModuleNode whichModule(DeclarationNode isIt) - { - for(int i = 0; i < editableModules.size(); i++) - { - ModuleNode mod = (ModuleNode)editableModules.get(i); - int index = mod.getIndex(isIt); - if(index > -1) - { - return mod; - } - } - return null; - } - - - public void mouseClicked(MouseEvent e) - { - } - - public void mouseEntered(MouseEvent e) - { - } - - public void mouseExited(MouseEvent e) - { - } - - public void mousePressed(MouseEvent e) - { - if(e.isPopupTrigger()) - { - lastPopNode = null; - //root popup - if(tree.getClosestPathForLocation(e.getX(), e.getY()).equals(new TreePath(root.getPath()))) - { - tree.setSelectionPath(new TreePath(root.getPath())); - //now the root is selected, show the popup - //(diabled for now) - //((GUIMultiModel)(handler.getGUIPlugin())).getPopup().show(tree, e.getX(), e.getY()); - } - //model type node - if(editable && tree.getClosestPathForLocation(e.getX(), e.getY()).equals(new TreePath(modelType.getPath()))) - { - tree.setSelectionPath(new TreePath(modelType.getPath())); - modelTypePopup.show(tree,e.getX(), e.getY()); - } - //module collection popup - else if(editable && modules != null && tree.getClosestPathForLocation(e.getX(), e.getY()).equals(new TreePath(modules.getPath()))) - { - tree.setSelectionPath(new TreePath(modules.getPath())); - moduleCollectionPopup.show(tree,e.getX(),e.getY()); - } - //declaration collection popup - else if(editable && declarations != null && tree.getClosestPathForLocation(e.getX(), e.getY()).equals(new TreePath(declarations.getPath()))) - { - tree.setSelectionPath(new TreePath(declarations.getPath())); - declarationCollectionPopup.show(tree,e.getX(),e.getY()); - } - else if(editable && constants != null && tree.getClosestPathForLocation(e.getX(), e.getY()).equals(new TreePath(constants.getPath())))//constant collection node - { - tree.setSelectionPath(new TreePath(constants.getPath())); - constantsCollectionPopup.show(tree,e.getX(), e.getY()); - } - else // is the path on a ModuleNode or a DeclarationNode or an ExpressionNode - { - TreePath selectedPath = tree.getClosestPathForLocation(e.getX(), e.getY()); - for(int i = 0; i < editableModules.size(); i++) //search each module - { - ModuleNode mn = (ModuleNode)editableModules.get(i); - if(new TreePath(mn.getPath()).equals(selectedPath)) - { - tree.setSelectionPath(selectedPath); - if(mn.isEditable()) - { - modulePopup.show(tree, e.getX(), e.getY()); - lastPopNode = mn; - - if(graphicEditor != null)graphicEditor.switchModuleView(mn); - } - return; - } - for(int j = 0; j < mn.getChildCount(); j++)//search local variables - { - DeclarationNode dn = (DeclarationNode)mn.getChildAt(j); - if(new TreePath(dn.getPath()).equals(selectedPath)) - { - tree.setSelectionPath(selectedPath); - if(dn.isEditable()) - { - declarationPopup.show(tree, e.getX(), e.getY()); - lastPopNode = dn; - } - return; - } - } - } - for(int i = 0; i < editableDeclarations.size(); i++)//search globals - { - DeclarationNode dn = (DeclarationNode)editableDeclarations.get(i); - if(new TreePath(dn.getPath()).equals(selectedPath)) - { - tree.setSelectionPath(selectedPath); - if(dn.isEditable()) - { - declarationPopup.show(tree, e.getX(), e.getY()); - lastPopNode = dn; - } - return; - } - } - for(int i = 0; i < editableConstants.size(); i++)//search constants - { - DeclarationNode dn = (DeclarationNode)editableConstants.get(i); - if(new TreePath(dn.getPath()).equals(selectedPath)) - { - tree.setSelectionPath(selectedPath); - if(dn.isEditable()) - { - declarationPopup.show(tree, e.getX(), e.getY()); - lastPopNode = dn; - } - return; - } - } - - //Could be an ExpressionNode - if(tree.getSelectionPath() != null) - { - TreeNode selectedNode = (TreeNode)tree.getSelectionPath().getLastPathComponent(); - if(selectedNode instanceof ExpressionNode) - { - ExpressionNode en = (ExpressionNode)selectedNode; - if(en.isEditable()) - { - expressionPopup.show(tree, e.getX(), e.getY()); - lastPopNode = en; - } - } - } - - } - - } - else - { - TreePath selectedPath = tree.getClosestPathForLocation(e.getX(), e.getY()); - for(int i = 0; i < editableModules.size(); i++) //search each module - { - ModuleNode mn = (ModuleNode)editableModules.get(i); - if(new TreePath(mn.getPath()).equals(selectedPath)) - { - tree.setSelectionPath(selectedPath); - if(graphicEditor != null)graphicEditor.switchModuleView(mn); - return; - } - } - } - - } - - public void mouseReleased(MouseEvent e) - { - if(e.isPopupTrigger()) - { - lastPopNode = null; - //root popup - if(tree.getClosestPathForLocation(e.getX(), e.getY()).equals(new TreePath(root.getPath()))) - { - tree.setSelectionPath(new TreePath(root.getPath())); - //now the root is selected, show the popup - //(diabled for now) - //((GUIMultiModel)(handler.getGUIPlugin())).getPopup().show(tree, e.getX(), e.getY()); - } - //model type node - if(editable && tree.getClosestPathForLocation(e.getX(), e.getY()).equals(new TreePath(modelType.getPath()))) - { - tree.setSelectionPath(new TreePath(modelType.getPath())); - modelTypePopup.show(tree,e.getX(), e.getY()); - } - //module collection popup - else if(editable && modules != null && tree.getClosestPathForLocation(e.getX(), e.getY()).equals(new TreePath(modules.getPath()))) - { - tree.setSelectionPath(new TreePath(modules.getPath())); - moduleCollectionPopup.show(tree,e.getX(),e.getY()); - } - //declaration collection popup - else if(editable && declarations != null && tree.getClosestPathForLocation(e.getX(), e.getY()).equals(new TreePath(declarations.getPath()))) - { - tree.setSelectionPath(new TreePath(declarations.getPath())); - declarationCollectionPopup.show(tree,e.getX(),e.getY()); - } - else if(editable && constants != null && tree.getClosestPathForLocation(e.getX(), e.getY()).equals(new TreePath(constants.getPath())))//constant collection node - { - tree.setSelectionPath(new TreePath(constants.getPath())); - constantsCollectionPopup.show(tree,e.getX(), e.getY()); - } - else // is the path on a ModuleNode or a DeclarationNode or an ExpressionNode - { - TreePath selectedPath = tree.getClosestPathForLocation(e.getX(), e.getY()); - for(int i = 0; i < editableModules.size(); i++) //search each module - { - ModuleNode mn = (ModuleNode)editableModules.get(i); - if(new TreePath(mn.getPath()).equals(selectedPath)) - { - tree.setSelectionPath(selectedPath); - if(mn.isEditable()) - { - modulePopup.show(tree, e.getX(), e.getY()); - lastPopNode = mn; - - if(graphicEditor != null)graphicEditor.switchModuleView(mn); - } - return; - } - for(int j = 0; j < mn.getChildCount(); j++)//search local variables - { - DeclarationNode dn = (DeclarationNode)mn.getChildAt(j); - if(new TreePath(dn.getPath()).equals(selectedPath)) - { - tree.setSelectionPath(selectedPath); - if(dn.isEditable()) - { - declarationPopup.show(tree, e.getX(), e.getY()); - lastPopNode = dn; - } - return; - } - } - } - for(int i = 0; i < editableDeclarations.size(); i++)//search globals - { - DeclarationNode dn = (DeclarationNode)editableDeclarations.get(i); - if(new TreePath(dn.getPath()).equals(selectedPath)) - { - tree.setSelectionPath(selectedPath); - if(dn.isEditable()) - { - declarationPopup.show(tree, e.getX(), e.getY()); - lastPopNode = dn; - } - return; - } - } - for(int i = 0; i < editableConstants.size(); i++)//search constants - { - DeclarationNode dn = (DeclarationNode)editableConstants.get(i); - if(new TreePath(dn.getPath()).equals(selectedPath)) - { - tree.setSelectionPath(selectedPath); - if(dn.isEditable()) - { - declarationPopup.show(tree, e.getX(), e.getY()); - lastPopNode = dn; - } - return; - } - } - - //Could be an ExpressionNode - if(tree.getSelectionPath() != null) - { - TreeNode selectedNode = (TreeNode)tree.getSelectionPath().getLastPathComponent(); - if(selectedNode instanceof ExpressionNode) - { - ExpressionNode en = (ExpressionNode)selectedNode; - if(en.isEditable()) - { - expressionPopup.show(tree, e.getX(), e.getY()); - lastPopNode = en; - } - } - } - - } - - } - else - { - TreePath selectedPath = tree.getClosestPathForLocation(e.getX(), e.getY()); - for(int i = 0; i < editableModules.size(); i++) //search each module - { - ModuleNode mn = (ModuleNode)editableModules.get(i); - if(new TreePath(mn.getPath()).equals(selectedPath)) - { - tree.setSelectionPath(selectedPath); - if(graphicEditor != null)graphicEditor.switchModuleView(mn); - return; - } - } - } - - } - - public String getToolTipText() - { - return handler.getParseErrorMessage(); - } - - public ModelType getModelType() - { - return ModelType.valueOf(modelType.getUserObject().toString()); - } - - public String getParseText() - { - int i,j; - String str = ""; - //Header - str+="//Generated by the PRISM Graphic Model Editor\n"; - str+="\n"; - - //Model Type - String type = modelType.getUserObject().toString(); - str += type.toLowerCase() + "\n\n"; - - //Constants - if(constants.getChildCount() != 0) - { - str+="//Constants\n\n"; - for(i = 0; i < constants.getChildCount(); i++) - { - ConstantNode cn = (ConstantNode)constants.getChildAt(i); - if(cn.isEditable())str+=cn.getParseText()+"\n"; - } - str+="\n"; - } - - //Globals - if(declarations.getChildCount() != 0) - { - str+="//Globals\n\n"; - for(i = 0; i < declarations.getChildCount(); i++) - { - DeclarationNode gn = (DeclarationNode)declarations.getChildAt(i); - if(gn.isEditable())str+= gn.getParseText()+"\n"; - } - str+="\n"; - } - - //Modules - if(modules.getChildCount() != 0) - { - str+="//GUI Modules\n\n"; - for(i = 0; i < modules.getChildCount(); i++) - { - ModuleNode mn = (ModuleNode)modules.getChildAt(i); - if(mn.isEditable()) - { - str+="module "+mn.getName()+"\n"; - for(j = 0; j < mn.getChildCount(); j++) - { - DeclarationNode dn = (DeclarationNode)mn.getChildAt(j); - str+=TAB+dn.getParseText()+"\n"; - } - - - ModuleModel aModuleModel = mn.getModuleModel(); - String stateVar = ((StateVarNode)mn.getChildAt(0)).getName(); - //now add the transition information - for(j = 0; j < aModuleModel.getNumStates(); j++) - { - State aState = aModuleModel.getState(j); - if(!aState.getCommentLabel().getString().equals("")) - str+=TAB+("//"+aState.getComment()+"\n"); - for(int k = 0; k < aModuleModel.getNumTransitions(); k++) - { - Transition aTrans = aModuleModel.getTransition(k); - if(aTrans.getFrom() == aState) - { - if(!(aTrans instanceof ProbTransition || aTrans.getTo() instanceof Decision))// if not branched - { - - String sync = removeCarriages(aTrans.getSyncLabel().getString()); - String guard = removeCarriages(aTrans.getGuardLabel().getString()); - if(!guard.equals("")) guard = " & ("+guard+")"; - String assign = removeCarriages(aTrans.getAssignmentLabel().getString()); - if(!assign.equals("")) assign = " & "+assign+""; - String prob = removeCarriages(aTrans.getProbabilityLabel().getString()); - int to = aModuleModel.getStateIndex(aTrans.getTo()); - if(prob.equals("") || prob == null) - { - str+=TAB+("["+sync+"]"+ "("+stateVar+"="+j+") "+guard+" -> ("+stateVar+"'="+to+")"+assign+";"+"\n"); - } - else - { - str+=TAB+("["+sync+"]"+ "("+stateVar+"="+j+") "+guard+" -> "+ prob +" : ("+stateVar+"'="+to+")"+assign+";"+"\n"); - } - } - else if(aTrans.getTo() instanceof Decision) // if branched - { - String sync = removeCarriages(aTrans.getSyncLabel().getString()); - String guard = removeCarriages(aTrans.getGuardLabel().getString()); - if(!guard.equals("")) guard = " & ("+guard+")"; - str+=(TAB+"["+sync+"] ("+stateVar+"="+j+") "+guard+" -> "); - Decision dec = (Decision)(aTrans.getTo()); - boolean firstDone = false; - for(int l = 0; l < aModuleModel.getNumTransitions(); l++) - { - Transition branch = aModuleModel.getTransition(l); - if(branch.getFrom() == dec) - { - ProbTransition pTran = (ProbTransition)branch; - String prob = pTran.getProbabilityLabel().getString(); - int to = aModuleModel.getStateIndex(pTran.getTo()); - String assign = removeCarriages(pTran.getAssignmentLabel().getString()); - if(!assign.equals("")) assign = " & "+assign+""; - if(firstDone)str+=("+ "); - firstDone = true; - str+=(prob+" : "+"("+stateVar+"'="+to+")"+assign+" "); - } - } - str+=(";\n"); - } - } - } - } - - str+="\n"; - str+="endmodule\n\n"; - } - } - str+="\n"; - - } - //System.out.println("parsed model = "+str); - return str; - } - public static final String TAB = " "; - - public ArrayList getEditableConstantNames() - { - ArrayList names = new ArrayList(); - for(int i = 0; i < editableConstants.size(); i++) - { - DeclarationNode dn = (DeclarationNode)editableConstants.get(i); - names.add(dn.getName()); - } - return names; - } - - public ArrayList getEditableConstantValues() - { - ArrayList values = new ArrayList(); - for(int i = 0; i < editableConstants.size(); i++) - { - ConstantNode cn = (ConstantNode)editableConstants.get(i); - if(cn.getValue() != null) - { - if(!cn.getValue().toString().equals("")) - { - values.add(cn.getValue().toString()); - } - else - values.add(null); - } - else values.add(null); - } - return values; - } - - public ArrayList getEditableConstantTypes() - { - ArrayList types = new ArrayList(); - for(int i = 0; i < editableConstants.size(); i++) - { - Object node = editableConstants.get(i); - if(node instanceof BoolConstantNode) - { - types.add(TypeBool.getInstance()); - } - else if(node instanceof IntegerConstantNode) - { - types.add(TypeInt.getInstance()); - } - else if(node instanceof DoubleConstantNode) - { - types.add(TypeDouble.getInstance()); - } - else types.add(null); - } - return types; - } - - public ArrayList getEditableGlobalNames() - { - ArrayList names = new ArrayList(); - for(int i = 0; i < editableDeclarations.size(); i++) - { - DeclarationNode dn = (DeclarationNode)editableDeclarations.get(i); - names.add(dn.getName()); - } - return names; - } - - public ArrayList getEditableGlobalMins() - { - ArrayList mins = new ArrayList(); - for(int i = 0; i < editableDeclarations.size(); i++) - { - Object node = editableDeclarations.get(i); - if(node instanceof GlobalNode) - { - GlobalNode gn = (GlobalNode)node; - mins.add(gn.getMin().toString()); - } - else - mins.add(null); - } - return mins; - } - - public ArrayList getEditableGlobalMaxs() - { - ArrayList maxs = new ArrayList(); - for(int i = 0; i < editableDeclarations.size(); i++) - { - Object node = editableDeclarations.get(i); - if(node instanceof GlobalNode) - { - GlobalNode gn = (GlobalNode)node; - maxs.add(gn.getMax().toString()); - } - else - maxs.add(null); - - } - return maxs; - } - - public ArrayList getEditableGlobalInits() - { - ArrayList inits = new ArrayList(); - for(int i = 0; i < editableDeclarations.size(); i++) - { - Object node = editableDeclarations.get(i); - if(node instanceof GlobalNode) - { - GlobalNode gn = (GlobalNode)node; - inits.add(gn.getInitial().toString()); - } - else if(node instanceof GlobalBoolNode) - { - GlobalBoolNode gbn = (GlobalBoolNode)node; - inits.add(gbn.getInitial().toString()); - } - } - return inits; - } - - public ArrayList getEditableGlobalTypes() - { - ArrayList types = new ArrayList(); - for(int i = 0; i < editableDeclarations.size(); i++) - { - Object node = editableDeclarations.get(i); - if(node instanceof GlobalBoolNode) - { - types.add(TypeBool.getInstance()); - } - else if(node instanceof GlobalNode) - { - types.add(TypeInt.getInstance()); - } - else types.add(null); - } - return types; - } - - public ArrayList getVariableNames(ModuleNode m) - { - ArrayList names = new ArrayList(); - for(int i = 0; i < m.getChildCount(); i++) - { - DeclarationNode vn = (DeclarationNode)m.getChildAt(i); - if(!(vn instanceof StateVarNode)) - { - names.add(vn.getName()); - } - } - return names; - } - - public ArrayList getVariableTypes(ModuleNode m) - { - ArrayList types = new ArrayList(); - for(int i = 0; i < m.getChildCount(); i++) - { - DeclarationNode dn = (DeclarationNode)m.getChildAt(i); - if(!(dn instanceof StateVarNode)) - { - if(dn instanceof BoolNode) - types.add(TypeBool.getInstance()); - else if(dn instanceof VarNode) - types.add(TypeInt.getInstance()); - else - types.add(null); - } - } - return types; - } - - public ArrayList getVariableMins(ModuleNode m) - { - ArrayList mins = new ArrayList(); - for(int i = 0; i < m.getChildCount(); i++) - { - DeclarationNode dn = (DeclarationNode)m.getChildAt(i); - if(!(dn instanceof StateVarNode)) - { - if(dn instanceof BoolNode) - mins.add(null); - else if(dn instanceof VarNode) - { - VarNode vn = (VarNode)dn; - String s = vn.getMin().toString(); - mins.add(s); - } - else - mins.add(null); - } - } - return mins; - } - - public ArrayList getVariableMaxs(ModuleNode m) - { - ArrayList maxs = new ArrayList(); - for(int i = 0; i < m.getChildCount(); i++) - { - DeclarationNode dn = (DeclarationNode)m.getChildAt(i); - if(!(dn instanceof StateVarNode)) - { - if(dn instanceof BoolNode) - maxs.add(null); - else if(dn instanceof VarNode) - { - VarNode vn = (VarNode)dn; - String s = vn.getMax().toString(); - maxs.add(s); - } - else - maxs.add(null); - } - } - return maxs; - } - - public ArrayList getVariableInits(ModuleNode m) - { - ArrayList inits = new ArrayList(); - for(int i = 0; i < m.getChildCount(); i++) - { - DeclarationNode dn = (DeclarationNode)m.getChildAt(i); - if(!(dn instanceof StateVarNode)) - { - if(dn instanceof BoolNode) - { - BoolNode bn = (BoolNode)dn; - String s = bn.getInitial().toString(); - inits.add(s); - } - else if(dn instanceof VarNode) - { - VarNode vn = (VarNode)dn; - String s = vn.getInitial().toString(); - inits.add(s); - } - else - inits.add(null); - } - } - return inits; - } - - public void updateTooltip() - { - tree.setToolTipText(handler.getParseErrorMessage()); - } - - - - - - - - //Node Data Structure Classes - - interface PrismTreeNode - { - public boolean isEditable(); - } - - class ModelRootNode extends DefaultMutableTreeNode implements PrismTreeNode - { - public ModelRootNode() - { - super("", true); - } - - public boolean isEditable() - { - return false; - } - - } - - class ModuleCollectionNode extends DefaultMutableTreeNode implements PrismTreeNode - { - public ModuleCollectionNode() - { - super("Modules", true); - super.setAllowsChildren(true); - } - - public void addModule(ModuleNode mod) - { - add(mod); - } - - public void removeModule(ModuleNode mod) - { - remove(mod); - } - - public boolean isEditable() - { - return editable; - } - - } - - class DeclarationCollectionNode extends DefaultMutableTreeNode implements PrismTreeNode - { - public DeclarationCollectionNode() - { - super("Global Variables", true); - super.setAllowsChildren(true); - } - - public void addDeclaration(DeclarationNode dec) - { - add(dec); - } - - public void removeDeclaration(DeclarationNode dec) - { - remove(dec); - } - - public boolean isEditable() - { - return editable; - } - - } - - class ConstantCollectionNode extends DefaultMutableTreeNode implements PrismTreeNode - { - public ConstantCollectionNode() - { - super("Constants", true); - } - - public void addConstant(ConstantNode n) - { - add(n); - } - - public void removeConstant(ConstantNode n) - { - remove(n); - } - - public boolean isEditable() - { - return editable; - } - } - - public class ModuleNode extends DefaultMutableTreeNode implements PrismTreeNode - { - private boolean editable; - private ModuleModel moduleModel; - - public ModuleNode(String moduleName, boolean editable) - { - super(moduleName, true); - moduleModel = null; - this.editable = editable; - } - - public void addVariable(VarNode var) - { - add(var); - } - - public void removeVariable(VarNode var) - { - remove(var); - } - - public void setName(String str) - { - setUserObject(str); - } - - public String getName() - { - return (String)getUserObject(); - } - - public boolean isEditable() - { - return editable; - } - - public void setEditable(boolean b) - { - editable = b; - } - - public void setModel(ModuleModel n) - { - moduleModel = n; - } - - public ModuleModel getModuleModel() - { - return moduleModel; - } - - public void childrenChanged() - { - theModel.nodeChanged(this); - theModel.nodeStructureChanged(this); - } - - public boolean isLeaf() - { - return false; - } - - } - //Editor for ModuleNode - class ModuleEditor extends JTextField implements TreeCellEditor - { - String name; - Vector listeners = new Vector(); - private static final int minWidth = 64; - - public ModuleEditor() - { - super(""); - addActionListener(new ActionListener() - { - public void actionPerformed(ActionEvent as) - { - if(stopCellEditing()) - fireEditingStopped(); - } - }); - } - - public void cancelCellEditing() - { - setText(""); - } - - public boolean stopCellEditing() - { - Expression exp; - String str = getText(); - try { - exp = handler.getGUIPlugin().getPrism().parseSingleExpressionString(str); - } - catch (PrismException e) { - return false; - } - if(exp instanceof ExpressionIdent) - { - name = str; - return true; - } - else - { - return false; - } - } - - public Object getCellEditorValue() - { - return name; - } - - public boolean isCellEditable(EventObject eo) - { - if((eo == null) | ((eo instanceof MouseEvent) && (((MouseEvent)eo).isMetaDown()))) - { - return true; - } - return false; - } - - public boolean shouldSelectCell(EventObject eo) - { - return true; - } - - public void removeCellEditroLIstner(CellEditorListener cel) - { - listeners.removeElement(cel); - } - - protected void fireEditingStopped() - { - if(listeners.size() > 0) - { - ChangeEvent ce = new ChangeEvent(this); - for(int i = listeners.size()-1; i >=0; i--) - { - ((CellEditorListener)listeners.elementAt(i)).editingStopped(ce); - } - - } - } - //make sure the JTree gives the editor enough space - public void setBounds(Rectangle r) - { - r.width = Math.max(minWidth, r.width); - super.setBounds(r); - } - - public void setBounds(int x, int y, int w, int h) - { - w = Math.max(minWidth, w); - super.setBounds(x,y,w,h); - } - - public void addCellEditorListener(CellEditorListener l) - { - listeners.addElement(l); - } - - public void removeCellEditorListener(CellEditorListener l) - { - listeners.removeElement(l); - } - - public Component getTreeCellEditorComponent(JTree tree, Object value, boolean isSelected, boolean expanded, boolean leaf, int row) - { - return this; - } - - //same listener and bounds methods as above - } - - public static final int LOCAL_INTEGER = 0; - public static final int LOCAL_BOOL = 1; - public static final int GLOBAL_INTEGER = 2; - public static final int GLOBAL_BOOL = 3; - public static final int CONST_INTEGER = 4; - public static final int CONST_BOOL = 5; - public static final int CONST_DOUBLE = 6; - - - abstract class DeclarationNode extends DefaultMutableTreeNode implements PrismTreeNode - { - private boolean editable; - private int type; - - public DeclarationNode(int type, String name, boolean editable) - { - super(name, true); - this.editable = editable; - this.type = type; - } - - public boolean getAllowsChildren() - { - return true; - } - - public boolean isLeaf() - { - return false; - } - - public boolean isEditable() - { - return editable; - } - - public String getName() - { - return (String)getUserObject(); - } - - public void setName(String str) - { - setUserObject(str); - } - - public String toString() - { - String name = getName(); - switch(type) - { - case LOCAL_INTEGER: return name; - case GLOBAL_INTEGER: - case CONST_INTEGER: return name+" : int"; - case LOCAL_BOOL: - case GLOBAL_BOOL: - case CONST_BOOL: return name+" : bool"; - case CONST_DOUBLE: return name+" : double"; - default: return ""; - } - } - - public abstract String getParseText(); - } - //Editor for DeclarationNode - class DeclarationEditor extends JTextField implements TreeCellEditor - { - String name; - Vector listeners = new Vector(); - private static final int minWidth = 64; - - public DeclarationEditor() - { - super(""); - addActionListener(new ActionListener() - { - public void actionPerformed(ActionEvent as) - { - if(stopCellEditing()) - fireEditingStopped(); - } - }); - } - - public void cancelCellEditing() - { - setText(""); - } - - public boolean stopCellEditing() - { - Expression exp; - String str = getText(); - try { - exp = handler.getGUIPlugin().getPrism().parseSingleExpressionString(str); - } - catch (PrismException e) { - return false; - } - if(exp instanceof ExpressionIdent) - { - name = str; - return true; - } - else - { - return false; - } - } - - public Object getCellEditorValue() - { - return name; - } - - public boolean isCellEditable(EventObject eo) - { - if((eo == null) | ((eo instanceof MouseEvent) && (((MouseEvent)eo).isMetaDown()))) - { - return true; - } - return false; - } - - public boolean shouldSelectCell(EventObject eo) - { - return true; - } - - protected void fireEditingStopped() - { - if(listeners.size() > 0) - { - ChangeEvent ce = new ChangeEvent(this); - for(int i = listeners.size()-1; i >=0; i--) - { - ((CellEditorListener)listeners.elementAt(i)).editingStopped(ce); - } - - } - } - //make sure the JTree gives the editor enough space - public void setBounds(Rectangle r) - { - r.width = Math.max(minWidth, r.width); - super.setBounds(r); - } - - public void setBounds(int x, int y, int w, int h) - { - w = Math.max(minWidth, w); - super.setBounds(x,y,w,h); - } - - public void addCellEditorListener(CellEditorListener l) - { - listeners.addElement(l); - } - - public void removeCellEditorListener(CellEditorListener l) - { - listeners.addElement(l); - } - - public Component getTreeCellEditorComponent(JTree tree, Object value, boolean isSelected, boolean expanded, boolean leaf, int row) - { - return this; - } - - } - - class VarNode extends DeclarationNode - { - - public VarNode(String name, Expression init, Expression min, Expression max, boolean editable) - { - super(LOCAL_INTEGER, name, editable); - super.add(new ExpressionNode("min: ", min, editable)); - super.add(new ExpressionNode("max: ", max, editable)); - super.add(new ExpressionNode("init: ", init, editable)); - } - - public VarNode(String name, String init, String min, String max, boolean editable) - { - super(LOCAL_INTEGER, name, editable); - try - { - Expression e_init = handler.getGUIPlugin().getPrism().parseSingleExpressionString(init); - Expression e_min = handler.getGUIPlugin().getPrism().parseSingleExpressionString(min); - Expression e_max = handler.getGUIPlugin().getPrism().parseSingleExpressionString(max); - super.add(new ExpressionNode("min: ", e_min, editable)); - super.add(new ExpressionNode("max: ", e_max, editable)); - super.add(new ExpressionNode("init: ", e_init, editable)); - } - catch(Exception e) - {} - } - - public void setInitial(Expression e) - { - ExpressionNode n = (ExpressionNode)getChildAt(2); - n.setUserObject(e); - theModel.nodeChanged(getChildAt(2)); - } - - public Expression getInitial() - { - ExpressionNode n = (ExpressionNode)getChildAt(2); - return n.getValue(); - } - - public void setMin(Expression e) - { - ExpressionNode n = (ExpressionNode)getChildAt(0); - n.setUserObject(e); - theModel.nodeChanged(getChildAt(0)); - } - - public Expression getMin() - { - ExpressionNode n = (ExpressionNode)getChildAt(0); - return n.getValue(); - } - - public void setMax(Expression e) - { - ExpressionNode n = (ExpressionNode)getChildAt(1); - n.setUserObject(e); - theModel.nodeChanged(getChildAt(1)); - } - - public Expression getMax() - { - ExpressionNode n = (ExpressionNode)getChildAt(1); - return n.getValue(); - } - - public String getParseText() - { - String str = getName()+" : ["+getMin()+".."+getMax()+"] init "+getInitial()+";"; - return str; - } - - } - - public class StateVarNode extends VarNode - { - ModuleNode mn; - public StateVarNode(ModuleNode mn) throws prism.PrismException - { - super("statevariable", "0", "0", "0", false); - this.mn = mn; - } - - public String getName() - { - return mn.getName()+"_s"; - } - } - - class BoolNode extends DeclarationNode - { - public BoolNode(String name, Expression init, boolean editable) - { - super(LOCAL_BOOL, name, editable); - super.add(new ExpressionNode("init: ", init, editable)); - } - - public void setInitial(Expression e) - { - ExpressionNode n = (ExpressionNode)getChildAt(0); - n.setUserObject(e); - } - - public Expression getInitial() - { - ExpressionNode n = (ExpressionNode)getChildAt(0); - return n.getValue(); - } - - public String getParseText() - { - String str = getName()+" : bool init "+getInitial()+";"; - return str; - } - - } - - class GlobalNode extends DeclarationNode - { - - public GlobalNode(String name, Expression init, Expression min, Expression max, boolean editable) - { - super(GLOBAL_INTEGER, name, editable); - super.add(new ExpressionNode("min: ", min, editable)); - super.add(new ExpressionNode("max: ", max, editable)); - super.add(new ExpressionNode("init: ", init, editable)); - } - - public void setInitial(Expression e) - { - ExpressionNode n = (ExpressionNode)getChildAt(2); - n.setUserObject(e); - } - - public Expression getInitial() - { - ExpressionNode n = (ExpressionNode)getChildAt(2); - return n.getValue(); - } - - public void setMin(Expression e) - { - ExpressionNode n = (ExpressionNode)getChildAt(0); - n.setUserObject(e); - } - - public Expression getMin() - { - ExpressionNode n = (ExpressionNode)getChildAt(0); - return n.getValue(); - } - - public void setMax(Expression e) - { - ExpressionNode n = (ExpressionNode)getChildAt(1); - n.setUserObject(e); - } - - public Expression getMax() - { - ExpressionNode n = (ExpressionNode)getChildAt(1); - return n.getValue(); - } - - public String getParseText() - { - String str = "global "+getName()+" : ["+getMin()+".."+getMax()+"] init "+getInitial()+";"; - return str; - } - - } - - class GlobalBoolNode extends DeclarationNode - { - public GlobalBoolNode(String name, Expression init, boolean editable) - { - super(GLOBAL_BOOL, name, editable); - super.add(new ExpressionNode("init: ", init, editable)); - } - - public void setInitial(Expression e) - { - ExpressionNode n = (ExpressionNode)getChildAt(0); - n.setUserObject(e); - } - - public Expression getInitial() - { - ExpressionNode n = (ExpressionNode)getChildAt(0); - return n.getValue(); - } - - public String getParseText() - { - String str = "global "+getName()+" : bool init "+getInitial()+";"; - return str; - } - - } - - abstract class ConstantNode extends DeclarationNode - { - public ConstantNode(int type, String name, boolean editable) - { - super(type, name, editable); - } - - public abstract void setValue(Expression e); - - public abstract Expression getValue(); - - public boolean equals(Object obj) - { - if(obj instanceof ConstantNode) - { - ConstantNode other = (ConstantNode)obj; - if(!other.getName().equals(getName())) return false; - else return true; //can only compare the equality of the names - } - else return false; - } - - public abstract String getParseText(); - - } - - class IntegerConstantNode extends ConstantNode - { - public IntegerConstantNode(String name, Expression value, boolean editable) - { - super(CONST_INTEGER, name, editable); - super.add(new ExpressionNode("value: ", value, editable)); - } - - public void setValue(Expression e) - { - ExpressionNode n = (ExpressionNode)getChildAt(0); - n.setUserObject(e); - } - - public Expression getValue() - { - ExpressionNode n = (ExpressionNode)getChildAt(0); - return n.getValue(); - } - - public String getParseText() - { - String str = "const int "+getName(); - if(getValue() != null) - { - str+=" = "+getValue()+";"; - } - else - { - str+=";"; - } - return str; - } - - } - - class DoubleConstantNode extends ConstantNode - { - public DoubleConstantNode(String name, Expression value, boolean editable) - { - super(CONST_DOUBLE, name, editable); - super.add(new ExpressionNode("value: ", value, editable)); - } - - public void setValue(Expression e) - { - ExpressionNode n = (ExpressionNode)getChildAt(0); - n.setUserObject(e); - } - - public Expression getValue() - { - ExpressionNode n = (ExpressionNode)getChildAt(0); - return n.getValue(); - } - - public String getParseText() - { - String str = "const double "+getName(); - if(getValue() != null) - { - str+=" = "+getValue()+";"; - } - else - { - str+=";"; - } - return str; - } - - } - - class BoolConstantNode extends ConstantNode - { - public BoolConstantNode(String name, Expression value, boolean editable) - { - super(CONST_BOOL, name, editable); - super.add(new ExpressionNode("value: ", value, editable)); - } - - public void setValue(Expression e) - { - ExpressionNode n = (ExpressionNode)getChildAt(0); - n.setUserObject(e); - } - - public Expression getValue() - { - ExpressionNode n = (ExpressionNode)getChildAt(0); - return n.getValue(); - } - - public String getParseText() - { - String str = "const bool "+getName(); - if(getValue() != null) - { - str+=" = "+getValue()+";"; - } - else - { - str+=";"; - } - return str; - } - - } - - - abstract class ValueNode extends DefaultMutableTreeNode implements PrismTreeNode - { - private String tag; - - public ValueNode(String tag, Object value) - { - super(value); - this.tag = tag; - } - - public String toString() - { - if(getUserObject() == null) return tag+"?"; - else return tag+getUserObject().toString(); - } - - public abstract boolean isEditable(); - - public boolean isLeaf() - { - return true; - } - - public void setUserObject(Object obj) - { - super.setUserObject(obj); - } - } - - class StringNode extends ValueNode - { - private boolean editable; - - public StringNode(String tag, String value, boolean editable) - { - super(tag, value); - this.editable = editable; - } - - public boolean isEditable() - { - return editable; - } - - public String getValue() - { - return (String)getUserObject(); - } - - } - - class ExpressionNode extends ValueNode - { - private boolean editable; - - public ExpressionNode(String tag, Expression value, boolean editable) - { - super(tag, value); - this.editable = editable; - } - - public boolean isEditable() - { - return editable; - } - - public Expression getValue() - { - return (Expression)getUserObject(); - } - - public void setValue(Expression value) - { - super.setUserObject(value); - } - - } - /* - class ExpressionEditor extends javax.swing.DefaultCellEditor - { - Expression exp; - int minWidth = 100; - - public ExpressionEditor() - { - super(new JTextField()); - } - - public Component getComponent() - { - return editorComponent; - } - - public boolean stopCellEditing() - { - String str = ((JTextField)editorComponent).getText(); - - try - { - Expression s = handler.getGUIPlugin().getPrism().parseSingleExpressionString(str); - exp = s; - } - catch(Exception e) - { - handler.getGUIPlugin().message("Error: Syntax Error"); - super.fireEditingStopped(); - return true; - } - super.fireEditingStopped(); - return true; - - } - - public void setBounds(Rectangle r) - { - r.width = Math.max(minWidth, r.width); - getComponent().setBounds(r); - tree.repaint(); - } - - public void setBounds(int x, int y, int w, int h) - { - w = Math.max(minWidth, w); - getComponent().setBounds(x,y,w,h); - tree.repaint(); - } - }*/ - - //Cell edit for ExpressionNode - class ExpressionEditor extends JTextField implements TreeCellEditor - { - Expression exp; - Vector listeners = new Vector(); - private static final int minWidth = 64; - - public ExpressionEditor() - { - super(""); - addActionListener(new ActionListener() - { - public void actionPerformed(ActionEvent as) - { - if(stopCellEditing()) - fireEditingStopped(); - } - }); - } - - public void cancelCellEditing() - { - setText(""); - } - - public boolean stopCellEditing() - { - String str = getText(); - - try - { - Expression s = handler.getGUIPlugin().getPrism().parseSingleExpressionString(str); - exp = s; - } - catch(Exception e) - { - handler.getGUIPlugin().message("Error: Syntax Error"); - return true; - } - return true; - - } - - public Object getCellEditorValue() - { - return exp; - } - - public boolean isCellEditable(EventObject eo) - { - if((eo == null) | ((eo instanceof MouseEvent) && (((MouseEvent)eo).isMetaDown()))) - { - MouseEvent me = (MouseEvent)eo; - if(me.getClickCount() >= 2) - { - return true; - } - } - return false; - } - - public boolean shouldSelectCell(EventObject eo) - { - if((eo == null) | ((eo instanceof MouseEvent) && (((MouseEvent)eo).isMetaDown()))) - { - MouseEvent me = (MouseEvent)eo; - if(me.getClickCount() >= 2) - { - return true; - } - } - return false; - } - - protected void fireEditingStopped() - { - if(listeners.size() > 0) - { - ChangeEvent ce = new ChangeEvent(this); - for(int i = listeners.size()-1; i >=0; i--) - { - ((CellEditorListener)listeners.elementAt(i)).editingStopped(ce); - } - - } - } - //make sure the JTree gives the editor enough space - public void setBounds(Rectangle r) - { - r.width = Math.max(minWidth, r.width); - super.setBounds(r); - tree.repaint(); - } - - public void setBounds(int x, int y, int w, int h) - { - w = Math.max(minWidth, w); - super.setBounds(x,y,w,h); - tree.repaint(); - } - - public void addCellEditorListener(CellEditorListener l) - { - listeners.addElement(l); - } - - public void removeCellEditorListener(CellEditorListener l) - { - listeners.addElement(l); - } - - public Component getTreeCellEditorComponent(JTree tree, Object value, boolean isSelected, boolean expanded, boolean leaf, int row) - { - return this; - } - - } - - class ModelTypeNode extends StringNode - { - public ModelTypeNode(String init, boolean editable) - { - super("Type: ", init, editable); - } - - public void setModelType(ModelType type) - { - setUserObject(type.toString()); - switch (type) { - case MDP: non.setSelected(true); break; - case DTMC: pro.setSelected(true); break; - case CTMC: sto.setSelected(true); break; - } - theModel.nodeChanged(this); - } - - public void setUserObject(Object obj) - { - super.setUserObject(obj); - //System.out.println("setting model type user object "+obj); - - } - } - //Cell Editor for ModelTypeNode - class ModelTypeEditor extends JComboBox implements TreeCellEditor - { - String value; - Vector listeners = new Vector(); - private static final int minWidth = 36; - Object[] list; - - public ModelTypeEditor(Object[] list) - { - super(list); - setFont(tree.getFont()); - setBackground(Color.white); - setForeground(Color.blue); - - this.list = list; - setEditable(false);//why??? - value = list[0].toString(); - - addActionListener(new ActionListener() - { - public void actionPerformed(ActionEvent e) - { - if(stopCellEditing()) - fireEditingStopped(); - } - }); - } - - public void setSelectedType(String str) - { - for(int i = 0; i < list.length; i++) - { - String cur = (String)list[i]; - if(cur.equals(str)) - { - super.setSelectedIndex(i); - break; - } - } - } - - public void cancelCellEditing() - {} - - public boolean stopCellEditing() - { - try - { - value = (String)getSelectedItem(); - if(value == null) - { - value = (String)getItemAt(0); - } - return true; - - } - catch(Exception e) - { - return false; - } - } - - public Object getCellEditorValue() - { - return value; - } - - public boolean isCellEditable(EventObject eo) - { - if((eo == null) || ((eo instanceof MouseEvent) && (((MouseEvent)eo).isMetaDown()))) - { - MouseEvent me = (MouseEvent)eo; - if(me.getClickCount() >= 2) - { - return true; - } - } - return false; - } - - public boolean shouldSelectCell(EventObject eo) - { - if((eo == null) | ((eo instanceof MouseEvent) && (((MouseEvent)eo).isMetaDown()))) - { - MouseEvent me = (MouseEvent)eo; - if(me.getClickCount() >= 2) - { - return true; - } - } - return false; - } - - public void addCellEditorListener(CellEditorListener cel) - { - listeners.addElement(cel); - } - - public void removeCellEditorListener(CellEditorListener cel) - { - listeners.removeElement(cel); - } - - protected void fireEditingStopped() - { - if(listeners.size() > 0) - { - ChangeEvent ce = new ChangeEvent(this); - for(int i = listeners.size()-1; i >=0; i--) - { - ((CellEditorListener)listeners.elementAt(i)).editingStopped(ce); - } - - } - } - - public Component getTreeCellEditorComponent(JTree tree, Object value, boolean isSelected, boolean expanded, boolean leaf, int row) - { - return this; - } - -/* - //make sure the JTree gives the editor enough space - public void setBounds(Rectangle r) - { - r.width = Math.max(minWidth, r.width); - super.setBounds(r); - } - - public void setBounds(int x, int y, int w, int h) - { - w = Math.max(minWidth, w); - super.setBounds(x,y,w,h); - }*/ - - } - - - //Node Renderer - class PrismNodeRenderer extends DefaultTreeCellRenderer - { - ImageIcon VAR = GUIPrism.getIconFromImage("smallVariable.png"); - ImageIcon MOD = GUIPrism.getIconFromImage("smallModule.png"); - //ImageIcon EXP = GUIPrism.getIconFromImage("smallExpression.png"); - ImageIcon VAL = GUIPrism.getIconFromImage("smallValue.png"); - ImageIcon GOOD = GUIPrism.getIconFromImage("smallTick.png"); - ImageIcon BAD = GUIPrism.getIconFromImage("smallCross.png"); - ImageIcon OUT_OF_SYNCH = GUIPrism.getIconFromImage("smallFilePrism.png"); - ImageIcon CLOCK = GUIPrism.getIconFromImage("smallClockAnim1.png"); - - public Component getTreeCellRendererComponent(JTree tree, Object value, boolean selected, boolean expanded, boolean leaf, int row, boolean hasFocus) - { - super.getTreeCellRendererComponent(tree,value,selected,expanded,leaf,row,hasFocus); - PrismTreeNode node = (PrismTreeNode)value; - - if(node == root) - { - if (isParsing) - { - setIcon(animIcon); - } else - { - switch(parseSynchState) - { - case TREE_SYNCHRONIZED_GOOD: setIcon(GOOD);break; - case TREE_SYNCHRONIZED_BAD: setIcon(BAD);break; - case TREE_NOT_SYNCHRONIZED: setIcon(OUT_OF_SYNCH);break; - } - } - } - else if(node instanceof VarNode) - { - setIcon(VAR); - } - else if(node instanceof BoolNode) - { - setIcon(VAR); - } - else if(node instanceof DeclarationNode) - { - setIcon(VAR); - } - else if(node instanceof ModuleNode) - { - setIcon(MOD); - } - else if(node instanceof ValueNode) - { - //if(node instanceof ExpressionNode) - //{ - //setIcon(EXP); - //} - //else - { - setIcon(VAL); - } - } - else if(node instanceof ModuleCollectionNode || node instanceof DeclarationCollectionNode || node instanceof ConstantCollectionNode) - { - setIcon(this.getDefaultClosedIcon()); - } - if(node.isEditable()) - { - setForeground(Color.blue); - } - else setForeground(Color.black); - - return this; - } - } - - class ModelTreeCellEditor extends DefaultTreeCellEditor - { - ModelTypeEditor modelTypeEditor; - ExpressionEditor expressionEditor; - ModuleEditor moduleEditor; - DeclarationEditor declarationEditor; - - String[] types = new String[] - {"Non-deterministic", "Probabilistic", "Stochastic"}; - - public ModelTreeCellEditor(JTree tree, PrismNodeRenderer renderer) - { - super(tree, renderer); - modelTypeEditor = new ModelTypeEditor(types); - expressionEditor = new ExpressionEditor(); - moduleEditor = new ModuleEditor(); - declarationEditor = new DeclarationEditor(); - realEditor = declarationEditor; - } - - public Component getTreeCellEditorComponent(JTree tree, Object value, boolean isSelected, boolean expanded, boolean leaf, int row) - { - if(value instanceof ExpressionNode) - { - realEditor = expressionEditor; - //((JTextField)expressionEditor.getComponent()).setText(((ExpressionNode)value).getValue().toString()); - } - else if(value instanceof ModelTypeNode) - { - realEditor = modelTypeEditor; - modelTypeEditor.setSelectedType(((ModelTypeNode)value).getValue()); - //tag = "Type: "; - } - else if(value instanceof ModuleNode) - { - realEditor = moduleEditor; - moduleEditor.setText(((ModuleNode)value).getName()); - } - else if(value instanceof DeclarationNode) - { - realEditor = declarationEditor; - declarationEditor.setText(((DeclarationNode)value).getName()); - } - return super.getTreeCellEditorComponent(tree, value, isSelected, expanded, leaf, row); - } - - public void addCellEditorListener(CellEditorListener l) - { - - modelTypeEditor.addCellEditorListener(l); - expressionEditor.addCellEditorListener(l); - - moduleEditor.addCellEditorListener(l); - - declarationEditor.addCellEditorListener(l); - super.addCellEditorListener(l); - } - - public void removeCellEditorListener(CellEditorListener l) - { - modelTypeEditor.removeCellEditorListener(l); - expressionEditor.removeCellEditorListener(l); - - moduleEditor.removeCellEditorListener(l); - - declarationEditor.removeCellEditorListener(l); - super.removeCellEditorListener(l); - } - } - /* - class ModelTreeCellEditor_n implements TreeCellEditor - { - ModelTypeEditor modelTypeEditor; - ExpressionEditor expressionEditor; - ModuleEditor moduleEditor; - DeclarationEditor declarationEditor; - - CellEditor currentEditor; - - DefaultTreeCellEditor ttt; - - String[] types = new String[] - {"Non-deterministic", "Probabilistic", "Stochastic"}; - - PrismNodeRenderer renderer; - - public ModelTreeCellEditor_n(PrismNodeRenderer renderer) - { - this.renderer = renderer; - modelTypeEditor = new ModelTypeEditor(types); - expressionEditor = new ExpressionEditor(); - moduleEditor = new ModuleEditor(); - declarationEditor = new DeclarationEditor(); - currentEditor = declarationEditor; - } - - - - public Component getTreeCellEditorComponent(JTree tree, Object value, boolean isSelected, boolean expanded, boolean leaf, int row) - { - String tag = ""; - if(value instanceof ExpressionNode) - { - currentEditor = expressionEditor; -// ((JTextField)expressionEditor.getComponent()).setText(((ExpressionNode)value).getValue().toString()); - } - else if(value instanceof ModelTypeNode) - { - currentEditor = modelTypeEditor; - modelTypeEditor.setSelectedType(((ModelTypeNode)value).getValue()); - tag = "Type: "; - } - else if(value instanceof ModuleNode) - { - currentEditor = moduleEditor; - moduleEditor.setText(((ModuleNode)value).getName()); - } - else if(value instanceof DeclarationNode) - { - currentEditor = declarationEditor; - declarationEditor.setText(((DeclarationNode)value).getName()); - } - DefaultTreeCellRenderer c = (DefaultTreeCellRenderer)renderer.getTreeCellRendererComponent(tree, value, isSelected, expanded, leaf, row, true); - JPanel p = new JPanel(); - p.setBackground(Color.white); - p.setLayout(new BorderLayout()); - JLabel l = new JLabel(tag,c.getIcon(), JLabel.HORIZONTAL); - l.setBackground(Color.white); - l.setForeground(Color.blue); - l.setFont(tree.getFont()); - p.add(l, BorderLayout.WEST); - if(currentEditor instanceof ExpressionEditor) - { - p.add(((ExpressionEditor)currentEditor).getComponent(), BorderLayout.CENTER); - } - else - { - p.add((Component)currentEditor, BorderLayout.CENTER); - } - return p;//(Component)currentEditor; - } - - public Object getCellEditorValue() - { - return currentEditor.getCellEditorValue(); - - } - - public boolean isCellEditable(EventObject event) - { - return true; - //return currentEditor.isCellEditable(event); - } - - public boolean shouldSelectCell(EventObject event) - { - return currentEditor.shouldSelectCell(event); - } - - public boolean stopCellEditing() - { - return currentEditor.stopCellEditing(); - } - - public void cancelCellEditing() - { - currentEditor.cancelCellEditing(); - } - - public void addCellEditorListener(CellEditorListener l) - { - - modelTypeEditor.addCellEditorListener(l); - expressionEditor.addCellEditorListener(l); - - moduleEditor.addCellEditorListener(l); - - declarationEditor.addCellEditorListener(l); - } - - public void removeCellEditorListener(CellEditorListener l) - { - modelTypeEditor.removeCellEditorListener(l); - expressionEditor.removeCellEditorListener(l); - - moduleEditor.removeCellEditorListener(l); - - declarationEditor.removeCellEditorListener(l); - } - - } - - */ - - - - - class IconThread extends Thread - { - int index; - ImageIcon[] images; - boolean canContinue = false; - public IconThread(int index) - { - this.index = index; - images = new ImageIcon[8]; - images[0] = GUIPrism.getIconFromImage("smallClockAnim1.png"); - images[1] = GUIPrism.getIconFromImage("smallClockAnim2.png"); - images[2] = GUIPrism.getIconFromImage("smallClockAnim3.png"); - images[3] = GUIPrism.getIconFromImage("smallClockAnim4.png"); - images[4] = GUIPrism.getIconFromImage("smallClockAnim5.png"); - images[5] = GUIPrism.getIconFromImage("smallClockAnim6.png"); - images[6] = GUIPrism.getIconFromImage("smallClockAnim7.png"); - images[7] = GUIPrism.getIconFromImage("smallClockAnim8.png"); - } - public void run() - { - try - { - int counter = 0; - while(!interrupted() && index>-1) - { - counter++; - counter = counter%8; - animIcon = images[counter]; - tree.repaint(); - sleep(150); - } - } - catch(InterruptedException e) - { - } - canContinue = true; - } - } - - private static String removeCarriages(String line) - { - String lineBuffer = ""; - for(int i = 0; i < line.length(); i++) - { - char c = line.charAt(i); - if(c!='\n') lineBuffer+=c; - else lineBuffer+=" "; - } - return lineBuffer; - } + } + } else if (notTreeDec.getType() instanceof TypeBool) { + BoolNode newVariable = new BoolNode(notTreeDec.getName(), parsedModel.getSystemDefn() == null ? notTreeDec.getStartOrDefault() : null, + false); + inTreeNode.add(newVariable); + cIndices[j] = getVarTreeIndexOf(notTreeDec, inTreeNode); + } else if (notTreeDec.getType() instanceof TypeClock) { + VarNode newVariable = new VarNode(notTreeDec.getName(), parsedModel.getSystemDefn() == null ? notTreeDec.getStartOrDefault() : null, + Expression.Int(0), null, false); + inTreeNode.add(newVariable); + cIndices[j] = getVarTreeIndexOf(notTreeDec, inTreeNode); + } + } + theModel.nodesWereInserted(inTreeNode, cIndices); + + /* remove variables which are in the tree but not in varInTree or + * varNotInTree */ + ArrayList removeNodes = new ArrayList(); + for (int j = 0; j < inTreeNode.getChildCount(); j++) { + DeclarationNode vNode = (DeclarationNode) inTreeNode.getChildAt(j); + if (!variableExists(vNode, varInTree, varNotInTree)) { + removeNodes.add(vNode); + } + } + Object[] remObj = new Object[removeNodes.size()]; + int[] remInd = new int[removeNodes.size()]; + for (int j = 0; j < removeNodes.size(); j++) { + DeclarationNode vNode = removeNodes.get(j); + int index = inTreeNode.getIndex(vNode); + remObj[j] = vNode; + remInd[j] = index; + } + //remove nodes backwards + for (int j = removeNodes.size() - 1; j >= 0; j--) { + inTreeNode.remove(remInd[j]); + } + theModel.nodesWereRemoved(inTreeNode, remInd, remObj); + } + + //add modules which are not in the tree + for (int i = 0; i < notInTree.size(); i++) { + Module aMod = notInTree.get(i); + ModuleNode newNode = new ModuleNode(aMod.getName(), false); + //add variables to this + for (int j = 0; j < aMod.getNumDeclarations(); j++) { + Declaration aDec = aMod.getDeclaration(j); + + if (aDec.getType() instanceof TypeInt) { + if (aDec.getDeclType() instanceof DeclarationInt) { + DeclarationInt declInt = (DeclarationInt) aDec.getDeclType(); + VarNode newVariable = new VarNode(aDec.getName(), parsedModel.getSystemDefn() == null ? aDec.getStartOrDefault() : null, + declInt.getLow(), declInt.getHigh(), false); + newNode.add(newVariable); + } else { + VarNode newVariable = new VarNode(aDec.getName(), parsedModel.getSystemDefn() == null ? aDec.getStartOrDefault() : null, null, + null, false); + newNode.add(newVariable); + } + } else if (aDec.getType() instanceof TypeBool) { + BoolNode newVariable = new BoolNode(aDec.getName(), parsedModel.getSystemDefn() == null ? aDec.getStartOrDefault() : null, false); + newNode.add(newVariable); + } + if (aDec.getType() instanceof TypeClock) { + VarNode newVariable = new VarNode(aDec.getName(), parsedModel.getSystemDefn() == null ? aDec.getStartOrDefault() : null, + Expression.Int(0), null, false); + newNode.add(newVariable); + } + } + modules.addModule(newNode); + int index = modules.getIndex(newNode); + theModel.nodesWereInserted(modules, new int[] { index }); + } + //remove modules from the tree which are not in either inTree or notInTree + ArrayList removeNodes = new ArrayList(); + for (int i = 0; i < modules.getChildCount(); i++) { + ModuleNode mNode = (ModuleNode) modules.getChildAt(i); + if (!moduleExists(mNode, inTree, notInTree)) { + removeNodes.add(mNode); + } + } + Object[] remObj = new Object[removeNodes.size()]; + int[] remInd = new int[removeNodes.size()]; + for (int i = 0; i < removeNodes.size(); i++) { + ModuleNode mNode = (ModuleNode) removeNodes.get(i); + int index = modules.getIndex(mNode); + remObj[i] = mNode; + remInd[i] = index; + } + //remove nodes backwards + for (int i = removeNodes.size() - 1; i >= 0; i--) { + modules.remove(remInd[i]); + } + theModel.nodesWereRemoved(modules, remInd, remObj); + + //DECLARATIONS + + //If there is no declaration tree, but we need to have declarations, add the tre + if (root.getIndex(declarations) == -1 && parsedModel.getNumGlobals() > 0) { + root.add(declarations); + theModel.nodesWereInserted(root, new int[] { root.getIndex(declarations) }); + } + //If there is a module tree, but no modules, remove the module tree + else if (root.getIndex(declarations) != -1 && parsedModel.getNumGlobals() == 0) { + int index = root.getIndex(declarations); + root.remove(declarations); + theModel.nodesWereRemoved(root, new int[] { index }, new Object[] { declarations }); + } + + /* Create 2 ArrayLists. One of Declarations in the tree and one of declarations + * not in the tree. */ + ArrayList decInTree = new ArrayList(); + ArrayList decNotInTree = new ArrayList(); + + for (int i = 0; i < parsedModel.getNumGlobals(); i++) { + Declaration d = parsedModel.getGlobal(i); + if (declarationIsMember(d)) + decInTree.add(d); + else + decNotInTree.add(d); + } + //make sure declarations in this declaration tree are valid + for (int i = 0; i < decInTree.size(); i++) { + Declaration inTreeDec = decInTree.get(i); + int decIndex = getIndexOfDec(inTreeDec); + DeclarationNode dNode = (DeclarationNode) declarations.getChildAt(decIndex); + if (dNode instanceof GlobalNode) { + GlobalNode vNode = (GlobalNode) declarations.getChildAt(decIndex); + DeclarationInt declInt = (DeclarationInt) inTreeDec.getDeclType(); + vNode.setInitial(parsedModel.getSystemDefn() == null ? inTreeDec.getStartOrDefault() : null); + vNode.setMin(declInt.getLow()); + vNode.setMax(declInt.getHigh()); + theModel.nodesChanged(vNode, new int[] { 0, 1, 2 }); + } else if (dNode instanceof BoolNode) { + BoolNode bNode = (BoolNode) dNode; + bNode.setInitial(parsedModel.getSystemDefn() == null ? inTreeDec.getStartOrDefault() : null); + theModel.nodesChanged(bNode, new int[] { 0 }); + } + + } + + //add declarations in decNotInTree to the tree + int[] cIndices = new int[decNotInTree.size()]; + for (int i = 0; i < decNotInTree.size(); i++) { + Declaration notTreeDec = decNotInTree.get(i); + if (notTreeDec.getType() instanceof TypeInt) { + DeclarationInt declInt = (DeclarationInt) notTreeDec.getDeclType(); + GlobalNode newVariable = new GlobalNode(notTreeDec.getName(), parsedModel.getSystemDefn() == null ? notTreeDec.getStartOrDefault() : null, + declInt.getLow(), declInt.getHigh(), false); + declarations.add(newVariable); + cIndices[i] = getIndexOfDec(notTreeDec); + } else if (notTreeDec.getType() instanceof TypeBool) { + BoolNode newVariable = new BoolNode(notTreeDec.getName(), parsedModel.getSystemDefn() == null ? notTreeDec.getStartOrDefault() : null, + false); + declarations.add(newVariable); + cIndices[i] = getIndexOfDec(notTreeDec); + } + } + theModel.nodesWereInserted(declarations, cIndices); + + /* remove declarations which are in the tree but not in decInTree or + * decNotInTree */ + removeNodes = new ArrayList(); + for (int i = 0; i < declarations.getChildCount(); i++) { + DeclarationNode vNode = (DeclarationNode) declarations.getChildAt(i); + if (!declarationExists(vNode, decInTree, decNotInTree)) { + removeNodes.add(vNode); + } + } + remObj = new Object[removeNodes.size()]; + remInd = new int[removeNodes.size()]; + for (int i = 0; i < removeNodes.size(); i++) { + DeclarationNode vNode = (DeclarationNode) removeNodes.get(i); + int index = declarations.getIndex(vNode); + remObj[i] = vNode; + remInd[i] = index; + } + //remove nodes backwards + for (int i = removeNodes.size() - 1; i >= 0; i--) { + declarations.remove(remInd[i]); + } + theModel.nodesWereRemoved(declarations, remInd, remObj); + + //CONSTANTS + + ConstantList csts = parsedModel.getConstantList(); + //If there is no constant tree, but we need to have constant, add the tre + if (root.getIndex(constants) == -1 && csts.size() > 0) { + root.add(constants); + theModel.nodesWereInserted(root, new int[] { root.getIndex(constants) }); + } + //If there is a constant tree, but no constants, remove the module tree + else if (root.getIndex(constants) != -1 && csts.size() == 0) { + int index = root.getIndex(constants); + root.remove(constants); + theModel.nodesWereRemoved(root, new int[] { index }, new Object[] { constants }); + } + + /* Create 2 ArrayLists. One of Constants in the tree and one of constants + * not in the tree. */ + ArrayList conInTree = new ArrayList(); + ArrayList conNotInTree = new ArrayList(); + + for (int i = 0; i < csts.size(); i++) { + String name = csts.getConstantName(i); + Expression expr = csts.getConstant(i); + Type type = csts.getConstantType(i); + ConstantNode cn; + if (type instanceof TypeBool) { + cn = new BoolConstantNode(name, expr, false); + } else if (type instanceof TypeDouble) { + cn = new DoubleConstantNode(name, expr, false); + } else { + cn = new IntegerConstantNode(name, expr, false); + } + if (constantIsMember(cn)) + conInTree.add(cn); + else + conNotInTree.add(cn); + } + + //make sure constants in this declaration tree are valid + for (int i = 0; i < conInTree.size(); i++) { + ConstantNode inTreeCon = conInTree.get(i); + int conIndex = getIndexOfCon(inTreeCon); + ConstantNode cNode = (ConstantNode) constants.getChildAt(conIndex); + if (cNode instanceof IntegerConstantNode) { + IntegerConstantNode iNode = (IntegerConstantNode) cNode; + + iNode.setName(inTreeCon.getName()); + iNode.setValue(inTreeCon.getValue()); + theModel.nodesChanged(iNode, new int[] { 0 }); + } else if (cNode instanceof BoolConstantNode) { + BoolConstantNode bNode = (BoolConstantNode) cNode; + + bNode.setName(inTreeCon.getName()); + bNode.setValue(inTreeCon.getValue()); + theModel.nodesChanged(bNode, new int[] { 0 }); + } else if (cNode instanceof DoubleConstantNode) { + DoubleConstantNode dNode = (DoubleConstantNode) cNode; + + dNode.setName(inTreeCon.getName()); + dNode.setValue(inTreeCon.getValue()); + theModel.nodesChanged(dNode, new int[] { 0 }); + } + + } + + //add declarations in decNotInTree to the tree + cIndices = new int[conNotInTree.size()]; + for (int i = 0; i < conNotInTree.size(); i++) { + ConstantNode notTreeCon = conNotInTree.get(i); + constants.add(notTreeCon); + cIndices[i] = getIndexOfCon(notTreeCon); + } + theModel.nodesWereInserted(constants, cIndices); + + /* remove declarations which are in the tree but not in decInTree or + * decNotInTree */ + removeNodes = new ArrayList(); + for (int i = 0; i < constants.getChildCount(); i++) { + ConstantNode cNode = (ConstantNode) constants.getChildAt(i); + if (!constantExists(cNode, conInTree, conNotInTree)) { + removeNodes.add(cNode); + } + } + remObj = new Object[removeNodes.size()]; + remInd = new int[removeNodes.size()]; + for (int i = 0; i < removeNodes.size(); i++) { + ConstantNode vNode = (ConstantNode) removeNodes.get(i); + int index = constants.getIndex(vNode); + remObj[i] = vNode; + remInd[i] = index; + } + //remove nodes backwards + for (int i = removeNodes.size() - 1; i >= 0; i--) { + constants.remove(remInd[i]); + } + theModel.nodesWereRemoved(constants, remInd, remObj); + + } else { + String tp = ""; + if (!modelType.getValue().equals(tp)) { + modelType.setUserObject(tp); + theModel.nodeChanged(modelType); + } + } + + if (tree != null) + tree.repaint(); + } + + public boolean moduleExists(ModuleNode mNode, ArrayList inTree, ArrayList outTree) + { + for (int i = 0; i < inTree.size(); i++) { + Module m = inTree.get(i); + if (mNode.getName().equals(m.getName())) { + return true; + } + } + for (int i = 0; i < outTree.size(); i++) { + Module m = outTree.get(i); + if (mNode.getName().equals(m.getName())) { + return true; + } + } + return false; + } + + public boolean variableExists(DeclarationNode vNode, ArrayList inTree, ArrayList outTree) + { + for (int i = 0; i < inTree.size(); i++) { + Declaration d = inTree.get(i); + if (vNode.getName().equals(d.getName())) { + return true; + } + } + for (int i = 0; i < outTree.size(); i++) { + Declaration d = outTree.get(i); + if (vNode.getName().equals(d.getName())) { + return true; + } + } + return false; + } + + public boolean declarationExists(DeclarationNode vNode, ArrayList inTree, ArrayList outTree) + { + for (int i = 0; i < inTree.size(); i++) { + Declaration d = inTree.get(i); + if (vNode.getName().equals(d.getName())) { + return true; + } + } + for (int i = 0; i < outTree.size(); i++) { + Declaration d = outTree.get(i); + if (vNode.getName().equals(d.getName())) { + return true; + } + } + return false; + } + + public boolean constantExists(ConstantNode cNode, ArrayList inTree, ArrayList outTree) + { + for (int i = 0; i < inTree.size(); i++) { + ConstantNode c = inTree.get(i); + if (c.equals(cNode)) + return true; + } + + for (int i = 0; i < outTree.size(); i++) { + ConstantNode c = outTree.get(i); + if (c.equals(cNode)) + return true; + } + return false; + } + + public boolean moduleIsMember(Module aMod) + { + boolean member = false; + for (int i = 0; i < modules.getChildCount(); i++) { + ModuleNode node = (ModuleNode) modules.getChildAt(i); + if (node.getName().equals(aMod.getName())) { + member = true; + break; + } + } + return member; + } + + public boolean declarationIsMember(Declaration d) + { + boolean member = false; + for (int i = 0; i < declarations.getChildCount(); i++) { + DeclarationNode dec = (DeclarationNode) declarations.getChildAt(i); + if (dec.getName().equals(d.getName())) //check same name + { + if (dec instanceof GlobalBoolNode && d.getType() instanceof TypeBool) //check type equality + { + member = true; + break; + } + if (dec instanceof GlobalNode && d.getType() instanceof TypeInt) { + member = true; + break; + } + } + } + return member; + } + + public boolean constantIsMember(ConstantNode n) + { + boolean member = false; + for (int i = 0; i < constants.getChildCount(); i++) { + ConstantNode inC = (ConstantNode) constants.getChildAt(i); + if (inC.equals(n)) { + member = true; + break; + } + } + return member; + } + + public boolean variableIsMember(Declaration d, ModuleNode node) + { + boolean member = false; + for (int i = 0; i < node.getChildCount(); i++) { + DeclarationNode dec = (DeclarationNode) node.getChildAt(i); + if (dec.getName().equals(d.getName())) //check same name + { + if (dec instanceof BoolNode && d.getType() instanceof TypeBool) //check type equality + { + member = true; + break; + } + if (dec instanceof VarNode && d.getType() instanceof TypeInt) { + member = true; + break; + } + } + } + return member; + } + + public int getVarTreeIndexOf(Declaration d, ModuleNode node) + { + int member = -1; + for (int i = 0; i < node.getChildCount(); i++) { + DeclarationNode vNode = (DeclarationNode) node.getChildAt(i); + if (vNode.getName().equals(d.getName())) { + member = i; + break; + } + } + return member; + } + + public int getModuleTreeIndexOf(Module aMod) + { + int member = -1; + for (int i = 0; i < modules.getChildCount(); i++) { + ModuleNode node = (ModuleNode) modules.getChildAt(i); + if (node.getName().equals(aMod.getName())) { + member = i; + break; + } + } + return member; + } + + public int getIndexOfDec(Declaration d) + { + int member = -1; + for (int i = 0; i < declarations.getChildCount(); i++) { + DeclarationNode dec = (DeclarationNode) declarations.getChildAt(i); + if (dec.getName().equals(d.getName())) { + member = i; + break; + } + } + return member; + } + + public int getIndexOfCon(ConstantNode cn) + { + int member = -1; + + for (int i = 0; i < constants.getChildCount(); i++) { + ConstantNode cc = (ConstantNode) constants.getChildAt(i); + if (cc.equals(cn)) { + member = i; + break; + } + } + return member; + } + + private void updateEditable(ModulesFile parsedModel) + { + String fn = handler.getShortActiveFileName(); + if (!root.getUserObject().equals(fn)) { + root.setUserObject("Model: " + fn); + theModel.nodeChanged(root); + } + + if (parsedModel != null) { + if (!modelType.getValue().equals(parsedModel.getType().toString())) { + modelType.setModelType(parsedModel.getModelType()); + } + + //MODULES + + //If there is no module tree, but we need to have modules, add the tre + if (root.getIndex(modules) == -1 && parsedModel.getNumModules() > 0) { + root.add(modules); + theModel.nodesWereInserted(root, new int[] { root.getIndex(modules) }); + } + + /* Create 2 ArrayLists. One of Modules in the tree and one of modules + * not in the tree. */ + ArrayList inTree = new ArrayList(); + ArrayList notInTree = new ArrayList(); + + for (int i = 0; i < parsedModel.getNumModules(); i++) { + Module aMod = parsedModel.getModule(i); + if (moduleIsMember(aMod)) + inTree.add(aMod); + else + notInTree.add(aMod); + } + + //make sure modules in the tree are valid + for (int i = 0; i < inTree.size(); i++) { + Module inTreeMod = inTree.get(i); + int treeIndex = getModuleTreeIndexOf(inTreeMod); //should not be -1 + ModuleNode inTreeNode = (ModuleNode) modules.getChildAt(treeIndex); + + /* Check its variables getting variables which are already there + * and putting them in varInTree, and getting variables which + * are not there and putting them in varNotInTree*/ + ArrayList varInTree = new ArrayList(); + ArrayList varNotInTree = new ArrayList(); + + for (int j = 0; j < inTreeMod.getNumDeclarations(); j++) { + Declaration d = inTreeMod.getDeclaration(j); + if (variableIsMember(d, inTreeNode)) + varInTree.add(d); + else + varNotInTree.add(d); + } + + //make sure variables in this module tree are valid + for (int j = 0; j < varInTree.size(); j++) { + Declaration inTreeDec = varInTree.get(j); + int decIndex = getVarTreeIndexOf(inTreeDec, inTreeNode); + DeclarationNode dNode = (DeclarationNode) inTreeNode.getChildAt(decIndex); + if (dNode instanceof VarNode) { + VarNode vNode = (VarNode) dNode; + DeclarationInt declInt = (DeclarationInt) inTreeDec.getDeclType(); + vNode.setInitial(parsedModel.getSystemDefn() == null ? inTreeDec.getStartOrDefault() : null); + vNode.setMin(declInt.getLow()); + vNode.setMax(declInt.getHigh()); + theModel.nodesChanged(vNode, new int[] { 0, 1, 2 }); + } else if (dNode instanceof BoolNode) { + BoolNode bNode = (BoolNode) dNode; + bNode.setInitial(parsedModel.getSystemDefn() == null ? inTreeDec.getStartOrDefault() : null); + theModel.nodesChanged(bNode, new int[] { 0 }); + } + + } + //add variable in varNotInTree to the tree + int[] cIndices = new int[varNotInTree.size()]; + for (int j = 0; j < varNotInTree.size(); j++) { + Declaration notTreeDec = varNotInTree.get(j); + if (notTreeDec.getType() instanceof TypeInt) { + DeclarationInt declInt = (DeclarationInt) notTreeDec.getDeclType(); + VarNode newVariable = new VarNode(notTreeDec.getName(), parsedModel.getSystemDefn() == null ? notTreeDec.getStartOrDefault() : null, + declInt.getLow(), declInt.getHigh(), false); + inTreeNode.add(newVariable); + cIndices[j] = getVarTreeIndexOf(notTreeDec, inTreeNode); + } else if (notTreeDec.getType() instanceof TypeBool) { + BoolNode newVariable = new BoolNode(notTreeDec.getName(), parsedModel.getSystemDefn() == null ? notTreeDec.getStartOrDefault() : null, + false); + inTreeNode.add(newVariable); + cIndices[j] = getVarTreeIndexOf(notTreeDec, inTreeNode); + } + } + theModel.nodesWereInserted(inTreeNode, cIndices); + + /* remove variables which are in the tree but not in varInTree or + * varNotInTree */ + ArrayList removeNodes = new ArrayList(); + for (int j = 0; j < inTreeNode.getChildCount(); j++) { + DeclarationNode vNode = (DeclarationNode) inTreeNode.getChildAt(j); + if (!variableExists(vNode, varInTree, varNotInTree)) { + removeNodes.add(vNode); + } + } + Object[] remObj = new Object[removeNodes.size()]; + int[] remInd = new int[removeNodes.size()]; + for (int j = 0; j < removeNodes.size(); j++) { + DeclarationNode vNode = removeNodes.get(j); + int index = inTreeNode.getIndex(vNode); + remObj[j] = vNode; + remInd[j] = index; + } + //remove nodes backwards + for (int j = removeNodes.size() - 1; j >= 0; j--) { + inTreeNode.remove(remInd[j]); + } + theModel.nodesWereRemoved(inTreeNode, remInd, remObj); + } + + //add modules which are not in the tree + for (int i = 0; i < notInTree.size(); i++) { + Module aMod = notInTree.get(i); + ModuleNode newNode = new ModuleNode(aMod.getName(), false); + //add variables to this + for (int j = 0; j < aMod.getNumDeclarations(); j++) { + Declaration aDec = aMod.getDeclaration(j); + + if (aDec.getType() instanceof TypeInt) { + DeclarationInt declInt = (DeclarationInt) aDec.getDeclType(); + VarNode newVariable = new VarNode(aDec.getName(), parsedModel.getSystemDefn() == null ? aDec.getStartOrDefault() : null, + declInt.getLow(), declInt.getHigh(), false); + newNode.add(newVariable); + } else if (aDec.getType() instanceof TypeBool) { + BoolNode newVariable = new BoolNode(aDec.getName(), parsedModel.getSystemDefn() == null ? aDec.getStartOrDefault() : null, false); + newNode.add(newVariable); + } + } + modules.addModule(newNode); + int index = modules.getIndex(newNode); + theModel.nodesWereInserted(modules, new int[] { index }); + } + //remove modules from the tree which are not in either inTree or notInTree + ArrayList removeNodes = new ArrayList(); + for (int i = 0; i < modules.getChildCount(); i++) { + ModuleNode mNode = (ModuleNode) modules.getChildAt(i); + if (!mNode.isEditable() && !moduleExists(mNode, inTree, notInTree)) { + removeNodes.add(mNode); + } + } + Object[] remObj = new Object[removeNodes.size()]; + int[] remInd = new int[removeNodes.size()]; + for (int i = 0; i < removeNodes.size(); i++) { + ModuleNode mNode = (ModuleNode) removeNodes.get(i); + int index = modules.getIndex(mNode); + remObj[i] = mNode; + remInd[i] = index; + } + //remove nodes backwards + for (int i = removeNodes.size() - 1; i >= 0; i--) { + modules.remove(remInd[i]); + } + theModel.nodesWereRemoved(modules, remInd, remObj); + + //DECLARATIONS + + //If there is no declaration tree, but we need to have declarations, add the tre + if (root.getIndex(declarations) == -1 && parsedModel.getNumGlobals() > 0) { + root.add(declarations); + theModel.nodesWereInserted(root, new int[] { root.getIndex(declarations) }); + } + + /* Create 2 ArrayLists. One of Declarations in the tree and one of declarations + * not in the tree. */ + ArrayList decInTree = new ArrayList(); + ArrayList decNotInTree = new ArrayList(); + + for (int i = 0; i < parsedModel.getNumGlobals(); i++) { + Declaration d = parsedModel.getGlobal(i); + if (declarationIsMember(d)) + decInTree.add(d); + else + decNotInTree.add(d); + } + + //make sure declarations in this declaration tree are valid + for (int i = 0; i < decInTree.size(); i++) { + Declaration inTreeDec = decInTree.get(i); + int decIndex = getIndexOfDec(inTreeDec); + DeclarationNode dNode = (DeclarationNode) declarations.getChildAt(decIndex); + if (dNode instanceof GlobalNode) { + GlobalNode vNode = (GlobalNode) declarations.getChildAt(decIndex); + DeclarationInt declInt = (DeclarationInt) inTreeDec.getDeclType(); + vNode.setInitial(parsedModel.getSystemDefn() == null ? inTreeDec.getStartOrDefault() : null); + vNode.setMin(declInt.getLow()); + vNode.setMax(declInt.getHigh()); + theModel.nodesChanged(vNode, new int[] { 0, 1, 2 }); + } else if (dNode instanceof GlobalBoolNode) { + GlobalBoolNode bNode = (GlobalBoolNode) dNode; + bNode.setInitial(parsedModel.getSystemDefn() == null ? inTreeDec.getStartOrDefault() : null); + theModel.nodesChanged(bNode, new int[] { 0 }); + } + + } + + //add declarations in decNotInTree to the tree + int[] cIndices = new int[decNotInTree.size()]; + for (int i = 0; i < decNotInTree.size(); i++) { + Declaration notTreeDec = decNotInTree.get(i); + if (notTreeDec.getType() instanceof TypeInt) { + DeclarationInt declInt = (DeclarationInt) notTreeDec.getDeclType(); + GlobalNode newVariable = new GlobalNode(notTreeDec.getName(), parsedModel.getSystemDefn() == null ? notTreeDec.getStartOrDefault() : null, + declInt.getLow(), declInt.getHigh(), false); + declarations.add(newVariable); + cIndices[i] = getIndexOfDec(notTreeDec); + } else if (notTreeDec.getType() instanceof TypeBool) { + GlobalBoolNode newVariable = new GlobalBoolNode(notTreeDec.getName(), parsedModel.getSystemDefn() == null ? notTreeDec.getStartOrDefault() + : null, false); + declarations.add(newVariable); + cIndices[i] = getIndexOfDec(notTreeDec); + } + } + theModel.nodesWereInserted(declarations, cIndices); + + /* remove declarations which are in the tree but not in decInTree or + * decNotInTree */ + removeNodes = new ArrayList(); + for (int i = 0; i < declarations.getChildCount(); i++) { + DeclarationNode vNode = (DeclarationNode) declarations.getChildAt(i); + if (!vNode.isEditable() && !declarationExists(vNode, decInTree, decNotInTree)) { + removeNodes.add(vNode); + } + } + remObj = new Object[removeNodes.size()]; + remInd = new int[removeNodes.size()]; + for (int i = 0; i < removeNodes.size(); i++) { + DeclarationNode vNode = (DeclarationNode) removeNodes.get(i); + int index = declarations.getIndex(vNode); + remObj[i] = vNode; + remInd[i] = index; + } + //remove nodes backwards + for (int i = removeNodes.size() - 1; i >= 0; i--) { + declarations.remove(remInd[i]); + } + theModel.nodesWereRemoved(declarations, remInd, remObj); + + //CONSTANTS + + ConstantList csts = parsedModel.getConstantList(); + //If there is no constant tree, but we need to have constant, add the tre + if (root.getIndex(constants) == -1 && csts.size() > 0) { + root.add(constants); + theModel.nodesWereInserted(root, new int[] { root.getIndex(constants) }); + } + + /* Create 2 ArrayLists. One of Constants in the tree and one of constants + * not in the tree. */ + ArrayList conInTree = new ArrayList(); + ArrayList conNotInTree = new ArrayList(); + + for (int i = 0; i < csts.size(); i++) { + String name = csts.getConstantName(i); + Expression expr = csts.getConstant(i); + Type type = csts.getConstantType(i); + ConstantNode cn; + if (type instanceof TypeBool) { + cn = new BoolConstantNode(name, expr, false); + } else if (type instanceof TypeDouble) { + cn = new DoubleConstantNode(name, expr, false); + } else { + cn = new IntegerConstantNode(name, expr, false); + } + if (constantIsMember(cn)) + conInTree.add(cn); + else + conNotInTree.add(cn); + } + + //make sure constants in this declaration tree are valid + for (int i = 0; i < conInTree.size(); i++) { + ConstantNode inTreeCon = conInTree.get(i); + int conIndex = getIndexOfCon(inTreeCon); + ConstantNode cNode = (ConstantNode) constants.getChildAt(conIndex); + if (cNode instanceof IntegerConstantNode) { + IntegerConstantNode iNode = (IntegerConstantNode) cNode; + + iNode.setName(inTreeCon.getName()); + iNode.setValue(inTreeCon.getValue()); + theModel.nodesChanged(iNode, new int[] { 0 }); + } else if (cNode instanceof BoolConstantNode) { + BoolConstantNode bNode = (BoolConstantNode) cNode; + + bNode.setName(inTreeCon.getName()); + bNode.setValue(inTreeCon.getValue()); + theModel.nodesChanged(bNode, new int[] { 0 }); + } else if (cNode instanceof DoubleConstantNode) { + DoubleConstantNode dNode = (DoubleConstantNode) cNode; + + dNode.setName(inTreeCon.getName()); + dNode.setValue(inTreeCon.getValue()); + theModel.nodesChanged(dNode, new int[] { 0 }); + } + + } + + //add declarations in decNotInTree to the tree + cIndices = new int[conNotInTree.size()]; + for (int i = 0; i < conNotInTree.size(); i++) { + ConstantNode notTreeCon = conNotInTree.get(i); + constants.add(notTreeCon); + cIndices[i] = getIndexOfCon(notTreeCon); + } + theModel.nodesWereInserted(constants, cIndices); + + /* remove declarations which are in the tree but not in decInTree or + * decNotInTree */ + removeNodes = new ArrayList(); + for (int i = 0; i < constants.getChildCount(); i++) { + ConstantNode cNode = (ConstantNode) constants.getChildAt(i); + if (!cNode.isEditable() && !constantExists(cNode, conInTree, conNotInTree)) { + removeNodes.add(cNode); + } + } + remObj = new Object[removeNodes.size()]; + remInd = new int[removeNodes.size()]; + for (int i = 0; i < removeNodes.size(); i++) { + ConstantNode vNode = (ConstantNode) removeNodes.get(i); + int index = constants.getIndex(vNode); + remObj[i] = vNode; + remInd[i] = index; + } + //remove nodes backwards + for (int i = removeNodes.size() - 1; i >= 0; i--) { + constants.remove(remInd[i]); + } + theModel.nodesWereRemoved(constants, remInd, remObj); + + } else { + /*String tp = ""; + if(!modelType.getValue().equals(tp)) + { + modelType.setUserObject(tp); + theModel.nodeChanged(modelType); + }*/ + } + + if (tree != null) + tree.repaint(); + } + + public void lastParseFailed() + { + parseSynchState = TREE_SYNCHRONIZED_BAD; + tree.repaint(); + } + + public void makeNotUpToDate() + { + parseSynchState = TREE_NOT_SYNCHRONIZED; + tree.repaint(); + } + + private void initComponents() + { + tree = new JTree(theModel) + { + public String getToolTipText(MouseEvent event) + { + String ret = null; + TreePath selectedPath = tree.getPathForLocation(event.getX(), event.getY()); + if (selectedPath != null) { + //if(selectedPath.getLastPathComponent() instanceof ModelRootNode) + if (parseSynchState == TREE_SYNCHRONIZED_BAD) + return handler.getParseErrorMessage(); + else if (parseSynchState == TREE_SYNCHRONIZED_GOOD) + return "Model parsed successfully"; + else + return "Model not parsed"; + } + + return ret; + } + + public boolean isPathEditable(TreePath path) + { + Object c = path.getLastPathComponent(); + if (c instanceof ValueNode) { + ValueNode v = (ValueNode) c; + return v.isEditable(); + } + return false; + } + + }; + PrismNodeRenderer prnr = new PrismNodeRenderer(); + tree.setCellRenderer(prnr); + /*JComboBox typeCombo = new JComboBox(new Object[] + {"Probabilistic", "Non-deterministic", "Stochastic"}); + typeCombo.setFont(tree.getFont()); + typeCombo.setBackground(tree.getBackground()); + ValueNodeCellEditor cellEdit = new ValueNodeCellEditor(new JTextField(), typeCombo); + tree.setCellEditor(new DefaultTreeCellEditor(tree, prnr, cellEdit));*/ + tree.setEditable(true); + tree.setCellEditor(new GUIMultiModelTree.ModelTreeCellEditor(tree, prnr)); + + setLayout(new BorderLayout()); + JScrollPane scr = new JScrollPane(); + scr.setViewportView(tree); + add(scr, BorderLayout.CENTER); + + moduleCollectionPopup = new JPopupMenu(); + addModule = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + a_addModule(); + } + }; + addModule.putValue(Action.LONG_DESCRIPTION, "Adds an editable module to the tree"); + addModule.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_A)); + addModule.putValue(Action.NAME, "Add Module"); + moduleCollectionPopup.add(addModule); + + declarationCollectionPopup = new JPopupMenu(); + addIntegerGlobal = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + a_addIntegerGlobal(); + } + }; + addIntegerGlobal.putValue(Action.NAME, "Add Global Integer"); + addBooleanGlobal = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + a_addBooleanGlobal(); + } + }; + addBooleanGlobal.putValue(Action.NAME, "Add Global Boolean"); + declarationCollectionPopup.add(addIntegerGlobal); + declarationCollectionPopup.add(addBooleanGlobal); + + constantsCollectionPopup = new JPopupMenu(); + addIntegerConstant = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + a_addIntegerConstant(); + } + }; + addIntegerConstant.putValue(Action.NAME, "Add Integer Constant"); + addBooleanConstant = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + a_addBooleanConstant(); + } + }; + addBooleanConstant.putValue(Action.NAME, "Add Boolean Constant"); + addDoubleConstant = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + a_addDoubleConstant(); + } + }; + addDoubleConstant.putValue(Action.NAME, "Add Double Constant"); + constantsCollectionPopup.add(addIntegerConstant); + constantsCollectionPopup.add(addBooleanConstant); + constantsCollectionPopup.add(addDoubleConstant); + + modulePopup = new JPopupMenu(); + removeModule = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + if (lastPopNode != null && lastPopNode instanceof ModuleNode) { + a_removeModule((ModuleNode) lastPopNode); + lastPopNode = null; + } + } + }; + removeModule.putValue(Action.NAME, "Remove"); + addBoolean = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + if (lastPopNode != null && lastPopNode instanceof ModuleNode) { + a_addLocalBoolean((ModuleNode) lastPopNode); + lastPopNode = null; + } + + } + }; + addBoolean.putValue(Action.NAME, "Add Boolean Variable"); + addInteger = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + if (lastPopNode != null && lastPopNode instanceof ModuleNode) { + a_addLocalInteger((ModuleNode) lastPopNode); + lastPopNode = null; + } + } + }; + addInteger.putValue(Action.NAME, "Add Integer Variable"); + renameModule = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + if (lastPopNode != null && lastPopNode instanceof ModuleNode) { + a_renameModule((ModuleNode) lastPopNode); + lastPopNode = null; + } + } + }; + renameModule.putValue(Action.NAME, "Rename"); + modulePopup.add(renameModule); + modulePopup.add(removeModule); + //modulePopup.add(new JSplitter()); + modulePopup.add(addInteger); + modulePopup.add(addBoolean); + + declarationPopup = new JPopupMenu(); + removeDeclaration = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + if (lastPopNode != null) { + if (lastPopNode instanceof BoolNode || lastPopNode instanceof VarNode) { + ModuleNode m = whichModule((DeclarationNode) lastPopNode); + if (m != null) + a_removeVariable((DeclarationNode) lastPopNode, m); + } else if (lastPopNode instanceof GlobalNode || lastPopNode instanceof GlobalBoolNode) { + a_removeGlobal((DeclarationNode) lastPopNode); + } else if (lastPopNode instanceof ConstantNode) { + a_removeConstant((ConstantNode) lastPopNode); + } + } + } + }; + removeDeclaration.putValue(Action.NAME, "Remove"); + declarationPopup.add(removeDeclaration); + + renameDeclaration = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + if (lastPopNode != null) { + a_renameDeclaration((DeclarationNode) lastPopNode); + } + } + }; + renameDeclaration.putValue(Action.NAME, "Rename"); + declarationPopup.add(renameDeclaration); + + expressionPopup = new JPopupMenu(); + + editExpression = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + if (lastPopNode != null) { + a_editExpression((ExpressionNode) lastPopNode); + } + } + }; + editExpression.putValue(Action.NAME, "Edit"); + expressionPopup.add(editExpression); + + modelTypePopup = new JPopupMenu(); + + non = new JRadioButton("Non-deterministic (mdp)"); + pro = new JRadioButton("Probabilistic (dtmc)"); + sto = new JRadioButton("Stochastic (ctmc)"); + + ButtonGroup gro = new ButtonGroup(); + gro.add(non); + gro.add(pro); + gro.add(sto); + + non.setSelected(true); + + modelTypePopup.add(non); + modelTypePopup.add(pro); + modelTypePopup.add(sto); + + non.addActionListener(new ActionListener() + { + public void actionPerformed(ActionEvent e) + { + if (non.isSelected()) + a_setModelType(ModelType.MDP); + modelTypePopup.setVisible(false); + } + }); + + pro.addActionListener(new ActionListener() + { + public void actionPerformed(ActionEvent e) + { + if (pro.isSelected()) + a_setModelType(ModelType.DTMC); + modelTypePopup.setVisible(false); + } + }); + + sto.addActionListener(new ActionListener() + { + public void actionPerformed(ActionEvent e) + { + if (sto.isSelected()) + a_setModelType(ModelType.CTMC); + modelTypePopup.setVisible(false); + } + }); + } + + public ModuleNode whichModule(DeclarationNode isIt) + { + for (int i = 0; i < editableModules.size(); i++) { + ModuleNode mod = editableModules.get(i); + int index = mod.getIndex(isIt); + if (index > -1) { + return mod; + } + } + return null; + } + + public void mouseClicked(MouseEvent e) + { + } + + public void mouseEntered(MouseEvent e) + { + } + + public void mouseExited(MouseEvent e) + { + } + + public void mousePressed(MouseEvent e) + { + if (e.isPopupTrigger()) { + lastPopNode = null; + //root popup + if (tree.getClosestPathForLocation(e.getX(), e.getY()).equals(new TreePath(root.getPath()))) { + tree.setSelectionPath(new TreePath(root.getPath())); + //now the root is selected, show the popup + //(diabled for now) + //((GUIMultiModel)(handler.getGUIPlugin())).getPopup().show(tree, e.getX(), e.getY()); + } + //model type node + if (editable && tree.getClosestPathForLocation(e.getX(), e.getY()).equals(new TreePath(modelType.getPath()))) { + tree.setSelectionPath(new TreePath(modelType.getPath())); + modelTypePopup.show(tree, e.getX(), e.getY()); + } + //module collection popup + else if (editable && modules != null && tree.getClosestPathForLocation(e.getX(), e.getY()).equals(new TreePath(modules.getPath()))) { + tree.setSelectionPath(new TreePath(modules.getPath())); + moduleCollectionPopup.show(tree, e.getX(), e.getY()); + } + //declaration collection popup + else if (editable && declarations != null && tree.getClosestPathForLocation(e.getX(), e.getY()).equals(new TreePath(declarations.getPath()))) { + tree.setSelectionPath(new TreePath(declarations.getPath())); + declarationCollectionPopup.show(tree, e.getX(), e.getY()); + } else if (editable && constants != null && tree.getClosestPathForLocation(e.getX(), e.getY()).equals(new TreePath(constants.getPath())))//constant collection node + { + tree.setSelectionPath(new TreePath(constants.getPath())); + constantsCollectionPopup.show(tree, e.getX(), e.getY()); + } else // is the path on a ModuleNode or a DeclarationNode or an ExpressionNode + { + TreePath selectedPath = tree.getClosestPathForLocation(e.getX(), e.getY()); + for (int i = 0; i < editableModules.size(); i++) //search each module + { + ModuleNode mn = editableModules.get(i); + if (new TreePath(mn.getPath()).equals(selectedPath)) { + tree.setSelectionPath(selectedPath); + if (mn.isEditable()) { + modulePopup.show(tree, e.getX(), e.getY()); + lastPopNode = mn; + + if (graphicEditor != null) + graphicEditor.switchModuleView(mn); + } + return; + } + for (int j = 0; j < mn.getChildCount(); j++)//search local variables + { + DeclarationNode dn = (DeclarationNode) mn.getChildAt(j); + if (new TreePath(dn.getPath()).equals(selectedPath)) { + tree.setSelectionPath(selectedPath); + if (dn.isEditable()) { + declarationPopup.show(tree, e.getX(), e.getY()); + lastPopNode = dn; + } + return; + } + } + } + for (int i = 0; i < editableDeclarations.size(); i++)//search globals + { + DeclarationNode dn = editableDeclarations.get(i); + if (new TreePath(dn.getPath()).equals(selectedPath)) { + tree.setSelectionPath(selectedPath); + if (dn.isEditable()) { + declarationPopup.show(tree, e.getX(), e.getY()); + lastPopNode = dn; + } + return; + } + } + for (int i = 0; i < editableConstants.size(); i++)//search constants + { + DeclarationNode dn = editableConstants.get(i); + if (new TreePath(dn.getPath()).equals(selectedPath)) { + tree.setSelectionPath(selectedPath); + if (dn.isEditable()) { + declarationPopup.show(tree, e.getX(), e.getY()); + lastPopNode = dn; + } + return; + } + } + + //Could be an ExpressionNode + if (tree.getSelectionPath() != null) { + TreeNode selectedNode = (TreeNode) tree.getSelectionPath().getLastPathComponent(); + if (selectedNode instanceof ExpressionNode) { + ExpressionNode en = (ExpressionNode) selectedNode; + if (en.isEditable()) { + expressionPopup.show(tree, e.getX(), e.getY()); + lastPopNode = en; + } + } + } + + } + + } else { + TreePath selectedPath = tree.getClosestPathForLocation(e.getX(), e.getY()); + for (int i = 0; i < editableModules.size(); i++) //search each module + { + ModuleNode mn = editableModules.get(i); + if (new TreePath(mn.getPath()).equals(selectedPath)) { + tree.setSelectionPath(selectedPath); + if (graphicEditor != null) + graphicEditor.switchModuleView(mn); + return; + } + } + } + + } + + public void mouseReleased(MouseEvent e) + { + if (e.isPopupTrigger()) { + lastPopNode = null; + //root popup + if (tree.getClosestPathForLocation(e.getX(), e.getY()).equals(new TreePath(root.getPath()))) { + tree.setSelectionPath(new TreePath(root.getPath())); + //now the root is selected, show the popup + //(diabled for now) + //((GUIMultiModel)(handler.getGUIPlugin())).getPopup().show(tree, e.getX(), e.getY()); + } + //model type node + if (editable && tree.getClosestPathForLocation(e.getX(), e.getY()).equals(new TreePath(modelType.getPath()))) { + tree.setSelectionPath(new TreePath(modelType.getPath())); + modelTypePopup.show(tree, e.getX(), e.getY()); + } + //module collection popup + else if (editable && modules != null && tree.getClosestPathForLocation(e.getX(), e.getY()).equals(new TreePath(modules.getPath()))) { + tree.setSelectionPath(new TreePath(modules.getPath())); + moduleCollectionPopup.show(tree, e.getX(), e.getY()); + } + //declaration collection popup + else if (editable && declarations != null && tree.getClosestPathForLocation(e.getX(), e.getY()).equals(new TreePath(declarations.getPath()))) { + tree.setSelectionPath(new TreePath(declarations.getPath())); + declarationCollectionPopup.show(tree, e.getX(), e.getY()); + } else if (editable && constants != null && tree.getClosestPathForLocation(e.getX(), e.getY()).equals(new TreePath(constants.getPath())))//constant collection node + { + tree.setSelectionPath(new TreePath(constants.getPath())); + constantsCollectionPopup.show(tree, e.getX(), e.getY()); + } else // is the path on a ModuleNode or a DeclarationNode or an ExpressionNode + { + TreePath selectedPath = tree.getClosestPathForLocation(e.getX(), e.getY()); + for (int i = 0; i < editableModules.size(); i++) //search each module + { + ModuleNode mn = editableModules.get(i); + if (new TreePath(mn.getPath()).equals(selectedPath)) { + tree.setSelectionPath(selectedPath); + if (mn.isEditable()) { + modulePopup.show(tree, e.getX(), e.getY()); + lastPopNode = mn; + + if (graphicEditor != null) + graphicEditor.switchModuleView(mn); + } + return; + } + for (int j = 0; j < mn.getChildCount(); j++)//search local variables + { + DeclarationNode dn = (DeclarationNode) mn.getChildAt(j); + if (new TreePath(dn.getPath()).equals(selectedPath)) { + tree.setSelectionPath(selectedPath); + if (dn.isEditable()) { + declarationPopup.show(tree, e.getX(), e.getY()); + lastPopNode = dn; + } + return; + } + } + } + for (int i = 0; i < editableDeclarations.size(); i++)//search globals + { + DeclarationNode dn = editableDeclarations.get(i); + if (new TreePath(dn.getPath()).equals(selectedPath)) { + tree.setSelectionPath(selectedPath); + if (dn.isEditable()) { + declarationPopup.show(tree, e.getX(), e.getY()); + lastPopNode = dn; + } + return; + } + } + for (int i = 0; i < editableConstants.size(); i++)//search constants + { + DeclarationNode dn = editableConstants.get(i); + if (new TreePath(dn.getPath()).equals(selectedPath)) { + tree.setSelectionPath(selectedPath); + if (dn.isEditable()) { + declarationPopup.show(tree, e.getX(), e.getY()); + lastPopNode = dn; + } + return; + } + } + + //Could be an ExpressionNode + if (tree.getSelectionPath() != null) { + TreeNode selectedNode = (TreeNode) tree.getSelectionPath().getLastPathComponent(); + if (selectedNode instanceof ExpressionNode) { + ExpressionNode en = (ExpressionNode) selectedNode; + if (en.isEditable()) { + expressionPopup.show(tree, e.getX(), e.getY()); + lastPopNode = en; + } + } + } + + } + + } else { + TreePath selectedPath = tree.getClosestPathForLocation(e.getX(), e.getY()); + for (int i = 0; i < editableModules.size(); i++) //search each module + { + ModuleNode mn = editableModules.get(i); + if (new TreePath(mn.getPath()).equals(selectedPath)) { + tree.setSelectionPath(selectedPath); + if (graphicEditor != null) + graphicEditor.switchModuleView(mn); + return; + } + } + } + + } + + public String getToolTipText() + { + return handler.getParseErrorMessage(); + } + + public ModelType getModelType() + { + return ModelType.valueOf(modelType.getUserObject().toString()); + } + + public String getParseText() + { + int i, j; + String str = ""; + //Header + str += "//Generated by the PRISM Graphic Model Editor\n"; + str += "\n"; + + //Model Type + String type = modelType.getUserObject().toString(); + str += type.toLowerCase() + "\n\n"; + + //Constants + if (constants.getChildCount() != 0) { + str += "//Constants\n\n"; + for (i = 0; i < constants.getChildCount(); i++) { + ConstantNode cn = (ConstantNode) constants.getChildAt(i); + if (cn.isEditable()) + str += cn.getParseText() + "\n"; + } + str += "\n"; + } + + //Globals + if (declarations.getChildCount() != 0) { + str += "//Globals\n\n"; + for (i = 0; i < declarations.getChildCount(); i++) { + DeclarationNode gn = (DeclarationNode) declarations.getChildAt(i); + if (gn.isEditable()) + str += gn.getParseText() + "\n"; + } + str += "\n"; + } + + //Modules + if (modules.getChildCount() != 0) { + str += "//GUI Modules\n\n"; + for (i = 0; i < modules.getChildCount(); i++) { + ModuleNode mn = (ModuleNode) modules.getChildAt(i); + if (mn.isEditable()) { + str += "module " + mn.getName() + "\n"; + for (j = 0; j < mn.getChildCount(); j++) { + DeclarationNode dn = (DeclarationNode) mn.getChildAt(j); + str += TAB + dn.getParseText() + "\n"; + } + + ModuleModel aModuleModel = mn.getModuleModel(); + String stateVar = ((StateVarNode) mn.getChildAt(0)).getName(); + //now add the transition information + for (j = 0; j < aModuleModel.getNumStates(); j++) { + State aState = aModuleModel.getState(j); + if (!aState.getCommentLabel().getString().equals("")) + str += TAB + ("//" + aState.getComment() + "\n"); + for (int k = 0; k < aModuleModel.getNumTransitions(); k++) { + Transition aTrans = aModuleModel.getTransition(k); + if (aTrans.getFrom() == aState) { + if (!(aTrans instanceof ProbTransition || aTrans.getTo() instanceof Decision))// if not branched + { + + String sync = removeCarriages(aTrans.getSyncLabel().getString()); + String guard = removeCarriages(aTrans.getGuardLabel().getString()); + if (!guard.equals("")) + guard = " & (" + guard + ")"; + String assign = removeCarriages(aTrans.getAssignmentLabel().getString()); + if (!assign.equals("")) + assign = " & " + assign + ""; + String prob = removeCarriages(aTrans.getProbabilityLabel().getString()); + int to = aModuleModel.getStateIndex(aTrans.getTo()); + if (prob.equals("") || prob == null) { + str += TAB + + ("[" + sync + "]" + "(" + stateVar + "=" + j + ") " + guard + " -> (" + stateVar + "'=" + to + ")" + assign + + ";" + "\n"); + } else { + str += TAB + + ("[" + sync + "]" + "(" + stateVar + "=" + j + ") " + guard + " -> " + prob + " : (" + stateVar + "'=" + to + + ")" + assign + ";" + "\n"); + } + } else if (aTrans.getTo() instanceof Decision) // if branched + { + String sync = removeCarriages(aTrans.getSyncLabel().getString()); + String guard = removeCarriages(aTrans.getGuardLabel().getString()); + if (!guard.equals("")) + guard = " & (" + guard + ")"; + str += (TAB + "[" + sync + "] (" + stateVar + "=" + j + ") " + guard + " -> "); + Decision dec = (Decision) (aTrans.getTo()); + boolean firstDone = false; + for (int l = 0; l < aModuleModel.getNumTransitions(); l++) { + Transition branch = aModuleModel.getTransition(l); + if (branch.getFrom() == dec) { + ProbTransition pTran = (ProbTransition) branch; + String prob = pTran.getProbabilityLabel().getString(); + int to = aModuleModel.getStateIndex(pTran.getTo()); + String assign = removeCarriages(pTran.getAssignmentLabel().getString()); + if (!assign.equals("")) + assign = " & " + assign + ""; + if (firstDone) + str += ("+ "); + firstDone = true; + str += (prob + " : " + "(" + stateVar + "'=" + to + ")" + assign + " "); + } + } + str += (";\n"); + } + } + } + } + + str += "\n"; + str += "endmodule\n\n"; + } + } + str += "\n"; + + } + //System.out.println("parsed model = "+str); + return str; + } + + public static final String TAB = " "; + + public ArrayList getEditableConstantNames() + { + ArrayList names = new ArrayList(); + for (int i = 0; i < editableConstants.size(); i++) { + DeclarationNode dn = editableConstants.get(i); + names.add(dn.getName()); + } + return names; + } + + public ArrayList getEditableConstantValues() + { + ArrayList values = new ArrayList(); + for (int i = 0; i < editableConstants.size(); i++) { + ConstantNode cn = editableConstants.get(i); + if (cn.getValue() != null) { + if (!cn.getValue().toString().equals("")) { + values.add(cn.getValue().toString()); + } else + values.add(null); + } else + values.add(null); + } + return values; + } + + public ArrayList getEditableConstantTypes() + { + ArrayList types = new ArrayList(); + for (int i = 0; i < editableConstants.size(); i++) { + Object node = editableConstants.get(i); + if (node instanceof BoolConstantNode) { + types.add(TypeBool.getInstance()); + } else if (node instanceof IntegerConstantNode) { + types.add(TypeInt.getInstance()); + } else if (node instanceof DoubleConstantNode) { + types.add(TypeDouble.getInstance()); + } else + types.add(null); + } + return types; + } + + public ArrayList getEditableGlobalNames() + { + ArrayList names = new ArrayList(); + for (int i = 0; i < editableDeclarations.size(); i++) { + DeclarationNode dn = editableDeclarations.get(i); + names.add(dn.getName()); + } + return names; + } + + public ArrayList getEditableGlobalMins() + { + ArrayList mins = new ArrayList(); + for (int i = 0; i < editableDeclarations.size(); i++) { + Object node = editableDeclarations.get(i); + if (node instanceof GlobalNode) { + GlobalNode gn = (GlobalNode) node; + mins.add(gn.getMin().toString()); + } else + mins.add(null); + } + return mins; + } + + public ArrayList getEditableGlobalMaxs() + { + ArrayList maxs = new ArrayList(); + for (int i = 0; i < editableDeclarations.size(); i++) { + Object node = editableDeclarations.get(i); + if (node instanceof GlobalNode) { + GlobalNode gn = (GlobalNode) node; + maxs.add(gn.getMax().toString()); + } else + maxs.add(null); + + } + return maxs; + } + + public ArrayList getEditableGlobalInits() + { + ArrayList inits = new ArrayList(); + for (int i = 0; i < editableDeclarations.size(); i++) { + Object node = editableDeclarations.get(i); + if (node instanceof GlobalNode) { + GlobalNode gn = (GlobalNode) node; + inits.add(gn.getInitial().toString()); + } else if (node instanceof GlobalBoolNode) { + GlobalBoolNode gbn = (GlobalBoolNode) node; + inits.add(gbn.getInitial().toString()); + } + } + return inits; + } + + public ArrayList getEditableGlobalTypes() + { + ArrayList types = new ArrayList(); + for (int i = 0; i < editableDeclarations.size(); i++) { + Object node = editableDeclarations.get(i); + if (node instanceof GlobalBoolNode) { + types.add(TypeBool.getInstance()); + } else if (node instanceof GlobalNode) { + types.add(TypeInt.getInstance()); + } else + types.add(null); + } + return types; + } + + public ArrayList getVariableNames(ModuleNode m) + { + ArrayList names = new ArrayList(); + for (int i = 0; i < m.getChildCount(); i++) { + DeclarationNode vn = (DeclarationNode) m.getChildAt(i); + if (!(vn instanceof StateVarNode)) { + names.add(vn.getName()); + } + } + return names; + } + + public ArrayList getVariableTypes(ModuleNode m) + { + ArrayList types = new ArrayList(); + for (int i = 0; i < m.getChildCount(); i++) { + DeclarationNode dn = (DeclarationNode) m.getChildAt(i); + if (!(dn instanceof StateVarNode)) { + if (dn instanceof BoolNode) + types.add(TypeBool.getInstance()); + else if (dn instanceof VarNode) + types.add(TypeInt.getInstance()); + else + types.add(null); + } + } + return types; + } + + public ArrayList getVariableMins(ModuleNode m) + { + ArrayList mins = new ArrayList(); + for (int i = 0; i < m.getChildCount(); i++) { + DeclarationNode dn = (DeclarationNode) m.getChildAt(i); + if (!(dn instanceof StateVarNode)) { + if (dn instanceof BoolNode) + mins.add(null); + else if (dn instanceof VarNode) { + VarNode vn = (VarNode) dn; + String s = vn.getMin().toString(); + mins.add(s); + } else + mins.add(null); + } + } + return mins; + } + + public ArrayList getVariableMaxs(ModuleNode m) + { + ArrayList maxs = new ArrayList(); + for (int i = 0; i < m.getChildCount(); i++) { + DeclarationNode dn = (DeclarationNode) m.getChildAt(i); + if (!(dn instanceof StateVarNode)) { + if (dn instanceof BoolNode) + maxs.add(null); + else if (dn instanceof VarNode) { + VarNode vn = (VarNode) dn; + String s = vn.getMax().toString(); + maxs.add(s); + } else + maxs.add(null); + } + } + return maxs; + } + + public ArrayList getVariableInits(ModuleNode m) + { + ArrayList inits = new ArrayList(); + for (int i = 0; i < m.getChildCount(); i++) { + DeclarationNode dn = (DeclarationNode) m.getChildAt(i); + if (!(dn instanceof StateVarNode)) { + if (dn instanceof BoolNode) { + BoolNode bn = (BoolNode) dn; + String s = bn.getInitial().toString(); + inits.add(s); + } else if (dn instanceof VarNode) { + VarNode vn = (VarNode) dn; + String s = vn.getInitial().toString(); + inits.add(s); + } else + inits.add(null); + } + } + return inits; + } + + public void updateTooltip() + { + tree.setToolTipText(handler.getParseErrorMessage()); + } + + //Node Data Structure Classes + + interface PrismTreeNode + { + public boolean isEditable(); + } + + class ModelRootNode extends DefaultMutableTreeNode implements PrismTreeNode + { + public ModelRootNode() + { + super("", true); + } + + public boolean isEditable() + { + return false; + } + + } + + class ModuleCollectionNode extends DefaultMutableTreeNode implements PrismTreeNode + { + public ModuleCollectionNode() + { + super("Modules", true); + super.setAllowsChildren(true); + } + + public void addModule(ModuleNode mod) + { + add(mod); + } + + public void removeModule(ModuleNode mod) + { + remove(mod); + } + + public boolean isEditable() + { + return editable; + } + + } + + class DeclarationCollectionNode extends DefaultMutableTreeNode implements PrismTreeNode + { + public DeclarationCollectionNode() + { + super("Global Variables", true); + super.setAllowsChildren(true); + } + + public void addDeclaration(DeclarationNode dec) + { + add(dec); + } + + public void removeDeclaration(DeclarationNode dec) + { + remove(dec); + } + + public boolean isEditable() + { + return editable; + } + + } + + class ConstantCollectionNode extends DefaultMutableTreeNode implements PrismTreeNode + { + public ConstantCollectionNode() + { + super("Constants", true); + } + + public void addConstant(ConstantNode n) + { + add(n); + } + + public void removeConstant(ConstantNode n) + { + remove(n); + } + + public boolean isEditable() + { + return editable; + } + } + + public class ModuleNode extends DefaultMutableTreeNode implements PrismTreeNode + { + private boolean editable; + private ModuleModel moduleModel; + + public ModuleNode(String moduleName, boolean editable) + { + super(moduleName, true); + moduleModel = null; + this.editable = editable; + } + + public void addVariable(VarNode var) + { + add(var); + } + + public void removeVariable(VarNode var) + { + remove(var); + } + + public void setName(String str) + { + setUserObject(str); + } + + public String getName() + { + return (String) getUserObject(); + } + + public boolean isEditable() + { + return editable; + } + + public void setEditable(boolean b) + { + editable = b; + } + + public void setModel(ModuleModel n) + { + moduleModel = n; + } + + public ModuleModel getModuleModel() + { + return moduleModel; + } + + public void childrenChanged() + { + theModel.nodeChanged(this); + theModel.nodeStructureChanged(this); + } + + public boolean isLeaf() + { + return false; + } + + } + + //Editor for ModuleNode + class ModuleEditor extends JTextField implements TreeCellEditor + { + String name; + Vector listeners = new Vector(); + private static final int minWidth = 64; + + public ModuleEditor() + { + super(""); + addActionListener(new ActionListener() + { + public void actionPerformed(ActionEvent as) + { + if (stopCellEditing()) + fireEditingStopped(); + } + }); + } + + public void cancelCellEditing() + { + setText(""); + } + + public boolean stopCellEditing() + { + Expression exp; + String str = getText(); + try { + exp = handler.getGUIPlugin().getPrism().parseSingleExpressionString(str); + } catch (PrismException e) { + return false; + } + if (exp instanceof ExpressionIdent) { + name = str; + return true; + } else { + return false; + } + } + + public Object getCellEditorValue() + { + return name; + } + + public boolean isCellEditable(EventObject eo) + { + if ((eo == null) | ((eo instanceof MouseEvent) && (((MouseEvent) eo).isMetaDown()))) { + return true; + } + return false; + } + + public boolean shouldSelectCell(EventObject eo) + { + return true; + } + + public void removeCellEditroLIstner(CellEditorListener cel) + { + listeners.removeElement(cel); + } + + protected void fireEditingStopped() + { + if (listeners.size() > 0) { + ChangeEvent ce = new ChangeEvent(this); + for (int i = listeners.size() - 1; i >= 0; i--) { + listeners.elementAt(i).editingStopped(ce); + } + + } + } + + //make sure the JTree gives the editor enough space + public void setBounds(Rectangle r) + { + r.width = Math.max(minWidth, r.width); + super.setBounds(r); + } + + public void setBounds(int x, int y, int w, int h) + { + w = Math.max(minWidth, w); + super.setBounds(x, y, w, h); + } + + public void addCellEditorListener(CellEditorListener l) + { + listeners.addElement(l); + } + + public void removeCellEditorListener(CellEditorListener l) + { + listeners.removeElement(l); + } + + public Component getTreeCellEditorComponent(JTree tree, Object value, boolean isSelected, boolean expanded, boolean leaf, int row) + { + return this; + } + + //same listener and bounds methods as above + } + + public static final int LOCAL_INTEGER = 0; + public static final int LOCAL_BOOL = 1; + public static final int GLOBAL_INTEGER = 2; + public static final int GLOBAL_BOOL = 3; + public static final int CONST_INTEGER = 4; + public static final int CONST_BOOL = 5; + public static final int CONST_DOUBLE = 6; + + abstract class DeclarationNode extends DefaultMutableTreeNode implements PrismTreeNode + { + private boolean editable; + private int type; + + public DeclarationNode(int type, String name, boolean editable) + { + super(name, true); + this.editable = editable; + this.type = type; + } + + public boolean getAllowsChildren() + { + return true; + } + + public boolean isLeaf() + { + return false; + } + + public boolean isEditable() + { + return editable; + } + + public String getName() + { + return (String) getUserObject(); + } + + public void setName(String str) + { + setUserObject(str); + } + + public String toString() + { + String name = getName(); + switch (type) { + case LOCAL_INTEGER: + return name; + case GLOBAL_INTEGER: + case CONST_INTEGER: + return name + " : int"; + case LOCAL_BOOL: + case GLOBAL_BOOL: + case CONST_BOOL: + return name + " : bool"; + case CONST_DOUBLE: + return name + " : double"; + default: + return ""; + } + } + + public abstract String getParseText(); + } + + //Editor for DeclarationNode + class DeclarationEditor extends JTextField implements TreeCellEditor + { + String name; + Vector listeners = new Vector(); + private static final int minWidth = 64; + + public DeclarationEditor() + { + super(""); + addActionListener(new ActionListener() + { + public void actionPerformed(ActionEvent as) + { + if (stopCellEditing()) + fireEditingStopped(); + } + }); + } + + public void cancelCellEditing() + { + setText(""); + } + + public boolean stopCellEditing() + { + Expression exp; + String str = getText(); + try { + exp = handler.getGUIPlugin().getPrism().parseSingleExpressionString(str); + } catch (PrismException e) { + return false; + } + if (exp instanceof ExpressionIdent) { + name = str; + return true; + } else { + return false; + } + } + + public Object getCellEditorValue() + { + return name; + } + + public boolean isCellEditable(EventObject eo) + { + if ((eo == null) | ((eo instanceof MouseEvent) && (((MouseEvent) eo).isMetaDown()))) { + return true; + } + return false; + } + + public boolean shouldSelectCell(EventObject eo) + { + return true; + } + + protected void fireEditingStopped() + { + if (listeners.size() > 0) { + ChangeEvent ce = new ChangeEvent(this); + for (int i = listeners.size() - 1; i >= 0; i--) { + listeners.elementAt(i).editingStopped(ce); + } + + } + } + + //make sure the JTree gives the editor enough space + public void setBounds(Rectangle r) + { + r.width = Math.max(minWidth, r.width); + super.setBounds(r); + } + + public void setBounds(int x, int y, int w, int h) + { + w = Math.max(minWidth, w); + super.setBounds(x, y, w, h); + } + + public void addCellEditorListener(CellEditorListener l) + { + listeners.addElement(l); + } + + public void removeCellEditorListener(CellEditorListener l) + { + listeners.addElement(l); + } + + public Component getTreeCellEditorComponent(JTree tree, Object value, boolean isSelected, boolean expanded, boolean leaf, int row) + { + return this; + } + + } + + class VarNode extends DeclarationNode + { + + public VarNode(String name, Expression init, Expression min, Expression max, boolean editable) + { + super(LOCAL_INTEGER, name, editable); + super.add(new ExpressionNode("min: ", min, editable)); + super.add(new ExpressionNode("max: ", max, editable)); + super.add(new ExpressionNode("init: ", init, editable)); + } + + public VarNode(String name, String init, String min, String max, boolean editable) + { + super(LOCAL_INTEGER, name, editable); + try { + Expression e_init = handler.getGUIPlugin().getPrism().parseSingleExpressionString(init); + Expression e_min = handler.getGUIPlugin().getPrism().parseSingleExpressionString(min); + Expression e_max = handler.getGUIPlugin().getPrism().parseSingleExpressionString(max); + super.add(new ExpressionNode("min: ", e_min, editable)); + super.add(new ExpressionNode("max: ", e_max, editable)); + super.add(new ExpressionNode("init: ", e_init, editable)); + } catch (Exception e) { + } + } + + public void setInitial(Expression e) + { + ExpressionNode n = (ExpressionNode) getChildAt(2); + n.setUserObject(e); + theModel.nodeChanged(getChildAt(2)); + } + + public Expression getInitial() + { + ExpressionNode n = (ExpressionNode) getChildAt(2); + return n.getValue(); + } + + public void setMin(Expression e) + { + ExpressionNode n = (ExpressionNode) getChildAt(0); + n.setUserObject(e); + theModel.nodeChanged(getChildAt(0)); + } + + public Expression getMin() + { + ExpressionNode n = (ExpressionNode) getChildAt(0); + return n.getValue(); + } + + public void setMax(Expression e) + { + ExpressionNode n = (ExpressionNode) getChildAt(1); + n.setUserObject(e); + theModel.nodeChanged(getChildAt(1)); + } + + public Expression getMax() + { + ExpressionNode n = (ExpressionNode) getChildAt(1); + return n.getValue(); + } + + public String getParseText() + { + String str = getName() + " : [" + getMin() + ".." + getMax() + "] init " + getInitial() + ";"; + return str; + } + + } + + public class StateVarNode extends VarNode + { + ModuleNode mn; + + public StateVarNode(ModuleNode mn) + { + super("statevariable", "0", "0", "0", false); + this.mn = mn; + } + + public String getName() + { + return mn.getName() + "_s"; + } + } + + class BoolNode extends DeclarationNode + { + public BoolNode(String name, Expression init, boolean editable) + { + super(LOCAL_BOOL, name, editable); + super.add(new ExpressionNode("init: ", init, editable)); + } + + public void setInitial(Expression e) + { + ExpressionNode n = (ExpressionNode) getChildAt(0); + n.setUserObject(e); + } + + public Expression getInitial() + { + ExpressionNode n = (ExpressionNode) getChildAt(0); + return n.getValue(); + } + + public String getParseText() + { + String str = getName() + " : bool init " + getInitial() + ";"; + return str; + } + + } + + class GlobalNode extends DeclarationNode + { + + public GlobalNode(String name, Expression init, Expression min, Expression max, boolean editable) + { + super(GLOBAL_INTEGER, name, editable); + super.add(new ExpressionNode("min: ", min, editable)); + super.add(new ExpressionNode("max: ", max, editable)); + super.add(new ExpressionNode("init: ", init, editable)); + } + + public void setInitial(Expression e) + { + ExpressionNode n = (ExpressionNode) getChildAt(2); + n.setUserObject(e); + } + + public Expression getInitial() + { + ExpressionNode n = (ExpressionNode) getChildAt(2); + return n.getValue(); + } + + public void setMin(Expression e) + { + ExpressionNode n = (ExpressionNode) getChildAt(0); + n.setUserObject(e); + } + + public Expression getMin() + { + ExpressionNode n = (ExpressionNode) getChildAt(0); + return n.getValue(); + } + + public void setMax(Expression e) + { + ExpressionNode n = (ExpressionNode) getChildAt(1); + n.setUserObject(e); + } + + public Expression getMax() + { + ExpressionNode n = (ExpressionNode) getChildAt(1); + return n.getValue(); + } + + public String getParseText() + { + String str = "global " + getName() + " : [" + getMin() + ".." + getMax() + "] init " + getInitial() + ";"; + return str; + } + + } + + class GlobalBoolNode extends DeclarationNode + { + public GlobalBoolNode(String name, Expression init, boolean editable) + { + super(GLOBAL_BOOL, name, editable); + super.add(new ExpressionNode("init: ", init, editable)); + } + + public void setInitial(Expression e) + { + ExpressionNode n = (ExpressionNode) getChildAt(0); + n.setUserObject(e); + } + + public Expression getInitial() + { + ExpressionNode n = (ExpressionNode) getChildAt(0); + return n.getValue(); + } + + public String getParseText() + { + String str = "global " + getName() + " : bool init " + getInitial() + ";"; + return str; + } + + } + + abstract class ConstantNode extends DeclarationNode + { + public ConstantNode(int type, String name, boolean editable) + { + super(type, name, editable); + } + + public abstract void setValue(Expression e); + + public abstract Expression getValue(); + + public boolean equals(Object obj) + { + if (obj instanceof ConstantNode) { + ConstantNode other = (ConstantNode) obj; + if (!other.getName().equals(getName())) + return false; + else + return true; //can only compare the equality of the names + } else + return false; + } + + public abstract String getParseText(); + + } + + class IntegerConstantNode extends ConstantNode + { + public IntegerConstantNode(String name, Expression value, boolean editable) + { + super(CONST_INTEGER, name, editable); + super.add(new ExpressionNode("value: ", value, editable)); + } + + public void setValue(Expression e) + { + ExpressionNode n = (ExpressionNode) getChildAt(0); + n.setUserObject(e); + } + + public Expression getValue() + { + ExpressionNode n = (ExpressionNode) getChildAt(0); + return n.getValue(); + } + + public String getParseText() + { + String str = "const int " + getName(); + if (getValue() != null) { + str += " = " + getValue() + ";"; + } else { + str += ";"; + } + return str; + } + + } + + class DoubleConstantNode extends ConstantNode + { + public DoubleConstantNode(String name, Expression value, boolean editable) + { + super(CONST_DOUBLE, name, editable); + super.add(new ExpressionNode("value: ", value, editable)); + } + + public void setValue(Expression e) + { + ExpressionNode n = (ExpressionNode) getChildAt(0); + n.setUserObject(e); + } + + public Expression getValue() + { + ExpressionNode n = (ExpressionNode) getChildAt(0); + return n.getValue(); + } + + public String getParseText() + { + String str = "const double " + getName(); + if (getValue() != null) { + str += " = " + getValue() + ";"; + } else { + str += ";"; + } + return str; + } + + } + + class BoolConstantNode extends ConstantNode + { + public BoolConstantNode(String name, Expression value, boolean editable) + { + super(CONST_BOOL, name, editable); + super.add(new ExpressionNode("value: ", value, editable)); + } + + public void setValue(Expression e) + { + ExpressionNode n = (ExpressionNode) getChildAt(0); + n.setUserObject(e); + } + + public Expression getValue() + { + ExpressionNode n = (ExpressionNode) getChildAt(0); + return n.getValue(); + } + + public String getParseText() + { + String str = "const bool " + getName(); + if (getValue() != null) { + str += " = " + getValue() + ";"; + } else { + str += ";"; + } + return str; + } + + } + + abstract class ValueNode extends DefaultMutableTreeNode implements PrismTreeNode + { + private String tag; + + public ValueNode(String tag, Object value) + { + super(value); + this.tag = tag; + } + + public String toString() + { + if (getUserObject() == null) + return tag + "?"; + else + return tag + getUserObject().toString(); + } + + public abstract boolean isEditable(); + + public boolean isLeaf() + { + return true; + } + + public void setUserObject(Object obj) + { + super.setUserObject(obj); + } + } + + class StringNode extends ValueNode + { + private boolean editable; + + public StringNode(String tag, String value, boolean editable) + { + super(tag, value); + this.editable = editable; + } + + public boolean isEditable() + { + return editable; + } + + public String getValue() + { + return (String) getUserObject(); + } + + } + + class ExpressionNode extends ValueNode + { + private boolean editable; + + public ExpressionNode(String tag, Expression value, boolean editable) + { + super(tag, value); + this.editable = editable; + } + + public boolean isEditable() + { + return editable; + } + + public Expression getValue() + { + return (Expression) getUserObject(); + } + + public void setValue(Expression value) + { + super.setUserObject(value); + } + + } + + /* + class ExpressionEditor extends javax.swing.DefaultCellEditor + { + Expression exp; + int minWidth = 100; + + public ExpressionEditor() + { + super(new JTextField()); + } + + public Component getComponent() + { + return editorComponent; + } + + public boolean stopCellEditing() + { + String str = ((JTextField)editorComponent).getText(); + + try + { + Expression s = handler.getGUIPlugin().getPrism().parseSingleExpressionString(str); + exp = s; + } + catch(Exception e) + { + handler.getGUIPlugin().message("Error: Syntax Error"); + super.fireEditingStopped(); + return true; + } + super.fireEditingStopped(); + return true; + + } + + public void setBounds(Rectangle r) + { + r.width = Math.max(minWidth, r.width); + getComponent().setBounds(r); + tree.repaint(); + } + + public void setBounds(int x, int y, int w, int h) + { + w = Math.max(minWidth, w); + getComponent().setBounds(x,y,w,h); + tree.repaint(); + } + }*/ + + //Cell edit for ExpressionNode + class ExpressionEditor extends JTextField implements TreeCellEditor + { + Expression exp; + Vector listeners = new Vector(); + private static final int minWidth = 64; + + public ExpressionEditor() + { + super(""); + addActionListener(new ActionListener() + { + public void actionPerformed(ActionEvent as) + { + if (stopCellEditing()) + fireEditingStopped(); + } + }); + } + + public void cancelCellEditing() + { + setText(""); + } + + public boolean stopCellEditing() + { + String str = getText(); + + try { + Expression s = handler.getGUIPlugin().getPrism().parseSingleExpressionString(str); + exp = s; + } catch (Exception e) { + handler.getGUIPlugin().message("Error: Syntax Error"); + return true; + } + return true; + + } + + public Object getCellEditorValue() + { + return exp; + } + + public boolean isCellEditable(EventObject eo) + { + if ((eo == null) | ((eo instanceof MouseEvent) && (((MouseEvent) eo).isMetaDown()))) { + MouseEvent me = (MouseEvent) eo; + if (me.getClickCount() >= 2) { + return true; + } + } + return false; + } + + public boolean shouldSelectCell(EventObject eo) + { + if ((eo == null) | ((eo instanceof MouseEvent) && (((MouseEvent) eo).isMetaDown()))) { + MouseEvent me = (MouseEvent) eo; + if (me.getClickCount() >= 2) { + return true; + } + } + return false; + } + + protected void fireEditingStopped() + { + if (listeners.size() > 0) { + ChangeEvent ce = new ChangeEvent(this); + for (int i = listeners.size() - 1; i >= 0; i--) { + listeners.elementAt(i).editingStopped(ce); + } + + } + } + + //make sure the JTree gives the editor enough space + public void setBounds(Rectangle r) + { + r.width = Math.max(minWidth, r.width); + super.setBounds(r); + tree.repaint(); + } + + public void setBounds(int x, int y, int w, int h) + { + w = Math.max(minWidth, w); + super.setBounds(x, y, w, h); + tree.repaint(); + } + + public void addCellEditorListener(CellEditorListener l) + { + listeners.addElement(l); + } + + public void removeCellEditorListener(CellEditorListener l) + { + listeners.addElement(l); + } + + public Component getTreeCellEditorComponent(JTree tree, Object value, boolean isSelected, boolean expanded, boolean leaf, int row) + { + return this; + } + + } + + class ModelTypeNode extends StringNode + { + public ModelTypeNode(String init, boolean editable) + { + super("Type: ", init, editable); + } + + public void setModelType(ModelType type) + { + setUserObject(type.toString()); + switch (type) { + case MDP: + non.setSelected(true); + break; + case DTMC: + pro.setSelected(true); + break; + case CTMC: + sto.setSelected(true); + break; + } + theModel.nodeChanged(this); + } + + public void setUserObject(Object obj) + { + super.setUserObject(obj); + //System.out.println("setting model type user object "+obj); + + } + } + + //Cell Editor for ModelTypeNode + class ModelTypeEditor extends JComboBox implements TreeCellEditor + { + String value; + Vector listeners = new Vector(); + Object[] list; + + public ModelTypeEditor(Object[] list) + { + super(list); + setFont(tree.getFont()); + setBackground(Color.white); + setForeground(Color.blue); + + this.list = list; + setEditable(false);//why??? + value = list[0].toString(); + + addActionListener(new ActionListener() + { + public void actionPerformed(ActionEvent e) + { + if (stopCellEditing()) + fireEditingStopped(); + } + }); + } + + public void setSelectedType(String str) + { + for (int i = 0; i < list.length; i++) { + String cur = (String) list[i]; + if (cur.equals(str)) { + super.setSelectedIndex(i); + break; + } + } + } + + public void cancelCellEditing() + { + } + + public boolean stopCellEditing() + { + try { + value = (String) getSelectedItem(); + if (value == null) { + value = (String) getItemAt(0); + } + return true; + + } catch (Exception e) { + return false; + } + } + + public Object getCellEditorValue() + { + return value; + } + + public boolean isCellEditable(EventObject eo) + { + if ((eo == null) || ((eo instanceof MouseEvent) && (((MouseEvent) eo).isMetaDown()))) { + MouseEvent me = (MouseEvent) eo; + if (me.getClickCount() >= 2) { + return true; + } + } + return false; + } + + public boolean shouldSelectCell(EventObject eo) + { + if ((eo == null) | ((eo instanceof MouseEvent) && (((MouseEvent) eo).isMetaDown()))) { + MouseEvent me = (MouseEvent) eo; + if (me.getClickCount() >= 2) { + return true; + } + } + return false; + } + + public void addCellEditorListener(CellEditorListener cel) + { + listeners.addElement(cel); + } + + public void removeCellEditorListener(CellEditorListener cel) + { + listeners.removeElement(cel); + } + + protected void fireEditingStopped() + { + if (listeners.size() > 0) { + ChangeEvent ce = new ChangeEvent(this); + for (int i = listeners.size() - 1; i >= 0; i--) { + listeners.elementAt(i).editingStopped(ce); + } + + } + } + + public Component getTreeCellEditorComponent(JTree tree, Object value, boolean isSelected, boolean expanded, boolean leaf, int row) + { + return this; + } + + /* + //make sure the JTree gives the editor enough space + public void setBounds(Rectangle r) + { + r.width = Math.max(minWidth, r.width); + super.setBounds(r); + } + + public void setBounds(int x, int y, int w, int h) + { + w = Math.max(minWidth, w); + super.setBounds(x,y,w,h); + }*/ + + } + + //Node Renderer + class PrismNodeRenderer extends DefaultTreeCellRenderer + { + ImageIcon VAR = GUIPrism.getIconFromImage("smallVariable.png"); + ImageIcon MOD = GUIPrism.getIconFromImage("smallModule.png"); + //ImageIcon EXP = GUIPrism.getIconFromImage("smallExpression.png"); + ImageIcon VAL = GUIPrism.getIconFromImage("smallValue.png"); + ImageIcon GOOD = GUIPrism.getIconFromImage("smallTick.png"); + ImageIcon BAD = GUIPrism.getIconFromImage("smallCross.png"); + ImageIcon OUT_OF_SYNCH = GUIPrism.getIconFromImage("smallFilePrism.png"); + ImageIcon CLOCK = GUIPrism.getIconFromImage("smallClockAnim1.png"); + + public Component getTreeCellRendererComponent(JTree tree, Object value, boolean selected, boolean expanded, boolean leaf, int row, boolean hasFocus) + { + super.getTreeCellRendererComponent(tree, value, selected, expanded, leaf, row, hasFocus); + PrismTreeNode node = (PrismTreeNode) value; + + if (node == root) { + if (isParsing) { + setIcon(animIcon); + } else { + switch (parseSynchState) { + case TREE_SYNCHRONIZED_GOOD: + setIcon(GOOD); + break; + case TREE_SYNCHRONIZED_BAD: + setIcon(BAD); + break; + case TREE_NOT_SYNCHRONIZED: + setIcon(OUT_OF_SYNCH); + break; + } + } + } else if (node instanceof VarNode) { + setIcon(VAR); + } else if (node instanceof BoolNode) { + setIcon(VAR); + } else if (node instanceof DeclarationNode) { + setIcon(VAR); + } else if (node instanceof ModuleNode) { + setIcon(MOD); + } else if (node instanceof ValueNode) { + //if(node instanceof ExpressionNode) + //{ + //setIcon(EXP); + //} + //else + { + setIcon(VAL); + } + } else if (node instanceof ModuleCollectionNode || node instanceof DeclarationCollectionNode || node instanceof ConstantCollectionNode) { + setIcon(this.getDefaultClosedIcon()); + } + if (node.isEditable()) { + setForeground(Color.blue); + } else + setForeground(Color.black); + + return this; + } + } + + class ModelTreeCellEditor extends DefaultTreeCellEditor + { + ModelTypeEditor modelTypeEditor; + ExpressionEditor expressionEditor; + ModuleEditor moduleEditor; + DeclarationEditor declarationEditor; + + String[] types = new String[] { "Non-deterministic", "Probabilistic", "Stochastic" }; + + public ModelTreeCellEditor(JTree tree, PrismNodeRenderer renderer) + { + super(tree, renderer); + modelTypeEditor = new ModelTypeEditor(types); + expressionEditor = new ExpressionEditor(); + moduleEditor = new ModuleEditor(); + declarationEditor = new DeclarationEditor(); + realEditor = declarationEditor; + } + + public Component getTreeCellEditorComponent(JTree tree, Object value, boolean isSelected, boolean expanded, boolean leaf, int row) + { + if (value instanceof ExpressionNode) { + realEditor = expressionEditor; + //((JTextField)expressionEditor.getComponent()).setText(((ExpressionNode)value).getValue().toString()); + } else if (value instanceof ModelTypeNode) { + realEditor = modelTypeEditor; + modelTypeEditor.setSelectedType(((ModelTypeNode) value).getValue()); + //tag = "Type: "; + } else if (value instanceof ModuleNode) { + realEditor = moduleEditor; + moduleEditor.setText(((ModuleNode) value).getName()); + } else if (value instanceof DeclarationNode) { + realEditor = declarationEditor; + declarationEditor.setText(((DeclarationNode) value).getName()); + } + return super.getTreeCellEditorComponent(tree, value, isSelected, expanded, leaf, row); + } + + public void addCellEditorListener(CellEditorListener l) + { + + modelTypeEditor.addCellEditorListener(l); + expressionEditor.addCellEditorListener(l); + + moduleEditor.addCellEditorListener(l); + + declarationEditor.addCellEditorListener(l); + super.addCellEditorListener(l); + } + + public void removeCellEditorListener(CellEditorListener l) + { + modelTypeEditor.removeCellEditorListener(l); + expressionEditor.removeCellEditorListener(l); + + moduleEditor.removeCellEditorListener(l); + + declarationEditor.removeCellEditorListener(l); + super.removeCellEditorListener(l); + } + } + + /* + class ModelTreeCellEditor_n implements TreeCellEditor + { + ModelTypeEditor modelTypeEditor; + ExpressionEditor expressionEditor; + ModuleEditor moduleEditor; + DeclarationEditor declarationEditor; + + CellEditor currentEditor; + + DefaultTreeCellEditor ttt; + + String[] types = new String[] + {"Non-deterministic", "Probabilistic", "Stochastic"}; + + PrismNodeRenderer renderer; + + public ModelTreeCellEditor_n(PrismNodeRenderer renderer) + { + this.renderer = renderer; + modelTypeEditor = new ModelTypeEditor(types); + expressionEditor = new ExpressionEditor(); + moduleEditor = new ModuleEditor(); + declarationEditor = new DeclarationEditor(); + currentEditor = declarationEditor; + } + + + + public Component getTreeCellEditorComponent(JTree tree, Object value, boolean isSelected, boolean expanded, boolean leaf, int row) + { + String tag = ""; + if(value instanceof ExpressionNode) + { + currentEditor = expressionEditor; + // ((JTextField)expressionEditor.getComponent()).setText(((ExpressionNode)value).getValue().toString()); + } + else if(value instanceof ModelTypeNode) + { + currentEditor = modelTypeEditor; + modelTypeEditor.setSelectedType(((ModelTypeNode)value).getValue()); + tag = "Type: "; + } + else if(value instanceof ModuleNode) + { + currentEditor = moduleEditor; + moduleEditor.setText(((ModuleNode)value).getName()); + } + else if(value instanceof DeclarationNode) + { + currentEditor = declarationEditor; + declarationEditor.setText(((DeclarationNode)value).getName()); + } + DefaultTreeCellRenderer c = (DefaultTreeCellRenderer)renderer.getTreeCellRendererComponent(tree, value, isSelected, expanded, leaf, row, true); + JPanel p = new JPanel(); + p.setBackground(Color.white); + p.setLayout(new BorderLayout()); + JLabel l = new JLabel(tag,c.getIcon(), JLabel.HORIZONTAL); + l.setBackground(Color.white); + l.setForeground(Color.blue); + l.setFont(tree.getFont()); + p.add(l, BorderLayout.WEST); + if(currentEditor instanceof ExpressionEditor) + { + p.add(((ExpressionEditor)currentEditor).getComponent(), BorderLayout.CENTER); + } + else + { + p.add((Component)currentEditor, BorderLayout.CENTER); + } + return p;//(Component)currentEditor; + } + + public Object getCellEditorValue() + { + return currentEditor.getCellEditorValue(); + + } + + public boolean isCellEditable(EventObject event) + { + return true; + //return currentEditor.isCellEditable(event); + } + + public boolean shouldSelectCell(EventObject event) + { + return currentEditor.shouldSelectCell(event); + } + + public boolean stopCellEditing() + { + return currentEditor.stopCellEditing(); + } + + public void cancelCellEditing() + { + currentEditor.cancelCellEditing(); + } + + public void addCellEditorListener(CellEditorListener l) + { + + modelTypeEditor.addCellEditorListener(l); + expressionEditor.addCellEditorListener(l); + + moduleEditor.addCellEditorListener(l); + + declarationEditor.addCellEditorListener(l); + } + + public void removeCellEditorListener(CellEditorListener l) + { + modelTypeEditor.removeCellEditorListener(l); + expressionEditor.removeCellEditorListener(l); + + moduleEditor.removeCellEditorListener(l); + + declarationEditor.removeCellEditorListener(l); + } + + } + + */ + + class IconThread extends Thread + { + int index; + ImageIcon[] images; + boolean canContinue = false; + + public IconThread(int index) + { + this.index = index; + images = new ImageIcon[8]; + images[0] = GUIPrism.getIconFromImage("smallClockAnim1.png"); + images[1] = GUIPrism.getIconFromImage("smallClockAnim2.png"); + images[2] = GUIPrism.getIconFromImage("smallClockAnim3.png"); + images[3] = GUIPrism.getIconFromImage("smallClockAnim4.png"); + images[4] = GUIPrism.getIconFromImage("smallClockAnim5.png"); + images[5] = GUIPrism.getIconFromImage("smallClockAnim6.png"); + images[6] = GUIPrism.getIconFromImage("smallClockAnim7.png"); + images[7] = GUIPrism.getIconFromImage("smallClockAnim8.png"); + } + + public void run() + { + try { + int counter = 0; + while (!interrupted() && index > -1) { + counter++; + counter = counter % 8; + animIcon = images[counter]; + tree.repaint(); + sleep(150); + } + } catch (InterruptedException e) { + } + canContinue = true; + } + } + + private static String removeCarriages(String line) + { + String lineBuffer = ""; + for (int i = 0; i < line.length(); i++) { + char c = line.charAt(i); + if (c != '\n') + lineBuffer += c; + else + lineBuffer += " "; + } + return lineBuffer; + } }