Skip to content

TTool
TTool
Commit d1663776 authored by Ludovic Apvrille's avatar Ludovic Apvrille
Browse files
Options

Addind uppaal dir

parent 0fa41a12
Hide whitespace changes
Inline Side-by-side
Showing with 147 additions and 56 deletions
modeling/modelsForTestingTTool/testdiplo.xml
View file @ d1663776
......@@ -1449,8 +1449,8 @@
<TMLActivityDiagramPanel name="T1" minX="10" maxX="2500" minY="10" maxY="1500" >
<COMPONENT type="1008" id="365" >
<cdparam x="176" y="106" />
<sizeparam width="71" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<cdparam x="177" y="106" />
<sizeparam width="68" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
<infoparam name="send event" value="comm1(x)" />
......@@ -1501,8 +1501,8 @@
<TMLActivityDiagramPanel name="T0" minX="10" maxX="2500" minY="10" maxY="1500" >
<COMPONENT type="1010" id="374" >
<cdparam x="384" y="131" />
<sizeparam width="75" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<cdparam x="385" y="131" />
<sizeparam width="72" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
<infoparam name="wait event" value="comm0(x) " />
......@@ -1553,8 +1553,8 @@
<TMLActivityDiagramPanel name="T2" minX="10" maxX="2500" minY="10" maxY="1500" >
<COMPONENT type="1008" id="383" >
<cdparam x="468" y="113" />
<sizeparam width="71" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<cdparam x="469" y="113" />
<sizeparam width="68" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
<infoparam name="send event" value="comm2(x)" />
......@@ -1648,9 +1648,9 @@
<SUBCOMPONENT type="1101" id="398" >
<father id="441" num="0" />
<cdparam x="445" y="269" />
<sizeparam width="109" height="40" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<sizeparam width="106" height="40" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="0" maxX="141" minY="0" maxY="160" />
<cdrectangleparam minX="0" maxX="144" minY="0" maxY="160" />
<infoparam name="TGComponent" value="Design3::T2" />
<TGConnectingPoint num="0" id="390" />
<TGConnectingPoint num="1" id="391" />
......@@ -1667,9 +1667,9 @@
<SUBCOMPONENT type="1101" id="407" >
<father id="441" num="1" />
<cdparam x="405" y="170" />
<sizeparam width="109" height="40" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<sizeparam width="106" height="40" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="0" maxX="141" minY="0" maxY="160" />
<cdrectangleparam minX="0" maxX="144" minY="0" maxY="160" />
<infoparam name="TGComponent" value="Design3::T0" />
<TGConnectingPoint num="0" id="399" />
<TGConnectingPoint num="1" id="400" />
......@@ -1686,9 +1686,9 @@
<SUBCOMPONENT type="1101" id="416" >
<father id="441" num="2" />
<cdparam x="413" y="213" />
<sizeparam width="109" height="40" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<sizeparam width="106" height="40" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="0" maxX="141" minY="0" maxY="160" />
<cdrectangleparam minX="0" maxX="144" minY="0" maxY="160" />
<infoparam name="TGComponent" value="Design3::T1" />
<TGConnectingPoint num="0" id="408" />
<TGConnectingPoint num="1" id="409" />
......@@ -2024,9 +2024,98 @@
<Validated value="" />
<Ignored value="" />
<COMPONENT type="5000" id="1206" >
<cdparam x="156" y="114" />
<sizeparam width="250" height="200" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
<infoparam name="Block0" value="Block0" />
<TGConnectingPoint num="0" id="1207" />
<TGConnectingPoint num="1" id="1208" />
<TGConnectingPoint num="2" id="1209" />
<TGConnectingPoint num="3" id="1210" />
<TGConnectingPoint num="4" id="1211" />
<TGConnectingPoint num="5" id="1212" />
<TGConnectingPoint num="6" id="1213" />
<TGConnectingPoint num="7" id="1214" />
<TGConnectingPoint num="8" id="1215" />
<TGConnectingPoint num="9" id="1216" />
<TGConnectingPoint num="10" id="1217" />
<TGConnectingPoint num="11" id="1218" />
<TGConnectingPoint num="12" id="1219" />
<TGConnectingPoint num="13" id="1220" />
<TGConnectingPoint num="14" id="1221" />
<TGConnectingPoint num="15" id="1222" />
<TGConnectingPoint num="16" id="1223" />
<TGConnectingPoint num="17" id="1224" />
<TGConnectingPoint num="18" id="1225" />
<TGConnectingPoint num="19" id="1226" />
<TGConnectingPoint num="20" id="1227" />
<TGConnectingPoint num="21" id="1228" />
<TGConnectingPoint num="22" id="1229" />
<TGConnectingPoint num="23" id="1230" />
<extraparam>
<CryptoBlock value="false" />
<Attribute access="0" id="x" value="1" type="8" typeOther="" />
</extraparam>
</COMPONENT>
</AVATARBlockDiagramPanel>
<AVATARStateMachineDiagramPanel name="Block0" minX="10" maxX="2500" minY="10" maxY="1500" >
<COMPONENT type="5101" id="1233" >
<cdparam x="384" y="136" />
<sizeparam width="20" height="20" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
<infoparam name="stop state" value="null" />
<TGConnectingPoint num="0" id="1234" />
</COMPONENT>
<COMPONENT type="5100" id="1231" >
<cdparam x="400" y="50" />
<sizeparam width="15" height="15" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
<infoparam name="start state" value="null" />
<TGConnectingPoint num="0" id="1232" />
</COMPONENT>
<CONNECTOR type="5102" id="1235" >
<cdparam x="407" y="70" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="null" />
<TGConnectingPoint num="0" id="1236" />
<P1 x="407" y="70" id="1232" />
<P2 x="394" y="131" id="1234" />
<AutomaticDrawing data="true" />
</CONNECTOR><SUBCOMPONENT type="-1" id="1237" >
<father id="1235" num="0" />
<cdparam x="400" y="100" />
<sizeparam width="58" height="15" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
<infoparam name="List of all parameters of an Avatar SMD transition" value="" />
<TGConnectingPoint num="0" id="1238" />
<TGConnectingPoint num="1" id="1239" />
<TGConnectingPoint num="2" id="1240" />
<TGConnectingPoint num="3" id="1241" />
<extraparam>
<guard value="[ ]" />
<afterMin value="" />
<afterMax value="" />
<computeMin value="" />
<computeMax value="" />
<actions value="x = x + 1" />
<filesToIncludeLine value="" />
<codeToIncludeLine value="" />
</extraparam>
</SUBCOMPONENT>
</AVATARStateMachineDiagramPanel>
</Modeling>
......
src/ui/window/JDialogUPPAALValidation.java
View file @ d1663776
......@@ -92,6 +92,7 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
protected java.util.List<String> customQueries;
public Map<String, Integer> verifMap;
protected int status = -1;
/** Creates new form */
public JDialogUPPAALValidation(Frame f, MainGUI _mgui, String title, String _cmdVerifyta, String _pathTrace, String _fileName, String _spec, String _host, TURTLEPanel _tp) {
super(f, title, true);
......@@ -113,7 +114,7 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
customChecks = new LinkedList<JCheckBox>();
initComponents();
myInitComponents();
verifMap = new HashMap<String, Integer>();
verifMap = new HashMap<String, Integer>();
pack();
//getGlassPane().addMouseListener( new MouseAdapter() {});
......@@ -316,15 +317,15 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
public void run() {
// String cmd1 = "";
// String data1;
// String cmd1 = "";
// String data1;
int id = 0;
String query;
String name;
int trace_id = 0;
int index;
String fn;
int result;
int result;
rshc = new RshClient(host);
RshClient rshctmp = rshc;
......@@ -355,11 +356,11 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
ArrayList<TGComponentAndUPPAALQuery> list = mgui.gtm.getUPPAALQueries(tp);
if ((list != null) && (list.size() > 0)){
for(TGComponentAndUPPAALQuery cq: list) {
String s = cq.uppaalQuery;
String s = cq.uppaalQuery;
index = s.indexOf('$');
if (cq.tgc != null) {
cq.tgc.setReachability(TGComponent.ACCESSIBILITY_UNKNOWN);
}
if (cq.tgc != null) {
cq.tgc.setReachability(TGComponent.ACCESSIBILITY_UNKNOWN);
}
if ((index != -1) && (mode != NOT_STARTED)) {
name = s.substring(index+1, s.length());
//TraceManager.addDev("****\n name=" + name + " list=" + list + "\n****\n");
......@@ -367,14 +368,14 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
//jta.append("\n\n--------------------------------------------\n");
jta.append("\nReachability of: " + name + "\n");
result = workQuery("E<> " + query, fn, trace_id, rshc);
if (cq.tgc != null) {
if (result == 0) {
cq.tgc.setReachability(TGComponent.ACCESSIBILITY_KO);
cq.tgc.setLiveness(TGComponent.ACCESSIBILITY_KO);
} else if (result == 1) {
cq.tgc.setReachability(TGComponent.ACCESSIBILITY_OK);
}
}
if (cq.tgc != null) {
if (result == 0) {
cq.tgc.setReachability(TGComponent.ACCESSIBILITY_KO);
cq.tgc.setLiveness(TGComponent.ACCESSIBILITY_KO);
} else if (result == 1) {
cq.tgc.setReachability(TGComponent.ACCESSIBILITY_OK);
}
}
trace_id++;
} else {
jta.append("A component could not be studied (internal error)\n");
......@@ -388,11 +389,11 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
if (stateA.isSelected() && (mode != NOT_STARTED)) {
ArrayList<TGComponentAndUPPAALQuery> list = mgui.gtm.getUPPAALQueries(tp);
if ((list != null) && (list.size() > 0)){
for(TGComponentAndUPPAALQuery cq: list) {
if (cq.tgc != null) {
cq.tgc.setLiveness(TGComponent.ACCESSIBILITY_UNKNOWN);
}
String s = cq.uppaalQuery;
for(TGComponentAndUPPAALQuery cq: list) {
if (cq.tgc != null) {
cq.tgc.setLiveness(TGComponent.ACCESSIBILITY_UNKNOWN);
}
String s = cq.uppaalQuery;
index = s.indexOf('$');
if ((index != -1) && (mode != NOT_STARTED)) {
name = s.substring(index+1, s.length());
......@@ -400,13 +401,13 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
//jta.append("\n--------------------------------------------\n");
jta.append("\nLiveness of: " + name + "\n");
result = workQuery("A<> " + query, fn, trace_id, rshc);
if (cq.tgc != null) {
if (result == 0) {
cq.tgc.setLiveness(TGComponent.ACCESSIBILITY_KO);
} else if (result == 1) {
cq.tgc.setLiveness(TGComponent.ACCESSIBILITY_OK);
}
}
if (cq.tgc != null) {
if (result == 0) {
cq.tgc.setLiveness(TGComponent.ACCESSIBILITY_KO);
} else if (result == 1) {
cq.tgc.setLiveness(TGComponent.ACCESSIBILITY_OK);
}
}
trace_id++;
} else {
jta.append("A component could not be studied (internal error)\n");
......@@ -472,14 +473,14 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
if (j.isSelected()){
jta.append(j.getText()+"\n");
String translation = translateCustomQuery(j.getText());
jta.append(translation);
status = -1;
jta.append(translation);
status = -1;
workQuery(translation, fn, trace_id, rshc);
verifMap.put(j.getText(), status);
verifMap.put(j.getText(), status);
trace_id++;
}
}
mgui.modelBacktracingUPPAAL(verifMap);
}
......@@ -513,7 +514,7 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
} catch (LauncherException le1) {}
return;
}
mode = NOT_STARTED;
setButtons();
}
......@@ -568,7 +569,7 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
// return: 1: property is satisfied
private int workQuery(String query, String fn, int trace_id, RshClient rshc) throws LauncherException {
int ret = -1;
int ret = -1;
TraceManager.addDev("Working on query: " + query);
......@@ -584,7 +585,7 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
}
cmd1 += fn + ".xml " + fn + ".q";
//jta.append("--------------------------------------------\n");
//TraceManager.addDev("Query:>" + cmd1 + "<");
//TraceManager.addDev("Query:>" + cmd1 + "<");
data = processCmd(cmd1);
//TraceManager.addDev("Results:>" + data + "<");
if(showDetails.isSelected()) {
......@@ -598,19 +599,19 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
}
else if (data.indexOf("Property is satisfied") >-1){
jta.append("-> property is satisfied\n");
status=1;
ret = 1;
status=1;
ret = 1;
}
else if (data.indexOf("Property is NOT satisfied") > -1) {
jta.append("-> property is NOT satisfied\n");
status = 0;
ret = 0;
status = 0;
ret = 0;
}
else {
jta.append("ERROR -> property could not be studied\n");
status=2;
status=2;
}
} else {
jta.append("** verification stopped **\n");
......@@ -622,8 +623,8 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
generateTraceFile(fn, trace_id, rshc);
}
return ret;
return ret;
}
private void generateTraceFile(String fn, int trace_id, RshClient rshc) throws LauncherException{
......
uppaal/README 0 → 100644
View file @ d1663776
Dir in which uppaal spec are generated
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment