Datasets and PBLSTL statements

The efficiency and expressivity of the methodology implemented in the model checker Mudi was illustrated based on two case studies namely phase variation patterning in bacterial colony growth and the chemotactic aggregation of cells (chemotaxis). 

Phase variation

 Description
 File  Size (bytes)
 Dataset (1000 STML files)
 stml_dataset_phase_variation.7z  511,912
 PBLSTL statements
 bmc_pblstl_phase_variation.in  6,499

Chemotaxis

 Description
 File  Size (bytes)
 Dataset (2500 STML files)
 stml_dataset_chemotaxis2D.7z  67,189,288
 PBLSTL statements
 bmc_pblstl_chemotaxis.in  4,756


Models

 Description
 File  Size (bytes)
 Phase variation
 phase_variation_rectangular_model.colstochpn  6,060,597
 Chemotaxis
 chemotaxis2D.xml  3,465


Visualisation and analysis

Phase variation patterning in bacterial colony growth


Visualisation

Phase variation simulation output visualisation


Analysis

Phase variation simulation output analysis



Chemotactic aggregation of cells


Visualisation

Chemotaxis (2D) simulation output visualisation


Analysis

Chemotaxis (2D) simulation output analysis