Kappa-Dev / KappaTools

Tool suite for kappa models. Documentation and binaries can be found in the release section. Try it online at
http://kappalanguage.org/
GNU Lesser General Public License v3.0
112 stars 41 forks source link

False detection of "useless molecular ambiguity" #404

Open hmedina opened 7 years ago

hmedina commented 7 years ago

Given the model:

%agent: A(n,m)
'0' A(n,m),A(n,m) <-> A(n!1,m),A(n,m!1) @ 1 {0},1 #first dimerization
'n' A(n,m),A(n,m!_) <-> A(n,m!1),A(n!1,m!_) @ 1 {0},1 #cap n-end with a monomer
'm' A(n!_,m),A(n,m) <-> A(n!_,m!1),A(n!1,m) @ 1 {0},1 #cap m-end with a monomer
'-' A(n!_,m),A(n,m!_) <-> A(n!_,m!1),A(n!1,m!_) @ 1 {0},1 #bind i-mer to j-mer with [i|j]>1
%init: 100 A()

KaSim / WebSim complain about:

+ Building initial simulation conditions...
    -variable declarations
    -rules
    -perturbations
    -observables
    -update_domain construction
    15 (sub)observables 20 navigation steps
    -initial conditions
File "model.ka", line 5, characters 58-59:
    Warning: Useless molecular ambiguity, the rules is always considered as unary.
File "model.ka", line 5, characters 58-59:
    Warning: Useless molecular ambiguity, the rules is always considered as unary.

Given that at line 5 only the forward rule has a unary rate, I'm assuming KaTool is complaining about the forward rule. The rule's LHS can embed in the following:

G = A(n,m!1),A(n!1,m),A(n,m!2),A(n!2,m)

Replacing it with:

G' = A(n,m!1),A(n!1,m!0),A(n!0,m!2),A(n!2,m)

However, G is not a connected graph. -'s LHS can be bimolecular.

pirbo commented 7 years ago

The warning is wrong, the model is not: because internally KaSim does not understand !_, it refines A(n!_,m!./!1),A(n!./!1,m!_) into

Then it complains that molecular ambiguity is useless in the 1st and the 3rd case! (but deal correctly with it in the second case...)

pirbo commented 7 years ago

(and yes because the unary rates is 0 it should even remove completely these cases ...)

feret commented 7 years ago

-> I think the warning should be raised only if none of the refinements of the initial rule has a unary application context. -> This is important to remember whether or not the rule could have been applied in a unary context (even if the unary rate of 0), so as to warn if it was not the case. When a model write 1{0}, I think it is important to have a warning if the rule could not have been applied in a unary context anyway.

Cheers. Jérôme.

Le 2 juin 2017 à 01:39, Pierre Boutillier notifications@github.com a écrit :

(and yes because the unary rates is 0 it should even remove completely these cases ...)

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/Kappa-Dev/KaSim/issues/404#issuecomment-305649740, or mute the thread https://github.com/notifications/unsubscribe-auth/AARts6xF5HV5u8UL337B62F5FiKW_Byoks5r_0vFgaJpZM4NtqOL.

hmedina commented 7 years ago

Ah, so because of the expansion into three unambiguous rules where 2 had no ambiguous molecularity, it printed 2 warnings. I had thought it was printing twice the same warning.

Also, I was under the impression !_ meant something like bound to entity not in this pattern, and so had not considered the first refinement as valid.

feret commented 7 years ago

NO!!!

‘!' means bound to whatever sites (not already specified as free, or as bound to another site). it may be: -> bound to another site with state ! or ? (or a even a binding type). -> bound to an unspecified site in an agent -> bound to a site in a fresh agent.

The same applies with binding types.


In particular, as it has been pointed by Jonathan Hayman:

A(x!),B(x!) -> A(x!_),B(x)

leads to some issue, when applied to A(x!1),B(x!1), since x@A has to be both free and bound after the application of the rule. This has led to the notion of external bonds, which is what you are referring to. It was making the formal results (about subject reduction (when you find an embedding from the lhs and a mixture, the push-out in the SPO semantics is defined, and the result is a mixture, clearer to express and prove)).

Yet, and I fully agree with this decision, we have kept the semantics of !_ as it was. I think it is more consistent with the "do not care do not write" principle. In the rule application that I have mentioned, the former behavior of the simulator has been replaced by a clash (which makes sense).

Le 2 juin 2017 à 08:39, Hector Medina notifications@github.com a écrit :

Ah, so because of the expansion into three unambiguous rules where 2 had no ambiguous molecularity, it printed 2 warnings. I had thought it was printing twice the same warning.

Also, I was under the impression !_ meant something like bound to entity not in this pattern, and so had not considered the first refinement as valid.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/Kappa-Dev/KaSim/issues/404#issuecomment-305703082, or mute the thread https://github.com/notifications/unsubscribe-auth/AARts5idIPHsx64qkAEUO24G6Y0DY45hks5r_64VgaJpZM4NtqOL.