diff --git a/ttool/src/test/java/pragmasmodel/AliceAndBobPragmasTest.java b/ttool/src/test/java/pragmasmodel/AliceAndBobPragmasTest.java
index 9efc4da3236ae060503874180e2b56d08b0558fa..8b85ed7df0896607242415be2bb7764fa25266d0 100644
--- a/ttool/src/test/java/pragmasmodel/AliceAndBobPragmasTest.java
+++ b/ttool/src/test/java/pragmasmodel/AliceAndBobPragmasTest.java
@@ -4,6 +4,7 @@ import myutil.FileException;
import myutil.FileUtils;
import myutil.TraceManager;
import org.junit.Assert;
+import org.junit.Before;
import org.junit.BeforeClass;
import org.junit.Test;
@@ -15,19 +16,20 @@ public class AliceAndBobPragmasTest {
private static AvatarNetworkProjectPragmaTests parent;
- private static HashMap<String, String[]> resultList;
+ private static HashMap<String, String[]> goldenList;
private static ArrayList<String> resultsToBeChecked;
- private static String currentTabbedPane;
+ private static final ArrayList<String> tabbedPanes = new ArrayList<>(Arrays.asList("SymExchangeArch"));;
+ private static int currentIdxTabbedPane = -1;
- //@BeforeClass
+
+ @BeforeClass
public static void setUp() {
parent = new AvatarNetworkProjectPragmaTests();
- parent.setProjectName("AliceAndBob");
- parent.buildTMAPPattern();
- resultList = new HashMap<String, String[]>();
+ parent.setProjectName("AliceAndBobHW");
+ goldenList = new HashMap<String, String[]>();
resultsToBeChecked = new ArrayList<>();
}
@@ -35,9 +37,6 @@ public class AliceAndBobPragmasTest {
@BeforeClass
public static void setUpGolden() throws FileException {
- //Buid ArrayList of the String name Pane
- ArrayList<String> tabbedPanes = new ArrayList<>(Arrays.asList("SymExchangeArch"));
-
String path = "test/resources/pragmasmodel/AliceAndBobHW/";
for (String tabbedPane : tabbedPanes){
@@ -45,18 +44,18 @@ public class AliceAndBobPragmasTest {
TraceManager.addDev("tabbedPane : " + tabbedPane);
String fileContent = FileUtils.loadFile(path + tabbedPane + "/golden");
- resultList.put(tabbedPane,fileContent.split("\n"));
+ goldenList.put(tabbedPane,fileContent.split("\n"));
}
}
- //@Before
+ @Before
public void switchTabbedPane() throws Exception {
- //currentTabbedPane = parent.switchTab();
+ //no index out of bounds because runs x times if x @Test. x Must be same length as tabbedPanes.size()
+ currentIdxTabbedPane+=1;
- parent.checkPragmas();
- parent.generatePvspec();
+ parent.buildPvspec(tabbedPanes.get(currentIdxTabbedPane));
parent.runProverif();
resultsToBeChecked = parent.getResultsToBeChecked();
@@ -65,22 +64,17 @@ public class AliceAndBobPragmasTest {
@Test
public void testPragmaResult_1(){
- iterateOverArrayList(currentTabbedPane);
+ iterateOverArrayList(tabbedPanes.get(currentIdxTabbedPane));
}
- @Test
- public void test(){
- }
public void iterateOverArrayList(String key){
- String[] resultsGolden = resultList.get(key);
+ String[] golden = goldenList.get(key);
- if (resultsGolden.length != resultsToBeChecked.size()){
- Assert.assertTrue(false);
- }
+ Assert.assertEquals(golden.length, resultsToBeChecked.size());
- for (int i = 0; i < resultsGolden.length; i++) {
- Assert.assertEquals(resultsGolden[i],resultsToBeChecked.get(i));
+ for (int i = 0; i < golden.length; i++) {
+ Assert.assertEquals(golden[i],resultsToBeChecked.get(i));
}
}
diff --git a/ttool/src/test/java/pragmasmodel/AvatarNetworkProjectPragmaTests.java b/ttool/src/test/java/pragmasmodel/AvatarNetworkProjectPragmaTests.java
index 3c3646c81b407898869f9c14de5a515df220cd5f..ad1bc316d79111c3aa6a4c87bc7410c7b53a94ca 100644
--- a/ttool/src/test/java/pragmasmodel/AvatarNetworkProjectPragmaTests.java
+++ b/ttool/src/test/java/pragmasmodel/AvatarNetworkProjectPragmaTests.java
@@ -1,22 +1,38 @@
package pragmasmodel;
+import avatartranslator.AvatarSpecification;
+import avatartranslator.toproverif.AVATAR2ProVerif;
import common.ConfigurationTTool;
import common.SpecConfigTTool;
import launcher.LauncherException;
import launcher.RshClient;
import launcher.RshClientReader;
+import myutil.FileException;
+import myutil.FileUtils;
+import myutil.MalformedConfigurationException;
import myutil.TraceManager;
import proverifspec.ProVerifOutputAnalyzer;
+import proverifspec.ProVerifSpec;
+import tmltranslator.TMLMapping;
+import tmltranslator.TMLMappingTextSpecification;
+import tmltranslator.TMLSyntaxChecking;
+import tmltranslator.patternhandling.PatternIntegration;
+import tmltranslator.toavatarsec.TML2Avatar;
import ui.AbstractUITest;
import ui.AvatarDesignPanel;
+import ui.TGComponent;
import ui.TGUIAction;
import ui.networkmodelloader.NetworkModel;
import java.io.BufferedReader;
+import java.io.File;
import java.io.IOException;
+import java.io.InputStreamReader;
import java.util.ArrayList;
-public class AvatarNetworkProjectPragmaTests extends AbstractUITest {
+import static org.junit.Assert.assertTrue;
+
+public class AvatarNetworkProjectPragmaTests {
protected static String PROJECT_NAME="";
@@ -29,83 +45,95 @@ public class AvatarNetworkProjectPragmaTests extends AbstractUITest {
private ProVerifOutputAnalyzer pvoa;
+ protected static String currentTabbedPane;
- public AvatarNetworkProjectPragmaTests() {super();}
-
- public void buildTMAPPattern() {
+ protected static String currentFolderPath;
- }
- public void setProjectName(String projectName){
- PROJECT_NAME=projectName;
- }
+ public AvatarNetworkProjectPragmaTests() {}
- public void switchTab(){
+ private TMLMapping<?> buildTMAPPattern() {
+ resultsToBeChecked = new ArrayList<>();
+ currentFolderPath = "test/resources/pragmasmodel/" + PROJECT_NAME + "/" + currentTabbedPane + "/";
+ String filename = "spec";
+ TMLMappingTextSpecification<Class<?>> tmts = new TMLMappingTextSpecification<Class<?>>(filename);
+ File f = new File(currentFolderPath + filename + ".tmap");
+ String spec = null;
+ try {
+ spec = FileUtils.loadFileData(f);
+ } catch (Exception e) {
+ System.out.println("Exception executing: loading " + currentTabbedPane);
+ }
+ boolean parsed = tmts.makeTMLMapping(spec, currentFolderPath);
+ TMLMapping<?> _tmapPattern = tmts.getTMLMapping();
+ // Checking syntax
+ TMLSyntaxChecking syntax = new TMLSyntaxChecking(_tmapPattern);
+ syntax.checkSyntax();
+ return _tmapPattern;
}
+ public void buildPvspec(String _currentTabbedPane) throws FileException {
+
+ currentTabbedPane = _currentTabbedPane;
+ TMLMapping<?> _tmapPattern = buildTMAPPattern();
+ //null for _referenceObject ?
+ Object o = null;
+ if (_tmapPattern.getTMLModeling().getReference() instanceof TGComponent) {
+ o = ((TGComponent)(_tmapPattern.getTMLModeling().getReference())).getTDiagramPanel().tp;
+ }
+ TML2Avatar tml2Avatar = new TML2Avatar(_tmapPattern,false,false,o);
+ AvatarSpecification avatarspec = tml2Avatar.generateAvatarSpec("1",true);
+ AVATAR2ProVerif avatar2proverif = new AVATAR2ProVerif(avatarspec);
+ ProVerifSpec proverif = avatar2proverif.generateProVerif(true, true, 0, true,
+ true);
- public void runProverif() throws LauncherException {
+ String filename = currentFolderPath + "pvspec";
+ FileUtils.saveFile(filename, proverif.getStringSpec());
- String cmd = "";
- cmd += ConfigurationTTool.ProVerifVerifierPath;
- cmd += " -in pitype ";
- cmd += pvspecPath;
- TraceManager.addDev("Executing command:" + cmd);
+ }
- rshc = new RshClient(ConfigurationTTool.ProVerifVerifierHost);
- rshc.setCmd(cmd);
- rshc.sendExecuteCommandRequest();
- RshClientReader reader = rshc.getDataReaderFromProcess();
+ public void setProjectName(String projectName){
+ PROJECT_NAME=projectName;
+ }
-// this.pvoa = mainGUI.gtm.getProVerifOutputAnalyzer();
-// this.pvoa.analyzeOutput(reader, true);
+ public void runProverif() throws MalformedConfigurationException {
+ String filename = currentFolderPath + "pvspec";
String str;
- BufferedReader bReader = new BufferedReader(reader);
+ ConfigurationTTool.loadConfiguration("/home/kali/Documents/Eurecom/SemesterProject/TTool/bin/config.xml",false);
+ String cmd = "/bin/bash -c \'" + ConfigurationTTool.ProVerifVerifierPath + " -in pitype " + filename + " |grep RESULT\'";
- try {
- StringBuffer sb = new StringBuffer("");
- // Loop through every line in the output
- while ((str = bReader.readLine()) != null) {
- sb.append(str + "\n");
+ TraceManager.addDev("proverif path : " + ConfigurationTTool.ProVerifVerifierPath);
+ TraceManager.addDev("Executing command " + cmd);
- if (str.isEmpty())
- continue;
+ try {
+ ProcessBuilder processBuilder = new ProcessBuilder("/bin/bash", "-c", cmd);
+ processBuilder.redirectErrorStream(true);
+ Process process = processBuilder.start();
+ BufferedReader process_in = new BufferedReader(new InputStreamReader(process.getInputStream()));
- //TraceManager.addDev("Analyzing trace:" + str);
+ while ((str = process_in.readLine()) != null) {
+ TraceManager.addDev("Output proverif : " + str);
+ resultsToBeChecked.add(str);
- // Found a line with a RESULT
- if (str.startsWith("RESULT ")) {
- // Remove 'RESULT ' at the begining
- str = str.substring(7);
- resultsToBeChecked.add(str);
- }
}
- } catch (IOException e) {
- TraceManager.addDev("readLine error");
+ } catch (Exception e) {
+ TraceManager.addDev("FAILED: executing: " + cmd + ": " + e.getMessage());
}
+
}
public void generatePvspec(){
pvspecPath = SpecConfigTTool.ProVerifCodeDirectory += "pvspec";
- mainGUI.gtm.generateProVerifFromAVATAR(
- pvspecPath,
- 1,
- true,
- true,
- "1");
-
}
public void checkPragmas() throws Exception {
- if (!mainGUI.checkModelingSyntax(mainGUI.getCurrentTURTLEPanel(),true)){
- throw new Exception();
- }
+
}
public ArrayList<String> getResultsToBeChecked(){