diff --git a/scripts/if2spdl/If.py b/scripts/if2spdl/If.py index 80be79e..b852427 100644 --- a/scripts/if2spdl/If.py +++ b/scripts/if2spdl/If.py @@ -70,6 +70,15 @@ class MsgList(list): for m in self: l = l + m.inTerms() + def __str__(self): + return "[ " + ", ".join(map(str,self)) + " ]" + + def getList(self): + l = [] + for e in self: + l.append(e) + return l + class Fact(list): def __repr__(self): return "Fact<" + list.__repr__(self) + ">" @@ -210,14 +219,47 @@ class MessageRule(Rule): def __init__(self,left=[],right=[]): Rule.__init__(self,left,right) self.actors = [] + # Add actors for fact in self.getFacts(): actor = fact.getActor() - if actor != None: + if actor != None and actor not in self.actors: self.actors.append(actor) + # Read/Send, before/after + self.readFact = None + self.before = None + for fact in self.left: + if type(fact) == MessageFact: + self.readFact = fact + elif type(fact) == PrincipalFact: + self.before = fact + self.sendFact = None + self.after = None + for fact in self.right: + if type(fact) == MessageFact: + self.sendFact = fact + elif type(fact) == PrincipalFact: + self.after = fact + + if self.before == None or self.after == None: + print "Warning: rule does not have both principal facts." + print self def __str__(self): return "Message " + Rule.__str__(self) + def getStepFrom(self): + if self.before != None: + return self.before.step + else: + return -1 + + def getStepTo(self): + if self.after != None: + return self.after.step + else: + return -1 + + class GoalRule(Rule): def __str__(self): return "Goal " + Rule.__str__(self) diff --git a/scripts/if2spdl/Ifparser.py b/scripts/if2spdl/Ifparser.py index 5a25d2f..c75e7d3 100755 --- a/scripts/if2spdl/Ifparser.py +++ b/scripts/if2spdl/Ifparser.py @@ -157,7 +157,7 @@ def ruleParser (): MsgList = Forward() MsgComp = Literal("c") + lbr + Message + comma + MsgList + rbr - MsgComp.setParseAction(lambda s,l,t: [ If.MsgList([ t[1] ]) + t[2] ]) + MsgComp.setParseAction(lambda s,l,t: [ If.MsgList([t[1]] + t[2].getList()) ]) MsgList << Or ([ MsgEtc, Variable, MsgComp ]) Step = Or ([ Number, Variable ]) @@ -218,7 +218,7 @@ def ruleParser (): mr3 = Literal("h") + lbr + Literal("xTime") + rbr + dot + MFPrincipal + Optional(dot + delimitedList(GoalFact, ".")) MessageRule = Group(mr1) + mr2 + Group(mr3) ## DEVIANT : BNF requires newlines MessageRule.setParseAction(lambda s,l,t: [ - If.MessageRule(t[0][3],t[1][2:]) ]) + If.MessageRule(t[0][3:],t[1][2:]) ]) InitialState = Literal("h") + lbr + Literal("xTime") + rbr + dot + State ## DEVIANT : BNF requires newlines InitialState.setParseAction(lambda s,l,t: [ If.InitialRule(t[2]) ]) diff --git a/scripts/if2spdl/Spdl.py b/scripts/if2spdl/Spdl.py index 5ebd07e..6137760 100644 --- a/scripts/if2spdl/Spdl.py +++ b/scripts/if2spdl/Spdl.py @@ -5,40 +5,12 @@ import If from misc import * -def action(protocol, actiontype, rule, fact): +def action(actiontype, fact): res = actiontype + "_" res += str(fact.step) res += fact.spdl() - res += ";\n" return res -def processRole(protocol, role): - - res = "" - print "Role", role - # initial knowledge - for rule in protocol: - if role in rule.getActors(): - for fact in rule.left: - if type(fact) == If.PrincipalFact: - print fact - - - # derive message sequence - for rule in protocol: - if role in rule.getActors(): - for fact in rule.left: - if type(fact) == If.MessageFact: - res += action(protocol, "read", rule, fact) - - for fact in rule.right: - if type(fact) == If.MessageFact: - res += action(protocol, "send", rule, fact) - - - print res - return "" - def getRoles(protocol): roles = [] @@ -46,12 +18,142 @@ def getRoles(protocol): roles += rule.getActors() return uniq(roles) +class Role(object): + """ Containts a list of rules, to be executed sequentially """ + def __init__(self,name,actor): + self.name = name + self.rules = [] + self.actor = actor + + def prependRule(self,rule): + self.rules = [rule] + self.rules + + def getLength(self): + return len(self.rules) + + def getFirst(self): + if self.getLength() > 0: + return self.rules[0] + else: + return None + + def getFirstStep(self): + return self.getFirst().getStepFrom() + + def getActor(self): + return self.actor + + def __str__(self): + res = "Role " + self.name + "\n\n" + for rule in self.rules: + res += str(rule) + res += "\n\n" + return res + + def spdl(self): + res = "" + if len(self.rules) == 0: + return res + res += "role " + self.name + " (" + # TODO Insert parameter agents + res += ")\n" + res += "{\n" + # TODO declare constants, variables + res += "\n" + # Message sequence + res += "\t// Knowledge before: " + str(self.rules[0].before.knowledge) + "\n" + for rule in self.rules: + # Read + if rule.readFact != None: + res += "\t" + action("read",rule.readFact) + ";\n" + # Show knowledge extending for this read + res += "\t// Knowledge delta: " + str(rule.before.runknowledge) + " -> " + str(rule.after.runknowledge) + "\n" + + + + # Send + if rule.sendFact != None: + res += "\t" + action("send",rule.sendFact) + ";\n" + # TODO claims + # Close up + res += "}\n\n" + return res + + def __cmp__(self,other): + return cmp(self.name, other.name) + +def extractRoles(protocol): + """ Extract the roles of a protocol description. This yields a + list of Role objects """ + + # Construct full list of rules to do + rulestodo = [] + for rule in protocol: + if type(rule) == If.MessageRule: + rulestodo.append(rule) + + # Now process them until none are left + # First, we have no rolenames yet + rolenames = [] + roles = [] + while len(rulestodo) > 0: + # Pick one hrule (with the highest step number, maybe) + highest = rulestodo[0].getStepFrom() + hrule = rulestodo[0] + for rule in rulestodo: + step = rule.getStepFrom() + step = max(step,rule.getStepTo()) + if step >= highest: + highest = step + hrule = rule + # hrule has been picked. Work back from here + # first make up a name + if len(hrule.getActors()) != 1: + print "Warning: weird actor list for hrule:", hrule.getActors() + name = "X" + actor = None + else: + actor = hrule.getActors()[0] + name = str(actor) + # Remove variable x prefix + if len(name) > 1 and name[0] == 'x': + name = name[1:] + + # This name is maybe already taken + if name in rolenames: + # Append counter + counter = 2 + while name + str(counter) in rolenames: + counter = counter+1 + name = name + str(counter) + + rolenames.append(name) + role = Role(name,actor) + roles.append(role) + + # Transfer to rule + role.prependRule(hrule) + rulestodo.remove(hrule) + + # Scan for preceding events until none is found + scan = True + while scan and role.getFirstStep() != -1: + scan = False + for rule in rulestodo: + if actor in rule.getActors() and rule.getStepTo() == role.getFirstStep(): + # This one works + role.prependRule(rule) + rulestodo.remove(rule) + scan = True + + return roles + def generator(protocol): - roles = getRoles(protocol) - print "Found",len(protocol),"rules." - print "Roles:", roles + roles = extractRoles(protocol) + roles.sort() res = "" + print "Found",len(roles),"roles." for role in roles: - res += processRole(protocol,role) + res += role.spdl() return res