scyther/test/boundanalyze.py

85 lines
2.0 KiB
Python
Raw Normal View History

2006-07-01 10:34:37 +01:00
#!/usr/bin/python
import os
2006-07-01 10:48:06 +01:00
firstbroken = {}
def analyze(file,bound):
2006-07-01 10:34:37 +01:00
claim = 0
correct = 0
attack = 0
boundokay = 0
notoccurs = 0
if os.path.isfile(file):
fp = open(file,'r')
for l in fp.readlines():
if l.startswith("claim"):
claim = claim + 1
2006-07-01 10:48:06 +01:00
dt = l.split('\t')
claimid = "%s,%s" % (dt[1],dt[2])
2006-07-01 10:34:37 +01:00
if l.find("\tFail\t") >= 0:
attack = attack + 1
2006-07-01 10:48:06 +01:00
if claimid not in firstbroken.keys():
firstbroken[claimid] = bound
2006-07-01 10:34:37 +01:00
else:
if l.find("bounds") >= 0:
boundokay = boundokay + 1
else:
if l.find("proof") >= 0:
correct = correct + 1
else:
if l.find("does not occur") >= 0:
notoccurs = notoccurs + 1
else:
print "Huh? ", l.strip()
fp.close()
if claim > 0:
ratio = (100.0 * (attack+correct)) / claim
print "[%s]\t%i\t%i\t%i\t%s%%" % (file, claim,attack,correct, str(ratio))
def timed(file):
if os.path.isfile(file):
fp = open(file,'r')
for l in fp.readlines():
l = l.strip()
if l.find("User time (seconds)") >= 0:
x = l.find(":")
time = float(l[(x+1):])
print file, time
return
print file, " no time found"
def all():
print "prot\t\t\tclaims\tattacks\tcorrect\tdecided"
2006-07-01 10:34:37 +01:00
for i in range(1,8):
2006-07-01 10:48:06 +01:00
analyze("boundruns%i.txt" % (i),i)
print
2006-07-01 10:34:37 +01:00
for i in range(1,8):
timed("boundtime%i.txt" % (i))
print
2006-07-01 10:48:06 +01:00
for i in range(1,8):
l = []
for k in firstbroken.keys():
if firstbroken[k] == i:
l.append(k)
print "Attack with %i runs:" % i
print l
2006-07-01 10:34:37 +01:00
all()