From 40e42366e9b8cfe47b815a6b5f5028da6726ca93 Mon Sep 17 00:00:00 2001
From: VIGNET Pierre <pierre.vignet@irisa.fr>
Date: Fri, 22 Nov 2019 00:28:06 +0100
Subject: [PATCH] [lib] MCLQuery, MCLMCLAnalyser, CLUnfolder: Add doc, module
doc, fix typos
---
.../clause_constraints/mcl/CLUnfolder.py | 172 +++++++++++++++---
.../clause_constraints/mcl/MCLAnalyser.py | 7 +
.../models/clause_constraints/mcl/MCLQuery.py | 12 ++
3 files changed, 170 insertions(+), 21 deletions(-)
diff --git a/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py b/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
index 09dcee7..00f66a3 100644
--- a/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
+++ b/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
@@ -39,8 +39,78 @@
##
## Contributor(s): Geoffroy Andrieux IRSET
##
-"""
-Main engine for constraint unfolding and solving
+"""Main engine for constraints unfolding and solving.
+
+Process from the intialization with a query to the finding of a solution.
+
+
+MCLSimpleQuery (reminder):
+ Object containing 2 main types of attributes describing properties:
+
+ - Attributes in text format: These are logical formulas that are humanly
+ readable.
+ Ex: start_prop, inv_prop, final_prop, variant_prop
+ - Attributes in DIMACS format: These are logical formulas encoded in
+ the form of clauses containing numerical values.
+ Ex: dim_start, dim_inv, dim_final, dim_variant_prop
+
+init_with_query(query):
+ Copy of the query attributes to temporary attributes internal to the CLUnfolder.
+
+ Textual properties of query are compiled into numeric clauses in
+ init_forward_unfolding(), just at the beginning of squery_is_satisfied()
+ and squery_solve().
+
+ ALL textual properties are susceptible to add new auxiliary variables in the
+ system.
+
+
+init_forward_unfolding():
+ Organization of the initialization of the system (its clauses) for
+ the current request and first variables shift.
+
+ Initialized attributes:
+ - __initial_constraints:
+ Query data + negative values of all places that are not frontiers.
+ - __final_constraints:
+ Query data
+ - __invariant_constraints:
+ List of Query data
+ - __list_variant_constraints:
+ Query data (automatic merge of textual and DIMACS forms)
+ - __variant_constraints:
+ Initilized with the first item of __list_variant_constraints
+
+ Shifted attributes with __shift_step (nb of variables in the system):
+ - __forward_init_dynamic(): __dynamic_constraints:
+ Shift dynamic_system.list_clauses + dynamic_system.aux_list_clauses + init
+ - __shift_final(): __final_constraints:
+ Shift + replace __final_constraints
+ - __shift_invariant(): _invariant_constraints:
+ Shift + append of the last element of __invariant_constraints
+
+ PS: __variant_constraints si already initialized for the first step
+
+
+shift():
+ Shift all clauses of the system to prepare it for the next step.
+
+ Called at each step by:
+ - squery_solve()
+ - squery_is_satisfied()
+
+ Modified attributes:
+ - __shift_dynamic(): __dynamic_constraints:
+ Shift + append of the last element of __dynamic_constraints
+ - __shift_variant(): __variant_constraints:
+ Shift clauses of the current step in __list_variant_constraints, and
+ append them to __variant_constraints.
+ - __shift_invariant()
+ ...
+ - __shift_final()
+ ...
+
+
"""
from __future__ import print_function
@@ -268,9 +338,12 @@ class CLUnfolder(object):
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().
+ init_forward_unfolding(), just at the beginning of squery_is_satisfied()
+ and squery_solve().
This compilation step is costly due to ANTLR performances...
+
+ .. warning:: ALL textual properties are susceptible to add new auxiliary
+ variables in the system (increase shift_step).
"""
# Reset the unfolder before a new query
self.reset()
@@ -687,6 +760,8 @@ class CLUnfolder(object):
def __shift_initial(self):
"""Shift initialisation condition
+ Shift + replace __initial_constraints
+
.. note:: Called by:
- shift()
- init_backward_unfolding()
@@ -700,6 +775,8 @@ class CLUnfolder(object):
def __shift_final(self):
"""Shift final property
+ Shift + replace __final_constraints
+
.. note:: Called by:
- shift()
- init_forward_unfolding()
@@ -713,6 +790,8 @@ class CLUnfolder(object):
def __shift_invariant(self):
"""Shift invariant property
+ Shift + append of the last element of __invariant_constraints
+
.. note:: Called by:
- shift()
- init_forward_unfolding()
@@ -730,7 +809,8 @@ class CLUnfolder(object):
def __shift_variant(self):
"""Shift variant property - depends on unfolding direction
- ## TODO audit...
+ Shift clauses of the current step in __list_variant_constraints, and
+ append them to __variant_constraints.
.. warning:: Refactor note: unclear function. No apparent reason for
only the first clause to be shifted...
@@ -753,7 +833,7 @@ class CLUnfolder(object):
if self.__shift_direction == "FORWARD":
# 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
+ # Shift constraints at current step and append them to __variant_constraints
for clause in current_constraint:
s_clause = self.__m_shift_clause(clause, self.__current_step)
self.__variant_constraints.append(s_clause)
@@ -765,16 +845,24 @@ class CLUnfolder(object):
def shift(self):
- """Shift all clauses of one step
+ """Shift all clauses of the system to prepare it for the next step.
self.__current_step is incremented here!
- Clauses shifted:
+ Modified attributes:
- __dynamic_constraints[-1] (last element)
+ Shift + append of the last element of __dynamic_constraints
- __invariant_constraints[-1] (last element)
- - __list_variant_constraints => TODO: audit...
+ Shift + append of the last element of __invariant_constraints
+ - __list_variant_constraints[current_step]
+ Shift clauses of the current step in __list_variant_constraints,
+ and append them to __variant_constraints.
- __final_constraints if __shift_direction is "FORWARD"
- __initial_constraints if __shift_direction is "BACKWARD"
+
+ Called at each step by:
+ - squery_solve()
+ - squery_is_satisfied()
"""
# Froze unfolder to avoid modifications of shift_step
self.__locked = True
@@ -864,13 +952,17 @@ class CLUnfolder(object):
Initialisation of self.__initial_constraints:
List of DIMACS clauses (lists of values).
+ self.__initial_constraints is filled with the current query data AND
+ with a clause with ALL places that are not frontiers (negative 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 to be disabled before each search.
+ places/entities that are not frontiers to be disabled before each
+ search.
default: True
:type no_frontier_init: <boolean>
"""
@@ -952,15 +1044,23 @@ class CLUnfolder(object):
def __init_variant_constraints_0(self):
"""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
+ .. TODO:: variant_property list d'étapes, chaque étape a une formule logique
+ impliquant les évènements (et des places? pas sur...)
+ => ensemble de place/propriétés devant etre valides à chaque étape
+
+ Automatic merge of textual and DIMACS forms:
+ 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) in
+ order to allow a merge.
- 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:
+ Built here and is used later to shift current variant properties
+ and update self.__variant_constraints in __shift_variant().
- self.__list_variant_constraints is built here and is used later to shift
- given variant properties in __shift_variant().
+ self.__variant_constraints:
+ - the only element passed to the solver.
+ - initilised with the first item of self.__list_variant_constraints
"""
# coding of variant properties
# Take __variant_property in priority on __dimacs_variant
@@ -1016,6 +1116,36 @@ class CLUnfolder(object):
def init_forward_unfolding(self):
"""Initialisation before generating constraints - forward trajectory
+ Organization of the initialization of the system (its clauses) for
+ the current request and first variables shift.
+
+ .. warning:: ALL textual properties are susceptible to add new auxiliary
+ variables in the system (increase shift_step).
+ This is why the shift is made after initialization.
+
+ Initialized attributes:
+ - __initial_constraints:
+ Query data + negative values of all places that are not frontiers.
+ - __final_constraints:
+ Query data
+ - __invariant_constraints:
+ List of Query data
+ - __list_variant_constraints:
+ Query data (automatic merge of textual and DIMACS forms)
+ - __variant_constraints:
+ Initilized with the first item of __list_variant_constraints
+
+ Shifted attributes with __shift_step (nb of variables in the system):
+ - __dynamic_constraints:
+ Shift dynamic_system.list_clauses + dynamic_system.aux_list_clauses + init
+ - __final_constraints:
+ Shift + replace __final_constraints
+ - __invariant_constraints:
+ Shift + append of the last element of __invariant_constraints
+
+ PS: __variant_constraints si already initialized for the first step.
+
+
Called at the begining of squery_is_satisfied() and squery_solve()
"""
self.__shift_direction = 'FORWARD'
@@ -1024,13 +1154,13 @@ class CLUnfolder(object):
self.__aux_code_table = dict() # flush auxiliary variables
self.__aux_list = [] # idem
- # init properties to generate all variable num codes
+ # Init properties to generate all variable num codes
self.__init_initial_constraint_0()
self.__init_final_constraint_0()
self.__init_invariant_constraint_0()
self.__init_variant_constraints_0()
- # now shifting is possible
+ # Now shifting is possible
self.__forward_init_dynamic()
self.__shift_final()
self.__shift_invariant()
@@ -1046,13 +1176,13 @@ class CLUnfolder(object):
self.__aux_code_table = dict() # flush auxiliary variables
self.__aux_list = [] # idem
- # init properties to generate all variable num codes
+ # Init properties to generate all variable num codes
self.__init_initial_constraint_0()
self.__init_final_constraint_0()
self.__init_invariant_constraint_0()
self.__init_variant_constraints_0()
- # now shifting is possible
+ # Now shifting is possible
self.__backward_init_dynamic()
self.__shift_initial()
self.__shift_invariant()
diff --git a/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py b/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py
index 7b2ced1..eb8e35d 100644
--- a/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py
+++ b/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py
@@ -42,6 +42,13 @@
"""
Main class to perform dynamic analysis of Cadbiom chart models.
+Discrete event system simulation is a standard simulation scheme which consists
+in the repetition of the following actions until some halting condition
+is satisfied:
+- Find the current events and inputs (including free events)
+- Find the state variables subject to change
+- Perform the state evolution
+
## Here you will find a global view of the process of dynamic analysis
mac_search:
diff --git a/library/cadbiom/models/clause_constraints/mcl/MCLQuery.py b/library/cadbiom/models/clause_constraints/mcl/MCLQuery.py
index c8e4b09..94b0c8b 100644
--- a/library/cadbiom/models/clause_constraints/mcl/MCLQuery.py
+++ b/library/cadbiom/models/clause_constraints/mcl/MCLQuery.py
@@ -52,6 +52,18 @@ LOGGER = cm.logger()
class MCLSimpleQuery(object):
"""Class packaging the elements of a query
+ Object containing 2 main types of attributes describing properties:
+
+ - Attributes in text format: These are logical formulas that are humanly
+ readable.
+ Ex: start_prop, inv_prop, final_prop, variant_prop
+ - Attributes in DIMACS format: These are logical formulas encoded in
+ the form of clauses containing numerical values.
+ Ex: dim_start, dim_inv, dim_final, dim_variant_prop
+
+ Textual properties of query are compiled into numeric clauses in the unfolder
+ with init_forward_unfolding(), just at the beginning of squery_is_satisfied()
+ and squery_solve().
Attributes:
--
GitLab