diff --git a/test/compareheuristics.py b/test/compareheuristics.py index 9236983..16e0025 100755 --- a/test/compareheuristics.py +++ b/test/compareheuristics.py @@ -9,6 +9,18 @@ import scythertest # Parse def parse(scout): + """Parse Scyther output for heuristics tests + + in: + A single Scyther output string (including newlines) + out: + ra: number of failed claims + rb: number of bounded proofs of claims + rc: number of complete proofs of claims + nc: number of processed claims (should be the sum of the previous) + st: number of states traversed + """ + ra = 0 rb = 0 rp = 0 @@ -32,8 +44,21 @@ def parse(scout): return (ra,rb,rp,nc,st) -# Test with a goal selector def test_goal_selector(goalselector, options): + """Test with a given goal selector + + in: + goalselector: as in Scyther docs. + options: options record (formatted as in optparse module) + out: + (attacks,bounds,proofs,claims,np,states) + attacks: number of failed claims + bounds: number of bounded proofs + proofs: number of complete proofs + np: number of protocols tested + states: total number of states explored. + """ + import protocollist scythertest.set_extra_parameters("--goal-select=" + str(goalselector)) @@ -61,12 +86,33 @@ def test_goal_selector(goalselector, options): # Max class maxor: + """Class for a dynamic maximum determination and corresponding formatting + """ + def __init__(self,dir=0,mymin=99999999, mymax=-99999999): + """Init + + in: + dir: bit 0 is set : notify of increase + bit 1 is set : notify of decrease + mymin: initial minimum + mymax: initial maximum + """ + self.dir = dir self.min = mymin self.max = mymax def reg(self,data): + """Store a new data element + + in: + element to be stored + out: + formatted element, plus increase/decrease + notifications according to initial settings. + """ + res = "" if self.min >= data: self.min = data diff --git a/test/multiprotocoltest.py b/test/multiprotocoltest.py index f0ab3a4..cc29a8b 100755 --- a/test/multiprotocoltest.py +++ b/test/multiprotocoltest.py @@ -45,22 +45,35 @@ safetxt = " " * 20 # LIBS # *********************** -# GetKeys -# -# Given a mapping f and a value x, returns a list of keys -# k for which f(k) = x def GetKeys (f, x): + """Get the list of keys of a mapping to some value + + in: + f: a mapping + x: an element of the range of f + out: + A list, with elements from the domain of f, such that + for each y in the list we have f(y)=x + """ + res = [] for k in f.keys(): if f[k] == x: res.append(k) return res -# GetListKeys -# -# Given a mapping f and a list l, returns a list of keys -# k for which f(k) = x, x in l + def GetListKeys (f, l): + """Get a list of keys for a list of elements (generalized GetKeys) + + in: + f: a mapping + l: a list of elements from the range of f + out: + A list, with elements from the domain of f, such that + for each y in the list we have f(y) in l. + """ + res = [] for x in l: for y in GetKeys (f, x): @@ -68,17 +81,32 @@ def GetListKeys (f, l): res.append(y) return res -# CommandLine -# -# Yield the commandline to test, given a list of protocols + def CommandLine (plist): + """Yield the commandline to test + + in: + a list of protocol file names + out: + a command line string + """ + linelist = " ".join(plist) return "cat " + IncludeProtocols + " " + linelist + " | " + CommandPrefix -# PrintProtStatus -# -# pretty-print the status of a protocol + def PrintProtStatus (file, prname): + """Pretty-print the protocol status + + in: + file: a file pointer to write to (e.g. stdout) + prname: a protocol name id + global: + ProtocolStatusMap: the pre-determined status of the protocols + out: + output is written to file + """ + file.write (prname + ": ") if ProtocolToStatusMap[prname] == 0: file.write ("All-Flawed") @@ -87,12 +115,23 @@ def PrintProtStatus (file, prname): else: file.write ("Mixed") -# ScytherEval -# -# Take the list of protocols in plist, and give them to Scyther. -# Returns a dictionary of claim -> bool; where 1 means that it is -# correct, and 0 means that it is false (i.e. there exists an attack) + def ScytherEval (plist): + """Evaluate a protocol file list using Scyther + + in: + A list of protocol file names + global: + options: settings for scyther + ArgumentsList: already reported arguments list for + scyther. + out: + A dictionary of claim->bool, where true means correct + (either complete or bounded) and false means attack. + If the arguments list that is constructed was not + reported before, it is now (to stdout). + """ + global options # Flush before trying (possibly fatal) external commands @@ -107,10 +146,21 @@ def ScytherEval (plist): return scythertest.default_parsed(plist, int(options.match), int(options.bounds)) -# ScytherEval1 -# -# The above, but do the preprocessing for a single protocol + def ScytherEval1 (protocol): + """Evaluate a single protocol and store the results for later usage + + in: + a single protocol file name + global: + ClaimToResultMap + ProtocolToFileMap + ProtocolToStatusMap + out: + Globals have been updated to reflect the computed + protocol status + """ + results = ScytherEval ([protocol]) # Add the claim to the list of ClaimToResultMap