author | blanchet |
Fri, 18 Oct 2013 13:38:55 +0200 | |
changeset 54150 | 942bb9d9b7a8 |
parent 54144 | 0fadd32e8d50 |
permissions | -rwxr-xr-x |
53100 | 1 |
#!/usr/bin/env python |
2 |
# Title: HOL/Tools/Sledgehammer/MaSh/src/mash |
|
50222 | 3 |
# Author: Daniel Kuehlwein, ICIS, Radboud University Nijmegen |
53100 | 4 |
# Copyright 2012 - 2013 |
50222 | 5 |
# |
6 |
# Entry point for MaSh (Machine Learning for Sledgehammer). |
|
7 |
||
50220 | 8 |
''' |
9 |
MaSh - Machine Learning for Sledgehammer |
|
10 |
||
11 |
MaSh allows to use different machine learning algorithms to predict relevant fact for Sledgehammer. |
|
12 |
||
13 |
Created on July 12, 2012 |
|
14 |
||
15 |
@author: Daniel Kuehlwein |
|
16 |
''' |
|
17 |
||
53119
ac18480cbf9d
new version of MaSh tool, with more server bugfixes
blanchet
parents:
53115
diff
changeset
|
18 |
import socket,sys,time,logging,os |
ac18480cbf9d
new version of MaSh tool, with more server bugfixes
blanchet
parents:
53115
diff
changeset
|
19 |
from os.path import realpath,dirname |
53100 | 20 |
|
21 |
from spawnDaemon import spawnDaemon |
|
22 |
from parameters import init_parser |
|
50840 | 23 |
|
53100 | 24 |
def communicate(data,host,port): |
54150 | 25 |
logger = logging.getLogger('communicate') |
26 |
sock = socket.socket(socket.AF_INET, socket.SOCK_STREAM) |
|
53100 | 27 |
try: |
28 |
sock.connect((host,port)) |
|
54144 | 29 |
sock.sendall(data+'\n') |
54079 | 30 |
received = '' |
31 |
cont = True |
|
32 |
counter = 0 |
|
33 |
while cont and counter < 100000: |
|
34 |
rec = sock.recv(4096) |
|
54144 | 35 |
if rec.endswith('stop'): |
54079 | 36 |
cont = False |
37 |
received += rec[:-4] |
|
38 |
else: |
|
39 |
received += rec |
|
40 |
counter += 1 |
|
54150 | 41 |
if rec == '': |
42 |
logger.warning('No response from server. Check server log for details.') |
|
43 |
except: |
|
53100 | 44 |
logger.warning('Communication with server failed.') |
45 |
received = -1 |
|
46 |
finally: |
|
47 |
sock.close() |
|
48 |
return received |
|
50220 | 49 |
|
53119
ac18480cbf9d
new version of MaSh tool, with more server bugfixes
blanchet
parents:
53115
diff
changeset
|
50 |
def start_server(host,port): |
ac18480cbf9d
new version of MaSh tool, with more server bugfixes
blanchet
parents:
53115
diff
changeset
|
51 |
logger = logging.getLogger('start_server') |
ac18480cbf9d
new version of MaSh tool, with more server bugfixes
blanchet
parents:
53115
diff
changeset
|
52 |
logger.info('Starting Server.') |
ac18480cbf9d
new version of MaSh tool, with more server bugfixes
blanchet
parents:
53115
diff
changeset
|
53 |
path = dirname(realpath(__file__)) |
54011
427b77238746
new version of MaSh that really honors the --port option and that checks for file name mismatches
blanchet
parents:
53789
diff
changeset
|
54 |
spawnDaemon(os.path.join(path,'server.py'),os.path.join(path,'server.py'),host,str(port)) |
53119
ac18480cbf9d
new version of MaSh tool, with more server bugfixes
blanchet
parents:
53115
diff
changeset
|
55 |
serverIsUp=False |
53555 | 56 |
for _i in range(20): |
53119
ac18480cbf9d
new version of MaSh tool, with more server bugfixes
blanchet
parents:
53115
diff
changeset
|
57 |
# Test if server is up |
ac18480cbf9d
new version of MaSh tool, with more server bugfixes
blanchet
parents:
53115
diff
changeset
|
58 |
try: |
ac18480cbf9d
new version of MaSh tool, with more server bugfixes
blanchet
parents:
53115
diff
changeset
|
59 |
sock = socket.socket(socket.AF_INET, socket.SOCK_STREAM) |
ac18480cbf9d
new version of MaSh tool, with more server bugfixes
blanchet
parents:
53115
diff
changeset
|
60 |
sock.connect((host,port)) |
ac18480cbf9d
new version of MaSh tool, with more server bugfixes
blanchet
parents:
53115
diff
changeset
|
61 |
sock.close() |
ac18480cbf9d
new version of MaSh tool, with more server bugfixes
blanchet
parents:
53115
diff
changeset
|
62 |
serverIsUp = True |
ac18480cbf9d
new version of MaSh tool, with more server bugfixes
blanchet
parents:
53115
diff
changeset
|
63 |
break |
ac18480cbf9d
new version of MaSh tool, with more server bugfixes
blanchet
parents:
53115
diff
changeset
|
64 |
except: |
ac18480cbf9d
new version of MaSh tool, with more server bugfixes
blanchet
parents:
53115
diff
changeset
|
65 |
time.sleep(0.5) |
ac18480cbf9d
new version of MaSh tool, with more server bugfixes
blanchet
parents:
53115
diff
changeset
|
66 |
if not serverIsUp: |
ac18480cbf9d
new version of MaSh tool, with more server bugfixes
blanchet
parents:
53115
diff
changeset
|
67 |
logger.error('Could not start server.') |
ac18480cbf9d
new version of MaSh tool, with more server bugfixes
blanchet
parents:
53115
diff
changeset
|
68 |
sys.exit(-1) |
ac18480cbf9d
new version of MaSh tool, with more server bugfixes
blanchet
parents:
53115
diff
changeset
|
69 |
return True |
ac18480cbf9d
new version of MaSh tool, with more server bugfixes
blanchet
parents:
53115
diff
changeset
|
70 |
|
50951 | 71 |
def mash(argv = sys.argv[1:]): |
50220 | 72 |
# Initializing command-line arguments |
53100 | 73 |
args = init_parser(argv) |
50388 | 74 |
# Set up logging |
50220 | 75 |
logging.basicConfig(level=logging.DEBUG, |
76 |
format='%(asctime)s %(name)-12s %(levelname)-8s %(message)s', |
|
77 |
datefmt='%d-%m %H:%M:%S', |
|
78 |
filename=args.log, |
|
50951 | 79 |
filemode='w') |
53100 | 80 |
logger = logging.getLogger('mash') |
81 |
||
50220 | 82 |
if args.quiet: |
83 |
logger.setLevel(logging.WARNING) |
|
50951 | 84 |
else: |
85 |
console = logging.StreamHandler(sys.stdout) |
|
86 |
console.setLevel(logging.INFO) |
|
87 |
formatter = logging.Formatter('# %(message)s') |
|
88 |
console.setFormatter(formatter) |
|
89 |
logging.getLogger('').addHandler(console) |
|
90 |
||
50220 | 91 |
if not os.path.exists(args.outputDir): |
92 |
os.makedirs(args.outputDir) |
|
93 |
||
53115
e08a58161bf1
new version of MaSh tool, with less broken server
blanchet
parents:
53100
diff
changeset
|
94 |
# Shutdown commands need not start the server fist. |
e08a58161bf1
new version of MaSh tool, with less broken server
blanchet
parents:
53100
diff
changeset
|
95 |
if args.shutdownServer: |
53789
8d9f4e89d8c8
new version of MaSh program, with proper shutdown
blanchet
parents:
53555
diff
changeset
|
96 |
logger.info('Sending shutdown command.') |
53115
e08a58161bf1
new version of MaSh tool, with less broken server
blanchet
parents:
53100
diff
changeset
|
97 |
try: |
53789
8d9f4e89d8c8
new version of MaSh program, with proper shutdown
blanchet
parents:
53555
diff
changeset
|
98 |
received = communicate('shutdown',args.host,args.port) |
8d9f4e89d8c8
new version of MaSh program, with proper shutdown
blanchet
parents:
53555
diff
changeset
|
99 |
logger.info(received) |
53115
e08a58161bf1
new version of MaSh tool, with less broken server
blanchet
parents:
53100
diff
changeset
|
100 |
except: |
e08a58161bf1
new version of MaSh tool, with less broken server
blanchet
parents:
53100
diff
changeset
|
101 |
pass |
e08a58161bf1
new version of MaSh tool, with less broken server
blanchet
parents:
53100
diff
changeset
|
102 |
return |
e08a58161bf1
new version of MaSh tool, with less broken server
blanchet
parents:
53100
diff
changeset
|
103 |
|
53100 | 104 |
# If server is not running, start it. |
53115
e08a58161bf1
new version of MaSh tool, with less broken server
blanchet
parents:
53100
diff
changeset
|
105 |
startedServer = False |
54011
427b77238746
new version of MaSh that really honors the --port option and that checks for file name mismatches
blanchet
parents:
53789
diff
changeset
|
106 |
received = communicate(' '.join(('ping',args.modelFile,args.dictsFile)),args.host,args.port) |
427b77238746
new version of MaSh that really honors the --port option and that checks for file name mismatches
blanchet
parents:
53789
diff
changeset
|
107 |
if received == -1: |
53119
ac18480cbf9d
new version of MaSh tool, with more server bugfixes
blanchet
parents:
53115
diff
changeset
|
108 |
startedServer = start_server(args.host,args.port) |
54011
427b77238746
new version of MaSh that really honors the --port option and that checks for file name mismatches
blanchet
parents:
53789
diff
changeset
|
109 |
elif received.startswith('Files do not match'): |
427b77238746
new version of MaSh that really honors the --port option and that checks for file name mismatches
blanchet
parents:
53789
diff
changeset
|
110 |
logger.error('Filesnames do not match!') |
427b77238746
new version of MaSh that really honors the --port option and that checks for file name mismatches
blanchet
parents:
53789
diff
changeset
|
111 |
logger.error('Modelfile server: '+ received.split()[-2]) |
427b77238746
new version of MaSh that really honors the --port option and that checks for file name mismatches
blanchet
parents:
53789
diff
changeset
|
112 |
logger.error('Modelfile argument: '+ args.modelFile) |
427b77238746
new version of MaSh that really honors the --port option and that checks for file name mismatches
blanchet
parents:
53789
diff
changeset
|
113 |
logger.error('Dictsfile server: '+ received.split()[-1]) |
427b77238746
new version of MaSh that really honors the --port option and that checks for file name mismatches
blanchet
parents:
53789
diff
changeset
|
114 |
logger.error('Dictsfile argument: '+ args.dictsFile) |
427b77238746
new version of MaSh that really honors the --port option and that checks for file name mismatches
blanchet
parents:
53789
diff
changeset
|
115 |
return |
427b77238746
new version of MaSh that really honors the --port option and that checks for file name mismatches
blanchet
parents:
53789
diff
changeset
|
116 |
|
53115
e08a58161bf1
new version of MaSh tool, with less broken server
blanchet
parents:
53100
diff
changeset
|
117 |
if args.init or startedServer: |
e08a58161bf1
new version of MaSh tool, with less broken server
blanchet
parents:
53100
diff
changeset
|
118 |
logger.info('Initializing Server.') |
53100 | 119 |
data = "i "+";".join(argv) |
120 |
received = communicate(data,args.host,args.port) |
|
121 |
logger.info(received) |
|
122 |
||
53152
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53119
diff
changeset
|
123 |
if not args.inputFile == None: |
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53119
diff
changeset
|
124 |
logger.debug('Using the following settings: %s',args) |
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53119
diff
changeset
|
125 |
# IO Streams |
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53119
diff
changeset
|
126 |
OS = open(args.predictions,'w') |
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53119
diff
changeset
|
127 |
IS = open(args.inputFile,'r') |
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53119
diff
changeset
|
128 |
lineCount = 0 |
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53119
diff
changeset
|
129 |
for line in IS: |
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53119
diff
changeset
|
130 |
lineCount += 1 |
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53119
diff
changeset
|
131 |
if lineCount % 100 == 0: |
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53119
diff
changeset
|
132 |
logger.info('On line %s', lineCount) |
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53119
diff
changeset
|
133 |
received = communicate(line,args.host,args.port) |
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53119
diff
changeset
|
134 |
if not received == '': |
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53119
diff
changeset
|
135 |
OS.write('%s\n' % received) |
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53119
diff
changeset
|
136 |
OS.close() |
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53119
diff
changeset
|
137 |
IS.close() |
53555 | 138 |
|
139 |
# Statistics |
|
140 |
if args.statistics: |
|
141 |
received = communicate('avgStats',args.host,args.port) |
|
142 |
logger.info(received) |
|
50619
b958a94cf811
new version of MaSh, with theory-level reasoning
blanchet
parents:
50482
diff
changeset
|
143 |
|
53152
cbd3c7c48d2c
learn new facts on query if there aren't too many of them in MaSh
blanchet
parents:
53119
diff
changeset
|
144 |
if args.saveModels: |
53115
e08a58161bf1
new version of MaSh tool, with less broken server
blanchet
parents:
53100
diff
changeset
|
145 |
communicate('save',args.host,args.port) |
50827 | 146 |
|
50388 | 147 |
|
53100 | 148 |
if __name__ == "__main__": |
50951 | 149 |
sys.exit(mash()) |