Whatever symbols for link state [#] (for whatever state bound or not), [_] (for bound to some site), may also induce side effects when they are not preserved in the RHS of a rule, as in

or

To avoid mistakes, sites and states mentioned on the left must be exactly the same as sites mentioned on the right. Use the explicit “whatever” [#] state when needed.

2.5.2 Edit notation rules

Near any modified element, modification is specified. Created agents are postfixed by a $+$. Degraded agents are postfixed by a $-$. Site modifications are described by writing the new (linking or internal) state after the symbol $∕$ inside the (curly/squared) bracket. Therefore, $∕.$ (inside squared brackets) means that the site becomes free, $∕9$ means that the site becomes part of link $9$ and $∕zzz$ inside curly brackets means that the new internal state of the site is $zzz$.

Here are all the rules mentioned above (+1 extra) translated in this unambiguous notation:

2.5.3 Rates

Kappa rules are equipped with one (or two) kinetic rate(s). A rate is an algebraic expression (often simply a real number) evaluated as such, called the individual-based or stochastic rate constant, it is the rate at which the corresponding rule is applied per instance of the rule. Its dimension is the inverse of a time $\left[T^{-1}\right]$.

The stochastic rate is related to the concentration-based rate constant $k$ of the rule of interest by the following relation:

where $V$ is the volume where the model is considered, $\mathcal{𝒜}=6.022\cdot 10^{23}$ is Avogadro’ s number, $a\ge 0$ is the arity of the rule (i.e. $2$ for a bimolecular rule).

In a modelling context, the constant $k$ is typically expressed using molars $M:=\mathit{m}oles{l}^{-1}$ (or variants thereof such as $\mu M$, $nM$), and seconds or minutes. If we choose molars and seconds, $k$’ s unit is ${\mathit{M}}^{1-a}{\mathit{s}}^{-1}$, as follows from the relation 2.1.

Concentration-based rates are usually favoured for measurements and/or deterministic models, so it is useful to know how to convert them into individual-based ones used by KaSim. Here are typical volumes used in modelling:

• Mammalian cell: $V=2.2510^{-12}l$ ($1l=10^{-3}{m}^3$), and $\mathcal{𝒜}V=1.3510^{12}$.

  A concentration of $1M$ in a mammalian cell volume corresponds to $1.3510^{12}$ molecules; $1nM\approx 1350$ molecules per cell.

• Yeast cell (haploid): $V=410^{-14}l$, and $\mathcal{𝒜}V=2.410^{10}$.

  A concentration of $1M$ in a yeast cell volume corresponds to $2.410^{10}$ molecules; $1nM\approx 24$ molecules per cell. The volume is doubled in a diploid cell.

• E. Coli cell: $V=10^{-15}l$, and $\mathcal{𝒜}V=10^8$.

  A concentration of $1M$ in a yeast cell volume corresponds to $10^8$ molecules; $10^{n}M\approx 1$ molecule per cell.

The table 2.4 lists typical ranges for deterministic rate constants and their stochastic counterparts assuming a mammalian cell volume.

2.5.4 Ambiguous molecularity

Using a Kappa rule of the form A(x[.]),B(y[.])$\to \dots$ @ $\gamma$ is not a good practice, where this rule could be applied in a context where A and B are sometimes already connected and sometimes disconnected. This would lead to an inconsistency in the definition of the kinetic rate $\gamma$ which should have a volume dependency in the former case and be volume independent in the latter case (e.g. see Section 2.5.3).

This sort of ambiguity should be resolved, if possible, by refining the ambiguous rule into cases that are either exclusively unary or binary. Each refinement having a kinetic rate that is consistent with its molecularity. Note that in practice, for models having a large number of agents, it is sufficient to assume that the rule A(x[.]),B(y[.])$\to \dots$ @ $\gamma$ will have only binary instances. In this case, it suffices to consider the approximate model:

There exist systems where enumerating unary cases becomes impossible or where the approximation on binary instances is wrong. As an alternative, one should use the Kappa notation for ambiguous rules:

• 'my rule'Kappa_expression $\to$ Kappa_expression @${\gamma }_2\left\{k_1\right\}$

which will tell KaSim to apply the rule named 'my rule' with a rate ${\gamma }_2$ for binary instances and a rate $k_1$ for unary instances.

The obtained model will behave exactly as a model in which the ambiguous rule has been replaced by unambiguous refinements. However the usage of such rule slowdowns simulation in a significant manner depending on various parameters (such as the presence of large polymers in the model). We give below an example of a model utilizing binary/unary rates for rules¹ .

Notice at lines 10-12 the use of binary/unary notation for rules. As a result binding between freely floating agents will occur at rate 'k2' while binding between agents that are part of the same complex will occur at rate 'k1'. Line 21 contains a intervention that requires KaSim to stop the simulation after 10,000 events and output the list of molecular species present in the final mixture as a dot file (e.g. see Section 2.7) that we give in Figure 2.1.

For rules with unary rates, one can also specify a horizon. For example in the following rule:

the unary rate is applied only when the agents $A$ and $B$ are at a horizon $5$ (or closer), of each other. Horizon is an algebraic expression. It is always truncated to a positive integer during simulation. This feature can change in the future.

2.5.5 Hybrid rules

In Kappa, there can be a special treatment of entities that cannot bind anything: tokens. Tokens can only appear or disappear, they are typically used to represent small particles such as ions, ATP, etc.

Tokens may have a continuous concentration.

Token signatures are declared using a statement of the form:

It is possible to mix agents and tokens in hybrid rules (which may also be bi-directional). A hybrid rule has the following form:

• Kappa_expression | token_expression $\to$ Kappa_expression | token_expression @ rate

Token expressions follow the grammar in Table 2.6.

Using Kappa hybrid rules, one may declare that an action has effects on the concentration of some particles of the system. For instance, a rule may consume atp, calcium ions, etc. It would be a waste of memory and time to use discrete agents to represent such particles. Instead one may declare tokens using declarations of the form:

One may then use these tokens in conjunction with a classical rule using the hybrid format:

When applied, the above rule will consume 0.2 atp token and produce 0.1 adp token. Note that as specified by the grammar given in Table 2.6, the number of consumed (and produced) tokens can be given by a sum of the form:

• lhs | a${}_1$ t${}_1$, ..., a${}_n$ t${}_n$ $\to$ rhs | a${}_1^{\prime }$ t${}_1^{\prime }$, ..., a${}_k^{\prime }$ t${}_k^{\prime }$ @ r

where each $a_i,a_i^{\prime }$ is an arbitrary algebraic expression (e.g. see Table 2.2) and each $t_i,t_i^{\prime }$ is a declared token. In the above hybrid rule, denoting by $n_i,n_i^{\prime }$ the respective evaluation of $a_i$ and $a_i^{\prime }$, the concentration of token $t_i$ will decrease from $n_i$ and the concentration of token $t_i^{\prime }$ will increase from $n_i^{\prime }$.

Importantly, the activity of a hybrid rule is still defined by |lhs|*r, where |lhs| is the number of embeddings of the LHS of the rule in the mixture, and does not take into account the concentration of the tokens it mentions. It is however possible to make its rate explicitly depend on the concentrations of the tokens using a variable rate.

Consuming $t$ tokens is strickly equivalent to producing $-t$ tokens. All variations in amount of tokens can be written on the RHS of rules. This is what is done in edit notation when tokens are used:

The variations make clear that the simulator does not check that the consumed amount of token is available. It consumes tokens even if the quantity becomes then negative!

2.6 Initial conditions

The initial mixture to which rules in the KF will be applied are declared as follows:

• %init: algebraic_expression Kappa_expression

or:

• %init: algebraic_expression token_name

where algebraic_expression is evaluated before initialization of the simulation (hence all token and Kappa expression values in the expression are evaluated to 0). This will add to the initial state of the model multiple copies of the graph described by the Kappa expression. The DCDW convention allows us not to write the complete interface of added agents (the remaining sites will be completed according to the agent’s signature). For instance:

will add 1000 instances of A in its default state A(x[.],y{u}[.],z{e0}[.]), 1000 instances of A in state A(x[.],y{p}[.],z{e0}[.]) and a concentration of 0.39 mM of calcium ions. Recall that the concentration of calcium can be observed during simulation by using the expression |ca2+|. As any other declaration, %init can be used multiple times, and agents will add up to the initial state.

2.7 Intervention language

Getting something out of a model is done like in lab experiment through intervention.

Each intervention directive is splitted in 4 parts:

clock

When trying to intervene should be considered

condition

what is the condition under which the intervention is triggered

intervention

what are the interventions

repeatition

if the intervention is triggered, under what condition should it be still tried afterward

There are 3 categories of intervention:

modification

where the model is changed at the time of trigger (a special rule applied, a variable changed, the simulation stopped)

immediate measurement

where a measure is taken at the time of trigger (value of %plot printed, the current status of the mixture output, ...)

continuous measurement switch

where you start or stop a measurement at time of trigger

They are all described in detail below.

2.7.1 directive syntax

The general syntax is

• %mod: alarm float boolean_expression do effect_list repeat boolean_expression

for

• %mod: clock condition do intervention repeat repeatition

and syntactic sugar detailed below is provided.

Boolean_expression and effect_list are defined by the grammar given in Table 2.7 (the operator rel can be any usual binary relation in $\left\{<,=,>\right\}$ and algebraic expressions are defined in Table 2.2).

There are 2 kind of clocks, an event based one and simulation time ones.

The event based one has the empty string for syntax: if nothing is written for clock, it uses the event based clock. It fires at the beginning of the simulation and every time a rule has just fired.

The time based one syntax is alarm float, it fires every amount of time unit given by the float (including at [T]=0).

For example %mod: alarm 2.3 [true] do $PLOTENTRY; repeat [true] will print a line in the data file every 2.3 time unit of simulation whereas %mod: |A()| > 1000 do $PLOTENTRY; repeat |B(x[_])| < |B(x[.])| will do it every event where there is more than 1000 A up to the first event where (there is more than 1000 A) and the number of |B(x[_])| becomes bigger than the number of |B(x[.])|.

When the conditions of several interventions that are tested at the same moment are satisfied simultanously, interventions are triggered in the order in which they have been declared in the KF. A intervention can only be fired once per event loop.

2.7.2 shortcuts

If the repeat keyword and the repeat condition are ommited, it is assumed that it is repeat [false] aka a one-shot intervention.

If the (pre)condition is ommited, it is considerated to be [true] unless both conditions are ommited and a clock is provided. In this case the implicit condition is [T] > 0 so that %mod: alarm 5.8 do effects is somehow a ’at’ operator. It means “do effects at [T] = 5.8”.

2.7.3 Model modification

Applying a rule during a simulation

Special cases: simply adding or deleting agents Continuing with the ABC model, the intervention effect: $ADD n C(x1~p) will add $n\ge 0$ instances of C with x1 already in state p (and the rest of its interface in the default state as specified line 4 of ABC.ka). Also the intervention effect: $DEL |B(x!_)| B(x!_) will remove all Bs connected to some agent from the mixture.

There are various ways one can use interventions to study more deeply a given Kappa model. A basic illustration is the use of a simple intervention to let a system equilibrate before starting a real simulation. For instance, as can be seen from the curve given in Fig. 1.1, the number of AB complexes is arbitrarily set to 0 in the initial state (all As are disconnected from Bs in the initial mixture). In order to avoid this, one can modify the Kappa file in the following way: one sets the initial concentration of C to 0 by deleting line 22. Now one introduces Cs after 25 t.u using the intervention: %mod: [T]=25 do $ADD 10000 C();.

The modified Kappa file is available in the source repository, in the model/ directory (file abc-pert.ka). Run a simulation again (a bit longer) by entering in the command line:

• KaSim ABC-pert.ka -l 300 -p 0.3 -o abc2.out

one obtains the curve given in Fig. 2.2.

Updating kinetic rates on the fly

Any variable between simple quotes can be updated during a simulation using a declaration of the form: %mod: ’Cpp’> 500 do $UPDATE ’k_on’0.0;

This intervention will be applied whenever the observable 'Cpp' will become greater than 500. Its effect will be to set the on rate of all binding rules to 0. Note that, according to the grammar given in Table 2.7, one may use any algebraic expression as the new value of the variable. For instance: %mod: ’Cpp’> 500 do $UPDATE ’k_on’’k_on’/100; will cause the on rate of all rules to decrease a hundred fold. Note that, it is possible to override the kinetic rate of a specific rule: in our ABC example, the declaration: %mod: ’Cpp’> 500 do $UPDATE ’a.b’inf; will set the kinetic rate of rule 'a.b' to infinity.

Interrupt simulation

The intervention $STOP will interrupt the simulation. It returns the hand to the user if one run in interactive mode or terminates the run in batch mode.

The intervention $STOP "final_state.ka" will in addition produce a snapshot of the last mixture.

2.7.4 Model immediate examination

Advanced and/or experimental examinations are listed in chapter 5.

Get a snapshot of the mixture

A snapshot is an instant photography of the current state of the mixture (a dump of the state at a given moment in the simulation).

A snapshot is suitable as an initial condition for a model. In the previous example, we let the system evolve for some time without its main reactant C in order to let other reactants go to a less arbitrary initial state. One may object that this way of proceeding is CPU-time consuming if one has to do this at each simulation.

An alternative is to use the $SNAPSHOT primitive that allows a user to export a snapshot of the mixture at a given time point as a new (piece of) Kappa file. For instance, the declaration: %mod: [E-]/([E]+[E-])>0.9 do $SNAPSHOT "prefix"; will ask KaSim to export the mixture the first time the percentage of null events reaches 90%. The exported file will be named prefix_$n$.ka where $n$ is the event number at which the snapshot was taken. One may also use a string_expression to construct any prefix using local variables.

One may omit to define a prefix and simply type: %mod: [E-]/([E]+[E-])>0.9 do $SNAPSHOT; in which case the default prefix snap.ka will be used for naming snapshots.

If the name already exists, a counter will be appended at the end of the file to prevent overwriting. Snapshots can be performed multiple times, for instance every 1,000 events, using the declaration:

which results in KaSim producing a snapshot every 1000 (productive) events until the simulation ends.

Note that instead of producing Kappa files, one may use snapshot interventions to produce an image of the mixture in the dot/html format using the parameter by specifying the extention in the name skeleton (%mod: [E-]/([E]+[E-])>0.9 do $SNAPSHOT "snap.dot";).

Printing values during a simulation

The effect $PRINT string_expression >string_expression enables one to output values during a computation to:

• standard output if the second string_expression and the > are ommited,
• to the file specified by the second string_expression otherwise.

For instance:

will ask KaSim to output the value of token A in a file "token_$n$.dat" which changes at each new productive event, each time its value gets below 0.

Add an entry in the output data

The effect $PLOTENTRY outputs a line with the current value of observables in the data file. For example, %mod: repeat [E] [mod] 10 = 0 do $PLOTENTRY; until [false] will store the value of observables every 10 productive events.

Chapter 3
The Kappa tools

3.1 The KaSim engine

KaSim is a stochastic simulator of rule-based models [13, 12, 14] written in Kappa. KaSim takes one or several Kappa files as input and generates stochastic trajectories of various observables. KaSim implements Danos et al’s implicit state simulation algorithm [10] which adapts Gillespie’s algorithm [21, 22] to rule-based models.

A simulation event corresponds to the application of a rewriting rule, contained in the Kappa files, to the current graph (also called a mixture). At each step, the next event is selected with a probability which is proportional to the rate of the rule it is an event of. If there are no events, i.e. if none of the rules apply to the current state of the system, one has a deadlock. Note that a given rule will in general apply in many different ways; one says it has many instances. The activity of a rule is the number of its instances in the current mixture multiplied by its rate. The probability that the next event is associated to a given rule is therefore proportional to the activity of the rule. Rule activities are updated at each step (see Fig. 3.1). Importantly, the cost of a simulation event is bounded by a constant that is independent of the size of the graph it is applied to [10].

3.2 The KaSa static analyser

KaSa is a static analyser tool of rule-based models [13, 12, 14] written in Kappa. KaSa takes one or several Kappa files as input and some command line options to toggle on/off some specific static analysis. Currently, KaSa can compute the contact map and the influence map. It can perform reachability analysis [17, 11] as well.

A graphical interface is proposed to navigate through the various options and utilities of KaSa. The compilation of this interface requires labltk and, in particular, tk-dev.

3.3 The KaDE ODEs generator

KaDE is a tool to compile rule-based models [13, 12, 14] written in Kappa into systems of ordinary differential equations, or equivalently into reaction networks. It also supports some model reduction techniques, that may reduce the dimension of the ODEs (or the number of different bio-molecular species in reaction networks).

KaDE takes one or several Kappa files and uses some command line options in order to select a backend format, tune the semantics, and call some model reduction methods.

A graphical interface is proposed to navigate through the various options and utilities of KaDE. The compilation of this interface requires labltk and, in particular, tk-dev.

Chapter 4
The stochastic simulator: KaSim

4.1 General usage

From a terminal window, KaSim can be invoked by typing:

• KaSim file_1 ... file_n [option]

where file_i are the input Kappa files containing the rules, initial conditions and observables (e.g. see Chapter 2). A simulation can generate several files that are described in the present chapter. One should really take advantage of the option -d so that these files all ends in a distinct directory.

In any case, a log called inputs.ka is generated. This is a valid Kappa file such that KaSim inputs.ka reruns exactly the simulation just ran outputing the exact same outputs (using the same pseudo random numbers!). First line of this file contains an uuid that is also present in any file output during the same run.

Tables 4.1 and 4.2 summarize all the options that can be given to the simulator.

Basically, one can specify an upper bound and a plot period either in simulated or bio-time (arbitrary time unit), or in number of events. Note that bio-time is computed using Gillespie's formula for time advance (see Fig. 3.1) and should not be confused with CPU-time (it is not even proportional).

4.2 Main options

Table 4.1 summarizes the main options that are accessible through the command line. Options that expect an argument are preceded by a single dash, options that do not need any argument start with a double dash.

Two key options are the plot period -p (how often you want a line in the data file) and the limit -l of simulation. These quantities can expressed in simulated time (the default) or in number of event (using -u event).

4.3 Advanced options

Table 4.2 summarizes the advanced options that are accessible through the command line.

4.4 Example

The command:

• KaSim model.ka -u event -l 1000000 -p 1000 -o model.out

will generate a file model.out containing the trajectories of the observables defined in the Kappa file model.ka. A measure will be taken every 1000 events in file model.out. The command:

• KaSim init.ka rules.ka obs.ka mod.ka -l 1.5 -p 0.0015

will generate a file data.csv (default name) containing 1,000 data points of a simulation of 1.5 (arbitrary) time units of the model. The input Kappa file is split into four files containing, for instance, the initial conditions, init.ka, the rule set, rules.ka, the observables, obs.ka, and the interventions, pert.ka (e.g. see Chapter 2).

4.5 Interactivity

Simulations are interruptible by sending a SIGINT to the simulator. (The easiest way to send a SIGINT to a process is to press Ctrl-c in the terminal window it runs into.)

In batch mode, this stops the simulation. In other circumstances, it launches a toplevel in which one can either type:

• $RUN (optionally followed by a pause condition) to resume simulation or
• any of the effects described in Section 2.7 to trigger it imediately.

A pause condition is a boolean expression (e.g. Section 2.7) under which the simulator will stop and fall back in the toplevel in order to allow a new interactive session.

The option -mode interactive interrupts automatically the simulation (and launches the toplevel) just after the initialization of the simulation.

Chapter 5
Advanced concepts

5.1 Experimental continuous examination

5.1.1 Causality analysis

In our ABC example, adding the instruction: %mod: [true] do $TRACK ’Cpp’[true]; will ask KaSim to turn on causality analysis for the observable 'Cpp' since the beginning of the simulation, and display the causal explanation of every new occurrence of 'Cpp', until the end of the simulation. The explanation, that we call a causal flow, is a set of rule applications ordered by causality and displayed as a graph using dot format. In this graph, an edge r$\to$ r' between two rule applications r and r' indicates that the first rule application has used, in the simulation, some sites that were modified by the application of the former. We show in Fig. 5.1 an example of such causal flow.

Causality analysis of the observable Cpp can be turned off at any time by using a declaration of the form: %mod: [T]>25 do $TRACK ’Cpp’[false];

Each time KaSim detects a new occurrence of the observable that is being tracked, it will dump its causal past as a graph using the dot format (see Fig. 5.1 above). The name of the file in which the causal flow is stored can be set by using the %def instruction (see Section 5.4).

Compressing causal flows.

In general, pure causal flows will contain a lot of information that modelers may not wish to consider. Indeed in classical flows, causality (represented by an edge between to rule applications in the graph) is purely local. Therefore a sequence $a\to b\to c$ only implies that an instance of rule $a$ caused an instance of rule $b$ which in turn created an instance of the observable $c$. However, it does not imply that $a$ was "necessary" for $c$ to occur (for instance, $c$ might have been possible before $a$ but not after, and $b$ would be simply re-enabling $c$). It is possible to tell KaSim to retain only events that are more strongly related to the observable using two compression techniques (see Ref. [8] for formal details). Intuitively, in a weakly compressed causal flow one has the additional property that if an event $e$ is a (possibly indirect) cause of the observable, then preventing $e$ from occurring would have prevented the rest of the causal flow to occur (i.e. it is not possible to reconstruct a computation trace containing the observable with the events that remain in the causal flow). A strongly compressed causal flow enjoys the same property with an additional level of compression obtained by considering different instances of the same rule to be indistinguishable. Note that, causal flow compressions may be memory and computation demanding. For large systems it may be safer to start with weak compressions only.

The type of compression can be set using the %def instruction (see Section 5.4). For instance: %def: "displayCompression" "none" "weak" "strong" will ask KaSim to output 3 versions of each computed causal flow, with all possible degrees of compressions. Each causal flow is outputted into a file [filename][Type]_$n$.dot where filename is the default name for causal flows which can be redefined using the parameter cflowFileName, Type is the type of compression (either nothing or Strongly, or Weakly) and $n$ is the identifier of the causal flow. For each compression type a summary file, named [filename][Type]Summary.dat, is also produced. It allows to map each compressed causal flow to the identifier of its uncompressed version (row #id), together with the production time $T$ and event number $E$ at which the observable was produced. It also contains information about the size of the causal flow.

Limit the number of flows

As an example, consider the computation of causal flows between $t=10$ and $t=20$ using the declarations:

The above declaration will ask KaSim to analyze each new occurrence of 'Cpp' in that time interval. If $n$ new instances took place, then KaSim will have to compute $n$ causal flows. One may want to bound the number of computed flows to a certain value, say 10. One may do so using the combination of interventions and variables given below:

The first line is a declaration of an $x$ variable that is initially set to 0. Note that, the second line is a intervention that contains two simultaneous effects, the first one triggering causality analysis and the second one updating the value of variable $x$ to the current value of variable 'Cpp'. The last line stops causality analysis whenever time is greater than 20 or when 10 new observables have been found (the difference between the current value of 'Cpp' and $x$).

5.1.2 Dynamic influence network

The dynamic influence network (DIN) is a powerful observation that tracks, on the fly, the influence that rule applications have on each others. It is dynamically generated and tracks effective impacts (positive or negative) at every rule application. The DIN can be computed using declarations of the form:

The result is a graph where a positive edge between rules $r$ and $s$ (in green) indicates an overall positive contribution of $r$ over $s$. Otherwise, the sum of $r$ applications increased the activity of $s$. Conversely, a negative edge (in red) will indicate that $r$ had an overall negative impact on the activity of $s$. Note that, the importance of the influence between two rules can be observed by looking at the label on the edges that indicate the overall activity transfer (positive or negative) between the rules. The above declaration produces the network shown in Fig. 5.2. Note that, influence may vary during time, therefore the time or event limit of the simulation is of importance and will likely change the aspect of the produced map.

5.1.3 Print species of an observable

The effect $SPECIES_OFF tracks the occurrence of an observable. Each time a new instance of the observable appears, the species in which it occured is printed in a file. For example:

prints in the file "species.ka" a new line for each new occurrence of A(a!1), B(a!1) with the time of occurrence and the species in which it occurred.

Note that, this intervention can only be applied if the observable is a connected component.

5.2 Implicit signature

KaSim permits users in a hurry to avoid writing agent signatures explicitly using the option --implicit-signature of the command line. The signature is then deduced using information gathered in the KF. Note that, it is not recommended to use the DCDW convention for introduced agents in conjunction with the --implicit-signature option unless the default state of all sites is mentioned in the %init declarations or in the rules that create agents.

5.3 Simulation packages

The simulation algorithm that is implemented in KaSim requires an initialization phase whose complexity is proportional to $R\ast G$ where $R$ is the cardinal of the rule set and $G$ is the size of the initial mixture. Thus for large systems, initialization may take a while. Whenever a user wishes to run several simulations of the same Kappa model, it is possible to skip this initialization phase by creating a simulation package. For instance:

• KaSim abc.ka -l $n$ -make-sim abc.kasim

will generate a standard simulation of the abc.ka model, but in addition, will create the simulation package abc.kasim (.kasim extension is not mandatory). This package is a binary file, i.e. not human readable, that can be used as input of a new simulation using the command:

• KaSim -load-sim abc.kasim -l $k$

Note that this simulation is now run for $k$ time units instead of $n$. Importantly, simulation packages can only be given as input to the same KaSim that produced it. As a consequence, recompiling the code, or obtaining different binaries, will cause the simulation package to become useless.

5.4 Simulation parameters configuration

In the KF (usually in a dedicated file) one may use expressions of the form:

%def: "parameter_name" "parameter_value"

where tunable parameters are described in table 5.1 (default values are given first in the possible values column).

5.5 Counters

An agent can have counters, which are sites storing a positive integer. When declaring an agent, each counter has to be assigned a min and a max value. For instance, the agent %agent: A(x,c:1 += 4,d:0 +=2) has two counters, named $c$ and $d$, which range from $1$ to $4$, and from $0$ to $2$, respectively.

At initialisation, an initial value for the counter has to be specified.

In rules, all counter tests have to be in the LHS, while the counter modifications in the RHS. A counter test can do three things: (i) check that the counter value is equal to a positive integer; (ii) check that the counter’s value is greater than a positive integer or (iii) declare a variable, to which the counter’s value is assigned. The variable can then be used in the rate constant.

A counter modification increments or decrements the original counter value. In the following table, $n\le 0$ and both $n$ and $i$ are integers.

If the counter goes negative, the compilation stops with an error. If the counter goes up beyond its declared maximum value, the simulation stops with an error.

Chapter 6
The KaSa static analyser

6.1 General usage

From a terminal window, KaSa can be invoked by typing the following command line:

• KaSa file_1 ... file_n [option]

where file_i are the input Kappa files containing the rules, initial conditions and observables (see Chapter 2).

All the options are summarised as follows:

Order in options matters, since they can be used to toggle on/off some functionalities or to assign a value to some environment variables. The options are interpreted from left to right.

More options are available in the OCaml file KaSa_rep/config/config.ml and can be tuned before compilation.

6.2 Graphical interface

6.2.1 Launching the interface

The graphical interface can be launched by typing the following command line:

• KaSa

without any option.

6.2.2 The areas of interest

There are five different areas of importance in the graphical interface:

1. On the top left of the window, a button allows for the selection between the Normal and the Expert mode (other modes may be available if activated at compilation). In expert mode, more options are available in the graphical interface.
2. On the top center/right, some button allows for the selection of the tab. There are currently six sub-tabs available: Actions, Syntax, Output, Reachability analysis, Trace analysis, Contact map, Influence map.
3. In the center, the options of the selected sub-tab are displayed and can be tuned.

   Contextual help is provided when the mouse is hovered over an element.

   The interface will store the options that are checked or filled and the order in which they have been selected. When launched, the analysis interprets these options in the order they have been entered.

   Some options appear in several sub-tabs. They denote the same option and share the same value.

4. File selector: The file selector can be used to upload as many Kappa files as desired. The button ’Clear’ can be used to reset the selection of files.
5. Bottom: Some buttons are available. The button ’Quit’ can be used to leave the interface. The button ’Reset to default’ tunes all the options to their default value. The button ’Import options’ can be used to restore the value of the options as saved during a previous session of the graphical interfaces. The button ’Save options’ can be used to save the value of the options for a further session. The button ’Launch analyze’ launches KaSa with the current options.

   Importantly, options are saved automatically under various occasions. Thus, it is possible to restore the value of the options before the last reset, before the last quit, or before the last analysis.

6.2.3 The sub-tab Actions

The sub-tab Actions (see Fig. 6.1) contains the main actions which can be performed.

The following options are available:

• The button --do-all activates all the functionalities.
• The button --reset-all inactivates all the functionalities.
• The option --compute-contact-map can be used to (des)activate the computation of the contact map.
• The option --compute-influence-map can be used to (des)activate the computation of the influence map.
• The option --compute-potential-cycles can be used to (des)activate the computation of the potential polymers.
• The option --compute-reachability-analysis can be used to (des)activate the computation of the reachability analysis.
• The option --compute-symmetries can be used to (des)activate the computation of pairs of equivalent sites. Equivalent sites may be used to reduce the number of variables in the system of ordinary differential equations that is associated to a Kappa model (e.g. see Sect. 7.3.2).
• The option --compute-local-traces can be used to (des)activate the computation of the trace analysis.
• The option --compute-separating-transitions can be used to (des)activate the computation of the transitions that are non weakly reversible. These are the transitions between two configurations of an agent, that are impossible to revert (even in several computation steps).

Lastly, a switch allows to select the version for Kappa syntax for the input file, among version $3$, V3, and version $4$, V4.

6.2.4 The sub-tab Syntax

The sub-tab Syntax (see Fig. 6.2) contains the switch to select between the version 3, V3, and the version 4, V4, of Kappa syntax.

6.2.5 The sub-tab Output

The sub-tab Ouput (see Fig. 6.3) contains the names of the output files and their format.

The following options are available:

• The field --output-directory can be used to set the repository where output file are written. KaSa will create this repository, if it does not exist.
• The field --output-contact-map-directory can be used to set the repository where the output file for the contact map is written, if a contact map is requested. KaSa will create this repository, if it does not exist.
• The field --output-contact-map contains the name of the file for the contact map. If the file name does not end by it, the proper extension will be added to the file name.
• The field --output-influence-map-directory can be used to set the repository where the output file for the influence map is written, if an influence map is requested. KaSa will create this repository, if it does not exist.
• The field --output-influence-map contains the name of the file for the influence map. If the file name does not end by it, the proper extension will be added to the file name.
• The format for the influence map can be chosen among DOT, DIM, and HTML thanks to the option --influence-map-format. In format DIM, the output of the influence map is a json file containing the support of the dynamic influence map that has been introduced in Sect. 5.1.2.
• The field --output-local-traces-directory can be used to set the repository where the output file for the result of trace analysis is written, if this analysis is requested. KaSa will create this repository, if it does not exist.
• The format for the local traces can be chosen among DOT and HTML thanks to the option --local-traces-format.

When a file already exists, it is overwritten without any warning.

6.3 Reachability analysis

Reachability analysis aimed at detecting statically properties about the bio-molecular species that may be formed in a model. Knowing whether, or not, a given bio-molecular species may be formed in a model is an undecidable problem [24]. Thus, our analysis is approximate. Indeed, it computes an over-approximation of the set of the bio-molecular species that can be reached from the initial state of the model, by applying an unbounded number of computation steps. As formalized in [11, 20], the abstraction consists in:

1. firstly, ignoring the number of occurrences of bio-molecular species (we assume that whenever a bio-molecular species may be formed, then it may be formed as many time as it could be necessary),
2. secondly, abstracting a bio-molecular species by the set of its properties.

The analysis takes into account also the chemical species that may be introduced in a intervention.

The classes of properties of interest are encoded in so called abstract domains, which can be independently enabled/disabled. The whole analysis can be understood as a mutual recursion between smaller analyses (one per abstract domain), that communicate information between each other at each step of the analysis. We took the same scheme of collaboration between abstract domains as in [6].

As an example, we consider the following model:

Typing the following command line:

will perform the reachability analysis on the model reachability.ka.

We obtain the following result:

This result is displayed in the standard output, and it is made of six parts.

The first two parts provide an enumeration of dead rules and dead agents. The next parts display what we call refinement lemmas. A refinement lemma is made of a precondition (on the left of the implication symbol) that is a site graph, and a postcondition (on the right of the implication symbol) that is a list of site graphs. Each site graph in the post-condition is a refinement of the precondition (the position of agent matters: the $n$-th agent in the precondition corresponds to the $n$-th agent in each site graph in the postcondition, but site graphs in a postcondition may have more agents than the site graph in the corresponding precondition). The meaning of a refinement lemma is that every embedding between its precondition into a reachable state can be refined/extended into an embedding from one site graph in its postcondition into the same reachable state. This way, a refinement lemma provides an enumeration of all the potential contexts for the precondition.

We now detail the seven different parts:

• Detection of dead rules. A rule is called dead, if there is no trace starting from the initial state in which this rule is applied. The analysis reports the list of the rules it has detected to be dead. Due to the over-approximation, it may happen that a dead rule is not discovered by the analysis. Yet, every rule that is reported as dead, is dead indeed.

  In our example, we notice that the rule ‘obs’ can never be trigered.

• Detection of dead agents. An agent is called dead, if there is no trace starting from the initial state with at least one state in which this agent occurs. The analysis reports the list of the agents it has detected to be dead. Due to the over-approximation, it may happen that a dead agent is not discovered by the analysis. Yet, every agent that is reported as dead, is dead indeed.

  In our example, there are no dead agent.

• Non-relational properties. The analysis detects for each kind of site, the set of states this site can take. Due to the over-approximation, the analysis reports a super-set of the set of the potential states. Yet, we are sure that a given site only take states within this set.

  In our example, the site cr of R may be free, or bound to the site n of an agent R.

• Relational properties. The analysis detects some relationships among the states of packs of sites within each agent, hence capturing potential valuations for local views [17, 11]. Due to the over-approximation of the analysis, the analysis may fail in discovering a relationship. But each relationship that is found by the analysis is satisfied.

  In our example, the states of the sites c, cr, n, and x of R are entangled with a relational property (othewise, we would have $5^2$ elements in the post-condition).

• Properties in connected agents. When two agents are connected, there may be a relation among the states of theirs respective sites. This abstraction [20] collects for each kind of bonds, the relation between the state of one site in the first agent and the state of one site in the second agent. Due to the over-approximation, the analysis reports a super-set of the set of the potential pairs of states.

  This abstraction aimed at capturing information about protein transportation. It is quite common to model the location of a protein as the internal state of a fictitious site. With such an encoding, it might be important to ensure that two connected proteins are always located in the same location. This abstraction focuses on this kind of properties.

• Properties of pairs of bonds.

  It might be interesting to know whether a protein can be bound to another protein twice simultaneously, and whether a protein can be bound to two instances of a same protein simultaneously. This abstraction [20] captures this kind of constraint. It can be used to prove that some proteins do not polymerize.

  In our example, when a R has its sites cr and c bound, they are necessarily bound to the same instance of R. The same statement holds for the sites cr and n.

• Properties of counters.

  KaSa is inferring the range of counters.

  There are no counter in our previous example. Let us consider the following one:

  1%agent:A(x1{u p},x2{u p q},x3{u p},c{=0},d{=0}) 
  2%agent: B(x) 
  3 
  4A(x1{u}) -> A(x1{p},c{+=3},d{+=2}) @1 
  5A(x1{p}) -> A(x1{u},c{-=3},d{-=1}) @1 
  6A(x2{u}) -> A(x2{p},c{+=2},d{+=1}) @1 
  7A(x2{p}) -> A(x2{u},c{-=2},d{-=2}) @1 
  8A(x2{p}) -> A(x2{q},c{+=1}) @1 
  9A(x2{q}) -> A(x2{p},c{-=1}) @1 
  10A(x3{u}) -> A(x3{p},c{+=3}) @1 
  11A(x3{p}) -> A(x3{u},c{-=3}) @1 
  12A(x1[.]),B(x[.]) -> A(x1[1],c{+=1}),B(x[1]) @1 
  13A(x1[1]),B(x[1]) -> A(x1[.],c{-=1}),B(x[.]) @1 
  14A(x2[.]),B(x[.]) -> A(x2[1],c{+=1}),B(x[1]) @1 
  15A(x2[1]),B(x[1]) -> A(x2[.],c{-=1}),B(x[.]) @1 
  16A(x3[.]),B(x[.]) -> A(x3[1],c{+=1}),B(x[1]) @1 
  17A(x3[1]),B(x[1]) -> A(x3[.],c{-=1}),B(x[.]) @1 
  18 
  19%init:10    A() 
  20%init: 10 B()

  Typing the following command line:

  KaSa reachability.ka --reset-all --compute-reachability-analysis

  we get in the section ‘Properties of counters’ of the output what is prompted in Fig. 6.11. KaSa has inferred that the counter c is ranging from $0$ to $12$ . There is no information on counter d since its value has no lower bound and no upper bound.

  By default, KaSa is using a relational numerical analysis based on a product between interval analysis [5] and affine relationship analysis [23]. The product is approximate. It used a decision procedure described in [16].

  Other abstractions for counters are available for pedagogical purpose. For instance, the following command line:

  KaSa reachability.ka --reset-all --compute-reachability-analysis  
       --counters-accuract octagon

  will provide no property for counters (e.g. see Fig. 6.12). KaSa has failed in bounding the range of the counter c

Now we describe the options that are available on this sub-tab.

The option --compute-reachability-analysis can be used to switch on/off then reachability analysis.

The option --enable-every-domain can be used to switch on every abstract domain, whereas the option --disable-every-domain can be used to switch off every abstract domain.

The option --contact-map-domain impacts the way side-effects are handled with during the analysis. In static mode, we consider that every bond that occurs syntactically in the initial state, in the RHS of a rule, or in an introduction directive of a intervention, may be released by side-effects. In dynamic mode, only the bond that has been encountered so far during the analysis are considered.

The option --views-domain can be used to switch on/off the views domains that combine the non-relational analysis and the relational analysis.

The option --counters-domain can be used to switch on/off the analysis of the potential range of counters.

The option --counter-accuracy can be used to select the abstraction for the potential range of counters. The domain mi consists in an approximate reduced product between interval analysis [5] and affine relationships [23]. The reduction between these two domains, is obtained by applying the decision procedure that is described in [16]. The domain octagons infer a range for each variable, each sum and each difference among two variables. Although both domains have the same complexity, the product between intervals and affine constraints is more appropriate in the case of counters, since usually the state of more than two variables have to be related.

The option --double-bonds-domain can be used to switch on/off the analysis of potential double bonds between proteins.

The option --site-across-bonds-domain can be used to switch on/off the analysis of the relations among the states of the sites in connected proteins.

It is possible to get more details about the computation of the analysis by tuning the verbosity level of the view analysis:

• With the option --verbosity-level-for-reachability-analysis Mute, nothing is displayed. Even the result of the analysis is omitted (eg. see Fig. 6.5).
• With the option --verbosity-level-for-reachability-analysis Low, only the result of the analysis is displayed (by default).
• With the option --verbosity-level-for-reachability-analysis Medium, the analysis also describes which rules are applied and in which order.

  When trying to apply a rule, the analysis may detect that the rule cannot be applied yet because the precondition is not satisfied at the current state of the iteration (eg. see Fig. 6.6). Otherwise, the analysis can apply the rule and update the state of the iteration accordingly (eg. see Fig. 6.7).

• With the option --verbosity-level-for-reachability-analysis High, the analysis also describes which patterns are discovered.

  In particular, at the beginning of the iteration, the analysis prompts the patterns of interest that occur in the initial state (eg. see Fig. 6.8). Then, each time a rule is applied successfully, the analysis shows which new patterns have been discovered (eg. see Fig. 6.9).

• When new patterns are discovered, then, it is necessary to apply again any rule that may operate over these patterns. With the following option:
        --verbosity-level-for-reachability-analysis Full,
  the analysis also describes which rules are awaken by the discovery of a new pattern (see Fig. 6.10).

The option --output-mode-for-reachability-analysis can be used to tune the output of the analysis. The default mode is kappa. In mode raw, patterns of interest are displayed extensionally. In mode english, properties of interest are explained in English. The option --use-natural-language can be used to switch on/off the translation of properties in natural language: when the option is disabled, each relationship is described in extension.

6.4 Local traces

Trace analysis is a refinement of reachability analysis that additionaly explains how one agent can go from a given view to another one, following a path that we call a local trace. Thus the set of the local traces for a given agent can be described as a transition system among the views for a given agent: in this transition system, the nodes are local views; introduction arrows correspond to either initial states, or creation rules; transitions denote a potential conformation change of an agent, from one local views to another one, due to the application of a given rule.

We consider the following example: