Parametric Kappa Models

[reb-ddm]

Implementation for the paper "Reachability Analysis for Parametric Rule-Based Models".

This pull request allows the definition of parametric models in Kappa: each rule and initial state can be guarded by a boolean formula made of boolean predicates. For example:

#[P && Q] . -> A() @ 1
#[P || Q] . -> B() @ 1

Each rule (and initial state) is activated only if the guard evaluates to true. The static analyzer KaSa computes the relationship between the values of the predicates and the reachable patterns.

Each valuation of the predicates induces a concrete instantiation of the model. An instantiation can be defined by choosing a value (true or false) for each predicate via the directive %guard_param:. The syntax is:

%guard_param: P [true]
%guard_param: Q [false]

If all parameters have a defined value, then the instantiated model can be simulated by KaSim or KaDE. Only the rules and initial states for which the guard evaluates to true are taken into account for the simulation.

Three directives are implemented to automatically exploit the expressibility of the parameters. They represent hypotheses for which it is not yet determined if they are true or false: boolean predicates are added to reflect the potential presence or absence of these hypotheses.

• Conflict between sites: The directive %conflict: A x y modifies the rules such that when the predicate @co-A-x-y is true, there is a conflict between the sites x and y of the agent A. This means that the two sites can only form a bond when the other one is free, i.e., the two sites cannot both be bound at the same time. When @co-A-x-y is false, then the activated rules are exactly the ones that are explicitly defined in the Kappa model.
• Sequential bond: The directive %sequential_bond: A x y represents the hypothesis that x and y can only bind sequentially, i.e., y can only bind to another site when x is already bound. A predicate @sq-A-x-y is added and each rule where y is bound on the right-hand side is modified to include the information that site x is bound (when @sq-A-x-y is true).
• The directive %working_setdefines a set of rules that are each automatically guarded by a fresh predicate of the form @rule-i where i is an increasing index starting at 0. Thus, the static analysis investigates the consequences of the activation or deactivation of each of these rules. This is useful to infer causal relationships between rule applications. Additionally, it can be used to implement an incremental analysis, where removing a rule does not require re-running the whole analysis.