Newer
Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
#!/bin/python
# This script tests a file containing a list of GR(1) assumptions, one per line.
# It computes d1 and d2 of their conjunction
# Syntax: $ python testFileExample <src_file>
import sys
import timeit
import Weakness.src.weakness as w
import ref_utils.io_utils as io
infile = open(sys.argv[1],"r")
varfile = open(sys.argv[1]+"_vars","r")
phi = " & ".join([x.strip() for x in infile.readlines() if x[0:2] != "//" and x != ""])
#gr1_units = [x.strip() for x in infile.readlines() if x[0:2] != "//" and x != ""]
# subformulae = gr1_units
# while subformulae.__len__() > 5:
# nextsubformulae = []
# remainderformulae = subformulae[-1:-(subformulae.__len__() % 5) - 1]
# for i in range(0,subformulae.__len__()/5):
# nextsubformulae.append('('+' & '.join(subformulae[5*i:5+5*i])+')')
# if remainderformulae.__len__() > 0:
# nextsubformulae.append('('+' & '.join(remainderformulae)+')')
# subformulae = nextsubformulae
#
# phi = subformulae[0]
vars = varfile.readlines()
vars = map(lambda x: x.strip(),vars)
print "vars: " + str(vars)
print "phi: "+ io.normalizeSpinFormulaSyntax(phi)
starttime = timeit.default_timer()
d2 = w.computeD2(phi,vars)
print "d2 = " + str(d2)
d1 = w.computeD1(phi,vars)
elapsed = timeit.default_timer() - starttime
print "d1 = " + str(d1)
print "time = " + str(elapsed)