Commit 90aa4741 authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[doc] Fix main sphinx warnings...

parent a77fad40
......@@ -352,7 +352,7 @@ def queries_2_common_graph(output_dir, model_file, path,
Create a GraphML formated file containing a unique representation of **all**
trajectories corresponding to all solutions in each complete MAC files
(*mac_complete files).
(\*mac_complete files).
This is a function to visualize paths taken by the solver from the boundaries
to the entities of interest.
......
......@@ -253,22 +253,22 @@ def get_solutions_graph_data(G, info, centralities):
Doc::
https://networkx.github.io/documentation/networkx-1.10/reference/algorithms.component.html
https://networkx.github.io/documentation/stable/reference/algorithms/shortest_paths.html
average_shortest_path_length
https://networkx.github.io/documentation/stable/reference/algorithms/generated/networkx.algorithms.shortest_paths.generic.average_shortest_path_length.html#networkx.algorithms.shortest_paths.generic.average_shortest_path_length
weakly_connected_component_subgraphs
https://networkx.github.io/documentation/networkx-1.10/reference/generated/networkx.algorithms.components.weakly_connected.weakly_connected_component_subgraphs.html#networkx.algorithms.components.weakly_connected.weakly_connected_component_subgraphs
Measures
https://networkx.github.io/documentation/stable/reference/algorithms/index.html
https://networkx.github.io/documentation/networkx-1.10/reference/algorithms.component.html
https://networkx.github.io/documentation/stable/reference/algorithms/shortest_paths.html
average_shortest_path_length
https://networkx.github.io/documentation/stable/reference/algorithms/generated/networkx.algorithms.shortest_paths.generic.average_shortest_path_length.html#networkx.algorithms.shortest_paths.generic.average_shortest_path_length
weakly_connected_component_subgraphs
https://networkx.github.io/documentation/networkx-1.10/reference/generated/networkx.algorithms.components.weakly_connected.weakly_connected_component_subgraphs.html#networkx.algorithms.components.weakly_connected.weakly_connected_component_subgraphs
Measures
https://networkx.github.io/documentation/stable/reference/algorithms/index.html
By default the following information are added::
- graph_nodes: Number of nodes
- graph_edges: Number of edges
- graph_nodes_places: Number of biological places/entities.
The graph is a false bipartite graph, we remove the subset of transitions
in order to have the real count of biological places/entities.
The graph is a false bipartite graph, we remove the subset of transitions
in order to have the real count of biological places/entities.
If centralities is True, the folliwing information are added to the a new
key named "centralities"::
......
......@@ -43,6 +43,7 @@
Collection of widgets for properties checking
Classes:
- :class:`ChartChecker`: GUI interface for query checking
- :class:`QueryCheckingForm`: Main form of ChartChecker Window
- :class:`SolutionWindow`: Show solutions found by the solver
......@@ -930,10 +931,11 @@ class PropertyVisitor(object):
Retain only subnodes if they are in a binary expression linked by a logical "and".
Because:
- not (a or b) is valid only if a and b are False;
thus we don't care of a and b
thus we don't care of a and b
- not (a and b) is valid only if a or b are True, or if a and b are False;
thus a and b can be True alternately and it is sufficient for us.
thus a and b can be True alternately and it is sufficient for us.
"""
# print("not node:", str(node))
root = self.root
......
......@@ -227,10 +227,11 @@ class SearchManager(object):
def on_extract(self, widget):
"""Extract nodes environment
- Get selected nodes
- Get all transitions of interest:
- ori and ext nodes are concerned
- ori or ext are concerned and the second node is a Start/Trap node
- ori and ext nodes are concerned
- ori or ext are concerned and the second node is a Start/Trap node
"""
if not self.model:
return
......
......@@ -43,12 +43,12 @@ Main views for the Cadbiom gui
Classes available and inheritance hierarchy:
gtk.DrawingArea
ChartView: Used by the graph editor window/page of charter
NavView: overview widget
gtk.DrawingArea:
:class:`ChartView`: Used by the graph editor window/page of charter
:class:`NavView`: overview widget
gtk.Frame
ChartPage: Graph editor window/page of charter
gtk.Frame:
:class:`ChartPage`: Graph editor window/page of charter
"""
import gtk
......@@ -58,18 +58,18 @@ class ChartView(gtk.DrawingArea):
.. note:: Also instanciated by the overview widget.
.. note:: DrawingArea can capture key-press-events::
.. note:: DrawingArea can capture key-press-events:
- add gtk.gdk.KEY_PRESS_MASK mask to event
- be sure that the DrawingArea has the focus by using grab_focus() on
mouse events.
mouse events.
.. TODO:: Optimize events handling::
.. TODO:: Optimize events handling:
- on_motion_notify: Mouse over the widget, causing multiple calls to
find_element() of the top node.
find_element() of the top node.
- on_expose_event: When the window is covered/partially covered;
all the pixmap is redrawn.
all the pixmap is redrawn.
"""
def __init__(self, width, height, drawing_style, controler, model):
......
......@@ -55,7 +55,7 @@ def logger(name=LOGGER_NAME, logfilename=None):
Equivalent of logging.getLogger() call.
:Example:
:Example::
cm.logger(name=__name__)
......@@ -89,6 +89,7 @@ _logger.addHandler(stream_handler)
def log_level(level):
"""Set terminal/file log level to given one.
.. note:: Don't forget the propagation system of messages:
From logger to handlers. Handlers receive log messages only if
the main logger doesn't filter them.
......
......@@ -171,12 +171,14 @@ class CLDynSys(object):
/!\ Should not be used after adding the clauses by GT2Clauses (?)
:Examples:
:Examples::
{'PGK_cGMP_active': ('state', 0), ...}
{'input_place': ('input', 0), ...}
{'A': ('state', 0), ...}
:Completed by MCLTranslator with add_free_clock():
:Completed by MCLTranslator with add_free_clock()::
{"_h_0000": ('clock', -1)}
:param report: Reporter for error reporting.
......@@ -197,9 +199,10 @@ class CLDynSys(object):
Added from MCLTranslator.
:param place_clocks: Dictionary of clocks as keys and places as values.
Association between a clock and an inductive place:
clock h -> [place P, ...] where P is a place preceding free clock h
`clock h -> [place P, ...]` where P is a place preceding free clock h.
:Example::
:Example:
{"_h_2772": ["BTG2_gene", ...]}
:param inputs: Other inputs
......@@ -229,15 +232,14 @@ class CLDynSys(object):
Added to base_var_set
Auxiliary variables: They are named by adding a value incremented at their end.
Added to base_var_set
Ex: "_lit00000"
Ex: `"_lit00000"`
Free clock variables: Their names are preserved from the model.
Added to base_var_set
Added to free_clocks
Added to the dict symb_tab:
Ex: {"_h_0000": ('clock', -1)}
Added to the dict symb_tab: Ex: `{"_h_0000": ('clock', -1)}`
Place clocks:
Added to place_clocks:
Ex: {"_h_2772": ["BTG2_gene", ...]}
Added to place_clocks::
Ex: `{"_h_2772": ["BTG2_gene", ...]}`
Input variables: Their names are "supposed to be" preserved from the model.
Added to base_var_set
Added to inputs (May be added multiple times ?)
......@@ -269,9 +271,11 @@ class CLDynSys(object):
self.lit_compt = 0 # for auxiliary variables generation
def add_var(self, name):
"""add a logical variable to the dynamic system
@param name: the name of the variable (string)
All entities of the model are added here
"""Add a logical variable to the dynamic system
All entities of the model are added here
:param name: the name of the variable (string)
"""
if name in self.base_var_set:
return
......@@ -290,9 +294,13 @@ class CLDynSys(object):
def add_free_clock(self, hname):
"""add a free clock variable
@param hname: the name of the clock variable (string)
:param hname: the name of the clock variable (string)
Free clocks are associated to the value ('clock', -1) in self.symb_tab
ex: {"_h_0000": ('clock', -1)}
:Example::
{"_h_0000": ('clock', -1)}
"""
if hname in self.base_var_set:
......@@ -318,7 +326,7 @@ class CLDynSys(object):
def add_clause(self, clause):
"""add a clause constraint
PS: How to debug a clause:
PS: How to debug a clause::
cla_str = str(clause)
if "_h_0" in cla_str or "A" in cla_str: print(cla_str)
......
......@@ -46,18 +46,16 @@ 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
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
the form of clauses containing numerical values.
Ex: `dim_start, dim_inv, dim_final, dim_variant`
---
About shifting clauses and variables:
Initialization of the dynamic system by __forward_init_dynamic() iterates on
all literals of the system.
If a literal is a t+1 literal, its value is shifted to the right or to the
......@@ -74,7 +72,7 @@ About shifting clauses and variables:
values to the right or to the left depending on whether their values are
positive or negative.
*constraints unfolder attributes are shifted at every step and submitted to
\*constraints unfolder attributes are shifted at every step and submitted to
the solver.
---
......@@ -96,28 +94,28 @@ init_forward_unfolding():
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
- __precomputed_variant_constraints:
Query data (automatic merge of textual and DIMACS forms)
- __variant_constraints:
Initialized with the first item of __precomputed_variant_constraints
- __precomputed_dynamic_constraints:
Initialized with the whole previously shifted system
if the size of the system hasn't changed, and if no auxiliary
clauses has been added meanwhile.
- `__initial_constraints`:
Query data + negative values of all places that are not frontiers.
- `__final_constraints`:
Query data
- `__invariant_constraints`:
List of Query data
- `__precomputed_variant_constraints`:
Query data (automatic merge of textual and DIMACS forms)
- `__variant_constraints`:
Initialized with the first item of `__precomputed_variant_constraints`
- `__precomputed_dynamic_constraints`:
Initialized with the whole previously shifted system
if the size of the system hasn't changed, and if no auxiliary
clauses has been added meanwhile.
Shifted attributes with __shift_step (nb of variables in the system):
- __forward_init_dynamic(): __dynamic_constraints:
Shift dynamic_system.clauses + dynamic_system.aux_clauses + init
Shift dynamic_system.clauses + dynamic_system.aux_clauses + init
- __shift_final(): __final_constraints:
Shift + replace __final_constraints
Shift + replace __final_constraints
- __shift_invariant(): __invariant_constraints:
Shift + append of the last element of __invariant_constraints
Shift + append of the last element of __invariant_constraints
PS: __variant_constraints si already initialized for the first step
......@@ -130,9 +128,9 @@ init_forward_unfolding():
__aux_code_table.
- __init_initial_constraint_0, __init_final_constraint_0, __init_invariant_constraint_0
Call __code_clause + __compile_property
Call __code_clause + __compile_property
- __init_variant_constraints_0
Call __code_clause + __compile_event
Call __code_clause + __compile_event
shift():
......@@ -144,14 +142,14 @@ shift():
Modified attributes:
- __shift_dynamic(): __dynamic_constraints:
Shift + append of the last element of __dynamic_constraints
Shift + append of the last element of __dynamic_constraints
- __shift_variant(): __variant_constraints:
Shift clauses of the current step in __precomputed_variant_constraints,
and append them to __variant_constraints.
Shift clauses of the current step in __precomputed_variant_constraints,
and append them to __variant_constraints.
- __shift_invariant()
...
...
- __shift_final()
...
...
PS: __initial_constraints are left as this for now
(shifted only with BACKWARD shift direction).
......@@ -194,8 +192,8 @@ class CLUnfolder(object):
variable names to DIMACS code and back, to extract the frontier of a model
and to extract informations from raw solutions.
Dynamic constraints unfolding management
========================================
Dynamic constraints unfolding management:
Each variable is coded as an integer (in var_code_table and var_list).
Each clause is represented as a list of signed integers (DIMACS coding).
......@@ -205,8 +203,8 @@ class CLUnfolder(object):
self.__shift_step depends on the number of variables so it is impossible
to add variables while generating a trajectory unfolding.
Glossary
========
Glossary:
- ground variables/ground DIMACS code: variables at time t=0 (not shifted).
- solution: a solution of the logical dynamic constraint from SAT solver
- state vector: list of DIMACS code of original (not shifted) variables
......@@ -215,9 +213,9 @@ class CLUnfolder(object):
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;
- `__*_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;
initialized from the query attributes.
"""
......@@ -525,6 +523,7 @@ class CLUnfolder(object):
"""Initialise the unfolder with the given query
Following attributes are used from the query:
start_prop, dim_start, inv_prop, dim_inv, final_prop, dim_final,
variant_prop, dim_variant, steps_before_check
......@@ -544,6 +543,7 @@ class CLUnfolder(object):
.. warning:: This option should be disable for performance reasons;
or if you know what you are doing.
You will assume in particular that:
- textual properties are not modified
- values of literals in DIMACS properties are already described
in the model (new literals are not allowed).
......@@ -684,7 +684,7 @@ class CLUnfolder(object):
.. note:: time index is the number of steps since the begining of the
simulation.
:Example - Only standard variables:
:Example - Only standard variables::
__shift_step = 2 (number of variables in the system)
shift_step_init = 2 (number of variables in the system at the initial state)
......@@ -702,7 +702,7 @@ class CLUnfolder(object):
=> return: "n1_3"
:Example - With an auxiliary variable:
:Example - With an auxiliary variable::
__shift_step = 2 (There is 1 auxiliary variable)
shift_step_init = 1
......@@ -731,8 +731,10 @@ class CLUnfolder(object):
=> return: "_lit0_2"
@param var_num: DIMACS literal coding
@return: name of the variable with the time index appended
:param var_num: DIMACS literal coding
:type var_num: <int>
:return: name of the variable with the time index appended
:rtype: <str>
"""
varnum1 = abs(var_num)
# Get the original var_code without shifts
......@@ -1593,28 +1595,30 @@ class CLUnfolder(object):
This is why the shift is made after initialization.
Initialized attributes:
- __initial_constraints:
Query data + negative values of all places that are not frontiers.
Query data + negative values of all places that are not frontiers.
- __final_constraints:
Query data
Query data
- __invariant_constraints:
List of Query data
List of Query data
- __precomputed_variant_constraints:
Query data (automatic merge of textual and DIMACS forms)
Query data (automatic merge of textual and DIMACS forms)
- __variant_constraints:
Initialized with the first item of __precomputed_variant_constraints
Initialized with the first item of __precomputed_variant_constraints
- __precomputed_dynamic_constraints:
Initialized with the whole previously shifted system
if the size of the system hasn't changed, and if no auxiliary
clauses has been added meanwhile.
Initialized with the whole previously shifted system
if the size of the system hasn't changed, and if no auxiliary
clauses has been added meanwhile.
Shifted attributes with __shift_step (nb of variables in the system):
- __dynamic_constraints:
Shift dynamic_system.clauses + dynamic_system.aux_clauses + init
Shift dynamic_system.clauses + dynamic_system.aux_clauses + init
- __final_constraints:
Shift + replace __final_constraints
Shift + replace __final_constraints
- __invariant_constraints:
Shift + append of the last element of __invariant_constraints
Shift + append of the last element of __invariant_constraints
PS: __variant_constraints si already initialized for the first step.
......@@ -1628,15 +1632,15 @@ class CLUnfolder(object):
__aux_code_table.
- __init_initial_constraint_0, __init_final_constraint_0, __init_invariant_constraint_0
Call __code_clause + __compile_property
Call __code_clause + __compile_property
- __init_variant_constraints_0
Call __code_clause + __compile_event
Call __code_clause + __compile_event
Called at the begining of squery_is_satisfied() and squery_solve()
TODO: Attention pour le moment les litéraux présents dans les attributs
.. TODO:: Attention pour le moment les litéraux présents dans les attributs
DIMACS de la query doivent déjà etre présents dans le modèle.
Lorsqu'ils sont ajoutés aux variables *constraints, à aucun moment
Lorsqu'ils sont ajoutés aux variables \*constraints, à aucun moment
les valeurs absentes de dynamic_constraints ne sont ajoutées à
__aux_code_table et __aux_list; shift_step n'est pas non plus incrémenté !!
"""
......
......@@ -45,9 +45,10 @@ 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
- 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
......@@ -84,14 +85,12 @@ __mac_exhaustive_search:
Pour bannir les solutions 2 choix se présentent:
- Soit les joindre par des "and" logiques et contraindre chaque solution
par un "non".
Ex: Pour 2 solutions [(A, B), (B, C)]:
not((A and B) or (B and C))
par un "non".
Ex: Pour 2 solutions `[(A, B), (B, C)]`: `not((A and B) or (B and C))`
- Soit conserver les valeurs de chaque ensemble de places frontière sous
forme de clauses constituées de valeurs numériques.
Ex: Pour 2 solutions [(A, B), (B, C)]:
[[-1, -2], [-2, -3]]
forme de clauses constituées de valeurs numériques.
Ex: Pour 2 solutions `[(A, B), (B, C)]`: `[[-1, -2], [-2, -3]]`
La deuxième solution est nettement plus performante car elle permet de
s'affranchir du travail de parsing réalisé par l'intervention d'une grammaire,
......@@ -576,42 +575,47 @@ class MCLAnalyser(object):
"""Compute active frontier places and timings
Compute the set of frontier place names which must be activated for
implying query satisfaction and returned it as a list of FrontierSolution.
implying query satisfaction and returned it as a list of `FrontierSolution`.
Quiet deprecated but referenced by:
gt_gui/chart_checker/chart_checker_controler
cadbiom_cmd/solution_search.py very old code for debug purpose
self.mac_inhibitor_search
- `gt_gui/chart_checker/chart_checker_controler`
- `cadbiom_cmd/solution_search.py` very old code for debug purpose
:meth:`mac_inhibitor_search`
In models of signal propagation, we are more interested in frontier solutions.
So the current method is better adapted: sq_frontier_solutions()
than sq_solutions() which returns RawSolutions.
So the current method is better adapted than :meth:`sq_solutions`
which returns `RawSolutions`.
This function is a wrapper of sq_solutions().
This function is a wrapper of :meth:`sq_solutions`.
The class FrontierSolution provides objects wrapping a symbolic
The class `FrontierSolution` provides objects wrapping a symbolic
representation of frontier values and timing from a raw solution.
- The main attributes are activated_frontier which is a set of
(string) names of frontier places which are activated in the solution.
(string) names of frontier places which are activated in the solution.
- The second important attribute is ic_sequence, a list of strings
which describes the successive activated inputs and free events in
the solution.
which describes the successive activated inputs and free events in
the solution.
If events h2, h5 and input in3 are activated at step k in the solution,
then the kth element of the list is “% h2 h5 in3”.
This format is understood by the Cadbiom simulator.
@warning: no frontier places are initialized to False
.. warning:: no frontier places are initialized to False
@param query: MCLSimpleQuery
@param max_step: int - Number of steps allowed in the unfolding;
:param query: Query
:param max_step: int - Number of steps allowed in the unfolding;
the horizon on which the properties must be satisfied
@param max_sol: max number of wanted solutions.
@return: List of FrontierSolutions built from RawSolutions from the solver.
:param max_sol: max number of wanted solutions.
:type query: MCLSimpleQuery
:type max_step: <int>
:type max_sol: <int>
:return: List of FrontierSolutions built from RawSolutions from the solver.
So, lists of lists of frontier place names which must be activated
for implying query satisfaction
for implying query satisfaction.
:rtype: <list <FrontierSolution>>
"""
vvars = self.unfolder.frontier_values
......@@ -832,10 +836,10 @@ class MCLAnalyser(object):
.. note:: __mac_exhaustive_search() returns DimacsFrontierSols
@param query: MCLSimpleQuery
@param max_step: int - Number of steps allowed in the unfolding;
:param query: MCLSimpleQuery
:param max_step: int - Number of steps allowed in the unfolding;
the horizon on which the properties must be satisfied
@return: <generator <FrontierSolution>>
:return: <generator <FrontierSolution>>
"""
## TODO: convert start_property in dim_start !! => eviter la recompilation des propriétés
# Get <generator <DimacsFrontierSol>>
......
......@@ -55,11 +55,11 @@ class MCLSimpleQuery(object):
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
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
the form of clauses containing numerical values.
Ex: `dim_start, dim_inv, dim_final, dim_variant`
Textual properties of query are compiled into numeric clauses in the unfolder
with init_forward_unfolding(), just at the beginning of squery_is_satisfied()
......@@ -72,15 +72,18 @@ class MCLSimpleQuery(object):
:param final_prop: final property; logical formulas
:param variant_prop: list of logical formulas from ic_sequence.
It's the trajectory of events of a solution.
:Example:
:Example::
['', 'h2 and h2', '', 'h2']
:param dim_start: start property in DIMACS form - optional
:param dim_inv: invariant property in DIMACS form - optional
:param dim_final: final property in DIMACS form - optional
:param dim_variant: list of lists of dimacs clauses
:Example:
:Example::