- Much improved.
This commit is contained in:
parent
5c065a7bba
commit
58f3aafc65
@ -1,4 +1,43 @@
|
|||||||
#!/usr/bin/python
|
#!/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):
|
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]
|
print ll[0]
|
||||||
|
@ -66,18 +66,18 @@ def ifParse (str):
|
|||||||
Fact = Principal | MessageFact | IntruderKnowledge | TimeFact | Secret | Give | Witness | Request
|
Fact = Principal | MessageFact | IntruderKnowledge | TimeFact | Secret | Give | Witness | Request
|
||||||
|
|
||||||
#State = Fact + OptioZeroOrMore ("." + Fact)
|
#State = Fact + OptioZeroOrMore ("." + Fact)
|
||||||
State = delimitedList (Fact, ".")
|
State = Group(delimitedList (Fact, "."))
|
||||||
|
|
||||||
# Rules and labels
|
# Rules and labels
|
||||||
rulename = Word (alphanums + "_")
|
rulename = Word (alphanums + "_")
|
||||||
rulecategory = oneOf("Protocol_Rules Invariant_Rules Decomposition_Rules Intruder_Rules Init Goal")
|
rulecategory = oneOf("Protocol_Rules Invariant_Rules Decomposition_Rules Intruder_Rules Init Goal")
|
||||||
label = hash + "lb" + equ + rulename + com + "type" + equ + rulecategory
|
label = hash + "lb" + equ + rulename + com + "type" + equ + rulecategory
|
||||||
rule = State + Optional(implies + State)
|
rule = Group(State + Optional(implies + State))
|
||||||
labeledrule = Group(label + rule)
|
labeledrule = Group(label + rule)
|
||||||
typeflag = hash + "option" + equ + oneOf ("untyped","typed")
|
typeflag = hash + "option" + equ + oneOf ("untyped","typed")
|
||||||
|
|
||||||
# A complete file
|
# A complete file
|
||||||
iffile = typeflag + OneOrMore(labeledrule)
|
iffile = typeflag + Group(OneOrMore(labeledrule))
|
||||||
|
|
||||||
parser = iffile
|
parser = iffile
|
||||||
parser.ignore("##" + restOfLine)
|
parser.ignore("##" + restOfLine)
|
||||||
|
Loading…
Reference in New Issue
Block a user