Transition System generator

In this section, we describe how to generate a transition system from given BCSL model. Following the idea of using approximate models with discrete-time semantics, the obtained transition system is a Discrete Time Markov Chain (DTMC) or a parametric Markov Chain (pMC), depending on whether there are some parameters used in rule rates which do not have defined value in definitions. 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).

• Bound (optional): Bound represents the maximal multiplicity of any agent in any state. If not given, an optional bound is computed automatically for potentially infinite systems. It implies the construction of special “hell” state aggregating all states beyond the bound.

• Advanced Options (all optional)

  • Maximal computation time: Possibility to specify the time (in seconds) boundary for the computation.

  • Maximal TS size: Represents approximately the maximal number of nodes in the final transition system.

  • Precomputed TS file: Possibility to enter pre-generated transition system for the same model and continue in its generating. Usually connected with the usage of two previous parameters.

Output specification

Transition system generator tool generates a file format .bcs.ts, which is JSON with the following structure:

• ordering: Ordered list of all distinct agents.

• nodes: Set of nodes representing states of the transition system. Each of them contains a unique ID and a tuple of numbers, representing the multiplicity of the agent on the respective position from the ordering.

• edges: Set of edges representing transitions. Each edge contains ID of the source node (s), and ID of the target node (t), and the probability of the transition (p). In the case of the parametrised model, the probability is replaced by a probability function of parameters.

• initial: ID of the initial state.

The transition system can be visualised as a network in an interactive chart called Transition system visualisation.

---

Command line arguments

usage: GenerateTS.py [-h] --model MODEL --output OUTPUT
                     [--transition_file TRANSITION_FILE] [--max_time MAX_TIME]
                     [--max_size MAX_SIZE] [--bound BOUND]

Transition system generating

required arguments:
  --model MODEL
  --output OUTPUT

optional arguments:
  --transition_file TRANSITION_FILE
  --max_time MAX_TIME
  --max_size MAX_SIZE
  --bound BOUND