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

Dumping duplicate snapshots #328

Closed hmedina closed 7 years ago

hmedina commented 7 years ago

I'm getting duplicate snapshots with a repeated perturbation: %mod: repeat ([E] [mod] 100) = 0 do $SNAPSHOT until [false]

With the invocation: KaSim -i model.ka -l 5000 -u events

And I see several snapshots got duped, for example snap_2700.ka and snap_2700~0.ka are identical. With the above invocation, out of the 51 snapshots, 4 got requested twice.

That perturbation appears in the manual, section 6.1.2

pirbo commented 7 years ago

I need more information. I do not see duplicated snapshots if I add the problematic line in the file models/abc.ka of the repo.

hmedina commented 7 years ago

The code:

%var: 'scale' 0.01
%var: 'nanoAvoVol' 1350 * 'scale'
%var: 'γon' 1.0e-4 / 'scale'
%var: 'γoff' 1.0e-2
%var: 'pf' 1.0
%agent: A(a,b,c)
%agent: B(a,b,c)
%agent: C(a,b,c)

A(a), A(a) <-> A(a!1), A(a!1) @ 'γon' /2 {'pf'}, 'γoff' /2
B(b), B(b) <-> B(b!1), B(b!1) @ 'γon' /2 {'pf'}, 'γoff' /2
C(c), C(c) <-> C(c!1), C(c!1) @ 'γon' /2 {'pf'}, 'γoff' /2
A(b), B(a) <-> A(b!1), B(a!1) @ 'γon' {'pf'}, 'γoff'
A(c), C(a) <-> A(c!1), C(a!1) @ 'γon' {'pf'}, 'γoff'
B(c), C(b) <-> B(c!1), C(b!1) @ 'γon' {'pf'}, 'γoff'

%init: 50 * 'nanoAvoVol' (A(), B(), C())
%mod: repeat ([E] [mod] 100) = 0 do $SNAPSHOT "snap_".[E].".ka" until [false]

With the invocation: KaSim -i model.ka -d snaps -l 5000 -u events Using Kappa Simulator: DomainBased-2445-g34bb01b

Produces this: capture

pirbo commented 7 years ago

And the culprits are ....... null events :-)

The simulator applies perturbations, advance time, try to apply a rule but pick a clashing instance end of a loop next event loop: apply perturbations, precondition is still valid because [E] has not changed, snapshot is regenerated !

It is tempting to say " perturbations should not be applied after null events" but is that correct? Time has increased between the 2 attempts, a precondition may be false on the first attempt but true on the second one. Should we apply the corresponding perturbation "now" or after the next productive event (because if there were no overappriximation this opportunity to apply would not exists)?

jkrivine commented 7 years ago

This would not happen with perturbation dependencies as only time dependant perturbation would be awaken by a null event

Le 4 janvier 2017 19:33:57 GMT+01:00, Pierre Boutillier notifications@github.com a écrit :

And the culprits are ....... null events :-)

The simulator applies perturbations, advance time, try to apply a rule but pick a clashing instance end of a loop next event loop: apply perturbations, precondition is still valid because [E] has not changed, snapshot is regenerated !

It is tempting to say " perturbations should not be applied after null events" but is that correct? Time has increased between the 2 attempts, a precondition may be false on the first attempt but true on the second one. Should we apply the corresponding perturbation "now" or after the next productive event (because if there were no overappriximation this opportunity to apply would not exists)?

-- You are receiving this because you are subscribed to this thread. Reply to this email directly or view it on GitHub: https://github.com/Kappa-Dev/KaSim/issues/328#issuecomment-270448409

-- Envoyé de mon appareil Android avec K-9 Mail. Veuillez excuser ma brièveté.

pirbo commented 7 years ago

OK but this is not the remaining question! Question is

Should we apply time dependant perturbation as soon as possible (i.e. potentially just after a null event) or after the next productive event?

feret commented 7 years ago

If I remember well, the history of perturbation semantics, I would suggest that we do time-dependent events as soon as possible. I understand that we are not exact w.r.t Ty’s semantics (that would require to backtrack when the current event is applied after that the perturbation is enabled), but at least we should be as precise as possible in our discrete world.

Here is a proposition for the description of the semantics: "The perturbation occurs as soon as the precondition is satisfied. When the precondition gets satisfied between two events, the perturbation is either applied immediately when applicable or at worse just after the next event (the choice being left to the simulator for the sake of efficiency)." (Should we specified what happens when the perturbation becomes enabled exactly at the same moment as the event ?)

Le 5 janv. 2017 à 04:50, Pierre Boutillier notifications@github.com a écrit :

OK but this is not the remaining question! Question is

Should we apply time dependant perturbation as soon as possible (i.e. potentially just after a null event) or after the next productive event?

— 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/328#issuecomment-270557731, or mute the thread https://github.com/notifications/unsubscribe-auth/AARtswSJtCbI6n3eoIToYcIQt_RX-fG7ks5rPGiWgaJpZM4LaHgk.

jkrivine commented 7 years ago

A null event is a perfectly legit event and perturbations should be applied after each event (if possible). It turns out that a null event does not modify the state but only the clock. So there is no need to try any perturbation that is not time dependent after a null event. So yes it does answer the question. What Jerome says is that if the time dependence is not of the form T=k then the spec should say the perturbation is applied after the first event for which the precondition is satisfied

feret commented 7 years ago

I do not understand why null events should be considered in the semantics.

In a Markov chain, the activity can be over approximated provided that the random draws can recover the probability to be in the real activity range (as opposed as to be in the over-approximation part). The interest being that there is no need to compute these quantities explicitly (Monte Carlo spirit). This allows for tuning the trade-off between what is computed before-hands (before we know what the next event is) and what is computed when the next event is selected (and its validity is checked). Also the structure of the so over-approximated activity is usually more convenient than the exact one.

Thus, the choice of introducing potential null events is a parameter of the simulation methods, but I do not think the semantics should refer to them.

Having said that, I thought it was important to have a semantics definition which matches what could be implemented in the simulator (I agree that implementing faithfully the time-continuous trace semantics is not a realistic option) hence not referring to null events.

Le 5 janv. 2017 à 10:45, Krivine notifications@github.com a écrit :

A null event is a perfectly legit event and perturbations should be applied after each event (if possible). It turns out that a null event does not modify the state but only the clock. So there is no need to try any perturbation that is not time dependent after a null event. So yes it does answer the question. What Jerome says is that if the time dependence is not of the form T=k then the spec should say the perturbation is applied after the first event for which the precondition is satisfied

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

feret commented 7 years ago

Two minor things: -> There is a typo I think in the manual, p39, just before sec 6.1.1.

"Therefore the only time dependent precondition with an equality test that is allowed in KaSim has to be of the form [T] =n with n ∈ N. For instance: %mod: [T]=10 do $STOP will interrupt the simulation after exactly 10 time units."

We can use any floating point number (not only natural numbers), cannot we ?

-> A perturbation can only be fired once per event loop. (p37)

This is not clear that everybody has the same definition for the event loop, and I have not found which version of the definition is used, in the handbook. It should be written somewhere (maybe it is but I have not found where), whether or not triggering a null event count as one iteration of the event loop, or not.