From 8f1041d41a0de75a5caf9388c37db65c19e17e2f Mon Sep 17 00:00:00 2001
From: VIGNET Pierre <pierre.vignet@irisa.fr>
Date: Wed, 20 Nov 2019 03:36:56 +0100
Subject: [PATCH] [lib] CLUnfolder: \! Refactor and audit __shift_variant and
__init_variant_constraints_0 => These functions are problematic and NOT
TESTED
---
.../clause_constraints/mcl/CLUnfolder.py | 110 ++++++++++++------
1 file changed, 74 insertions(+), 36 deletions(-)
diff --git a/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py b/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
index 0bbacec..fa9ac2e 100644
--- a/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
+++ b/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
@@ -728,23 +728,40 @@ class CLUnfolder(object):
)
def __shift_variant(self):
- """
- shift variant property - depends on unfolding direction
+ """Shift variant property - depends on unfolding direction
+
+ ## TODO audit...
+
+ .. warning:: Refactor note: unclear function. No apparent reason for
+ only the first clause to be shifted...
+
+ Process:
+ - Take the clauses (constraint) of the current step
+ - Shift the first clause
+ - Append it to __variant_constraints
+ - Stop ????
+
+ Example:
+ current_step: 2 (shift for step 3)
+ [[], [[4], [4]], [[6], [7]], []]
+ => Only [6] is shifted...
+
+ .. note:: Called by shift()
"""
if not self.__list_variant_constraints:
return
if self.__shift_direction == "FORWARD":
- index = self.__current_step # constraint t0 already included
- current_constraint = self.__list_variant_constraints[index]
+ # Constraint t0 already included from the query during initialisation
+ current_constraint = self.__list_variant_constraints[self.__current_step]
# shift constraint at current step and add to var_constraints
for clause in current_constraint:
- s_clause = self.__m_shift_clause(clause, index)
+ s_clause = self.__m_shift_clause(clause, self.__current_step)
self.__variant_constraints.append(s_clause)
- return
- elif self.__shift_direction == 'BACKWARD':
+ return # ?????
+ elif self.__shift_direction == "BACKWARD":
raise MCLException("Not yet implemented")
else:
- raise MCLException("Shift incoherent data: "+self.__shift_direction)
+ raise MCLException("Shift incoherent data: " + self.__shift_direction)
def shift(self):
@@ -909,46 +926,67 @@ class CLUnfolder(object):
self.__invariant_constraints = self.__invariant_constraints + d_inv
def __init_variant_constraints_0(self):
- """
- if variant_property is set, compile each property into clauses and
+ """Code variant constraints in a numerical clause.
+
+ variant_property list d'étapes, chaque étape a une formule logique impliquant les évènements (et les places? pas sur.;)
+ => ensemble de place/propriétés devant ^etre valides à chaque étape
+
+ If variant_property is set, compile each property into clauses and
encode these clauses. Clauses already in dimacs form are added.
The two variant constraint forms must be compatible (same length)
+
+ self.__list_variant_constraints is built here and is used later to shift
+ given variant properties in __shift_variant().
"""
# coding of variant properties
+ # Take __variant_property in priority on __dimacs_variant
if self.__variant_property:
- self.__list_variant_constraints = []
+ self.__list_variant_constraints = list()
+
for prop in self.__variant_property:
- # compile initial (X0) property
- l_clauses = self.__compile_event(prop)
- # encode the clauses
- dim_cl = []
- for clause in l_clauses:
- dim_cl.append(self.__code_clause(clause))
- self.__list_variant_constraints.append(dim_cl)
-
- # add variant properties in dimacs form
- if self.__dim_variant:
- vp_length = len(self.__variant_property)
- if vp_length != len(self.__dim_variant):
- mess = "Incoherent variant properties"
- raise MCLException(mess)
-
- for i in range(vp_length):
- c_var = self.__list_variant_constraints[i]
- c_var = c_var + self.__dim_variant[i]
- self.__list_variant_constraints[i] = c_var
- else:
- if self.__dim_variant:
- self.__list_variant_constraints = self.__dim_variant
- # initialisation
+ # compile initial (X0) property into numeric form
+ # For each property in step of __variant_property
+ self.__list_variant_constraints.append(
+ [self.__code_clause(clause)
+ for clause in self.__compile_event(prop)]
+ )
+ print(self.__list_variant_constraints)
+
+ if self.__dimacs_variant:
+ # Add DIMACS aux clauses initial properties
+ # Check if the number of steps is equal
+ if len(self.__variant_property) != len(self.__dimacs_variant):
+ raise MCLException(
+ "Incoherent variant properties; sizes of "
+ "__variant_property and __dimacs_variant differ"
+ )
+
+ # Merge together all steps content
+ # Ex:
+ # __list_variant_constraints due to __variant_property convertion:
+ # [[], [[4]], [], []]
+ # __dimacs_variant:
+ # [[], [[4]], [[6], [7]], []]
+ # Result:
+ # [[], [[4], [4]], [[6], [7]], []]
+ self.__list_variant_constraints = \
+ [list(it.chain(*cpl)) for cpl
+ in zip(self.__dimacs_variant, self.__list_variant_constraints)]
+
+ elif self.__dimacs_variant:
+ # No __variant_property, keep only __dimacs_variant
+ self.__list_variant_constraints = self.__dimacs_variant
+
+ # Initialisation
if self.__list_variant_constraints:
if self.__shift_direction == "FORWARD":
+ # For now, keep only the events of the first step (t0)
+ # Other steps are taken during shift() calls
self.__variant_constraints = self.__list_variant_constraints[0]
elif self.__shift_direction == "BACKWARD":
raise MCLException("Not yet implemented")
else:
- raise MCLException("Shift incoherent data: "
- + self.__shift_direction)
+ raise MCLException("Shift incoherent data: " + self.__shift_direction)
## Whole initialisations ###################################################
def init_forward_unfolding(self):
--
GitLab