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
113 stars 41 forks source link

possibly incorrect deadlock #584

Closed nilsbecker closed 5 years ago

nilsbecker commented 5 years ago

my rule set deadlocks unexpectedly. i have boiled it down to the example below. my expectation is that the two agents in the middle will get rewired back and forth indefinitely so that they keep swapping positions. but maybe i'm not fully getting the semantics of patterns and rules?

%agent:
E(n{a b c left right}, pos{s e}, x{b p}[x.E], y[y.E])

'rewire'
E(x{b}[1/3]), E(x{p}[1/4]), E(x{b}[2/4]), E(x{p}[2/3])
@ 0.0 {1.0}

/* why does this give a deadlock ? */
%init: 1
E(n{left}  , pos{e} , x{b}[1] , y[.]) ,
E(n{a}     , pos{s} , x{p}[1] , y[2]) ,
E(n{a}     , pos{e} , x{p}[3] , y[2]) ,
E(n{right} , pos{s} , x{b}[3] , y[.])

cheers!

nilsbecker commented 5 years ago

i've reduced it a bit further:

%agent:
E(n{a1 a2 left right}, x{b p}[x.E], y[y.E])

'rewire'
E(x{b}[1/3]), E(x{p}[1/4]), E(x{b}[2/4]), E(x{p}[2/3])
@ 0.0 {1.0}

/* why does this give a deadlock ? */
%init: 1
E(n{left}  , x{b}[1] , y[.]) ,
E(n{a1}    , x{p}[1] , y[2]) ,
E(n{a2}    , x{p}[3] , y[2]) ,
E(n{right} , x{b}[3] , y[.])

this gives erratic behavior. after around 8 successful swaps or so, i get a deadlock?!

nilsbecker commented 5 years ago

using kappapp 4.1-beta3 on os x

vd1 commented 5 years ago

it may be a bug but note that in general deadlocks are not always true deadlocks - if the simulator is clashing repeatedly it will give up and say "deadlock". There maybe remaining events that the simulator was just not lucky enough to find. So that explains the varying number of steps you obtain (which otherwise could look bizare as the embedded discrete-time chain is deterministic - so where is this randomness coming from, one would wonder).

On Wed, 15 May 2019 at 11:10, nilsbecker notifications@github.com wrote:

i've reduced it a bit further:

%agent: E(n{a1 a2 left right}, x{b p}[x.E], y[y.E])

'rewire' E(x{b}[1/3]), E(x{p}[1/4]), E(x{b}[2/4]), E(x{p}[2/3]) @ 0.0 {1.0}

/ why does this give a deadlock ? / %init: 1 E(n{left} , x{b}[1] , y[.]) , E(n{a1} , x{p}[1] , y[2]) , E(n{a2} , x{p}[3] , y[2]) , E(n{right} , x{b}[3] , y[.])

this gives erratic behavior. after around 8 successful swaps or so, i get a deadlock?!

— 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/584?email_source=notifications&email_token=AADQELWIWBXWC5D3C3LGV63PVPHPZA5CNFSM4HNBD3WKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGODVOBBHA#issuecomment-492572828, or mute the thread https://github.com/notifications/unsubscribe-auth/AADQELT3XXMY2XZS3OQCLM3PVPHPZANCNFSM4HNBD3WA .

nilsbecker commented 5 years ago

hmm. the fact that the simulator gives up based on a heuristic is somewhat disconcerting. this sounds like the simulation is not exact (i.e. guaranteed to give the precisely correct statistics, like pure gillespie simulation) but rather approximate: the result depends on the occurrence of clashes and their interpretation by the simulation loop logic.

is there a way to avoid such a premature exit, e.g. by restricting the type of rules? can the ambiguous rule be responsible? note that i explicitly only allowed unimolecular reactions, hoping that this would eliminate complications coming from the search for bimolecular instances of a rule (i also need the restriction to unimolecular in the full version of my problem)

nilsbecker commented 5 years ago

ps. in the simulator interface, i get the information that 0% of event loops were productive and that 'clashing instance' was the cause in 100% of the cases -- i do not know what 'clashing instance' means.

jkrivine commented 5 years ago

Here is a hint of the problem. The following model does NOT deadlock:

%agent: E(x{b p}[x.E], y[y.E])

'rewire' E(x{b}[1/3]), E(x{p}[1/4]), E(x{b}[2/4]), E(x{p}[2/3]) @ 1 {inf}

/ why does this give a deadlock ? / %init: 1 E(x{b}[1] , y[.]) , E(x{p}[1] , y[2]) , E(x{p}[3] , y[2]) , E(x{b}[3] , y[.])

So it seems that KaSim is unhappy with the only binary rate being set to 0 (it does not take unary rate into account for detecting deadlocks).

Le 15 mai 2019 à 14:54, nilsbecker notifications@github.com a écrit :

ps. in the simulator interface, i get the information that 0% of event loops were productive and that 'clashing instance' was the cause in 100% of the cases -- i do not know what 'clashing instance' means.

— 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/584?email_source=notifications&email_token=AACHTDVLLX2KGMFJDG2EK73PVQBZ3A5CNFSM4HNBD3WKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGODVOR73Y#issuecomment-492642287, or mute the thread https://github.com/notifications/unsubscribe-auth/AACHTDX5OFAELERD5AHJZS3PVQBZ3ANCNFSM4HNBD3WA.

nilsbecker commented 5 years ago

ah, interesting! what i really want is just to disallow binary reactions -- in my full problem i get multiple complexes but i don't actually want any reactions between complexes, just rewirings within them. (so your test example would not be a workaround for my full problem.)

jkrivine commented 5 years ago

It was not meant to be a workaround but more a guidance for debugging. However because in my example unary reaction are given infinite rate, no reaction between different complex will trigger as long as unary ones are possible.

Le 15 mai 2019 à 15:14, nilsbecker notifications@github.com a écrit :

ah, interesting! what i really want is just to disallow binary reactions -- in my full problem i get multiple complexes but i don't actually want any reactions between complexes, just rewirings within them. (so your test example would not be a workaround for my full problem.)

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/Kappa-Dev/KaSim/issues/584?email_source=notifications&email_token=AACHTDR4PT4FG4UGVD43MKLPVQEE3A5CNFSM4HNBD3WKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGODVOTWUI#issuecomment-492649297, or mute the thread https://github.com/notifications/unsubscribe-auth/AACHTDWXPELCPBI63V7TG7DPVQEE3ANCNFSM4HNBD3WA.

nilsbecker commented 5 years ago

fair enough. i guess it might be possible to construct a workaround for my full use-case by using the precedence of infinite-rate reactions in some way. but better would be to have no need for a workaround. is my originally reported behavior to be considered a bug?

feret commented 5 years ago

I think that we should wait for @pirbo’s answer. He is the main engineer of the actual simulator, and he knows precisely how intra VS extra molecular interactions and clashes, are handled.

The use of clashes is a standard technique in stochastic simulation. It consists in over-estimating the set of potential events, but checking at run-time if the ones that are selected are valid. Due to nice properties of exp distributions, it is semantically transparent: it induces the same Markov chain.

Here you have two potential sources of clashes: 1) the selection of the two pairs of connected A, (that appears in the las of your rules) are made independently. If one A is used twice (i.e. your two pairs of A overlaps), then it is a clash. 2) Two patterns that should be connected somehow are not, or some patterns that should not be connected are.

The source 2) may not happen in your model. Thus I guess this is the first source. To avoid this, you could refine your rule to avoid clashes. If you specify that the first A has his state n in state left, and the last one n in state right, then it should not change your model (maybe you need to update the rate accordingly). But now you may not have clashes anymore.

Indeed the following model…

%agent: E(n{a1 a2 left right}, x{b p}[x.E], y[y.E])

'rewire' E(x{b}[1/3],n{left}), E(x{p}[1/4]), E(x{b}[2/4],n{right}), E(x{p}[2/3]) @ 0.0 {1.0}

/ why does this give a deadlock ? / %init: 1 E(n{left} , x{b}[1] , y[.]) , E(n{a1} , x{p}[1] , y[2]) , E(n{a2} , x{p}[3] , y[2]) , E(n{right} , x{b}[3] , y[.])

...makes no clash.

Then to know why the first version of the model crashes with a deadlock, we should wait for @pirbo’s enlightenment. But I would guess this is not an intended behaviour.


Jerome Feret DI - Ecole Normale Superieure 45, rue d'Ulm 75230 Paris Cedex 5

phone: +33 1 44 32 37 66 fax : +33 1 44 32 21 51 mail : feret@ens.fr

Le 15 mai 2019 à 14:54, nilsbecker notifications@github.com a écrit :

ps. in the simulator interface, i get the information that 0% of event loops were productive and that 'clashing instance' was the cause in 100% of the cases -- i do not know what 'clashing instance' means.

— 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/584?email_source=notifications&email_token=AACG3M2AC5ONEQ6W5ZVAZHDPVQBZ3A5CNFSM4HNBD3WKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGODVOR73Y#issuecomment-492642287, or mute the thread https://github.com/notifications/unsubscribe-auth/AACG3M4SOMNT7TPYP6ACQ6TPVQBZ3ANCNFSM4HNBD3WA.

nilsbecker commented 5 years ago

@feret thanks for this detailed answer! i think i understand the concept of a clash a bit better now.

iiuc, as long as clashes are detected correctly, if there is also a non-clashing proposal, one would always end up with a valid next event in principle. however, if the set of potential events is grossly over estimated, one might have to wait arbitrarily long to hit a valid event, and the simulation has no way of deciding if the unsuccessful events are going to terminate -- is this where a heuristic to stop searching is applied? if so, this would indicate that the simulation is exact as long as it does not stop, but it may stop wrongly prematurely in some cases. correct?

1) the selection of the two pairs of connected A, (that appears in the las of your rules) are made independently. If one A is used twice (i.e. your two pairs of A overlaps), then it is a clash.

this brings me to a question about semantics in kappa i had: are the agents on the LHS of a rule always interpreted as pairwise distinct? your answer makes me think yes. since each agent may get modified differently on the RHS of the rule, this seems to be the only interpretation that makes sense. (and the simulation loop then has to try at runtime if they are really distinct). correct?

your example looks promising. i would have to reformulate my rules such that it is clear from the rule that all agents are in fact distinct. unfortunately, the full problem involves a whole chain in which many values of the state n appear: {left a b c d e f g h i right}, and rewiring is possible anywhere. the rule set would seem to explode combinatorically if i have to list all possible options of four distinct elements with these names -- i was hoping to be able to avoid that.

feret commented 5 years ago

@feret thanks for this detailed answer! i think i understand the concept of a clash a bit better now.

iiuc, as long as clashes are detected correctly, if there is also a non-clashing proposal, one would always end up with a valid next event in principle. however, if the set of potential events is grossly over estimated, one might have to wait arbitrarily long to hit a valid event, and the simulation has no way of deciding if the unsuccessful events are going to terminate -- is this where a heuristic to stop searching is applied? if so, this would indicate that the simulation is exact as long as it does not stop, but it may stop wrongly prematurely in some cases. correct?

I do not know, let us wait for @pirbo confirmation.

  1. the selection of the two pairs of connected A, (that appears in the las of your rules) are made independently. If one A is used twice (i.e. your two pairs of A overlaps), then it is a clash.

this brings me to a question about semantics in kappa i had: are the agents on the LHS of a rule always interpreted as pairwise distinct? your answer makes me think yes. since each agent may get modified differently on the RHS of the rule, this seems to be the only interpretation that makes sense. (and the simulation loop then has to try at runtime if they are really distinct). correct?

your example looks promising. i would have to reformulate my rules such that it is clear from the rule that all agents are in fact distinct. unfortunately, the full problem involves a whole chain in which many values of the state n appear: {left a b c d e f g h i right}, and rewiring is possible anywhere. the rule set would seem to explode combinatorically if i have to list all possible options of four distinct elements with these names -- i was hoping to be able to avoid that.

yes, agents of the lhs of your rule must be mapped injectively to the agents of your state.

pirbo commented 5 years ago

So, stupid bug ... HUGE CONSEQUENCES!

What @vd1 said was only partially true.

Now, in the case of unary rules, the computation of the exact number of instances was done correctly but then the refined activity of the rule was computed as: exact_number_of_instances * activity_of_a_binary_instance_of_the_rule!!!

I immediately need to sync with @hmedina to see how deep the consequences are in his case but If you find my body cut in 5cm^2 pieces spread all over Boston, consider that I deserved it...

nilsbecker commented 5 years ago

oops... at least the bug is squashed now! good luck!

what's a good way to update kappapp to HEAD? i am familiar with opam/ocaml so i could potentially compile it but i don't know what the dependencies are for the GUI. or i could wait for another beta?

pirbo commented 5 years ago

A kappapp corresponding to the last master is build automatically by the continuous integration and available at https://tools.kappalanguage.org/nightly-builds/

The dependencies to build the UI are opam install -y lwt_react tyxml-ppx js_of_ocaml-lwt js_of_ocaml-tyxml atdgen. Then the magic make incantation is make Kappapp.app under OSX or make Kappapp.tar.gz under linux. (These makefile rules require an internet connection)

nilsbecker commented 5 years ago

this worked! i pinned the git repo with opam and then built the os x app in the .opam/.../build tree. i get a shiny GUI which does not deadlock in this example anymore. great!