BigMC -- Bigraphical Model Checker

• Home
• Manual
• GitHub

4 BGM file structure

The basic structure for a bigraph model file is as follows:

     # Comments
     <control definitions>
     
     <names>
     
     <reaction rules>
     
     <model definition>
     
     <properties>
     
     %check;

4.1 Comments

Comments are lines starting with '#', and continue to the end of the line.

     # This is a comment

4.2 Control Definitions

Control definitions take one of two forms:

     %active control-name : arity;
     %passive control-name : arity;

All of the information must be present. For example:

     %passive send : 1;
     %active foo : 3;

4.3 Names

The top-level outer names are defined as follows:

     %name name;

For example:

     %name a;
     %name b;

The alternative keyword %outer is also accepted to make explicit the fact that these are specifically outer names.

Names need not be unique with respect to control names; however, it might be best to keep them that way to avoid confusion.