From 03864e633b9436e278ab83a10428a3a26642151f Mon Sep 17 00:00:00 2001
From: Ludovic Apvrille <ludovic.apvrille@telecom-paristech.fr>
Date: Tue, 29 Jun 2010 12:48:02 +0000
Subject: [PATCH] Update on AVATAR (new icons, new choice operator at SMD)
 Possibility to select - as an option and in the config.xml file - the port
 number used by the launcher

---
 src/Main.java                                 |  21 ++++++++++++++++--
 src/RTLLauncher.java                          |  16 +++++++++++++
 .../touppaal/AVATAR2UPPAAL.java               |  16 +++++++------
 src/launcher/RshClient.java                   |   9 +++++++-
 src/launcher/RshServer.java                   |   5 ++++-
 src/ui/AvatarDesignPanelTranslator.java       |  10 +++++++++
 src/ui/ConfigurationTTool.java                |  16 +++++++++++++
 src/ui/IconManager.java                       |   4 +++-
 src/ui/MainGUI.java                           |   2 ++
 src/ui/TGComponentManager.java                |   8 ++++++-
 src/ui/TGUIAction.java                        |   6 +++--
 src/ui/avatarsmd/AvatarSMDPanel.java          |  10 ++++-----
 src/ui/avatarsmd/AvatarSMDReceiveSignal.java  |   2 ++
 src/ui/avatarsmd/AvatarSMDSendSignal.java     |   2 ++
 src/ui/avatarsmd/AvatarSMDToolBar.java        |  19 ++++++++++++++--
 src/ui/images/avatarbdcomp.gif                | Bin 95 -> 95 bytes
 src/ui/images/avatarbdlink.gif                | Bin 94 -> 94 bytes
 src/ui/images/avatarblock.gif                 | Bin 108 -> 108 bytes
 src/ui/images/avatardatatype.gif              | Bin 104 -> 104 bytes
 src/ui/images/avatarstate.gif                 | Bin 0 -> 105 bytes
 src/uppaaldesc/UPPAALTemplate.java            |   8 +++++++
 21 files changed, 132 insertions(+), 22 deletions(-)
 create mode 100644 src/ui/images/avatarstate.gif

diff --git a/src/Main.java b/src/Main.java
index 2494ae5e63..435c2ab8a2 100755
--- a/src/Main.java
+++ b/src/Main.java
@@ -103,6 +103,8 @@ public class Main implements ActionListener {
         // setting default language
         splashFrame.setMessage("Setting language");
         Locale.setDefault(new Locale("en"));
+		
+		boolean startLauncher = false;
         
         // Analyzing arguments
         String config = "config.xml";
@@ -120,8 +122,8 @@ public class Main implements ActionListener {
                 System.out.println("LOTOS features activated");
             }
              if (args[i].compareTo("-launcher") == 0) {
-                Thread t = new Thread(new RTLLauncher());
-                t.start();
+				startLauncher = true;
+               
             }
             if (args[i].compareTo("-diplodocus") == 0) {
                 systemc = true;
@@ -199,6 +201,21 @@ public class Main implements ActionListener {
         TraceManager.addDev(ConfigurationTTool.getConfiguration(systemc));
         TraceManager.addDev("\nDebugging trace:\n----------------");
         
+		if (ConfigurationTTool.LauncherPort.length() > 0) {
+			try {
+				int port = Integer.decode(ConfigurationTTool.LauncherPort).intValue();
+				launcher.RshClient.PORT_NUMBER = port;
+				launcher.RshServer.PORT_NUMBER = port;
+				TraceManager.addDev("Port number set to: " + port);
+			} catch (Exception e) {
+				TraceManager.addError("Wrong port number:" + ConfigurationTTool.LauncherPort);
+			}
+		}
+		
+		if (startLauncher) {
+			Thread t = new Thread(new RTLLauncher());
+			t.start();
+		}
         
         // making main window
         splashFrame.setMessage("Creating main window");
diff --git a/src/RTLLauncher.java b/src/RTLLauncher.java
index 5fffc4472e..6ad319de14 100755
--- a/src/RTLLauncher.java
+++ b/src/RTLLauncher.java
@@ -51,6 +51,22 @@ import launcher.*;
 public class RTLLauncher implements Runnable {
     
     public static void main(String[] args) {
+		for(int i=0; i<args.length; i++) {
+			if (args[i].compareTo("-port") == 0) {
+				if (i != (args.length -1)) {
+					try {
+						int port = Integer.decode(args[i+1]).intValue();
+						RshServer.PORT_NUMBER = port;
+						System.out.println("Port number set to " + port);
+					} catch (Exception e) {
+						System.out.println("Wrong port number");
+					}
+					System.out.println("SystemC features activated - these are beta features that are meant to be used only for research purpose");
+				} else {
+					System.out.println("Missing port number");
+				}
+            }
+		}
         System.out.println("Server side of the launcher\nVersion: " + RshServer.VERSION);
         (new RshServer()).startServer();
     }
diff --git a/src/avatartranslator/touppaal/AVATAR2UPPAAL.java b/src/avatartranslator/touppaal/AVATAR2UPPAAL.java
index bd55b38d1f..09030f831a 100755
--- a/src/avatartranslator/touppaal/AVATAR2UPPAAL.java
+++ b/src/avatartranslator/touppaal/AVATAR2UPPAAL.java
@@ -454,7 +454,7 @@ public class AVATAR2UPPAAL {
 					tr = addTransition(_template, loc1, loc1);
 					tmps = CHOICE_VAR + j + " = 0";
 					setAssignment(tr, tmps);
-					tmps = "(" + CHOICE_VAR + j + " < 0) && (h__ >" + CHOICE_VAR + j  + ")";
+					tmps = "(" + CHOICE_VAR + j + " > 0) && (h__ >" + CHOICE_VAR + j  + ")";
 					setGuard(tr, tmps);
 					j ++;
 				}
@@ -809,16 +809,18 @@ public class AVATAR2UPPAAL {
 		
 		while(iterator.hasNext()) {
 			template = (UPPAALTemplate)(iterator.next());
-			dec += template.getName() + "__" + id + " = " + template.getName() + "();\n";
-			system += template.getName() + "__" + id;
-			if (iterator.hasNext()) {
-				system += ",";
-			} else {
-				system += ";";
+			if (template.getNbOfTransitions() > 0) {
+				dec += template.getName() + "__" + id + " = " + template.getName() + "();\n";
+				if (id > 0) {
+					system += ",";
+				}
+				system += template.getName() + "__" + id;
 			}
 			id++;
 		}
 		
+		system += ";";
+		
 		spec.addInstanciation(dec+system);
 	}
 	
diff --git a/src/launcher/RshClient.java b/src/launcher/RshClient.java
index fa00fd9d6b..7b26f77e9f 100755
--- a/src/launcher/RshClient.java
+++ b/src/launcher/RshClient.java
@@ -63,10 +63,11 @@ public class RshClient {
     private static String ID_FAILED = "Wrong id";
     
     private static int BUFSIZE = 511;
+	public static int PORT_NUMBER = 8375;
     
     private String host;
     private String cmd;
-    private static int port = 8375;
+    private int port = PORT_NUMBER;
     private int portString = -1;
     private int portString2 = -1;
     private Socket clientSocket = null;
@@ -78,14 +79,20 @@ public class RshClient {
     private boolean go;
     
     public RshClient(String _cmd, String _host) {
+		//System.out.println("Using port: " + port);
         cmd = _cmd;
         host = _host;
     }
     
     public RshClient(String _host) {
+		//System.out.println("Using port: " + port);
         host = _host;
     }
     
+	public void setPort(int _port) {
+		port = _port;
+	}
+	
     public void setCmd(String _cmd) {
         cmd = _cmd;
     }
diff --git a/src/launcher/RshServer.java b/src/launcher/RshServer.java
index 8f783c996a..d615accbdb 100755
--- a/src/launcher/RshServer.java
+++ b/src/launcher/RshServer.java
@@ -52,7 +52,9 @@ import java.net.*;
 import java.util.*;
 
 public class RshServer {
-    private int port = 8375;
+	public static int PORT_NUMBER = 8375;
+	
+    private int port = PORT_NUMBER;
     private ServerSocket server = null;
     private int id = 0;
     private Vector processes;
@@ -62,6 +64,7 @@ public class RshServer {
     private boolean []sessions = new boolean[10]; // 0 is never used.
 
     public RshServer() {
+		System.out.println("Using port: " + port);
         processes = new Vector();
         try {
             server = new ServerSocket(port);
diff --git a/src/ui/AvatarDesignPanelTranslator.java b/src/ui/AvatarDesignPanelTranslator.java
index 89f87f2d62..46f8d0b753 100644
--- a/src/ui/AvatarDesignPanelTranslator.java
+++ b/src/ui/AvatarDesignPanelTranslator.java
@@ -355,6 +355,8 @@ public class AvatarDesignPanelTranslator {
 		String tmp;
 		TAttribute ta;
 		
+		int choiceID = 0;
+		
 		while(iterator.hasNext()) {
 			tgc = (TGComponent)(iterator.next());
 				
@@ -481,6 +483,14 @@ public class AvatarDesignPanelTranslator {
 				}
 				listE.addCor(astate, tgc);
 			
+				
+			// Choice
+			} else if (tgc instanceof AvatarSMDChoice) {
+				astate = new AvatarState("choice__" + choiceID, tgc);
+				choiceID ++;
+				asm.addElement(astate);
+				listE.addCor(astate, tgc);
+			
 			// Start state
 			} else if (tgc instanceof AvatarSMDStartState) {
 				astart = new AvatarStartState("start", tgc);
diff --git a/src/ui/ConfigurationTTool.java b/src/ui/ConfigurationTTool.java
index 1649aee222..915fabb1f2 100755
--- a/src/ui/ConfigurationTTool.java
+++ b/src/ui/ConfigurationTTool.java
@@ -62,6 +62,7 @@ import myutil.*;
 */
 public class ConfigurationTTool {
     
+	public static String LauncherPort = "";
     public static String RTLHost = "";
     public static String RTLPath = "";
     public static String DTA2DOTPath = "";
@@ -248,6 +249,9 @@ public class ConfigurationTTool {
     
     public static String getConfiguration(boolean systemcOn) {
 		StringBuffer sb = new StringBuffer("");
+		
+		sb.append("Launcher:\n");
+		sb.append("LauncherPort: " + LauncherPort + "\n");
 		// Formal verification
 		sb.append("RTL:\n");
         sb.append("RTLHost: " + RTLHost + "\n");
@@ -346,6 +350,9 @@ public class ConfigurationTTool {
             Document doc = db.parse(bais);
             NodeList nl;
             
+			nl = doc.getElementsByTagName("LauncherPort");
+            if (nl.getLength() > 0)
+                LauncherPort(nl);
             nl = doc.getElementsByTagName("RTLHost");
             if (nl.getLength() > 0)
                 RTLHOST(nl);
@@ -517,6 +524,15 @@ public class ConfigurationTTool {
             throw new MalformedConfigurationException(e.getMessage());
         }
     }
+	
+	private static void LauncherPort(NodeList nl) throws MalformedConfigurationException {
+        try {
+            Element elt = (Element)(nl.item(0));
+            LauncherPort = elt.getAttribute("data");
+        } catch (Exception e) {
+            throw new MalformedConfigurationException(e.getMessage());
+        }
+    }
     
     private static void RTLHOST(NodeList nl) throws MalformedConfigurationException {
         try {
diff --git a/src/ui/IconManager.java b/src/ui/IconManager.java
index 6c06166e2a..602c90c4d8 100755
--- a/src/ui/IconManager.java
+++ b/src/ui/IconManager.java
@@ -139,7 +139,7 @@ public class IconManager {
 	public static ImageIcon imgic5000, imgic5002, imgic5004, imgic5006, imgic5008;
 	public static ImageIcon imgic5010, imgic5012, imgic5014, imgic5016, imgic5018;
 	public static ImageIcon imgic5020, imgic5022, imgic5024, imgic5026, imgic5028;
-	public static ImageIcon imgic5030, imgic5032, imgic5034;
+	public static ImageIcon imgic5030, imgic5032, imgic5034, imgic5036;
 	
 	public static ImageIcon imgic5100, imgic5102, imgic5104;
 	
@@ -501,6 +501,7 @@ public class IconManager {
 	private static String icon5030 = "images/avatarpdtemporalconstraint.gif";
 	private static String icon5032 = "images/avatarpdalias.gif";
 	private static String icon5034 = "images/avatardatatype.gif";
+	private static String icon5036 = "images/avatarstate.gif";
 	
 	private static String icon5100 = "images/avatarhead16.gif";
 	private static String icon5102 = "images/avatarhead32.gif";
@@ -838,6 +839,7 @@ public class IconManager {
 		imgic5030 = getIcon(icon5030);
 		imgic5032 = getIcon(icon5032);
 		imgic5034 = getIcon(icon5034);
+		imgic5036 = getIcon(icon5036);
 		
 		imgic5100 = getIcon(icon5100);
 		imgic5102 = getIcon(icon5102);
diff --git a/src/ui/MainGUI.java b/src/ui/MainGUI.java
index 771530e8ff..a016029497 100755
--- a/src/ui/MainGUI.java
+++ b/src/ui/MainGUI.java
@@ -6081,6 +6081,8 @@ public	class MainGUI implements ActionListener, WindowListener, KeyListener {
             actionOnButton(TGComponentManager.COMPONENT, TGComponentManager.AVATARSMD_PARALLEL);
 		} else if (command.equals(actions[TGUIAction.ASMD_STATE].getActionCommand())) {
             actionOnButton(TGComponentManager.COMPONENT, TGComponentManager.AVATARSMD_STATE);
+		} else if (command.equals(actions[TGUIAction.ASMD_CHOICE].getActionCommand())) {
+            actionOnButton(TGComponentManager.COMPONENT, TGComponentManager.AVATARSMD_CHOICE);
 			
 		// AVATAR RD
 		} else if (command.equals(actions[TGUIAction.ARD_EDIT].getActionCommand())) {
diff --git a/src/ui/TGComponentManager.java b/src/ui/TGComponentManager.java
index 5119a505e0..9f285a4597 100755
--- a/src/ui/TGComponentManager.java
+++ b/src/ui/TGComponentManager.java
@@ -301,6 +301,7 @@ public class TGComponentManager {
 	public static final int AVATARSMD_RECEIVE_SIGNAL = 5104;
 	public static final int AVATARSMD_PARALLEL = 5105;
 	public static final int AVATARSMD_STATE = 5106;
+	public static final int AVATARSMD_CHOICE = 5107;
 	
 	// AVATAR RD -> starts at 5200
 	public static final int AVATARRD_REQUIREMENT = 5200;
@@ -358,6 +359,9 @@ public class TGComponentManager {
                 break;
 			case AVATARSMD_STATE:
                 tgc = new AvatarSMDState(x, y, tdp.getMinX(), tdp.getMaxX(), tdp.getMinY(), tdp.getMaxY(), false, null, tdp);
+                break;
+			case AVATARSMD_CHOICE:
+                tgc = new AvatarSMDChoice(x, y, tdp.getMinX(), tdp.getMaxX(), tdp.getMinY(), tdp.getMaxY(), false, null, tdp);
                 break;
 			case AVATARRD_REQUIREMENT:
                 tgc = new AvatarRDRequirement(x, y, tdp.getMinX(), tdp.getMaxX(), tdp.getMinY(), tdp.getMaxY(), false, null, tdp);
@@ -835,7 +839,9 @@ public class TGComponentManager {
 		} else if (tgc instanceof AvatarSMDParallel) {
 			return AVATARSMD_PARALLEL;		
 		} else if (tgc instanceof AvatarSMDState) {
-			return AVATARSMD_STATE;		
+			return AVATARSMD_STATE;	
+		} else if (tgc instanceof AvatarSMDChoice) {
+			return AVATARSMD_CHOICE;	
 			
 		// AVATAR RD
 		} else if (tgc instanceof AvatarRDRequirement) {
diff --git a/src/ui/TGUIAction.java b/src/ui/TGUIAction.java
index 68791c5d34..70edeaed4a 100755
--- a/src/ui/TGUIAction.java
+++ b/src/ui/TGUIAction.java
@@ -310,6 +310,7 @@ public class TGUIAction extends AbstractAction {
 	public static final int ASMD_RECEIVE_SIGNAL = 297;
 	public static final int ASMD_PARALLEL = 298;
 	public static final int ASMD_STATE = 299;
+	public static final int ASMD_CHOICE = 325;
 	
 	// AVATAR Requirement
 	public static final int ARD_EDIT = 300;
@@ -444,7 +445,7 @@ public class TGUIAction extends AbstractAction {
     //Action for the help button created by Solange
     public static final int PRUEBA_1 = 205;
 
-    public static final int NB_ACTION = 325;
+    public static final int NB_ACTION = 326;
 
     private  static final TAction [] actions = new TAction[NB_ACTION];
     
@@ -839,7 +840,8 @@ public class TGUIAction extends AbstractAction {
         actions[ASMD_SEND_SIGNAL] = new TAction("add-asmd-sendsignal", "Send signal", IconManager.imgic904, IconManager.imgic904, "Send signal", "Add a send signal operator to the currently opened AVATAR state machine diagram", 0);
         actions[ASMD_RECEIVE_SIGNAL] = new TAction("add-asmd-receivesignal", "Receive signal", IconManager.imgic908, IconManager.imgic908, "Receive signal", "Add a receive signal operator to the currently opened AVATAR state machine diagram", 0);
         actions[ASMD_PARALLEL] = new TAction("add-asmd-parallel", "Parallel", IconManager.imgic206, IconManager.imgic206, "Parallel", "Add a parallel operator to the currently opened AVATAR state machine diagram", 0);
-        actions[ASMD_STATE] = new TAction("add-asmd-state", "State", IconManager.imgic204, IconManager.imgic204, "State", "Add a new state to the currently opened AVATAR state machine diagram", 0);
+        actions[ASMD_STATE] = new TAction("add-asmd-state", "State", IconManager.imgic5036, IconManager.imgic5036, "State", "Add a new state to the currently opened AVATAR state machine diagram", 0);
+        actions[ASMD_CHOICE] = new TAction("add-asmd-choice", "Add Choice", IconManager.imgic208, IconManager.imgic208, "Choice", "Add a choice - non-deterministic or guarded - to the currently opened AVATAR state machine diagram", 0);
         
 		// AVATAR Requirement Diagrams
 		actions[ARD_EDIT] = new TAction("edit-ard-diagram", "Edit AVATAR Requirement Diagram", IconManager.imgic100, IconManager.imgic101, "Edit AVATAR Requirement Diagram", "Make it possible to edit the currently opened AVATAR requirement diagram", 0);
diff --git a/src/ui/avatarsmd/AvatarSMDPanel.java b/src/ui/avatarsmd/AvatarSMDPanel.java
index 1738d81b5b..1c178b3686 100755
--- a/src/ui/avatarsmd/AvatarSMDPanel.java
+++ b/src/ui/avatarsmd/AvatarSMDPanel.java
@@ -112,7 +112,7 @@ public class AvatarSMDPanel extends TDiagramPanel {
         // Position correctly guards of choice
     }
     
-    /*public void enhance() {
+    public void enhance() {
         //System.out.println("enhance");
         Vector v = new Vector();
         Object o;
@@ -120,8 +120,8 @@ public class AvatarSMDPanel extends TDiagramPanel {
         
         while(iterator.hasNext()) {
             o = iterator.next();
-            if (o instanceof TMLADStartState){
-                enhance(v, (TMLADStartState)o);
+            if (o instanceof AvatarSMDStartState){
+                enhance(v, (AvatarSMDStartState)o);
             }
         }
         
@@ -147,7 +147,7 @@ public class AvatarSMDPanel extends TDiagramPanel {
         v.add(tgc);
         
         //System.out.println("Nb of nexts: " + tgc.getNbNext());
-        if (!(tgc instanceof TMLADStartState)) {
+        if (!(tgc instanceof AvatarSMDStartState)) {
             for(i=0; i<tgc.getNbNext(); i++) {
                 tgc1 = getNextTGComponent(tgc, i);
                 tgcon = getNextTGConnector(tgc, i);
@@ -164,7 +164,7 @@ public class AvatarSMDPanel extends TDiagramPanel {
             tgc1 = getNextTGComponent(tgc, i);
             enhance(v, tgc1);
         }
-    }*/
+    }
 	
 	public void setConnectorsToFront() {
 		TGComponent tgc;
diff --git a/src/ui/avatarsmd/AvatarSMDReceiveSignal.java b/src/ui/avatarsmd/AvatarSMDReceiveSignal.java
index d2043595b2..e5ad45178e 100644
--- a/src/ui/avatarsmd/AvatarSMDReceiveSignal.java
+++ b/src/ui/avatarsmd/AvatarSMDReceiveSignal.java
@@ -80,6 +80,8 @@ public class AvatarSMDReceiveSignal extends AvatarSMDBasicComponent implements C
         connectingPoint[0] = new AvatarSMDConnectingPoint(this, 0, -lineLength, true, false, 0.5, 0.0);
         connectingPoint[1] = new AvatarSMDConnectingPoint(this, 0, lineLength, false, true, 0.5, 1.0);
         
+		addTGConnectingPointsComment();
+		
         moveable = true;
         editable = true;
         removable = true;
diff --git a/src/ui/avatarsmd/AvatarSMDSendSignal.java b/src/ui/avatarsmd/AvatarSMDSendSignal.java
index b1985d2da8..0f97e83c1c 100644
--- a/src/ui/avatarsmd/AvatarSMDSendSignal.java
+++ b/src/ui/avatarsmd/AvatarSMDSendSignal.java
@@ -80,6 +80,8 @@ public class AvatarSMDSendSignal extends AvatarSMDBasicComponent implements Chec
         connectingPoint[0] = new AvatarSMDConnectingPoint(this, 0, -lineLength, true, false, 0.5, 0.0);
         connectingPoint[1] = new AvatarSMDConnectingPoint(this, 0, lineLength, false, true, 0.5, 1.0);
         
+		addTGConnectingPointsComment();
+		
         moveable = true;
         editable = true;
         removable = true;
diff --git a/src/ui/avatarsmd/AvatarSMDToolBar.java b/src/ui/avatarsmd/AvatarSMDToolBar.java
index ab38fa852f..a5700d13f2 100755
--- a/src/ui/avatarsmd/AvatarSMDToolBar.java
+++ b/src/ui/avatarsmd/AvatarSMDToolBar.java
@@ -62,6 +62,8 @@ public class AvatarSMDToolBar extends TToolBar {
     protected void setActive(boolean b) {
         mgui.actions[TGUIAction.ASMD_EDIT].setEnabled(b);
         mgui.actions[TGUIAction.UML_NOTE].setEnabled(b);
+		mgui.actions[TGUIAction.CONNECTOR_COMMENT].setEnabled(b);
+		
         mgui.actions[TGUIAction.ASMD_CONNECTOR].setEnabled(b);
         mgui.actions[TGUIAction.ASMD_START].setEnabled(b);
         mgui.actions[TGUIAction.ASMD_STOP].setEnabled(b);
@@ -69,6 +71,9 @@ public class AvatarSMDToolBar extends TToolBar {
         mgui.actions[TGUIAction.ASMD_RECEIVE_SIGNAL].setEnabled(b);
 		mgui.actions[TGUIAction.ASMD_PARALLEL].setEnabled(b);
 		mgui.actions[TGUIAction.ASMD_STATE].setEnabled(b);
+		mgui.actions[TGUIAction.ASMD_CHOICE].setEnabled(b);
+		
+		mgui.actions[TGUIAction.ACT_ENHANCE].setEnabled(b);
 		
 		mgui.actions[TGUIAction.ACT_ZOOM_MORE].setEnabled(false);
 		mgui.actions[TGUIAction.ACT_ZOOM_LESS].setEnabled(false);
@@ -86,11 +91,16 @@ public class AvatarSMDToolBar extends TToolBar {
         
         button = this.add(mgui.actions[TGUIAction.UML_NOTE]);
         button.addMouseListener(mgui.mouseHandler);
+		
+		button = this.add(mgui.actions[TGUIAction.CONNECTOR_COMMENT]);
+        button.addMouseListener(mgui.mouseHandler);
+        
         
         this.addSeparator();
         
 		button = this.add(mgui.actions[TGUIAction.ASMD_CONNECTOR]);
         button.addMouseListener(mgui.mouseHandler);
+		
         
         this.addSeparator();
         
@@ -105,6 +115,11 @@ public class AvatarSMDToolBar extends TToolBar {
 		button = this.add(mgui.actions[TGUIAction.ASMD_STATE]);
         button.addMouseListener(mgui.mouseHandler);
 		
+		this.addSeparator();
+		
+		button = this.add(mgui.actions[TGUIAction.ASMD_CHOICE]);
+        button.addMouseListener(mgui.mouseHandler);
+		
 		/*this.addSeparator();
 		
 		button = this.add(mgui.actions[TGUIAction.ASMD_PARALLEL]);
@@ -119,12 +134,12 @@ public class AvatarSMDToolBar extends TToolBar {
         button.addMouseListener(mgui.mouseHandler);
         
         
-        /*this.addSeparator();
+        this.addSeparator();
         
         button = this.add(mgui.actions[TGUIAction.ACT_ENHANCE]);
         button.addMouseListener(mgui.mouseHandler);
 		
-		this.addSeparator();
+		/*this.addSeparator();
 		
 		button = this.add(mgui.actions[TGUIAction.ACT_TOGGLE_INTERNAL_COMMENT]);
         button.addMouseListener(mgui.mouseHandler);
diff --git a/src/ui/images/avatarbdcomp.gif b/src/ui/images/avatarbdcomp.gif
index 2dd19f56edb722d7c045a5ac0a45dc5c62c67d55..8e3aa154b082195eb44835fbebbe4807fc9e0c2a 100644
GIT binary patch
delta 31
mcma!#mvr}Zv#?C$XAodm$jkr)2XB2mcmLO%JBubtx&Z)>M+<-e

delta 31
lcma!#mvr}Zv#?C$XAodm$jkr)4O`BhyZ`I||Nj#u-2jcI3)lbv

diff --git a/src/ui/images/avatarbdlink.gif b/src/ui/images/avatarbdlink.gif
index be9b21f4545d161e4f14bd39ac39f0ea72009fcd..e7c626de03145e809eae5c2027917a2200115c70 100644
GIT binary patch
delta 31
mcma!xlXUlVv#?C$XAodm$jkr)2XB2mcmLO%JBubtx&i=?2@8Dy

delta 31
lcma!xlXUlVv#?C$XAodm$jkr)4O`BhyZ`I||Nj#uT>*_~3)KJs

diff --git a/src/ui/images/avatarblock.gif b/src/ui/images/avatarblock.gif
index d2dfefb8adcf23cdfe7e205a7472348f96630274..330963443bdeb448d412d44d06f770aa7b18ddf4 100644
GIT binary patch
delta 31
kcmd1Fk#zTTv#?C$XAodm$ix5y2XB2mcmEd<O_U4<0F?I(GXMYp

delta 31
lcmd1Fk#zTTv#?C$XAodm$jkr)4O`BhyZ`I||Nj#ug8`7t3;zHB

diff --git a/src/ui/images/avatardatatype.gif b/src/ui/images/avatardatatype.gif
index aaa2a1265ea0bd872072e248f1e66fe605ac114c..db9c0cc34a5a401911ba232c8bbec61de4fea019 100644
GIT binary patch
delta 31
kcmd1EkaYKSv#?C$XAodm$ix5ybM7oUcmEd<O_cNp0FOfpwEzGB

delta 31
lcmd1EkaYKSv#?C$XAodm$jkr)xd$(uyZ`I||Nj#u{Q-}$3-SN}

diff --git a/src/ui/images/avatarstate.gif b/src/ui/images/avatarstate.gif
new file mode 100644
index 0000000000000000000000000000000000000000..8c5d27643d9e128d03f2d7429733613e9e9c93d5
GIT binary patch
literal 105
zcmZ?wbhEHb<Yy3ISjfZx1P5<@Ja_*W5Gnp-VPs%nX3znNg5(*PtmgF3Y*@o~q%%K2
zL;S{^^Rg{TI~<k77l;&WQqkPG#QV4|Z}caN^t<~7Q`nk10y1P?O<CG{VP$}v5i5f=
E05&frRR910

literal 0
HcmV?d00001

diff --git a/src/uppaaldesc/UPPAALTemplate.java b/src/uppaaldesc/UPPAALTemplate.java
index e11a130bb0..46e0916819 100755
--- a/src/uppaaldesc/UPPAALTemplate.java
+++ b/src/uppaaldesc/UPPAALTemplate.java
@@ -64,6 +64,14 @@ public class UPPAALTemplate {
 		transitions = new LinkedList();
     }
 	
+	public int getNbOfLocations() {
+		return locations.size();
+	}
+	
+	public int getNbOfTransitions() {
+		return transitions.size();
+	}
+	
 	public void setIdInstanciation(int _idInstanciation) {
 		idInstanciation = _idInstanciation;
 	}
-- 
GitLab