- Improvements to the testing suite.

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]
+                st += localstates
-                if tag == 'Fail':
+
+            # 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):
+    problems = {}
-            (ra,rb,rp,nc,np,st,timeouts) = test_goal_selector(g, options,
+    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__':

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
+    ScytherProgram = newprg
-	if not os.path.exists(ScytherProgram):
+    if not os.path.exists(ScytherProgram):
-		print "Cannot find any file at", ScytherProgram, " and it cannot be used as a Scyther executable."
+        print "Cannot find any file at", ScytherProgram, " and it cannot be used as a Scyther executable."
-		sys.exit()
+        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
+    clstring = ScytherProgram + " " + argumentstring + " " + inputfile
-	(status,scout) = commands.getstatusoutput(clstring)
+    (status,scout) = commands.getstatusoutput(clstring)
-	return (status,scout)
+    return (status,scout)
 
 #----------------------------------------------------------------------------
 # Cached evaluation
 #----------------------------------------------------------------------------
 
-#	cached results
+#    cached results
-#	input:	a large string (consisting of read input files)
+#    input:    a large string (consisting of read input files)
-#	argstring:	a smaller string
+#    argstring:    a smaller string
 def evaluate (argumentstring, inputstring):
 
-	def cacheid():
+    def cacheid():
-		m = md5.new()
+        m = md5.new()
-	
+    
-		# Determine scyther version
+        # Determine scyther version
-		(status, scout) = scythercall ("--version", "")
+        (status, scout) = scythercall ("--version", "")
-		if status == 1 or status < 0:
+        if status == 1 or status < 0:
-			# some problem
+            # some problem
-			print "Problem with determining scyther version!"
+            print "Problem with determining scyther version!"
-		 	os.exit()
+            os.exit()
-		# Add version to hash
+        # Add version to hash
-		m.update (scout)
+        m.update (scout)
 
-		# Add inputfile to hash
+        # Add inputfile to hash
-		m.update (inputstring)
+        m.update (inputstring)
 
-		# Add arguments to hash
+        # Add arguments to hash
-		m.update (argumentstring)
+        m.update (argumentstring)
 
-		# Return a readable ID (good for a filename)
+        # Return a readable ID (good for a filename)
-		return m.hexdigest()
+        return m.hexdigest()
 
-	# slashcutter
+    # slashcutter
-	# Takes 'str': cuts of the first 'depth' strings of length
+    # Takes 'str': cuts of the first 'depth' strings of length
-	# 'width' and puts 'substr' in between
+    # 'width' and puts 'substr' in between
-	def slashcutter(str,substr,width,depth):
+    def slashcutter(str,substr,width,depth):
-		res = ""
+        res = ""
-		while len(str)>width and depth>0:
+        while len(str)>width and depth>0:
-			res = res + str[0:width] + substr
+            res = res + str[0:width] + substr
-			str = str[width:]
+            str = str[width:]
-			depth = depth-1
+            depth = depth-1
-		return res + str
+        return res + str
 
-	# Determine name
+    # Determine name
-	def cachefilename(id):
+    def cachefilename(id):
-		fn = gettempdir() + "/scyther/"
+        fn = gettempdir() + "/scyther/"
-		fn = fn + slashcutter(id,"/",3,2)
+        fn = fn + slashcutter(id,"/",3,2)
-		fn = fn + ".txt"
+        fn = fn + ".txt"
-		return fn
+        return fn
 
-	# Ensure directory
+    # Ensure directory
-	def ensureDirectory (path):
+    def ensureDirectory (path):
-		if not os.path.exists(path):
+        if not os.path.exists(path):
-			os.mkdir(path)
+            os.mkdir(path)
 
-	# Ensure directories for a file
+    # Ensure directories for a file
-	def ensureDirectories (filename):
+    def ensureDirectories (filename):
-		for i in range(1,len(filename)):
+        for i in range(1,len(filename)):
-			if filename[i] == '/':
+            if filename[i] == '/':
-				np = i+1
+                np = i+1
-				ensureDirectory(filename[:np])
+                ensureDirectory(filename[:np])
 
-	def compute_and_cache(cachefile):
+    def compute_and_cache(cachefile):
-		# Hmm, we need to compute this result
+        # Hmm, we need to compute this result
-		# Compute duration (in seconds)
+        # Compute duration (in seconds)
-		h = NamedTemporaryFile()
+        h = NamedTemporaryFile()
-		h.write(inputstring)
+        h.write(inputstring)
-		h.flush()
+        h.flush()
-		starttime = time.time()
+        starttime = time.time()
-		(status, scout) = scythercall (argumentstring, h.name)
+        (status, scout) = scythercall (argumentstring, h.name)
-		duration = time.time() - starttime
+        duration = time.time() - starttime
-		h.close()
+        h.close()
 
-		# Only cache if it took some time
+        # Only cache if it took some time
-		if duration >= CacheTimer:
+        if duration >= CacheTimer:
-			# Write cache file even if it's wrong
+            # Write cache file even if it's wrong
-			ensureDirectories(cachefile)
+            ensureDirectories(cachefile)
-			f = open(cachefile,'w')
+            f = open(cachefile,'w')
-			f.write(scout)
+            f.write(scout)
-			f.close()
+            f.close()
 
-		return (status,scout)
+        return (status,scout)
 
-	def retrieve_from_cache(file):
+    def retrieve_from_cache(file):
-		f = open(file,'r')
+        f = open(file,'r')
-		res = f.read()
+        res = f.read()
-		f.close()
+        f.close()
-		# TODO technically, we should store the status in the
+        # TODO technically, we should store the status in the
-		# cache file as well. For now, we just return 0 status.
+        # cache file as well. For now, we just return 0 status.
-		return (0,res)
+        #print "Retrieved cached version for [%s]." % argumentstring
+        return (0,res)
 
-	# Determine the unique filename for this test
+    # Determine the unique filename for this test
-	cachefile = cachefilename(cacheid())
+    cachefile = cachefilename(cacheid())
-	if os.path.exists(cachefile) and RetrieveFromCache:
+    if os.path.exists(cachefile) and RetrieveFromCache:
-		return retrieve_from_cache(cachefile)
+        return retrieve_from_cache(cachefile)
-	else:
+    else:
-		return compute_and_cache(cachefile)
+        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()

test/scythertest.py

@@ -117,9 +117,7 @@ def default_arguments(plist,match,bounds):
 
     args += " --plain"
 
-    extra = get_extra_parameters()
+    args = get_extra_parameters() + " " + args
-    if extra != "":
-        args = extra + " " + args
     return args
 
 # Yield test results