Next: Example, Previous: Property language, Up: Top
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.
This work funded in part by the Danish Research Agency (grant no.: 2106-080046) and the IT University of Copenhagen (the Jingling Genies project)