Commit 1e683db2 authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

New proper script

parent ab205c5f
......@@ -30,27 +30,6 @@ class ErrorRep(object):
def set_context(self, cont):
self.context = cont
def logical_or(elements):
"""
@return logical_formula: str - OR of the input list
"""
# print("or: elements:", elements)
if len(elements) == 0:
return
else:
return '(' + " or ".join(elements) + ')'
def logical_and(elements):
"""
@return logical_formula: str - AND of the input list
"""
# print("and: elements:", elements)
if len(elements) == 0:
return
else:
return '(' + " and ".join(elements) + ')'
def logical_operator(elements, operator):
"""
......@@ -62,50 +41,131 @@ def logical_operator(elements, operator):
return '(' + " {} ".format(operator).join(elements) + ')'
def camFile2notOr(camFile):
def make_logical_formula(previous_frontier_places, start_prop):
"""Make a logical formula based on previous results of MAC
translate a cam file into a logical formula to forbid previous cam
1 line: ex: "A B" => (A and B)
another line: ex: "B C" => (B and C)
merge all lines: (A and B) or (B and C)
forbid all combinaisons: not((A and B) or (B and C))
"""
with open(camFile, 'r') as file:
# Logical and between each place
cam_list = [logical_and(line.rstrip('\n').split('\t'))
for line in file]
def add_start_prop(prev_frontier_places_formula):
"""Deal with start_prop if given"""
if start_prop and prev_frontier_places_formula:
return start_prop + ' and (' + prev_frontier_places_formula + ')'
elif prev_frontier_places_formula:
return prev_frontier_places_formula
else:
return start_prop
cam_list = [logical_operator(frontier_places, 'and')
for frontier_places in previous_frontier_places]
if len(cam_list) != 0:
# Logical or between each line
return 'not(' + logical_or(cam_list) + ')'
else :
return ''
return add_start_prop('not(' + logical_operator(cam_list, 'or') + ')')
else:
return add_start_prop('')
def write_list(input_list, output_file) :
"""
write input_list in output_file, tabular form
"""
def main2(chart_file, cam_file, cam_step_file, cam_complete_file, cam_strong_file,
steps, final_prop, start_prop, inv_prop):
"""
with open(output_file, 'a') as file:
file.write('\t'.join(input_list) + '\n')
.. todo: handle these QUERY PARAMETERS... from GUI program
# if self.possible:
# if len(inv_prop) == 0:
# inv_prop = None
# else :
# inv_prop = "not ("+inv_prop+")"
# else:
# if len(inv_prop) != 0:
# sert pas:
# final_prop = "not ("+final_prop+" and "+inv_prop+")"
def get_last_line(input_file):
"""Return last line of steps file"""
"""
with open(input_file, "rb") as f:
first = f.readline() # Read the first line.
f.seek(-2, 2) # Jump to the second last byte.
try:
while f.read(1) != b"\n": # Until EOL is found...
# Raises an IOError if the file contains only 1 line
f.seek(-2, 1) # ...jump back the read byte plus one more.
return f.readline().rstrip('\n') # Read last line.
except IOError:
return first.rstrip('\n')
# Build MCLA
error_reporter = ErrorRep()
mcla = MCLAnalyser(error_reporter)
# Load file
mcla.build_from_chart_file(chart_file)
if error_reporter.error:
raise "Error during loading of file"
# Frontier places asked
previous_frontier_places = set()
while True:
frontier_places, min_steps = \
find_mac(mcla, start_prop, inv_prop, final_prop, steps)
# Add theese frontier places to set of previous ones
previous_frontier_places.update(frontier_places)
LOGGER.debug("Prev frontier places: " + \
str(previous_frontier_places))
# Compute the formula of the next start_property
start_prop = make_logical_formula(previous_frontier_places,
start_prop)
LOGGER.debug("Next start_prop formula: " + str(start_prop))
def find_mac(mcla, start_prop, inv_prop, final_prop, steps):
# Build query
query = MCLSimpleQuery(start_prop, inv_prop, final_prop)
# Is the property reacheable ?
reacheable = mcla.sq_is_satisfiable(query, steps)
# If yes, in how many steps ?
min_step = mcla.unfolder.get_current_step()
if reacheable:
LOGGER.info(
"Property {} is reacheable in {} steps".format(
final_prop, min_step
)
)
else:
LOGGER.info(
"Property {} is NOT reacheable in {} steps".format(
final_prop, min_step
)
)
LOGGER.info("STOP the search!")
exit()
# Find next MAC
next_mac_object = mcla.next_mac(query, min_step)
if next_mac_object:
LOGGER.debug("Next MAC object:\n{}".format(next_mac_object))
# Save MAC and timings
LOGGER.debug("Save MAC and timings...")
with open(cam_complete_file, 'a') as file:
next_mac_object.save(file)
# Save MAC
next_mac = next_mac_object.activated_frontier
LOGGER.debug("Save next MAC: {}".format(next_mac))
with open(cam_file, 'a') as file:
file.write('\t'.join(next_mac) + '\n')
# Save min steps
min_step = mcla.unfolder.get_current_step()
LOGGER.debug("Save minimal steps: {}".format(min_step))
with open(cam_step_file, 'a') as file:
file.write(str(min_step)+'\n')
return next_mac, min_step
else:
LOGGER.info("STOP the search! No more MAC.")
exit()
def main(chart_file, cam_file, cam_step_file, cam_complete_file, cam_strong_file,
steps, final_prop, start_prop, inv_prop):
......@@ -265,35 +325,12 @@ if __name__ == "__main__":
remove_file(cam_strong_file)
# MAC research
status = 0
while status == 0:
print("NEW LOOP !")
status = \
main(chart_file, # chart_file
cam_file, # cam_file
cam_step_file, # cam_step_file
cam_complete_file, # cam_complete_file
cam_strong_file, # cam_strong_file
steps, final_prop, start_prop, inv_prop
)
# QUERY PARAMETERS
# if self.possible:
# if len(inv_prop) == 0:
# inv_prop = None
# else :
# inv_prop = "not ("+inv_prop+")"
# else:
# if len(inv_prop) != 0:
# sert pas:
# final_prop = "not ("+final_prop+" and "+inv_prop+")"
main2(
chart_file, # chart_file
cam_file, # cam_file
cam_step_file, # cam_step_file
cam_complete_file, # cam_complete_file
cam_strong_file, # cam_strong_file
steps, final_prop, start_prop, inv_prop
)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment