diff --git a/gui/Gui/Scytherthread.py b/gui/Gui/Scytherthread.py index 14ea177..8555a57 100644 --- a/gui/Gui/Scytherthread.py +++ b/gui/Gui/Scytherthread.py @@ -370,6 +370,7 @@ class ResultWindow(wx.Frame): addtxt(role,xpos+1) xpos += 2 + # claim id addtxt(str(cl.id),xpos) xpos += 1 @@ -406,38 +407,15 @@ class ResultWindow(wx.Frame): makeTC("Fail","red") xpos += 1 - # remark something about completeness - remark = "" - atxt = cl.stateName(n) - vstatus = "" - 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) - if not cl.state: - vstatus = "Falsified" - else: - if n == 0: - # no attacks, no states - remark = "No %s" % (atxt) - if cl.state: - vstatus = "Falsified" - else: - vstatus = "Verified" - else: - # there exist n states/attacks (within any number of runs) - remark = "Exactly %i %s" % (n,atxt) - if cl.state: - vstatus = "Verified" - else: - vstatus = "Falsified" + # verified? + vt = cl.getVerified() + if vt: + addtxt(vt,xpos) + xpos += 1 - addtxt(vstatus,xpos) - addtxt(remark,xpos+1) - xpos += 2 + # remark something + addtxt(cl.getComment(),xpos) + xpos += 1 # add view button (enabled later if needed) if n > 0: diff --git a/gui/Scyther/Claim.py b/gui/Scyther/Claim.py index 04c67e2..2d9c031 100644 --- a/gui/Scyther/Claim.py +++ b/gui/Scyther/Claim.py @@ -71,17 +71,73 @@ class Claim(object): def stateName(self,count=1,caps=False): return stateDescription(self.state,count,caps) + def getComment(self): + """ + returns a sentence describing the results for this claim + """ + n = len(self.attacks) + atxt = self.stateName(n) + remark = "" + if not self.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) + return remark + "." + + def getVerified(self): + """ + returns an element of [None,'Verified','Falsified'] + """ + n = len(self.attacks) + if self.state: + # this is about reachability + if n > 0: + return "Verified" + else: + if self.complete: + return "Falsified" + else: + # this is about attacks + if n > 0: + return "Falsified" + else: + if self.complete: + return "Verified" + return None + def __str__(self): + """ + Resulting string + """ s = "claim id [%s]" % (self.id) s+= " " + str(self.claimtype) if self.parameter: s+= " " + str(self.parameter) # determine status - s+= " : %i " % (self.failed) + s+= " : " + if self.okay: + s+= "[Ok] " + else: + s+= "[Fail] " + + s+= " %i " % (self.failed) s+= self.stateName(self.failed) - if self.complete: - s+= " (complete)" + + vt = self.getVerified() + if vt: + s+= " (%s)" % vt + s+= " [%s]" % self.getComment() return s