From 965762823cf00f947aa6fa0e30982fd368cb0037 Mon Sep 17 00:00:00 2001
From: Ludovic Apvrille <ludovic.apvrille@telecom-paristech.fr>
Date: Wed, 28 Jul 2010 13:38:54 +0000
Subject: [PATCH] DIPLODOCUS: Update on multiple params supported by events
---
src/tmltranslator/touppaal/TML2UPPAAL.java | 1 +
src/translator/TClassEventFinite.java | 36 ++++++++++++++------
src/translator/TURTLEModelChecker.java | 38 ++++++++++++----------
3 files changed, 47 insertions(+), 28 deletions(-)
diff --git a/src/tmltranslator/touppaal/TML2UPPAAL.java b/src/tmltranslator/touppaal/TML2UPPAAL.java
index eb52f61b29..bf8bd9fb00 100755
--- a/src/tmltranslator/touppaal/TML2UPPAAL.java
+++ b/src/tmltranslator/touppaal/TML2UPPAAL.java
@@ -120,6 +120,7 @@ public class TML2UPPAAL {
}
public UPPAALSpec generateUPPAAL(boolean _debug) {
+ TraceManager.addDev("Generating UPPAAL Specification");
tmlmodeling.removeAllRandomSequences();
debug = _debug;
diff --git a/src/translator/TClassEventFinite.java b/src/translator/TClassEventFinite.java
index 05022061d4..c147094970 100755
--- a/src/translator/TClassEventFinite.java
+++ b/src/translator/TClassEventFinite.java
@@ -172,15 +172,30 @@ public class TClassEventFinite extends TClass implements TClassEventCommon, FIFO
ad.getStartState().addNext(adstop);
return;
}
+
+ Param [] params_a = new Param[nbPara];
+ Param [] params_b = new Param[nbPara];
- p1 = new Param("p0", Param.NAT, "0");
+ /*p1 = new Param("p0", Param.NAT, "0");
p2 = new Param("p1", Param.NAT, "0");
p3 = new Param("p2", Param.NAT, "0");
+ p4 = new Param("p3", Param.NAT, "0");
+ p5 = new Param("p4", Param.NAT, "0");
p10 = new Param("p00", Param.NAT, "0");
p20 = new Param("p10", Param.NAT, "0");
p30 = new Param("p20", Param.NAT, "0");
-
- if (nbPara > 0) {
+ p40 = new Param("p30", Param.NAT, "0");
+ p50 = new Param("p40", Param.NAT, "0");*/
+
+ for(i=0; i<nbPara; i++) {
+ params_a[i] = new Param("pa" + i, Param.NAT, "0");
+ params_b[i] = new Param("pb" + i, Param.NAT, "0");
+ addParameter(params_a[i]);
+ addParameter(params_b[i]);
+ }
+
+
+ /*if (nbPara > 0) {
addParameter(p1);
addParameter(p10);
}
@@ -191,7 +206,8 @@ public class TClassEventFinite extends TClass implements TClassEventCommon, FIFO
if (nbPara > 2) {
addParameter(p3);
addParameter(p30);
- }
+ }*/
+
nb = new Param("nb", Param.NAT, "0");
addParameter(nb);
@@ -223,7 +239,7 @@ public class TClassEventFinite extends TClass implements TClassEventCommon, FIFO
ad.add(adag);
action = "";
for(i=0; i<nbPara; i++) {
- action += "?p" + i + "0:nat";
+ action += "?pb" + i + ":nat";
}
action += "?index:nat";
adag.setActionValue(action);
@@ -238,7 +254,7 @@ public class TClassEventFinite extends TClass implements TClassEventCommon, FIFO
ad.add(adag);
action = "";
for(i=0; i<nbPara; i++) {
- action += "!p" + i + "0";
+ action += "!pb" + i + "";
}
action += "!index";
adag.setActionValue(action);
@@ -304,7 +320,7 @@ public class TClassEventFinite extends TClass implements TClassEventCommon, FIFO
ad.add(adag);
action = "";
for(i=0; i<nbPara; i++) {
- action += "?p" + i + "0:nat";
+ action += "?pb" + i + ":nat";
}
adag.setActionValue(action);
adch3.addNext(adag);
@@ -316,7 +332,7 @@ public class TClassEventFinite extends TClass implements TClassEventCommon, FIFO
ad.add(adag);
action = "";
for(i=0; i<nbPara; i++) {
- action += "!p" + i + "0";
+ action += "!pb" + i + "";
}
action+="!index";
adag.setActionValue(action);
@@ -344,7 +360,7 @@ public class TClassEventFinite extends TClass implements TClassEventCommon, FIFO
ad.add(adag);
action = "";
for(i=0; i<nbPara; i++) {
- action += "?p" + i + ":nat";
+ action += "?pa" + i + ":nat";
}
action += "!index_r";
adag.setActionValue(action);
@@ -382,7 +398,7 @@ public class TClassEventFinite extends TClass implements TClassEventCommon, FIFO
ad.add(adag);
action = "";
for(i=0; i<nbPara; i++) {
- action += "!p" + i + "";
+ action += "!pa" + i + "";
}
adag.setActionValue(action);
adch3.addNext(adag);
diff --git a/src/translator/TURTLEModelChecker.java b/src/translator/TURTLEModelChecker.java
index 562e2f0c89..f11e25eb10 100755
--- a/src/translator/TURTLEModelChecker.java
+++ b/src/translator/TURTLEModelChecker.java
@@ -50,6 +50,7 @@ import compiler.tmlparser.*;
import java.util.*;
import java.io.*;
+import myutil.*;
public class TURTLEModelChecker {
@@ -114,7 +115,7 @@ public class TURTLEModelChecker {
}
public Vector syntaxAnalysisChecking() {
- //System.out.println("modelChecking");
+ //TraceManager.addDev("modelChecking");
Vector errors = new Vector();
warnings = new Vector();
syntaxAnalysisCheckingCD(errors, warnings);
@@ -134,7 +135,7 @@ public class TURTLEModelChecker {
}
public void syntaxAnalysisCheckingAD(TClass t, Vector errors, Vector warnings) {
- //System.out.println("Checking activity diagram of " + t.getName());
+ //TraceManager.addDev("Checking activity diagram of " + t.getName());
checkRuleAD000(t, errors, warnings);
checkRuleAD001(t, errors, warnings);
checkRuleAD004(t, errors, warnings);
@@ -323,7 +324,7 @@ public class TURTLEModelChecker {
boolean b = adp.isAValidMotif(t);
if (b) {
for(j=0; j<adp.nbGate(); j++) {
- //System.out.println("Getting gate #" + j + " of t " + t.getName());
+ //TraceManager.addDev("Getting gate #" + j + " of t " + t.getName());
g = adp.getGate(j);
if (tm.syncRelationWith(t, g) != null) {
CheckingError error = new CheckingError(CheckingError.BEHAVIOR_ERROR, t.getName() + "/Parallel operator: " + g.getName() + ERROR_AD_007);
@@ -359,7 +360,7 @@ public class TURTLEModelChecker {
boolean b = adp.isAValidMotif(t);
if (b) {
for(j=0; j<adp.nbGate(); j++) {
- //System.out.println("Getting gate #" + j + " of t " + t.getName());
+ //TraceManager.addDev("Getting gate #" + j + " of t " + t.getName());
g = adp.getGate(j);
if (tm.canReachSynchroOn(adp, g)) {
CheckingError error = new CheckingError(CheckingError.BEHAVIOR_ERROR, t.getName() + "/Parallel operator: " + g.getName() + ERROR_AD_008);
@@ -412,7 +413,7 @@ public class TURTLEModelChecker {
if ((action!= null) && (action.length() > 0)) {
parsing(t, ad1, "actiongate", action, errors);
} else {
- //System.out.println("null action on gate=" + ((ADActionStateWithGate)ad1).getGate().getName() + action);
+ //TraceManager.addDev("null action on gate=" + ((ADActionStateWithGate)ad1).getGate().getName() + action);
}
} else if (ad1 instanceof ADActionStateWithParam) {
@@ -506,20 +507,20 @@ public class TURTLEModelChecker {
// First parsing
parser = new TMLExprParser(new StringReader(parseCmd + " " + action));
try {
- //System.out.println("\nParsing :" + parseCmd + " " + action);
+ //TraceManager.addDev("\nParsing :" + parseCmd + " " + action);
root = parser.CompilationUnit();
//root.dump("pref=");
- //System.out.println("Parse ok");
+ //TraceManager.addDev("Parse ok");
} catch (ParseException e) {
- System.out.println("\nParsing :" + parseCmd + " " + action);
- System.out.println("ParseException --------> Parse error in :" + parseCmd + " " + action);
+ TraceManager.addDev("\nParsing :" + parseCmd + " " + action);
+ TraceManager.addDev("ParseException --------> Parse error in :" + parseCmd + " " + action);
CheckingError error = new CheckingError(CheckingError.BEHAVIOR_ERROR, ERROR_AD_009_0 + " in expression " + action + " of tclass " + t.getName());
error.setTClass(t);
putCorrespondance(error, elt);
errors.add(error);
return;
} catch (TokenMgrError tke) {
- System.out.println("TokenMgrError --------> Parse error in :" + parseCmd + " " + action);
+ TraceManager.addDev("TokenMgrError --------> Parse error in :" + parseCmd + " " + action);
CheckingError error = new CheckingError(CheckingError.BEHAVIOR_ERROR, ERROR_AD_009_0 + " in expression " + action + " of tclass " + t.getName());
error.setTClass(t);
putCorrespondance(error, elt);
@@ -550,22 +551,22 @@ public class TURTLEModelChecker {
parser = new TMLExprParser(new StringReader(parseCmd + " " + modif));
try {
- //System.out.println("\nParsing :" + parseCmd + " " + modif);
+ //TraceManager.addDev("\nParsing :" + parseCmd + " " + modif);
root = parser.CompilationUnit();
//root.dump("pref=");
- //System.out.println("Parse ok");
+ //TraceManager.addDev("Parse ok");
} catch (ParseException e) {
- System.out.println("\nParsing :" + parseCmd + " " + modif);
- System.out.println("\n(Original parsing :" + parseCmd + " " + action);
- System.out.println("ParseException --------> Parse error in :" + parseCmd + " " + action);
+ TraceManager.addDev("\nParsing :" + parseCmd + " " + modif);
+ TraceManager.addDev("\n(Original parsing :" + parseCmd + " " + action);
+ TraceManager.addDev("ParseException --------> Parse error in :" + parseCmd + " " + action);
CheckingError error = new CheckingError(CheckingError.BEHAVIOR_ERROR, ERROR_AD_009_1 + " in expression " + action + " of tclass " + t.getName());
error.setTClass(t);
errors.add(error);
putCorrespondance(error, elt);
return;
} catch (TokenMgrError tke ) {
- System.out.println("\nParsing :" + parseCmd + " " + modif);
- System.out.println("TokenMgrError --------> Parse error in :" + parseCmd + " " + action);
+ TraceManager.addDev("\nParsing :" + parseCmd + " " + modif);
+ TraceManager.addDev("TokenMgrError --------> Parse error in :" + parseCmd + " " + action);
CheckingError error = new CheckingError(CheckingError.BEHAVIOR_ERROR, ERROR_AD_009_1 + " in expression " + action + " of tclass " + t.getName());
error.setTClass(t);
putCorrespondance(error, elt);
@@ -578,7 +579,8 @@ public class TURTLEModelChecker {
for(String s: vars) {
// is that string a variable?
if ((s.compareTo("true") != 0) && (s.compareTo("false") != 0) && (s.compareTo("nil") != 0)) {
- System.out.println("Variable not declared: " +s);
+ TraceManager.addDev("\nParsing :" + parseCmd + " " + modif + " tclass" + t.getName());
+ TraceManager.addDev("Variable not declared: " +s);
CheckingError error = new CheckingError(CheckingError.BEHAVIOR_ERROR, s + ": " + ERROR_AD_009_2 + " in expression " + action + " of tclass " + t.getName());
error.setTClass(t);
putCorrespondance(error, elt);
--
GitLab