scyther/gui/Claim.py

81 lines
2.0 KiB
Python
Raw Normal View History

2006-08-02 13:59:57 +01:00
#
# Claim
#
import Term
class Claim(object):
def __init__(self):
self.id = None # a unique id string, consisting of 'protocol,label'
2006-08-02 13:59:57 +01:00
self.claimtype = None
self.label = None
self.shortlabel = None
2006-08-02 13:59:57 +01:00
self.protocol = None
self.role = None
self.parameter = None
self.failed = 0
self.count = 0
self.states = 0
self.complete = False
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
2006-08-02 13:59:57 +01:00
# 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" % (self.protocol,self.shortlabel)
# some additional properties
2006-08-02 13:59:57 +01:00
if str(self.claimtype) == 'Reachable':
self.state = True
if self.failed > 0:
self.foundstates = True
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)
2006-08-02 13:59:57 +01:00
def stateName(self,count=1):
if self.state:
s = "state"
else:
s = "attack"
if count != 1:
s += "s"
return s
def __str__(self):
s = "claim id [%s]" % (self.id)
2006-08-02 13:59:57 +01:00
s+= " " + str(self.claimtype)
if self.parameter:
s+= " " + str(self.parameter)
# determine status
s+= " : %i " % (self.failed)
s+= self.stateName(self.failed)
if self.complete:
s+= " (complete)"
return s