diff --git a/scripts/if2spdl/If.py b/scripts/if2spdl/If.py index ecff5f5..dc38b36 100644 --- a/scripts/if2spdl/If.py +++ b/scripts/if2spdl/If.py @@ -48,6 +48,43 @@ class Fact(list): def __repr__(self): return "Fact<" + list.__repr__(self) + ">" +class GoalFact(Fact): + def __repr__(self): + return "Goal " + Fact.__repr__(self) + +class PrincipalFact(Fact): + def __str__(self): + res = "Principal Fact:" + res += "\nStep " + str(self[0]) + res += "\nReadNextFrom " + str(self[1]) + res += "\nActor " + str(self[2]) + res += "\nRunKnowledge " + str(self[3]) + res += "\nKnowledge " + str(self[4]) + #res += "\nBool " + str(self[5]) + res += "\nSession " + str(self[6]) + return res + "\n" + + def __repr__(self): + return str(self) + +class TimeFact(Fact): + def __repr__(self): + return "Time " + Fact.__repr__(self) + +class MessageFact(Fact): + def __str__(self): + res = "Message Fact:" + res += "\nStep " + str(self[0]) + res += "\nRealSender " + str(self[1]) + res += "\nClaimSender " + str(self[2]) + res += "\nRecipient " + str(self[3]) + res += "\nMessage " + str(self[4]) + res += "\nSession " + str(self[5]) + return res + "\n" + + def __repr__(self): + return str(self) + class State(list): def __repr__(self): return "State<" + list.__repr__(self) + ">" @@ -77,9 +114,13 @@ class Rule(object): if self.label != None: res += " (" + str(self.label) +")" res += "\n" - res += str(self.left) + "\n" - res += "=>\n" - res += str(self.right) + "\n" + if self.left != None: + res += str(self.left) + "\n" + if self.right != None: + if self.left != None: + res += "=>\n" + res += str(self.right) + "\n" + res += ".\n" return res def __repr__(self): diff --git a/scripts/if2spdl/Ifparser.py b/scripts/if2spdl/Ifparser.py index e261419..3484e32 100755 --- a/scripts/if2spdl/Ifparser.py +++ b/scripts/if2spdl/Ifparser.py @@ -138,9 +138,11 @@ def ruleParser (): # Principal fact Principal = Literal("w") + lbr + Step + comma + Agent + comma + Agent + comma + MsgList + comma + MsgList + comma + Boolean + comma + Session + rbr + Principal.setParseAction(lambda s,l,t: [ If.PrincipalFact(t[1:]) ]) # Message fact MessageFact = Literal("m") + lbr + Step + comma + Agent + comma + Agent + comma + Agent + comma + Message + comma + Session + rbr + MessageFact.setParseAction(lambda s,l,t: [ If.MessageFact(t[1:]) ]) # Goal fact Secret = Literal("secret") + lbr + Message + Literal("f") + lbr + Session + rbr + rbr @@ -148,6 +150,7 @@ def ruleParser (): Witness = Literal("witness") + lbr + Agent + comma + Agent + comma + Constant + comma + Message + rbr Request = Literal("request") + lbr + Agent + comma + Agent + comma + Constant + comma + Message + rbr GoalFact = Or ([ Secret, Give, Witness, Request ]) + GoalFact.setParseAction(lambda s,l,t: [ If.GoalFact(t) ]) # Goal State # It actually yields a rule (not a state per se) Correspondence = Principal + dot + Principal @@ -164,6 +167,7 @@ def ruleParser (): # TimeFact TimeFact = Literal("h") + lbr + Message + rbr + TimeFact.setParseAction(lambda s,l,t: [ If.TimeFact(t[1]) ]) # Intruder knowledge IntruderKnowledge = Literal("i") + lbr + Message + rbr @@ -180,7 +184,8 @@ def ruleParser (): mr2 = implies 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],t[1]) ]) + MessageRule.setParseAction(lambda s,l,t: [ + 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]) ]) @@ -216,8 +221,7 @@ def ifParser(): def labeledruleAction(s,l,t): rule = t[1] - if type(rule) == "Rule": - rule.setLabel(t[0]) + rule.setLabel(t[0]) return [rule] labeledrule.setParseAction(labeledruleAction) @@ -259,6 +263,8 @@ def linesParse(lines): parser = ifParser() result = parser.parseString("".join( lines[1:])) + + ### TEST #print result # Main code