   Small examples in NBac format 
Small examples in NBac format
You can easily modify the properties contained in these examples. The property
is defined by the state variable ok.
 incalt
 This is the running example of the
tutorial. We give variations of it, using as parameters
the number of Boolean and numerical variables. p numerical variables are
incremented one after the other, while the control moves according to a ring
of size 2^{n} defined by n Boolean variables. The goal is to check the
invariance property x_{0} >= x_{1} >= x_{2}... where the x_{i} are the
numerical variables, x_{i} being incremented before x_{i+1}.
The naming scheme is incaltPN_xyz.ba; P and N have already been
described, and xyz means that the property to be checked is x >= y >= z
(i.e., we do not necessarily check the general property on all the
numerical variables).
This example shows how the tool unfold the implicit control structure in
order to prove the property.
 plane

These are 2 small, purely numerical examples, in 2 dimensions, that shows how
the tool can split locations according to numerical constraints.
The trajectory of plane1.ba is:
And the trajectory of plane2.ba is
Bertrand Jeannet, February 10, 2011
   Small examples in NBac format 