- Significantly improved result windows.

gui/Gui/Mainwindow.py

@@ -108,14 +108,14 @@ class MainWindow(wx.Frame):
     def SetupToolBar(self):
 
         tb = self.CreateToolBar(wx.TB_HORIZONTAL
-                | wx.NO_BORDER
+                #| wx.NO_BORDER
-                | wx.TB_FLAT
+                #| wx.TB_FLAT
                 | wx.TB_TEXT
+                | wx.TB_NOICONS
                 )
 
         #print "Default toolbar tool size: %s\n" % tb.GetToolBitmapSize()
 
-
         def getBmp(name):
             bmp = wx.Bitmap(os.path.join("Images","%s.png" % name),wx.BITMAP_TYPE_PNG)
             if not bmp.Ok():
@@ -127,9 +127,10 @@ class MainWindow(wx.Frame):
         bmpcharacterize = getBmp("characterize-button")
 
         # add the actual tools
-        tb.AddSimpleTool(ID_VERIFY, bmpverify,"Verify","Verify claims")
+        tb.AddSimpleTool(ID_VERIFY, bmpverify,shortHelpString="Verify")
         self.Bind(wx.EVT_TOOL, self.OnVerify, id=ID_VERIFY)
-        tb.AddSimpleTool(ID_STATESPACE, bmpcharacterize,"Statespace","Generate statespace for all roles")
+        tb.AddSimpleTool(ID_STATESPACE,
+                bmpcharacterize,shortHelpString="Statespace")
         self.Bind(wx.EVT_TOOL, self.OnStatespace, id=ID_STATESPACE)
 
         # tb.AddSeparator()

gui/Gui/Scytherthread.py

@@ -266,22 +266,21 @@ class ResultWindow(wx.Frame):
 
         def titlebar(x,title,width=1):
             txt = wx.StaticText(self,-1,title)
-            font = wx.Font(14,wx.NORMAL,wx.NORMAL,wx.NORMAL)
+            font = wx.Font(14,wx.NORMAL,wx.NORMAL,wx.BOLD)
             txt.SetFont(font)
             grid.Add(txt,(0,x),(1,width),wx.ALL,10)
 
-        titlebar(0,"Claim",5)
+        titlebar(0,"Claim",4)
-        if len(claims) > 0:
+        titlebar(4,"Status",2)
-            sn = claims[0].stateName(2)
-            resulttxt = sn[0].upper() + sn[1:]
-        else:
-            resulttxt = "Results"
-        titlebar(5,resulttxt,2)
 
         self.lastprot = None
         self.lastrole = None
+        views = 0
         for index in range(0,len(claims)):
-            self.BuildClaim(grid,claims[index],index+1)
+            views += self.BuildClaim(grid,claims[index],index+1)
+
+        if views > 0:
+            titlebar(6,"View",1)
 
         self.SetSizer(grid)
         self.Fit()
@@ -291,17 +290,8 @@ class ResultWindow(wx.Frame):
         def addtxt(txt,column):
             grid.Add(wx.StaticText(self,-1,txt),(ypos,column),(1,1),wx.ALIGN_CENTER_VERTICAL|wx.ALL,10)
 
-        # button for ok/fail
+        n = len(cl.attacks)
-        tsize = (16,16)
+        xpos = 0
-        if cl.okay:
-            bmp = wx.ArtProvider_GetBitmap(wx.ART_TICK_MARK,wx.ART_CMN_DIALOG,tsize)
-        else:
-            bmp = wx.ArtProvider_GetBitmap(wx.ART_CROSS_MARK,wx.ART_CMN_DIALOG,tsize)
-        if not bmp.Ok():
-            bmp = wx.EmptyBitmap(tsize)
-        bmpfield = wx.StaticBitmap(self,-1,bmp)
-
-        grid.Add(bmpfield,(ypos,0),(1,1),wx.ALIGN_CENTER_VERTICAL|wx.ALL,10)
 
         # protocol, role, label
         prot = str(cl.protocol)
@@ -314,43 +304,84 @@ class ResultWindow(wx.Frame):
             self.lastrole = role
             showPR = True
         if showPR:
-            addtxt(prot,1)
+            addtxt(prot,xpos)
-            addtxt(role,2)
+            addtxt(role,xpos+1)
+        xpos += 2
         
-        addtxt(str(cl.shortlabel),3)
+        addtxt(str(cl.id),xpos)
+        xpos += 1
 
+        # claim parameters
         claimdetails = str(cl.claimtype)
         if cl.parameter:
             claimdetails += " %s" % (cl.parameter)
-        addtxt(claimdetails + "  ",4)
+        addtxt(claimdetails + "  ",xpos)
+        xpos += 1
 
-        # add view button (if needed)
+        # button for ok/fail
-        n = len(cl.attacks)
+        if None:
+            # old style buttons (but they looked ugly on windows)
+            tsize = (16,16)
+            if cl.okay:
+                bmp = wx.ArtProvider_GetBitmap(wx.ART_TICK_MARK,wx.ART_CMN_DIALOG,tsize)
+            else:
+                bmp = wx.ArtProvider_GetBitmap(wx.ART_CROSS_MARK,wx.ART_CMN_DIALOG,tsize)
+            if not bmp.Ok():
+                bmp = wx.EmptyBitmap(tsize)
+            bmpfield = wx.StaticBitmap(self,-1,bmp)
+            grid.Add(bmpfield,(ypos,xpos),(1,1),wx.ALIGN_CENTER_VERTICAL|wx.ALL,10)
+        else:
+            # new style text control Ok/Fail
+            def makeTC(txt,colour):
+                txt = wx.StaticText(self,-1,txt)
+                font = wx.Font(11,wx.NORMAL,wx.NORMAL,wx.BOLD)
+                txt.SetFont(font)
+                txt.SetForegroundColour(colour)
+                grid.Add(txt,(ypos,xpos),(1,1),wx.ALL,10)
+            if cl.okay:
+                makeTC("Ok","forest green")
+            else:
+                makeTC("Fail","red")
+        xpos += 1
+
+        # remark something about completeness
+        remark = ""
+        atxt = cl.stateName(n)
+        if not cl.complete:
+            if n == 0:
+                # no attacks, no states within bounds
+                remark = "No %s within bounds" % (atxt)
+            else:
+                # some attacks/states within bounds
+                remark = "At least %i %s" % (n,atxt)
+        else:
+            if n == 0:
+                # no attacks, no states
+                remark = "No %s" % (atxt)
+            else:
+                # there exist n states/attacks (within any number of runs)
+                remark = "Exactly %i %s" % (n,atxt)
+        addtxt(remark,xpos)
+        xpos += 1
+                
+        # add view button (enabled later if needed)
+        if n > 0:
             cl.button = wx.Button(self,-1,"%i %s" % (n,cl.stateName(n)))
             cl.button.claim = cl
-        grid.Add(cl.button,(ypos,5),(1,1),wx.ALIGN_CENTER_VERTICAL|wx.ALL,1)
+            grid.Add(cl.button,(ypos,xpos),(1,1),wx.ALIGN_CENTER_VERTICAL|wx.ALL,5)
             cl.button.Disable()
             if n > 0:
                 # Aha, something to show
                 self.Bind(wx.EVT_BUTTON, self.onViewButton,cl.button)
+        else:
+            cl.button = None
+        xpos += 1
 
-        # remark something about completeness
+        # Return 1 if there is a view possible
-        remark = ""
+        if n > 0:
-        if not cl.complete:
+            return 1
-            if n == 0:
-                # no attacks, no states within bounds
-                remark = "within bounds"
         else:
-                # some attacks/states within bounds
+            return 0
-                remark = "at least, maybe more"
-        else:
-            if n == 0:
-                # no attacks, no states
-                remark = "none"
-            else:
-                # there exist n states/attacks (within any number of runs)
-                remark = "exactly"
-        addtxt(" (%s)" % remark,6)
 
 
 #---------------------------------------------------------------------------