From 52075e7cdcb628a8303791f5ab348d31fb762ff2 Mon Sep 17 00:00:00 2001 From: VIGNET Pierre <pierre.vignet@irisa.fr> Date: Mon, 25 Nov 2019 02:48:57 +0100 Subject: [PATCH] [lib] CLUnfolder: update class doc --- .../clause_constraints/mcl/CLUnfolder.py | 21 +++++++++++++------ 1 file changed, 15 insertions(+), 6 deletions(-) diff --git a/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py b/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py index 80bd525..59d3d10 100644 --- a/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py +++ b/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py @@ -115,12 +115,10 @@ init_forward_unfolding(): PS: __variant_constraints si already initialized for the first step - The following functions use the following methods to decompile textual - properties or events (__compile_property(), __compile_event()) and to - code them into DIMACS clauses constraints (__code_clause()). - - __code_clause() is susceptible to add new auxiliary numeric variables - during this process if a variable is not found in __var_code_table or in + The following functions decompile textual properties or events and code them + into DIMACS clauses constraints via __code_clause(). + __code_clause() is susceptible to add new auxiliary numerical variables + during this process if a variable is not found in __var_code_table and in __aux_code_table. - __init_initial_constraint_0, __init_final_constraint_0, __init_invariant_constraint_0 @@ -199,6 +197,17 @@ class CLUnfolder(object): - state vector: list of DIMACS code of original (not shifted) variables corresponding to a step. - trajectory: list of state_vectors + + + Some attributes (Please read the constructor comments for much more information): + + __*_property: Logical formulas in text format from the current query. + __dimacs_*: Clauses in DIMACS format from the current query. + __*_constraints: CLUnfolder attributes for unfolding and shift initialised + from the query attributes. + + :param dynamical_system: dynamical system in clause constraint form + :type dynamical_system: <CLDynSys> """ def __init__(self, dynamic_system, debug=False): -- GitLab