Commit 68329bef authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[lib] MCLA: black

parent 9bcc0045
......@@ -189,7 +189,7 @@ from cadbiom.models.guard_transitions.translators.chart_xml_pid import \
MakeModelFromPidFile
from cadbiom.models.guard_transitions.analyser.ana_visitors import TableVisitor
from cadbiom.models.clause_constraints.mcl.MCLTranslators import GT2Clauses
from cadbiom.models.clause_constraints.mcl.MCLTranslators import GT2Clauses
from cadbiom.models.clause_constraints.mcl.CLUnfolder import CLUnfolder
from cadbiom.models.clause_constraints.mcl.MCLSolutions import MCLException
......@@ -197,7 +197,10 @@ from cadbiom.models.clause_constraints.CLDynSys import CLDynSys
from cadbiom.models.guard_transitions.translators.cadlangLexer import cadlangLexer
from cadbiom.models.guard_transitions.translators.cadlangParser import cadlangParser
from cadbiom.models.guard_transitions.chart_model import ChartModel
from cadbiom.models.clause_constraints.mcl.MCLSolutions import FrontierSolution, DimacsFrontierSol
from cadbiom.models.clause_constraints.mcl.MCLSolutions import (
FrontierSolution,
DimacsFrontierSol,
)
from cadbiom.models.clause_constraints.mcl.MCLQuery import MCLSimpleQuery
from cadbiom import commons as cm
......@@ -347,7 +350,6 @@ class MCLAnalyser(object):
activated_per_sol = [sol.nb_activated_frontiers for sol in dimacs_solution_list]
return dimacs_solution_list[activated_per_sol.index(min(activated_per_sol))]
def __solve_with_inact_fsolution(self, dimacs_front_sol, query, max_step, max_sol):
"""Frontier states not activated in dimacs_front_sol (DimacsFrontierSol)
are **forced to be False at start**; solve this and return DimacsFrontierSol
......@@ -374,9 +376,11 @@ class MCLAnalyser(object):
# [[var] for var in dimacs_front_sol.frontier_values if var < 0]
# Intersection between pre-computed negative values for all frontiers
# (negative and positive) in the given solution, and all frontiers.
inactive_frontier_values = \
[[var] for var in
self.unfolder.frontiers_negative_values & dimacs_front_sol.frontier_values]
inactive_frontier_values = [
[var]
for var in self.unfolder.frontiers_negative_values
& dimacs_front_sol.frontier_values
]
# Append inactivated frontier places as a start property in DIMACS form
# PS: do not test dim_start: In the worse case, it's an empty list.
......@@ -386,7 +390,6 @@ class MCLAnalyser(object):
# Get <tuple <DimacsFrontierSol>>
return self.__sq_dimacs_frontier_solutions(query, max_step, max_sol)
def __prune_frontier_solution(self, fsol, query, max_step):
""""Take a frontier condition which induces a property "prop" and try to
reduce the number of activated frontier variables from this solution while
......@@ -432,25 +435,21 @@ class MCLAnalyser(object):
# PS: We need to index the result in less_activated_solution
# thus, this why __solve_with_inact_fsolution() returns a tuple.
dimacs_solutions = \
self.__solve_with_inact_fsolution(
sol_to_prune,
query,
max_step,
self.nb_sols_to_be_pruned
)
dimacs_solutions = self.__solve_with_inact_fsolution(
sol_to_prune, query, max_step, self.nb_sols_to_be_pruned
)
LOGGER.info(
"MCLA::Prune: Iteration %s, nb pruned inact solutions: %s",
i,
len(dimacs_solutions)
len(dimacs_solutions),
)
# PS: dimacs_solutions should never be None or empty
if len(dimacs_solutions) == 1:
# No new solution has been found,
# the current solution is the best (sol_to_prune)
return dimacs_solutions[0] # it's sol_to_prune variable
return dimacs_solutions[0] # it's sol_to_prune variable
# Seach for less activated solution
# Get the solution with the less number of activated states
......@@ -500,7 +499,6 @@ class MCLAnalyser(object):
# go
return self.unfolder.squery_is_satisfied(max_step)
def sq_solutions(self, query, max_step, max_sol, vvars, max_user_step=None):
"""Return a list of RawSolution objects
......@@ -570,8 +568,9 @@ class MCLAnalyser(object):
# variant_prop, dim_variant, steps_before_check
self.unfolder.init_with_query(query, check_query=False)
# go
return self.unfolder.squery_solve(vvars, max_step, max_sol, max_user_step=max_user_step)
return self.unfolder.squery_solve(
vvars, max_step, max_sol, max_user_step=max_user_step
)
def sq_frontier_solutions(self, query, max_step, max_sol):
"""Compute active frontier places and timings
......@@ -645,7 +644,9 @@ class MCLAnalyser(object):
"""
vvars = self.unfolder.frontier_values
# sq_solutions() returns <list <RawSolution>>
raw_sols = self.sq_solutions(query, max_step, max_sol, vvars, max_user_step=max_user_step)
raw_sols = self.sq_solutions(
query, max_step, max_sol, vvars, max_user_step=max_user_step
)
# Get unique DimacsFrontierSol objects from RawSolution objects
dimacfrontsol = DimacsFrontierSol.get_unique_dimacs_front_sols_from_raw_sols(raw_sols)
......@@ -660,7 +661,6 @@ class MCLAnalyser(object):
)
return dimacfrontsol
def __mac_exhaustive_search(self, query, max_user_step):
"""Return a generator of FrontierSolution objects.
......@@ -733,10 +733,7 @@ class MCLAnalyser(object):
# to avoid all activated solutions
# Get <tuple <DimacsFrontierSol>>
dimacs_front_sol = self.__sq_dimacs_frontier_solutions(
query,
min_step,
2,
max_user_step=max_user_step
query, min_step, 2, max_user_step=max_user_step
)
# Self-adjustment of min_step/max_step may have taken place;
......@@ -755,14 +752,13 @@ class MCLAnalyser(object):
LOGGER.info(
"MCLA:__mac_exhaustive_search: No more solution; current step %s",
self.unfolder.current_step
self.unfolder.current_step,
)
assert (self.unfolder.current_step == max_user_step)
assert self.unfolder.current_step == max_user_step
# just break the loop
break
# Get the solution with the less number of activated states
small_fsol = self.less_activated_solution(dimacs_front_sol)
......@@ -781,7 +777,7 @@ class MCLAnalyser(object):
)
LOGGER.debug(
"MCLA::mac_exhaustive_search: forbidden frontiers: %s",
forbidden_frontier_values
forbidden_frontier_values,
)
def next_mac(self, query, max_step):
......@@ -831,7 +827,6 @@ class MCLAnalyser(object):
return FrontierSolution.from_dimacs_front_sol(current_mac)
def mac_search(self, query, max_step):
"""Wrapper for __mac_exhaustive_search(); return a generator of
FrontierSolution objects.
......@@ -904,20 +899,19 @@ class MCLAnalyser(object):
@return: a list of variables (list<string>)
"""
# query with mac init frontier places and timing
inh_query1 = MCLSimpleQuery.from_frontier_sol_same_timing(mac,
self.unfolder)
inh_query1 = MCLSimpleQuery.from_frontier_sol_same_timing(mac, self.unfolder)
# query with negation of final prop as invariant property
if not query.final_prop:
raise MCLException("Query must have a final property")
if not query.inv_prop:
inv_prop = "not (" + query.final_prop + ")"
else:
inv_prop = query.inv_prop + "and (not (" + query.final_prop +"))"
inv_prop = query.inv_prop + "and (not (" + query.final_prop + "))"
inh_query2 = MCLSimpleQuery(None, inv_prop, None)
# init + timing + final property not reachable
inh_query = inh_query1.merge(inh_query2)
max_step = len(inh_query.variant_prop)
assert(max_step == len(mac.ic_sequence))
assert max_step == len(mac.ic_sequence)
# search solutions - diseable aux clauses
self.unfolder.set_include_aux_clauses(False)
......@@ -925,7 +919,6 @@ class MCLAnalyser(object):
self.unfolder.set_include_aux_clauses(True)
return next_inhib
def mac_inhibitor_search(self, mac, query, max_sol):
"""Search inhibitors for a mac scenario
......@@ -946,13 +939,13 @@ class MCLAnalyser(object):
if not query.inv_prop:
inv_prop = "not (" + query.final_prop + ")"
else:
inv_prop = query.inv_prop + "and (not (" + query.final_prop +"))"
inv_prop = query.inv_prop + "and (not (" + query.final_prop + "))"
inh_query2 = MCLSimpleQuery(None, inv_prop, None)
# init + timing + final property not reachable
inh_query = inh_query1.merge(inh_query2)
max_step = len(inh_query.variant_prop)
assert(max_step == len(mac.ic_sequence))
assert max_step == len(mac.ic_sequence)
# search solutions - diseable aux clauses
self.unfolder.set_include_aux_clauses(False)
# lsol = self.sq_frontier_solutions(inh_query, max_step, max_sol)
......@@ -979,8 +972,7 @@ class MCLAnalyser(object):
if not query.inv_prop:
inv_prop = "not (" + query.final_prop + ")"
else:
inv_prop = query.inv_prop + "and (not (" + query.final_prop +"))"
inv_prop = query.inv_prop + "and (not (" + query.final_prop + "))"
inh_query = MCLSimpleQuery(None, inv_prop, None)
query_1 = inh_query.merge(query_1)
return not self.sq_is_satisfiable(query_1, max_step)
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