- We have output again (if you wait for it, that is...)

gui/Attackwindow.py

@@ -14,13 +14,13 @@ import Icon
 #---------------------------------------------------------------------------
 
 class AttackDisplay(wx.ScrolledWindow):
-    def __init__(self, daddy, parent, claim,attackid):
+    def __init__(self, daddy, parent, claim,attack):
 
         self.win = daddy
 
         wx.ScrolledWindow.__init__(self,parent,id=-1)
         # Wait for the attack to be computed
-        while attackid >= len(claim.attacks):
+        while not attack.pngfile:
             time.sleep(1)
 
         self.Bind(wx.EVT_SIZE, self.OnSize)
@@ -31,7 +31,7 @@ class AttackDisplay(wx.ScrolledWindow):
         self.hbox.Add(self.box,1,wx.ALIGN_CENTER)
         self.SetSizer(self.hbox)
 
-        filename = claim.attacks[attackid].GetImage()
+        filename = attack.pngfile
         self.original = wx.Image(filename,wx.BITMAP_TYPE_PNG)
 
 
@@ -93,29 +93,24 @@ class AttackWindow(wx.Frame):
 
     def SetTitle(self):
 
-        if self.claim.attackcount == 1:
+        tstr = self.claim.stateName(len(self.claim.attacks))
-            tstr = "Attack"
+        tstr += " for claim %s" % self.claim.id
-        else:
-            tstr = "Attacks"
-
-        tstr += " for claim %s" % str(self.claim)
         super(AttackWindow, self).SetTitle(tstr)
 
-
     def CreateInteriorWindowComponents(self):
         ''' Create "interior" window components. In this case it is the
         attack picture. '''
 
         self.displays=[]
-        if self.claim.attackcount <= 1:
+        if self.claim.failed <= 1:
             # Just a single window
             self.tabs = None
-            self.displays.append(AttackDisplay(self,self,self.claim,0))
+            self.displays.append(AttackDisplay(self,self,self.claim,self.claim.attacks[0]))
         else:
             # Multiple tabs
             self.tabs = wx.Notebook(self,-1)
-            for i in range(0,self.claim.attackcount):
+            for i in range(0,len(self.claim.attacks)):
-                disp =  AttackDisplay(self,self.tabs,self.claim,i)
+                disp = AttackDisplay(self,self.tabs,self.claim.attacks[i])
                 classname = "Class %i" % ((i+1))
                 self.tabs.AddPage(disp, classname)
                 self.displays.append(disp)

gui/Claim.py

@@ -6,8 +6,10 @@ import Term
 
 class Claim(object):
     def __init__(self):
+        self.id = None          # a unique id string, like 'ns3,r,r3'
         self.claimtype = None
         self.label = None
+        self.shortlabel = None
         self.protocol = None
         self.role = None
         self.parameter = None
@@ -18,12 +20,25 @@ class Claim(object):
         self.timebound = False
         self.attacks = []
         self.state = False      # if true, it is a state, not an attack
+        self.okay = None        # true if good, false if bad
 
         # derived info
         self.foundstates = False
         self.foundproof = False
 
     def analyze(self):
+
+        # determine short label
+        # We need the rightmost thingy here
+        label = self.label
+        while isinstance(label,Term.TermTuple):
+            label = label[1]
+        self.shortlabel = label
+
+        # determine id
+        self.id = "%s,%s,%s" % (self.protocol,self.role,self.shortlabel)
+
+        # some additional properties
         if str(self.claimtype) == 'Reachable':
             self.state = True
         if self.failed > 0:
@@ -31,6 +46,14 @@ class Claim(object):
         if self.complete:
             self.foundproof = True
 
+        # status
+        # normally, with attacks, okay means none
+        self.okay = (self.failed == 0)
+        if self.state:
+            # but the logic reverses when it is states and not
+            # attacks...
+            self.okay = (not self.okay)
+
     def stateName(self,count=1):
         if self.state:
             s = "state"
@@ -41,16 +64,7 @@ class Claim(object):
         return s
 
     def __str__(self):
-        s = "claim "
+        s = "claim id [%s]" % (self.id)
-        s+= " " + str(self.protocol)
-        s+= " " + str(self.role)
-
-        # We need the rightmost thingy here
-        label = self.label
-        while isinstance(label,Term.TermTuple):
-            label = label[1]
-
-        s+= " " + str(label)
         s+= " " + str(self.claimtype)
         if self.parameter:
             s+= " " + str(self.parameter)

gui/Mainwindow.py

@@ -345,38 +345,48 @@ class SummaryWindow(wx.ListCtrl, listmix.ListCtrlAutoWidthMixin):
 
     def update(self):
         self.DeleteAllItems()
-        self.claimlist = self.win.claimlist
+        claims = self.win.claims
-        for key in range(0,len(self.claimlist)):
+        for key in range(0,len(claims)):
-            cl = self.claimlist[key]
+            cl = claims[key]
-            index = self.InsertStringItem(sys.maxint,cl.protocol)
+            index = self.InsertStringItem(sys.maxint,str(cl.protocol))
-            self.SetStringItem(index,1,cl.role)
-            self.SetStringItem(index,2,cl.claim)
-            self.SetStringItem(index,3,cl.label)
-            self.SetStringItem(index,4,cl.param)
-            self.SetStringItem(index,5,cl.status)
-            self.SetStringItem(index,6,str(cl.attackcount))
-            self.SetStringItem(index,7,cl.comments)
-            self.SetItemData(index,key)
 
-            if cl.status == "Fail":
+            def addThing(i,x):
-                # Failed :(
+                self.SetStringItem(index,i,str(x))
-                item = self.GetItem(key)
+
-                item.SetTextColour(wx.RED)
+            addThing(1,cl.role)
-                self.SetItem(item)
+            addThing(2,cl.claimtype)
+            addThing(3,cl.shortlabel)
+            addThing(4,cl.parameter)
+            if cl.okay:
+                addThing(5,"Ok")
             else:
-                # Okay! But with bound?
+                addThing(5,"Fail")
-                if cl.comments.find("bounds") == -1:
+            addThing(6,cl.failed)
-                    # No bounds, great :)
+            addThing(7,"Comments")
-                    item = self.GetItem(key)
+
-                    item.SetTextColour(wx.GREEN)
+            self.SetItemData(index,key)
-                    self.SetItem(item)
+            key += 1
+
+            # if cl.okay == "Fail":
+            #     # Failed :(
+            #     item = self.GetItem(key)
+            #     item.SetTextColour(wx.RED)
+            #     self.SetItem(item)
+            # else:
+            #     # Okay! But with bound?
+            #     if cl.comments.find("bounds") == -1:
+            #         # No bounds, great :)
+            #         item = self.GetItem(key)
+            #         item.SetTextColour(wx.GREEN)
+            #         self.SetItem(item)
+            
         #for i in range(0,7):
         #    self.SetColumnWidth(i,wx.LIST_AUTOSIZE)
 
     def OnItemSelected(self, event):
         self.currentItem = event.m_itemIndex
-        cl = self.claimlist[self.currentItem]
+        cl = self.win.claims[self.currentItem]
-        if cl.attackcount > 0:
+        if len(cl.attacks) > 0:
             display = Attackwindow.AttackWindow(cl)
             display.Show(1)
         self.Refresh()

gui/Scytherthread.py

@@ -82,6 +82,7 @@ class ScytherThread(threading.Thread):
         self.summary = str(scyther)
 
         self.win.errors.update(self.summary)
+        self.win.report.update()
 
     def makeImages(self):
         """ create images """