# HG changeset patch # User Eugen Sawin # Date 1310946666 -7200 # Node ID d95a6fb428868108c4545efb82702f2677c7952c # Parent a0a90e9ae77a5a91a56773e5bb580dd8d4422b78 Updated with goodies. diff -r a0a90e9ae77a -r d95a6fb42886 downloads/cau.zip Binary file downloads/cau.zip has changed diff -r a0a90e9ae77a -r d95a6fb42886 downloads/sml.py --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/downloads/sml.py Mon Jul 18 01:51:06 2011 +0200 @@ -0,0 +1,447 @@ +""" +Name: sml - Simple Modal Logic Lib. +Description: sml provides classes for simple modal logic formulae construction and reduction. It also features a disfunctional parser for the SML syntax. +Author: Eugen Sawin +""" + +TMP_DIMACS = "dimacs~" +TMP_SOLUTION = "solution~" + +def main(): + # edit your formulae here + p = Variable("p") + q = Variable("q") + r = Variable("r") + s = Variable("s") + formula1 = Imp(Eq(p, q), r) + formula2 = Not(Or(p, q)) + formula3 = Not(Not(p)) + formula4 = Imp(Box(Imp(Diamond(p), p)), Box(Imp(p, Box(p)))) + formula5 = Imp(And(Or(p, q), r), Not(s)) + formula6 = And(Or(p, Or(q, Not(s))), And(Or(r, Not(s)), Or(Not(p), s))) + formula = formula6 # choose your formula here + + args = parse_arguments() + if (args.formula): + scanner = Scanner(TOKENS) + parser = Parser(SYNTAX, scanner) + (accepted, out, tree_nodes) = parser.parse(args.formula) + if not accepted: + print EXCUSE + return + tree = SyntaxTree(out, tree_nodes) + formula = tree.root + + original = formula + print "formula: \t\t\t%s [%i]" % (formula, formula.depth()) + formula = expand_imp_eq(formula) + print "expanded -> and <->: \t\t%s [%i]" % (formula, formula.depth()) + formula = de_morgan(formula) + print "reduced ~: \t\t\t%s [%i]" % (formula, formula.depth()) + formula = reduce_iter(formula) + print "reduced iterated modalities: \t%s [%i]" % (formula, formula.depth()) + formula = reduce_iter(dist_mod((formula))) + print "distributed modalities+: \t%s [%i]" % (formula, formula.depth()) + formula = mcnf(formula) + print "alpha mcnf: \t\t\t%s [%i]" % (formula, formula.depth()) + #cnf_formula = cnf(original) + #print "alpha cnf: \t\t\t%s [%i]" % (cnf_formula, cnf_formula.depth()) + + if not args.dimacs: + dimacs_file = TMP_DIMACS + else: + dimacs_file = args.dimacs + solution = sat_test(original, dimacs_file) + if solution: + print "satisfiable: \t\t\t%s " % (", ".join([str(s) for s in solution])) + else: + print "not satisfiable" + +from subprocess import call, PIPE + +def sat_test(formula, dimacs_file): + out, variables = dimacs(formula) + with open(dimacs_file, "w") as f: + f.write(out) + call(["minisat2", "-verb=0", dimacs_file, TMP_SOLUTION], stdout=PIPE) + with open(TMP_SOLUTION) as f: + solved, assignment = f.readlines() + solved = solved[0] == "S" + if solved: + positive = set() + for a in assignment.split(): + neg = a[0] == "-" + if not neg: + positive.add(int(a)) + solution = [] + for v, n in variables.iteritems(): + if n in positive: + solution.append(Variable(v)) + else: + solution.append(Not(Variable(v))) + return solution + +def dimacs(formula): + def clausify(f): + if f.id == AND: + c1 = clausify(f.values[0]) + c2 = clausify(f.values[1]) + if c1: + clauses.append(clausify(f.values[0])) + if c2: + clauses.append(clausify(f.values[1])) + if f.id == OR: + clause = [] + clause.extend(clausify(f.values[0])) + clause.extend(clausify(f.values[1])) + return clause + if f.id == NOT: + return ["-" + clausify(f.values[0])] + if f.id == VARIABLE: + if f.values[0] in variables: + n = variables[f.values[0]] + else: + n = len(variables) + 1 + variables[f.values[0]] = n + return str(n) + + variables = {} + clauses = [] + clausify(formula) + out = "c DIMACS CNF input file generated by sml\n" + out += "c Author: Eugen Sawin \n" + out += "p cnf %i %i\n" % (len(variables), len(clauses)) + out += " 0\n".join([" ".join(c) for c in clauses]) + " 0\n" + return out, variables + +def values(fun, f): + return [fun(v) for v in f.values] + +def expand_imp_eq(formula): + expmap = {IMP: lambda (a, b): Or(Not(a), b), + EQ: lambda (a, b): And(Or(Not(a), b), Or(a, Not(b)))} + if not isinstance(formula, Operator): + return formula + if formula.id in expmap: + return expmap[formula.id](values(expand_imp_eq, formula)) + return formula.__class__(*values(expand_imp_eq, formula)) + +def de_morgan(formula): + negmap = {AND: lambda (a, b): Or(negate(a), negate(b)), + OR: lambda (a, b): And(negate(a), negate(b)), + BOX: lambda (a,): Diamond(negate(a)), + DIAMOND: lambda (a,): Box(negate(a)), + VARIABLE: lambda (a,): Not(Variable(a)), + NOT: lambda (a,): a} + def negate(f): + return negmap[f.id](f.values) + if not isinstance(formula, Operator): + return formula + if formula.id == NOT: + return negate(formula.values[0]) + return formula.__class__(*values(de_morgan, formula)) + +def reduce_iter(formula): + redset = set(((BOX, BOX), (DIAMOND, DIAMOND), (DIAMOND, BOX), (BOX, DIAMOND))) + if not isinstance(formula, Operator) or not isinstance(formula.values[0], Operator): + return formula + ids = (formula.id, formula.values[0].id) + if ids in redset: + return reduce_iter(formula.values[0]) + return formula.__class__(*values(reduce_iter, formula)) + +def dist_mod(formula): + distmap = {(BOX, AND): lambda (a, b): And(Box(a), Box(b)), + (DIAMOND, OR): lambda (a, b): Or(Diamond(a), Diamond(b)), + (BOX, OR): lambda (a, b): (isinstance(a, Box) or isinstance(b, Box)) + and Or(Box(a), Box(b)) or Box(Or(a, b)), + (DIAMOND, AND): lambda (a, b): (isinstance(a, Diamond) or isinstance(b, Diamond)) + and And(Diamond(a), Diamond(b)) or Diamond(And(a, b))} + if not isinstance(formula, Operator) or not isinstance(formula.values[0], Operator): + return formula + ids = (formula.id, formula.values[0].id) + if ids in distmap: + return distmap[ids](values(dist_mod, formula.values[0])) + return formula.__class__(*values(dist_mod, formula)) + +def mcnf(formula): + if formula.id == OR: + conj_id = int(formula.values[1].id == AND) + return And(Or(formula.values[conj_id].values[0], formula.values[1 - conj_id]), + Or(formula.values[conj_id].values[1], formula.values[1 - conj_id])); + return formula + +def cnf(formula): + def part(f): + for v in f.values: + if v.id != VARIABLE: + sub_formulae.append(v) + part(v) + + def conjunct(f): + if len(bicon): + return And(f, conjunct(bicon.pop())) + return f + + sub_formulae = [formula] + part(formula) + sub_formulae.reverse() + known = {} + bicon = [] + for s in sub_formulae: + for i, v in enumerate(s.values): + if v in known: + s.values[i] = known[v] + bicon.append(Eq(Variable("x" + str(len(bicon))), s)) + known[s] = bicon[-1].values[0] + return mcnf(dist_mod(reduce_iter(de_morgan(expand_imp_eq(conjunct(known[formula])))))) + +""" The Parser - Do NOT look below this line! """ +import re + +NOT = "~" +AND = "&" +OR = "|" +IMP = "->" +EQ = "<->" +BOX = "[]" +DIAMOND = "<>" +VARIABLE = "VAR" +LB = "(" +RB = ")" + +class Operator(object): + def __init__(self, id, arity, *values): + self.id = id + self.arity = arity + self.values = list(values) + def depth(self): + if self.arity == 0: + return 0 + if self.id in (BOX, DIAMOND): + return 1 + self.values[0].depth() + if self.id == NOT: + return self.values[0].depth() + return max(self.values[0].depth(), self.values[1].depth()) + def __eq__(self, other): + return self.id == other.id and self.values == other.values # commutative types not considered yet + def __str__(self): + out = self.id + if self.arity == 0: + out = str(self.values[0]) + if self.arity == 1: + out = self.id + str(self.values[0]) + elif self.arity == 2: + out = "(" + str(self.values[0]) + " " + self.id + " " + str(self.values[1]) + ")" + return out + +class Not(Operator): + arity = 1 + def __init__(self, *values): + Operator.__init__(self, NOT, Not.arity, *values) + def __call__(self): + pass + +class And(Operator): + arity = 2 + def __init__(self, *values): + Operator.__init__(self, AND, And.arity, *values) + +class Or(Operator): + arity = 2 + def __init__(self, *values): + Operator.__init__(self, OR, Or.arity, *values) + +class Imp(Operator): + arity = 2 + def __init__(self, *values): + Operator.__init__(self, IMP, Imp.arity, *values) + +class Eq(Operator): + arity = 2 + def __init__(self, *values): + Operator.__init__(self, EQ, Eq.arity, *values) + +class Box(Operator): + arity = 1 + def __init__(self, *values): + Operator.__init__(self, BOX, Box.arity, *values) + +class Diamond(Operator): + arity = 1 + def __init__(self, *values): + Operator.__init__(self, DIAMOND, Diamond.arity, *values) + +class Variable(Operator): + arity = 0 + def __init__(self, *values): + Operator.__init__(self, VARIABLE, Variable.arity, *values) + +class Lb(Operator): + arity = -1 + def __init__(self, *values): + Operator.__init__(self, LB, Lb.arity, *values) + +class Rb(Operator): + arity = -1 + def __init__(self, *values): + Operator.__init__(self, RB, Rb.arity, *values) + +class Formula(object): + def __init__(self): + pass + +TOKENS = {re.compile("\("): Lb, + re.compile("\)"): Rb, + re.compile("~"): Not, + re.compile("&"): And, + re.compile("\|"): Or, + re.compile("->"): Imp, + re.compile("<->"): Eq, + re.compile("\[\]"): Box, + re.compile("<>"): Diamond, + re.compile("[a-z]+"): Variable} + +class Scanner(object): + def __init__(self, tokens, source=None): + self.tokens = tokens + self.reset(source) + def next(self): + while self.i < len(self.source): + re.purge() + for p, token in self.tokens.iteritems(): + m = p.match(self.source[self.i:]) + if m: + self.i += m.end(0) + value = m.group(0) + return (token, value) + self.i += 1 + return (None, None) + def reset(self, source): + self.i = 0 + self.source = source + +S = Formula +A = "A" +#0 S: (Variable,), +#1 S: (Not, S), +#2 S: (Lb, A, Rb), +#3 S: (Box, S), +#4 S: (Diamond, S), +#5 A: (S, And, S), +#6 A: (S, Or, S), +#7 A: (S, Imp, S), +#8 A: (S, Eq, S) +SYNTAX = ((Variable,), + (Not, S), + (Lb, A, Rb), + (Box, S), + (Diamond, S), + (S, And, S), + (S, Or, S), + (S, Imp, S), + (S, Eq, S)) + +class Parser(object): + def __init__(self, syntax, scanner): + self.syntax = syntax + self.scanner = scanner + def parse(self, source): + table = {(S, Variable): 0, + (S, Not): 1, + (S, Lb): 2, + (S, Box): 3, + (S, Diamond): 4, + (A, S, And): 5, + (A, S, Or): 6, + (A, S, Imp): 7, + (A, S, Eq): 8, + (A, Variable, And): 5, + (A, Variable, Or): 6, + (A, Variable, Imp): 7, + (A, Variable, Eq): 8, + (A, Not, Variable, And): 5, + (A, Not, Variable, Or): 6, + (A, Not, Variable, Imp): 7, + (A, Not, Variable, Eq): 8} + stack = [S] + tree_nodes = [] + tree = None + out = [] + self.scanner.reset(source) + (token, value) = self.scanner.next() + (lookahead, la_value) = self.scanner.next() + (lookahead2, la2_value) = self.scanner.next() + accepted = True + while token and len(stack): + top = stack[-1] + if top == token: + tree_nodes.append((token, value)) + stack.pop() + #tree_nodes.append((stack.pop(), value)) + (token, value) = (lookahead, la_value) + (lookahead, la_value) = (lookahead2, la2_value) + #(lookahead, _) = self.scanner.next() + (lookahead2, la2_value) = self.scanner.next() + else: + action = None + if (top, token) in table: + action = table[(top, token)] + elif (top, token, lookahead) in table: + action = table[(top, token, lookahead)] + elif (top, token, lookahead, lookahead2) in table: + action = table[(top, token, lookahead, lookahead2)] + if action is None: + accepted = False + break + + out.append(action) + stack.pop() + stack.extend(reversed(self.syntax[action])) + accepted = accepted and not len(stack) + return (accepted, out, tree_nodes) + +class SyntaxTree(object): + def __init__(self, seq, tree_nodes): + seq.reverse() + tree_nodes.reverse() + self.root = self.compile(seq, tree_nodes)[0] + def compile(self, seq, tree_nodes): + stack = [] + while len(seq): + s = seq.pop() + if s == 0: + c, v = tree_nodes.pop() + while c != Variable: + c, v = tree_nodes.pop() + stack.append(Variable(v)) + elif s == 1: + stack.append(Not(self.compile(seq, tree_nodes))) + elif s == 2: + stack.extend(self.compile(seq, tree_nodes)) + elif s == 3: + stack.append(Box(self.compile(seq, tree_nodes))) + elif s == 4: + stack.append(Diamond(self.compile(seq, tree_nodes))) + elif s == 5: + stack.append(And(self.compile(seq, tree_nodes))) + elif s == 6: + stack.append(Or(self.compile(seq, tree_nodes))) + elif s == 7: + stack.append(Imp(self.compile(seq, tree_nodes))) + elif s == 8: + stack.append(Eq(self.compile(seq, tree_nodes))) + return stack + +from argparse import ArgumentParser + +def parse_arguments(): + parser = ArgumentParser(description="Tries to parse simple modal logic syntax and reduces the formula. Edit your formula directly in the code file for best results.") + parser.add_argument("-f", "--formula", help="provide your own formula here, or better don't") + parser.add_argument("-d", "--dimacs", help="output file for the CNF DIMACS output") + return parser.parse_args() + +EXCUSE = """The formula was not accepted by me, because I do not like you. It is not personal. 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""" + +if __name__ == "__main__": + main() diff -r a0a90e9ae77a -r d95a6fb42886 downloads/tim.zip Binary file downloads/tim.zip has changed diff -r a0a90e9ae77a -r d95a6fb42886 factory/v2011/linksend.html --- a/factory/v2011/linksend.html Sat Jul 16 12:52:33 2011 +0200 +++ b/factory/v2011/linksend.html Mon Jul 18 01:51:06 2011 +0200 @@ -44,6 +44,7 @@

Recursive

  • -This End. +This End.
    +Recursive humour recycled from Stephan Schulz, to preserve the environment.
diff -r a0a90e9ae77a -r d95a6fb42886 factory/v2011/personalwork.html --- a/factory/v2011/personalwork.html Sat Jul 16 12:52:33 2011 +0200 +++ b/factory/v2011/personalwork.html Mon Jul 18 01:51:06 2011 +0200 @@ -1,4 +1,42 @@ -

Here an unfiltered, random stack of small hacks, that I've produced for recreational reasons.

+

Here is an unfiltered, undocumented, user-unfriendly random stack of little hacks, that I've produced for recreational reasons. I put them online in spirit of the liberation of useless machines.

+ +

Tim

+ + +

Cau

+cau screenshot +
    +
  • +

    Description

    +Is bad PI-approximation good enough? A cellular automaton-based PI-approximation machine with Tkinter-based visualisation.
    • +
  • +

    Version

    +Working, approximating, slowly visualising. +
    + Download Cau (Python and Tkinter required)
    • +
+ +

SML

+
    +
  • +

    Description

    +A simple Simple Modal Logic library doing all kinds of reductions including Modal Conjunctive Normal Form. It also features DIMACS output and a satisfiability test via MiniSat2.
    • +
  • +

    Version

    +Reliable version except for features noted as alpha. Parser has too much personality. +
    + Download SML (Python and MiniSat2 required)
    • +
+

NetChannel

  • @@ -6,9 +44,9 @@ NetChannel is a simple Python object for message-based network communication on the TCP/IP stack. NetChannel is based on stateful sessions for improved performance.
  • -

    Version 0.7

    +

    Version

    A stable prototype. -
    +
    Download NetChannel (Python required)
@@ -20,9 +58,9 @@ Eden Plotter or Eden One is a quick prototype for my genetic programming routines. It approximates a given function by the methods of GP.
  • -

    Version 0.9

    +

    Version

    An unendurable slow prototype. -
    +
    Download Eden Plotter (Python required)
    • @@ -47,11 +85,11 @@

  • Version Antquarium Prototype

    Antquarium is the predecessor of ANQ. It was an extended course assignment and serves as a prototype for ANQ. -
    +
    Download Antquarium for Windows (Python and .Net 2.0 required)
  • -

    Version 0.4.1

    +

    Version

    Stable version missing features like flow and runtime topology control.
    • @@ -70,7 +108,8 @@

  • Requirements

    -
    • Microsoft Windows XP or Vista
    • Graphics card supporting OpenGL 1.3 or higher
    • One keyboard with at least the arrow keys working
    Download Theme Blocks (1.4MB)
    +
    • Microsoft Windows XP or Vista
    • Graphics card supporting OpenGL 1.3 or higher
    • One keyboard with at least the arrow keys working
    +
    Download Theme Blocks (1.4MB)
    • @@ -84,9 +123,9 @@

  • Features

    • Three AI difficulty levels
    • Endless gameplay, play till you're bored!
    -
    +
    Download Pyng Pong for Windows (2.4MB)
    -
    +
    Download Pyng Pong Source (Python + PyGame needed) (0.4MB)
    • @@ -101,7 +140,7 @@

  • Features

    • Drag, create and remove sound sources
    • Height of placement sets the sound pitch
    -
    +
    Download Klangbild (Python and PyGlet required)