Commit 3c8421f8 authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[lib] Global Fix typos; more accurate doc

parent 15c615e1
......@@ -207,7 +207,7 @@ class CLUnfolder(object):
# It's the trajectory of events of a solution.
# FP(X): Final property
self.__initial_constraints = [] # DIMACS clauses: C(X_0)
self.__initial_constraints = [] # DIMACS clauses: C(X_0) <list <list <int>>>
self.__final_constraints = [] # idem: C(X_n)
self.__invariant_constraints = [] # DIMACS clauses: C(X_i))
self.__variant_constraints = [] # variant constraints along trajectory
......@@ -222,23 +222,27 @@ class CLUnfolder(object):
def reset(self):
"""Reset the unfolder before a new query
Reset only properties and dimacs clauses from the current query;
AND __list_variant_constraints.
This function is called from the constructor and during
MCLAnalyser.sq_is_satisfiable() and MCLAnalyser.sq_solutions()
following the call of init_with_query().
"""
# Properties to be checked
self.__initial_property = None # logical formula - literal boolean expression
self.__dim_initial = None # list of DIMACS clauses
self.__dimacs_initial = None # list of DIMACS clauses
self.__final_property = None # logical formula
self.__dim_final = None # list of DIMACS clauses
self.__dimacs_final = None # list of DIMACS clauses
self.__invariant_property = None # logical formula
self.__dim_invariant = None # list of DIMACS clauses
self.__dimacs_invariant = None # list of DIMACS clauses
self.__variant_property = None # list<logic formulas>
self.__dim_variant = None # list<list<DIMACS clauses>>
self.__dimacs_variant = None # list<list<DIMACS clauses>>
# list of variant temporal constraints in Dimacs ground code
self.__list_variant_constraints = None # list<list<DIMACS clauses>>
# If called from the constructor, for now these variables are just redefined here
# If this function is called from the constructor,
# the following variables are just redefined here.
# For reachability optimisation. Number of shifts before checking
# the final property
......@@ -252,22 +256,27 @@ class CLUnfolder(object):
Following attributes are used from the query:
start_prop, dim_start, inv_prop, dim_inv, final_prop, dim_final,
variant_prop, dim_variant_prop, steps_before_check
Textual properties of query are compiled into numeric clauses in
init_forward_unfolding(), just before squery_is_satisfied() and
squery_solve().
This compilation step is costly due to ANTLR performances...
"""
# Reset the unfolder before a new query
self.reset()
# Init with query properties and clauses
self.__initial_property = query.start_prop
self.__dim_initial = query.dim_start
self.__initial_property = query.start_prop # logical formula in text
self.__dimacs_initial = query.dim_start
self.__final_property = query.final_prop
self.__dim_final = query.dim_final
self.__final_property = query.final_prop # logical formula in text
self.__dimacs_final = query.dim_final
self.__invariant_property = query.inv_prop
self.__dim_invariant = query.dim_inv
self.__invariant_property = query.inv_prop # logical formula in text
self.__dimacs_invariant = query.dim_inv
# It's the trajectory of events of a solution.
self.__variant_property = query.variant_prop
self.__dim_variant = query.dim_variant_prop
self.__variant_property = query.variant_prop # logical formula in text
self.__dimacs_variant = query.dim_variant_prop
# For reachability optimisation. Number of shifts before checking
# the final property (default 0)
......@@ -596,6 +605,9 @@ class CLUnfolder(object):
(no used anymore, replaced by direct use of C++ code)
Basically, `shift_step` is added to positive variables and subtracted
from negative variables in `numeric_clause`.
self.shift_step must be frozen in order to avoid problems during the
unflatten() step of RawSolutions.
=> Each step MUST have the same number of variables.
......@@ -625,6 +637,9 @@ class CLUnfolder(object):
=> Each step MUST have the same number of variables.
Thus, we lock the Unfolder by turning self.__locked to True.
Called by: __shift_variant()
@param ncl: DIMACS clause
@param nb_steps: number of shifts asked
@warning: lock the unfolder
......@@ -746,7 +761,7 @@ class CLUnfolder(object):
self.__shift_initial()
else:
# Shift direction must be set
raise MCLException("Shift incoherent data: "+self.__shift_direction)
raise MCLException("Shift incoherent data: " + self.__shift_direction)
# Increment the current step
self.__current_step += 1
......
......@@ -351,7 +351,7 @@ class MCLAnalyser(object):
variables), a RawSolution object registers data which permit information
extraction from these raw solutions. The most important methods are:
- extract_frontier_values():
- frontier_pos_and_neg_values:
Which extracts the frontier values from the solution.
These values are in DIMACS code.
......
......@@ -196,15 +196,15 @@ class MCLSimpleQuery(object):
if not var_prop:
var_prop = None
# inactivation of other frontier places at start (DIMACS format)
# Inactivation of other frontier places at start (DIMACS format)
# Search all frontiers that are not in activated_frontier
# and force their inactivation with a negative value.
## dim_start doit-il etre ordonné ?
# Get negative values of activated frontiers in FrontierSolution object
# 1 - Get negative values of activated frontiers in FrontierSolution object
activated_frontier_neg_values = \
{-unfolder.var_dimacs_code(name) for name in f_sol.activated_frontier}
# Get list of values of inactivated frontiers in the FrontSolution object
# 2 - Get values of inactivated frontiers in the FrontSolution object
dim_start_values = \
[[val] for val in unfolder.frontiers_negative_values - activated_frontier_neg_values]
......@@ -328,13 +328,13 @@ class MCLSimpleQuery(object):
else:
var_prop = []
# 2 empty, 1 empty and not the other, none empty
for a, b in zip(self.variant_prop, query.variant_prop):
if a and b:
var_prop.append(a + " and " + b)
elif a and not b:
var_prop.append(a)
elif not a and b:
var_prop.append(b)
for current, other in zip(self.variant_prop, query.variant_prop):
if current and other:
var_prop.append(current + " and " + other)
elif current and not other:
var_prop.append(current)
elif not current and other:
var_prop.append(other)
else:
var_prop.append("")
......
......@@ -393,11 +393,12 @@ class TestMCLAnaLyzer(unittest.TestCase):
query = MCLSimpleQuery(st_prop, inv_prop, f_prop)
lsol = mcla.sq_solutions(query, 4, 1, mcla.unfolder.frontier_values)
sol = lsol[0]
res = len(lsol) == 2
assert len(lsol) == 2
ic_seq = sol.extract_act_input_clock_seq()
#print ic_seq
expected_sol = [[2], [], []]
res = res and lit_sol_equal(expected_sol, ic_seq)
res = lit_sol_equal(expected_sol, ic_seq)
print("expected ic_seq:", expected_sol)
print("found ic_seq:", ic_seq)
self.assert_(res, 'Error clock/input sequence for C3 and not C4')
f_prop = "C4 and C3"
......@@ -459,7 +460,7 @@ class TestMCLAnaLyzer(unittest.TestCase):
[
# Get all activated frontiers in the DimacsFrontierSol
[-var for var in dimacs_front_sol.activated_frontier_values]
for dimacs_front_sol in lsol
for dimacs_front_sol in lsol
]
# print(lforbidden)
## TODO: assert lforbidden
......@@ -857,8 +858,9 @@ class TestMCLAnaLyzer(unittest.TestCase):
assert found == None
found = query_1.variant_prop
assert found == ['not (h2)', 'not (h2)', '', '']
# Inactivation of of other frontier places (not used in the solution)
found = query_1.dim_start
assert found == [[-2]]
assert found == [[-2]] # D
print("is strong inhibitor ?", res)
# it is a strong inhibitor
......
......@@ -779,11 +779,11 @@ class TestFull(unittest.TestCase):
mcla = MCLAnalyser(rep)
mcla.opti = False
mcla.build_from_chart_file("../ucl/examples/test_tgfb_ref_300511.bcx")
mess = '\n- NB Clauses:' + str(len(mcla.cl_dyn_sys.list_clauses))
mess = '\n- NB Clauses:' + str(len(mcla.dynamical_system.list_clauses))
TRACE_FILE.write(mess)
mcla = MCLAnalyser(rep)
mcla.build_from_chart_file("../ucl/examples/test_tgfb_ref_300511.bcx")
mess = '\n- NB Clauses:' + str(len(mcla.cl_dyn_sys.list_clauses))
mess = '\n- NB Clauses:' + str(len(mcla.dynamical_system.list_clauses))
TRACE_FILE.write(mess)
class TestMCLSigExprVisitor (unittest.TestCase):
......
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