From dcc0f887a11615f3c36b394215117719bb46aaf8 Mon Sep 17 00:00:00 2001
From: rtrimana <rtrimana@uci.edu>
Date: Wed, 24 Jul 2019 12:42:31 -0700
Subject: [PATCH] Adding a script to run automation for model-checking.

---
 ModelCheck.py | 62 +++++++++++++++++++++++++++++++++++++++++++++++++++
 Runner.py     |  3 +++
 2 files changed, 65 insertions(+)
 create mode 100644 ModelCheck.py

diff --git a/ModelCheck.py b/ModelCheck.py
new file mode 100644
index 0000000..145bd22
--- /dev/null
+++ b/ModelCheck.py
@@ -0,0 +1,62 @@
+#!/usr/bin/python
+
+import itertools
+import sys
+import os
+
+# Input parameters:
+# - JPF directory
+# - JPF logs directory
+# - app directory
+# - list #1
+# - list #2 (if needed)
+
+# Index 0 is always for the Python script itself
+jpfDir = sys.argv[1]
+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 = []
+appList2 = []
+# Extract the first list
+extractAppList = open(firstList, "r")
+for app in extractAppList:
+	appList1.append(app.strip())
+extractAppList.close()
+
+# Try to create pairs
+appPairs = []
+# Extract the second list if provided (this is for combinations between two lists)
+if (len(sys.argv) == 6):
+	secondList = sys.argv[5]
+	extractAppList = open(secondList, "r")
+	for app in extractAppList:
+		appList2.append(app.strip())
+	extractAppList.close()
+# 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]))
+
+# PART 2: 
+print "PHASE 2: Running JPF ...\n"
+for item in appPairs:
+	# Copy apps into Extractor/App1 and Extractor/App2	
+	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"
+	os.system("cd " + jpfDir + ";./run.sh " + jpfLogDir + item[0] + "--" + item[1] + ".log" + " main.jpf")
diff --git a/Runner.py b/Runner.py
index d3d7c16..2309a88 100644
--- a/Runner.py
+++ b/Runner.py
@@ -71,6 +71,9 @@ Out.write("import SpeechSynthesis.SpeechSynthesises\n")
 Out.write("import Event.Event\n")
 Out.write("import Timer.SimulatedTimer\n")
 Out.write("\n")
+Out.write("//JPF's Verify API\n")
+Out.write("import gov.nasa.jpf.vm.Verify\n")
+Out.write("\n")
 Out.write("//Global eventHandler\n")
 for line in eventHandler:
 	Out.write(line)
-- 
2.34.1