Library package

Global settings

cadbiom.commons.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.

cadbiom.commons.logger(name='cadbiom', logfilename=None)

Return logger of given name, without initialize it.

Equivalent of logging.getLogger() call.

Example::cm.logger(name=__name__) Parameters:name – Name of the logger, only displayed if “%(name)s” is present in the logging.Formatter.

Dynamical analysis

Dynamic system

Classes for building clause constraint models

class cadbiom.models.clause_constraints.CLDynSys.CLDynSys(symb_tab, report)

Class to describe a dynamic system in clause form.

Parameters:

• symb_tab (<dict <str>: <tuple <str>, <int>>>) –

  Symbol table of charter model produced by Table_visitor Dict of entities names as keys, and states as values. States are described like: (type, deepness); where deepness if the imbrication level of macro states (Cf Table_visitor).

  All keys = no_frontiers + frontiers + model name (probably a bug for this last one)

  /!Should not be used after adding the clauses by GT2Clauses (?)

  Examples::{‘PGK_cGMP_active’: (‘state’, 0), …} {‘input_place’: (‘input’, 0), …} {‘A’: (‘state’, 0), …} Completed by MCLTranslator with add_free_clock()::  {“_h_0000”: (‘clock’, -1)}
• report (<Reporter>) – Reporter for error reporting.
• base_var_set (<set <str>>) – Set of ALL variables of the dynamic system (including inputs, entities, clocks/events, auxiliary variables)
• clauses (<list <Clause>>) – Clauses Added from MCLTranslator.
• aux_clauses (<list <Clause>>) – Auxiliary clauses. Added from MCLTranslator.
• frontiers (<list <str>>) – All frontiers of the model. Used by CLUnfolder. Added from MCLTranslator. Cf GT2Clauses.visit_csimple_node()
• no_frontiers (<list <str>>) – Places that are not frontiers. Added from MCLTranslator. Cf GT2Clauses.visit_csimple_node()
• free_clocks (<list <str>>) – Free clocks names inputs. Added from MCLTranslator.
• place_clocks (<defaultdict <list>>) –

  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.

  Example::{“_h_2772”: [“BTG2_gene”, …]}
• inputs (<list <str>>) – Other inputs
• lit_compt (<int>) – Incrementable id for auxiliary variables naming.

The frontiers, free_clocks, place_clocks lists are used for extraction of informations from solutions. The place_clocks list is used for generating the structural constraints OR(place P and clock h) implying that at least one clock transition must be activated at each step.

Additional information about attributes:

Model Entities: Their names are preserved from the model.

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”

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)}

Place clocks:

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 ?)

Clauses:

Added to clauses

Auxiliary clauses:

Added to aux_clauses

add_aux_clause(clause)

add an auxiliary clause constraint

add_aux_var()

create an auxiliary variable for compiler purpose

Auxiliary variables are named by adding a value incremented at their end

ex: “_lit00000”

add_clause(clause)

add a clause constraint

PS: How to debug a clause:

cla_str = str(clause)
if "_h_0" in cla_str or "A" in cla_str: print(cla_str)

add_free_clock(hname)

add a free clock variable

Parameters:hname –

the name of the clock variable (string) Free clocks are associated to the value (‘clock’, -1) in self.symb_tab

Example::{“_h_0000”: (‘clock’, -1)}

add_input(name)

add a variable representing an input @param name: name of the input

add_place_clock(pname, hname)

add an association hname –> pname between a clock and an inductive place

add_var(name)

Add a logical variable to the dynamic system

All entities of the model are added here

Parameters:name – the name of the variable (string)

get_var_number()

Get the number of ALL variables of the dynamic system (including inputs, entities, clocks/events, auxiliary variables)

class cadbiom.models.clause_constraints.CLDynSys.Clause(list_lit=[])

Objects representing logical clauses

A clause is represented as a list of literals.

Attributes:

param literals:Variable name type literals:<list <Literal>>

add_lit(lit)

Add a literal to the clause @param lit: <Literal>

classmethod string_to_clause(text_clause)

Transform a string into a clause (not used)

Example of text: “a,not b,not c”.

Warning

strict syntax - no check - for tests only

class cadbiom.models.clause_constraints.CLDynSys.Literal(name, sign)

Object representing literals.

A literal is a pair (string, boolean).

Attributes:

param name:Variable name param sign:Boolean the sign of the literal. Positive or negative: True or False type name:<str> type sign:<boolean>

code_name()

Return a string representing the literal

lit_not()

Return the negation of the literal (opposite sign)

opposite(other)

true if one literal is the negation of the other

Unfolding and solving engine

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

—

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 left depending on whether its sign is positive or negative (addition vs soustraction of the shift_step value which is the number of variables in the system).

Otherwise, the literal is a t literal and its value stays untouched.

t+1 and t literals are generated by CLDynSys object directly from the current model.

Shifting a clause consists to iterates on all its literals and shift their 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 the solver.

—

init_with_query(query):

Copy of the query attributes to temporary attributes of 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 (increase shift_step). This is why any shift must be made after the initialization.

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
• __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_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

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 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 Call __code_clause + __compile_property
• __init_variant_constraints_0 Call __code_clause + __compile_event

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 __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).

class cadbiom.models.clause_constraints.mcl.CLUnfolder.CLUnfolder(dynamic_system, debug=False)

When loading a model in a MCLAnalyser object, a CLUnfolder is generated which implies the compilation of the dynamical system into a clause constraint dynamical system and the DIMACS coding of all the variables. This coding cannot be changed later. The unfolding of constraints is performed efficiently on the numeric form of the clause constraints. The CLUnfolder provide various method to convert 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:

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).

During unfolding, clauses are shifted either to the future (forward) or to the past (backward). The shift operator is a simple addition of self.__shift_step. The shift direction depends only on initializations. self.__shift_step depends on the number of variables so it is impossible to add variables while generating a trajectory unfolding.

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 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; initialized from the query attributes.

check_query(query)

Check textual and DIMACS properties of the given query

If textual properties have changed since the last initialization of the CLUnfolder, new auxiliary variables will be added to the dynamic system.

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. 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 involve events that are not in the model…

Called by:

init_with_query()

Parameters:query (<MCLSimpleQuery>) – Query built with start, invariant, final, variant properties in textual and/or DIMACS forms.

current_step

@return: the current number of unfolding

dynamic_constraints

For tests: returns coded dynamic constraints

final_constraints

For tests: returns coded final constraints

free_clocks

Get the DIMACS codes of the free_clocks variables

get_system_var_number()

Get number of variables in the clause constraint dynamical system (including inputs, entities, clocks/events, auxiliary variables) (for tests)

Note

This number should be equal to the number of variables in self.get_var_number()

get_var_indexed_name(var_num)

Get name of the variable with the time index appended

Note

time index is the number of steps since the begining of the simulation.

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) __var_list = [“##”, “n1”, “n2”]

Virtual list of indexes in the state vector of a solution: [0, 1, 2, 3, 4, 5, 6, 7, 8, …]

#|n1,n2|n1,n2|n1,n2|n1,n2|

ti=0 ti=1 ti=2 ti=3

Given var_num = 7: index of var_name in __var_list: ((7-1) % 2) + 1 = 1 var_name = “n1” time index: (7 - 1) / 2 = 3

=> return: “n1_3”

Example - With an auxiliary variable::  

__shift_step = 2 (There is 1 auxiliary variable) shift_step_init = 1 __var_list = [“##”, “n1”] __aux_list = [“_lit0”]

Virtual list of indexes in the state vector of a solution: [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, …]

#|n1,_lit0|n1,_lit0|n1,_lit0|

ti=0 ti=1 ti=2

If the index is > shift_step_init, then it is an auxiliary variable. In order to get the index in __aux_list we have to substract:

• 1 because on the contrary of __var_list, __aux_list begins at index 0
• shift_step_init because value of the first aux variable

follows the last value of __var_list

Given var_num = 6 var_code of var_name: ((6-1) % 2) + 1 = 2 2 > shift_step_init index of var_name in __aux_list:

var_code - shift_step_init - 1 2 -1 -1 = 0

var_name = “_lit0”

=> return: “_lit0_2”

Parameters:

var_num (<int>) – DIMACS literal coding

Returns:

name of the variable with the time index appended

Return type:

<str>

get_var_name(var_num)

Get name of the variable

See also

Explanations on get_var_indexed_name()

@param var_num: DIMACS literal coding of an initial variable @return: name of the variable

get_var_number()

Get number of principal variables (properties excluded) in the unfolder (including inputs, entities, clocks/events, auxiliary variables) (for tests)

Note

This number should be equal to the number of variables in self.get_system_var_number()

init_backward_unfolding()

Initialisation before generating constraints - backward trajectory Never used (and backward not implemented in __init_variant_constraints_0)

init_forward_unfolding()

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
• __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):

• __dynamic_constraints: Shift dynamic_system.clauses + dynamic_system.aux_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.

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 and in __aux_code_table.

• __init_initial_constraint_0, __init_final_constraint_0, __init_invariant_constraint_0 Call __code_clause + __compile_property
• __init_variant_constraints_0 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 DIMACS de la query doivent déjà etre présents dans le modèle. 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é !!

init_with_query(query, check_query=True)

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

Textual properties of query are compiled into numeric clauses in 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). Thus, the system will be rebuilt.

Parameters:

query (<MCLSimpleQuery>) – Query built with start, invariant, final, variant properties in textual and/or DIMACS forms.

Key check_query:  

Check textual and DIMACS properties of the given query.

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).

initial_constraints

For tests: returns coded initial constraints

inputs

Get the DIMACS codes of the input variables

invariant_constraints

For tests: returns coded invariant constraints

reset()

Reset the unfolder before a new query

Reset only properties and dimacs clauses from the current query; AND __precomputed_variant_constraints.

__initial_constraints, __final_constraints, __invariant_constraints, __variant_constraints and __dynamic_constraints ARE NOT reset here (see init_forward_unfolding()).

This function is called from the constructor and during MCLAnalyser.sq_is_satisfiable() and MCLAnalyser.sq_is_satisfiable() following the call of init_with_query().

set_include_aux_clauses(val)

Flag to include auxiliary clause to eliminate undesirable solutions.

If A->B has clock h, an aux constraint added is h included in h when A Must be set to False for inhibitors computations.

Warning

This function impacts the shift_step number.

Tested by:

• __forward_init_dynamic
• __backward_init_dynamic

set_stats()

Enable solver statistics (for tests)

shift()

Shift all clauses of the system to prepare it for the next step.

self.__current_step is incremented here!

Modified attributes:

• __dynamic_constraints[-1] (last element)

  Shift + append of the last element of __dynamic_constraints

• __invariant_constraints[-1] (last element)

  Shift + append of the last element of __invariant_constraints

• __precomputed_variant_constraints[current_step]

  Shift clauses of the current step in __precomputed_variant_constraints, and append them to __variant_constraints.

• __final_constraints if __shift_direction is “FORWARD”
• __initial_constraints if __shift_direction is “BACKWARD”

PS: __initial_constraints are left as this for now (shifted only with BACKWARD shift direction)

Called at each step by:

• squery_solve()
• squery_is_satisfied()

shift_direction

@return: string “FORWARD” or “BACKWARD”

shift_step

@return: the shift step ss (if n is X_0 code, n+ss is X_1 code)

squery_is_satisfied(max_step)

Ask the SAT solver if the query/system is satisfiable in the given number of steps.

If __invariant_property is set and __final_property is not set, 1 satisfiability test is made only after all shift() calls for each remaining step from the current step.

Otherwise, 1 test is made for each remaining step after each shift() call.

Warning

vvars (frontier values) are not tested. Thus the satisfiability is not tested for interesting variables like in squery_solve().

Note

This function checks and corrects incoherent data on step number. __steps_before_check can’t be >= max_step. max_step can’t be >= to __precomputed_variant_constraints.

Parameters:max_step (<int>) – The horizon on which the properties must be satisfied.

squery_solve(vvars, max_step, max_sol, max_user_step=None)

Search max_sol number of solutions with max_step steps, involving variables of interest (frontiers).

Assert a query is loaded (start_condition, inv_condition, final_condition)

If __invariant_property is set and __final_property is not set, 1 unique solution search is made only after all shift() calls for each remaining step from the current step.

Otherwise, 1 test is made for each remaining step after each shift() call.

Note

This function checks and corrects incoherent data on step number. __steps_before_check can’t be >= max_step. max_step can’t be >= to __precomputed_variant_constraints.

Note

À propos de l’auto-ajustement du nombre maximal d’étapes (max_step) à l’aide de max_user_step:

Lorsqu’il n’y a plus de solutions pour 1 étape donnée, mais que ce nombre d’étapes est < au nombre fixé par l’utilisateur, on peut bénéficier des shifts précédents sur le modèle et on éviter de reconstruire le problème pour un nouveau test de satisfiabilité à l’étape suivante. Le fait de rechercher 1 propriété est déjà un test de satisfiabilité. Rien de plus ou de moins n’est fait par le solveur. Concrètement squery_solve est capable d’incrémenter tout seul le max_step jusqu’au max_user_step durant l’étape de solving.

Aucun risque d’augmenter le min_step lors de l’étape d’élagage d’une solution connue car : - le pb n’est pas moins contraint que lorsqu’il a trouvé la solution à élaguer => 1 solution au moins est toujours retournée. - max_user_step est laissé à None

Parameters:

• max_step (<int>) – bounded horizon for computations
• max_sol (<int>) – The maximum number of solutions to be returned
• vvars (<list <int>>) – Variables for which solutions must differ. In practice, it is a list with the values (Dimacs code) of all frontier places of the system.

Key max_user_step:  

(Optional) If max_user_step is set, we increment the current max_step until it reaches max_user_step. This saves some cycles by reusing the current CLUnfolder for an extra step. .. seealso:: cadbiom.models.clause_constraints.mcl.MCLAnalyser.__mac_exhaustive_search()

Returns:

RawSolution objects RawSolution objects contain a solution got from SAT solver with all variable parameters from the unfolder

Return type:

<tuple <RawSolution>>

stats()

Display solver statistics

unset_stats()

Disable solver statistics (never used)

var_dimacs_code(var_name)

Returns DIMACS code of var_name (string) variable (for tests)

var_names_in_clause(clause)

Return the names of the variables from values in the given numeric clause (DEBUG never used)

variant_constraints

For tests: returns coded variant constraints

class cadbiom.models.clause_constraints.mcl.CLUnfolder.PropertyVisitor(aux_cpt=0)

SigExpression on states and events into a set of clauses Type checking must be done.

visit_sig_const(exp)

translate a constant expression

visit_sig_default(exp)

default translation

visit_sig_ident(tnode)

ident -> literal

visit_sig_not(node)

translate a not

visit_sig_sync(binnode)

translate a binary (or/and) expression

visit_sig_when(exp)

when translation

Dynamic analysis

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:

Wrapper for __mac_exhaustive_search() Return a generator of FrontierSolution objects.

__mac_exhaustive_search:

Return a generator of FrontierSolution objects.

Test if the given query is satisfiable according the given maximum number of steps. Get the minimum of steps that are mandatory to reach the final property in the query.

This task is made with: sq_is_satisfiable(query, max_user_step) Which call internal functions of the unfolder (this is beyond the scope of this doc)

• Initialisation: self.unfolder.init_with_query(query)
• Ultimate test: self.unfolder.squery_is_satisfied(max_step)

Adjust the attribute steps_before_check of the query, this is the number of useless shifts that are needed by the unfolder before finding a solution.

Reload in the query a list of frontiers values that constitute each solution previously found. These values are in DIMACS format (i.e, numerical values). Since we doesn’t want further similar solutions, each value has a negative sign (which which means that a value is prohibited).

On banni les solutions précédemment trouvées. Une solution est apparentée à un ensemble de places frontières; Notons qu’il n’y a pas de contraintes sur les trajectoires ayant permis d’obtenir un ensemble de places frontières.

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))
• 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]]

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, des propriétés de plus en plus complexes au fur et à mesure des solutions trouvées.

Ainsi, chaque nouvelle requête se voit recevoir dans son attribut dim_start, l’ensemble des solutions précédentes, bannies, au format DIMACS.

On cherche ensuite d’abord des solutions non minimales (actuellement 2) via: self.__sq_dimacs_frontier_solutions(query, nb_step, 2)

Pour ensuite les élaguer en supprimant les places non essentielles à la satisfiabilité de la propriété via: small_fsol = self.less_activated_solution(lfsol) current_mac = self.__prune_frontier_solution(small_sol, query, nb_step)

Ce processus itératif est le plus “time-consuming” car nous n’avons pas le controle sur les solutions fournies par SAT et les solutions non minimales sont en général très éloignées de la solution minimale, c.-à-d. contiennent beaucoup plus de places (ces places excédentaires sont dispensables).

next_mac(self, query, max_step):

Search a Minimal Access Condition for the given query.

This is a function very similar to __mac_exhaustive_search(), but it returns only 1 solution. Satisfiability tests and the banishment of previous solutions must be done before the call.

—

## Back on the few mentioned functions and their call dependencies:

less_activated_solution(self, dimacs_solution_list):

Get the solution with the less number of activated frontier places among the given solutions.

__prune_frontier_solution(self, fsol, query, max_step):

Take a frontier condition which induces a property “prop” and try to reduce the number of activated frontier variables from this solution while inducing “prop”.

Find at most nb_sols_to_be_pruned frontier solutions inducing the same final property but with all inactivated frontier places forced to be initially False.

Repeat the operation until there is only one solution.

Return <DimacsFrontierSol>

This functions calls __solve_with_inact_fsolution().

__solve_with_inact_fsolution(self, dimacs_front_sol, query, max_step, max_sol):

Frontier states not activated in dimacs_front_sol (DimacsFrontierSol) are forced to be False at start; solve this and return DimacsFrontierSol objects matching this constraint (their number is defined with the argument max_sols) Return <tuple <DimacsFrontierSol>>

This function calls __sq_dimacs_frontier_solutions().

__sq_dimacs_frontier_solutions(self, query, max_step, max_sol)

Search set of minimal solutions for the given query, with a maximum of steps Tuple of unique DimacsFrontierSol objects built from RawSolutions from the solver. Return <tuple <DimacsFrontierSol>>

This function calls sq_solutions().

sq_solutions(query, max_step, max_sol, vvars)

This function is the lowest level function exploiting the solver results. Return <list <RawSolution>>

This function calls:

self.unfolder.init_with_query(query, check_query=False) self.unfolder.squery_solve(vvars, max_step, max_sol)

## Quiet deprecated but still used in the GUI:

sq_frontier_solutions(self, query, max_step, max_sol):

This function is a wrapper of sq_solutions(). Return <list <FrontierSolution>>

class cadbiom.models.clause_constraints.mcl.MCLAnalyser.MCLAnalyser(report, debug=False)

Query a dynamical system and analyse the solutions

When loading a model in a MCLAnalyser object, a CLUnfolder is generated which implies the compilation of the dynamical system into a clause constraint dynamical system and the DIMACS coding of all the variables. This coding cannot be changed later. The unfolding of constraints is performed efficiently on the numeric form of the clause constraints. The CLUnfolder provide various method to convert variable names to DIMACS code and back, to extract the frontier of a model and to extract informations from raw solutions.

Attributes and default values:

param dynamic_system:  dynamical system in clause constraint form param unfolder:computation management: unfolding param reporter:reporter for generic error display param translator_opti:  turn on optimizations for ANTLR translation (subexpression elimination) param nb_sols_to_be_pruned:  For mac search: We search a number of solutions that will be pruned later, in order to find the most optimized MAC with a reduced the number of activated frontiers. key debug:(optional) Used to activate debug mode in the Unfolder type dynamic_system:  None before loading a model / <CLDynSys> type unfolder:None before loading a model / <CLUnfolder> type debug:False / <boolean> type reporter:<ErrorRep> type translator_opti:  True / <boolean> type nb_sols_to_be_pruned:  10

build_from_cadlang(file_name)

Build an MCLAnalyser from a .cal, Cadlang file

Parameters:file_name (<str>) – path of .cal file

build_from_chart_file(file_name)

Build an MCLAnalyser from a .bcx file

Parameters:file_name (<str>) – path of the .bcx file

build_from_chart_model(model)

Build an MCLAnalyser and its CLUnfolder from a chartmodel object.

Every parser uses this function at the end.

Parameters:model (<ChartModel>) – Chart Model

build_from_pid_file(file_name, has_clock=True, ai_interpretation=0)

Build an MCLAnalyser from a .xml file of PID database

Parameters:file_name (<str>) – path of .xml file

dynamic_system

Return the CLDynSys object of the current unfolder

is_strong_activator(act_sol, query)

Test if an activation condition is a strong one (independent of timing)

final property becomes the invariant property => Ex: test if “C3 and C4” will never append if start property is “A1 and C1 and B1” Cf TestMCLAnalyser…

@return: False if the problem is satisfiable, True otherwise @param act_sol: FrontierSolution with activation condition @param query: the query used for act_sol condition

is_strong_inhibitor(in_sol, query)

Test if an activation condition inhibitor is a strong one (i.e independent of timing)

@param in_sol: FrontierSolution with activation condition and inhibition @param query: the property which is inhibed

less_activated_solution(dimacs_solution_list)

Get the solution with the less number of activated frontier places among the given solutions.

Note

There is not constraint on the complexity of the trajectories; only on the number of activated frontier places.

Parameters:dimacs_solution_list (<tuple <DimacsFrontierSol>>) – list of DimacsFrontierSol objects Returns:1 DimacsFrontierSol with the less number of activated states. Return type:<DimacsFrontierSol>

mac_inhibitor_search(mac, query, max_sol)

Search inhibitors for a mac scenario

@param mac: the mac @param query: the property enforced by the mac @param max_sol: limit on the number of solutions @param max_sol: maximum number of solutions

@return: a list of frontier solution

mac_search(query, max_step)

Wrapper for __mac_exhaustive_search(); return a generator of FrontierSolution objects.

Note

__mac_exhaustive_search() returns DimacsFrontierSols

Parameters:

• query – MCLSimpleQuery
• max_step – int - Number of steps allowed in the unfolding; the horizon on which the properties must be satisfied

Returns:

<generator <FrontierSolution>>

next_inhibitor(mac, query)

if st_prop contains negation of mac conditions, return a different mac if any same parameters as __mac_exhaustive_search Used for search on cluster

@param mac: FrontierSolution @param query: MCLSimpleQuery @param max_step: int - number of dynamical step @return: a list of variables (list<string>)

next_mac(query, max_step)

Search a Minimal Access Condition for the given query.

This is a function very similar to __mac_exhaustive_search(), but it returns only 1 solution. Satisfiability tests and the banishment of previous solutions must be done before the call.

—

On cherche ensuite d’abord des solutions non minimales (actuellement 2) via: self.__sq_dimacs_frontier_solutions(query, nb_step, 2)

Pour ensuite les élaguer en supprimant les places non essentielles à la satisfiabilité de la propriété via: small_fsol = self.less_activated_solution(lfsol) current_mac = self.__prune_frontier_solution(small_sol, query, nb_step)

Ce processus itératif est le plus “time-consuming” car nous n’avons pas le controle sur les solutions fournies par SAT et les solutions non minimales sont en général très éloignées de la solution minimale, c.-à-d. contiennent beaucoup plus de places (ces places excédentaires sont dispensables).

Parameters:max_step (<int>) – Number of steps allowed in the unfolding; the horizon on which the properties must be satisfied Returns:A FrontierSolution which is a wrapper of a symbolic representation of frontier values and timings from a raw solution. Return type:<FrontierSolution> - <list <str>>

sq_frontier_solutions(query, max_step, max_sol)

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.

Quiet deprecated but referenced by:

• gt_gui/chart_checker/chart_checker_controler
• cadbiom_cmd/solution_search.py very old code for debug purpose mac_inhibitor_search()

In models of signal propagation, we are more interested in frontier solutions. So the current method is better adapted than sq_solutions() which returns RawSolutions.

This function is a wrapper of sq_solutions().

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.
• The second important attribute is ic_sequence, a list of strings 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

Parameters:

• query (MCLSimpleQuery) – Query
• max_step (<int>) – int - Number of steps allowed in the unfolding; the horizon on which the properties must be satisfied
• max_sol (<int>) – max number of wanted solutions.

Returns:

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.

Return type:

<list <FrontierSolution>>

sq_is_satisfiable(query, max_step)

Check if the query is satisfiable.

Warning

Many logical variables are auxiliary variables with no interest other than technical, we want different solutions to differ by their values on some set of significant variables.

These variables of interest are not checked here!

It is just a satisfiability test!

Warning

No frontier place is initialized to False in simple queries.

Parameters:

• query (<MCLSimpleQuery>) –
• max_step (<int>) – Number of steps allowed in the unfolding; the horizon on which the properties must be satisfied

Return type:

<boolean>

sq_solutions(query, max_step, max_sol, vvars, max_user_step=None)

Return a list of RawSolution objects

This function is the lowest level function exploiting the solver results.

Parameters are the same as in sq_is_satisfiable() except for vvars parameter which deserves some explanations.

The solver doesn’t provide all solutions of the set of logical constraints encoding the temporal property. It gives only a sample of these solutions limited in number by the max_sol parameter. Since many logical variables are auxiliary variables with no interest other than technical, we want different solutions to differ by their values on some set of significant variables. That is the meaning of the vvars parameter.

Remark that the variables of interest must be specified in DIMACS code. Most of the time, this method is used internally, so DIMACS code is transparent to the user.

The class RawSolution provides a representation of solutions which are raw results from the SAT solver with all variable parameters from the unfolder, and consequently not easily readable. In addition to the solution in DIMACS form (including values for auxiliary variables), a RawSolution object registers data which permit information extraction from these raw solutions. The most important methods are:

• frontier_pos_and_neg_values:

  Which extracts the frontier values from the solution. These values are in DIMACS code.

• extract_activated_frontier_values():

  Extracts frontier variables which are active in solution.

• extract_act_input_clock_seq():

  Extract the sequence of activated inputs and events in the solution.

In models of signal propagation, we are more interested in frontier solutions. The following method is then well adapted: sq_frontier_solutions(), because it returns FrontierSolutions.

Parameters:

• query (<MCLSimpleQuery>) – Query.
• max_step (<int>) – Number of steps allowed in the unfolding; the horizon on which the properties must be satisfied
• vvars (<list <int>>) – Variables for which solutions must differ. In practice, it is a list with the values (Dimacs code) of all frontier places of the system.

Key max_user_step:  

(Optional) See __mac_exhaustive_search().

Returns:

a list of RawSolutions from the solver

Return type:

<list <RawSolution>>

Warning

no_frontier places are initialized to False in simple queries except if initial condition.

Warning

if the query includes variant constraints, the horizon (max_step) is automatically adjusted to min(max_step, len(variant_constraints)).

Query

Query internal representation

class cadbiom.models.clause_constraints.mcl.MCLQuery.MCLSimpleQuery(start_prop, inv_prop, final_prop, variant_prop=[])

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

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:

param start_prop:  

start property; logical formulas

param inv_prop:

invariant property; logical formulas

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:

['', '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:

[[[16], [16]], [[22], [22]]]

param steps_before_check:  

Number of shifts before testing the final property - optional

type start_prop:  

<str>

type inv_prop:

<str>

type final_prop:  

<str>

type variant_prop:  

<list <str>>

type dim_start:

<list <DClause>>, default []

type dim_inv:

<list <DClause>>, default []

type dim_final:

<list <DClause>>, default []

type dim_variant:  

<list <list <DClause>>

type steps_before_check:  

<int>, default value 0

NB: DClause: A clause coded as a list of DIMACS coded literals: <list <int>>

classmethod from_frontier_sol(f_sol)

Build a query from a frontier solution

Start property is based on activated frontiers.

All frontiers that are not in activated_frontier ARE NOT forced to be inactivated with a negative value.

Variant property enforces same timing on activated events, and the others are free.

@param f_sol: FrontierSolution (human readable solution) @param unfolder: current unfolder

classmethod from_frontier_sol_new_timing(f_sol, unfolder)

Build a query from a frontier solution

Start property is based on activated frontiers.

Search all frontiers that are not in activated_frontier and force their inactivation with a negative value.

Variant property enforces new timing

@param f_sol: FrontierSolution (human readable solution) @param unfolder: unfolder

classmethod from_frontier_sol_same_timing(f_sol, unfolder)

Build a query from a frontier solution

Start property is based on activated frontiers.

Search all frontiers that are not in activated_frontier and force their inactivation with a negative value.

Variant property enforces same timing on activated events, and the others are free.

@param f_sol: FrontierSolution (human readable solution) @param unfolder: current unfolder

merge(query)

Return a new query which is a merge of two queries into one.

• start, invariant and final properties are merged.
• If both queries have variant properties, they must be on the same horizon (number of steps).
• steps before reach is set to zero.
• dim properties are also merged: dim_start, dim_inv, dim_final

Parameters:query – a MCLSimpleQuery Raises:MCLException If the queries have variant properties with different horizons (nb of steps).

Solutions representation

Classes used to store solver answers.

RawSolution:

Contain a solution got from SAT solver with all variable parameters from the unfolder.

DimacsFrontierSol:

A numerical representation of frontier values and timings from a raw solution.

FrontierSolution:

Provides is a wrapper for a symbolic representation (human readable) of activated frontiers defined in RawSolution and DimacsFrontierSol objects.

class cadbiom.models.clause_constraints.mcl.MCLSolutions.DimacsFrontierSol(raw_sol)

Class for solution frontier and timings representation

DimacsFrontierSol is a numerical representation of frontier values and timings from a raw solution.

Attributes:

param frontier_values:  

Frontier values from the solution. These values are in DIMACS code. This attribute is immutable. Based on the initial RawSolution.

param ic_sequence:  

Sequence of activated inputs and events in the solution. Only used in FrontierSolution.from_dimacs_front_sol() (at the end of the search process for the cast into FrontierSolution) and for tests. Based on the initial RawSolution.

param current_step:  

The number of steps allowed in the unfolding; the current_step on which the properties must be satisfied (never used) Based on the initial RawSolution.

param nb_activated_frontiers:  

Number of activated places in the current Dimacs solution. This attribute is precomputed because it is used intensively and multiple times for each object in:

• MCLAnalyser.less_activated_solution
• MCLAnalyser.__prune_frontier_solution
• MCLAnalyser.__mac_exhaustive_search

param activated_frontier_values:  

Values of activated frontier places in the current Dimacs solution. Convenient attribute used:

• by FrontierSolution.from_dimacs_front_sol()
• to accelerate the call of self.nb_activated_frontiers
• as a criterion of uniqueness, to do set operations

type frontier_values:  

<frozenset <int>>

type ic_sequence:  

<list <list <int>>>

type current_step:  

<int>

type nb_activated_frontiers:  

<int>

type activated_frontier_values:  

<frozenset <int>>

classmethod get_unique_dimacs_front_sols_from_raw_sols(raw_sols)

Get a tuple of DimacsFrontierSols from a list of RawSolutions.

The conversion extracts keeps only frontier values from RawSolutions. This functions eliminates the duplicates.

Cf TestMCLAnalyser.py:523:

raw_sols len 6 tpl len: 6

TestMCLAnalyser.py:559

raw_sols len 12: tpl len: 7

TestMCLAnalyser.py:667

raw_sols len 7: tpl len: 1

TestMCLAnalyser.py:700

raw_sols len 7 tpl len: 1

..note:: We need to index the result in MCLAnalyser.less_activated_solution()

thus, this why we return a tuple here.

..note:: The tuple of DimacsFrontierSols is not sorted by order of calculation.

Thus, the first item is not the first solution found. TODO: An order could be used to adjust the number of solutions asked during the pruning operation in __solve_with_inact_fsolution()

Parameters:raw_sols (<list <RawSolution>>) – List of raw solutions; most of the time obtained with sq_solutions() Returns:Set of DimacsFrontierSol Return type:<tuple <DimacsFrontierSol>>

get_var_name(var_num)

For translation to symbolic representation Return the string that corresponds to he name of the variable value. :rtype: <str>

ic_sequence

Sequence of activated inputs and events (clocks) in the solution.

(may be empty if data-flow model is without input)

See also

RawSolution.extract_act_input_clock_seq()

Note

Only used in FrontierSolution.from_dimacs_front_sol() (at the end of the search process for the cast into FrontierSolution) and for tests. => This step is expensive !

nb_timed()

Count the number of events in the current Dimacs solution (not used) :rtype: <int>

class cadbiom.models.clause_constraints.mcl.MCLSolutions.FrontierSolution(activated_frontiers, ic_sequence, current_step)

Class for symbolic (human readable) frontiers and timings representation

The class FrontierSolution provides is a wrapper for a symbolic representation (human readable) of activated frontiers defined in RawSolution and DimacsFrontierSol objects.

Attributes:

• The main attributes are activated_frontier which is a set of (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.
• current_step is the number of steps used during the unfolding that made 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.

Todo

• Faire une super classe dont héritent RawSolution et DimacsFrontierSol pour éviter la duplication de code et le stockage d’attributs qu’on connait déjà dans les types de plus bas niveaux…
• … Ou détecter le type d’objet dans le constructeur => ducktyping
• renommer l’attr activated_frontier en activated_frontiers

classmethod build_input_clock_sequence(get_var_name, ic_sequence)

Get strings representing timings of each step in the solution.

Parameters:

• get_var_name (<function>) – Method to call for a conversion of values to names. (binding of the method get_var_name() of an unfolder).
• ic_sequence (<tuple <tuple <int>>) –
  • Each tuple is the state of literals in a step of the solution.
  • Each literal in the tuple is an activated variable in a step.
  • Variables are inputs or events (free clocks) ONLY!

Returns:

List of strings representing timings of each step in ic_sequence.

Return type:

<list <str>>

classmethod from_dimacs_front_sol(dimacs_front_sol)

Build FrontierSolution object, a symbolic representation of frontier values and timings from a DimacsFrontierSolution solution.

• Convert activated frontiers values to places names (strings)
• Extract inputs and clocks sequence (steps of the whole solution)

classmethod from_file(file_name)

Build a symbolic representation of frontier values and timing from a DimacsFrontierSolution solution

..warning:: This method can only be used if the file contains 1 solution…

Note: use cadbiom_cmd/tools/solutions.py functions to reload frontiers

classmethod from_raw(raw_sol)

Build FrontierSolution object, a symbolic representation of frontier values and timings from a RawSolution solution.

• Extract activated frontiers values (literals)
• Convert activated frontiers values to places names (strings)
• Extract inputs and clocks sequence (steps of the whole solution)

save(outfile, only_macs=False)

Save a symbolic solution in a file The format is readable by the simulator and all Cadbiom tools.

Note

Frontiers are sorted in (lower case) alphabetical order.

Parameters:

• outfile (<open file>) – Writable file handler
• only_macs (<boolean>) – Write only frontiers, and skip timings.

sorted_activated_frontier

Sort activated places in alphanumeric order.

Intended to facilitate readability and debugging.

Returns:List of sorted places Return type:<list <str>>

exception cadbiom.models.clause_constraints.mcl.MCLSolutions.MCLException(mess)

Exception for MCLAnalyser

class cadbiom.models.clause_constraints.mcl.MCLSolutions.RawSolution(solution, unfolder)

RawSolution objects contain a solution got from SAT solver with all variable parameters from the unfolder.

The class RawSolution provides a representation of solutions which are raw results from the SAT solver with all variable parameters from the unfolder, and consequently not easily readable.

In addition to the solution in DIMACS form (including values for auxiliary variables), a RawSolution object registers data which permit information extraction from these raw solutions. The most important methods/attributes are:

• frontier_pos_and_neg_values:

  Extracts the frontier values from the solution. These values are in DIMACS code.

• extract_activated_frontier_values():

  Extracts frontier variables which are active in solution.

• extract_act_input_clock_seq():

  Extract the sequence of activated inputs and events in the solution.

..warning:: IMPORTANT: the solution MUST correspond to the properties registered

for its computation. Any change in these properties will give incorrect results (current_step, etc.).

Attributes:

param shift_direction:  Unfolding direction param shift_step:  The shift step ss (if n is X_0 code, n+ss is X_1 code) (?) Dependant on the run. param solution:DIMACS encoding of a solution from the solver A solution is list of state vectors (tuple of literals). Each literal is a variable. ..note:: The solver returns list of solutions. param unfolder:Get the current unfolder for the solution (unfolder is used for invariant constants) param current_step:  Get current step of the unfolder (Thus the current number of steps related to the current solution and by extension the maximum of steps until now) type shift_direction:  “FORWARD” or “BACKWARD” type shift_step:  <int> type solution:<tuple <int>> type unfolder:<CLUnfolder> type current_step:  <int>

display_activ_sol()

For debug: display only activated variables (auxiliary variables are pruned)

extract_act_input_clock_seq()

Extract the sequence of activated inputs and events/free clocks in the current solution.

Note

• Each tuple is the state of literals in a step of the solution.
• Each literal in the tuple is an activated variable in a step.
• Variables are inputs or events (free clocks) ONLY!

Note

A solution is list of state vectors (list of literals).

Note

This function is called by: - FrontierSolution.from_raw() - DimacsFrontierSol.ic_sequence

Returns:list of input vector (may be empty if data-flow model is without input) Return type:<tuple <tuple <int>>>

extract_act_inputs_clocks(state_vector)

Extract active inputs and free_clocks from a state vector.

Return the intersection of all inputs and free clocks of the system with the given state vector.

PS: unfolder.inputs_and_free_clocks contains only positive values

so the intersection with state_vector allows to get only activated variables.

Used only by extract_act_input_clock_seq().

Parameters:state_vector (<list <int>>) – A state vector. A list of literals. Returns:Tuple of activated inputs and free_clocks in the given state vector. Return type:<tuple>

extract_activated_frontier_values()

Extracts frontier variables which are active in solution.

Returns:Set of activated frontier values. Return type:<frozenset>

frontier_pos_and_neg_values

Extracts the frontier values from the solution. These values are in DIMACS code.

Warning

This function returns values of active AND inactive frontiers.

Warning

Assert: solution is sorted by variable code for BACKWARD

Note

This function makes set operations between all values of frontiers and the current solution. This last one is a list of hundreds of thousands items (ex: ~500000 for a solution with 10 steps). Thus, the operation is costly and we use a decorator @cached_property to put the result in cache.

Note

Used by: - self.extract_activated_frontier_values() - DimacsFrontierSol.__init__()

Note

frontiers (fixed size): 3824 solution (increasing size): 171231, 228314, 285405, 285453, 400091 etc.

Returns:A dimacs code set of the activation state on the frontiers for the current solution. Return type:<frozenset <int>>

get_unshift_code(var_num)

Get the real value of the given variable in the system (remove the shift)

..warning:: DEPRECATED Used internally by self.unflatten()

@param var_num: DIMACS literal coding of a shifted variable x_i @return: DIMACS literal coding of x_0 with same value :return: <int>

get_var_name(var_num)

For translation to symbolic representation Return the name of a variable with its value.

unflatten()

Extract trajectories from the current solution

Transform a flat DIMACS representation of a trajectory into a <list <list <int>>>. Each sublist represents a state vector (the state of all variables of the system for 1 step in the trajectory).

..note:: This assertion seems to be not true:

Auxiliary variables introduced by properties compiling are ignored. => there are lots of variables on the format “_name”…

..note:: Debug with:

>>> raw_sol = RawSolution()
>>> print(raw_sol)

..note:: The list returns all variables of the system including

inputs, clocks, auxiliary variables.

Returns:A list of state vectors (<list <int>>) in DIMACS format Return type:<list <list <int>>>

Tests

CLUnfolder

Unitary Test of the unfolder

Test forward initialization for various models and properties types

Pytest call:

pytest cadbiom/models/clause_constraints/mcl/TestCLUnfolder.py::test_init_forward

Query attributes:

self.dim_start = [] # list<DClause> self.dim_inv = [] # list<DClause> self.dim_final = [] # list<DClause> self.dim_variant = [] # list<list<DClause>>

CLUnfolder attributes that contain query attributes:

self.__initial_property = None # logical formula - literal boolean expression self.__dimacs_initial = None # list of DIMACS clauses self.__final_property = None # logical formula self.__dimacs_final = None # list of DIMACS clauses self.__invariant_property = None # logical formula self.__dimacs_invariant = None # list of DIMACS clauses self.__variant_property = None # list<logic formulas> self.__dimacs_variant = None # list<list<DIMACS clauses>>

CLUnfolder attributes that contain clauses:

self.__precomputed_variant_constraints = None # list<list<DIMACS clauses>> dynamic_constraints initial_constraints invariant_constraints variant_constraints final_constraints

Note

Mangling prefix for protected attributes: unfolder._CLUnfolder__*

Example to get a mapping of numeric clauses to str clauses:  

mappings = [[unfolder.get_var_name(value) for value in clause]

for clause in dynamic_constraints[0]]

class cadbiom.models.clause_constraints.mcl.TestCLUnfolder.ErrorReporter

error reporter of the compil type

display(mess)

just printing

display_info(mess)

just printing

set_context(cont)

for transition compiling

class cadbiom.models.clause_constraints.mcl.TestCLUnfolder.TestCLUnfolder(methodName='runTest')

Test public and some private methods (test_method form)

test_free_clocks_inputs()

test on free clocks and input computation

test_frontier()

Test frontier computation and encoding

test_var_name()

Test of variables at initial state uncoding and decoding

cadbiom.models.clause_constraints.mcl.TestCLUnfolder.create_unfolder(model)

Return an unfolder for the given model

cadbiom.models.clause_constraints.mcl.TestCLUnfolder.feed_mclanalyser(*args, **kwargs)

Setup MCLAnalyser with a bcx model

15 places: A, B, C, D, E, F, G, H, I, J, K, L, M, N, P 8 clocks: _h2, _h3, _h4, _h5, _h6, _h7, _h_0, _h_1 Frontiers: D, E, F, G, I, L, N

cadbiom.models.clause_constraints.mcl.TestCLUnfolder.init_forward_unfolding_part_1(unfolder)

Initialization step only

cadbiom.models.clause_constraints.mcl.TestCLUnfolder.init_forward_unfolding_part_2(unfolder)

Shift step only

cadbiom.models.clause_constraints.mcl.TestCLUnfolder.init_forward_unfolding_solution_1(mcla, dimacs_check=True)

• Test first part of init_forward_unfolding: init of constraints
• Test second part of init_forward_unfolding: shift of initialized constraints

Query:

start, invariant, final: ("M", "L", "C")
No solution (because inhibitor M is activated)

Key dimacs_check:  

(Optional) Boolean used to check expected initial constraints. For now, only literals in textual properties are removed from the CLUnfolder __no_frontier_init variable. DIMACS literals are not filtered and could lead to falsely unsatisfactory problems.

See also

test_init_forward_unfolding_solution_1_dimacs()

cadbiom.models.clause_constraints.mcl.TestCLUnfolder.init_forward_unfolding_solution_2(mcla)

• Test first part of init_forward_unfolding: init of constraints
• Test second part of init_forward_unfolding: shift of initialized constraints

Query:

start, invariant, final: ("", "L", "C and K")
Solution: D E F I L

cadbiom.models.clause_constraints.mcl.TestCLUnfolder.init_forward_unfolding_solution_3(mcla, dimacs_check=True)

• Test first part of init_forward_unfolding: init of constraints
• Test second part of init_forward_unfolding: shift of initialized constraints

Query:

start, invariant, final: Union of textual and DIMACS properties:
    ("", "L", "C and K") => [], [[12]], [[3, -47], [11, -47], [-3, -11, 47], [47]]
    [[13]], [[12]], [[3]] <= ("M", "L", "C")
No solution

Todo

This test contains some stupid results from the generator of clauses.

=> clauses redondantes en cas d’égalité des events entre l’attribut au format texte et celui au format DIMACS. (invariant_constraints)

Key dimacs_check:  

(Optional) Boolean used to check expected initial constraints. For now, only literals in textual properties are removed from the CLUnfolder __no_frontier_init variable. DIMACS literals are not filtered and could lead to falsely unsatisfactory problems.

See also

test_init_forward_unfolding_solution_3()

cadbiom.models.clause_constraints.mcl.TestCLUnfolder.init_forward_unfolding_solution_4(mcla)

• Test first part of init_forward_unfolding: init of constraints
• Test second part of init_forward_unfolding: shift of initialized constraints

Query:

start, invariant, final: ("", "", "C")
Solutions: F E L D, D E F I

cadbiom.models.clause_constraints.mcl.TestCLUnfolder.model1()

A simple ChartModel with two nodes and a transition

cadbiom.models.clause_constraints.mcl.TestCLUnfolder.model2()

ChartModel model1 + 3 nodes and 2 transitions and a cycle without start

cadbiom.models.clause_constraints.mcl.TestCLUnfolder.model3()

ChartModel model2 + 1 node + 1 start node and a transition

cadbiom.models.clause_constraints.mcl.TestCLUnfolder.model4()

ChartModel with:

• 1 input node: in1
• 5 nodes: n1, n2, n3, n4, n5
• 5 transitions: n1-n2, n3-n4, n4-n5, n5-n3, in1-n1
• 2 free clocks: hh1: (n3 or n4) on n1-n2, hh2: (n1 and n3) on n4-n5

cadbiom.models.clause_constraints.mcl.TestCLUnfolder.numeric_properties(*args, **kwargs)

start, invariant, final properties in DIMACS form

cadbiom.models.clause_constraints.mcl.TestCLUnfolder.test_init_forward_unfolding_solution_1_dimacs(feed_mclanalyser, numeric_properties)

Query:

dim_start, dim_inv, dim_final = [[13]], [[12]], [[3]]
DIMACS equiv of: start, invariant, final: ("M", "L", "C"):
No solution (because inhibitor M is activated)

Note

Actuellement, pas de solution à cause de initial_constraints qui contient 2 clauses contraires: [-13] et [13]. En effet, les valeurs DIMACS ne sont pas controlées contrairement aux propriétés textuelles. M en tant que start place n’est donc pas retiré de la liste des places non frontières (__no_frontier_init). Ex: [[-1], [-2], [-3], [-8], [-10], [-11], [-13], [-15], [13]]

cadbiom.models.clause_constraints.mcl.TestCLUnfolder.test_init_forward_unfolding_solution_1_text(feed_mclanalyser, textual_properties)

Query:

start, invariant, final: ("M", "L", "C")
No solution (because inhibitor M is activated)

cadbiom.models.clause_constraints.mcl.TestCLUnfolder.test_init_forward_unfolding_solution_2_dimacs(feed_mclanalyser, numeric_properties)

Query:

dim_start, dim_inv, dim_final = [], [[12]], [[3, -47], [11, -47], [-3, -11, 47], [47]]
DIMACS equiv of: start, invariant, final: ("", "L", "C and K")
Solution: D E F I L

cadbiom.models.clause_constraints.mcl.TestCLUnfolder.test_init_forward_unfolding_solution_2_text(feed_mclanalyser, textual_properties)

Query:

start, invariant, final: ("", "L", "C and K")
Solution: D E F I L

cadbiom.models.clause_constraints.mcl.TestCLUnfolder.test_init_forward_unfolding_solution_3(feed_mclanalyser, textual_properties, numeric_properties)

Query:

start, invariant, final: Union of textual and DIMACS properties:
    ("", "L", "C and K") => [], [[12]], [[3, -47], [11, -47], [-3, -11, 47], [47]]
    [[13]], [[12]], [[3]] <= ("M", "L", "C")
No solution

Note

Actuellement, pas de solution à cause de initial_constraints qui contient 2 clauses contraires: [-13] et [13]. En effet, les valeurs DIMACS ne sont pas controlées contrairement aux propriétés textuelles. M en tant que start place n’est donc pas retiré de la liste des places non frontières (__no_frontier_init). Ex: [[-1], [-2], [-3], [-8], [-10], [-11], [-13], [-15], [13]]

cadbiom.models.clause_constraints.mcl.TestCLUnfolder.test_init_forward_unfolding_solution_4(feed_mclanalyser, textual_properties)

Query:

start, invariant, final: ("", "", "C")
Solutions: D E F L, D E F I

cadbiom.models.clause_constraints.mcl.TestCLUnfolder.test_init_forward_unfolding_solution_5(feed_mclanalyser)

Test variant_prop, dim_variant attributes of a query and their solutions

Query:

variant text: ["_h4 and _h2 and _h3", "_h5", "_h_0"]
variant DIMACS: [[[18], [16], [17]], [[19]], [[22]]]
Solution: D E I (not D E F I)

variant text: ["_h4 and _h2 and _h3", "_h5 and _h7", "_h_0"]
variant DIMACS: [[[18], [16], [17]], [[19], [21]], [[22]]]
Solution: D E G I
Note: 2 events on the second step (test the correct parsing)

cadbiom.models.clause_constraints.mcl.TestCLUnfolder.test_init_forward_unfolding_variant_constraints(feed_mclanalyser)

Test variant_prop and dim_variant attributes of a query

Note

No solution is tested here. If you do that, do not forget to reset dim_start attribute of the query before reusing with MCLA.mac_search(). This attr contains the banished previous solutions.

Todo

This test contains some stupid results from the generator of clauses.

=> clauses redondantes en cas d’égalité des events dans 1 formule (Ex: “h2 and h2”)

=> clauses redondantes en cas d’égalité des events entre l’attribut au format texte et celui au format DIMACS.

=> On peut mettre n’importe quel nom d’event, aucun test n’est fait pour vérifier qu’il existe dans le modèle.

cadbiom.models.clause_constraints.mcl.TestCLUnfolder.test_shift(feed_mclanalyser, textual_properties)

Test shift of constraints during the solutions search

cadbiom.models.clause_constraints.mcl.TestCLUnfolder.textual_properties(*args, **kwargs)

start, invariant, final properties in textual form

MCLAnalyser

Unitary Tests for the MCLAnalyser

class cadbiom.models.clause_constraints.mcl.TestMCLAnalyser.ErrorRep

error reporter of the compil type

display(mess)

just printing

display_info(mess)

just printing

set_context(cont)

for transition compiling

class cadbiom.models.clause_constraints.mcl.TestMCLAnalyser.TestMCLAnaLyzer(methodName='runTest')

Unit tests for MCLAnalyser class

test_delay1()

simple delay computation

test_delay1_w_ic()

Simple delay computation with clock sequence

First test: f_prop = “C4” # old solver [[], [], [3], []] [[-1, -2, -3, 4, -5, -6, -7, -8, -9, -10, -11, -12, 13, -14, -15, 16], [-1, -2, -3, -4, -5, -6, 7, -8, -9, -10, -11, 12, -13, -14, -15, 16], [-1, -2, 3, -4, -5, 6, -7, -8, -9, -10, -11, 12, -13, 14, -15, 16], #3>0 free clocks: (3, ‘:’, ‘h2’) [1, -2, -3, -4, -5, -6, -7, 8, 9, -10, 11, 12, -13, -14, -15, -16]] [‘A1’, ‘C1’, ‘B1’] [‘A2’, ‘C2’, ‘B1’] [‘h2’, ‘A3’, ‘C2’, ‘_lit0’, ‘B1’] # activated clock: h2 [‘_lit2’, ‘A4’, ‘B2’, ‘_lit3’, ‘C2’]

[[], [], [], []] [[-1, -2, -3, 4, -5, -6, -7, -8, -9, -10, -11, -12, 13, -14, -15, -16], [-1, -2, -3, -4, -5, -6, 7, -8, -9, -10, -11, 12, -13, -14, -15, -16], [-1, -2, -3, -4, -5, 6, -7, -8, -9, -10, -11, 12, -13, -14, -15, -16], [1, -2, -3, -4, -5, -6, -7, 8, -9, -10, 11, 12, -13, -14, -15, -16]] [‘A1’, ‘C1’] [‘A2’, ‘C2’] [‘A3’, ‘C2’] [‘_lit2’, ‘A4’, ‘_lit3’, ‘C2’]

# new solver (no clock used => better solution): [[], [], [], []] [[-1, -2, -3, 4, -5, -6, -7, -8, -9, -10, -11, -12, 13, -14, -15, -16], [-1, -2, -3, -4, -5, -6, 7, -8, -9, -10, -11, 12, -13, -14, -15, -16], [-1, -2, -3, -4, -5, 6, -7, -8, -9, -10, -11, 12, -13, -14, -15, -16], [1, -2, -3, -4, -5, -6, -7, 8, -9, -10, 11, 12, -13, -14, -15, -16]] [‘A1’, ‘C1’] [‘A2’, ‘C2’] [‘A3’, ‘C2’] [‘_lit2’, ‘A4’, ‘_lit3’, ‘C2’]

[[], [], [], []] [[-1, -2, -3, 4, -5, -6, -7, -8, -9, -10, -11, -12, 13, -14, -15, 16], [-1, -2, -3, -4, -5, -6, 7, -8, -9, -10, -11, 12, -13, -14, -15, 16], [-1, -2, -3, -4, -5, 6, -7, -8, -9, -10, -11, 12, -13, -14, -15, 16], [1, -2, -3, -4, -5, -6, -7, 8, -9, -10, 11, 12, -13, -14, -15, 16]] [‘A1’, ‘C1’, ‘B1’] [‘A2’, ‘C2’, ‘B1’] [‘A3’, ‘C2’, ‘B1’] [‘_lit2’, ‘A4’, ‘_lit3’, ‘C2’, ‘B1’]

Note

Debugging of solutions - help:

for i, sol in enumerate(lsol, 1):
    print("Sol", i)
    # [[], [], [], []]
    print(sol.extract_act_input_clock_seq())
    # [[....], [....], [....], [....]]
    print(x.unflatten())

    # Convert literal values to str, display only activated ones (val > 0)
    for step in sol.unflatten():
        print([sol.unfolder.get_var_name(val) for val in step if val > 0])

test_dimacs_frontier_ban()

Ban previous solution and try to get a new different one

test_input1()

simple input computation

test_lit_sol_equal()

Test the test helper function

test_load1()

Load from a bcx file

test_load2()

Load from a cadlang file

test_load3()

Load from a PID file

test_mac_clock()

mac with clocks

test_mac_delay_save()

Test save on the delay example

x_file content:

A1 B1 C1

% % h2 % %

test_mac_inhibitor()

test [A1, B1, C1] not strong activator, D is a strong inhibitor

test_mac_no_clock()

test mac without clocks

test_mcl_query_merge()

Test zone for some MCLSimpleQuery merge functions used in MCLAnalyser.is_strong_activator()

test_solution_pruning()

Pruning a solution by trying to get a new solution with a smaller number of active frontier places

test_unflatten()

Test unflatten trajectory

test_valid_simul_delay()

Test simulation of the delay example

test_valid_simul_input()

Test simulation of the input example

cadbiom.models.clause_constraints.mcl.TestMCLAnalyser.lit_sol_equal(sol1, sol2)

@param sol1,sol2: list<list<string>>

cadbiom.models.clause_constraints.mcl.TestMCLAnalyser.lit_subsol_equal(ssol1, ssol2)

@param ssol1,ssol2: list<string> CAREFULL: change order in lists

MCLTranslators

Unitary tests for the translators

class cadbiom.models.clause_constraints.mcl.TestMCLTranslators.ErrorRep

Simple error reporter

display(mess)

set error and print

class cadbiom.models.clause_constraints.mcl.TestMCLTranslators.TestFull(methodName='runTest')

test full models

test_antlr_optimization()

Optimization gain comparison when using MCLTranslator optimizations for ANTLR translation (subexpression elimination)

Note

Use test file instead of not provided: “../ucl/examples/test_tgfb_ref_300511.bcx”

test_constraints()

As it says

test_model1()

n1 –> n2; h1[not n4] n1 –> n3; h2[] n4 –> n1; h3[]

test_model2()

n1 –> n2; h1 when n2 default h2[not n4] n1 –> n3; h2 when n4[] n4 –> n1; h3[]

test_model3()

testInputCondEvent n4; n1/p –> n2; h[n4];

class cadbiom.models.clause_constraints.mcl.TestMCLTranslators.TestMCLSigExprVisitor(methodName='runTest')

Test of signal expression

test_bin1()

X or Y

test_bin2()

X and Y

test_bin3()

h1 default h2

test_bin4()

h1 when (a or b)

test_cse1()

common subexpression elimination h1 when (a or b) default h2 when (b or a)

test_cse2()

common subexpression elimination h1 when (a or b) default h2 when (b or a)

test_ident1()

sigexp = xx

class cadbiom.models.clause_constraints.mcl.TestMCLTranslators.TestTransitionClauses(methodName='runTest')

Test of transitions into clauses

test_cond()

n1 –> n2; [not n3]

test_cond_event()

n1 –> n2; h[not n3]

test_input_cond_event()

n4/i; n1/i –> n2; h[n4];

test_no_cond()

n1 –> n2; []

test_no_cond_event()

n1 –> n2; h[]

test_no_cond_event_default()

testNoCondEventWhen1 n1 –> n2; h1 when c1 default h2[c3]

test_no_cond_event_when1()

n1 –> n2; h when n3[] n3;

test_no_cond_event_when2()

n1 –> n2; h when n3[] n3 –> n1 ; h2 when h[] Error h is not a state

test_no_cond_event_when3()

n1 –> n2; h when n3[] n3 –> n1 ; n2 when n1[] Error n2 is not a clock

test_perm_cond_event()

n4; n1/p –> n2; h[n4];

test_perm_no_cond_event()

n1/p –> n2; h[];

class cadbiom.models.clause_constraints.mcl.TestMCLTranslators.TestTransitionList(methodName='runTest')

As it says

test_no_cond_on_out2events()

n1 –> n2; h1[not n4] n1 –> n3; h2[] n4 –> n1; h3[] gen_transition_list_clock tested

test_simple()

n1 –> n2; h1[not n4] n1 –> n3; h2[] n4 –> n1; h3[]

test_simple_in_no_out()

n2 –> n1; h1[not n4] n4 –> n1; h3[]

test_simple_no_trans()

n1;

test_simple_out_no_in()

n1 –> n2; h1[not n4] n1 –> n3; h2[]

test_very_simple()

n1 –> n2; []

Models

Chart model

Classes of nodes, transitions and model for representing a guarded transition model

Classes available and their inheritance relationships:

• ChartModel: Model of a chart
• CTransition
• CNode
  • CStartNode
    • CTrapNode
  • CSimpleNode
    • CPermNode
    • CInputNode
    • CMacroNode
      • CTopNode

class cadbiom.models.guard_transitions.chart_model.CInputNode(xcoord, ycoord, name, model, **kwargs)

An input node cannot have an in-transition

draw(view, xfr, yfr, wfr, hfr, depth)

special drawing for diamond

find_element(mox, moy, dstyle, w_coef, h_coef)

Simple node - No handle

get_center_loc_coord(dstyle, w_ratio, h_ratio)

Returns center coordinate in surrounding node

intersect(node2, dstyle, nb_trans, w_ratio, h_ratio)

An input node can be the origin of some transition to a node. One transition by node.

move(v_dx, v_dy, v_size, top_node)

Move the node - mx_virt, my virt are virtual coordinates of the mouse click_loc is the location of the clic in node’s frame

class cadbiom.models.guard_transitions.chart_model.CMacroNode(xcoord, ycoord, width, height, name, model, **kwargs)

Main building block for charts

Quick note::

new_transitions attribute is a defaultdict(list) which allow to get all transitions related to a couple of nodes. In theory there is only 1 transition for each couple of nodes (cf. :meth:add_transition).

transitions attribute is a binding over values of new_transitions (so it is read-only!).

So, every CMacroNode and CTopNode contain all transitions involving nodes that they contain.

accept(visitor)

Standard visitor acceptor

add_copy(node)

add a node of the same type

add_input_node(name, xcoord, ycoord)

Add input node

add_macro_subnode(name, xcoord, ycoord, width, height)

Add a macro node as subnode with dimensions

add_perm_node(name, xcoord, ycoord)

Add a perm node

add_simple_node(name, xcoord, ycoord)

Add a simple node

add_start_node(xcoord, ycoord, name=None)

Add a start node

add_start_trap_node(node, name)

Add a start or trape node to he model

Handy function called by add_start_node, add_trap_node

add_transition(ori, ext)

Add a transition to the model

Note

Reflexive transitions are not authorized. Duplications of transitions are not authorized. BUT! Not exception is raised in these cases. Have fun <3

Parameters:

• ori – a simple node
• ext – a simple node

Returns:

A new transition or None if the couple of nodes was not valid.

Return type:

<CTransition> or None

add_trap_node(xcoord, ycoord, name=None)

Add a trap node

build_new_transition_to_nodes(transitions_group, ori, ext)

Handle a new transition: build and attach it to the model

Parameters:

• arg1 (<list <CTransition>>) – List of transitions that concern the given couple of nodes The list should not exceed 2 elements (see add_transition())
• arg2 (<Node>) – Node
• arg3 (<Node>) – Node

clean_code()

clean the code

copy(model=None)

Duplicate a macronode - performs a deep copy

copy_subnodes(child_node, model=None)

Copy current subnodes to the child node

copy_transitions(child_node)

Copy current transitions to the child node

TODO: méthode alternative de copie d’un noeud complexe: itérer sur les transitions du noeud courant et créer les subnodes du child_node en conséquence => pas de création des subnodes en amont => pas besoin de rechercher les nodes d’après leurs coordonnées avec _find_in_subnodes (méthode hasardeuse en cas de nombreux noeuds empilés les uns sur les autres => la méthode a du mal à retrouver le bon noeud et peut créer des transitions incorrectes)

draw(view, xfr, yfr, wfr, hfr, depth)

Draw transitions and nodes contained in this MacroNode

@param view: drawing area @param xfr: x coordinate of father in virtual screen @param yfr: y - @param wfr: father’s width in virtual screen @param hfr: father’s height in virtual @param depth: depth of the node; less than depth_max

find_element(mox, moy, dstyle, w_coef, h_coef)

@param mox, moy: mouse coordinate in container frame @param dstyle: drawing style @param w_coef, h_coef: affinity ratios for view -> container frame

find_transition(mox, moy, dstyle, w_coef, h_coef)

Look for transitions pointed by mouse No recursive search - transitions are in current node

get_center_loc_coord(dstyle, w_ratio, h_ratio)

Returns center coordinate in surrounding node (father)

intersect(node2, dstyle, nb_trans, w_ratio, h_ratio)

Gives the the first point where to branch a transition, the gap between two arrows and a boolean horizontal true if arrows start from horizontal edge @param node2: second node of the transition @param dstyle: drawing style @param nb_trans: number of transitions to be drawn @param w_ratio,h_ratio: dimentions of the screen for fixed size nodes

is_for_extremity()

Legitimate transition extremity

is_for_origin()

Legitimate transition origin

move(v_dx, v_dy, v_size, top_node)

Move the node - mx_virt, my virt are virtual coordinates of the mouse click_loc (pair) is the location of the clic in node’s frame

remove()

Remove this node and its sub-nodes from the model

resize(mx_virt, my_virt, handle, screen_w, screen_h, top_node)

Resize the node with the mouse

@param mx_virt, my_virt: mouse coordinates in virtual window @param handle: as determined by find_node @param screen_w, screen_h: size of the screen in pixels @param top_node: root node of the sub model

self_to_virtual_frame(xcoord, ycoord, top_node)

Coordinate change

set_model(model)

Set the model for a subtree of nodes - used for copy/paste from one model to another

transitions

Compatibility code

Note

The old API uses this attribute as a list<list<CTransitions>>. Sublists are transitions with common extremities.

Returns:An iterator over the values of self.new_transitions. Similar to: <list <list <CTransitions>>> Return type:<dictionary-valueiterator>

v_affinity_coef(top_node)

Affinity ratios cw,ch: local_horizontal_length = screen_horizontal_length * cw Similar relation for vertical length. @param top_node: root of the sub_model

virt_to_self_frame(xcoord, ycoord, s_width, s_height, top_node)

xcoord,ycoord must be virtual coordinates result is the coordinates of (x,y) in self frame @param xcoord, ycoord: coordinate in virtual window (screen -> 1.0 x 1.0 window) @param s_width, s_height: screen dimensions @param top_node: root of the sub_model

class cadbiom.models.guard_transitions.chart_model.CNode(x_coord, y_coord, model, note=u'')

Abstract node class for guarded transition models Base class for model components

Parameters:

• father (None or <CNode>) – Parent node. All nodes are aware of their parent node. Most of the time it is the CTopNode; but this can differ for nodes in CMacroNodes. Such “Complex” nodes can be used to build a linked list of nodes since they also contain a list of subnodes.
• search_mark (<boolean>) – This flag is used to change the color of selected nodes with a search from the list of simple/frontier nodes or from search entry of the GUI. .. seealso:: drawing_style()
• selected (<boolean>) – This flag is used to change the color of mouse selected nodes .. seealso:: drawing_style()

clean()

Abstract

find_element(mox, moy, dstyle)

The mouse coordinates must be in the same frame than nodes coordinates

get_coordinates()

As it says

is_input()

As it says

is_macro()

As it says

is_perm()

As it says

is_simple()

As it says

is_start()

As it says

is_top_node()

As it says

is_trap()

As it says

remove()

Remove this node from:

• its model
• its father’s transitions

Warning

assume it is not a TopNode nor a MacroNode

set_layout_coordinates(x_coord, y_coord)

As it says

set_model(model)

As it says

set_name(name)

As it says

class cadbiom.models.guard_transitions.chart_model.CPermNode(xcoord, ycoord, name, model, **kwargs)

permanent node are never unactivated

draw(view, xfr, yfr, wfr, hfr, depth)

depth is less than depth_max @param xfr, yfr: coordinates of father node (reference frame) in view @param wfr,hfr: width and height of father node in view (affinity ratios)

class cadbiom.models.guard_transitions.chart_model.CSimpleNode(xcoord, ycoord, name, model, **kwargs)

A simple node cannot have sub nodes Simple nodes have constant screen dimensions

accept(visitor)

standard visitor acceptor

copy(model=None)

As says

draw(view, xfr, yfr, wfr, hfr, depth)

depth is less than depth_max @param xfr: x coordinate of father in view screen @param yfr: y coordinate of father in view screen @param wfr: width of father in virtual screen @param hfr: height of father in virtual screen

find_element(mox, moy, dstyle, w_coef, h_coef)

Simple node - No handle

get_center_loc_coord(dstyle, w_ratio, h_ratio)

Returns center coordinate in surrounding node

intersect(node2, dstyle, nb_trans, w_ratio, h_ratio)

Gives the the first point where to branch a transition, the gap between two arrows and a boolean horizontal true if arrows start from horizontal edge Assume wloc and hloc computed (node drawn) - coordinates in container frame

@param node2: second node of the transition @param dstyle: drawing style @param nb_trans: number of transitions to be drawn @param w_ratio, h_ratio: dimentions of the screen for fixed size nodes

is_for_extremity()

Can be used as transition extremity

is_for_origin()

Can be used as transition origin

move(v_dx, v_dy, v_size, top_node)

Move the node - mx_virt, my virt are virtual coordinates of the mouse click_loc is the location of the clic in node’s frame

set_name(name)

Rename the current node; update simple_node_dict attr of the model

class cadbiom.models.guard_transitions.chart_model.CStartNode(x_coord, y_coord, model, **kwargs)

Start node show macro-states initialisation

accept(visitor)

Generic visitor acceptor

copy(model=None)

As says

draw(view, xfr, yfr, wfr, hfr, depth)

depth is less than depth_max

find_element(mox, moy, dstyle, w_coef, h_coef)

No handle

get_center_loc_coord(dstyle, w_ratio, h_ratio)

@param dstyle: drawing style (not used here) @param w_ratio,h_ratio: affinity ratios for virtual screen (not used here)

Returns center coordinate in surrounding node - here node coordinates

intersect(node2, dstyle, nb_trans, w_ratio, h_ratio)

@param dstyle: drawing style @param w_ratio, h_ratio: affinity ratios virtual -> local frame

is_for_extremity()

As says

is_for_origin()

As says

is_start()

As says

move(v_dx, v_dy, dstyle, top_node)

Move the node - mx_virt, my virt coordinates of the mouse in virtual screen frame click_loc is the location of the clic in node’s frame

class cadbiom.models.guard_transitions.chart_model.CTopNode(name, model, **kwargs)

A virtual macronode on top of the hierarchy. A model can be a list of hierarchy. This artificial node groups all the hierarchy. From a graphical point of view, it represents the virtual drawing window.

Note

We assume that the first node in sub_nodes is the main MacroNode. TODO: test if there are another nodes in sub_nodes?

add_submodel(mnode)

add a submodel (subtree) with root a macro node (no check performed)

aff_coef(swidth, sheight, top_node)

Affinity coefficients

copy()

Duplicate a CTopNode - Performs a deep copy - Reduce displayed dimensions - The top node is changed into a macro node - The env_node (if any) is not copied.

draw(view)

The TOP node is virtual - so no drawing if there is only one subnode which is a macro - draw it full screen (this is the case when a macro node is edited in a new tab)

find_element(mox, moy, dstyle)

@param mox,moy :coordinates of the mouse in local frame (own frame for top node) @param dstyle: drawing style used in the view

Given the window mouse coordinates, return (node, handle, center) where node is the node the mouse is in, handle the handle of the node the mouse is in and c are the coordinates of the node center in view. If no handle, handle = 0, handle are 1,2,3,4 clockwise numbered from upper left corner If no node found returns (None,0,(0,0))

class cadbiom.models.guard_transitions.chart_model.CTransition(origin, extremity)

A guarded transition object

Parameters:

• macro_node (<CMacroNode>) – The parent macro node containing this transition
• ori (<CNode>) – The node on the left of the transition
• ext (<CNode>) – The node on the right of the transition
• name (<str>) – The name of the transition (never used => legacy ?)
• event (<str>) – The logical formula of the event
• condition (<str>) – The logical formula of the condition
• note (<str>) – Text (JSON formatted on v2 models) with data about related to the transition
• search_mark (<boolean>) – This flag is used to change the color of selected transition from the GUI. .. seealso:: drawing_style()
• selected (<boolean>) – This flag is used to change the color of mouse selected transitions. .. seealso:: drawing_style()

accept(visitor)

standard accept visitor

clean()

Unmark

get_influencing_places()

Return set of places that influence the condition of the transition

Places are taken from:

• The condition (logical formula) of the current transition,
• The definition of logical events in the events’ attribute of the current transition.

Note that when multiple events share 1 transition, the condition attribute should be empty.

See also

parse_condition() and cadbiom.models.biosignal.translators.gt_visitors.get_conditions_from_event().

Return type:<set <str>>

get_key()

key for storing the transition in dictionaries

is_me(mox, moy, dstyle, w_coef, h_coef)

Tell if mouse position is closed to transition

Parameters:moy (mox,) – mouse coordinates in container coord (local coordinates) Returns:True or False Return type:<boolean>

parse_condition(**kwds)

Get set of places from a condition (logical formula)

The grammar used here is simplified compared to that used for loading models.

See also

cadbiom.models.biosignal.translators.gt_visitors.compile_cond()

Parameters:condition (<str>) – Returns:Set of places involved in the condition. Return type:<set <str>>

remove()

Remove the current transition from its macro node

set_action(act)

@param act: string

set_condition(cond)

@param cond : string

set_event(event)

@param event: string

set_name(name)

@param name: string

set_note(note)

@param note: string

class cadbiom.models.guard_transitions.chart_model.CTrapNode(xcoord, ycoord, model, **kwargs)

Dead end node

accept(visitor)

Standard acceptor

draw(view, xfr, yfr, wfr, hfr, depth)

depth is less than depth_max

class cadbiom.models.guard_transitions.chart_model.ChartModel(name, xml_namespace=u'http://cadbiom.genouest.org/')

Model of a chart - implements the observer pattern as subject observers must have an update method

Attributes:

param name:

Name of the model

param xml_namespace:  

Version of cadbiom model

Allowed values:

• v1 (default): http://cadbiom.genouest.org/
• v2: http://cadbiom.genouest.org/v2/

Note: v2 models allow metadata in JSON format.

param simple_node_dict:  

For quick finding - name -> node. This is for the GUI: list only CSimpleNodes

param node_dict:  

For quick finding - name -> node. This is for internal use and this attribute can contain all types of nodes: Start/Trap/Input/Perm/Macro/Top/Simple nodes.

param transition_list:  

All the transitions in the model

param signal_transition_dict:  

For quick finding - simple node name -> list of influenced transitions. i.e: nodes that are in the condition of a transition only.

param __root:

A virtual macronode on top of the hierarchy. This artificial CTopNode node groups all the hierarchy.

See also

CTopNode()

param constraints:  

biosignal clock constraints

param modified:

Boolean to test if the model has been modified. Used to test if the model can be closed safely without loose of data.

param show_macro:  

Boolean used show/hide the MacroNodes if MAX_SIZE_MACRO (default: 50) is exceeded.

param max_size:

Max number of nodes allowed to be drawn. default: MAX_SIZE=2000

param __observer_list:  

For observer pattern (?)

param marked_nodes:  

Set of marked (highlighted/selected) nodes in the graph editor

param marked_transitions:  

Set of marked (highlighted/selected) transitions in the graph editor

type name:

<str>

type xml_namespace:  

<str>

type simple_node_dict:  

<dict <str>:<CSimpleNode>>

type node_dict:

<dict <str>:<CNode>>

type transition_list:  

<list <CTransition>>

type signal_transition_dict:  

<dict <str>:<list <CTransition>>>

type __root:

<CTopNode>

type constraints:  

<str>

type modified:

<boolean>

type show_macro:  

<boolean>

type max_size:

<int>

type __observer_list:  

<list <?>>

type marked_nodes:  

<set>

type marked_transitions:  

<set>

accept(visitor)

Visitors entrance

attach(obs)

observer pattern standard attach methods

build_from_cadlang(file_name, reporter)

Build a model from a .cal file of PID database (Test purpose)

Used only by library.cadbiom.models.clause_constraints.mcl.TestMCLAnalyser

@param file_name: str - path of .cal file

clean()

Clean markers

clean_code()

Clean code attribute

detach(obs)

observer pattern standard detach methods

draw(view)

Redraw the model

Asked from:

• cadbiom_gui.gt_gui.chart_view.ChartView: via its update() and on_expose_event() methods
• cadbiom_gui.gt_gui.chart_view.NavView: idem

@param view: chart_view

find_element(m_v_c, dstyle)

@param m_v_c :coordinates of the mouse in virtual screen @param dstyle: drawing style (gives virtual size of fixed size nodes)

Given the window mouse coordinates, return (node, handle, center) where node is the node the mouse is in, handle the handle of the node the mouse is in and c are the coordinates of the node center in view. If no handle, handle = 0, handle are 1,2,3,4 clockwise numbered from upper left corner If no node found returns (None,0,(0,0))

get_influenced_transition(node_name)

Parameters:node_name – Name of a node Returns:The transitions influenced by the node i.e. when the node name appears in the condition

get_matching_node_names(regex_obj)

Return node names that contain the given regular expression

Parameters:regex_obj (<_sre.SRE_Pattern>) – Compiled regular expression

get_node(name)

Parameters:name – string - name of the node Returns:a node

get_root()

@return: the root of the hierarchy

get_simple_node(name)

Parameters:name – string - name of the node Returns:a simple node with given name

get_simple_node_names()

Return list of the simple nodes in the model

This function is called each time an update of SearchManager and SearchFrontier is required by the user; or by ToggleWholeModel

See also

• cadbiom_gui.gt_gui.chart_misc_widgets.SearchManager.display_nodes()
• cadbiom_gui.gt_gui.chart_simulator.chart_simul_controler.ToggleWholeModel()

Note

The signal_transition_dict is refreshed here on condition that the transitions of the model have changed.

The boolean self.modified can’t be tested here because it can be True only because moved nodes.

is_submodel()

test if it is a submodel (for macro view)

make_submodel(mnode)

make a submodel from a macronode (no check) of another model

mark_as_frontier(node_name)

Given the name of a simple node, add a start node and a transition from the start node to the simple node

Warning

notify observers

Parameters:node_name – Name of a node

notify()

Observer pattern: standard notify methods

Notify observers when the model have been changed (move/delete/add item)

Observers are:

• ChartView (GtkDrawingArea)
• NavView (GtkDrawingArea)
• SearchManager
• SearchFrontier

set_search_mark(node_names)

Notify observers after marking nodes and transitions related to the given nodes names

Note: mark status of nodes implies their coloring in the graph editor.

Parameters:node_names (<list <str>>>) – List of names

turn_into_input(node_name)

Turn a simple node into an input node

turn_into_perm(node_name)

Turn a simple node into a perm node

unmark_nodes_and_transitions()

Handy function to unmark simple nodes and transitions with conditions

Note: mark status of nodes implies their coloring in the graph editor.

Called by: search_mark(), unmark_nodes_and_transitions()

unset_search_mark()

Notify observers after unmarking nodes and transitions with conditions

Note: mark status of nodes implies their coloring in the graph editor.

exception cadbiom.models.guard_transitions.chart_model.ChartModelException(mess)

Exception for chart models

cadbiom.models.guard_transitions.chart_model.intersect_simple(node1, node2, dstyle, nb_trans, w_ratio, h_ratio)

Helper function: Intersection of a node with a transition

Standard representation of biosignal expressions as trees. In addition to standard logical operator, we introduce the default and when operators.

class cadbiom.models.biosignal.sig_expr.SigBinExpr(exp1, exp2)

Binary expression - abstract class

get_signals()

Gives the set of idents used in the expression

get_ultimate_signals(mcsys)

Gives the set of signals used in the expression

class cadbiom.models.biosignal.sig_expr.SigBotExpr

Usefull signal for initialisations - should not appear in normal signal expressions

accept(visitor)

Method for all kind of visitors - raise exception if not implemented

get_signals()

Gives the set of idents used in the expression

is_bot()

As it says

class cadbiom.models.biosignal.sig_expr.SigConstExpr(val)

Constant signals: True, False

accept(visitor)

Method for all kind of visitors - raise exception if not implemented

get_signals()

Gives the set of idents used in the expression

is_clock(symb_table, method=None)

Tick and true are considered as similar

is_const()

As it says

is_const_false()

As it says

class cadbiom.models.biosignal.sig_expr.SigConstraintExpr(name, explist=[])

Implements constraints on events

accept(visitor)

Method for all kind of visitors - raise exception if not implemented

add_arg(arg)

Constraints are n-ary operators - this method add an operand

class cadbiom.models.biosignal.sig_expr.SigDefaultExpr(exp1, exp2)

Implements the default operator

accept(visitor)

Method for all kind of visitors - raise exception if not implemented

is_clock(symb_table, method=None)

Check if an expression always give a clock

class cadbiom.models.biosignal.sig_expr.SigDiffExpr(exp1, exp2)

Implement the different test: sig1 != sig2 when both present

accept(visitor)

Method for all kind of visitors - raise exception if not implemented

is_clock(symb_table, method=None)

Check if an expression always give a clock

class cadbiom.models.biosignal.sig_expr.SigEqualExpr(exp1, exp2)

Implement the equality test: sig1 == sig2 when both present

accept(visitor)

Method for all kind of visitors - raise exception if not implemented

is_clock(symb_table, method=None)

Check if an expression always give a clock

class cadbiom.models.biosignal.sig_expr.SigEventExpr(exp)

Event operand creates a clock

accept(visitor)

Method for all kind of visitors - raise exception if not implemented

get_signals()

Gives the set of idents used in the expression

get_ultimate_signals(mcsys)

Gives the set of signals used in the expression

is_clock(symb_table, method=None)

Check if an expression always give a clock

class cadbiom.models.biosignal.sig_expr.SigExpression

Generic abstract class

accept(visitor)

Method for all kind of visitors - raise exception if not implemented

get_signals()

Gives the set of idents used in the expression

get_ultimate_signals(mcsystem)

Gives the set of signals used in the expression

is_bot()

As it says

is_clock(symb_table, method=None)

Check if an expression always give a clock

is_const()

As it says

is_const_false()

As it says

is_ident()

As it says

class cadbiom.models.biosignal.sig_expr.SigIdentExpr(name)

Ident expressions are represented by their name. So we need a symbol table for type checking

accept(visitor)

Method for all kind of visitors - raise exception if not implemented

get_signals()

Gives the set of idents used in the expression

get_ultimate_signals(mcsystem)

Gives the set of signals used in the expression

is_clock(symb_table, method=None)

Check if an expression always give a clock

is_ident()

As it says

class cadbiom.models.biosignal.sig_expr.SigNotExpr(exp)

Boolean not on a signal

accept(visitor)

Method for all kind of visitors - raise exception if not implemented

get_signals()

Gives the set of idents used in the expression

get_ultimate_signals(mcsys)

Gives the set of signals used in the expression

is_clock(symb_table, method=None)

Check if an expression always give a clock

class cadbiom.models.biosignal.sig_expr.SigSyncBinExpr(operator, exp1, exp2)

Generic class for boolean operation on signals A boolean operator emits a signal when both operand are present

accept(visitor)

Method for all kind of visitors - raise exception if not implemented

is_clock(symb_table, method=None)

Clocks are assimilated to boolean signals with true value And and or give true in this case, so its a clock!!

class cadbiom.models.biosignal.sig_expr.SigWhenExpr(exp1, exp2)

Implements when expression

accept(visitor)

Method for all kind of visitors - raise exception if not implemented

is_clock(symb_table, method=None)

Check if an expression always give a clock

Translators

BCX models

Load and generate Cadbiom xml files

Classes:

• XmlVisitor: Visitor used to generate xml cadbiom code when the model is exported.
• MakeHandler: Make a handler for the parser when the model is loaded.
• MakeModelFromXmlFile: Handy class used to parse an xml file.
• MakeModelFromXmlString: Handy class used to parse an xml string.

class cadbiom.models.guard_transitions.translators.chart_xml.MakeHandler(model=None)

Make a handler for the parser when the model is loaded.

Users are expected to subclass ContentHandler to support their application. The following methods are called by the parser on the appropriate events in the input document:

https://docs.python.org/2/library/xml.sax.handler.html

characters(chr)

Receive notification of character data.

The Parser will call this method to report each chunk of character data. SAX parsers may return all contiguous character data in a single chunk, or they may split it into several chunks; => we need to do a concatenation

Parameters:arg1 (<str>) – chunck of characters.

endElement(name)

Called when an elements ends

Note

We handle only elements that need post processing like transitions and nodes: reset self.current_element that is used to load notes (inner text of xml object).

init_node_functions(top_pile=None)

Bind functions to add different types of nodes to the cadbiom model

Note

Must be call after the init of self.top_pile with the xml root object.

Note

If called when a MacroNode is encountered; must be called when the end-tag is encountered with the parent node set in top_pile argument.

Parameters:top_pile (<CNode>) – If set, all futures nodes will belong to this node. It is used for MacroNodes: all subnodes belong to them.

startElement(name, att)

Signal the start of an element

Note

Nodes have to be at the top of the model (Before transitions) Transitions do not allow reflexive ones (as it could be said in the doc); Duplication of transitions are not authorized but only print a warning in the shell (they are not taken into account)

Parameters:

• arg1 (<str>) – Contains the raw XML 1.0 name of the element.
• arg2 (<xml.sax.xmlreader.AttributesImpl>) – Holds an object of the Attributes interface.

class cadbiom.models.guard_transitions.translators.chart_xml.MakeModelFromXmlFile(xml_file, model=None)

Handy class used to parse an xml file

model

Return the model generated from the XML file

Return type:<ChartModel>

class cadbiom.models.guard_transitions.translators.chart_xml.MakeModelFromXmlString(xml_string)

Handy class used to parse an xml string.

model

Return the model generated from the XML string

Return type:<ChartModel>

class cadbiom.models.guard_transitions.translators.chart_xml.XmlVisitor(model)

Visitor used to generate XML Cadbiom code when the model is exported.

Parameters:

• model (<ChartModel>) – Chart model - Cadbiom model
• fact_list (<list <str>>) – List of fact ids found in all the transitions.
• xml (<str>) – xml string representation of the model
• symb (<set>) – symbol set used to check double naming of nodes; Double declarations are problematic.
• default_node_attributes (<tuple <str>>) –

check_name(name)

Detect double declarations

get_existing_attributes(node)

Return dict of attributes of the given node

Note

The set of attributes are defined in the default_node_attributes attribute of the current class.

Note

We use OrderedDict in order to improve human readability of the produced models.

Returns:Dictionary of attributes. Keys: names of attributes; Values: Values of attributes; Note that values are converted to strings in order to fit with lxml requirements. Return type:<OrderedDict <str>:<str>>

get_fact_ids()

Get litterature references

Return type:<set>

return_xml()

Return the model as xml string.

Note

Used when the model is saved in a .bcx file.

visit_chart_model()

Entrance point for visitors

Called by the constructor and by the cadbiom.models.guard_transitions.chart_model.ChartModel.accept() method.

visit_cinput_node(inn)

Return tag name and formated attributes of an input node

Returns:Tuple of tag name and OrderedDict of attributes Return type:<str>, <OrderedDict <str>:<str>>

visit_cmacro_node(mnode)

Explore subnodes and transitions in the given macro node.

Return tag name and formated attributes of a macro node.

Returns:Tuple of tag name and OrderedDict of attributes Return type:<str>, <OrderedDict <str>:<str>>

visit_cperm_node(pnode)

Return tag name and formated attributes of a perm node

Returns:Tuple of tag name and OrderedDict of attributes Return type:<str>, <OrderedDict <str>:<str>>

visit_csimple_node(sin)

Return tag name and formated attributes of a simple node

Returns:Tuple of tag name and OrderedDict of attributes Return type:<str>, <OrderedDict <str>:<str>>

visit_cstart_node(snode)

Return tag name and formated attributes of a start node

Returns:Tuple of tag name and OrderedDict of attributes Return type:<str>, <OrderedDict <str>:<str>>

visit_ctop_node(tnode)

Interative build of XML tree for model saving

Note

namespace seems to be useless regarding nsmap here, because we use the default namespace without prefix… See http://lxml.de/tutorial.html#namespaces.

visit_ctransition(trans)

Return tag name and formated attributes of a transition

Returns:Tuple of tag name and OrderedDict of attributes Return type:<str>, <OrderedDict <str>:<str>>

visit_ctrap_node(tnode)

Return tag name and formated attributes of a trap node

Returns:Tuple of tag name and OrderedDict of attributes Return type:<str>, <OrderedDict <str>:<str>>

PID models

Guarded transition interpretation of PID data

class cadbiom.models.guard_transitions.translators.chart_xml_pid.MEvent(inputs, outputs, act_list, inhib_list, pmid, ai_inter)

Object merging similar events in PID

merge(mev)

merge two events: we take the “or” of the two conditions references are concatenated without redondancy check

set_clock()

Create a clock ident and store it in the object

class cadbiom.models.guard_transitions.translators.chart_xml_pid.MakeModelFromPidFile(xml_file, reporter, has_clock=True, ai_inter=0, model=None, e_loc=[])

Object for parsing a PID xml file

clock_trans(mev, input, output, condition)

translation with clock introduction

coord_inc()

increment coordinates of nodes for a rectangular layout

extract_int(inter)

Extract information from a PID interaction

location_converter(location)

convert PID location coding into cadbiom one

make_dict()

build the two dictionaries dict_id and dict_name - Cadbiom basic names are created. Cadbiom names result from a mangling of basic name (‘PF’ one if any) and various information such that localisation, activity, ptm …see throught_components

make_mev_dict()

Since several events with same inputs and outputs (and different conditions) may exist in PID, we merge them

make_new_node(node_name, node_type)

add a new node in the model

make_transition(mev)

mev is the current merge event

no_clock_trans(mev, input, output, condition)

translation without clock - data flow interpretation

throught_component(component)

Cadbiom names result from a mangling of basic name (‘PF’ one if any) and various information such that localisation, activity, ptm … This is done here.

cadbiom.models.guard_transitions.translators.chart_xml_pid.default_clock(cl1, cl2)

generate a literal default clock

cadbiom.models.guard_transitions.translators.chart_xml_pid.logical_and(lprop)

@return: str - AND of the input list

cadbiom.models.guard_transitions.translators.chart_xml_pid.logical_or(list)

@return: str - OR of the input list

cadbiom.models.guard_transitions.translators.chart_xml_pid.make_name(name, act, ptm, loc)

tgenerate a name

cadbiom.models.guard_transitions.translators.chart_xml_pid.make_new_name(name)

remove unusable characters

cadbiom.models.guard_transitions.translators.chart_xml_pid.ptm_converter(ptm_term)

post transformation convertion from PID to Cadbiom

cadbiom.models.guard_transitions.translators.chart_xml_pid.when_clock(clo, cond)

generate a when literal expression

Analyser

Static analysis

Classes for static analysis

class cadbiom.models.guard_transitions.analyser.static_analysis.StaticAnalyzer(reporter)

Main class for static analysis

build_from_cadlang(file_name)

Build a StaticAnalyser from a .cal file of PID database @param file_name: str - path of .cal file

build_from_chart_file(file_name)

Build a StaticAnalyser from a .bcx file @param file_name: str - path of the .bcx file

build_from_chart_model(chart_model)

For technical purpose

build_from_pid_file(file_name, has_clock=True, ai_interpretation=0)

Build an StaticAnalyser from a .xml file of PID database @param file_name: str - path of .xml file

export_2_dot(graph, dot_file)

As it says @param graph: the graph to export @param dot_file: filename

export_2_graphml(graph, graphml_file)

As it says @param graph: the graph to export @param graphml_file: filename

get_basal_activated_genes()

Basal activated genes are genes which are activated even if all the places present in activation condition, are inactivate

get_frontier_node_names()

returns a (list<string>) list of frontier place names

get_frontier_scc()

Find initial strongly connected components in the transition graph

Warning

If the model is modified but not reloaded, KeyError is raised (see below); we inform the user of that…

Returns:List of list of node names in frontier strongly connected components Return type:<list <list <str>>>

get_gene_places()

Return gene places

Note

We assume that places representing a gene contain the ‘_gene’ string in the name

Returns:List of places. Return type:<list <place>>

get_local_neighbors(dgraph, node)

return node direct neighbors (successors and predecessors) in a same list @return: a list of str neighbor name

get_predecessors(dgraph, node, rank=None)

return all node predecessors if rank=None, predecessors under the rank else @return: a list of str predecessor name

get_statistics(sfile=False)

Merge various information on the model and its nodes

Note

In models written in verson (without JSON extra-data), we assume PID encoding to detect locations of entities.

Warning

Start nodes (__start__0) are counted here in ‘other_locations’ and ‘other_types’.

Parameters:arg1 (<open file>) – Opened file (optional). Returns:Information (status of nodes and their cellular locations). Return type:<str>

get_stats_entities_data()

Return occurences of various locations and entity types in the model

Note

Start nodes (with a name like __start__x) are handled even with no JSON data. They are counted in the other_types and other_locations fields.

Example:

static_analyser = StaticAnalyzer(Reporter())
static_analyser.build_from_chart_model(model)
locations, entity_types =                     static_analyser.get_stats_entities_data()

Returns:

locations, entity_types .. note:: For v1 models, entity_types will be an empty dictionary.

Return type:

<Counter>, <Counter>

get_stats_model_data()

Return info from the model

Returns:Dictionary: List of keys: - model_name: Name of the model - places: Number of places in the model (length of node_dict attr) - transitions: Number of transitions in the model (length of transition_list) Return type:<dict>

get_stats_model_structure_data()

Return occurences of various types of nodes in the model

Note

• Nb input nodes
• Nb frontier nodes (no incoming transitions)
• Nb terminal nodes (no outgoing transitions)
• Nb isolated nodes (frontier places in conditions/not used)

Returns:Dict with occurences of input_nodes, frontier_nodes, final_nodes, isolated_nodes. Return type:<dict>

get_successors(dgraph, node, rank=None)

return all node successors if rank=None, successors under the rank else @return: a list of str successor name

get_tr_principal_variables(trans)

Compute the essentiel, inhibitors, dominant inhibitors, essential activators and dominant activators of a transition tr.

get_why_basal_genes()

More complete than get_basal_activated_genes. Returns a list of pairs (g,lpv) where g is a basal activated gene and lpv are the principal variables (isolated_inhib., dominant_inhib, essential_act, dominant activator)

in_degree_cut_off(dgraph, degree)

@return: a Networkx digraph without nodes with input degree upper than degree parameter

make_dependence_dg(weight=False)

Build the directed graph of transitions and conditions (dependence graph) if weight : dependencies from transitions have a weight of 2, dependencies from conditions have a weight of 1 else : all dependencies have a weight of 1 @return: a Networkx digraph

make_full_dependence_dg(weight=False)

Build the directed graph of transitions and conditions (dependence graph) Conditions also influence input @return: a Networkx digraph

make_transition_dg()

Build the directed graph of transitions (flow graph) @return: a Networkx digraph

out_degree_cut_off(dgraph, degree)

@return: a Networkx digraph without nodes with output degree upper than degree parameter

remove_nodes_in_list(graph, node_list)

@return: a Networkx graph (or digraph) without nodes in the input list

remove_nodes_not_in_list(graph, node_list)

@return: a Networkx graph (or digraph) without nodes NOT in the input list

test_get_tr_node_variables(trans)

externalize a private method for test only

cadbiom.models.guard_transitions.analyser.static_analysis.cmpval(xxx, yyy)

utility

cadbiom.models.guard_transitions.analyser.static_analysis.stat_on_dgraph(dgraph)

???

cadbiom.models.guard_transitions.analyser.static_analysis.stat_on_graph(graph)

???

cadbiom.models.guard_transitions.analyser.static_analysis.view_graph(graph)

draw interaction graph with matplotlib

cadbiom.models.guard_transitions.analyser.static_analysis.view_weighted_graph(graph, rank)

???

Visitors of guarded transitions models

Visitors for guarded transition model analysis

Visitors:

• TableVisitor: used to collect action and place declarations of a model
• FrontierVisitor: Simple frontier computation for editor
• IndirectFlowGraphBuilder: build a networkx indirect graph of transitions (for debugging only)
• DirectFlowGraphBuilder: build a networkx graph of transitions (for tests only)
• EstimExpVisitor: Partial Evaluator of event and condition expressions (subset of sig expressions)
• SigExpIdCollectVisitor: Collect idents in a sig expression

Note

2 more visitors are kept elsewhere for practical reasons and for now at:

• cadbiom.models.clause_constraints.mcl.CLUnfolder.PropertyVisitor() (involve Clause and Literals).
• cadbiom_gui.gt_gui.chart_checker.chart_checker_controler.PropertyVisitor() (used to get mandatory nodes in conditions of transitions)

class cadbiom.models.guard_transitions.analyser.ana_visitors.DirectFlowGraphBuilder(nwx_graph, direct=True)

build a networkx graph of transitions (for tests only)

visit_chart_model(model)

entrance through top node

visit_cinput_node(node)

Nothing to do

visit_cmacro_node(node)

collect edges from transitions

visit_cperm_node(node)

Nothing to do

visit_csimple_node(node)

Nothing to do

visit_cstart_node(node)

Nothing to dot

visit_ctop_node(node)

t same as macro

visit_ctrap_node(node)

Nothing to do

class cadbiom.models.guard_transitions.analyser.ana_visitors.EstimExpVisitor(symb_t)

Partial Evaluator of event and condition expressions (subset of sig expressions) The value of an expression is either True (1) or False (-1) or Indeterminate (0) If no symbol table, all variables are evaluated to False

=> Evaluate if the expression is True or False given the presence or absence of entities in symb_t.

visit_sig_const(cex)

coding of the constant on 1,-1

visit_sig_default(dex)

this evaluation is valid for clocks only

visit_sig_equal(eex)

not yet implemented

visit_sig_ident(iex)

@param iex: the biosignal ident expression

visit_sig_not(nex)

opposite in our coding

visit_sig_sync(sex)

estimation depends on the operator

visit_sig_when(wex)

left operand is a clock and right operand a condition

class cadbiom.models.guard_transitions.analyser.ana_visitors.FrontierVisitor

Simple frontier computation for editor

is_frontier(node)

Find if a node is a frontier node or a start node.

visit_chart_model(model)

Entrance for the visitor

visit_cinput_node(node)

Nothing to do

visit_cmacro_node(node)

macros are not on the frontier

visit_cperm_node(node)

Nothing to do

visit_csimple_node(node)

check if it is a frontier node

visit_cstart_node(node)

Nothing to do

visit_ctop_node(node)

visit subnodes

visit_ctrap_node(node)

Nothing to do

class cadbiom.models.guard_transitions.analyser.ana_visitors.IndirectFlowGraphBuilder(nwx_graph)

build a networkx indirect graph of transitions (for debugging only)

visit_chart_model(model)

entrance through top node

visit_cinput_node(node)

Nothing to do

visit_cmacro_node(node)

visit sub elements

visit_cperm_node(node)

Nothing to do

visit_csimple_node(node)

Nothing to do

visit_cstart_node(node)

Nothing to do

visit_ctop_node(node)

same as macro

visit_ctrap_node(node)

Nothing to do

class cadbiom.models.guard_transitions.analyser.ana_visitors.SigExpIdCollectVisitor

Collect idents in a sig expression

visit_sig_const(cexp)

no id

visit_sig_default(dexp)

ids come from both operands

visit_sig_equal(eex)

not implemented

visit_sig_ident(iexp)

@param iexp: the expression

visit_sig_not(nex)

same as operand

visit_sig_sync(sex)

ids come from both operands

visit_sig_when(wexp)

ids come from both operands

class cadbiom.models.guard_transitions.analyser.ana_visitors.TableVisitor(erdisplay)

Visitor used to collect action and place declarations

Events and conditions are not considered so implicit free clocks are not registered. The name of a place must be unique in a whole chart (no scope implemented). The same holds for an event declared in an action. Pseudo places used for inputs can be declared several time

TYPES: state, input, emit OTHER TYPES: clock (used when free clocks are found)

The attribute tab_symb is filled for the following types:

- SimpleNodes: type: state,
- InputNodes: type: input, deep: 0,
- PermNodes: type: state,
- MacroNodes: type: state,
- TopNodes: type: state,
- Transitions: type: emit

The deepness of each node is the imbrication level of Macro states and is dynamically adjusted for elements contained in MacroNodes/TopNodes.

declare(name, stype)

Register an identifier with its type

visit_chart_model(model)

first step in the visit

visit_cinput_node(node)

register the ident as input

visit_cmacro_node(node)

register the node as a state deepness is updated

visit_cperm_node(node)

register the node as a state

visit_csimple_node(node)

register the node as a state

visit_cstart_node(node)

nothing to declare

visit_ctop_node(node)

after registering the node, visit subnodes and transitions

visit_ctransition(trans)

visit transition

visit_ctrap_node(node)

nothing to declare

Simulator

Building blocks for a simulator

class cadbiom.models.guard_transitions.simulator.chart_simul_elem.Condition(exp)

A condition is a boolean expression on place values

class cadbiom.models.guard_transitions.simulator.chart_simul_elem.Event(exp)

An event is a clock from a Biosignal point of view - it is defined as a signal expression

is_input_event()

As it says

is_place()

As it says

set_activated(val)

@param val: activation value

class cadbiom.models.guard_transitions.simulator.chart_simul_elem.InputEvent(exp)

Special events for inputs

add_ev_place(pla)

pla must be an input place

is_input_event()

As it says

set_activated(val)

overload the method of general class

class cadbiom.models.guard_transitions.simulator.chart_simul_elem.InputPlace(g_state, name=None)

@param g_state: Corresponding place in CadbiomChart model (possibly None) @param name: Must be given if g_state=None An input place coming from the graph model is a sort of perm place An input place representing a free event has no corresponding element in chart model (g_state = None)

activate()

As it says

desactivate()

places without graph representation are artificial inputs thus perm = True

input_activate()

special activation for input

input_desactivate()

special unsactivation for input

is_input_place()

As it says

class cadbiom.models.guard_transitions.simulator.chart_simul_elem.Place(g_state, name=None)

A place represents a component of the state of the system

activate()

As it says

desactivate()

places without graph representation are artificial inputs thus perm = True

force_desactivate()

Used to clear chart_model places activations desactivate all places - even permanent places

is_input_event()

As it says

is_input_place()

As it says

is_place()

As it says

set_perm()

Turn into a permanent node

class cadbiom.models.guard_transitions.simulator.chart_simul_elem.STransition(ori, ext, gtrans=None)

Represents a normal transition between places - For optimization of induced transitions, STransitions have several origins and several targets. This is for taking care of initializations when a macro state is activated and multiple un-activations for output transitions from places representing macros.

activate()

activation

desactivate()

unactivation

init_desactivate()

initial RAZ

set_condition(cond)

standard setter

set_event(evt)

standard setter

set_signal(sig)

standard setter

Visitor for simulator generation

class cadbiom.models.guard_transitions.simulator.translators.gt_visitors.GenSimVisitor(tab_symb, mod, free_clocks, report)

Generate a simulator model - needs a symbol table of the charter model

build_input_transition(trans)

Build a perm place (if not already done) and a transition from the perm node to the target of trans. @param trans: the chart model transition

build_transition(trans, trap=False)

build a transition from a graph transition @param trans: the chart transition @param trap: True if target is a trap node

visit_chart_model(model)

visit chart model, generate simulation model and collect free clocks

visit_cinput_node(node)

create an input place (artificial perm place) and an event representing the input

visit_cmacro_node(node)

macro nodes are treated as simple nodes (no real macros allowed)

visit_cperm_node(node)

create a place in the simulator model register it in the symbol table mark it as permanent

visit_csimple_node(node)

create a place in the simulator model register it in the symbol table

visit_cstart_node(node)

do nothing: see transitions

visit_ctop_node(node)

trap node is unique for all the system it is created here

visit_ctransition(trans)

main visitor - the code generation is dispatched in several helper methods

visit_ctrap_node(node)

do nothing: see transitions

cadbiom.models.guard_transitions.simulator.translators.gt_visitors.input_perm_name(in_node)

generate a standard name for pseudo perm places associated with inputs

cadbiom.models.guard_transitions.simulator.translators.gt_visitors.input_trans_name(trans)

generate a standard name for transitions

Guarded transition systems simulator implementation

class cadbiom.models.guard_transitions.simulator.chart_simul.ChartSimulator

wrap everything for simulation - this include the simulator model and simulator attribute to manage simulation.

add_event(evt, name)

add an event

add_input(inp)

add an input

add_place(place)

add any place

add_state_place(place, name)

state places are referenced in the simulator symbol table

add_transition(trans)

add a transition

build(chart_model, sim_option, reporter)

Given a chart_model, build a simulator @param chart_model: a ChartModel object @param sim_option: allows free clocks if True @param reporter: must be a CompilReporter

check_inv_conditions()

evaluate invariant property in the current state Raise a SimulPropViolation exception if invariant property is not satisfied.

check_reachable_property()

evaluate final property in the current state @return: the result (bool) of the evaluation

get_step()

value of the simulator step counter

get_symb_tab()

the symbol table: name -> chart_simul_elem

has_input()

test if the simulated model has inputs

set_act_file_input_stream(filename)

Find the file containing input description as an enumeration of activated __inputs - set the input stream Throw SimulException

set_act_input_stream(act_input_list)

Set the input stream from a list of activated __inputs in format “% i1 i2 h2 h4 h8”

set_cfile_input_stream(filename)

Find the file containing input description using a language - set the input stream Throw SimulException

set_invariant_prop(prop)

set invariant property to be checked. A property violation exception is raised if violated @param prop: string - textual representation of property on places

set_reachable_prop(prop)

set reachable property to be checked. @param prop: string - textual representation of property on places

set_sce_file_input_stream(filename)

Find the file containing description of a scenario set the input stream to read the __inputs only Throw SimulException

simul_init()

Simulator initialization

simul_init_places(init_places)

@param init_places: list of place names to be activated

simul_step()

Perform a simulation step

simul_step_trace(trace_file=None)

same as simul_step but register a trace

class cadbiom.models.guard_transitions.simulator.chart_simul.SimReport

Simple reporter used for simulation

display(mess)

Interrupt all in case of problems

Tests

PathExtractor

Test Visitors for extracting submodels. PathExtractor : abstract a trajectory as a set of path in the transition graph

class cadbiom.models.guard_transitions.TestModelExtraction.Reporter

Simple reporter for tests

display(mes)

print message

class cadbiom.models.guard_transitions.TestModelExtraction.TestExtractVisitors(methodName='runTest')

Test visitor for model extraction

test_exec1(**kwargs)

Test on simple exp

test_exec2()

test visitor execution

Static analysis

Review: Pay attention: Lots of tests are made without any assertion.

Valid tests are only a weak guarantee that the program does not crash since everything comes out on stdout (masked by pytest). In addition, many files essential to the tests are lost/missing because they were never added to the project.

Have fun.

class cadbiom.models.guard_transitions.analyser.TestStaticAnalysis.Reporter

Simple reporter for tests

display(mes)

print message

class cadbiom.models.guard_transitions.analyser.TestStaticAnalysis.TestAnaVisitors(methodName='runTest')

Test visitor for static analysis

test_frontier()

frontier visitor test

class cadbiom.models.guard_transitions.analyser.TestStaticAnalysis.TestStaticAnalysis(methodName='runTest')

Test static analysis

test_cadbiom_2_graphml(**kwargs)

test export in GML

test_frontier1()

frontier computation

test_frontier1_no_clock()

test with a rather big clockless model

test_frontier2()

frontier computation on all database

test_gene_signal_dependent(**kwargs)

As it says

test_get_pred_and_succ(**kwargs)

test predecessors and successors

test_get_tr_node_variables()

n1 –> n2; h1 when n2 default h2 when n3[not n4] n1 –> n3; h2 when n4[] n4 –> n1; h3[]

Get the node idents in the guard expression of the transition condition and event

test_ordering_pred(**kwargs)

write a predecessor file clustering predecessors into 10 class in fact of the distance of the shortest path to a given target Each line of the output file is a tab separated list of predecessors of the same class

test_pred_dependence_graph(**kwargs)

As it says

test_pred_graph_extraction(**kwargs)

As it says

test_principal_variables()

n1 –> n2; h1 when n2 default h2 when n3[not n4] n1 –> n3; h2 when n4[n1 or (not n4)] n4 –> n1; h3[n3 or not n4]

Compute the essentiel, inhibitors, dominant inhibitors, essential activators and dominant activators of a transition tr.

n4: dominant inhibitor of tr1

test_signal_gene_influent(**kwargs)

???