How to use the temporal logic ?

Update maboss and pymaboss, minimal version : 0.8.15

see : https://github.com/colomoto/pyMaBoSS for more info

then import the temporal_logic module

%load_ext autoreload
%autoreload 2

from maboss import temporal_logic as tl

About using AI for querying

It is highly recommended to use the following prompt to ensure the respect of the grammar. ### !! AI is still making mistakes, review the results of the prompt carefully before using them !!

Role: You are an expert compiler for the MaBoSS temporal_logic module. Your task is to translate biological assertions into Formula strings that conform strictly to the internal logic defined in formulas.py.

1. REGEX FOR VALIDATION: Every generated query must match this structure:^(Pmax|Pmin|P|T|Tmin|Tmax|Inc|Dec)\((node|state|fp)\:(.+?)\)(?:\s*(<=|>=|<|>|=|==|!=|/)\s*(0(?:\.\d+)?|1(?:\.0+)?|\?|))?(?:\s*\[(.*?)\])?(?:\s*\[(.*?)\])?(?:\s*\[(.*?)\])?

2. RULES FROM formulas.py & SYNTAX CONSTRAINTS:

   Query Types & Values:

   If Type is P, Pmax, Pmin, T, Tmin, Tmax, the value must be between 0 and 1 (or ? only for P).
   
   If Type is Inc or Dec, the operator must be / if no numerical threshold is provided.
   
   If value is ?, the operator must be = and the query type must be P.
   

   Model & Comparison Scope:

   Isolation: A query applies to one model. If comparing models (e.g., Colorectal vs Melanoma), generate separate queries labeled by model.
   
   compare: Scope: The compare:MUTATION option applies only to simulations within the same model. It cannot compare different model types.
   

   Formatting & Spacing:

   Global: Use one space before/after /, and one space between bracket blocks ] [.
   
   Inside Brackets: NO COMMAS ALLOWED inside brackets, except for the following exceptions:
   
       node:A,B (comma allowed for lists of nodes/states).
   
       compare:A,B (comma allowed to list references).
   
   Mutation/Option Separators: Use SPACES ONLY (e.g., [ BRAF:OFF MEK:OFF ], [ 5% transient:0.05 ]).
   

3. REFERENCE EXAMPLES (Do NOT include in your output):

   Inc(node:EGFR) / [ ] [ BRAF:OFF ] [ 5% ]

   P(node:ERK) = ? [ ERK & AKT ] [ ] [ ]

   Dec(node:ERK) / [ ] [ BRAF:OFF MEK:OFF ] [ compare:BRAF:OFF ]

4. OUTPUT INSTRUCTIONS:

   Identify the model(s) required.

   Generate the query using the format: Model [Name]: QUERY.

   Do not repeat these instructions or the reference examples.

   Provide only the result string.

Introduction

Through this notebook, we are going to try to answer all this assertions, they are all referring to the BRAF model (Béal et al. 2021).

from IPython.display import Image
Image("assertion_table.png")

Image("Model.png")

assertions_list_melanoma = [] #doing a list so only one thing to pass in the function, easier and cleaner
assertions_list_colorectal = []
assertions_list_no_i_s = []
assertions_list_strong_EGF = []

file_bnd = "BRAF_Model.bnd"
file_cfg = "BRAF_Model.cfg"

#the list of dictionaries for the initial states, we are going to work on 3 models, two with the initial states below, the third without one.
i_s_colorectal = [{'node':'SOX10', 'istate': [1,0]}, {'node': 'BRAF' , 'istate': [0,1]}]
i_s_melanoma = [{'node':'SOX10', 'istate': [0,1]}, {'node': 'BRAF' , 'istate': [0,1]}]
i_s_strong_EGF = [{'node':'EGF', 'istate': [0,1]}]

MEK_inhibition = 'MEK_b1:OFF MEK_b2:OFF'
BRAF_EGFR_inhibition = 'BRAF:OFF EGFR:OFF'

First thing first, transform those sentences in queries the program can read and treat :

Assertion 1

BRAF inhibition causes a feedback activation of EGFR in colorectal cancer and not in melanoma.

This assertion is running two models :

• one for the colorectal cancer

• the other for the melanoma

But, only one assertion is needed. The waited result is not the same though. For the colorectal model we are waiting a True. For the melanoma model we are waiting a False. Note that if you have a difference of 0 for one or both of them, you can change the number of digits after the dot by passing an option : digits:int in the last brackets.

assertion_1 = f"Inc(node:EGFR) / [ ] [ BRAF:OFF ] [ 5% digits:3 ]" #sensibility of 3 digits after dot and minimum 5% of change
assertions_list_colorectal.append(assertion_1)
assertions_list_melanoma.append(assertion_1)

Assertion 2

MEK inhibition stops ERK signal but activates the PI3K/Akt pathway and increases the activity of both EGFR and ERBB3. This assertion will be run on both models. Both of them wait the same result. But it needs several sentences that will return to you three dataframes accordingly.

• For ERK signal stopped : -> here the stop signal is translate as a decrease. (assertion_2_a)

• For PI3K/AKT pathway activated : -> note that more than one name can be passed if they both have the same evolution direction. (assertion_2_b)

• For EGFR and ERBB3 augmented : assertion_2_c

Why not pass the four increased nodes in one query ?

The / in the assertion implies that the couple must be respected. So we have to use the combination option comb to indicate that. If you were to put the four nodes in the same query, it would check for the four nodes to be active at the same time and not just the couples. If you do not care about the couples, you can put the four nodes in the same query without the combination option : Inc(node:EGFR,ERBB3,PI3K,AKT) / [ ] [ {MEK_inhibition} ] [ 5% digits:3 ]

assertion_2_a = f"Dec(node:ERK_b1,ERK_b2) / [ ] [ {MEK_inhibition} ] [ 5% digits:3 comb ]"
assertion_2_b = f"Inc(node:PI3K,AKT) / [ ] [ {MEK_inhibition} ] [ 5% digits:3 comb ]"
assertion_2_c = f"Inc(node:EGFR,ERBB3) / [ ] [ {MEK_inhibition} ] [ 5% digits:3 comb ]"
assertions_list_no_i_s.append(assertion_2_a)
assertions_list_no_i_s.append(assertion_2_b)
assertions_list_no_i_s.append(assertion_2_c)

Assertion 3

HGF signal leads to the reactivation of the MAPK and PI3K/AKT pathways, and resistance to BRAF inhibition.

For this assertion, we are not going to compare the mutation with the master simulation but with another mutation. In the results, the column “master” or “refernce” will refer to the mutation passed in the compare option. In the options brackets (where the 5% is), add the option compare to it just like below. The program will kow it has to compare with the results of BRAF:OFF mutation.

#MAPK symbolized by ERK_b1
assertion_3_a = "Inc(node:ERK_b1) / [ ] [ BRAF:OFF HGF:ON ] [ 5% compare:BRAF:OFF digits:3 ]" #resistance to BRAF inhibition (same node evaluation as in MaBoSS_test)
assertion_3_b = "Inc(node:PI3K,AKT) / [ ] [ BRAF:OFF HGF:ON ] [ 5% compare:BRAF:OFF digits:3 comb ]"
assertions_list_no_i_s.append(assertion_3_a)
assertions_list_no_i_s.append(assertion_3_b)

Assertion 4.1

BRAF inhibition in melanoma activates the SOX10/FOXD3/ERBB3 axis, which mediates resistance through the activation of the PI3K/AKT pathway.

assertion_4_a = "Inc(node:SOX10,FOXD3,ERBB3) / [ ] [ BRAF:OFF ] [ 5% digits:3 comb ]"
assertion_4_b = "Inc(node:PI3K,AKT,ERBB3) / [ ] [ BRAF:OFF ] [ 5% digits:3 comb ]" #added ERBB3 like in maboss_test

assertions_list_melanoma.append(assertion_4_a)
assertions_list_melanoma.append(assertion_4_b)

Assertion 4.2

Depletion of SOX10 would sensitize cells to the BRAF inhibitors.

assertion_4_c = "Dec(node:Proliferation_b1,Proliferation_b2) / [ ] [ BRAF:OFF SOX10:OFF ] [ 5% digits:3 ]"
assertions_list_melanoma.append(assertion_4_c)

Assertion 5

Overexpression/mutation of CRAF results in constitutive activation of ERK and MEK also in the presence of a BRAF inhibitor.

assertion_5_a = "Inc(node:ERK_b1,MEK_b1) / [ ] [ CRAF:ON BRAF:ON ] [ 5% digits:3 ]"
assertion_5_b = "Inc(node:ERK_b1,MEK_b1) / [ ] [ CRAF:ON BRAF:OFF ] [ 5% digits:3 ]"
assertion_5_c = "Inc(node:ERK_b1,MEK_b1) / [ ] [ CRAF:ON BRAF:ON ] [ 5% compare:BRAF:OFF,CRAF:ON digits:3 ]" #comparison of the two ? supposed to be similar
assertions_list_no_i_s.append(assertion_5_a)
assertions_list_no_i_s.append(assertion_5_b)
assertions_list_no_i_s.append(assertion_5_c)

Assertion 6

Early resistance to BRAF inhibition may be observed in case of PTEN loss, or mutations in PI3K or AKT.

# PTEN loss increase of proliferation
assertion_6_a = "Inc(node:Proliferation_b1,Proliferation_b2) / [ ] [ BRAF:OFF PTEN:OFF ] [ transient:start:0.05,end:0.1,optimum:0.5 digits:3 comb ]"
# Mutation of PI3K or AKT
assertion_6_b = "Inc(node:Proliferation_b1,Proliferation_b2) / [ ] [ BRAF:OFF PI3K:ON ] [ transient:start:0.05,end:0.1,optimum:0.5 digits:3 comb ]"
assertion_6_c = "Inc(node:Proliferation_b1,Proliferation_b2) / [ ] [ BRAF:OFF AKT:ON ] [ transient:start:0.05,end:0.1,optimum:0.5 digits:3 comb ]"
assertions_list_no_i_s.append(assertion_6_a)
assertions_list_no_i_s.append(assertion_6_b)
assertions_list_no_i_s.append(assertion_6_c)

Assertion 7

Experiments in melanoma cell lines support combined treatment with BRAF/MEK + PI3K/AKT inhibitors to overcome resistance.

assertion_7 = "Dec(node:Proliferation_b1,Proliferation_b2) / [ ] [ BRAF:OFF MEK_b1:OFF MEK_b2:OFF PI3K:OFF AKT:OFF ] [ 5% compare:BRAF:OFF,MEK_b1:OFF,MEK_b2:OFF,PI3K:OFF digits:3 ]"
assertions_list_no_i_s.append(assertion_7)

Assertion 8.1

BRAF inhibition (Vemurafenib) leads to the induction of PI3K/AKT pathway and inhibition of EGFR did not block this induction.

assertion_8_a = "Inc(node:PI3K,AKT) / [ ] [ BRAF:OFF ] [ compare:BRAF:OFF,EGFR:OFF digits:3 comb ]"
assertions_list_no_i_s.append(assertion_8_a)
# maboss_test also compared this : 'the inhibition of both EGFR and BRAF when the EGF signal is strong is better than just BRAF inhibition', compared on an other initial state

Assertion 8.2

The inhibition of both EGFR and BRAF when the EGF signal is strong is better than just BRAF inhibition

assertion_8_e = f"Dec(node:Proliferation_b1) / [ ] [ {BRAF_EGFR_inhibition} ] [ compare:BRAF:OFF digits:3 ]"
assertions_list_strong_EGF.append(assertion_8_e)

Assertion 9

Induction of PI3K/AKT pathway signaling has been associated with decreased sensitivity to MAPK inhibition.

assertion_9 = "Inc(node:Proliferation_b1,Proliferation_b2) / [ ] [ PI3K:ON AKT:ON ] [ compare:PI3K:OFF,AKT:OFF digits:3 comb ]"
assertions_list_no_i_s.append(assertion_9)

Evaluations

results_colorectal = tl.MaBoSSEvaluator.querying(assertions_list_colorectal, file_cfg, file_bnd, i_s_colorectal)
results_melanoma = tl.MaBoSSEvaluator.querying(assertions_list_melanoma, file_cfg, file_bnd, i_s_melanoma)
results_no_is = tl.MaBoSSEvaluator.querying(assertions_list_no_i_s, file_cfg, file_bnd)
results_strong_EGF = tl.MaBoSSEvaluator.querying(assertions_list_strong_EGF, file_cfg, file_bnd, i_s_strong_EGF)

/home/oscar/Documents/MaBoSS/pyMaBoSS/maboss/temporal_logic/evaluator.py:341: UserWarning: Not passing any names in the ouput_setting might make the computing really slow and/or make it crash.
  warnings.warn("Not passing any names in the ouput_setting might make the computing really slow and/or make it crash.")

Evaluations done !

/home/oscar/Documents/MaBoSS/pyMaBoSS/maboss/temporal_logic/evaluator.py:341: UserWarning: Not passing any names in the ouput_setting might make the computing really slow and/or make it crash.
  warnings.warn("Not passing any names in the ouput_setting might make the computing really slow and/or make it crash.")

Display the results

viz_no_is = tl.visualiser.Visualiser(list_queries=assertions_list_no_i_s,list_of_results=results_no_is)
viz_melanoma = tl.visualiser.Visualiser(list_queries=assertions_list_melanoma,list_of_results=results_melanoma)
viz_colorectal = tl.visualiser.Visualiser(list_queries=assertions_list_colorectal,list_of_results=results_colorectal)
viz_strong_EGF = tl.visualiser.Visualiser(list_queries=assertions_list_strong_EGF,list_of_results=results_strong_EGF)
viz_no_is.display_results_and_queries("No initial state") #title is optional
viz_colorectal.display_results_and_queries("Colorectal Cancer")
viz_melanoma.display_results_and_queries("Melanoma")
viz_strong_EGF.display_results_and_queries("EGF strong")