andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

- Some improvements to Python usage.

Browse Source
This commit is contained in:
ccremers 2005-12-05 15:35:00 +00:00
parent 40d5991ad0
commit b5f627054e
1 changed files with 9 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

25
scripts/if2spdl/Spdl.py
View File

@ -185,18 +185,15 @@ def sanitizeRole(protocol, role):
# Try to substitute stuff until sane # Try to substitute stuff until sane
# First check whether knowledge lists actually agree in length, # First check whether knowledge lists actually agree in length,
# otherwise this does not make sense at all. # otherwise this does not make sense at all.
nmax = len(rules)-1 for n in range(0,len(rules)-1):
n = 0
while n < nmax:
knowbefore = rules[n].after.runknowledge knowbefore = rules[n].after.runknowledge
knowafter = rules[n+1].before.runknowledge knowafter = rules[n+1].before.runknowledge
if len(knowbefore) != len(knowafter): if len(knowbefore) != len(knowafter):
print "Error: Lengths differ for step", n raise "KnowledgeDeltaLenDiff", n
else: else:
# The after items should be substituted by the # The after items should be substituted by the
# before items # before items
i = 0 for i in range(0,len(knowbefore)):
while i < len(knowbefore):
# Substitute this item # Substitute this item
msgfrom = knowafter[i] msgfrom = knowafter[i]
msgto = knowbefore[i] msgto = knowbefore[i]
@ -205,15 +202,11 @@ def sanitizeRole(protocol, role):
print "Substituting %s by %s" % (str(msgfrom), str(msgto)) print "Substituting %s by %s" % (str(msgfrom), str(msgto))
# In all subsequent terms... TODO or # In all subsequent terms... TODO or
# just the next one? # just the next one?
j = n+1 for j in range(n+1, len(rules)):
while j < len(rules):
events = ruleevents[j] events = ruleevents[j]
for ev in events: for ev in events:
ev.substitute(msgfrom, msgto) ev.substitute(msgfrom, msgto)
j = j+1
i = i + 1
n = n + 1
# Extract knowledge etc # Extract knowledge etc
role.knowledge = role.rules[0].before.knowledge role.knowledge = role.rules[0].before.knowledge
@ -234,8 +227,8 @@ def sanitizeRole(protocol, role):
# not necessarily correct. TODO # not necessarily correct. TODO
### constants.append(t) ### constants.append(t)
cname = "n" cname = "n"
rname = role.name rname = role.name.lower()
if rname[0] == "x": if rname.startswith("x"):
rname = rname[1:] rname = rname[1:]
cname += rname cname += rname
cname += str(noncecounter) cname += str(noncecounter)
@ -274,7 +267,7 @@ def extractRoles(protocol):
# First, we have no rolenames yet # First, we have no rolenames yet
rolenames = [] rolenames = []
roles = [] roles = []
while len(rulestodo) > 0: while (len(rulestodo) > 0):
# Pick one hrule (with the highest step number, maybe) # Pick one hrule (with the highest step number, maybe)
highest = rulestodo[0].getStepFrom() highest = rulestodo[0].getStepFrom()
hrule = rulestodo[0] hrule = rulestodo[0]
@ -298,7 +291,7 @@ def extractRoles(protocol):
if name in rolenames: if name in rolenames:
# Append counter # Append counter
counter = 2 counter = 2
while name + str(counter) in rolenames: while (name + str(counter) in rolenames):
counter = counter+1 counter = counter+1
name = name + str(counter) name = name + str(counter)
@ -312,7 +305,7 @@ def extractRoles(protocol):
# Scan for preceding events until none is found # Scan for preceding events until none is found
scan = True scan = True
while scan and role.getFirstStep() != -1: while (scan and role.getFirstStep() != -1):
scan = False scan = False
for rule in protocol: for rule in protocol:
if actor in rule.getActors() and rule.getStepTo() == role.getFirstStep(): if actor in rule.getActors() and rule.getStepTo() == role.getFirstStep():