KappaTools icon indicating copy to clipboard operation
KappaTools copied to clipboard

Dead site throws an error in KaSa when it is bound on the left-hand side of a rule

Open reb-ddm opened this issue 7 months ago • 0 comments

example Kappa model that throws the error:

%agent: A(x y z)
%agent: B(x y)

%init: 1 A(),B()

A(y[.]), A(y[.]), B(y[.]) -> ., A(y[1]), B(y[1]) @ 1
A(y[.]), A(z[_],x[.],y[.]), B(y[.]) -> ., A(x[.],z[_],y[1]), B(y[1]) @ 1

When I analyze this file with KaSa (on the master branch), it throws the following error message:

error: file_name: core/KaSa_rep/frontend/preprocess.ml; message: line 1457; exception:Exit error: file_name: core/KaSa_rep/reachability_analysis/common_static.ml; message: line 562; exception:Exit

The error is thrown because A is considered as a dead agent by KaSa, as one of its sites (z) is dead (see also Preprocess.translate_view, where each agent is translated to either Dead_agent if some sites are dead or Agent if not).

The analyzer should not throw an exception. It is enough to print that the second rule is reachable, which it already correctly does.

reb-ddm avatar Jun 30 '25 09:06 reb-ddm