diff --git a/gui/Gui/Mainwindow.py b/gui/Gui/Mainwindow.py index 72da3b2..7171ac2 100644 --- a/gui/Gui/Mainwindow.py +++ b/gui/Gui/Mainwindow.py @@ -5,17 +5,13 @@ """ Import externals """ import wx import os.path -import sys -import wx.lib.mixins.listctrl as listmix #--------------------------------------------------------------------------- """ Import scyther-gui components """ -import Preference -import Attackwindow +import Settingswindow import Scytherthread import Icon -import Scyther.Claim as Claim #--------------------------------------------------------------------------- @@ -102,7 +98,7 @@ class MainWindow(wx.Frame): os.chdir(self.dirname) textfile.close() self.top.AddPage(self.control,"Protocol description") - self.settings = SettingsWindow(self.top,self) + self.settings = Settingswindow.SettingsWindow(self.top,self) self.top.AddPage(self.settings,"Verification parameters") #sizer.Add(self.top,1,wx.EXPAND,1) @@ -232,101 +228,3 @@ class MainWindow(wx.Frame): #--------------------------------------------------------------------------- -class SettingsWindow(wx.Panel): - - def __init__(self,parent,daddy): - wx.Panel.__init__(self,parent,-1) - - self.win = daddy - - # Bound on the number of runs - self.maxruns = int(Preference.get('maxruns','5')) - r1 = wx.StaticText(self,-1,"Maximum number of runs (0 disables bound)") - l1 = wx.SpinCtrl(self, -1, "",style=wx.RIGHT) - l1.SetRange(0,100) - l1.SetValue(self.maxruns) - self.Bind(wx.EVT_SPINCTRL,self.EvtRuns,l1) - - # Matchin options - self.match = int(Preference.get('match','0')) - claimoptions = ['typed matching','find basic type flaws','find all type flaws'] - r2 = wx.StaticText(self,-1,"Matching type") - l2 = self.ch = wx.Choice(self,-1,choices=claimoptions) - l2.SetSelection(self.match) - self.Bind(wx.EVT_CHOICE,self.EvtMatch,l2) - - ### MISC expert stuff - - # Bound on the number of classes/attacks - self.maxattacks = int(Preference.get('maxattacks','100')) - stname = Claim.stateDescription(True,2,False) - atname = Claim.stateDescription(False,2,False) - txt = "%s/%s" % (stname,atname) - r9 = wx.StaticText(self,-1,"Maximum number of %s for all claims combined (0 disables maximum)" % txt) - l9 = wx.SpinCtrl(self, -1, "",style=wx.RIGHT) - l9.SetRange(0,100) - l9.SetValue(self.maxattacks) - self.Bind(wx.EVT_SPINCTRL,self.EvtMaxAttacks,l9) - - self.misc = Preference.get('scytheroptions','') - r10 = wx.StaticText(self,-1,"Additional parameters for the Scyther tool") - l10 = wx.TextCtrl(self,-1,self.misc,size=(150,-1)) - self.Bind(wx.EVT_TEXT,self.EvtMisc,l10) - - # Combine - space = 10 - sizer = wx.FlexGridSizer(cols=3, hgap=space,vgap=space) - sizer.AddMany([ l1,r1, (0,0), - l2,r2, (0,0), - l9,r9, (0,0), - l10,r10, (0,0), - ]) - self.SetSizer(sizer) - self.SetAutoLayout(True) - - def EvtMatch(self,evt): - self.match = evt.GetInt() - - def EvtRuns(self,evt): - self.maxruns = evt.GetInt() - - def EvtMaxAttacks(self,evt): - self.maxattacks = evt.GetInt() - - def EvtMisc(self,evt): - self.misc = evt.GetString() - - def ScytherArguments(self,mode): - """ Note: constructed strings should have a space at the end to - correctly separate the options. - """ - - tstr = "" - - # Number of runs - tstr += "--max-runs=%s " % (str(self.maxruns)) - # Matching type - tstr += "--match=%s " % (str(self.match)) - # Max attacks/classes - if self.maxattacks != 0: - tstr += "--max-attacks=%s " % (str(self.maxattacks)) - - # Verification type - if mode == "check": - tstr += "--check " - elif mode == "autoverify": - tstr += "--auto-claims " - elif mode == "statespace": - tstr += "--state-space " - - # Anything else? - if self.misc != "": - tstr += " " + self.misc + " " - - return tstr - -#--------------------------------------------------------------------------- - - - - diff --git a/gui/Gui/Scytherthread.py b/gui/Gui/Scytherthread.py index fe426e7..25be15b 100644 --- a/gui/Gui/Scytherthread.py +++ b/gui/Gui/Scytherthread.py @@ -110,64 +110,48 @@ class AttackThread(threading.Thread): wx.CallAfter(self.callbackdone) def writeGraph(self,txt,fp): + + EDGE = 0 + NODE = 1 + DEFAULT = 2 + ALL = 3 def graphLine(txt): fp.write("\t%s;\n" % (txt)) - def setAttr(EdgeNodeDefAll,atxt): - if EdgeNodeDefAll == 3: - setAttr(0,atxt) - setAttr(1,atxt) - setAttr(2,atxt) + def setAttr(atxt,EdgeNodeDefAll=ALL): + if EdgeNodeDefAll == ALL: + setAttr(atxt,EDGE) + setAttr(atxt,NODE) + setAttr(atxt,DEFAULT) else: - if EdgeNodeDefAll == 0: + if EdgeNodeDefAll == EDGE: edge = "edge" - elif EdgeNodeDefAll == 1: + elif EdgeNodeDefAll == NODE: edge = "node" else: graphLine("%s" % atxt) return graphLine("%s [%s]" % (edge,atxt)) - def oldFontDefs(txt): - """ - Old hack. Remove after windows recompile TODO - """ - if txt.startswith("\tfontname"): - return True - if txt.startswith("\tfontsize"): - return True - if txt.startswith("\tnode [fontname"): - return True - if txt.startswith("\tnode [fontsize"): - return True - if txt.startswith("\tedge [fontname"): - return True - if txt.startswith("\tedge [fontsize"): - return True - return False - + # write all graph lines but add layout modifiers for l in txt.splitlines(): - # hack to get rid of font defs - # TODO remove this once new windows version is compiled - if not oldFontDefs(l): - fp.write(l) - if l.startswith("digraph"): - # Write additional stuff for this graph - graphLine("dpi=96") - graphLine("rankdir=TB") - graphLine("nodesep=0.1") - graphLine("ranksep=0.001") - graphLine("mindist=0.1") - if sys.platform.startswith("lin"): - setAttr(3,"fontname=\"Sans\"") - else: - setAttr(3,"fontname=\"Arial\"") - setAttr(3,"fontsize=10") - setAttr(1,"height=\"0.01\"") - setAttr(1,"width=\"0.01\"") - setAttr(1,"margin=\"0.08,0.03\"") - #setAttr(0,"decorate=true") + fp.write(l) + if l.startswith("digraph"): + # Write additional stuff for this graph + graphLine("dpi=96") + graphLine("rankdir=TB") + graphLine("nodesep=0.1") + graphLine("ranksep=0.001") + graphLine("mindist=0.1") + if sys.platform.startswith("lin"): + setAttr("fontname=\"Helvetica\"") + else: + setAttr("fontname=\"Arial\"") + setAttr("fontsize=12") + setAttr("height=\"0.01\"",NODE) + setAttr("width=\"0.01\"",NODE) + setAttr("margin=\"0.08,0.03\"",NODE) def makeImage(self,attack): """ create image for this particular attack """ diff --git a/gui/Gui/Settingswindow.py b/gui/Gui/Settingswindow.py new file mode 100644 index 0000000..15d47bd --- /dev/null +++ b/gui/Gui/Settingswindow.py @@ -0,0 +1,117 @@ +#!/usr/bin/python + +#--------------------------------------------------------------------------- + +""" Import externals """ +import wx + +#--------------------------------------------------------------------------- + +""" Import scyther-gui components """ +import Preference +import Scyther.Claim as Claim + +#--------------------------------------------------------------------------- + +class SettingsWindow(wx.Panel): + + def __init__(self,parent,daddy): + wx.Panel.__init__(self,parent,-1) + + self.win = daddy + space = 10 + grid = wx.GridBagSizer(hgap=space,vgap=space) + ypos = 0 + + # Bound on the number of runs + self.maxruns = int(Preference.get('maxruns','5')) + txt = wx.StaticText(self,-1,"Maximum number of runs (0 disables bound)") + ctrl = wx.SpinCtrl(self, -1, "",style=wx.RIGHT) + ctrl.SetRange(0,100) + ctrl.SetValue(self.maxruns) + self.Bind(wx.EVT_SPINCTRL,self.EvtRuns,ctrl) + grid.Add(ctrl,(ypos,0)) + grid.Add(txt,(ypos,1)) + ypos += 1 + + # Matchin options + self.match = int(Preference.get('match','0')) + claimoptions = ['typed matching','find basic type flaws','find all type flaws'] + r2 = wx.StaticText(self,-1,"Matching type") + l2 = self.ch = wx.Choice(self,-1,choices=claimoptions) + l2.SetSelection(self.match) + self.Bind(wx.EVT_CHOICE,self.EvtMatch,l2) + grid.Add(l2,(ypos,0)) + grid.Add(r2,(ypos,1)) + ypos += 1 + + ### MISC expert stuff + + # Bound on the number of classes/attacks + self.maxattacks = int(Preference.get('maxattacks','100')) + stname = Claim.stateDescription(True,2,False) + atname = Claim.stateDescription(False,2,False) + txt = "%s/%s" % (stname,atname) + r9 = wx.StaticText(self,-1,"Maximum number of %s for all claims combined (0 disables maximum)" % txt) + l9 = wx.SpinCtrl(self, -1, "",style=wx.RIGHT) + l9.SetRange(0,100) + l9.SetValue(self.maxattacks) + self.Bind(wx.EVT_SPINCTRL,self.EvtMaxAttacks,l9) + grid.Add(l9,(ypos,0)) + grid.Add(r9,(ypos,1)) + ypos += 1 + + self.misc = Preference.get('scytheroptions','') + r10 = wx.StaticText(self,-1,"Additional parameters for the Scyther tool") + l10 = wx.TextCtrl(self,-1,self.misc,size=(150,-1)) + self.Bind(wx.EVT_TEXT,self.EvtMisc,l10) + grid.Add(l10,(ypos,0)) + grid.Add(r10,(ypos,1)) + ypos += 1 + + # Combine + self.SetSizer(grid) + self.SetAutoLayout(True) + + def EvtMatch(self,evt): + self.match = evt.GetInt() + + def EvtRuns(self,evt): + self.maxruns = evt.GetInt() + + def EvtMaxAttacks(self,evt): + self.maxattacks = evt.GetInt() + + def EvtMisc(self,evt): + self.misc = evt.GetString() + + def ScytherArguments(self,mode): + """ Note: constructed strings should have a space at the end to + correctly separate the options. + """ + + tstr = "" + + # Number of runs + tstr += "--max-runs=%s " % (str(self.maxruns)) + # Matching type + tstr += "--match=%s " % (str(self.match)) + # Max attacks/classes + if self.maxattacks != 0: + tstr += "--max-attacks=%s " % (str(self.maxattacks)) + + # Verification type + if mode == "check": + tstr += "--check " + elif mode == "autoverify": + tstr += "--auto-claims " + elif mode == "statespace": + tstr += "--state-space " + + # Anything else? + if self.misc != "": + tstr += " " + self.misc + " " + + return tstr + +#---------------------------------------------------------------------------