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

diff --git a/ModelCheck.py b/ModelCheck.py
index d00c699..1a0c940 100644
--- a/ModelCheck.py
+++ b/ModelCheck.py
@@ -17,10 +17,31 @@ def checkResult(logDirName):
 		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
@@ -92,12 +113,18 @@ for item in appPairs:
 	# 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"
+	error = extractError()
 	logName = item[0] + "--" + item[1] + ".log"
-	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")