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
108 stars 40 forks source link

`File "core/siteGraphs/edges.ml", line 418, characters 13-19: Assertion failed` #665

Closed hmedina closed 6 months ago

hmedina commented 1 year ago

The model:

%def: "seed" "110028773"

%init: 100 poly()
%init: 5 degrader()
%mod: |poly()| = 90 do $SNAPSHOT "snap.ka" [true] ; $STOP ;
// %mod: |poly()| = 50 do $STOP ;

%agent: poly(head, tail, belly, state{a, b, c})
%agent: degrader(site)

poly(head[.]), poly(tail[.])        <-> poly(head[1]), poly(tail[1])        @ 1.0e-4 {1.0}, 1.0e-2
degrader(site[.]), poly(belly[.])   <-> degrader(site[1]), poly(belly[1])   @ 1.0e-4, 1.0e-2

degrader(site[1/.]), poly(belly[1/.], state{a/b})       @ 1.0e-4
degrader(site[1/.]), poly(belly[1/.], state{b/c})       @ 1.0e-4
degrader(site[1]), poly(belly[1], state{c})-            @ 1.0e-4

Standard output printed:

$ KaSim -i model.ka -d kasim-output
Parsing model.ka...
done
+ simulation parameters
+ Sanity checks
+ Compiling...
+ Building initial simulation conditions...
         -variable declarations
         -rules
         -interventions
         -observables
         -update_domain construction
         15 (sub)observables 6 navigation steps
         -initial conditions
+ Building initial state (105 agents)
Done
+ Command line to rerun is: 'KaSim' '-i' 'model.ka' '-d' 'kasim-output'
122968.94 time units in 227454 eventsFile "core/siteGraphs/edges.ml", line 418, characters 13-19: Assertion failed

KaSim version:

$ KaSim --version
Kappa Simulator: v4.1-97-gb9248b7eb8

Seed was "110028773"; unfortunately trying to produce snapshots of the state just prior to the crash changes the random number trajectory, and I have trouble replicating the crash while producing snapshots. More troublingly, even while keeping the model as described above, with a fixed seed, I'm seeing inconsistent behavior: the assertion fails always after a degradation event (that's the last entry in the trace, as digested by KaTie), but the event number, the time, the identifier of the degradee, are different, as if fixing the seed were not yielding reproducing behavior.

The witness files for these runs, inputs.ka, all have the same value for the seed: %def: "seed" "110028773"

However, they fail at different times & events: ``` hmedina@Onyx:~/Katie/tests/unit/snapshot_start$ KaSim -i model.ka -d kasim-output Parsing model.ka... done + simulation parameters + Sanity checks + Compiling... + Building initial simulation conditions... -variable declarations -rules -interventions -observables -update_domain construction 15 (sub)observables 6 navigation steps -initial conditions + Building initial state (105 agents) Done + Command line to rerun is: 'KaSim' '-i' 'model.ka' '-d' 'kasim-output' 124614.11 time units in 230412 eventsFile "core/siteGraphs/edges.ml", line 418, characters 13-19: Assertion failed hmedina@Onyx:~/Katie/tests/unit/snapshot_start$ KaSim -i model.ka -d kasim-output Parsing model.ka... done + simulation parameters + Sanity checks + Compiling... + Building initial simulation conditions... -variable declarations -rules -interventions -observables -update_domain construction 15 (sub)observables 6 navigation steps -initial conditions + Building initial state (105 agents) Done + Command line to rerun is: 'KaSim' '-i' 'model.ka' '-d' 'kasim-output' 121644.31 time units in 224973 eventsFile "core/siteGraphs/edges.ml", line 418, characters 13-19: Assertion failed hmedina@Onyx:~/Katie/tests/unit/snapshot_start$ KaSim -i model.ka -d kasim-output Parsing model.ka... done + simulation parameters + Sanity checks + Compiling... + Building initial simulation conditions... -variable declarations -rules -interventions -observables -update_domain construction 15 (sub)observables 6 navigation steps -initial conditions + Building initial state (105 agents) Done + Command line to rerun is: 'KaSim' '-i' 'model.ka' '-d' 'kasim-output' 124694.91 time units in 230562 eventsFile "core/siteGraphs/edges.ml", line 418, characters 13-19: Assertion failed ```

For all the traces produced in these runs, KaTIE reports the last event in the trace to have been the degradation of a poly, 29 in this example (I'm using KaTIE's agent identifiers, which do identify agents throughout the simulation)

  "304216": [
    "degrader(site[1]), poly(head[#] tail[#] belly[1] state{c}[#])-",
    "del(poly.29) free(poly.29.head) free(poly.29.tail) free(poly.29.state) free(poly.65.head) free(poly.65.tail)"
  ]

Something happens next that causes the assertion to fail. And since fixing the random seed does not yield reproduceable runs, I'm not sure how to provide a smaller MWE.

feret commented 1 year ago

I think that the problem comes from this rule:

degrader(site[1]), poly(belly[1], state{c})- @ 1.0e-4

This is the Jonathan Hayman's paradox... The degradation of poly should frees the site "site" of the agent "degrader" whereas the rule specifies that it remains bound. The rule should have been rejected by the frontend (or replaced to the following one):

degrader(site[1/.]), poly(belly[1], state{c})- @ 1.0e-4

The simulation works well with the latter rule.

feret commented 1 year ago

Note that this even simpler rule:

degrader(site[1]), poly(belly[1/.], state{a/b}) @ 1.0e-4

is accepted by the frontend.

feret commented 1 year ago

This model is well treated:

%agent: A(x) %init: 1 A(x[1]),A(x[1])

A(x[]),A() -> A(x[]),. @1

(it produces a clash, instead of an exception).

feret commented 1 year ago

TODO: add an additional sanity check in term/lkappa.ml

feret commented 1 year ago

@hmedina please check that it is OK for you (directly in the master branch).

hmedina commented 1 year ago

Nice error message! Very informative and precise.

I can see how the rule can express an unfulfilling command now; I had in mind the order of operations outlined in https://github.com/Kappa-Dev/KappaTools/issues/658, of first performing the bond removal, then the agent degradation, but here the problem was identifying the operations to be performed out of the Kappa statement.

degrader(site[1/.]), poly(belly[1], state{c})- @ 1.0e-4 Is accepted, but in a way, it looks odd to have 1 as "sort of" dangling? This looks to my eye more like a typo, than an intentional statement

degrader(site[1/.]), poly(belly[1/.], state{c})- @ 1.0e-4 Is rejected, with "a modification is forbidden here", even though that's what's happening.

I think:

rule outcome
degrader(site[1]), poly(belly[1], state{c})- @ 1.0e-4 message: side effect
degrader(site[1/.]), poly(belly[1], state{c})- @ 1.0e-4 warning: dangling bond
degrader(site[1/.]), poly(belly[1/.], state{c})- @ 1.0e-4 fully valid
feret commented 1 year ago

There is one firm rule, is that the rhs of a rule should embed to the post-state after application. This is what was violated by your rule. To see if that is the case you need to expand your edit notation into a classic rule.

Thus, as long as you got the agent degradation '-', the interpretation of the edit notation is that there is no longer any link identifier in the corresponding agent. I prefer the message that I put with respect to a dangling bond, since it would have been cryptic to the user.

Since, everything vanishes in a degraded agent, the choice was to forbid any transformation (which would have been discarded by the compiler anyway).

What I can do is to try to update the compiler to accept also this: degrader(site[1/.]), poly(belly[1/.], state{c})- I acknowledge that it may look better to the eyes.

More specifically, I would accept freeing a site in a degraded agent, only if the pending site is also freed in the rule.

Thus in your examples, the second and the third ones would be accepted, while the first one would be rejected with my 'nice' error message.

feret commented 1 year ago

The following rules are now allowed:

degrader(site[1/.]), poly(belly[1], state{c})- @ 1.0e-4 degrader(site[1/.]), poly(belly[1/.], state{c})- @ 1.0e-4 degrader(site[1/.])-, poly(belly[1], state{c})- @ 1.0e-4