Skip to content

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

@reb-ddm

Description

@reb-ddm

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions