Maj terminée. Pour consulter la release notes associée voici le lien :
https://about.gitlab.com/releases/2021/07/07/critical-security-release-gitlab-14-0-4-released/

Commit 35bdef62 authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[lib] Fix collisions between literals in start/inv properties and no frontiers initialization

parent 83486da0
......@@ -300,14 +300,25 @@ class CLUnfolder(object):
self.__aux_code_table = dict() # name to code
self.__aux_list = [] # code to name
# ordered list of DIMACS codes of the simple variables/places
# Disable all variables of places (entities) in the model (except frontiers)
self.__no_frontier_init = [
[-self.__var_code_table[not_front_name]]
# No frontier init:
# Set of DIMACS codes of the simple variables/places that are not frontiers
# Used to disable all variables of places in the model (except frontiers)
self.no_frontier_values = frozenset(
self.__var_code_table[not_front_name]
for not_front_name in self.dynamic_system.no_frontiers
]
# ordered list of DIMACS codes of the frontier variables/places
)
# Used in __prune_initial_no_frontier_constraint_0() in order to
# compute values of literals that are specified in user constraints.
# These literals should not be blindly disabled by default in __no_frontier_init
self.initial_values = set()
# Ordered list of DIMACS codes of the places that are not frontiers
# => Clauses of negatives values
# Ex: [[-1], [-2], ...]
# The values are usually a subset of no_frontier_values
self.__no_frontier_init = list()
# Frontiers:
# Ordered list of DIMACS codes of the frontier variables/places
self.frontier_values = [
self.__var_code_table[front_name]
for front_name in self.dynamic_system.frontiers
......@@ -409,6 +420,12 @@ class CLUnfolder(object):
# list of variant temporal constraints in DIMACS ground code
self.__precomputed_variant_constraints = None # list<list<DIMACS clauses>>
# Note: temp_initial_values is used in:
# __init_initial_constraint_0()
# __init_invariant_constraint_0()
# See __prune_initial_no_frontier_constraint_0()
self.temp_initial_values = set()
# If this function is called from the constructor,
# the following variables are just redefined here.
......@@ -1207,40 +1224,59 @@ class CLUnfolder(object):
"error during parsing of '%s', please check the event syntax"
% property_text
)
## DEBUG clauses encoding print("treeprop, ste, fcl", tree_prop, ste, fcl)
## DEBUG clauses encoding print("lit cpt before", self.__lit_cpt)
# Avoid name collisions of aux var
prop_visitor = PropertyVisitor(self.__lit_cpt)
tree_prop.accept(prop_visitor)
self.__lit_cpt = prop_visitor.cpt # avoid name collisions of aux var
## DEBUG clauses encoding print("event visitor clauses", prop_visitor.clauses)
## DEBUG clauses encoding print("lit cpt after", self.__lit_cpt)
# raise Exception("event")
return prop_visitor.clauses
def __init_initial_constraint_0(self, no_frontier_init=True):
"""Code initial constraints in a numerical clause.
Initialisation of `__initial_constraints`:
List of DIMACS clauses (lists of values).
Automatic merge of textual and DIMACS forms:
If initial property is set (in text format of logical formulas, or
in dimacs format of numerical values), this function generates
constraints clauses in numerical form.
Initialisation of self.__initial_constraints:
List of DIMACS clauses (lists of values).
We have to wait until all variables are num coded before shifting anything!
.. note:: Compilation of properties in text format (logical formulas)
to numeric format is expensive when they must be parsed at each query.
:key no_frontier_init: (Optional) Boolean to force all variables of
places/entities that are not frontiers to be disabled before each
search with a clause with their negative values.
default: True
places/entities that are not frontiers to be disabled at the
initialization step. Default: True
.. warning:: We avoid inactivation/activation collisions if such
places are explicitly mentioned in textual properties (only).
See :meth:`__prune_initial_no_frontier_constraint_0`.
DIMACS properties are not checked.
:type no_frontier_init: <boolean>
"""
self.__initial_constraints = list()
if no_frontier_init:
# Disable all variables of places (entities) in the model (except frontiers)
self.__initial_constraints += self.__no_frontier_init
## TODO: optimize this...
## The list of literals due to __initial_property (and by extension
## __no_frontier_init) may be invariable and is reprocessed here at
## each reload of the unfolder.
## The literals in banished solutions represent a variable part of
## __initial_constraints and become more and more numerous at each run.
## __initial_constraints is huge and will be, shifted at every step for
## backward search (not used), or simply reloaded at each step as this
## for forward search.
## Caching __initial_constraints could be possible if an extra set of
## constraints is dedicated to banished solutions...
if self.__initial_property:
# Compile initial property from text logical formulas to numeric form
......@@ -1250,6 +1286,12 @@ class CLUnfolder(object):
[self.__code_clause(clause) for clause
in self.__compile_property(self.__initial_property)]
if no_frontier_init:
# TODO: useless if __initial_property has not changed...
self.temp_initial_values.update(
abs(val) for val in it.chain(*self.__initial_constraints)
)
if self.__dimacs_initial:
# Add DIMACS clauses
self.__initial_constraints += self.__dimacs_initial
......@@ -1283,7 +1325,7 @@ class CLUnfolder(object):
# Add DIMACS clauses
self.__final_constraints += self.__dimacs_final
def __init_invariant_constraint_0(self):
def __init_invariant_constraint_0(self, no_frontier_init=True):
"""Code final constraints in a numerical clause.
Automatic merge of textual and DIMACS forms:
......@@ -1312,6 +1354,19 @@ class CLUnfolder(object):
.. note:: Compilation of properties in text format (logical formulas)
to numeric format is expensive when they must be parsed at each query.
:key no_frontier_init: (Optional) Boolean to force all variables of
places/entities that are not frontiers to be disabled at the
initialization step. Default: True
.. warning:: We avoid inactivation/activation collisions if such
places are explicitly mentioned in textual properties (only).
See :meth:`__prune_initial_no_frontier_constraint_0`.
DIMACS properties are not checked.
:type no_frontier_init: <boolean>
"""
self.__invariant_constraints = list()
......@@ -1322,6 +1377,12 @@ class CLUnfolder(object):
in self.__compile_property(self.__invariant_property)]
)
if no_frontier_init:
# TODO: useless if __invariant_property has not changed...
self.temp_initial_values.update(
abs(val) for val in it.chain(*self.__invariant_constraints[0])
)
if self.__dimacs_invariant:
# Add DIMACS clauses
if self.__invariant_constraints:
......@@ -1403,7 +1464,101 @@ class CLUnfolder(object):
elif self.__shift_direction == "BACKWARD":
raise MCLException("Shift direction 'BACKWARD' is not yet implemented")
else:
raise MCLException("Shift incoherent data: " + self.__shift_direction)
raise MCLException("Shift unsupported direction: " + self.__shift_direction)
def __prune_initial_no_frontier_constraint_0(self, no_frontier_init=True):
"""Prevent the places mentioned in constraints to be inactivated
at the initial state of the system.
Why? This will return an unsatisfiable system whatever the constraints.
How? Get all values in the recently compiled initial and invariant
contraints. Then, built __no_frontier_init with allowed places and
append it to initial_constraints.
Positive side-effect: __no_frontier_init is cached as much as possible
from a run to another.
`__initial_constraints` is a list of DIMACS clauses (lists of values)
composed of 4 types of clauses:
1 - non frontier literals (computed here)
2 - literals from text properties (initial/invariant)
3 - literals from DIMACS properties (initial/invariant)
4 - clauses from banished solutions
(see :meth:`__init_initial_constraint_0`)
If the textual properties do not change from one run to another,
then only the clauses related to the banishment of the solutions
change.
:Example:
Places that are not frontiers are inactivated; initial_constraints
will be:
[[-1],]
Then you want to force the literal 1 to be activated under certain
conditions in start_property or invariant_property of a query.
You don't want to have the following initial_constraints because the
system is still unsatisfiable whatever the constraints:
[[-1], [1],]
.. note:: About reproductible runs and constraints order:
The order of clauses impacts the final result;
In order to keep the results obtained with the old library;
the literals of non boundaries must be placed at the beginning
of __initial_constraints (not at the beginning).
"""
if not no_frontier_init:
return
# Note: temp_initial_values comes from:
# __init_initial_constraint_0
# __init_invariant_constraint_0
if self.temp_initial_values == self.initial_values and self.__no_frontier_init:
# __no_frontier_init is already initialiazed according to the
# same initial/invariant textual properties
LOGGER.info("RELOAD __no_frontier_init")
# pas de += => pas reproductible avec les anciens runs
self.__initial_constraints = self.__no_frontier_init + self.__initial_constraints
return
if self.temp_initial_values:
# Different initial_values since the last run
# Prune no_frontier_values (remove values in user constraints from them)
LOGGER.info("INIT prune __no_frontier_init")
pruned_no_frontier_values = self.no_frontier_values - self.temp_initial_values
self.__no_frontier_init = [[-val] for val in pruned_no_frontier_values]
else:
# Take all no_frontier_values
LOGGER.info("INIT basic __no_frontier_init")
# Not reproductible with previous runs
# self.__no_frontier_init = [
# [-not_front_val]
# for not_front_val in sorted(self.no_frontier_values)
# ]
# Reproductible
self.__no_frontier_init = [
[-self.__var_code_table[not_front_name]]
for not_front_name in self.dynamic_system.no_frontiers
]
# Keep temp_initial_values for the next run
# LOGGER.debug(
# "previous initial values: %s; vs new initial values: %s",
# self.initial_values, self.temp_initial_values
# )
self.initial_values = self.temp_initial_values
# Disable all variables of places (entities) in the model (except frontiers)
# pas de += => pas reproductible avec les anciens runs
self.__initial_constraints = self.__no_frontier_init + self.__initial_constraints
## Whole initialisations ###################################################
def init_forward_unfolding(self):
......@@ -1471,6 +1626,8 @@ class CLUnfolder(object):
self.__init_final_constraint_0()
self.__init_invariant_constraint_0()
self.__init_variant_constraints_0()
# Should be after init_initial and init_invariant
self.__prune_initial_no_frontier_constraint_0()
# Now shifting is possible
## TODO: check shift_direction too (not urgent, backward is not usable)
......@@ -1497,7 +1654,6 @@ class CLUnfolder(object):
self.__shift_final()
self.__shift_invariant()
def init_backward_unfolding(self):
"""Initialisation before generating constraints - backward trajectory
Never used (and backward not implemented in __init_variant_constraints_0)
......@@ -1513,6 +1669,8 @@ class CLUnfolder(object):
self.__init_final_constraint_0()
self.__init_invariant_constraint_0()
self.__init_variant_constraints_0()
# Should be after init_initial and init_invariant
self.__prune_initial_no_frontier_constraint_0()
# Now shifting is possible
self.__backward_init_dynamic()
......
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