diff --git a/test/compareheuristics.py b/test/compareheuristics.py index 31c6083..63f105d 100755 --- a/test/compareheuristics.py +++ b/test/compareheuristics.py @@ -36,26 +36,33 @@ def parse(scout): # Determine timeout, count states nc += 1 timeout = False + localstates = 0 for d in data: if d.startswith("states="): - st = st + int(d[7:]) + localstates += int(d[7:]) if d.startswith("time="): timeout = True - # Determine claim status + # Only count the states if no timeout (otherwise not + # dependable) if not timeout: - tag = data[4] - if tag == 'Fail': + st += localstates + + # Determine claim status + tag = data[4] + if tag == 'Fail': ra += 1 - elif tag == 'Ok': - if l.rfind("proof of correctness") != -1: - rp += 1 - else: - rb += 1 - else: - print "Weird tag [%s] in line [%s]." % (tag, l) else: - to += 1 + if not timeout: + if tag == 'Ok': + if l.rfind("proof of correctness") != -1: + rp += 1 + else: + rb += 1 + else: + print "Weird tag [%s] in line [%s]." % (tag, l) + else: + to += 1 return (ra,rb,rp,nc,st,to) @@ -79,7 +86,7 @@ def test_goal_selector(goalselector, options,branchbound): global hurry - scythertest.set_extra_parameters("--count-states --heuristic=" + str(goalselector)) + scythertest.add_extra_parameters("--count-states --heuristic=" + str(goalselector)) result = str(goalselector) plist = protocollist.from_literature() np = len(plist) @@ -90,6 +97,7 @@ def test_goal_selector(goalselector, options,branchbound): claims = 0 states = 0 timeouts = 0 + undecidedprotocols = [] for p in plist: (status,scout) = scythertest.default_test([p], \ int(options.match), \ @@ -101,11 +109,14 @@ def test_goal_selector(goalselector, options,branchbound): attacks += ra bounds += rb proofs += rp + # is something undecided for this protocol? + if (rb > 0) or (to > 0): + undecidedprotocols += [p] if hurry and (bounds * states) > branchbound: return (-1,0,0,0,0,0) - return (attacks,bounds,proofs,claims,np,states,timeouts) + return (attacks,bounds,proofs,claims,np,states,timeouts,undecidedprotocols) # Max class maxor: @@ -177,8 +188,12 @@ def main(): timeoutsmax = maxor(2) decidemax = maxor(1) - for g in range(1,16): - (ra,rb,rp,nc,np,st,timeouts) = test_goal_selector(g, options, + problems = {} + sharedproblems = [] + firstproblem = True + + for g in range(1,8): + (ra,rb,rp,nc,np,st,timeouts,prot_undec) = test_goal_selector(g, options, boundstatesmax.get()) res = str(g) @@ -205,9 +220,30 @@ def main(): res = shows (res, statesmax, st) res = shows (res, boundstatesmax, boundstates) + problems[g] = prot_undec + if firstproblem: + firstproblem = False + sharedproblems = prot_undec + else: + nl = [] + for p in sharedproblems: + if p in prot_undec: + nl += [p] + sharedproblems = nl + print res print print "Goal selector scan completed." + print + print "%i shared problem protocols:" % len(sharedproblems) + print sharedproblems + print + for g in problems.keys(): + print g, + print " has %i extra problems: " % (len(problems[g]) - len(sharedproblems)), + print [ p for p in problems[g] if p not in sharedproblems ] + print + print # Only if main stuff if __name__ == '__main__': diff --git a/test/scythercache.py b/test/scythercache.py index 7d6c60a..a47d577 100755 --- a/test/scythercache.py +++ b/test/scythercache.py @@ -1,10 +1,10 @@ #!/usr/bin/python # -# Scyther caching mechanism +# Scyther caching mechanism # -# Uses md5 hashes to store previously calculated results. +# Uses md5 hashes to store previously calculated results. # -# (c)2005 Cas Cremers +# (c)2005 Cas Cremers # # @@ -29,133 +29,134 @@ RetrieveFromCache = True #---------------------------------------------------------------------------- def scytheroverride (newprg): - global ScytherProgram + 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() + 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() def cacheoverride (): - global RetrieveFromCache + global RetrieveFromCache - RetrieveFromCache = False + RetrieveFromCache = False #---------------------------------------------------------------------------- # How to call Scyther #---------------------------------------------------------------------------- -# scyther should reside in $PATH +# scyther should reside in $PATH def scythercall (argumentstring, inputfile): - global ScytherProgram + global ScytherProgram - clstring = ScytherProgram + " " + argumentstring + " " + inputfile - (status,scout) = commands.getstatusoutput(clstring) - return (status,scout) + clstring = ScytherProgram + " " + argumentstring + " " + inputfile + (status,scout) = commands.getstatusoutput(clstring) + return (status,scout) #---------------------------------------------------------------------------- # Cached evaluation #---------------------------------------------------------------------------- -# cached results -# input: a large string (consisting of read input files) -# argstring: a smaller string +# cached results +# input: a large string (consisting of read input files) +# argstring: a smaller string def evaluate (argumentstring, inputstring): - def cacheid(): - m = md5.new() - - # Determine scyther version - (status, scout) = scythercall ("--version", "") - if status == 1 or status < 0: - # some problem - print "Problem with determining scyther version!" - os.exit() - # Add version to hash - m.update (scout) + def cacheid(): + m = md5.new() + + # Determine scyther version + (status, scout) = scythercall ("--version", "") + if status == 1 or status < 0: + # some problem + print "Problem with determining scyther version!" + os.exit() + # Add version to hash + m.update (scout) - # Add inputfile to hash - m.update (inputstring) + # Add inputfile to hash + m.update (inputstring) - # Add arguments to hash - m.update (argumentstring) + # Add arguments to hash + m.update (argumentstring) - # Return a readable ID (good for a filename) - return m.hexdigest() + # Return a readable ID (good for a filename) + return m.hexdigest() - # slashcutter - # Takes 'str': cuts of the first 'depth' strings of length - # 'width' and puts 'substr' in between - def slashcutter(str,substr,width,depth): - res = "" - while len(str)>width and depth>0: - res = res + str[0:width] + substr - str = str[width:] - depth = depth-1 - return res + str + # slashcutter + # Takes 'str': cuts of the first 'depth' strings of length + # 'width' and puts 'substr' in between + def slashcutter(str,substr,width,depth): + res = "" + while len(str)>width and depth>0: + res = res + str[0:width] + substr + str = str[width:] + depth = depth-1 + return res + str - # Determine name - def cachefilename(id): - fn = gettempdir() + "/scyther/" - fn = fn + slashcutter(id,"/",3,2) - fn = fn + ".txt" - return fn + # Determine name + def cachefilename(id): + fn = gettempdir() + "/scyther/" + fn = fn + slashcutter(id,"/",3,2) + fn = fn + ".txt" + return fn - # Ensure directory - def ensureDirectory (path): - if not os.path.exists(path): - os.mkdir(path) + # Ensure directory + def ensureDirectory (path): + if not os.path.exists(path): + os.mkdir(path) - # Ensure directories for a file - def ensureDirectories (filename): - for i in range(1,len(filename)): - if filename[i] == '/': - np = i+1 - ensureDirectory(filename[:np]) + # Ensure directories for a file + def ensureDirectories (filename): + for i in range(1,len(filename)): + if filename[i] == '/': + np = i+1 + ensureDirectory(filename[:np]) - def compute_and_cache(cachefile): - # Hmm, we need to compute this result - # Compute duration (in seconds) - h = NamedTemporaryFile() - h.write(inputstring) - h.flush() - starttime = time.time() - (status, scout) = scythercall (argumentstring, h.name) - duration = time.time() - starttime - h.close() + def compute_and_cache(cachefile): + # Hmm, we need to compute this result + # Compute duration (in seconds) + h = NamedTemporaryFile() + h.write(inputstring) + h.flush() + starttime = time.time() + (status, scout) = scythercall (argumentstring, h.name) + duration = time.time() - starttime + h.close() - # Only cache if it took some time - if duration >= CacheTimer: - # Write cache file even if it's wrong - ensureDirectories(cachefile) - f = open(cachefile,'w') - f.write(scout) - f.close() + # Only cache if it took some time + if duration >= CacheTimer: + # Write cache file even if it's wrong + ensureDirectories(cachefile) + f = open(cachefile,'w') + f.write(scout) + f.close() - return (status,scout) + return (status,scout) - def retrieve_from_cache(file): - f = open(file,'r') - res = f.read() - f.close() - # TODO technically, we should store the status in the - # cache file as well. For now, we just return 0 status. - return (0,res) + def retrieve_from_cache(file): + f = open(file,'r') + res = f.read() + f.close() + # TODO technically, we should store the status in the + # cache file as well. For now, we just return 0 status. + #print "Retrieved cached version for [%s]." % argumentstring + return (0,res) - # Determine the unique filename for this test - cachefile = cachefilename(cacheid()) - if os.path.exists(cachefile) and RetrieveFromCache: - return retrieve_from_cache(cachefile) - else: - return compute_and_cache(cachefile) + # Determine the unique filename for this test + cachefile = cachefilename(cacheid()) + if os.path.exists(cachefile) and RetrieveFromCache: + return retrieve_from_cache(cachefile) + else: + return compute_and_cache(cachefile) #---------------------------------------------------------------------------- # Standalone usage #---------------------------------------------------------------------------- def main(): - print "This module has currently no standalone functionality." + print "This module has currently no standalone functionality." # Only if main stuff if __name__ == '__main__': - main() + main() diff --git a/test/scythertest.py b/test/scythertest.py index 7d6e45b..7d1215d 100755 --- a/test/scythertest.py +++ b/test/scythertest.py @@ -117,9 +117,7 @@ def default_arguments(plist,match,bounds): args += " --plain" - extra = get_extra_parameters() - if extra != "": - args = extra + " " + args + args = get_extra_parameters() + " " + args return args # Yield test results