BigMC -- Bigraphical Model Checker

• Home
• Manual
• GitHub

7 Checking

Having defined your reaction rules, model and properties, the final line in your file should be %check. This signals to bigmc that checking should actually begin.

For example, we could check some diverge_prop.bgm (which is in the doc/example directory of your BigMC distribution):

     %active a : 0;
     %active b : 0;
     %active c : 0;
     
     a.b;
     
     b -> a.b;
     a.a.b -> a;
     a.$0 -> c.$0;
     
     %property growth size() >= $pred->size();
     
     %check;

We invoke bigmc using a command such as:

     $ bigmc diverge_prop.bgm

This will result in the following backtrace:

     *** Found violation of property: growth
     *** growth: size >= $pred->size()
     #0  a.nil   <- *** VIOLATION ***
      >> a.a.b.nil -> a.nil
     
     #1  a.a.b.nil
      >> b.nil -> a.b.nil
     
     #2  a.b.nil
      >> (root)
     mc::step(): Counter-example found.

We interpret the backtrace as showing us a state that violated the property growth. States are displayed from “newest” to “oldest”, interleaved with the reaction rule that was applied to reach that state from the previous one.