diff --git a/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py b/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
index caebfb766d4b763cef6e78aef14214a49aedf371..3a789a28cee34af82d071d1cdd9a9edba70d7452 100644
--- a/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
+++ b/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
@@ -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
diff --git a/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py b/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py
index 7345623a9b20fa53c68709efb7cc2a97ef081842..c5e6ab869b23bd6fc80d508abb2eb42a73e4f7fb 100644
--- a/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py
+++ b/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py
@@ -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.
diff --git a/library/cadbiom/models/clause_constraints/mcl/MCLQuery.py b/library/cadbiom/models/clause_constraints/mcl/MCLQuery.py
index 0c8b71580c56f928d933e35b9629e239372a2b39..86daf95bf4bd2e91d1ab20127493a270eb4a32ea 100644
--- a/library/cadbiom/models/clause_constraints/mcl/MCLQuery.py
+++ b/library/cadbiom/models/clause_constraints/mcl/MCLQuery.py
@@ -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("")
diff --git a/library/cadbiom/models/clause_constraints/mcl/TestMCLAnalyser.py b/library/cadbiom/models/clause_constraints/mcl/TestMCLAnalyser.py
index e98e2d5b16938641809494556432f9c19cce676c..1a5ba92696016b86fadd95503b6fefdc2aa27d4b 100644
--- a/library/cadbiom/models/clause_constraints/mcl/TestMCLAnalyser.py
+++ b/library/cadbiom/models/clause_constraints/mcl/TestMCLAnalyser.py
@@ -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
diff --git a/library/cadbiom/models/clause_constraints/mcl/TestMCLTranslators.py b/library/cadbiom/models/clause_constraints/mcl/TestMCLTranslators.py
index c5e371b64b9321f58acf33325539c74fddc2fbfc..5d7ce40f239572c32a49b4c66cff7cb6ab7d781d 100644
--- a/library/cadbiom/models/clause_constraints/mcl/TestMCLTranslators.py
+++ b/library/cadbiom/models/clause_constraints/mcl/TestMCLTranslators.py
@@ -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):