1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/mc.py	Wed May 18 01:51:18 2011 +0200
     1.3 @@ -0,0 +1,69 @@
     1.4 +"""
     1.5 +Name:
     1.6 +Author: Eugen Sawin <sawine@informatik.uni-freiburg.de>
     1.7 +"""
     1.8 +
     1.9 +def main():    
    1.10 +    goal = ((0, 0, 0), (3, 3, 1))
    1.11 +    node = Node(((3, 3, 1), (0, 0, 0)))
    1.12 +    frontier = [node]
    1.13 +    explored = set()
    1.14 +    solutions = set()
    1.15 +    while len(frontier):
    1.16 +        node = frontier.pop()
    1.17 +        explored.add(node.state)      
    1.18 +        for action in actions(node.state):            
    1.19 +            child = Node(apply(node.state, action), node, action)      
    1.20 +            if child.state == child.parent.state:
    1.21 +                print child
    1.22 +                return
    1.23 +            if child.state not in explored and child not in frontier:
    1.24 +                if child.state == goal:
    1.25 +                    solutions.add(child)
    1.26 +                else:
    1.27 +                    frontier.append(child) 
    1.28 +    for i, s in enumerate(solutions):
    1.29 +        print "solution ", i
    1.30 +        parent = s.parent
    1.31 +        parents = []
    1.32 +        while parent:
    1.33 +            parents.append(parent)            
    1.34 +            parent = parent.parent
    1.35 +        print [p.state for p in reversed(parents)]
    1.36 +            
    1.37 +def negate(action):
    1.38 +    return (-action[0], -action[1], -action[2]) 
    1.39 +
    1.40 +def apply(state, action):
    1.41 +    if len(state) == 2:
    1.42 +        return (apply(state[0], action), apply(state[1], negate(action)))
    1.43 +    return (state[0] + action[0], state[1] + action[1], state[2] + action[2])
    1.44 +
    1.45 +def actions(state):      
    1.46 +    actions = [(-2, 0, -1), (-1, 0, -1), (-1, -1, -1), (0, -2, -1), (0, -1, -1)]
    1.47 +    actions.extend([negate(a)for a in actions])
    1.48 +    states = [apply(state, a) for a in actions]   
    1.49 +    good_states = [s[0] for s in states if s[0][2] >= 0 and s[1][2] >= 0 
    1.50 +                   and (s[0][0] >= s[0][1] or not s[0][0]) 
    1.51 +                   and (s[1][0] >= s[1][1] or not s[1][0])
    1.52 +                   and s[0][1] >= 0 and s[1][1] >= 0
    1.53 +                   and s[0][2] >= 0 and s[1][2] >= 0]
    1.54 +    return [a for a in actions if apply(state[0], a) in good_states]
    1.55 +
    1.56 +class Node(object):
    1.57 +    def __init__(self, state, parent=None, action=None, cost=None):
    1.58 +        self.state = state
    1.59 +        self.parent = parent
    1.60 +        self.action = action
    1.61 +        self.cost = cost
    1.62 +    
    1.63 +
    1.64 +from argparse import ArgumentParser
    1.65 +
    1.66 +def parse_arguments():
    1.67 +    parser = ArgumentParser(description="Parses simple modal logic syntax.")
    1.68 +    parser.add_argument("-f", "--formula", help="your formula") 
    1.69 +    return parser.parse_args()
    1.70 +
    1.71 +if __name__ == "__main__":
    1.72 +    main()