- Added some further tests.
This commit is contained in:
parent
c52a340d8e
commit
7686ea4f64
62
test/boundanalyze.py
Executable file
62
test/boundanalyze.py
Executable file
@ -0,0 +1,62 @@
|
||||
#!/usr/bin/python
|
||||
|
||||
import os
|
||||
|
||||
def analyze(file):
|
||||
|
||||
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
|
||||
if l.find("\tFail\t") >= 0:
|
||||
attack = attack + 1
|
||||
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():
|
||||
for i in range(1,8):
|
||||
analyze("boundruns%i.txt" % (i))
|
||||
for i in range(1,8):
|
||||
timed("boundtime%i.txt" % (i))
|
||||
|
||||
all()
|
||||
|
||||
|
||||
|
||||
|
12
test/boundtest.sh
Executable file
12
test/boundtest.sh
Executable file
@ -0,0 +1,12 @@
|
||||
#!/bin/sh
|
||||
|
||||
rm boundtime?.txt
|
||||
rm boundruns?.txt
|
||||
|
||||
\time -v -o boundtime1.txt ./test-all.sh scyther -r1 --plain >boundruns1.txt
|
||||
\time -v -o boundtime2.txt ./test-all.sh scyther -r2 --plain >boundruns2.txt
|
||||
\time -v -o boundtime3.txt ./test-all.sh scyther -r3 --plain >boundruns3.txt
|
||||
\time -v -o boundtime4.txt ./test-all.sh scyther -r4 --plain >boundruns4.txt
|
||||
\time -v -o boundtime5.txt ./test-all.sh scyther -r5 --plain >boundruns5.txt
|
||||
\time -v -o boundtime6.txt ./test-all.sh scyther -r6 --plain >boundruns6.txt
|
||||
\time -v -o boundtime7.txt ./test-all.sh scyther -r6 --plain >boundruns7.txt
|
@ -198,7 +198,8 @@ def main():
|
||||
sharedproblems = []
|
||||
firstproblem = True
|
||||
|
||||
for g in range(1,8):
|
||||
for g in range(-1,512):
|
||||
if (g != 0) and ((g == -1) or ((g & (64+16+8+4+1)) == 0)):
|
||||
(ra,rb,rp,nc,np,st,timeouts,prot_undec) = test_goal_selector(g, options,
|
||||
boundstatesmax.get())
|
||||
|
||||
|
@ -152,17 +152,9 @@ def select(type):
|
||||
|
||||
|
||||
def main():
|
||||
(good, bad, others) = make_lists()
|
||||
|
||||
def show (tag, list):
|
||||
print tag + " (%i)" % len(list)
|
||||
print
|
||||
for l in list:
|
||||
print l
|
||||
|
||||
show ("Good", good)
|
||||
show ("Bad", bad)
|
||||
show ("Others", others)
|
||||
l = from_all()
|
||||
for f in l:
|
||||
print f
|
||||
|
||||
|
||||
if __name__ == '__main__':
|
||||
|
4
test/test-all.sh
Executable file
4
test/test-all.sh
Executable file
@ -0,0 +1,4 @@
|
||||
#!/bin/sh
|
||||
|
||||
./protocollist.py | xargs -n 1 $*
|
||||
|
5
test/test-one.sh
Executable file
5
test/test-one.sh
Executable file
@ -0,0 +1,5 @@
|
||||
#!/bin/sh
|
||||
|
||||
echo $*
|
||||
|
||||
scyther $*
|
Loading…
Reference in New Issue
Block a user