From 49b351aca2e39dc756420924f87de0ba6d0ecb6b Mon Sep 17 00:00:00 2001
From: Sophie Coudert <sophie.coudert@telecom-paris.fr>
Date: Tue, 16 Jul 2024 17:07:22 +0200
Subject: [PATCH] building test in progress
---
.../tosysmlv2/Avatar2SysML.java | 8 +-
.../tosysmlv2/Avatar2SysMLLexer.java | 4 +-
.../tosysmlv2/Avatar2SysMLNames.java | 8 +-
.../tosysmlv2/AvatarFromSysML.java | 39 +-
.../test/java/cli/CLIAvatar2SysMLV2Test.java | 428 +-----------------
5 files changed, 38 insertions(+), 449 deletions(-)
diff --git a/src/main/java/avatartranslator/tosysmlv2/Avatar2SysML.java b/src/main/java/avatartranslator/tosysmlv2/Avatar2SysML.java
index de4b6d38b1..f9c99abfc0 100644
--- a/src/main/java/avatartranslator/tosysmlv2/Avatar2SysML.java
+++ b/src/main/java/avatartranslator/tosysmlv2/Avatar2SysML.java
@@ -420,13 +420,13 @@ public class Avatar2SysML {
// Binding block signals to the channel ................
if (out2in) { // depends on direction. symetric.
- avsysml.append(indentation + "binding : '#InSignalBinding' bind " + blk1SysMLname + "." + sig1SYSMLname + " = " + channelSYSMLname +
+ avsysml.append(indentation + "binding : '#OutSignalBinding' bind " + blk1SysMLname + "." + sig1SYSMLname + " = " + channelSYSMLname +
";\n");
- avsysml.append(indentation + "binding : '#OutSignalBinding' bind " + blk2SysMLname + "." + sig2SYSMLname + " = " + channelSYSMLname +
+ avsysml.append(indentation + "binding : '#InSignalBinding' bind " + blk2SysMLname + "." + sig2SYSMLname + " = " + channelSYSMLname +
";\n");
} else {
- avsysml.append(indentation + "binding : '#OutSignalBinding' bind " + blk1SysMLname + "." + sig1SYSMLname + " = " + channelSYSMLname + ";\n");
- avsysml.append(indentation + "binding : '#InSignalBinding' bind " + blk2SysMLname + "." + sig2SYSMLname + " = " + channelSYSMLname + ";\n");
+ avsysml.append(indentation + "binding : '#InSignalBinding' bind " + blk1SysMLname + "." + sig1SYSMLname + " = " + channelSYSMLname + ";\n");
+ avsysml.append(indentation + "binding : '#OutSignalBinding' bind " + blk2SysMLname + "." + sig2SYSMLname + " = " + channelSYSMLname + ";\n");
}
// Message declarations .........................
diff --git a/src/main/java/avatartranslator/tosysmlv2/Avatar2SysMLLexer.java b/src/main/java/avatartranslator/tosysmlv2/Avatar2SysMLLexer.java
index 66a50fff7d..6aac3646a8 100644
--- a/src/main/java/avatartranslator/tosysmlv2/Avatar2SysMLLexer.java
+++ b/src/main/java/avatartranslator/tosysmlv2/Avatar2SysMLLexer.java
@@ -1,4 +1,4 @@
-/* The following code was generated by JFlex 1.4.3 on 04/07/2024 16:14 */
+/* The following code was generated by JFlex 1.4.3 on 16/07/2024 15:36 */
/* Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
*
@@ -45,7 +45,7 @@ import java_cup.runtime.*;
/**
* This class is a scanner generated by
* <a href="http://www.jflex.de/">JFlex</a> 1.4.3
- * on 04/07/2024 16:14 from the specification file
+ * on 16/07/2024 15:36 from the specification file
* <code>__Avatar2SysMLLexer__.jflex</code>
*/
public class Avatar2SysMLLexer implements java_cup.runtime.Scanner {
diff --git a/src/main/java/avatartranslator/tosysmlv2/Avatar2SysMLNames.java b/src/main/java/avatartranslator/tosysmlv2/Avatar2SysMLNames.java
index fdfaed752f..080ea810ec 100644
--- a/src/main/java/avatartranslator/tosysmlv2/Avatar2SysMLNames.java
+++ b/src/main/java/avatartranslator/tosysmlv2/Avatar2SysMLNames.java
@@ -196,8 +196,12 @@ public class Avatar2SysMLNames {
/** convert an Avatar int/bool expression into a SysML expression */
public static String expr2SysML(String _expr) {
- Avatar2SysMLParser parser = new Avatar2SysMLParser(new Avatar2SysMLLexer(new StringReader (_expr)), new ComplexSymbolFactory());
- try { return (String)parser.parse().value; }
+ Avatar2SysMLParser parser = new Avatar2SysMLParser(new Avatar2SysMLLexer(new StringReader (_expr)));
+ try {
+ String res = (String)parser.parse().value;
+ System.out.println("$$$$$$$$$$$$$$$$$$$ E2SYSML " + _expr + " - " + res);
+ return res;
+ }
catch (java.lang.Exception e) {
e.printStackTrace();
return ""; }
diff --git a/src/main/java/avatartranslator/tosysmlv2/AvatarFromSysML.java b/src/main/java/avatartranslator/tosysmlv2/AvatarFromSysML.java
index 717b3739e6..b9961d5c30 100644
--- a/src/main/java/avatartranslator/tosysmlv2/AvatarFromSysML.java
+++ b/src/main/java/avatartranslator/tosysmlv2/AvatarFromSysML.java
@@ -142,18 +142,24 @@ public class AvatarFromSysML {
errors = stxSpec.getErrors();
// Build Specification from parser-returned abstract syntax tree.
- TraceManager.addDev("Building Specification");
- avSpec = new AvatarSpecification("FromSysMLV2_EXAMPLE_SPECIFICATION",null);
- signalMap.clear();
- blockMap.clear();
- stateMap.clear();
- TraceManager.addDev("Building DataTypes");
- buildDataTypes();
- TraceManager.addDev("Building Blocks");
- buildBlocks();
- TraceManager.addDev("Building Relations");
- buildRelations();
-
+ try {
+ TraceManager.addDev("Building Specification");
+ avSpec = new AvatarSpecification("FromSysMLV2_EXAMPLE_SPECIFICATION", null);
+ signalMap.clear();
+ blockMap.clear();
+ stateMap.clear();
+ TraceManager.addDev("Building DataTypes");
+ buildDataTypes();
+ TraceManager.addDev("Building Blocks");
+ buildBlocks();
+ TraceManager.addDev("Building Relations");
+ buildRelations();
+ }
+ catch (Exception ex) {
+ for(AvatarFromSysMLError e : errors)
+ TraceManager.addDev(e.toString());
+ throw ex;
+ }
// TODO: move error handling
for(AvatarFromSysMLError e : errors)
TraceManager.addDev(e.toString());
@@ -845,8 +851,8 @@ public class AvatarFromSysML {
}
state.setSignal( getSignal(transition.getSignal()));
if (state.getSignal().isIn()) {
- new AvatarFromSysMLError(AvatarFromSysMLError.HIGHERROR, transition.getRleft(),
- "signal of sending transition must be an output signal", transition.getSignal().getLeft());
+ addError(new AvatarFromSysMLError(AvatarFromSysMLError.HIGHERROR, transition.getRleft(),
+ "signal of sending transition must be an output signal", transition.getSignal().getLeft()));
continue;
}
if (! transition.getSignal().isDeclared()) {
@@ -923,8 +929,8 @@ public class AvatarFromSysML {
continue;
}
if (state.getSignal().isOut()) {
- new AvatarFromSysMLError(AvatarFromSysMLError.HIGHERROR, transition.getRleft(),
- "signal of receiving transition must be an input signal", transition.getSignal().getLeft());
+ addError(new AvatarFromSysMLError(AvatarFromSysMLError.HIGHERROR, transition.getRleft(),
+ "signal of receiving transition must be an input signal", transition.getSignal().getLeft()));
continue;
}
if (transition.getSignal().getChannel() == null) {
@@ -992,7 +998,6 @@ public class AvatarFromSysML {
"receiving transition should lead to a receive state", transition.getRleft()));
continue;
}
-
}
// set-timer transitions =====================
diff --git a/ttool/src/test/java/cli/CLIAvatar2SysMLV2Test.java b/ttool/src/test/java/cli/CLIAvatar2SysMLV2Test.java
index 71b7a2262e..03cf3b04e7 100644
--- a/ttool/src/test/java/cli/CLIAvatar2SysMLV2Test.java
+++ b/ttool/src/test/java/cli/CLIAvatar2SysMLV2Test.java
@@ -68,7 +68,6 @@ public class CLIAvatar2SysMLV2Test extends AbstractTest implements InterpreterOu
final static String PATH_TO_MODELS = "cli/models/";
private StringBuilder outputResult;
- private static final String DEADLOCKS [] = {"#MainBlock", "-stop", "#Receiver", "-stopCreated", "-MainChoice"};
public CLIAvatar2SysMLV2Test() {
//
@@ -87,12 +86,12 @@ public class CLIAvatar2SysMLV2Test extends AbstractTest implements InterpreterOu
System.out.println("info from interpreter:" + s);
outputResult.append(s);
}
-
- @Test
- public void testTranslationAndModelChecking() {
+
+ //@Test
+ public void testOriginalModel() {
String filePath = getBaseResourcesDir() + PATH_TO_TEST_FILE + "scriptavsysml";
String script;
-
+
outputResult = new StringBuilder();
File f = new File(filePath);
@@ -142,423 +141,4 @@ public class CLIAvatar2SysMLV2Test extends AbstractTest implements InterpreterOu
}
-
-
-
- //@Test
- public void testStateLimitCoffeeMachine() {
- String filePath = getBaseResourcesDir() + PATH_TO_TEST_FILE + "scriptmodelchecker_n";
- String script;
-
- outputResult = new StringBuilder();
-
- File f = new File(filePath);
- assertTrue(myutil.FileUtils.checkFileForOpen(f));
-
- script = myutil.FileUtils.loadFileData(f);
-
- assertTrue(script.length() > 0);
-
- boolean show = false;
- Interpreter interpret = new Interpreter(script, (InterpreterOutputInterface)this, show);
- interpret.interpret();
-
- // Must now load the graph
- filePath = "rgmodelchecker.aut";
- f = new File(filePath);
- assertTrue(myutil.FileUtils.checkFileForOpen(f));
- String data = myutil.FileUtils.loadFileData(f);
-
- assertTrue(data.length() > 0);
- AUTGraph graph = new AUTGraph();
- graph.buildGraph(data);
- graph.computeStates();
-
- System.out.println("states=" + graph.getNbOfStates() + " transitions=" + graph.getNbOfTransitions());
- assertTrue(graph.getNbOfStates() == 12);
- assertTrue(graph.getNbOfTransitions() > 10);
- }
-
- //@Test
- public void testReachabilityLivenessCoffeeMachine() {
- String filePath = getBaseResourcesDir() + PATH_TO_TEST_FILE + "scriptmodelchecker_rl";
- String script;
-
- outputResult = new StringBuilder();
-
- File f = new File(filePath);
- assertTrue(myutil.FileUtils.checkFileForOpen(f));
-
- script = myutil.FileUtils.loadFileData(f);
-
- assertTrue(script.length() > 0);
-
- boolean show = false;
- Interpreter interpret = new Interpreter(script, (InterpreterOutputInterface)this, show);
- interpret.interpret();
-
- // Must now load the graph
- filePath = "rgmodelchecker.aut";
- f = new File(filePath);
- assertTrue(myutil.FileUtils.checkFileForOpen(f));
- String data = myutil.FileUtils.loadFileData(f);
-
- assertTrue(data.length() > 0);
- AUTGraph graph = new AUTGraph();
- graph.buildGraph(data);
- graph.computeStates();
-
- filePath = getBaseResourcesDir() + PATH_TO_EXPECTED_FILE + "modelchecker_rl_expected";
- f = new File(filePath);
- assertTrue(myutil.FileUtils.checkFileForOpen(f));
- String expectedOutput = myutil.FileUtils.loadFileData(f);
-
- System.out.println("states=" + graph.getNbOfStates() + " transitions=" + graph.getNbOfTransitions());
- assertTrue(graph.getNbOfStates() == 14);
- assertTrue(graph.getNbOfTransitions() == 16);
-
- System.out.println("\nExpected:>" + expectedOutput + "<");
- System.out.println("\nObtained:>" + outputResult.toString() + "<");
-
- String s1 = reworkStringForComparison(expectedOutput);
- String s2 = reworkStringForComparison(outputResult.toString());
- assertEquals(s1, s2);
- }
-
- //@Test
- public void testReachabilityLivenessSafetyAirbusDoor_V2() {
- String filePath = getBaseResourcesDir() + PATH_TO_TEST_FILE + "scriptmodelchecker_s";
- String script;
-
- outputResult = new StringBuilder();
-
- File f = new File(filePath);
- assertTrue(myutil.FileUtils.checkFileForOpen(f));
-
- script = myutil.FileUtils.loadFileData(f);
-
- assertTrue(script.length() > 0);
-
- boolean show = false;
- Interpreter interpret = new Interpreter(script, (InterpreterOutputInterface)this, show);
- interpret.interpret();
-
- // Must now load the graph
- filePath = "rgmodelchecker.aut";
- f = new File(filePath);
- assertTrue(myutil.FileUtils.checkFileForOpen(f));
- String data = myutil.FileUtils.loadFileData(f);
-
- assertTrue(data.length() > 0);
- AUTGraph graph = new AUTGraph();
- graph.buildGraph(data);
- graph.computeStates();
-
- filePath = getBaseResourcesDir() + PATH_TO_EXPECTED_FILE + "modelchecker_s_expected";
- f = new File(filePath);
- assertTrue(myutil.FileUtils.checkFileForOpen(f));
- String expectedOutput = myutil.FileUtils.loadFileData(f);
-
- System.out.println("states=" + graph.getNbOfStates() + " transitions=" + graph.getNbOfTransitions());
- assertTrue(graph.getNbOfStates() == 251);
- assertTrue(graph.getNbOfTransitions() > 700);
- assertTrue(graph.getNbOfTransitions() < 770);
-
- String s1 = expectedOutput.trim();
- String s2 = outputResult.toString().trim();
-
- System.out.println("TEST expected=\t>" + s1 + "<\nTEST output:\t>" + s2 + "<");
-
- // Rework string
- s1 = reworkStringForComparison(s1);
- s2 = reworkStringForComparison(s2);
-
- //System.out.println("TEST expected=\t>" + s1 + "<\nTEST output:\t>" + s2 + "<");
-
- /*for(int i=0; i<s1.length(); i++) {
- System.out.println(i + "\t" + s1.substring(i, i+1) + " " + s2.substring(i, i+1));
- }*/
-
- assertTrue(s1.equals(s2));
- }
-
- //@Test
- public void testCoffeeMachine_NoTime() {
- String filePath = getBaseResourcesDir() + PATH_TO_TEST_FILE + "scriptmodelchecker_s_notime";
- String script;
-
- outputResult = new StringBuilder();
-
- File f = new File(filePath);
- assertTrue(myutil.FileUtils.checkFileForOpen(f));
-
- script = myutil.FileUtils.loadFileData(f);
-
- assertTrue(script.length() > 0);
-
- boolean show = false;
- Interpreter interpret = new Interpreter(script, (InterpreterOutputInterface)this, show);
- interpret.interpret();
-
- // Must now load the graph
- filePath = "rgmodelchecker_notime.aut";
- f = new File(filePath);
- assertTrue(myutil.FileUtils.checkFileForOpen(f));
- String data = myutil.FileUtils.loadFileData(f);
-
- assertTrue(data.length() > 0);
- AUTGraph graph = new AUTGraph();
- graph.buildGraph(data);
- graph.computeStates();
-
- System.out.println("states=" + graph.getNbOfStates() + " transitions=" + graph.getNbOfTransitions());
-
- ArrayList<AUTTransition> trs = graph.getTransitions();
- for(AUTTransition tr: trs) {
- //System.out.println("label:" + tr.transition);
- assertTrue(tr.transition.endsWith("[0...0]"));
- }
- }
-
- //@Test
- public void testCoffeeMachine_Time() {
- String filePath = getBaseResourcesDir() + PATH_TO_TEST_FILE + "scriptmodelchecker_s_time";
- String script;
-
- outputResult = new StringBuilder();
-
- File f = new File(filePath);
- assertTrue(myutil.FileUtils.checkFileForOpen(f));
-
- script = myutil.FileUtils.loadFileData(f);
-
- assertTrue(script.length() > 0);
-
- boolean show = false;
- Interpreter interpret = new Interpreter(script, (InterpreterOutputInterface)this, show);
- interpret.interpret();
-
- // Must now load the graph
- filePath = "rgmodelchecker_time.aut";
- f = new File(filePath);
- assertTrue(myutil.FileUtils.checkFileForOpen(f));
- String data = myutil.FileUtils.loadFileData(f);
-
- assertTrue(data.length() > 0);
- AUTGraph graph = new AUTGraph();
- graph.buildGraph(data);
- graph.computeStates();
-
- System.out.println("states=" + graph.getNbOfStates() + " transitions=" + graph.getNbOfTransitions());
-
- //At least one state with different time
- ArrayList<AUTTransition> trs = graph.getTransitions();
- int cpt = 0;
- for(AUTTransition tr: trs) {
- //System.out.println("label:" + tr.transition);
- if (!tr.transition.endsWith("[0...0]")) {
- cpt ++;
- }
- }
- System.out.println("Nb of transition with non-zero time: " + cpt);
- assertTrue(cpt >= 1);
- }
-
- //@Test
- public void testValidateCoffeeMachine() {
- String filePath = getBaseResourcesDir() + PATH_TO_TEST_FILE + "scriptmodelchecker_val1";
- String script;
-
- outputResult = new StringBuilder();
-
- File f = new File(filePath);
- assertTrue(myutil.FileUtils.checkFileForOpen(f));
-
- script = myutil.FileUtils.loadFileData(f);
-
- assertTrue(script.length() > 0);
-
- Interpreter interpret = new Interpreter(script, (InterpreterOutputInterface)this, false);
- interpret.interpret();
-
- assertTrue(outputResult.toString().contains("true"));
- }
-
- //@Test
- public void testValidateAirbusDoor_V2() {
- String filePath = getBaseResourcesDir() + PATH_TO_TEST_FILE + "scriptmodelchecker_val2";
- String script;
-
- outputResult = new StringBuilder();
-
- File f = new File(filePath);
- assertTrue(myutil.FileUtils.checkFileForOpen(f));
-
- script = myutil.FileUtils.loadFileData(f);
-
- assertTrue(script.length() > 0);
-
- Interpreter interpret = new Interpreter(script, (InterpreterOutputInterface)this, false);
- interpret.interpret();
-
- assertTrue(outputResult.toString().contains("true"));
- }
-
- //@Test
- public void testValidatePressureController() {
- String filePath = getBaseResourcesDir() + PATH_TO_TEST_FILE + "scriptmodelchecker_val3";
- String script;
-
- outputResult = new StringBuilder();
-
- File f = new File(filePath);
- assertTrue(myutil.FileUtils.checkFileForOpen(f));
-
- script = myutil.FileUtils.loadFileData(f);
-
- assertTrue(script.length() > 0);
-
- Interpreter interpret = new Interpreter(script, (InterpreterOutputInterface)this, false);
- interpret.interpret();
-
- assertTrue(outputResult.toString().contains("true"));
- }
-
- //@Test
- public void testCoffeeMachineAsync() {
- String filePath = getBaseResourcesDir() + PATH_TO_TEST_FILE + "scriptmodelchecker_val4";
- String script;
-
- outputResult = new StringBuilder();
-
- File f = new File(filePath);
- assertTrue(myutil.FileUtils.checkFileForOpen(f));
-
- script = myutil.FileUtils.loadFileData(f);
-
- assertTrue(script.length() > 0);
-
- Interpreter interpret = new Interpreter(script, (InterpreterOutputInterface)this, false);
- interpret.interpret();
-
- assertTrue(outputResult.toString().contains("true"));
- }
-
- //@Test
- public void testCliCustomQuery () {
- String filePath = getBaseResourcesDir() + PATH_TO_TEST_FILE + "scriptmodelchecker_q";
- String script;
-
- outputResult = new StringBuilder();
-
- File f = new File(filePath);
- assertTrue(myutil.FileUtils.checkFileForOpen(f));
-
- script = myutil.FileUtils.loadFileData(f);
-
- assertTrue(script.length() > 0);
-
- Interpreter interpret = new Interpreter(script, (InterpreterOutputInterface)this, false);
- interpret.interpret();
-
- filePath = getBaseResourcesDir() + PATH_TO_EXPECTED_FILE + "modelchecker_q_expected";
- f = new File(filePath);
- assertTrue(myutil.FileUtils.checkFileForOpen(f));
- String expectedOutput = myutil.FileUtils.loadFileData(f);
-
- assertEquals(expectedOutput, outputResult.toString()+"\n");
- }
-
- //@Test
- public void testAdvancedRandom() {
- System.out.println("advanced random model checker test");
- String filePath = getBaseResourcesDir() + PATH_TO_TEST_FILE + "scriptmodelcheckerrandom";
- String script;
-
- outputResult = new StringBuilder();
-
- File f = new File(filePath);
- assertTrue(myutil.FileUtils.checkFileForOpen(f));
-
- script = myutil.FileUtils.loadFileData(f);
-
- assertTrue(script.length() > 0);
-
- boolean show = false;
- Interpreter interpret = new Interpreter(script, (InterpreterOutputInterface)this, show);
- interpret.interpret();
- System.out.println("Graph generated");
-
- // Must now load the graph
- filePath = "rgmodelcheckerrandom.aut";
- f = new File(filePath);
- assertTrue(myutil.FileUtils.checkFileForOpen(f));
- String data = myutil.FileUtils.loadFileData(f);
-
- assertTrue(data.length() > 0);
- AUTGraph graph = new AUTGraph();
- graph.buildGraph(data);
- graph.computeStates();
-
- System.out.println("random Cstates=" + graph.getNbOfStates() + " transitions=" + graph.getNbOfTransitions());
- assertTrue(graph.getNbOfStates() == 49);
- assertTrue(graph.getNbOfTransitions() == 48);
-
- filePath = "deadlockmodel.txt";
- f = new File(filePath);
- assertTrue(myutil.FileUtils.checkFileForOpen(f));
-
- BufferedReader reader;
- String block = "";
- String state = "";
- try {
- reader = new BufferedReader(new FileReader("deadlockmodel.txt"));
- String line = "";
- while (line != null) {
- // read next line
- line = reader.readLine();
- if (line == null) {
- break;
- }
- TraceManager.addDev("line of file=" + line);
- if (line.startsWith("#")) {
- block = line.trim();
- TraceManager.addDev("Block=" + block);
- }
- if (line.startsWith("-")) {
- state = line.trim();
- assertTrue(checkNames(block, state));
- }
-
- }
- reader.close();
- } catch (IOException e) {
- assertTrue(false);
- }
-
-
-
- }
-
- private boolean checkNames(String blockName, String stateName) {
- TraceManager.addDev("Checking for block=" + blockName + " state=" + stateName);
- boolean blockFound = false;
- for(String s: DEADLOCKS) {
- TraceManager.addDev("s=" + s);
- if (s.compareTo(blockName) == 0) {
- blockFound = true;
- TraceManager.addDev("Found block");
- } else if (blockFound) {
- if (s.startsWith("#")) {
- return false;
- }
- if (s.compareTo(stateName) == 0) {
- TraceManager.addDev("s found");
- return true;
- }
- }
- }
- return false;
- }
-
}
--
GitLab