Dead rule detection misses unary/binary rate subtlety

[hmedina]

The GUI (via KaSa I presume) can detect dead rules. However this does not extend to rules that rely on a connecting third party (or parties). Take for example:

%agent: K(c)
%agent: C(k,s)
%agent: S(c)
%init: 1000 (K(), S())
%init: 1000 C()
'R1' K(c[.]),C(k[.]) <-> K(c[1]),C(k[1]) @ 1,1
//'R2' S(c[.]),C(s[.]) <-> S(c[1]),C(s[1]) @ 1,1
'R3' S(),K() -> .,K() @ 0 {1}

The third rule should be marked as dead. Without R2 firing, R3 can't fire. The tool seems to not know that a disconnected contact map and a binary rate of zero guarantee R3 to be dead...

[feret]

As you know, knowing whether a rule is dead in Kappa is undecidable (just encode a two counters machine, and write a rule that require a specific states for the counters). Also if you want to have a reactive UI, this would not be a so good idea to enumerate all the potential biochemical compounds. Thus, we rely on approximation.

Currently, the abstract domains cope with local views, parallel-bonds (when an agent is bound twice, is this necessarily to the same instance of another agent?), site across bonds (are the two states of sites x in A and y in B related when A is bound to B, useful when some sites are used to encode compartments).

There is actually no reasoning about connectivity.

I have a new intern next Monday that will work on this topic. The goal is to build an abstraction to compute lower and upper bound for the potential distance between each pair of agent types. This will solve your issue, but you need to wait, let us say 6 months.