Commit d76de0f6 authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[lib] CLU: check_query: Some fix and doc

parent 734559d0
......@@ -415,7 +415,17 @@ class CLUnfolder(object):
Also check if values of literals are in the limits of the dynamical
system (shift_step_init). If it's not the case, a ValueError exception
will be raised.
will be raised. Indeed, literals **can't** be used without a proper init.
.. TODO:: Keep in mind that adding auxiliary variables is possible in
the future.
Il faut remplir __aux_code_table, __aux_list, jusqu'à la valeur
du litéral inconnu dans le système et incrémenter les
variables en conséquence.
S'inspirer de __code_clause()
.. TODO:: We do not test if the textual events of query.variant_prop
involves events that are not in the model...
Called by:
......@@ -429,17 +439,24 @@ class CLUnfolder(object):
or self.__final_property != query.final_prop
or self.__invariant_property != query.inv_prop
or self.__variant_property != query.variant_prop):
# System will be modified; Auxiliary clauses will be added
# Do not reload cached constraints
# Properties have changed:
# The system will be modified; Auxiliary clauses will be added.
# Do not reload cached constraints. Cf init_forward_unfolding()
self.__include_aux_clauses_changed = True
# Check literals
if query.dim_inv:
# Check dimacs invariant: Initial state only (will be shifted later)
# Ex: [[12]]
assert len(query.dim_inv) == 1
# Check values of literals
values = set(it.chain(*query.dim_start))
if query.dim_variant:
# Handle empty steps:
# Ex: [[[12], [1]], [[58], [47]], [[104], [93]]
# Ex: [[[12], [1]], [[58], [47]], []]
g = (step for step in query.dim_variant if step)
[values.update(it.chain(*step)) for step in g]
......@@ -449,11 +466,12 @@ class CLUnfolder(object):
# The literal comes from an auxilary clause; not from the dynamic model.
# Since the auxiliary clauses are reset here, this literal is suspect
# and its use dangerous because its value is not reproductible.
raise ValueError(
"%s variable(s) is/are not in the initial system.\n"
"Insertion of auxiliary variables is not allowed here."
"Insertion of literals from auxiliary clauses is not allowed here.\n"
"Since the auxiliary clauses are reset here, this literal is suspect\n"
"and its use dangerous because its value is not reproductible\n"
"(the value can refer to a different constraint from one run to another)."
% out_of_range_values
Supports Markdown
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