X-Git-Url: http://plrg.eecs.uci.edu/git/?p=smartthings-infrastructure.git;a=blobdiff_plain;f=ModelCheck.py;h=1a0c940bb66ff273d3fc6300b4914d8879f940c5;hp=82c6adffeffe847fe202635448f8659031b161db;hb=c97f75cb3ddb7ae3196f38967adaa3439b2315c2;hpb=4f9a1209b0c1ca5caf60a0f811e18dde6a92e9e9

diff --git a/ModelCheck.py b/ModelCheck.py
index 82c6adf..1a0c940 100644
--- 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,6 +55,7 @@ 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"
 appList1 = []
@@ -30,6 +69,7 @@ extractAppList.close()
 
 # Try to create pairs
 appPairs = []
+useSecondList = False
 # Extract the second list if provided (this is for combinations between two lists)
 if (len(sys.argv) == 6):
 	secondList = sys.argv[5]
@@ -38,34 +78,69 @@ if (len(sys.argv) == 6):
 		if '#' not in app:
 			appList2.append(app.strip())
 	extractAppList.close()
+	useSecondList = True
 # Just copy the first list to the second list
 else:
 	appList2 = appList1
 
-# Generate the permutations of pairs
-for i in range(len(appList1)):
-	for j in range(i + 1, len(appList2)):
-		appPairs.append((appList1[i], appList2[j]))
+if useSecondList is False:
+	# Generate the permutations of pairs
+	for i in range(len(appList1)):
+		for j in range(i + 1, len(appList2)):
+			appPairs.append((appList1[i], appList2[j]))
+else:
+	# Generate pairs from 2 lists
+	for i in range(len(appList1)):
+		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
 writeLogList = open(jpfLogDir + "logList", "w+")
 for item in appPairs:
 
-	# Copy apps into Extractor/App1 and Extractor/App2	
+	# Copy apps into Extractor/App1 and Extractor/App2
+	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"
 	os.system("make Runner")
-	os.system("make main")
-	
-	# 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")
-	
+	error = extractError()
+	logName = item[0] + "--" + item[1] + ".log"
+	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()
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+