From 58f3aafc65dc2b6753f0bc9a45d10d3748aaff95 Mon Sep 17 00:00:00 2001 From: ccremers Date: Wed, 16 Nov 2005 18:19:50 +0000 Subject: [PATCH] - Much improved. --- scripts/if2spdl/generator.py | 39 ++++++++++++++++++++++++++++++++++++ scripts/if2spdl/parser.py | 6 +++--- 2 files changed, 42 insertions(+), 3 deletions(-) diff --git a/scripts/if2spdl/generator.py b/scripts/if2spdl/generator.py index 4a4369c..d52c82b 100644 --- a/scripts/if2spdl/generator.py +++ b/scripts/if2spdl/generator.py @@ -1,4 +1,43 @@ #!/usr/bin/python +def unfold(arg): + for x in arg: + print x + +def initialState(arg): + print "Initial State" + unfold(arg) + +def protocolRules(arg): + print "Protocol Rules" + unfold(arg) + +# Goals: ignored for now +def goal(arg): + return + +def labeledRule(lr): + type = None + label = None + if lr[0] == "lb": + label = lr[1] + if lr[2] == "type": + type = lr[3] + arg = lr[4] + + if type == "Init": + initialState(arg) + elif type == "Protocol_Rules": + protocolRules(arg) + elif type == "Goal": + goal(arg) + def generateSpdl(ll): + if ll[0] == "option": + print "Option [" + ll[1] + "]" + for i in ll[2]: + labeledRule(i) + return + + print "Not understood element: " print ll[0] diff --git a/scripts/if2spdl/parser.py b/scripts/if2spdl/parser.py index 2e0cc13..be58823 100755 --- a/scripts/if2spdl/parser.py +++ b/scripts/if2spdl/parser.py @@ -66,18 +66,18 @@ def ifParse (str): Fact = Principal | MessageFact | IntruderKnowledge | TimeFact | Secret | Give | Witness | Request #State = Fact + OptioZeroOrMore ("." + Fact) - State = delimitedList (Fact, ".") + State = Group(delimitedList (Fact, ".")) # Rules and labels rulename = Word (alphanums + "_") rulecategory = oneOf("Protocol_Rules Invariant_Rules Decomposition_Rules Intruder_Rules Init Goal") label = hash + "lb" + equ + rulename + com + "type" + equ + rulecategory - rule = State + Optional(implies + State) + rule = Group(State + Optional(implies + State)) labeledrule = Group(label + rule) typeflag = hash + "option" + equ + oneOf ("untyped","typed") # A complete file - iffile = typeflag + OneOrMore(labeledrule) + iffile = typeflag + Group(OneOrMore(labeledrule)) parser = iffile parser.ignore("##" + restOfLine)