Pvspec generation and checking procedure without order

ttool/src/test/java/ui/AvatarSecurityTests.java

 package ui;
 
+import avatartranslator.AvatarSpecification;
+import avatartranslator.toproverif.AVATAR2ProVerif;
 import common.ConfigurationTTool;
 import common.SpecConfigTTool;
+import myutil.FileException;
+import myutil.FileUtils;
+import myutil.TraceManager;
 import org.junit.BeforeClass;
 import org.junit.Test;
+import proverifspec.ProVerifSpec;
 
 import java.io.*;
+import java.util.ArrayList;
+import java.util.List;
 
-import static org.junit.Assert.assertNull;
-import static org.junit.Assert.assertTrue;
+import static org.junit.Assert.*;
 
 public class AvatarSecurityTests extends AbstractUITest {
 
@@ -16,7 +23,11 @@ public class AvatarSecurityTests extends AbstractUITest {
     final static String INPUT_FOLDER = "input/";
     final static String GOLDEN_SUFFIX = "_golden";
     final static String OUTPUT_FOLDER = "output/";
+    final static String PVSPEC_SUFFIX = "_pvspec";
     static String OUTPUT_DIR;
+    static final String PROVERIF_SUMMARY = "Verification summary:";
+    static final String PROVERIF_QUERY_PREFIX = "Query";
+
 
     final static String[] MODELS = {
             "AliceAndBob",
@@ -51,45 +62,74 @@ public class AvatarSecurityTests extends AbstractUITest {
         }
     }
 
-    private void runTest(String model){
+    private void runTest(String model) {
+        TraceManager.addDev("Start testing " + model);
+
         openModel(model);
+        AvatarSpecification avatarSpecification = mainGUI.gtm.getAvatarSpecification();
         mainGUI.checkModelingSyntax(true);
-        mainGUI.avatarProVerifVerification();
 
-        // TODO click on start button
+        String pvspecPath = OUTPUT_DIR + model + PVSPEC_SUFFIX;
+        boolean pvspecGenerated = mainGUI.gtm.generateProVerifFromAVATAR(pvspecPath, 0, true, true);
+        assertTrue(pvspecGenerated);
 
-        String cmd = "proverif -in pitype " + OUTPUT_DIR + "pvspec";
+
+        String cmd = "proverif -in pitype " + pvspecPath;
         String goldenPath = INPUT_DIR + model + GOLDEN_SUFFIX;
         Process process;
         BufferedReader cmdOutput;
 
-
         try {
             process = Runtime.getRuntime().exec(cmd);
             cmdOutput = new BufferedReader(new InputStreamReader(process.getInputStream()));
 
-            BufferedReader goldenFile = new BufferedReader(new FileReader(goldenPath));
+            List<String> golden = generateGoldenList(goldenPath);
 
             String outputLine;
-            String goldenLine = null;
-            boolean result = true;
+            int checked = 0;
+            boolean summaryFound = false;
 
             while ((outputLine = cmdOutput.readLine()) != null){
-                if(outputLine.contains("RESULT")){
-                    goldenLine = goldenFile.readLine();
 
-                    if (!outputLine.equals(goldenLine)) {
-                        result = false;
-                        break;
+                if (summaryFound){
+                    if(outputLine.startsWith(PROVERIF_QUERY_PREFIX)){
+                        if (golden.contains(outputLine)) {
+                            checked += 1;
+                        } else {
+                            checked = -1;
+                            break;
+                        }
+                    }
+
+                } else {
+                    if (outputLine.contains(PROVERIF_SUMMARY)){
+                        summaryFound = true;
                     }
                 }
             }
-            goldenLine = goldenFile.readLine();
-            assertTrue(result);
-            assertNull(goldenLine); // check if golden was entirely read
+            assertEquals(golden.size(), checked);
+
+        } catch (Exception e) {
+            throw new RuntimeException(e);
+        }
+    }
 
-        } catch (IOException e) {
+    private List<String> generateGoldenList(String goldenPath) throws IOException {
+        BufferedReader goldenFile = null;
+        try {
+            goldenFile = new BufferedReader(new FileReader(goldenPath));
+        } catch (FileNotFoundException e) {
+            TraceManager.addDev("File " + goldenPath + " not found");
             throw new RuntimeException(e);
         }
+        List<String> goldenList = new ArrayList<>();
+        String line;
+        while ((line = goldenFile.readLine()) != null){
+            if (line.startsWith(PROVERIF_QUERY_PREFIX))
+                goldenList.add(line);
+        }
+        return goldenList;
     }
+
 }
+

ttool/src/test/resources/ui/avatarsecuritytests/input/AliceAndBob_golden

-RESULT not attacker(Alice___secretData[!1 = v]) is true.
-RESULT not event(enteringState___Alice___makingMessage) is false.
-RESULT not event(enteringState___Alice___sendingMessage) is false.
-RESULT not event(enteringState___Alice___beforeFinish) is false.
-RESULT not event(enteringState___Bob___waitingForMessage) is false.
-RESULT not event(enteringState___Bob___messageDecrypt) is false.
-RESULT not event(enteringState___Bob___messageDecrypted) is false.
-RESULT not event(enteringState___Bob___SecretDataReceived) is false.
-RESULT inj-event(authenticity___Bob___m__data___messageDecrypted(dummyM)) ==> inj-event(authenticity___Alice___m__data___sendingMessage(dummyM)) is false.
-RESULT (but event(authenticity___Bob___m__data___messageDecrypted(dummyM)) ==> event(authenticity___Alice___m__data___sendingMessage(dummyM)) is true.)
+--------------------------------------------------------------
+Verification summary:
+
+Query not attacker(Alice___secretData[!1 = v]) is true.
+
+Query not event(enteringState___Alice___makingMessage) is true.
+
+Query not event(enteringState___Alice___sendingMessage) is true.
+
+Query not event(enteringState___Alice___beforeFinish) is true.
+
+Query not event(enteringState___Bob___waitingForMessage) is true.
+
+Query not event(enteringState___Bob___messageDecrypt) is true.
+
+Query not event(enteringState___Bob___messageDecrypted) is true.
+
+Query not event(enteringState___Bob___SecretDataReceived) is true.
+
+Query inj-event(authenticity___Bob___m__data___messageDecrypted(dummyM)) ==> inj-event(authenticity___Alice___m__data___sendingMessage(dummyM)) is false.
+
+--------------------------------------------------------------