Added modality distribution.
2 Name: sml - Simple Modal Logic Lib.
3 Description: sml provides classes for simple modal logic formulae construction and reduction. It also features a disfunctional parser for the SML syntax.
4 Author: Eugen Sawin <sawine@informatik.uni-freiburg.de>
9 # edit your formulae here
13 formula1 = Imp([Eq([p, q]), r])
14 formula2 = Not([Or([p, q])])
15 formula3 = Not([Not([p])])
16 formula = formula1 # choose your formula here
18 args = parse_arguments()
20 scanner = Scanner(TOKENS)
21 parser = Parser(SYNTAX, scanner)
22 (accepted, out, tree_nodes) = parser.parse(args.formula)
26 tree = SyntaxTree(out, tree_nodes)
29 print "formula: \t\t\t", formula
30 print "expanded -> and <->: \t\t", expand_imp_eq(formula)
31 print "reduced ~: \t\t\t", de_morgan(expand_imp_eq(formula))
32 print "reduced iterated modalities: \t", reduce_iter(de_morgan(expand_imp_eq(formula)))
33 print "distributed modalities+: \t", reduce_iter(dist(reduce_iter(de_morgan(expand_imp_eq(formula)))))
36 return [fun(v) for v in f.values]
38 def expand_imp_eq(formula):
39 map = {IMP: lambda (a, b): Or([Not([a]), b]),
40 EQ: lambda (a, b): And([Or([Not([a]), b]), Or([a, Not([b])])])}
41 if not isinstance(formula, Operator) or formula.id not in map:
43 return map[formula.id](values(expand_imp_eq, formula))
45 def de_morgan(formula):
46 negmap = {AND: lambda (a, b): Or([negate(a), negate(b)]),
47 OR: lambda (a, b): And([negate(a), negate(b)]),
48 BOX: lambda (a,): Diamond([negate(a)]),
49 DIAMOND: lambda (a,): Box([negate(a)]),
50 VARIABLE: lambda (a,): Not([a]),
53 return negmap[f.id](f.values)
54 if not isinstance(formula, Operator):
57 return negate(formula.values[0])
58 return formula.__class__(values(de_morgan, formula))
60 def reduce_iter(formula):
61 redset = set(((BOX, BOX), (DIAMOND, DIAMOND), (DIAMOND, BOX), (BOX, DIAMOND)))
62 if not isinstance(formula, Operator) or not isinstance(formula.values[0], Operator):
64 ids = (formula.id, formula.values[0].id)
66 return reduce_iter(formula.values[0])
67 return formula.__class__(values(reduce_iter, formula))
70 distmap = {(BOX, AND): lambda (a, b): And([Box([a]), Box([b])]),
71 (DIAMOND, OR): lambda (a, b): Or([Diamond([a]), Diamond([b])]),
72 (BOX, OR): lambda (a, b): (isinstance(a, Box) or isinstance(b, Box))
73 and Or([Box([a]), Box([b])]) or Box([Or([a, b])]),
74 (DIAMOND, AND): lambda (a, b): (isinstance(a, Diamond) or isinstance(b, Diamond))
75 and And([Diamond([a]), Diamond([b])]) or Diamond([And([a, b])])}
76 if not isinstance(formula, Operator) or not isinstance(formula.values[0], Operator):
78 ids = (formula.id, formula.values[0].id)
80 return distmap[ids](formula.values[0].values)
81 return formula.__class__(values(dist, formula))
94 class Operator(object):
95 def __init__(self, id, arity, values):
102 out = str(self.values[0])
104 out = self.id + str(self.values[0])
105 elif self.arity == 2:
106 out = "(" + str(self.values[0]) + " " + self.id + " " + str(self.values[1]) + ")"
111 def __init__(self, values):
112 Operator.__init__(self, NOT, Not.arity, values)
118 def __init__(self, values):
119 Operator.__init__(self, AND, And.arity, values)
123 def __init__(self, values):
124 Operator.__init__(self, OR, Or.arity, values)
128 def __init__(self, values):
129 Operator.__init__(self, IMP, Imp.arity, values)
133 def __init__(self, values):
134 Operator.__init__(self, EQ, Eq.arity, values)
138 def __init__(self, values):
139 Operator.__init__(self, BOX, Box.arity, values)
141 class Diamond(Operator):
143 def __init__(self, values):
144 Operator.__init__(self, DIAMOND, Diamond.arity, values)
146 class Variable(Operator):
148 def __init__(self, values):
149 Operator.__init__(self, VARIABLE, Variable.arity, values)
153 def __init__(self, values):
154 Operator.__init__(self, LB, Lb.arity, values)
158 def __init__(self, values):
159 Operator.__init__(self, RB, Rb.arity, values)
161 class Formula(object):
165 TOKENS = {re.compile("\("): Lb,
166 re.compile("\)"): Rb,
167 re.compile("~"): Not,
168 re.compile("&"): And,
169 re.compile("\|"): Or,
170 re.compile("->"): Imp,
171 re.compile("<->"): Eq,
172 re.compile("\[\]"): Box,
173 re.compile("<>"): Diamond,
174 re.compile("[a-z]+"): Variable}
176 class Scanner(object):
177 def __init__(self, tokens, source=None):
181 while self.i < len(self.source):
183 for p, token in self.tokens.iteritems():
184 m = p.match(self.source[self.i:])
188 return (token, value)
191 def reset(self, source):
206 SYNTAX = ((Variable,),
217 def __init__(self, parent, value):
221 def addChild(self, value):
222 self.children.append(self, node)
224 class Parser(object):
225 def __init__(self, syntax, scanner):
227 self.scanner = scanner
228 def parse(self, source):
229 table = {(S, Variable): 0,
238 (A, Variable, And): 5,
239 (A, Variable, Or): 6,
240 (A, Variable, Imp): 7,
241 (A, Variable, Eq): 8,
242 (A, Not, Variable, And): 5,
243 (A, Not, Variable, Or): 6,
244 (A, Not, Variable, Imp): 7,
245 (A, Not, Variable, Eq): 8}
250 self.scanner.reset(source)
251 (token, value) = self.scanner.next()
252 (lookahead, la_value) = self.scanner.next()
253 (lookahead2, la2_value) = self.scanner.next()
255 while token and len(stack):
258 tree_nodes.append((token, value))
260 #tree_nodes.append((stack.pop(), value))
261 (token, value) = (lookahead, la_value)
262 (lookahead, la_value) = (lookahead2, la2_value)
263 #(lookahead, _) = self.scanner.next()
264 (lookahead2, la2_value) = self.scanner.next()
267 if (top, token) in table:
268 action = table[(top, token)]
269 elif (top, token, lookahead) in table:
270 action = table[(top, token, lookahead)]
271 elif (top, token, lookahead, lookahead2) in table:
272 action = table[(top, token, lookahead, lookahead2)]
279 stack.extend(reversed(self.syntax[action]))
280 accepted = accepted and not len(stack)
281 return (accepted, out, tree_nodes)
283 class SyntaxTree(object):
284 def __init__(self, seq, tree_nodes):
287 self.root = self.compile(seq, tree_nodes)[0]
288 def compile(self, seq, tree_nodes):
293 c, v = tree_nodes.pop()
295 c, v = tree_nodes.pop()
296 stack.append(Variable(v))
298 stack.append(Not(self.compile(seq, tree_nodes)))
300 stack.extend(self.compile(seq, tree_nodes))
302 stack.append(Box(self.compile(seq, tree_nodes)))
304 stack.append(Diamond(self.compile(seq, tree_nodes)))
306 stack.append(And(self.compile(seq, tree_nodes)))
308 stack.append(Or(self.compile(seq, tree_nodes)))
310 stack.append(Imp(self.compile(seq, tree_nodes)))
312 stack.append(Eq(self.compile(seq, tree_nodes)))
315 from argparse import ArgumentParser
317 def parse_arguments():
318 parser = ArgumentParser(description="Parses simple modal logic syntax.")
319 parser.add_argument("-f", "--formula", help="your formula")
320 return parser.parse_args()
322 EXCUSE = """The formula was not accepted by me, because I don't like you and the rest of the world. I seem to have some issues with formulae with inner nesting and I generally suffer from my hasty implementation. I would like to thank you for your coorporation by providing the formula within the code file itself. Thank you. ~The Parser"""
324 if __name__ == "__main__":