- A large number of fixes and additions to the test programs.

* More default options (e.g. --program)
  * Results testing
- Added a heuristics comparison test.
This commit is contained in:
ccremers 2005-03-11 13:44:16 +00:00
parent 391033ec3e
commit ee0e401190
4 changed files with 158 additions and 2 deletions

72
test/compareheuristics.py Executable file
View File

@ -0,0 +1,72 @@
#!/usr/bin/python
#
# Compare heuristics
#
import sys
from optparse import OptionParser
import scythertest
# Parse
def parse(scout):
ra = 0
rb = 0
rp = 0
nc = 0
for l in scout.splitlines():
data = l.split()
if len(data) > 6 and data[0] == 'claim':
nc = nc + 1
tag = data[6]
if tag == 'failed:':
ra = ra + 1
if tag == 'correct:':
if l.rfind("complete_proof") != -1:
rp = rp + 1
else:
rb = rb + 1
return (ra,rb,rp,nc)
# Test with a goal selector
def test_goal_selector(goalselector):
import protocollist
scythertest.set_extra_parameters("--goal-select=" + str(goalselector))
result = str(goalselector)
plist = protocollist.from_literature()
np = len(plist)
attacks = 0
bounds = 0
proofs = 0
claims = 0
for p in plist:
(status,scout) = scythertest.default_test([p],0,0)
(ra,rb,rp,nc) = parse(scout)
attacks = attacks + ra
bounds = bounds + rb
proofs = proofs + rp
claims = claims + nc
return (attacks,bounds,proofs,claims,np)
# Main code
def main():
parser = OptionParser()
scythertest.default_options(parser)
(options, args) = parser.parse_args()
scythertest.process_default_options(options)
print "G-sel\tAttack\tBound\tProof"
print
for g in range(1,31):
(ra,rb,rp,nc,np) = test_goal_selector(g)
print str(g) + "\t" + str(ra) + "\t" + str(rb) + "\t" + str(rp) + "\t" + str(nc)
print
print "Goal selector scan completed."
# Only if main stuff
if __name__ == '__main__':
main()

View File

@ -537,6 +537,7 @@ def main():
help = "suppress a progress bar")
(options, args) = parser.parse_args()
scythertest.process_default_options(options)
the_great_houdini(args, int(options.tuplewidth), int(options.match))

View File

@ -21,6 +21,19 @@ from tempfile import NamedTemporaryFile, gettempdir
# Minimum duration for a test to get into the cache (in seconds)
CacheTimer = 0.1
ScytherProgram = "scyther"
#----------------------------------------------------------------------------
# How to override Scyther program setting
#----------------------------------------------------------------------------
def scytheroverride (newprg):
global ScytherProgram
ScytherProgram = newprg
if not os.path.exists(ScytherProgram):
print "Cannot find any file at", ScytherProgram, " and it cannot be used as a Scyther executable."
sys.exit()
#----------------------------------------------------------------------------
# How to call Scyther
@ -28,7 +41,9 @@ CacheTimer = 0.1
# scyther should reside in $PATH
def scythercall (argumentstring, inputfile):
clstring = "scyther " + argumentstring + " " + inputfile
global ScytherProgram
clstring = ScytherProgram + " " + argumentstring + " " + inputfile
(status,scout) = commands.getstatusoutput(clstring)
return (status,scout)

View File

@ -6,7 +6,13 @@
#
import sys
from optparse import OptionParser
from scythercache import evaluate
from scythercache import evaluate, scytheroverride
#----------------------------------------------------------------------------
# Globals
#----------------------------------------------------------------------------
g_extra = ""
#----------------------------------------------------------------------------
# Parsing Output
@ -47,6 +53,26 @@ def default_protocols(plist):
plist.sort()
return ['../spdl/spdl-defaults.inc'] + plist
# Get the extra parameters
def get_extra_parameters():
global g_extra
return g_extra
# Set the extra parameters
def set_extra_parameters(args):
global g_extra
g_extra = args
# Add the extra parameters
def add_extra_parameters(args):
global g_extra
if args != "":
if g_extra != "":
g_extra = g_extra + " "
g_extra = g_extra + args
# Yield arguments, given a bound type:
# 0: fast
@ -78,6 +104,10 @@ def default_arguments(plist,match,bounds):
args = "--arachne --timer=%i --max-runs=%i --max-length=%i" % (timer, maxruns, maxlength)
matching = "--match=" + str(match)
allargs = "--summary " + matching + " " + args
extra = get_extra_parameters()
if extra != "":
allargs = extra + " " + allargs
return allargs
# Yield test results
@ -115,6 +145,23 @@ def default_options(parser):
parser.add_option("-b","--bounds", dest="bounds",
default = 0,
help = "bound type selection (0: quickscan, 1:thorough)")
parser.add_option("-x","--extra", dest="extra",
default = "",
help = "add arguments to pass to Scyther")
parser.add_option("-P","--program", dest="program",
default = "",
help = "define alternative scyther executable")
# Process the default options
def process_default_options(options):
if options.program != "":
scytheroverride(options.program)
print "Using", options.program, "as Scyther executable."
if options.extra != "":
add_extra_parameters(options.extra)
print "Added extra options, now:", get_extra_parameters(options.extra)
#----------------------------------------------------------------------------
# Some default testing stuff
@ -130,6 +177,18 @@ def all_unless_given(plist):
# Scan for compilation errors or stuff like that
def scan_for_results(options,args):
# Select specific list
plist = all_unless_given(args)
# Now check all things in the list
for p in plist:
# Test and gather output
(status,scout) = default_test([p], 0, 0)
print scout
print
print "Scan complete."
def scan_for_errors(options,args):
# Select specific list
plist = all_unless_given(args)
@ -205,15 +264,24 @@ def main():
default = "False",
action = "store_true",
help = "detect compilation errors for all protocols [in list_all]")
parser.add_option("-r","--results", dest="results",
default = "False",
action = "store_true",
help = "scan for results for all protocols [in list_all]")
parser.add_option("-t","--timeouts", dest="timeouts",
default = "False",
action = "store_true",
help = "scan for timeout errors for all protocols [in list_all]")
(options, args) = parser.parse_args()
# Globals
process_default_options(options)
# Subcases
if options.errors != "False":
scan_for_errors(options,args)
elif options.results != "False":
scan_for_results(options,args)
elif options.timeouts != "False":
scan_for_timeouts(options,args)
else: