Attention une mise à jour du service Gitlab va être effectuée le mardi 30 novembre entre 17h30 et 18h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes. Cette mise à jour intermédiaire en version 14.0.12 nous permettra de rapidement pouvoir mettre à votre disposition une version plus récente.

Commit 0f193aa3 authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[lib] CLDynSys: fix confusing attribute: DRY: remove list into their names

parent 50fe2004
......@@ -160,9 +160,9 @@ class CLDynSys(object):
:param report: Reporter for error reporting.
:param base_var_set: Set of ALL variables of the dynamic system
(including inputs, entities, clocks/events, auxiliary variables)
:param list_clauses: Clauses
:param clauses: Clauses
Added from MCLTranslator.
:param aux_list_clauses: Auxiliary clauses.
:param aux_clauses: Auxiliary clauses.
Added from MCLTranslator.
:param frontiers: All frontiers of the model.
Used by CLUnfolder.
......@@ -186,8 +186,8 @@ class CLDynSys(object):
:type symb_tab: <dict <str>: <tuple <str>, <int>>>
:type report: <Reporter>
:type base_var_set: <set <str>>
:type list_clauses: <list <Clause>>
:type aux_list_clauses: <list <Clause>>
:type clauses: <list <Clause>>
:type aux_clauses: <list <Clause>>
:type frontiers: <list <str>>
:type no_frontiers: <list <str>>
:type free_clocks: <list <str>>
......@@ -220,9 +220,9 @@ class CLDynSys(object):
Added to base_var_set
Added to inputs (May be added multiple times ?)
Clauses:
Added to list_clauses
Added to clauses
Auxiliary clauses:
Added to aux_list_clauses
Added to aux_clauses
"""
def __init__(self, symb_tab, report):
# symbol table of charter model produced by Table_visitor
......@@ -231,9 +231,9 @@ class CLDynSys(object):
self.report = report # reporter for errors
# Set of ALL variables of the dynamic system (including auxiliary ones).
self.base_var_set = set()
self.list_clauses = [] # clause form of the dynamic
self.clauses = [] # clause form of the dynamic
# structural constraints valid if there is no timing constraints
self.aux_list_clauses = []
self.aux_clauses = []
self.frontiers = [] # frontiers places of the model
self.no_frontiers = [] # Places that are not frontiers
......@@ -293,18 +293,14 @@ class CLDynSys(object):
self.base_var_set.add(name)
self.inputs.append(name) # May be added multiple times ?
def add_clause(self, cla):
"""
add a clause constraint
"""
def add_clause(self, clause):
"""add a clause constraint"""
#TODO: do not add satisfied clauses (n or not n)
self.list_clauses.append(cla)
self.clauses.append(clause)
def add_aux_clause(self, cla):
"""
add an auxiliary clause constraint
"""
self.aux_list_clauses.append(cla)
def add_aux_clause(self, clause):
"""add an auxiliary clause constraint"""
self.aux_clauses.append(clause)
def get_var_number(self):
"""Get the number of ALL variables of the dynamic system
......
......@@ -113,7 +113,7 @@ init_forward_unfolding():
Shifted attributes with __shift_step (nb of variables in the system):
- __forward_init_dynamic(): __dynamic_constraints:
Shift dynamic_system.list_clauses + dynamic_system.aux_list_clauses + init
Shift dynamic_system.clauses + dynamic_system.aux_clauses + init
- __shift_final(): __final_constraints:
Shift + replace __final_constraints
- __shift_invariant(): __invariant_constraints:
......@@ -268,8 +268,8 @@ class CLUnfolder(object):
# i.e with a last char '`' at the end.
# Thus it is easy to search them directly in the dict (in O(1)),
# instead of slicing them.
# Note: "future" literals are already in self.dynamic_system.list_clauses
# and maybe in self.dynamic_system.aux_list_clauses
# Note: "future" literals are already in self.dynamic_system.clauses
# and maybe in self.dynamic_system.aux_clauses
temp_var_code_table = \
{var_name + "`": var_num for var_name, var_num in self.__var_code_table.iteritems()}
self.__var_code_table.update(temp_var_code_table)
......@@ -804,13 +804,13 @@ class CLUnfolder(object):
if self.__include_aux_clauses:
# Auxiliary clauses are supported (default)
self.__dynamic_constraints = \
forward_init_dynamic(self.dynamic_system.list_clauses,
forward_init_dynamic(self.dynamic_system.clauses,
self.__var_code_table,
self.__shift_step,
self.dynamic_system.aux_list_clauses)
self.dynamic_system.aux_clauses)
else:
self.__dynamic_constraints = \
forward_init_dynamic(self.dynamic_system.list_clauses,
forward_init_dynamic(self.dynamic_system.clauses,
self.__var_code_table,
self.__shift_step)
......@@ -826,12 +826,12 @@ class CLUnfolder(object):
"""
num_clause_list = \
[self.__backward_code(clause)
for clause in self.dynamic_system.list_clauses]
for clause in self.dynamic_system.clauses]
if self.__include_aux_clauses:
num_clause_list += \
[self.__backward_code(clause)
for clause in self.dynamic_system.aux_list_clauses]
for clause in self.dynamic_system.aux_clauses]
self.__dynamic_constraints = [num_clause_list]
......@@ -1333,7 +1333,7 @@ class CLUnfolder(object):
Shifted attributes with __shift_step (nb of variables in the system):
- __dynamic_constraints:
Shift dynamic_system.list_clauses + dynamic_system.aux_list_clauses + init
Shift dynamic_system.clauses + dynamic_system.aux_clauses + init
- __final_constraints:
Shift + replace __final_constraints
- __invariant_constraints:
......
......@@ -102,7 +102,7 @@ class TestTransitionClauses(unittest.TestCase):
TRACE_FILE.write( '\n\nn1 --> n2; []\n')
htr = gen_transition_clock(trans, cl_ds, None, reporter)
TRACE_FILE.write( 'Transition clock:'+ htr.__str__()+'\n')
for cla in cl_ds.list_clauses:
for cla in cl_ds.clauses:
TRACE_FILE.write( cla.__str__()+'\n')
mess = 'free clocks registered:' + cl_ds.free_clocks.__str__() + '\n'
TRACE_FILE.write(mess)
......@@ -128,7 +128,7 @@ class TestTransitionClauses(unittest.TestCase):
TRACE_FILE.write( '\n\nn1 --> n2; [not n3]'+'\n')
htr = gen_transition_clock(trans, cl_ds, None, reporter)
TRACE_FILE.write( 'Transition clock:' + htr.__str__()+'\n')
for cla in cl_ds.list_clauses:
for cla in cl_ds.clauses:
TRACE_FILE.write( cla.__str__() + '\n')
mess = 'free clocks registered:' + cl_ds.free_clocks.__str__()+'\n'
TRACE_FILE.write(mess)
......@@ -153,7 +153,7 @@ class TestTransitionClauses(unittest.TestCase):
TRACE_FILE.write( '\n\nn1 --> n2; h[]'+'\n')
htr = gen_transition_clock(trans, cl_ds, None, reporter)
TRACE_FILE.write( 'Transition clock:'+ htr.__str__()+'\n')
for cla in cl_ds.list_clauses:
for cla in cl_ds.clauses:
TRACE_FILE.write( cla.__str__() + '\n')
mess = 'free clocks registered:' +cl_ds.free_clocks.__str__()+'\n'
TRACE_FILE.write(mess)
......@@ -166,7 +166,7 @@ class TestTransitionClauses(unittest.TestCase):
cl_ds = CLDynSys(tvisit.tab_symb, reporter)
htr = gen_transition_clock(trans, cl_ds, sed, reporter)
TRACE_FILE.write( 'Transition clock:'+ htr.__str__()+'\n')
for cla in cl_ds.list_clauses:
for cla in cl_ds.clauses:
TRACE_FILE.write( cla.__str__()+'\n')
mess = 'free clocks registered:' + cl_ds.free_clocks.__str__() + '\n'
TRACE_FILE.write(mess)
......@@ -193,7 +193,7 @@ class TestTransitionClauses(unittest.TestCase):
TRACE_FILE.write( '\n\nn1 --> n2; h[not n3]'+'\n')
htr = gen_transition_clock(trans, cl_ds, None, reporter)
TRACE_FILE.write( 'Transition clock:'+ htr.__str__()+'\n')
for cla in cl_ds.list_clauses:
for cla in cl_ds.clauses:
TRACE_FILE.write( cla.__str__()+'\n')
mess = 'free clocks registered:'+ cl_ds.free_clocks.__str__()+'\n'
TRACE_FILE.write(mess)
......@@ -209,7 +209,7 @@ class TestTransitionClauses(unittest.TestCase):
TRACE_FILE.write( '\n\nn1 --> n2; h[not n3]'+'\n')
htr = gen_transition_clock(trans, cl_ds, sed, reporter)
TRACE_FILE.write( 'Transition clock:'+ htr.__str__()+'\n')
for cla in cl_ds.list_clauses:
for cla in cl_ds.clauses:
TRACE_FILE.write( cla.__str__()+'\n')
mess = 'free clocks registered:'+ cl_ds.free_clocks.__str__()+'\n'
TRACE_FILE.write(mess)
......@@ -238,7 +238,7 @@ class TestTransitionClauses(unittest.TestCase):
TRACE_FILE.write( '\n\nn1/p --> n2; h[]'+'\n' )
htr = gen_transition_clock(trans, cl_ds, None, reporter)
TRACE_FILE.write( 'Transition clock:'+htr.__str__()+'\n')
for cla in cl_ds.list_clauses:
for cla in cl_ds.clauses:
TRACE_FILE.write( cla.__str__()+'\n')
mess = 'free clocks registered:'+ cl_ds.free_clocks.__str__()+'\n'
TRACE_FILE.write(mess)
......@@ -266,7 +266,7 @@ class TestTransitionClauses(unittest.TestCase):
TRACE_FILE.write( '\n\nn1/p --> n2; h[n4]' +'\n')
htr = gen_transition_clock(trans, cl_ds, None, reporter)
TRACE_FILE.write( 'Transition clock:'+ htr.__str__()+'\n')
for cla in cl_ds.list_clauses:
for cla in cl_ds.clauses:
TRACE_FILE.write(cla.__str__()+'\n')
mess = 'free clocks registered:'+ cl_ds.free_clocks.__str__()+'\n'
TRACE_FILE.write(mess)
......@@ -294,7 +294,7 @@ class TestTransitionClauses(unittest.TestCase):
TRACE_FILE.write( '\n\nn1/i --> n2; h[n4]'+'\n')
htr = gen_transition_clock(trans, cl_ds, None, reporter)
TRACE_FILE.write( 'Transition clock:' +htr.__str__()+'\n')
for cla in cl_ds.list_clauses:
for cla in cl_ds.clauses:
TRACE_FILE.write( cla.__str__()+'\n')
mess = 'free clocks registered:'+ cl_ds.free_clocks.__str__()+'\n'
TRACE_FILE.write(mess)
......@@ -322,7 +322,7 @@ class TestTransitionClauses(unittest.TestCase):
TRACE_FILE.write( '\n\nn1 --> n2; h when n3[]; n3;'+'\n')
htr = gen_transition_clock(trans, cl_ds, None, reporter)
TRACE_FILE.write( 'Transition clock:'+ htr.__str__()+'\n')
for cla in cl_ds.list_clauses:
for cla in cl_ds.clauses:
TRACE_FILE.write( cla.__str__()+'\n')
mess = 'free clocks registered:' +cl_ds.free_clocks.__str__()+'\n'
TRACE_FILE.write(mess)
......@@ -357,7 +357,7 @@ class TestTransitionClauses(unittest.TestCase):
TRACE_FILE.write( 'Transition clock:'+ htr.__str__()+'\n')
htr = gen_transition_clock(tr2, cl_ds, None, reporter)
TRACE_FILE.write( 'Transition clock:'+ htr.__str__()+'\n')
for cla in cl_ds.list_clauses:
for cla in cl_ds.clauses:
TRACE_FILE.write( cla.__str__()+'\n')
mess = 'free clocks registered:' +cl_ds.free_clocks.__str__()+'\n'
TRACE_FILE.write(mess)
......@@ -391,7 +391,7 @@ class TestTransitionClauses(unittest.TestCase):
TRACE_FILE.write( 'Transition clock:'+ htr.__str__()+'\n')
htr = gen_transition_clock(tr2, cl_ds, None, reporter)
TRACE_FILE.write( 'Transition clock:'+ htr.__str__()+'\n')
for cla in cl_ds.list_clauses:
for cla in cl_ds.clauses:
TRACE_FILE.write( cla.__str__()+'\n')
mess = 'free clocks registered:' +cl_ds.free_clocks.__str__()+'\n'
TRACE_FILE.write(mess)
......@@ -423,7 +423,7 @@ class TestTransitionClauses(unittest.TestCase):
htr = gen_transition_clock(tr1, cl_ds, None, reporter)
TRACE_FILE.write( 'Transition clock:'+ htr.__str__()+'\n')
for cla in cl_ds.list_clauses:
for cla in cl_ds.clauses:
TRACE_FILE.write( cla.__str__()+'\n')
mess = 'free clocks registered:' +cl_ds.free_clocks.__str__()+'\n'
TRACE_FILE.write(mess)
......@@ -473,8 +473,8 @@ class TestTransitionList(unittest.TestCase):
sed = dict()
htr = gen_transition_list_clock(trl, cl_ds, sed, reporter)
TRACE_FILE.write( 'Transition clock:' +htr.__str__()+'\n')
TRACE_FILE.write( 'NB Clauses:' +str(len(cl_ds.list_clauses))+'\n')
for cla in cl_ds.list_clauses:
TRACE_FILE.write( 'NB Clauses:' +str(len(cl_ds.clauses))+'\n')
for cla in cl_ds.clauses:
TRACE_FILE.write( cla.__str__()+'\n')
mess = 'free clocks registered:'+cl_ds.free_clocks.__str__()+'\n'
TRACE_FILE.write(mess)
......@@ -498,7 +498,7 @@ class TestTransitionList(unittest.TestCase):
TRACE_FILE.write('\ntestVerySimple')
TRACE_FILE.write( '\n\nn1 --> n2; [] \n')
gen_simple_evolution(nn1, cl_ds, None, reporter)
for cla in cl_ds.list_clauses:
for cla in cl_ds.clauses:
TRACE_FILE.write( cla.__str__()+'\n')
mess = 'free clocks registered:'+cl_ds.free_clocks.__str__()+'\n'
TRACE_FILE.write(mess)
......@@ -534,8 +534,8 @@ class TestTransitionList(unittest.TestCase):
TRACE_FILE.write(mess)
sed = dict()
gen_simple_evolution(nn1, cl_ds, sed, reporter)
TRACE_FILE.write( 'NB Clauses:' + str(len(cl_ds.list_clauses)) + '\n')
for cla in cl_ds.list_clauses:
TRACE_FILE.write( 'NB Clauses:' + str(len(cl_ds.clauses)) + '\n')
for cla in cl_ds.clauses:
TRACE_FILE.write( cla.__str__() + '\n')
mess = 'free clocks registered:'+ cl_ds.free_clocks.__str__()+'\n'
TRACE_FILE.write(mess)
......@@ -565,7 +565,7 @@ class TestTransitionList(unittest.TestCase):
TRACE_FILE.write('\ntestSimpleInNoOut')
TRACE_FILE.write( '\n\nn2 --> n1; h1[not n4] \nn4 --> n1; h3[]\n')
gen_simple_evolution(nn1, cl_ds, None, reporter)
for cla in cl_ds.list_clauses:
for cla in cl_ds.clauses:
TRACE_FILE.write( cla.__str__()+'\n')
mess = 'free clocks registered:' + cl_ds.free_clocks.__str__() + '\n'
TRACE_FILE.write(mess)
......@@ -595,7 +595,7 @@ class TestTransitionList(unittest.TestCase):
TRACE_FILE.write('\ntestSimpleOutNoIn')
TRACE_FILE.write( '\n\nn1 --> n2; h1[not n4] \nn1 --> n3; '+'\n')
gen_simple_evolution(nn1, cl_ds, None, reporter)
for cla in cl_ds.list_clauses:
for cla in cl_ds.clauses:
TRACE_FILE.write( cla.__str__()+'\n')
mess = 'free clocks registered:'+ cl_ds.free_clocks.__str__()+'\n'
TRACE_FILE.write(mess)
......@@ -615,7 +615,7 @@ class TestTransitionList(unittest.TestCase):
TRACE_FILE.write('\ntestSimpleNoTrans')
TRACE_FILE.write( '\n\nn1; \n')
gen_simple_evolution(nn1, cl_ds, None, reporter)
for cla in cl_ds.list_clauses:
for cla in cl_ds.clauses:
TRACE_FILE.write( cla.__str__() + '\n')
mess = 'free clocks registered:' + cl_ds.free_clocks.__str__() + '\n'
TRACE_FILE.write(mess)
......@@ -655,8 +655,8 @@ class TestFull(unittest.TestCase):
TRACE_FILE.write(mess)
gt2clauses = GT2Clauses(cl_ds, False, reporter)
model.accept(gt2clauses)
TRACE_FILE.write( 'NB Clauses:' +str(len(cl_ds.list_clauses))+'\n')
for cla in cl_ds.list_clauses:
TRACE_FILE.write( 'NB Clauses:' +str(len(cl_ds.clauses))+'\n')
for cla in cl_ds.clauses:
TRACE_FILE.write( cla.__str__()+'\n')
TRACE_FILE.write( 'variables'+ cl_ds.base_var_set.__str__()+'\n')
mess = 'free clocks registered:'+ cl_ds.free_clocks.__str__()+'\n'
......@@ -694,7 +694,7 @@ class TestFull(unittest.TestCase):
TRACE_FILE.write(mess)
gt2clauses = GT2Clauses(cl_ds, reporter, False)
model.accept(gt2clauses)
for cla in cl_ds.list_clauses:
for cla in cl_ds.clauses:
TRACE_FILE.write( cla.__str__()+'\n')
TRACE_FILE.write( 'variables'+ cl_ds.base_var_set.__str__()+'\n')
mess = 'free clocks registered:'+ cl_ds.free_clocks.__str__()+'\n'
......@@ -732,7 +732,7 @@ class TestFull(unittest.TestCase):
TRACE_FILE.write( '\n\n\n')
gt2clauses = GT2Clauses(cl_ds, reporter, False)
model.accept(gt2clauses)
for cla in cl_ds.list_clauses:
for cla in cl_ds.clauses:
TRACE_FILE.write( cla.__str__()+'\n')
TRACE_FILE.write( 'variables'+ cl_ds.base_var_set.__str__()+'\n')
mess = 'free clocks registered:'+ cl_ds.free_clocks.__str__()+'\n'
......@@ -763,7 +763,7 @@ class TestFull(unittest.TestCase):
cl_ds = CLDynSys( tvisit.tab_symb, reporter)
gt2clauses = GT2Clauses(cl_ds, reporter, False)
model.accept(gt2clauses)
for cla in cl_ds.list_clauses:
for cla in cl_ds.clauses:
TRACE_FILE.write( cla.__str__()+'\n')
TRACE_FILE.write( 'variables'+ cl_ds.base_var_set.__str__()+'\n')
mess = 'free clocks registered:'+ cl_ds.free_clocks.__str__()+'\n'
......@@ -787,7 +787,7 @@ class TestFull(unittest.TestCase):
"../../guard_transitions/translators/tests/tgf_cano_noclock_cmp.cal"
)
mcla.build_from_cadlang(filename)
nb_clauses_without_opti = len(mcla.dynamic_system.list_clauses)
nb_clauses_without_opti = len(mcla.dynamic_system.clauses)
TRACE_FILE.write('\n- NB Clauses:' + str(nb_clauses_without_opti))
mcla = MCLAnalyser(rep)
......@@ -796,7 +796,7 @@ class TestFull(unittest.TestCase):
"../../guard_transitions/translators/tests/tgf_cano_noclock_cmp.cal"
)
mcla.build_from_cadlang(filename)
nb_clauses_with_opti = len(mcla.dynamic_system.list_clauses)
nb_clauses_with_opti = len(mcla.dynamic_system.clauses)
TRACE_FILE.write('\n- NB Clauses:' + str(nb_clauses_with_opti))
assert nb_clauses_with_opti < nb_clauses_without_opti
......@@ -818,7 +818,7 @@ class TestMCLSigExprVisitor (unittest.TestCase):
TRACE_FILE.write( '\n\n sigexpr: xx'+'\n')
TRACE_FILE.write( 'RETURN var (xx)'+ var.__str__()+'\n')
TRACE_FILE.write( 'Clauses'+'\n')
for cla in cl_ds.list_clauses:
for cla in cl_ds.clauses:
TRACE_FILE.write( cla.__str__()+'\n')
def test_bin1(self):
......@@ -834,7 +834,7 @@ class TestMCLSigExprVisitor (unittest.TestCase):
TRACE_FILE.write( '\n\n sigexpr: X or Y'+'\n')
TRACE_FILE.write( 'RETURN var (Z)'+ var.__str__()+'\n')
TRACE_FILE.write( 'Clauses'+'\n')
for cla in cl_ds.list_clauses:
for cla in cl_ds.clauses:
TRACE_FILE.write( cla.__str__()+'\n')
def test_bin2(self):
......@@ -851,7 +851,7 @@ class TestMCLSigExprVisitor (unittest.TestCase):
TRACE_FILE.writelines( '\n\n sigexpr: X and Y'+'\n')
TRACE_FILE.write( 'RETURN var (aux var)'+ var.__str__()+'\n')
TRACE_FILE.write( 'Clauses'+'\n')
for cla in cl_ds.list_clauses:
for cla in cl_ds.clauses:
TRACE_FILE.write( cla.__str__()+'\n')
def test_bin3(self):
......@@ -871,7 +871,7 @@ class TestMCLSigExprVisitor (unittest.TestCase):
TRACE_FILE.writelines( '\n\n sigexpr: h1 default h2'+'\n')
TRACE_FILE.write( 'RETURN var (aux var)'+ var.__str__()+'\n')
TRACE_FILE.write( 'Clauses'+'\n')
for cla in cl_ds.list_clauses:
for cla in cl_ds.clauses:
TRACE_FILE.write( cla.__str__()+'\n')
def test_bin4(self):
......@@ -894,7 +894,7 @@ class TestMCLSigExprVisitor (unittest.TestCase):
TRACE_FILE.writelines( '\n\n sigexpr: h1 when (a or b)'+'\n')
TRACE_FILE.write( 'RETURN var (aux var)'+ var.__str__()+'\n')
TRACE_FILE.write( 'Clauses'+'\n')
for cla in cl_ds.list_clauses:
for cla in cl_ds.clauses:
TRACE_FILE.write( cla.__str__()+'\n')
def test_cse1(self):
......@@ -921,9 +921,9 @@ class TestMCLSigExprVisitor (unittest.TestCase):
#sexpv.output_lit = None # for output var generation
var = sexpr.accept(sexpv)
TRACE_FILE.write( '\n\n- RETURN var (aux var)'+ var.__str__()+'\n')
TRACE_FILE.write('\n- NB Clauses:' + str(len(cl_ds.list_clauses)))
TRACE_FILE.write('\n- NB Clauses:' + str(len(cl_ds.clauses)))
TRACE_FILE.write( '\n- Clauses'+'\n')
for cla in cl_ds.list_clauses:
for cla in cl_ds.clauses:
TRACE_FILE.write( cla.__str__()+'\n')
def test_cse2(self):
......@@ -946,9 +946,9 @@ class TestMCLSigExprVisitor (unittest.TestCase):
#sexpv.output_lit = None # for output var generation
var = sexpr.accept(sexpv)
TRACE_FILE.write( '\n\n- RETURN var (aux var)'+ var.__str__()+'\n')
TRACE_FILE.write('\n- NB Clauses:' + str(len(cl_ds.list_clauses)))
TRACE_FILE.write('\n- NB Clauses:' + str(len(cl_ds.clauses)))
TRACE_FILE.write( '\n- Clauses'+'\n')
for cla in cl_ds.list_clauses:
for cla in cl_ds.clauses:
TRACE_FILE.write( cla.__str__()+'\n')
......
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