6 Property language
Having defined a model in the previous section, we want to start to be able to make some
kind of specification of properties which we would like to ensure hold. We do this using the
%property specifier, which is of the form:
%property property-name property-expression;
The property-name is a non-semantically-significant name which will be reported if the checker encounters a violation of a property during checking.
A single .bgm file can have arbitrarily many
%property declarations. The order
in which they appear in the file will be the order in which they are considered at each new
state; it may be a sensible strategy to place matches more likely to fail earlier in the
6.1 Property Expressions
The basic unit of most property expressions is the predicate. An exhaustive list of available predicates will be provided in a subsequent section of this manual. Aside from predicates, various familiar programming language logical connectives are provided:
P ::= B && B P ::= B || B P ::= !B B ::= E == E B ::= E != E B ::= E <= E B ::= E >= E B ::= E < E B ::= E > E E ::= predicate(parameters) E ::= integer literal
The essential execution model associated with these properties is that each time a new state is discovered and considered, the predicates are applied to that state. The simplest property we could define might be:
%property not_empty !empty();
Assuming we have some (pre-defined) predicate called
empty that takes no arguments, then
this property will be satisfied iff every state in the model is not empty.
It turns out that this is sufficient to write specifications that inspect the properties of individual states, but what if we want to write a specification that defines properties over states as they evolve? We have another mechanism for that:
%property growth size() >= $pred->size();
This property assumes that we have a pre-existing predicate called
size that returns the
“size” of a given term (spoiler alert: we do). The first application of the predicate
size will evaluate to the size of the current state under consideration. The second
instance of the predicate is prefixed with
$pred (short for predecessor), which
is a placeholder for “the state from which the current state was created by a step of
reaction”, so in this instance
size is being applied to the predecessor state, not
the current state. Finally, taking the greater-than-or-equal-to connective
>=, this is a
property stating that this model must never shrink through a step of reaction. If the checker
can find any two consecutive states in the transition system where a state is smaller than
the one from which it is derived, this will constitute a violation of the growth
6.2 Pre-defined Scopes
The full list of scopes:
$predThe predecessor to the current state, such that there exists some step of reaction from
$predto the current state.
$thisThe current state.
$succThe set of successor states, i.e., those reachable by a step of reaction from the current state.
$terminalThe predicate in question is only applied to states marked
terminal, that is, they do not lead to any further states and there are no reactions that can be applied to them.
truewhen applied to non-terminal states, or
p()if applied to a terminal state.
- ... More to come? Suggest more useful scopes!
It's important to note that scopes like
pred will not work when in
local checking mode!
6.3 Pre-defined Predicates
This predicate returns a count of the number of place-graph nodes in the current agent. For example:
a.a.a.nil --> 3 a.nil | b.nil --> 2 nil | nil | nil --> 0 nil --> 0
This can be used to construct properties such as:
%property growth $pred->size() <= size();
This checks whether a given redex t matches anywhere within the current agent, subject to the usual active contexts restriction. For example:
%active a : 0; %active b : 0; %active c : 0; a.b | a.c; a.$1 | $0 -> c.$1 | $0; %property cc !matches(c.c); %check
This is equivalent to the property
size() == 0.
This checks the property of the current node in the transition system and returns
false if the node has outgoing edges (i.e. there are further agents reachable by the application of some reaction rule to this agent), or
true otherwise. See doc/examples/dining.bgm for an example use of this predicate to define deadlock-freedom.
Table of Contents
- 1 Introduction
- 2 Obtaining BigMC
- 3 Invoking bigmc
- 4 BGM file structure
- 5 Term language
- 6 Property language
- 7 Checking
- 8 Example