Skip to content
Snippets Groups Projects
Commit 96576282 authored by Ludovic Apvrille's avatar Ludovic Apvrille
Browse files

DIPLODOCUS: Update on multiple params supported by events

parent 17d7a5e4
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/tmltranslator/touppaal/TML2UPPAAL.java
+ 1
− 0
View file @ 96576282
......@@ -120,6 +120,7 @@ public class TML2UPPAAL {
}
public UPPAALSpec generateUPPAAL(boolean _debug) {
TraceManager.addDev("Generating UPPAAL Specification");
tmlmodeling.removeAllRandomSequences();
debug = _debug;
......
src/translator/TClassEventFinite.java
+ 26
− 10
View file @ 96576282
......@@ -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);
......
src/translator/TURTLEModelChecker.java
+ 20
− 18
View file @ 96576282
......@@ -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);
......
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