Merge branch 'oldInfraNewAnalysis' of ssh://plrg.eecs.uci.edu/home/git/smartthings...

[smartthings-infrastructure.git] / ModelCheck.py

diff --git a/ModelCheck.py b/ModelCheck.py
index c192cfa48ecafe72be736fc997adcd6bb9a33ef1..443fc82255669c95aee4823b594662b7ffc72555 100644 (file)
--- a/ModelCheck.py
+++ b/ModelCheck.py
@@ -4,6 +4,44 @@ import itertools
 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
+               elif "Direct-Direct Interaction detected:" in line:
+                       result = "direct-direct"
+                       break
+       
+       return result
+
+# Extract the error from specific error logs
+def extractError():
+       err = ""
+       if os.path.exists("appCreationError.log"):
+               extractError = open("appCreationError.log", "r")
+               for line in extractError:
+                       err = err + line
+               extractError.close()
+               os.system("rm appCreationError.log")
+       return err
+
+# Write error log to the log directory
+# In this case we skip running JPF
+# e.g., in the case of having a direct-direct interaction pair
+def writeErrorLog(jpfLogDir, logName, error):
+       writeError = open(jpfLogDir + logName, "w+")
+       writeError.write(error)
+       writeError.close()
+       
 # Input parameters:
 # - JPF directory
 # - JPF logs directory
@@ -17,8 +55,9 @@ jpfLogDir = sys.argv[2]
 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"
+print("PHASE 1: Extracting the app pairs from the app lists ...\n")
 appList1 = []
 appList2 = []
 # Extract the first list
@@ -57,28 +96,51 @@ else:
                        if appList1[i] == appList2[j]:
                                continue
                        appPairs.append((appList1[i], appList2[j]))
-                       
+
+               
 # PART 2: 
-print "PHASE 2: Running JPF ...\n"
+print("PHASE 2: Running JPF ...\n")
 # List down all the log file names
 writeLogList = open(jpfLogDir + "logList", "w+")
 for item in appPairs:
 
        # Copy apps into Extractor/App1 and Extractor/App2
-       print "==> First app: %s" % item[0]
-       print "==> Second app: %s" % item[1]            
+       print("==> First app: %s" % item[0])
+       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"
+       print("==> Compiling the apps ...\n")
        os.system("make Runner")
-       os.system("make main")
-       
-       # Call JPF
-       print "==> Calling JPF and generate logs ...\n"
+       error = extractError()
        logName = item[0] + "--" + item[1] + ".log"
-       writeLogList.write(logName + "\n")
-       os.system("cd " + jpfDir + ";./run.sh " + jpfLogDir + logName + " main.jpf")
-       
+       if error == "":
+               # Compile
+               os.system("make main")
+               # Call JPF
+               print("==> Calling JPF and generate logs ...\n")
+               os.system("cd " + jpfDir + ";./run.sh " + jpfLogDir + logName + " main.jpf")
+       else:
+               # This is for specific error, e.g., direct-direct interaction that we need to skip
+               writeErrorLog(jpfLogDir, logName, error)
+               
+       result = checkResult(jpfLogDir + logName)
+       writeLogList.write(logName + "\t\t" + result + "\n")
+
 writeLogList.close()
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+