diff --git a/src/main/java/common/ConfigurationTTool.java b/src/main/java/common/ConfigurationTTool.java
index 4fa1b7fa9d825a3b92394b05ac2c3c4c7d089cb6..d0840dc99a196040a2dba7a641c24be10c2fdb3b 100755
--- a/src/main/java/common/ConfigurationTTool.java
+++ b/src/main/java/common/ConfigurationTTool.java
@@ -36,13 +36,8 @@
* knowledge of the CeCILL license and that you accept its terms.
*/
-
-
-
package common;
-//import java.awt.*;
-
import myutil.FileUtils;
import myutil.MalformedConfigurationException;
import myutil.TraceManager;
@@ -58,8 +53,6 @@ import java.io.ByteArrayInputStream;
import java.io.File;
import java.io.FileOutputStream;
-//import org.xml.sax.*;
-
/**
* Class ConfigurationTTool
@@ -116,6 +109,12 @@ public class ConfigurationTTool {
public static String UPPAALCodeDirectory = "";
public static String UPPAALVerifierPath = "";
public static String UPPAALVerifierHost = "";
+
+ // Issue #35: UPPAAL change in property verification message
+ public static String UPPAALPropertyVerifMessage = "";
+ public static String UPPAALPropertyNotVerifMessage = "";
+
+
public static String ProVerifCodeDirectory = "";
public static String ProVerifVerifierPath = "";
public static String ProVerifVerifierHost = "";
@@ -200,7 +199,7 @@ public class ConfigurationTTool {
}
public static void saveConfiguration() throws MalformedConfigurationException {
- int index0, index1, index2, index3;
+ int index0, index1, index2;//, index3;
String tmp, tmp1, tmp2, location;
File f = new File(fileName);
boolean write = false;
@@ -375,6 +374,13 @@ public class ConfigurationTTool {
sb.append("\nUPPAAL:\n");
sb.append("UPPAALCodeDirectory: " + UPPAALCodeDirectory + "\n");
sb.append("UPPAALVerifierPATH: " + UPPAALVerifierPath + "\n");
+ sb.append("UPPAALVerifierHOST: " + UPPAALVerifierHost + "\n");
+
+ // Issue #35
+ sb.append("UPPAALPropertyVerifMessage: " + UPPAALPropertyVerifMessage + "\n");
+ sb.append("UPPAALPropertyNotVerifMessage: " + UPPAALPropertyNotVerifMessage + "\n");
+
+
sb.append("AVATARCPPSIMCompileCommand: " + AVATARCPPSIMCompileCommand + "\n");
sb.append("AVATARCPPSIMCodeExecuteCommand: " + AVATARCPPSIMCodeExecuteCommand + "\n");
sb.append("AVATARCPPSIMInteractiveExecuteCommand: " + AVATARCPPSIMInteractiveExecuteCommand + "\n");
@@ -383,7 +389,9 @@ public class ConfigurationTTool {
sb.append("\nAVATAR (simulation):\n");
sb.append("AVATARSimulationHost: " + AVATARSimulationHost + "\n");
sb.append("AVATARCPPSIMCodeDirectory: " + AVATARCPPSIMCodeDirectory + "\n");
- sb.append("UPPAALVerifierHOST: " + UPPAALVerifierHost + "\n");
+
+ // Issue #35: Moved with other UPPAAL properties
+// sb.append("UPPAALVerifierHOST: " + UPPAALVerifierHost + "\n");
// AVATAR: executable code
sb.append("\nAVATAR (executable code):\n");
@@ -702,6 +710,16 @@ public class ConfigurationTTool {
if (nl.getLength() > 0)
UPPAALVerifierHost(nl);
+ nl = doc.getElementsByTagName("UPPAALPropertyVerifMessage");
+ if (nl.getLength() > 0) {
+ UPPAALPropertyVerifMessage(nl);
+ }
+
+ nl = doc.getElementsByTagName("UPPAALPropertyNotVerifMessage");
+ if (nl.getLength() > 0) {
+ UPPAALPropertyNotVerifMessage(nl);
+ }
+
nl = doc.getElementsByTagName("ProVerifCodeDirectory");
if (nl.getLength() > 0)
ProVerifCodeDirectory(nl);
@@ -1213,6 +1231,24 @@ public class ConfigurationTTool {
}
}
+ private static void UPPAALPropertyVerifMessage(NodeList nl) throws MalformedConfigurationException {
+ try {
+ Element elt = (Element)(nl.item(0));
+ UPPAALPropertyVerifMessage = elt.getAttribute("data");
+ } catch (Exception e) {
+ throw new MalformedConfigurationException(e.getMessage());
+ }
+ }
+
+ private static void UPPAALPropertyNotVerifMessage(NodeList nl) throws MalformedConfigurationException {
+ try {
+ Element elt = (Element)(nl.item(0));
+ UPPAALPropertyNotVerifMessage = elt.getAttribute("data");
+ } catch (Exception e) {
+ throw new MalformedConfigurationException(e.getMessage());
+ }
+ }
+
private static void AVATARSimulationHost(NodeList nl) throws MalformedConfigurationException {
try {
Element elt = (Element)(nl.item(0));
diff --git a/src/main/java/launcher/ExecutionThread.java b/src/main/java/launcher/ExecutionThread.java
index 048f9b7f690dbaba74f3bf621dc5d07697a82ea3..e0e364a4584b750e3c2796e260bf0874c2fc5011 100755
--- a/src/main/java/launcher/ExecutionThread.java
+++ b/src/main/java/launcher/ExecutionThread.java
@@ -46,6 +46,8 @@ import myutil.TraceManager;
import java.io.*;
import java.net.ServerSocket;
import java.net.Socket;
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
/**
@@ -56,7 +58,10 @@ import java.net.Socket;
* @author Ludovic APVRILLE
*/
class ExecutionThread extends Thread {
- private final String cmd;
+ private static final String ERROR_KEY = "error=";
+ private static final Pattern ERROR_PATTERN = Pattern.compile( ".*(" + ERROR_KEY + "\\d+,).*" );
+
+ private final String cmd;
private final int port;
private final RshServer rsh;
private ServerSocket server;// = null;
@@ -86,6 +91,7 @@ class ExecutionThread extends Thread {
rsh = _rsh;
server = null;
go = true;
+ sendReturnCode = false;
returnCode = null;
mustWaitForPiped = false;
parentExecThread = null;
@@ -217,9 +223,9 @@ class ExecutionThread extends Thread {
}
}
- private void respond( final PrintStream out,
- final ResponseCode code,
- final String message ) {
+ private void respond( final PrintStream out,
+ final ResponseCode code,
+ final String message ) {
SocketComHelper.send( out, code, message);
//try {
//out.println( co de.name() + message );
@@ -228,13 +234,52 @@ class ExecutionThread extends Thread {
// }
}
+ /**
+ * Issue #35: Handle the case where the executable to be run does not exists or is not accessible
+ * @param ex
+ * @param out
+ * @throws InterruptedException
+ */
+ private void handleReturnCode( final IOException ex,
+ final PrintStream out )
+ throws InterruptedException {
+ if ( ex.getMessage() == null ) {
+ returnCode = - 1;
+ }
+ else {
+ returnCode = parseErrorCode( ex.getMessage() );
+ }
+
+ final String message = "Error executing command " + cmd + " with return code " + returnCode + ".";
+ TraceManager.addError( message );
+ respond( out, ResponseCode.PROCESS_OUTPUT, message );
+ respond( out, ResponseCode.PROCESS_OUTPUT, ex.getMessage() );
+ respond( out, ResponseCode.PROCESS_END, null );//"5");
+ }
+
+ private Integer parseErrorCode( final String message ) {
+ final Matcher matcher = ERROR_PATTERN.matcher( message );
+
+ if ( matcher.matches() ) {
+ if ( matcher.groupCount() > 1 ) {
+ final String expr = matcher.group( 1 );
+ final String errorNum = expr.substring( ERROR_KEY.length(), expr.length() - 1 );
+
+ return Integer.decode( errorNum );
+ }
+ }
+
+ return -1;
+ }
+
private void handleReturnCode( PrintStream out )
- throws InterruptedException {
+ throws InterruptedException {
if ( sendReturnCode ) {
returnCode = proc.waitFor();
final String message = "Ended command " + cmd + " with return code " + returnCode + ".";
TraceManager.addDev( message );
respond( out, ResponseCode.PROCESS_OUTPUT, message );
+ respond( out, ResponseCode.PROCESS_END, null );//"5");
}
else {
returnCode = null;
@@ -316,33 +361,39 @@ class ExecutionThread extends Thread {
// TraceManager.addDev("Going to start command " + cmd + "..." );
final PrintStream out = new PrintStream( s.getOutputStream(), true );
- proc = Runtime.getRuntime().exec(cmd);
-
- if ( parentExecThread != null ) {
- // TraceManager.addDev( "Giving my pipe to the other..." );
- parentExecThread.setMyPipe( proc.getOutputStream() );
- }
-
- proc_in = new BufferedReader( new InputStreamReader( proc.getInputStream() ) );
- String str;
-
- //TraceManager.addDev("Reading the output stream of the process " + cmd);
- while ( go && ( str = proc_in.readLine() ) != null ) {
- // TraceManager.addDev( "Sending " + str + " from " + port + " to client..." );
- respond( out, ResponseCode.PROCESS_OUTPUT, str );
- }
-
- proc_err = new BufferedReader(new InputStreamReader(proc.getErrorStream()));
-
- while ( go && ( str = proc_err.readLine() ) != null ) {
- TraceManager.addError( str );
- respond( out, ResponseCode.PROCESS_OUTPUT_ERROR, str );
+ try {
+ proc = Runtime.getRuntime().exec(cmd);
+
+ if ( parentExecThread != null ) {
+ // TraceManager.addDev( "Giving my pipe to the other..." );
+ parentExecThread.setMyPipe( proc.getOutputStream() );
+ }
+
+ proc_in = new BufferedReader( new InputStreamReader( proc.getInputStream() ) );
+ String str;
+
+ //TraceManager.addDev("Reading the output stream of the process " + cmd);
+ while ( go && ( str = proc_in.readLine() ) != null ) {
+ // TraceManager.addDev( "Sending " + str + " from " + port + " to client..." );
+ respond( out, ResponseCode.PROCESS_OUTPUT, str );
+ }
+
+ proc_err = new BufferedReader(new InputStreamReader(proc.getErrorStream()));
+
+ while ( go && ( str = proc_err.readLine() ) != null ) {
+ TraceManager.addError( str );
+ respond( out, ResponseCode.PROCESS_OUTPUT_ERROR, str );
+ }
+
+ handleReturnCode( out );
}
-
- handleReturnCode( out );
-
- if ( s != null ) {
- closeConnect( s );
+ catch ( final IOException ex ) {
+ handleReturnCode( ex, out );
+ }
+ finally {
+ if ( s != null ) {
+ closeConnect( s );
+ }
}
}
}
diff --git a/src/main/java/myutil/ScrolledJTextArea.java b/src/main/java/myutil/ScrolledJTextArea.java
index f0e9a8834b51f49c132095ecb1cb6027044b70cd..fef77e32e3908b2a42bc9cec2d892c1f1dcccb24 100755
--- a/src/main/java/myutil/ScrolledJTextArea.java
+++ b/src/main/java/myutil/ScrolledJTextArea.java
@@ -36,9 +36,6 @@
* knowledge of the CeCILL license and that you accept its terms.
*/
-
-
-
package myutil;
@@ -47,7 +44,7 @@ import javax.swing.*;
/**
* Class ScrolledJTextArea
- * For scrolling a textarea in xhich text is appended
+ * For scrolling a textarea in which text is appended
* Creation: 2005
* @version 1.1 09/03/2005
* @author Ludovic APVRILLE
diff --git a/src/main/java/ui/TGUIAction.java b/src/main/java/ui/TGUIAction.java
index 2869df6e7976f650ecaafb917fdf6555226da6fe..c6cd59ee3bcf0314ba660850d492e1c8a24fe530 100755
--- a/src/main/java/ui/TGUIAction.java
+++ b/src/main/java/ui/TGUIAction.java
@@ -720,8 +720,11 @@ public class TGUIAction extends AbstractAction {
actions[ACT_GEN_LOTOS] = new TAction("gen_lotos-command", "Generate LOTOS", IconManager.imgic90, IconManager.imgic90, "Generate LOTOS specification", "Generates a LOTOS specification from TTool diagrams", '0');
actions[ACT_ONECLICK_LOTOS_RG] = new TAction("gen_rglotos-command", "One-click LOTOS-based verification", IconManager.imgic342, IconManager.imgic342, "One-click LOTOS-based verification", "Generates a LOTOS-based RG from TTool diagrams", '0');
actions[ACT_ONECLICK_RTLOTOS_RG] = new TAction("gen_rgrtlotos-command", "Generate RT-LOTOS-based RG", IconManager.imgic342, IconManager.imgic342, "Generate RT-LOTOS-based RG ", "Generates an RT-LOTOS-based RG from TTool diagrams", '0');
- actions[ACT_GEN_UPPAAL] = new TAction("gen_uppaal-command", "Safety formal verification with UPPAAL", IconManager.imgic86, IconManager.imgic86, "Generate UPPAAL specification", "Generates a UPPAAL specification from TTool diagrams", '0');
- actions[ACT_AVATAR_MODEL_CHECKER] = new TAction("avatar-model-checker", "Avatar model checker", IconManager.imgic140, IconManager.imgic140, "Avatar model checker", "Executes the AVATAR model checker from an AVATAR design", '0');
+
+ // Issue #35: Renamed action name to be closer to actual functionality
+ actions[ACT_GEN_UPPAAL] = new TAction("gen_uppaal-command", "Formal Verification with UPPAAL", IconManager.imgic86, IconManager.imgic86, "Formal Verification with UPPAAL", "Formal verification of TTool diagrams with UPPAAL", '0');
+
+ actions[ACT_AVATAR_MODEL_CHECKER] = new TAction("avatar-model-checker", "Avatar model checker", IconManager.imgic140, IconManager.imgic140, "Avatar model checker", "Executes the AVATAR model checker from an AVATAR design", '0');
actions[ACT_GEN_JAVA] = new TAction("gen_java-command", "Generate JAVA", IconManager.imgic38, IconManager.imgic39, "Generate JAVA", "Generates Java code from TURTLE diagrams", 0);
actions[ACT_SIMU_JAVA] = new TAction("gen_simujava-command", "Java-based simulation", IconManager.imgic38, IconManager.imgic39, "JAVA-based simualtion", "Simulate diagrams using Java language", 0);
//@author: Huy TRUONG
diff --git a/src/main/java/ui/window/JDialogUPPAALValidation.java b/src/main/java/ui/window/JDialogUPPAALValidation.java
index 3f26530e17dc88735dfb0baeff8c2e30588082ac..045b68225e96792270352049fa11af593859a028 100755
--- a/src/main/java/ui/window/JDialogUPPAALValidation.java
+++ b/src/main/java/ui/window/JDialogUPPAALValidation.java
@@ -36,31 +36,52 @@
* knowledge of the CeCILL license and that you accept its terms.
*/
-
-
-
package ui.window;
+import java.awt.BorderLayout;
+import java.awt.Container;
+import java.awt.Cursor;
+import java.awt.Dimension;
+import java.awt.Font;
+import java.awt.Frame;
+import java.awt.GridBagConstraints;
+import java.awt.GridBagLayout;
+import java.awt.Insets;
+import java.awt.event.ActionEvent;
+import java.awt.event.ActionListener;
+import java.util.Collection;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.Hashtable;
+import java.util.LinkedList;
+import java.util.Map;
+
+import javax.swing.JButton;
+import javax.swing.JCheckBox;
+import javax.swing.JLabel;
+import javax.swing.JPanel;
+import javax.swing.JScrollPane;
+import javax.swing.JTextArea;
+import javax.swing.JTextField;
+
import avatartranslator.AvatarBlock;
import avatartranslator.AvatarSpecification;
import avatartranslator.touppaal.AVATAR2UPPAAL;
+import common.ConfigurationTTool;
import launcher.LauncherException;
import launcher.RshClient;
import myutil.FileException;
import myutil.FileUtils;
import myutil.ScrolledJTextArea;
import myutil.TraceManager;
-import ui.*;
+import ui.MainGUI;
+import ui.TGComponent;
+import ui.TGComponentAndUPPAALQuery;
+import ui.TURTLEPanel;
import ui.util.IconManager;
import uppaaldesc.UPPAALSpec;
import uppaaldesc.UPPAALTemplate;
-import javax.swing.*;
-import java.awt.*;
-import java.awt.event.ActionEvent;
-import java.awt.event.ActionListener;
-import java.util.*;
-
/**
* Class JDialogUPPAALValidation
* Dialog for managing the syntax analysis of LOTOS specifications
@@ -69,7 +90,34 @@ import java.util.*;
* @author Ludovic APVRILLE
*/
public class JDialogUPPAALValidation extends javax.swing.JDialog implements ActionListener, Runnable {
- private static boolean deadlockAChecked/*, deadlockEChecked*/, generateTraceChecked, customChecked, stateAChecked, stateEChecked, stateLChecked, showDetailsChecked, translateChecked;
+
+ // Issue #35: Handle the different output message labels of different versions of UPPAAL
+ private static final java.util.Set<String> PROP_VERIFIED_LABELS = new HashSet<String>();
+ private static final java.util.Set<String> PROP_NOT_VERIFIED_LABELS = new HashSet<String>();
+
+ static {
+ for ( final String label : ConfigurationTTool.UPPAALPropertyVerifMessage.split( "," ) ) {
+ PROP_VERIFIED_LABELS.add( label.trim() );
+ }
+
+ // Handle the case where nothing is defined in the configuration
+ if ( PROP_VERIFIED_LABELS.isEmpty() ) {
+ PROP_VERIFIED_LABELS.add( "Property is satisfied" );
+ PROP_VERIFIED_LABELS.add( "Formula is satisfied" );
+ }
+
+ for ( final String label : ConfigurationTTool.UPPAALPropertyNotVerifMessage.split( "," ) ) {
+ PROP_NOT_VERIFIED_LABELS.add( label.trim() );
+ }
+
+ // Handle the case where nothing is defined in the configuration
+ if ( PROP_NOT_VERIFIED_LABELS.isEmpty() ) {
+ PROP_NOT_VERIFIED_LABELS.add( "Property is NOT satisfied" );
+ PROP_NOT_VERIFIED_LABELS.add( "Formula is NOT satisfied" );
+ }
+ }
+
+ private static boolean deadlockAChecked/*, deadlockEChecked*/, generateTraceChecked, customChecked, stateAChecked, stateEChecked, stateLChecked, showDetailsChecked;//, translateChecked;
protected MainGUI mgui;
@@ -87,7 +135,9 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
protected final static int STOPPED = 3;
//components
+
protected JTextArea jta;
+
protected JButton start;
protected JButton stop;
protected JButton close;
@@ -99,10 +149,8 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
protected TURTLEPanel tp;
protected java.util.List<JCheckBox> customChecks;
protected boolean hasFiniteSize;
- protected static String sizeInfiniteFIFO = "8";
+// protected static String sizeInfiniteFIFO = "8";
protected JTextField sizeOfInfiniteFIFO;
-
-
protected java.util.List<String> customQueries;
public Map<String, Integer> verifMap;
@@ -143,118 +191,118 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
}
protected void initComponents() {
- int index = spec.indexOf("DEFAULT_INFINITE_SIZE");
- String size = "1024";
- hasFiniteSize = (index > -1);
- if (hasFiniteSize) {
- String subspec = spec.substring(index+24, spec.length());
- int indexEnd = subspec.indexOf(";");
- //TraceManager.addDev("indexEnd = " + indexEnd + " subspec=" + subspec);
- if (indexEnd == -1) {
- hasFiniteSize = false;
- } else {
- size = subspec.substring(0, indexEnd);
- TraceManager.addDev("size=" + size);
- }
- }
-
- Container c = getContentPane();
- setFont(new Font("Helvetica", Font.PLAIN, 14));
- c.setLayout(new BorderLayout());
- //setDefaultCloseOperation(JFrame.DISPOSE_ON_CLOSE);
-
- JPanel jp1 = new JPanel();
- GridBagLayout gridbag1 = new GridBagLayout();
- GridBagConstraints c1 = new GridBagConstraints();
- jp1.setLayout(gridbag1);
- jp1.setBorder(new javax.swing.border.TitledBorder("Verify with UPPAAL: options"));
- //jp1.setPreferredSize(new Dimension(300, 150));
-
- // first line panel1
- //c1.gridwidth = 3;
- c1.gridheight = 3;
- c1.weighty = 1.0;
- c1.weightx = 1.0;
- c1.gridwidth = GridBagConstraints.REMAINDER; //end row
- c1.fill = GridBagConstraints.BOTH;
- c1.gridheight = 1;
-
- /*deadlockE = new JCheckBox("Search for absence of deadock situations");
+ int index = spec.indexOf("DEFAULT_INFINITE_SIZE");
+ String size = "1024";
+ hasFiniteSize = (index > -1);
+ if (hasFiniteSize) {
+ String subspec = spec.substring(index+24, spec.length());
+ int indexEnd = subspec.indexOf(";");
+ //TraceManager.addDev("indexEnd = " + indexEnd + " subspec=" + subspec);
+ if (indexEnd == -1) {
+ hasFiniteSize = false;
+ } else {
+ size = subspec.substring(0, indexEnd);
+ TraceManager.addDev("size=" + size);
+ }
+ }
+
+ Container c = getContentPane();
+ setFont(new Font("Helvetica", Font.PLAIN, 14));
+ c.setLayout(new BorderLayout());
+ //setDefaultCloseOperation(JFrame.DISPOSE_ON_CLOSE);
+
+ JPanel jp1 = new JPanel();
+ GridBagLayout gridbag1 = new GridBagLayout();
+ GridBagConstraints c1 = new GridBagConstraints();
+ jp1.setLayout(gridbag1);
+ jp1.setBorder(new javax.swing.border.TitledBorder("Verify with UPPAAL: options"));
+ //jp1.setPreferredSize(new Dimension(300, 150));
+
+ // first line panel1
+ //c1.gridwidth = 3;
+ c1.gridheight = 3;
+ c1.weighty = 1.0;
+ c1.weightx = 1.0;
+ c1.gridwidth = GridBagConstraints.REMAINDER; //end row
+ c1.fill = GridBagConstraints.BOTH;
+ c1.gridheight = 1;
+
+ /*deadlockE = new JCheckBox("Search for absence of deadock situations");
deadlockE.addActionListener(this);
jp1.add(deadlockE, c1);
deadlockE.setSelected(deadlockEChecked);*/
- JPanel jp01 = new JPanel();
- GridBagLayout gridbag01 = new GridBagLayout();
- GridBagConstraints c01 = new GridBagConstraints();
- jp01.setLayout(gridbag01);
- jp01.setBorder(new javax.swing.border.TitledBorder("Options of UPPAAL Specification"));
-
-
- // first line panel01
- //c1.gridwidth = 3;
-
- c01.gridheight = 1;
- c01.weighty = 1.0;
- c01.weightx = 1.0;
- c01.gridwidth = GridBagConstraints.REMAINDER; //end row
- c01.fill = GridBagConstraints.BOTH;
- c01.gridheight = 1;
-
-
- sizeOfInfiniteFIFO = new JTextField(size, 10);
- c01.gridwidth = 1;
- jp01.add(new JLabel("Size of infinite FIFO = "), c01);
- c01.gridwidth = GridBagConstraints.REMAINDER; //end row
- jp01.add(sizeOfInfiniteFIFO, c01);
- jp1.add(jp01, c1);
-
- c1.gridheight = 1;
-
-
- deadlockA = new JCheckBox("Search for absence of deadock situations");
- deadlockA.addActionListener(this);
- jp1.add(deadlockA, c1);
- deadlockA.setSelected(deadlockAChecked);
-
- stateE = new JCheckBox("Reachability of selected states");
- stateE.addActionListener(this);
- stateE.setToolTipText("Study the fact that a given state may be reachable i.e. in at least one path");
- jp1.add(stateE, c1);
- stateE.setSelected(stateEChecked);
-
- stateA = new JCheckBox("Liveness of selected states");
- stateA.addActionListener(this);
- stateA.setToolTipText("Study the fact that a given state is always reachable i.e. in all paths");
- jp1.add(stateA, c1);
- stateA.setSelected(stateAChecked);
-
- stateL = new JCheckBox("Leads to");
- stateL.addActionListener(this);
- stateL.setToolTipText("Study the fact that, if accessed, a given state is eventually followed by another one");
- jp1.add(stateL, c1);
- stateL.setSelected(stateLChecked);
- c1.gridwidth = GridBagConstraints.REMAINDER;
- custom = new JCheckBox("Custom verification");
- custom.addActionListener(this);
- jp1.add(custom, c1);
- custom.setSelected(customChecked);
- if (customQueries != null) {
- for (String s: customQueries){
- c1.gridwidth = GridBagConstraints.RELATIVE;
- JLabel space = new JLabel(" ");
- c1.weightx=0.0;
- jp1.add(space, c1);
- c1.gridwidth = GridBagConstraints.REMAINDER; //end row
- JCheckBox cqb = new JCheckBox(s);
- cqb.addActionListener(this);
- c1.weightx=1.0;
- jp1.add(cqb, c1);
- customChecks.add(cqb);
-
- }
- }
- /* jp1.add(new JLabel("Custom formula to translate = "), c1);
+ JPanel jp01 = new JPanel();
+ GridBagLayout gridbag01 = new GridBagLayout();
+ GridBagConstraints c01 = new GridBagConstraints();
+ jp01.setLayout(gridbag01);
+ jp01.setBorder(new javax.swing.border.TitledBorder("Options of UPPAAL Specification"));
+
+
+ // first line panel01
+ //c1.gridwidth = 3;
+
+ c01.gridheight = 1;
+ c01.weighty = 1.0;
+ c01.weightx = 1.0;
+ c01.gridwidth = GridBagConstraints.REMAINDER; //end row
+ c01.fill = GridBagConstraints.BOTH;
+ c01.gridheight = 1;
+
+
+ sizeOfInfiniteFIFO = new JTextField(size, 10);
+ c01.gridwidth = 1;
+ jp01.add(new JLabel("Size of infinite FIFO = "), c01);
+ c01.gridwidth = GridBagConstraints.REMAINDER; //end row
+ jp01.add(sizeOfInfiniteFIFO, c01);
+ jp1.add(jp01, c1);
+
+ c1.gridheight = 1;
+
+
+ deadlockA = new JCheckBox("Search for absence of deadock situations");
+ deadlockA.addActionListener(this);
+ jp1.add(deadlockA, c1);
+ deadlockA.setSelected(deadlockAChecked);
+
+ stateE = new JCheckBox("Reachability of selected states");
+ stateE.addActionListener(this);
+ stateE.setToolTipText("Study the fact that a given state may be reachable i.e. in at least one path");
+ jp1.add(stateE, c1);
+ stateE.setSelected(stateEChecked);
+
+ stateA = new JCheckBox("Liveness of selected states");
+ stateA.addActionListener(this);
+ stateA.setToolTipText("Study the fact that a given state is always reachable i.e. in all paths");
+ jp1.add(stateA, c1);
+ stateA.setSelected(stateAChecked);
+
+ stateL = new JCheckBox("Leads to");
+ stateL.addActionListener(this);
+ stateL.setToolTipText("Study the fact that, if accessed, a given state is eventually followed by another one");
+ jp1.add(stateL, c1);
+ stateL.setSelected(stateLChecked);
+ c1.gridwidth = GridBagConstraints.REMAINDER;
+ custom = new JCheckBox("Custom verification");
+ custom.addActionListener(this);
+ jp1.add(custom, c1);
+ custom.setSelected(customChecked);
+ if (customQueries != null) {
+ for (String s: customQueries){
+ c1.gridwidth = GridBagConstraints.RELATIVE;
+ JLabel space = new JLabel(" ");
+ c1.weightx=0.0;
+ jp1.add(space, c1);
+ c1.gridwidth = GridBagConstraints.REMAINDER; //end row
+ JCheckBox cqb = new JCheckBox(s);
+ cqb.addActionListener(this);
+ c1.weightx=1.0;
+ jp1.add(cqb, c1);
+ customChecks.add(cqb);
+
+ }
+ }
+ /* jp1.add(new JLabel("Custom formula to translate = "), c1);
c1.gridwidth = GridBagConstraints.REMAINDER; //end row
customText = new JTextField("Type your CTL formulae here!", 80);
customText.addActionListener(this);
@@ -269,54 +317,55 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
translatedText = new JTextField("Translated CTL formula here", 80);
customText.addActionListener(this);
jp1.add(translatedText,c1);
- */
- generateTrace = new JCheckBox("Generate simulation trace");
- generateTrace.addActionListener(this);
- jp1.add(generateTrace, c1);
- generateTrace.setSelected(generateTraceChecked);
-
- showDetails = new JCheckBox("Show verification details");
- showDetails.addActionListener(this);
- jp1.add(showDetails, c1);
- showDetails.setSelected(showDetailsChecked);
-
- jp1.setMinimumSize(jp1.getPreferredSize());
- c.add(jp1, BorderLayout.NORTH);
-
- jta = new ScrolledJTextArea();
- jta.setEditable(false);
- jta.setMargin(new Insets(10, 10, 10, 10));
- jta.setTabSize(3);
- jta.append("Select options and then, click on 'start' to start generation of RG\n");
- Font f = new Font("Courrier", Font.BOLD, 12);
- jta.setFont(f);
- JScrollPane jsp = new JScrollPane(jta, JScrollPane.VERTICAL_SCROLLBAR_ALWAYS, JScrollPane.HORIZONTAL_SCROLLBAR_ALWAYS);
-
- c.add(jsp, BorderLayout.CENTER);
-
- start = new JButton("Start", IconManager.imgic53);
- stop = new JButton("Stop", IconManager.imgic55);
- close = new JButton("Close", IconManager.imgic27);
- eraseAll = new JButton("Del", IconManager.imgic337);
-
- start.setPreferredSize(new Dimension(100, 30));
- stop.setPreferredSize(new Dimension(100, 30));
- close.setPreferredSize(new Dimension(110, 30));
- eraseAll.setPreferredSize(new Dimension(100, 30));
-
- start.addActionListener(this);
- stop.addActionListener(this);
- close.addActionListener(this);
- eraseAll.addActionListener(this);
-
- JPanel jp2 = new JPanel();
- jp2.add(start);
- jp2.add(stop);
- jp2.add(close);
- jp2.add(eraseAll);
- c.add(jp2, BorderLayout.SOUTH);
+ */
+ generateTrace = new JCheckBox("Generate simulation trace");
+ generateTrace.addActionListener(this);
+ jp1.add(generateTrace, c1);
+ generateTrace.setSelected(generateTraceChecked);
+
+ showDetails = new JCheckBox("Show verification details");
+ showDetails.addActionListener(this);
+ jp1.add(showDetails, c1);
+ showDetails.setSelected(showDetailsChecked);
+
+ jp1.setMinimumSize(jp1.getPreferredSize());
+ c.add(jp1, BorderLayout.NORTH);
+
+ jta = new ScrolledJTextArea();
+ jta.setEditable(false);
+ jta.setMargin(new Insets(10, 10, 10, 10));
+ jta.setTabSize(3);
+ jta.append("Select options and then, click on 'start' to start generation of RG\n");
+ Font f = new Font("Courrier", Font.BOLD, 12);
+ jta.setFont(f);
+ JScrollPane jsp = new JScrollPane(jta, JScrollPane.VERTICAL_SCROLLBAR_ALWAYS, JScrollPane.HORIZONTAL_SCROLLBAR_ALWAYS);
+
+ c.add(jsp, BorderLayout.CENTER);
+
+ start = new JButton("Start", IconManager.imgic53);
+ stop = new JButton("Stop", IconManager.imgic55);
+ close = new JButton("Close", IconManager.imgic27);
+ eraseAll = new JButton("Del", IconManager.imgic337);
+
+ start.setPreferredSize(new Dimension(100, 30));
+ stop.setPreferredSize(new Dimension(100, 30));
+ close.setPreferredSize(new Dimension(110, 30));
+ eraseAll.setPreferredSize(new Dimension(100, 30));
+
+ start.addActionListener(this);
+ stop.addActionListener(this);
+ close.addActionListener(this);
+ eraseAll.addActionListener(this);
+
+ JPanel jp2 = new JPanel();
+ jp2.add(start);
+ jp2.add(stop);
+ jp2.add(close);
+ jp2.add(eraseAll);
+ c.add(jp2, BorderLayout.SOUTH);
}
+ @Override
public void actionPerformed(ActionEvent evt) {
String command = evt.getActionCommand();
@@ -365,25 +414,24 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
}
public void startProcess() {
- // hack spec if necessary.
-
- if (hasFiniteSize) {
- try {
- int sizeDef = Integer.decode(sizeOfInfiniteFIFO.getText()).intValue();
- int index = spec.indexOf("DEFAULT_INFINITE_SIZE");
- String specEnd = spec.substring(index+24, spec.length());
- String specbeg = spec.substring(0, index+24);
- specbeg += sizeDef;
- specEnd = specEnd.substring(specEnd.indexOf(";"), specEnd.length());
- spec = specbeg + specEnd;
- } catch (Exception e) {
+ // hack spec if necessary.
+
+ if (hasFiniteSize) {
+ try {
+ int sizeDef = Integer.decode(sizeOfInfiniteFIFO.getText()).intValue();
+ int index = spec.indexOf("DEFAULT_INFINITE_SIZE");
+ String specEnd = spec.substring(index+24, spec.length());
+ String specbeg = spec.substring(0, index+24);
+ specbeg += sizeDef;
+ specEnd = specEnd.substring(specEnd.indexOf(";"), specEnd.length());
+ spec = specbeg + specEnd;
+ } catch (Exception e) {
jta.append("Non valid size for infinite FIFO");
jta.append("Using default size");
-
}
-
- //TraceManager.addDev("spec=" + spec);
- }
+
+ //TraceManager.addDev("spec=" + spec);
+ }
t = new Thread(this);
mode = STARTED;
@@ -391,7 +439,7 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
t.start();
}
-
+ @Override
public void run() {
// String cmd1 = "";
@@ -430,7 +478,8 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
}
if (stateE.isSelected()&& (mode != NOT_STARTED)) {
- ArrayList<TGComponentAndUPPAALQuery> list = mgui.gtm.getUPPAALQueries(tp);
+ java.util.List<TGComponentAndUPPAALQuery> list = mgui.gtm.getUPPAALQueries(tp);
+
if ((list != null) && (list.size() > 0)){
for(TGComponentAndUPPAALQuery cq: list) {
String s = cq.uppaalQuery;
@@ -464,7 +513,7 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
}
if (stateA.isSelected() && (mode != NOT_STARTED)) {
- ArrayList<TGComponentAndUPPAALQuery> list = mgui.gtm.getUPPAALQueries(tp);
+ java.util.List<TGComponentAndUPPAALQuery> list = mgui.gtm.getUPPAALQueries(tp);
if ((list != null) && (list.size() > 0)){
for(TGComponentAndUPPAALQuery cq: list) {
if (cq.tgc != null) {
@@ -495,7 +544,7 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
}
}
if (stateL.isSelected() && (mode != NOT_STARTED)) {
- ArrayList<TGComponentAndUPPAALQuery> list = mgui.gtm.getUPPAALQueries(tp);
+ java.util.List<TGComponentAndUPPAALQuery> list = mgui.gtm.getUPPAALQueries(tp);
String s1, s2, name1, name2, query1, query2;
int index1, index2;
if ((list != null) && (list.size() > 0)){
@@ -574,6 +623,7 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
jta.append(le.getMessage() + "\n");
mode = NOT_STARTED;
setButtons();
+
try{
if (rshctmp != null) {
rshctmp.freeId(id);
@@ -581,7 +631,7 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
} catch (LauncherException le1) {}
return;
} catch (Exception e) {
- TraceManager.addError("Exception: " + e.getMessage());
+ TraceManager.addError( e );
mode = NOT_STARTED;
setButtons();
try{
@@ -640,11 +690,22 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
return finQuery;
}
-
+ private static boolean checkAnalysisResult( final String resultData,
+ final Collection<String> labels ) {
+ for ( final String verifiedLabel : labels ) {
+ if ( resultData.contains( verifiedLabel ) ) {
+ return true;
+ }
+ }
+
+ return false;
+ }
+
// return: -1: error
// return: 0: property is NOt satisfied
// return: 1: property is satisfied
- private int workQuery(String query, String fn, int trace_id, RshClient rshc) throws LauncherException {
+ private int workQuery(String query, String fn, int trace_id, RshClient rshc)
+ throws LauncherException {
int ret = -1;
TraceManager.addDev("Working on query: " + query);
@@ -670,16 +731,21 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
}
//NOTE: [error] is only visible if Error Stream is parsed
if (mode != NOT_STARTED) {
- if (data.trim().length() == 0) {
+ if (data.trim().length() == 0) {
//jta.append("The verifier of UPPAAL could not be started: error\n");
throw new LauncherException("The verifier of UPPAAL could not be started.\nProbably, UPPAAL is badly installed, or TTool is badly configured:\nCheck for UPPAALVerifierPath and UPPAALVerifierHost configurations.");
}
- else if (data.indexOf("Property is satisfied") >-1){
+
+ // Issue #35: Different labels for UPPAAL 4.1.19
+ else if ( checkAnalysisResult( data, PROP_VERIFIED_LABELS ) ) {
+// else if (data.indexOf("Property is satisfied") >-1){
jta.append("-> property is satisfied\n");
status=1;
ret = 1;
}
- else if (data.indexOf("Property is NOT satisfied") > -1) {
+ // Issue #35: Different labels for UPPAAL 4.1.19
+ else if ( checkAnalysisResult( data, PROP_NOT_VERIFIED_LABELS ) ) {
+// else if (data.indexOf("Property is NOT satisfied") > -1) {
jta.append("-> property is NOT satisfied\n");
status = 0;
ret = 0;
@@ -694,14 +760,11 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
jta.append("** verification stopped **\n");
}
-
-
if (generateTrace.isSelected()) {
generateTraceFile(fn, trace_id, rshc);
}
return ret;
-
}
private void generateTraceFile(String fn, int trace_id, RshClient rshc) throws LauncherException{
@@ -725,12 +788,35 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
}
}
- protected String processCmd(String cmd) throws LauncherException {
+ protected String processCmd(String cmd)
+ throws LauncherException {
rshc.setCmd(cmd);
- String s = null;
- rshc.sendExecuteCommandRequest();
- s = rshc.getDataFromProcess();
- return s;
+
+ // Issue #35: Test the value of return code and display appropriate error message
+ rshc.sendExecuteCommandRequest( true );
+
+ final String data = rshc.getDataFromProcess();
+
+ final Integer retCode = rshc.getProcessReturnCode();
+
+ if ( retCode == null || retCode != 0 ) {
+ final String message;
+
+ if ( data == null || data.isEmpty() ) {
+ message = "Error executing command '" + cmd + "' with return code " + retCode;
+ }
+ else {
+ message = data;
+ }
+
+ throw new LauncherException( System.lineSeparator() + message );
+ }
+
+ return data;
+// String s = null;
+// rshc.sendExecuteCommandRequest();
+// s = rshc.getDataFromProcess();
+// return s;
}
protected void setButtons() {
diff --git a/ttool/launch_configurations/config.xml b/ttool/launch_configurations/config.xml
index 7e0b80524f17583969c41a26198eb8a2deefcc94..86a78484afb320709a4577e0bbef1af22071cd93 100755
--- a/ttool/launch_configurations/config.xml
+++ b/ttool/launch_configurations/config.xml
@@ -41,8 +41,10 @@
<GTKWavePath data="/opt/local/bin/gtkwave" />
<VCDPath data="../simulators/c++2/" />
<UPPAALCodeDirectory data="../uppaal/" />
-<UPPAALVerifierPath data="/packages/uppaal-4.0.11/verifyta" />
+<UPPAALVerifierPath data="/home/dblouin/Produits/uppaal64-4.1.19/bin-Linux/verifyta" />
<UPPAALVerifierHost data="localhost" />
+<UPPAALPropertyVerifMessage data="Property is satisfied, Formula is satisfied"/>
+<UPPAALPropertyNotVerifMessage data="Property is NOT satisfied, Formula is NOT satisfied"/>
<ProVerifCodeDirectory data="../proverif/" />
<ProVerifVerifierPath data="/packages/proverif/proverif" />
<ProVerifVerifierHost data="localhost" />
@@ -65,7 +67,7 @@
<PLUGIN_JAVA_CODE_GENERATOR data="../plugins/CustomizerAvatarCodeGeneration.jar" />
-<LastOpenFile data="/home/dblouin/Projets/TTool/git/TTool/modeling/DIPLODOCUS/ZigBeeDEMO.xml"/>
+<LastOpenFile data="/home/dblouin/Projets/TTool/git/TTool/modeling/DIPLODOCUS/ZigBeeTutorial.xml"/>