Commit be601afa authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[lib] MCLTranslator: black

parent b0a3e6fc
......@@ -39,11 +39,17 @@
"""
Translators from guarded transition models to clause constraint models
"""
from cadbiom.models.biosignal.sig_expr import SigIdentExpr, SigSyncBinExpr, \
SigConstraintExpr
from cadbiom.models.biosignal.translators.gt_visitors import compile_cond, \
compile_event, compile_constraint
from cadbiom.models.biosignal.sig_expr import (
SigIdentExpr,
SigSyncBinExpr,
SigConstraintExpr,
)
from cadbiom.models.biosignal.translators.gt_visitors import (
compile_cond,
compile_event,
compile_constraint,
)
from cadbiom.models.clause_constraints.CLDynSys import Literal, Clause
......@@ -52,6 +58,7 @@ class MCLNoImplemented(Exception):
"""
Exception for non implemented features
"""
def __init__(self, mess):
self.message = mess
......@@ -70,7 +77,8 @@ class MCLSigExprVisitor(object):
@param output: the variable name y or None for intermediate expressions)
@param subexpressions: dictionary op#x#y -> literal for subexpressions memorization
"""
def __init__(self, cldyn_sys, output, subexpressions = None):
def __init__(self, cldyn_sys, output, subexpressions=None):
"""
@param cldyn_sys: clause constraint dynamical system to pupulate
"""
......@@ -87,7 +95,7 @@ class MCLSigExprVisitor(object):
if output:
# added because it may not appear in evolution
self.cldyn_sys.add_var(output)
self.output_lit = Literal(output, True) # output literal y
self.output_lit = Literal(output, True) # output literal y
else:
self.output_lit = None
......@@ -110,23 +118,21 @@ class MCLSigExprVisitor(object):
else:
return nlit # return the ident (Literal) if no output_var
def visit_sig_not(self, sexpr):
"""
if y is given and the expression is not f(X) we generate not y <=> f(X)
"""
if self.output_lit: # y = not exp or (not y) = not expr
if self.output_lit: # y = not exp or (not y) = not expr
slit = self.output_lit
self.output_lit = self.output_lit.lit_not()
notnl = sexpr.operand.accept(self)
self.output_lit = slit # restore preceding value
else :
self.output_lit = slit # restore preceding value
else:
nlit = sexpr.operand.accept(self)
notnl = nlit.lit_not()
# don't generate more clauses than operand
return notnl
def visit_sig_sync(self, binsexpr):
"""
the output_var is the next variable, the root of the tree
......@@ -156,7 +162,7 @@ class MCLSigExprVisitor(object):
if self.opti:
var = search_sub_exp(operator, nlit1, nlit2, True, self.sub_dict)
if var:
if self.output_lit: # y = var
if self.output_lit: # y = var
notnvar = var.lit_not()
cl1 = Clause([notnl, var])
cl2 = Clause([nlit, notnvar])
......@@ -182,7 +188,7 @@ class MCLSigExprVisitor(object):
# sub expression memorization
if self.opti:
key = operator + '#' + nlit1.code_name() + '#' + nlit2.code_name()
key = operator + "#" + nlit1.code_name() + "#" + nlit2.code_name()
self.sub_dict[key] = nlit
return nlit
......@@ -236,9 +242,9 @@ class MCLSigExprVisitor(object):
# check if both operands are clocks
if not dex.is_clock(self.cldyn_sys.symb_tab, check_clock):
mess = "Default signal:"+dex.__str__()+" is not a clock"
mess = "Default signal:" + dex.__str__() + " is not a clock"
self.reporter.display(mess)
return nlit # no meaning
return nlit # no meaning
# visit recursively each operand
olit = self.output_lit
......@@ -250,11 +256,11 @@ class MCLSigExprVisitor(object):
self.output_lit = olit
# is a similar expression already visited?
operator = 'default'
operator = "default"
if self.opti:
var = search_sub_exp(operator, nl1, nl2, True, self.sub_dict)
if var:
if self.output_lit: # y = var
if self.output_lit: # y = var
notnvar = var.lit_not()
cl1 = Clause([notnl, var])
cl2 = Clause([nlit, notnvar])
......@@ -265,12 +271,12 @@ class MCLSigExprVisitor(object):
# generate nlit = nl1 or nl2
self.cldyn_sys.add_clause(Clause([notnl, nl1, nl2])) # nl => nl1 or nl2
self.cldyn_sys.add_clause(Clause([notnl1, nlit])) # nl1 => nlit
self.cldyn_sys.add_clause(Clause([notnl2, nlit])) # nl2 => nlit
self.cldyn_sys.add_clause(Clause([notnl1, nlit])) # nl1 => nlit
self.cldyn_sys.add_clause(Clause([notnl2, nlit])) # nl2 => nlit
# sub expression memorization
if self.opti:
key = operator + '#' + nl1.code_name() + '#' + nl2.code_name()
key = operator + "#" + nl1.code_name() + "#" + nl2.code_name()
self.sub_dict[key] = nlit
return nlit
......@@ -294,9 +300,9 @@ class MCLSigExprVisitor(object):
# check if left operand is clock
if not wex.left_h.is_clock(self.cldyn_sys.symb_tab, check_clock):
mess = "Default signal:"+wex.__str__()+" is not a clock"
mess = "Default signal:" + wex.__str__() + " is not a clock"
self.reporter.display(mess)
return nlit # no meaning
return nlit # no meaning
# visit recursively each operand
olit = self.output_lit
......@@ -308,11 +314,11 @@ class MCLSigExprVisitor(object):
self.output_lit = olit
# is a similar expression already visited?
operator = 'when'
operator = "when"
if self.opti:
var = search_sub_exp(operator, nl1, nl2, False, self.sub_dict)
if var:
if self.output_lit: # y = var
if self.output_lit: # y = var
notnvar = var.lit_not()
cl1 = Clause([notnl, var])
cl2 = Clause([nlit, notnvar])
......@@ -323,12 +329,12 @@ class MCLSigExprVisitor(object):
# generate nlit = nl1 and nl2
# nl1 and nl2 => nlit
self.cldyn_sys.add_clause(Clause([notnl1, notnl2, nlit]))
self.cldyn_sys.add_clause(Clause([notnl, nl1])) # nlit => nl1
self.cldyn_sys.add_clause(Clause([notnl, nl2])) # nlit => nl2
self.cldyn_sys.add_clause(Clause([notnl, nl1])) # nlit => nl1
self.cldyn_sys.add_clause(Clause([notnl, nl2])) # nlit => nl2
# sub expression memorization
if self.opti:
key = operator + '#' + nl1.code_name() + '#' + nl2.code_name()
key = operator + "#" + nl1.code_name() + "#" + nl2.code_name()
self.sub_dict[key] = nlit
return nlit
......@@ -357,12 +363,13 @@ class MCLSigExprVisitor(object):
"""
raise MCLNoImplemented("MCLSigExprVisitor: Not yet implemented")
# helper fonctions
def gen_code_synchro(cex, visit):
"""
code generator for a synchro constraint
"""
if len(cex.arg) <2:
if len(cex.arg) < 2:
visit.reporter.display("Incorrect clock synchro")
return None
exp = cex.arg[0]
......@@ -373,11 +380,12 @@ def gen_code_synchro(cex, visit):
visit.cldyn_sys.add_clause(Clause([lit1, lit.lit_not()]))
lit1 = lit
def gen_code_exclu(cex, visit):
"""
code generator for an exclusion constraint
"""
if len(cex.arg) <2:
if len(cex.arg) < 2:
visit.reporter.display("Incorrect clock exclusion")
return None
llit = []
......@@ -385,21 +393,22 @@ def gen_code_exclu(cex, visit):
lit = exp.accept(visit)
llit.append(lit)
for i in range(len(llit)):
for j in range(i+1, len(llit)):
visit.cldyn_sys.add_clause(Clause([llit[i].lit_not(),
llit[j].lit_not()]))
for j in range(i + 1, len(llit)):
visit.cldyn_sys.add_clause(Clause([llit[i].lit_not(), llit[j].lit_not()]))
def gen_code_included(cex, visit):
"""
code generator for an inclusion constraint
"""
if len(cex.arg) !=2:
if len(cex.arg) != 2:
visit.reporter.display("Incorrect clock inclusion")
return None
lit1 = cex.arg[0].accept(visit)
lit2 = cex.arg[1].accept(visit)
visit.cldyn_sys.add_clause(Clause([lit1.lit_not(), lit2]))
def search_sub_exp(ope, op1, op2, com, sub_dict):
"""
search if an expression a op b was already translated to clause constraints
......@@ -409,13 +418,13 @@ def search_sub_exp(ope, op1, op2, com, sub_dict):
@param com: bool - true if operator is commutative
@param sub_dict:directory of sub expressions
"""
key = ope + '#' + op1.code_name() + '#' + op2.code_name()
key = ope + "#" + op1.code_name() + "#" + op2.code_name()
try:
val_var = sub_dict[key]
return val_var
except KeyError:
if com:
key = ope + '#' + op2.code_name() + '#' + op1.code_name()
key = ope + "#" + op2.code_name() + "#" + op1.code_name()
try:
val_var = sub_dict[key]
return val_var
......@@ -424,6 +433,7 @@ def search_sub_exp(ope, op1, op2, com, sub_dict):
else:
return None
class GT2Clauses(object):
"""
visit a charter_model based on guarded transitions and populate the associated
......@@ -437,14 +447,13 @@ class GT2Clauses(object):
"""
@param cldyn_sys: a new dynamic system in clause constraints.
"""
self.cl_ds = cldyn_sys # CLSysDyn to be populated
self.cl_ds = cldyn_sys # CLSysDyn to be populated
self.reporter = reporter # for error reporting
if opti:
self.sub_exp = dict() # for subexpression elimination
self.sub_exp = dict() # for subexpression elimination
else:
self.sub_exp = None
def visit_chart_model(self, model):
"""
Enter a model - after traversal, clock constraints are compiled
......@@ -452,8 +461,9 @@ class GT2Clauses(object):
model.clean_code()
model.get_root().accept(self)
gen_aux_clock_constraints(self.cl_ds)
gen_clock_constraints(model.constraints, self.cl_ds,
self.sub_exp, self.reporter)
gen_clock_constraints(
model.constraints, self.cl_ds, self.sub_exp, self.reporter
)
def visit_csimple_node(self, node):
"""
......@@ -513,13 +523,16 @@ class GT2Clauses(object):
for sst in node.sub_nodes:
sst.accept(self)
# helper functions
def check_clock(vva):
"""
simple check
"""
return vva[0] == 'clock'
return vva[0] == "clock"
def gen_transition_clock(trans, cl_ds, sub_exp, reporter):
"""
......@@ -553,9 +566,9 @@ def gen_transition_clock(trans, cl_ds, sub_exp, reporter):
# event compiling
if trans.event:
ev_sexpr, sex, free_clocks = compile_event(trans.event,
cl_ds.symb_tab,
True, reporter)
ev_sexpr, sex, free_clocks = compile_event(
trans.event, cl_ds.symb_tab, True, reporter
)
for hne in free_clocks:
cl_ds.add_free_clock(hne)
if ev_sexpr.is_ident():
......@@ -564,19 +577,19 @@ def gen_transition_clock(trans, cl_ds, sub_exp, reporter):
sexpv = MCLSigExprVisitor(cl_ds, None, sub_exp)
h_event = ev_sexpr.accept(sexpv)
if not log_sexp: # trans_h = ev because cond = True
if not log_sexp: # trans_h = ev because cond = True
return h_event
# register (trans.ori, h_event) since trans.ori is an
# induction place of h_event
if not trans.ori.is_perm():
cl_ds.add_place_clock(trans.ori.name, h_event.name)
nh_event = h_event.lit_not()
nnn = cl_ds.add_aux_var() # name of the transition clock
nnn = cl_ds.add_aux_var() # name of the transition clock
h_tr = Literal(nnn, True)
noth_tr = Literal(nnn, False)
cl1 = Clause([noth_tr, h_event]) # not tr_h or ev
cl1 = Clause([noth_tr, h_event]) # not tr_h or ev
cl_ds.add_clause(cl1)
cl2 = Clause([noth_tr, v_cond]) # not tr_h or cond
cl2 = Clause([noth_tr, v_cond]) # not tr_h or cond
cl_ds.add_clause(cl2)
# tr_h or (not cond) or (not ev)
cl3 = Clause([nh_event, notv_cond, h_tr])
......@@ -586,6 +599,7 @@ def gen_transition_clock(trans, cl_ds, sub_exp, reporter):
else:
return v_cond
def gen_transition_list_clock(ltr, cl_ds, sub_exp, reporter):
"""
@param ltr: a list of transitions - must be non_empty
......@@ -596,12 +610,12 @@ def gen_transition_list_clock(ltr, cl_ds, sub_exp, reporter):
The clause constraint dynamic system cl_ds is modified
"""
if ltr == []:
return None
return None
ltr_h = []
for trans in ltr:
if trans.ori.is_start():
continue # trans is a pseudo transition
if not trans.clock: # avoid multiple transition compilation
continue # trans is a pseudo transition
if not trans.clock: # avoid multiple transition compilation
tr_h = gen_transition_clock(trans, cl_ds, sub_exp, reporter)
trans.clock = tr_h
else:
......@@ -609,7 +623,7 @@ def gen_transition_list_clock(ltr, cl_ds, sub_exp, reporter):
ltr_h.append(tr_h)
if len(ltr_h) == 1:
return ltr_h[0]
h_name = cl_ds.add_aux_var() # name of the default clock
h_name = cl_ds.add_aux_var() # name of the default clock
h_def = Literal(h_name, True)
nh_def = Literal(h_name, False)
# add all the clauses h_def or not h_i
......@@ -623,6 +637,7 @@ def gen_transition_list_clock(ltr, cl_ds, sub_exp, reporter):
return h_def
def gen_simple_evolution(splace, cl_ds, sub_exp, reporter):
"""
generate evolution equation of a place as clauses constraints
......@@ -636,13 +651,11 @@ def gen_simple_evolution(splace, cl_ds, sub_exp, reporter):
pname = splace.name
p_lit = Literal(pname, True)
np_lit = Literal(pname, False)
pnext = pname+"`"
pnext = pname + "`"
pnext_lit = Literal(pnext, True)
npnext_lit = Literal(pnext, False)
h_in = gen_transition_list_clock(splace.incoming_trans,
cl_ds, sub_exp, reporter)
h_out = gen_transition_list_clock(splace.outgoing_trans,
cl_ds, sub_exp, reporter)
h_in = gen_transition_list_clock(splace.incoming_trans, cl_ds, sub_exp, reporter)
h_out = gen_transition_list_clock(splace.outgoing_trans, cl_ds, sub_exp, reporter)
# clauses for evolution equation
if h_in and h_out:
# not X' or h_in or X
......@@ -688,6 +701,7 @@ def gen_simple_evolution(splace, cl_ds, sub_exp, reporter):
cla = Clause([pnext_lit, np_lit])
cl_ds.add_clause(cla)
def gen_aux_clock_constraints(cl_ds):
"""
generate structural clock constraints:
......@@ -703,16 +717,17 @@ def gen_aux_clock_constraints(cl_ds):
llit.append(plit)
cl_ds.add_aux_clause(Clause(llit))
def gen_clock_constraints(constraints_txt, cl_ds, sub_exp, reporter):
"""
cleaning clock constraints
"""
text_const = ""
for cha in constraints_txt:
if cha != ';' and cha != '\n':
if cha != ";" and cha != "\n":
text_const += cha
else:
if cha == ';':
if cha == ";":
gen_code_clock_const(text_const, cl_ds, sub_exp, reporter)
text_const = ""
......@@ -738,4 +753,3 @@ def is_frontier(node):
if trans.ori.is_start():
return True
return False
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