Completing model-check automation script with result extraction.

[smartthings-infrastructure.git] / ModelCheck.py

diff --git a/ModelCheck.py b/ModelCheck.py
index 601323e0f9012dd5251d395a412c42a05a8238d6..661018e1749353637721c704a8f2fdaea189c586 100644 (file)
--- a/ModelCheck.py
+++ b/ModelCheck.py
@@ -4,6 +4,23 @@ import itertools
 import sys
 import os
 
 import sys
 import os
 

+# Helper methods
+# Check the result in the log and print a summary
+def checkResult(logDirName):
+       extractResult = open(logDirName, "r")
+       result = "other errors--PLEASE CHECK!"
+       
+       for line in extractResult:
+               if "no errors detected" in line:
+                       result = "no conflict"
+                       break
+               elif "java.lang.RuntimeException: Conflict between apps App1 and App2:" in line:
+                       result = "conflict"
+                       break
+       
+       return result
+
+

 # Input parameters:
 # - JPF directory
 # - JPF logs directory
 # Input parameters:
 # - JPF directory
 # - JPF logs directory


@@ -17,6 +34,7 @@ jpfLogDir = sys.argv[2]
 appDir = sys.argv[3]
 firstList = sys.argv[4]
 
 appDir = sys.argv[3]
 firstList = sys.argv[4]
 

+

 # PART 1: Generate the permutations of app pairs
 print "PHASE 1: Extracting the app pairs from the app lists ...\n"
 appList1 = []
 # PART 1: Generate the permutations of app pairs
 print "PHASE 1: Extracting the app pairs from the app lists ...\n"
 appList1 = []


@@ -52,9 +70,13 @@ if useSecondList is False:
 else:
        # Generate pairs from 2 lists
        for i in range(len(appList1)):
 else:
        # Generate pairs from 2 lists
        for i in range(len(appList1)):

-                       for j in range(len(appList2)):
-                               appPairs.append((appList1[i], appList2[j]))
-                       
+               for j in range(len(appList2)):
+                       # Skip if both are the same
+                       if appList1[i] == appList2[j]:
+                               continue
+                       appPairs.append((appList1[i], appList2[j]))
+
+               

 # PART 2: 
 print "PHASE 2: Running JPF ...\n"
 # List down all the log file names
 # PART 2: 
 print "PHASE 2: Running JPF ...\n"
 # List down all the log file names


@@ -63,19 +85,40 @@ for item in appPairs:
 
        # Copy apps into Extractor/App1 and Extractor/App2
        print "==> First app: %s" % item[0]
 
        # Copy apps into Extractor/App1 and Extractor/App2
        print "==> First app: %s" % item[0]

-       print "==> Second app: %s" % item[1]
+       print "==> Second app: %s" % item[1]            

        os.system("cp " + appDir + item[0] + " Extractor/App1/App1.groovy")
        os.system("cp " + appDir + item[1] + " Extractor/App2/App2.groovy")
        
        # Run Runner.py to extract things and create main.groovy, then compile it
        print "==> Compiling the apps ...\n"
        os.system("make Runner")
        os.system("cp " + appDir + item[0] + " Extractor/App1/App1.groovy")
        os.system("cp " + appDir + item[1] + " Extractor/App2/App2.groovy")
        
        # Run Runner.py to extract things and create main.groovy, then compile it
        print "==> Compiling the apps ...\n"
        os.system("make Runner")

-       #os.system("make main")
+       os.system("make main")

        
        # Call JPF
        print "==> Calling JPF and generate logs ...\n"
        
        # Call JPF
        print "==> Calling JPF and generate logs ...\n"

-       logName = jpfLogDir + item[0] + "--" + item[1] + ".log"
-       writeLogList.write(logName + "\n")
-       os.system("cd " + jpfDir + ";./run.sh " + logName + " main.jpf")
-       
+       logName = item[0] + "--" + item[1] + ".log"
+       os.system("cd " + jpfDir + ";./run.sh " + jpfLogDir + logName + " main.jpf")
+       result = checkResult(jpfLogDir + logName)
+       writeLogList.write(logName + "\t\t" + result + "\n")
+

 writeLogList.close()
 writeLogList.close()

+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+