Static analysis

Static analysis techniques are performed directly on the model syntax and are therefore extremely fast by definition.

In particular, we have developed a method to detect (potentially) redundant rules in the model. This can be useful in large models to detect potentially concurrent rules and to make the model more compact. The redundant rules are denoted by adding comments at the end of such potentially redundant rules and connecting them by an integer identifier. A step by step Galaxy tour showing how to use the tool can be found here.

Another static analysis technique is used to reduce the context of the model to a minimal level in order to produce a smaller and more abstract model. The resulting model still preserves some properties while making the analysis of the model computationally simpler. A step by step Galaxy tour showing how to use the tool can be found here.

Finally, a non-reachability static analysis can be used to check whether a single agent is non-reachable before enumerating the entire transition system of the model. This analysis is based on the idea that in order to reach an agent, there has to be a rule which creates it or a lesser specified agent; in other words, the particular states inside of the agent are changed at some point. A step by step Galaxy tour showing how to use the tool can be found here.

Input specification

• Model file: Selected model in BCSL language (see Model syntax for details).

• Choose static analysis method:

  • Static non-reachability: This option computes non-reachability for the particular agent given in Complex agent.

  • Rule redundancy elimination: This option marks pairs of rules which might be redundant in the model.

  • Context based reduction: This option removes all states from all agents in the model, reducing context to a minimum. Rule with no sense (e.g. rules where left- and right-hand sides are equal) are removed.

Output specification

The results of the tool depend on the particular method which was chosen.

For Static non-reachability method, the output is textual a states whether the agent of interest cannot be reached and can possibly be reached in the model.

For Rule redundancy elimination method, the output is a .bcs model. In the first case, just some comments are added to the file indicating potential (if any) redundant rules.

For Context based reduction method, the output is a .bcs model. In the output model, all states are absent, leaving only rules for complex formation and dissociation, production, and degradation.

---

Command line arguments

usage: StaticAnalysis.py [-h] --model MODEL --output OUTPUT --method METHOD
                         [--complex COMPLEX]

Static analysis

required arguments:
  --model MODEL
  --output OUTPUT
  --method METHOD

optional arguments:
  --complex COMPLEX