Skip to content
Snippets Groups Projects
Commit 6111eac6 authored by dgelessus's avatar dgelessus
Browse files

Remove BLanguage section whose content can be found on the wiki

parent b72bf27a
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
Showing
with 0 additions and 1745 deletions
src/docs/chapter/user/12_BLanguage/00_section_header.adoc deleted 100644 → 0
+ 0
− 4
View file @ b72bf27a
[[b-language]]
= B Language
:leveloffset: +1
src/docs/chapter/user/12_BLanguage/01_Current_Limitations.adoc deleted 100644 → 0
+ 0
− 57
View file @ b72bf27a
[[current-limitations]]
= Current Limitations
ProB in general requires all <<deferred-sets,deferred sets>> to be
given a finite cardinality. If no cardinality is specified, a default
size will be used. Also, unless finite bounds can be inferred by the
ProB constraint solver, mathematical integers will only be enumerated
within `MININT` to `MAXINT` (and ProB will generate enumeration
warnings in case no solution is found).
Other general limitations are:
* Trees and binary trees are specific to the AtelierB
tool and are only partially supported (the `STRING` type is now supported).
* Definitions (from the `DEFINITIONS` clause) with
arguments are supported, but in contrast to AtelierB they are parsed
independently and have to be either an expression, a predicate, or a
substitution; definitions which are predicates or substitutions must be
declared before first use.
Also: the arguments of `DEFINITIONS` have to
be expressions. Finally, when replacing DEFINITIONS the associativity is
not changed. E.g., with `PLUS(x,y) == x+y`, the expression
`PLUS(2,3)*10` will evaluate to 50 (and not to 32 as with Atelier-B).
Also, ProB will generate a warning when variable capture may occur.
* There are also limitations with refinements, as discussed below.
* The `VALUES` clause of `IMPLEMENTATION` machines is not yet
supported.
* Parsing: ProB will require parentheses around the comma, the
relational composition, and parallel product operators. For example, you
cannot write `r2=rel;rel`. You need to write `r2=(rel;rel)`. This allows
ProB to distinguish the relational composition from the sequential
composition (or other uses of the semicolon).
See the page <<using-prob-with-atelier-b,Using ProB with Atelier B>> for more details.
[[multiple-machines-and-refinements]]
== Multiple Machines and Refinements
It is possible to use multiple B machines with ProB. However, ProB may
not enforce all of the classical B visibility rules (although we try
to). As far as the visibility rules are concerned, it is thus a good
idea to check the machines in another B tool, such as Atelier B or the
B-Toolkit.
While refinements are supported, the preconditions of operations are not
propagated down to refinement machines. This means that you should
rewrite the preconditions of operations (and, if necessary, reformulate
them in terms of the variables of the refinement machine). Also, the
refinement checker does yet check the gluing invariant.
Note however, that for Rodin Event-B models, ProB fully supports multi-level
animation and validation.
src/docs/chapter/user/12_BLanguage/01_Summary_of_B_Syntax.adoc deleted 100644 → 0
+ 0
− 476
View file @ b72bf27a
[[summary-of-b-syntax]]
= Summary of B Syntax
[[logical-predicates]]
== Logical predicates:
....
P & Q conjunction
P or Q disjunction
P => Q implication
P <=> Q equivalence
not P negation
!(x).(P=>Q) universal quantification
#(x).(P&Q) existential quantification
....
Above, `P` and `Q` stand for predicates. Inside the universal
quantification, `P` must give a value type to the quantified variable.
Note: you can also introduce multiple variables inside a universal or
existential quantification, e.g., `!(x,y).(P => Q)`.
[[equality]]
== Equality:
....
E = F equality
E /= F disequality
....
[[booleans]]
== Booleans:
....
TRUE
FALSE
BOOL set of boolean values ({TRUE,FALSE})
bool(P) convert predicate into BOOL value
....
Warning: `TRUE` and `FALSE` are values and not predicates in B and
cannot be combined using logical connectives. To combine two boolean
values `x` and `y` using conjunction you have to write
`x=TRUE & y=TRUE`. To convert a predicate such as `z>0` into a boolean
value you have to use `bool(z>0)`.
[[sets]]
== Sets:
....
{} empty set
{E} singleton set
{E,F} set enumeration
{x|P} comprehension set
POW(S) power set
POW1(S) set of non-empty subsets
FIN(S) set of all finite subsets
FIN1(S) set of all non-empty finite subsets
card(S) cardinality
S*T cartesian product
S\/T set union
S/\T set intersection
S-T set difference
E:S element of
E/:S not element of
S<:T subset of
S/<:T not subset of
S<<:T strict subset of
S/<<:T not strict subset of
union(S) generalised union over sets of sets
inter(S) generalised intersection over sets of sets
UNION(z).(P|E) generalised union with predicate
INTER(z).(P|E) generalised intersection with predicate
....
[[numbers]]
== Numbers:
....
INTEGER set of integers
NATURAL set of natural numbers
NATURAL1 set of non-zero natural numbers
INT set of implementable integers (MININT..MAXINT)
NAT set of implementable natural numbers
NAT1 set of non-zero implementable natural numbers
n..m set of numbers from n to m
MININT the minimum implementable integer
MAXINT the maximum implementable integer
m>n greater than
m<n less than
m>=n greater than or equal
m<=n less than or equal
max(S) maximum of a set of numbers
min(S) minimum of a set of numbers
m+n addition
m-n difference
m*n multiplication
m/n division
m**n power
m mod n remainder of division
PI(z).(P|E) Set product
SIGMA(z).(P|E) Set summation
succ(n) successor (n+1)
pred(n) predecessor (n-1)
....
[[relations]]
== Relations:
....
S<->T relation
E|->F maplet
dom(r) domain of relation
ran(r) range of relation
id(S) identity relation
S<|r domain restriction
S<<|r domain subtraction
r|>S range restriction
r|>>S range subtraction
r~ inverse of relation
r[S] relational image
r1<+r2 relational overriding (r2 overrides r1)
r1><r2 direct product {x,(y,z) | x,y:r1 & x,z:r2}
(r1;r2) relational composition {x,y| x|->z:r1 & z|->y:r2}
(r1||r2) parallel product {((x,v),(y,w)) | x,y:r1 & v,w:r2}
prj1(S,T) projection function (usage prj1(Dom,Ran)(Pair))
prj2(S,T) projection function (usage prj2(Dom,Ran)(Pair))
closure1(r) transitive closure
closure(r) reflexive & transitive closure
(non-standard version: closure({}) = {}; see iterate(r,0) below)
iterate(r,n) iteration of r with n>=0
(Note: iterate(r,0) = id(s) where s = dom(r)\/ran(r))
fnc(r) translate relation A<->B into function A+->POW(B)
rel(r) translate relation A<->POW(B) into relation A<->B
....
[[functions]]
== Functions:
....
S+->T partial function
S-->T total function
S+->>T partial surjection
S-->>T total surjection
S>+>T partial injection
S>->T total injection
S>+>>T partial bijection
S>->>T total bijection
%x.(P|E) lambda abstraction
f(E) function application
f(E1,...,En) is now supported (as well as f(E1|->E2))
....
[[sequences]]
== Sequences:
....
<> or [] empty sequence
[E] singleton sequence
[E,F] constructed sequence
seq(S) set of sequences over Sequence
seq1(S) set of non-empty sequences over S
iseq(S) set of injective sequences
iseq1(S) set of non-empty injective sequences
perm(S) set of bijective sequences (permutations)
size(s) size of sequence
s^t concatenation
E->s prepend element
s<-E append element
rev(s) reverse of sequence
first(s) first element
last(s) last element
front(s) front of sequence (all but last element)
tail(s) tail of sequence (all but first element)
conc(S) concatenation of sequence of sequences
s/|\n take first n elements of sequence
s\|/n drop first n elements from sequence
....
[[records]]
== Records:
....
struct(ID:S,...,ID:S) set of records with given fields and field types
rec(ID:E,...,ID:E) construct a record with given field names and values
E'ID get value of field with name ID
....
[[strings]]
== Strings:
....
"astring" a specific (single-line) string value
'''astring''' an alternate way of writing (multi-line) strings, no need to escape "
STRING the set of all strings
Note: for the moment enumeration of strings is limited (if a variable
of type STRING is not given a value by the machine, then ProB assumes
STRING = { "STR1", "STR2" })
....
Atelier-B does not support any operations on strings, apart from
equality and disequality. However, the ProB
<<external-functions,external function library>> contains several
operators on strings. ProB also allows multi-line strings. As of version
1.7.0, ProB will support the following escape sequences within strings:
....
\n newline (ASCII character 13)
\r carriage return (ASCII 10)
\t tab (ASCII 9)
\" the double quote symbol "
\' the single quote symbol '
\\ the backslash symbol
....
Within single-line string literals, you do not need to escape '. Within
multi-line string literals, you do not need to escape " and you can use
tabs and newlines. ProB assumes that all B machines and strings use the
UTF-8 encoding.
[[trees]]
== Trees:
Nodes in the tree are denoted by index sequences (branches), e.g,
n=[1,2,1] Each node in the tree is labelled with an element from a
domain S. A tree is a function mapping of branches to elements of the
domain S.
....
tree(S) set of trees over domain S
btree(S) set of binary trees over domain S
top(t) top of a tree
const(E,s) construct a tree from info E and sequence of subtrees s
rank(t,n) rank of the node at end of branch n in the tree t
father(t,n) father of the node denoted by branch n in the tree t
son(t,n,i) the ith son of the node denoted by branch n in tree t
sons(t) the sequence of sons of the root of the tree t
subtree(t,n)
arity(t,n)
bin(E) construct a binary tree with a single node E
bin(tl,E,tr) construct a binary tree with root info E and subtrees tl,tr
left(t) the left (first) son of the root of the binary tree t
right(t) the right (last) son of the root of the binary tree t
sizet(t) the size of the tree (number of nodes)
prefix(t) the nodes of the tree t in prefix order
postfix(t) the nodes of the tree t in prefix order
mirror, infix are recognised by the parser but not yet supported by ProB itself
....
[[let-and-if-then-else]]
== LET and IF-THEN-ELSE
ProB allows the following for predicates and expressions:
....
IF P THEN E1 ELSE E2 END conditional for expressions or predicates E1,E2
LET x1,... BE x1=E1 & ... IN E END
....
Note: The expressions E1,... defining x1,... are not allowed to use x1,...
[[statements-aka-substitutions]]
== Statements (aka Substitutions):
....
skip no operation
x := E assignment
f(x) := E functional override
x :: S choice from set
x : (P) choice by predicate P (constraining x)
x <-- OP(x) call operation and assign return value
G||H parallel substitution**
G;H sequential composition**
ANY x,... WHERE P THEN G END non deterministic choice
LET x,... BE x=E & ... IN G END
VAR x,... IN G END generate local variables
PRE P THEN G END
ASSERT P THEN G END
CHOICE G OR H END
IF P THEN G END
IF P THEN G ELSE H END
IF P1 THEN G1 ELSIF P2 THEN G2 ... END
IF P1 THEN G1 ELSIF P2 THEN G2 ... ELSE Gn END
SELECT P THEN G WHEN ... WHEN Q THEN H END
SELECT P THEN G WHEN ... WHEN Q THEN H ELSE I END
CASE E OF EITHER m THEN G OR n THEN H ... END END
CASE E OF EITHER m THEN G OR n THEN H ... ELSE I END END
WHEN P THEN G END is a synonym for SELECT P THEN G END
**: cannot be used at the top-level of an operation, but needs to
be wrapped inside a BEGIN END or another statement (to avoid
problems with the operators ; and ||).
....
[[machine-header]]
== Machine header:
....
MACHINE or REFINEMENT or IMPLEMENTATION
Note: machine parameters can either be SETS (if identifier is all upper-case)
or scalars (i.e., integer, boolean or SET element; if identifier is not
all upper-case; typing must be provided be CONSTRAINTS)
You can also use MODEL or SYSTEM as a synonym for MACHINE, as well
as EVENTS as a synonym for OPERATIONS.
....
[[machine-sections]]
== Machine sections:
----
CONSTRAINTS P (logical predicate)
SETS S;T={e1,e2,...};...
CONSTANTS x,y,...
CONCRETE_CONSTANTS cx,cy,...
PROPERTIES P (logical predicate)
DEFINITIONS m(x,...) == BODY;....
VARIABLES x,y,...
CONCRETE_VARIABLES cv,cw,...
INVARIANT P (logical predicate)
ASSERTIONS P;...;P (list of logical predicates separated by ;)
INITIALISATION
OPERATIONS
----
[[machine-inclusion]]
== Machine inclusion:
....
USES list of machines
INCLUDES list of machines
SEES list of machines
EXTENDS list of machines
PROMOTES list of operations
REFINES machine
CSP_CONTROLLER controller will use controller.csp to guide machine (currently disabled in 1.3)
Note:
Refinement machines should express the operation preconditions in terms
of their own variables.
....
[[definitions]]
== Definitions:
....
NAME1 == Expression; Definition without arguments
NAME2(ID,...,ID) == E2; Definition with arguments
....
....
"FILE.def"; Include definitions from file`
....
There are a few Definitions which can be used to influence the animator:
....
GOAL == P to define a custom Goal predicate for Model Checking
(the Goal is also set by using "Advanced Find...")
SCOPE == P to limit the search space to "interesting" nodes
scope_SETNAME == n..n to define custom cardinality for set SETNAME
scope_SETNAME == n equivalent to 1..n
SET_PREF_MININT == n
SET_PREF_MAXINT == n
SET_PREF_MAX_INITIALISATIONS == n max. number of intialisations computed
SET_PREF_MAX_OPERATIONS == n max. number of enablings per operation computed
SET_PREF_SYMBOLIC == TRUE/FALSE
ASSERT_LTL... == "LTL Formula" using X,F,G,U,R LTL operators +
Y,O,H,S Past-LTL operators +
atomic propositions: e(OpName), [OpName], {BPredicate}
ANIMATION_FUNCTION == e a function (INT*INT) +-> INT or an INT
ANIMATION_FUNCTION_DEFAULT == e a function (INT*INT) +-> INT or an INT
instead of any INT above you can also use BOOL or any SET
ANIMATION_IMGn == "PATH to .gif" a path to a gif file
ANIMATION_STRn == "sometext" a string without spaces
....
[[comments-and-pragmas]]
== Comments and Pragmas
....
B supports two styles of comments:
/* ... */ block comments
// ... line comments
....
----
ProB recognises several pragma comments of the form /*@ PRAGMA VALUE */
The whitespace between @ and PRAGMA is optional.
/*@symbolic */ put before comprehension set or lambda to instruct ProB
to keep it symbolic and not try to compute it explicitly
/*@label LBL */ associates a label LBL with the following predicate
(LBL must be identifier or a string "....")
/*@desc DESC */ associates a description DESC with the preceding predicate
/*@file PATH */ associates a file for machines in SEES, INCLUDES, ...
put pragma after a seen or included machine
/*@package NAME */ at start of machine, machine file should be in folder NAME/...
NAME can be qualified N1.N2...Nk, in which case the machine
file should be in N1/N2/.../Nk
/*@import-package NAME */ adds ../NAME to search paths for SEES,...
NAME can also be qualified N1.N2...Nk, use after package pragma
/*@unit U */ associates a unit U with the following constant or variable in the
CONSTANTS or VARIABLES section, possible units are, e.g.,
"m", "s", "mps", "m * s**-2" (quotes must be used);
see https://www3.hhu.de/stups/prob/index.php/Tutorial_Unit_Plugin
----
[[file-extensions]]
== File Extensions
....
.mch for abstract machine files
.ref for refinement machines
.imp for implementation machines
.def for DEFINITIONS files
.rmch for Rules machines for data validation
....
[[differences-with-atelierbb4free]]
== Differences with AtelierB/B4Free
Basically, ProB tries to be compatible with Atelier B and conforms to
the semantics of Abrial's B-Book and of
http://www.atelierb.eu/php/documents-en.php#manuel-reference[Atelier B's
reference manual]. Here are the main differences with Atelier B:
- Tuples without parentheses are not supported; write `(a,b,c)` instead of a,b,c
- Relational composition has to be wrapped into parentheses; write `(f;g)`
- Parallel product also has to be wrapped into parentheses; write `(f||g)`
- Trees are not yet fully supported
- The VALUES clause is only partially supported
- Definitions have to be syntactically correct and be either an expression,
predicate or substitution;
the arguments to definitions have to be expressions;
definitions which are predicates or substitutions must be declared before first use
- Definitions are local to a machine
- For ProB the order of fields in a record is not relevant (internally the fields are
sorted), Atelier-B reports a type error if the order of the name of the fields changes
- Well-Definedness: for disjunctions and implications ProB uses the L-system
of well-definedness (i.e., for `P => Q`, P should be well-defined and
if P is true then Q should also be well-defined)
- ProB allows WHILE loops and sequential composition in abstract machines
- ProB now allows the IF-THEN-ELSE and LET for expressions and predicates
(e.g., `IF x<0 THEN -x ELSE x END or LET x BE x=f(y) IN x+x END`)
- ProB's type inference is stronger than Atelier-B's, much less typing predicates
are required
- ProB accepts operations with parameters but without pre-conditions
- ProB allows identifiers consisting of a single character
- ProB allows multi-line strings and supports UTF-8 characters in strings,
and ProB allows string literals written using three apostrophes (`'''string'''`)
- ProB allows a she-bang line in machine files starting with `#!` +
(If you discover more differences, please let us know!)
See also: <<using_prob_with_atelier,Using ProB with AtelierB>>
Also note that there are various differences between BToolkit and
AtelierB/ProB:
- AtelierB/ProB do not allow true as predicate;
e.g., PRE true THEN ... END is not allowed (use BEGIN ... END instead)
- AtelierB/ProB do not allow a machine parameter to be used in the PROPERTIES
- AtelierB/ProB require a scalar machine parameter to be typed in the
CONSTRAINTS clause
- In AtelierB/ProB the BOOL type is pre-defined and cannot be redefined
[[other-notes]]
== Other notes
ProB is best at treating universally quantified formulas of the form `!x.(x:SET => RHS)`,
or `!(x,y).(x|->y:SET =>RHS)`, `!(x,y,z).(x|->y|->z:SET =>RHS)`, ...;+
otherwise the treatment of `!(x1,...,xn).(LHS => RHS)` may delay until all values treated by LHS are known. +
Similarly, expressions of the form `SIGMA(x).(x:SET|Expr)` and `PI(x).(x:SET|Expr)` lead to better constraint propagation. +
The construction S:FIN(S) is recognised by ProB as equivalent to the Event-B finite(S) operator. +
ProB assumes that machines and STRING values are encoded using UTF-8.
src/docs/chapter/user/12_BLanguage/02_Types.adoc deleted 100644 → 0
+ 0
− 103
View file @ b72bf27a
[[types]]
= Types
ProB requires all constants and variables to be typed. As of version
1.3, ProB uses a new unification-based type inference and checking
algorithm. As such, you should be able to use most Atelier B models
without problem. On the other hand, certain models that ProB accepts
will have to be rewritten to be type checked by Atelier B (e.g., by
adding additional typing predicates). Also note that, in contrast to
Atelier B, ProB will type check macro DEFINITIONS.
[[what-is-a-basic-type-in-b]]
== What is a basic type in B
* BOOL
* INTEGER
* Any name of a set introduced in a SETS clause or introduced as a
parameter of the machine
* POW (τ) (power set) for τ being a type
* τ1 * τ2 (Cartesian product) for τ1 and τ2 being two types
[[what-needs-to-be-typed]]
== What needs to be typed
Generally speaking, any constant or variable. More precisely:
* Constants declared in the CONSTANTS clause must be typed in the
PROPERTIES clause;
* Variables declared in the VARIABLES clause must be typed in the
INVARIANT;
* Arguments of an operation must be typed in the precondition PRE or a
top-level SELECT statement of the operation;
* Variables in universal or existential quantifications;
* Variables of set comprehensions must be typed in a conjunct of the
body of the set comprehension. For example, `\{xx | xx:NAT & xx>0 & xx<5}`
is fine, but `\{xx | xx>0 & xx<5}` is not;
* Variables of lambda abstractions must be typed in the predicate part
of the abstraction. For example, `%yy.(yy:NAT|yy-1)` properly types the
variable `yy`;
* Variables introduced in ANY statements must be typed in the WHERE part
of the statement.
ProB will warn you if a variable has not been given a type.
*HINT: The Analyse|Show Typing command reveals the typing that ProB has
inferred for your constants and global variables.*
[[restriction-on-the-domains-of-the-variables]]
== Restriction on the Domains of the Variables
Animating and verifying a B specification is in principle undecidable.
ProB overcomes this by requiring that the domain of the variables is
finite (i.e., with finitely many values) or integer. This ensures that
the state space has finite size. Typing of the B specification ensures
this restriction.
In the B specification, a set is either defined explicitely, thus being
a finite domain, or its definition is deferred. In the later case, the
user can indicate the size of the set mySET (without defining its
elements) by creating a macro in the DEFINITIONS clause with the name
`scope_mySET` and an integer value (e.g. `scope_mySET==2`) or a value
specified as a range (e.g. `scope_mySET == 1..12`). The macros with the
prefix `scope_` will be used by ProB and do not modify the B
specification. If the size of the set is unspecified, ProB considers the
set to have a default size. The value for the default size is defined in
the Preferences|Animation Preferences... preference window by the
preference Size of unspecified sets in SETS section.
The B method enables to specify the size of a set with the card operator
in the PROPERTIES clause; this form of constraint is now supported by
ProB, provided it is of a simple form `card(S)=Nr`, where `S` is a deferred
set and `Nr` a natural number.
[[enumeration-in-prob]]
== Enumeration in ProB
The typing information is used by ProB to enumerate the possible values
of a constant or a variable whenever a specification does not narrow
down that value to a single value.
For example, if you write `xx:NAT & xx=1` ProB does not have to resort to
enumeration as the `xx=1` constraint imposes a single possible value for
`xx`. However, if you write `xx:NAT & xx<3` ProB will enumerate the possible
values of `xx` in order to find those that satisfy the constraints imposed
by the machine (here 0,1,2).
ProB will use the constraints to try to cut down the enumeration space,
and will resort to enumeration usually only as a last resort. So
something like `xx:NAT & xx<10 & x>2 & x=5` will not result in
enumeration.
The enumeration range for integers is controlled by two preferences in
the Preferences|Animation Preferences... preference window: `!MinInt`,
used for expressions such as `xx::INT`, and `!MaxInt`, used for expressions
such as `xx::NAT` preferences. Nevertheless, writing `xx: NAT & xx = 55`
puts the value `55` in `xx` no matter what `!MaxInt` is set to, as no
enumeration is required.
Note that these preferences also apply to the mathematical integers
(INTEGER) and natural numbers (NATURAL). In case a mathematical integer
or natural number is enumerated (using `!MinInt` and `!MaxInt`) a warning is
printed on the console.
src/docs/chapter/user/12_BLanguage/03_Deferred_Sets.adoc deleted 100644 → 0
+ 0
− 69
View file @ b72bf27a
[[deferred-sets]]
= Deferred Sets
A deferred set in B is declared in the SETS Section and is not
explicitly enumerated. In the example below, AA is a deferred set and BB
is an enumerated set.
....
MACHINE M0
SETS AA; BB={bb,cc,dd}
END
....
ProB in general requires all deferred sets to be given a finite
cardinality before starting animation or model checking. If no
cardinality is specified, a default size will be used (which is
controlled by the `DEFAULT_SETSIZE`
<<controlling-prob-preferences,preference>>).
In general (for both probcli and ProB Tcl/Tk) you can set the
cardinality of a set AA either by
* making it an enumerated set, i.e., adding `AA = {v1,v2,…}` to the SETS
clause
* adding a predicate `card(AA) = constant` to the PROPERTIES clause
* Note: various other predicates in the PROPERTIES clause will also
influence the size used for AA by ProB, for example:
`- card(AA) > 1` +
`- aa:AA & bb:AA & aa/=bb` +
`- AA = {aa,bb} & aa/=bb` +
`- …`
* you can add a DEFINITION `scope_AA == constant` to instruct ProB to
set the cardinality of AA to the constant.
[[using-refinement-for-animation-preferences]]
== Using Refinement for Animation Preferences
Note: instead of adding AA = \{aa,bb} to the SETS clause you can also
add `AA = {aa,bb} & aa/=bb` to the PROPERTIES clause. This can also be
done in a refinement. A good idea is then to generate a refinement for
animation with ProB (which may contain other important settings for
animation):
....
REFINEMENT M0_ProB REFINES M0
CONSTANTS aa,bb
PROPERTIES
AA = {aa,bb} & aa/=bb
END
....
[[setting-deferred-set-cardinalities-within-probcli]]
== Setting Deferred Set Cardinalities within probcli
From the command-line, using probcli you can use the command-line
switch:
`-card <GS> <VAL>`
Example:
`probcli my.mch -card PID 5`
See
<<using-the-command-line-version-of-prob,manual
page for probcli>>.
src/docs/chapter/user/12_BLanguage/10_External_Functions.adoc deleted 100644 → 0
+ 0
− 116
View file @ b72bf27a
[[external-functions]]
= External Functions
As of version 1.3.5-beta7 ProB can make use of externally defined
functions. These functions must currently be written in Prolog (in
principle C, Java, Tcl or even other languages can be used via the
SICStus Prolog external function interfaces). These functions can be
used to write expressions, predicates, or substitutions. The general
mechanism that is used is to mark certain DEFINITIONS as external, in
which case ProB will make use of external Prolog code rather than using
the right-hand-side of the DEFINITION whenever it is used. However,
these DEFINITIONS can often (unless they are polymorphic) be wrapped
into B (constant) functions. If you just want to use the standard
external functions already defined by ProB, then you don't have to
understand this mechanism in detail (or at all).
[[standard-libraries-provided-by-prob]]
== Standard Libraries provided by ProB
In a first instance we have predefined a series of external functions
and grouped them in various library machines and definition files:
* `LibraryMath.mch`: defining sin, cos, tan, sinx, cosx, tanx, logx,
gcd, msb, random as well as access to all other Prolog built-in
arithmetic functions.
* `LibraryStrings.mch`: functions manipulating B STRING objects by
providing `length`, `append`, `split` and conversion functions `chars`,
`codes`.
* `LibraryFiles.mch`: various functions to obtain information about
files and directories in the underlying file system.
* `LibraryIO.def`: providing functions to write information to screen or
file. Note: these external functions are polymorphic and as such cannot
be defined as B constants: you have to use the DEFINITIONS provided in
`LibraryIO.def`.
* `CHOOSE.def`: providing the
http://planetmath.org/encyclopedia/HilbertsEpsilonOperator.html[Hilbert
choice operator] for choosing a designated element from each set. Again,
this function is polymorphic and thus cannot be defined as a B function.
This function is useful for defining
<<recursively-defined-functions,recursive functions>> over sets (see
also <<tla,TLA>>). Note that it in ProB it is undefined for the empty
set.
* `LibraryMeta.def`: providing access to meta-information about the
loaded model (`PROJECT_INFO`), about the state space (`HISTORY`,
`STATE_TRANS`, ...) and about ProB itself (GET_PREF, `PROB_INFO_STR`,
`PROB_INFO_INT`,..).
As of version 1.6.1 there is also a `READ_XML` external function to read
in XML files and convert them to a B data structure with strings and
records.
Since version 1.5 the standard library is shipped with ProB and
references to machines and DEFINITION-files in the standard library are
resolved automatically when referenced (see <<probpath,PROBPATH>> for
information about how to customize the lookup path).
To use a library machine you can use the `SEES` mechanism:
`SEES LibraryMath`
In general you can do the following with an external function, such as
`sin`, wrapped into a constant:
* apply the function: `sin(x)`
* compute the image of the function: `sin[1..100]`
* compose the function with a finite relation on the left:
`([1..100] ; sin)`
* compute the domain of the function: `dom(sin)`
To use a library definition file, you need to include the file in the
DEFINITIONS clause:
-------------
DEFINITIONS
"LibraryIO.def"
-------------
[[overview-of-the-external-function-definition-mechanism]]
== Overview of the External Function DEFINITION Mechanism
Currently, external functions are linked to classical B machines using B
DEFINITIONS as follows:
* one definition, which defines the function as it is seen by tools
other than ProB (e.g., Atelier-B). Suppose we want to declare an
external cosinus function named `COS`, then this definition could be
`COS(x) == cos(x)`.
* one definition declaring the type of the function. For `COS` this
would be `EXTERNAL_FUNCTION_COS == INTEGER --> INTEGER`.
* Prolog code which gets called by ProB in place of the right-hand-side
of the first definition
Usually, it is also a good idea to encapsulate the external function
inside a CONSTANT which is defined as a lambda abstraction with as body
simply the call to the first DEFINITION. For `COS` this would be
`cos = %x.(x:NATURAL|COS(x))`. Observe that for Atelier-B this is a
tautology. For ProB, the use of such a constant allows one to have a
real B function representing the external function, for which we can
compute the domain, range, etc.
For the typing of an external function `NAME` with type `TYPE` there are
three possibilities, depending on whether the function is a function, a
predicate or a substitution:
* `EXTERNAL_FUNCTION_NAME == TYPE`
* `EXTERNAL_PREDICATE_NAME == TYPE`
* `EXTERNAL_SUBSTITUTION_NAME == TYPE`
In case the external function is polymorphic, the `DEFINITION` can take
extra arguments: each argument is treated like a type variable. For
example, the following is used in `CHOOSE.def` to declare the
http://planetmath.org/encyclopedia/HilbertsEpsilonOperator.html[Hilbert
choice operator]:
* `EXTERNAL_FUNCTION_CHOOSE(T) == (POW(T)-->T)`
src/docs/chapter/user/12_BLanguage/11_Recursively_Defined_Functions.adoc deleted 100644 → 0
+ 0
− 199
View file @ b72bf27a
[[recursively-defined-functions]]
= Recursively Defined Functions
[[symbolic-functions-and-relations]]
== Symbolic Functions and Relations
Take the following function:
---------
CONSTANTS parity
PROPERTIES
parity : (NATURAL --> {0,1}) &
parity(0) = 0 &
!x.(x:NATURAL => parity(x+1) = 1 - parity(x))
---------
Here, ProB will complain that it cannot find a solution for parity. The
reason is that parity is a function over an infinite domain, but ProB
tries to represent the function as a finite set of maplets.
There are basically four solutions to this problem:
* Write a finite function:
---------
parity : (NAT --> {0,1}) &
parity(0) = 0 &
!x.(x:NAT & x<MAXINT => parity(x+1) = 1 - parity(x))
---------
* Rewrite your function so that in the forall you do not refer to values
of parity greater than x:
---------
parity : (NATURAL --> {0,1}) &
parity(0) = 0 &
!x.(x:NATURAL1 => parity(x) = 1 - parity(x-1))
---------
* Write your function constructively using a single recursive equation
using set comprehensions, lambda abstractions, finite sets and set
union. This requires ProB 1.3.5-beta7 or higher and you need to declare
`parity` as `ABSTRACT_CONSTANT`. Here is a possible equation:
---------
parity : INTEGER <-> INTEGER &
parity = {0|->0} \/ %x.(x:NATURAL1|1-parity(x-1))
---------
Note, you have to remove the check `parity : (NATURAL --> {0,1})`, as
this will currently cause expansion of the recursive function. We
describe this new scheme in more detail below.
* Another solution is try and write your function constructively and
non-recursively, ideally using a lambda abstraction:
---------
parity : (NATURAL --> INTEGER) &
parity = %x.(x:NATURAL|x mod 2)
---------
* Here ProB detects that parity is an infinite function and will keep it
symbolic (if possible). With such an infinite function you can:
** apply the function, e.g., `parity(10001)` is the value `1`
** compute the image of the function, e.g., `parity[10..20]` is `{0,1}`
** check if a tuple is a member of the function, e.g., `20|->0 : parity`
** check if a tuple is not a member of the function, e.g.,
`21|->0 /: parity`
** check if a finite set of tuples is a subset of the function, e.g.,
`{20|->0, 120|->0, 121|->1, 1001|->1} <: parity`
** check if a finite set of tuples is not a subset of the function,
e.g., `{20|->0, 120|->0, 121|->1, 1001|->2} /<: parity`
** compose the function with a finite relation, e.g.,
`(id(1..10) ; parity)` gives the value `[1,0,1,0,1,0,1,0,1,0]`
** sometimes compute the domain of the function, here, `dom(parity)` is
determined to be `NATURAL`. But this only works for simple infinite
functions.
** sometimes check that you have a total function, e.g.,
`parity: NATURAL --> INTEGER` can be checked by ProB. However, if you
change the range (say from `INTEGER` to `0..1`), then ProB will try to
expand the function.
** In version 1.3.7 we are adding more and more operators that can be
treated symbolically. Thus you can now also compose two symbolic
functions using relational composition `;` or take the transitive
closure (`closure1`) symbolically.
You can experiment with those by using the <<eval-console,Eval
console>> of ProB, experimenting for example with the following complete
machine. Note, you should use ProB 1.3.5-beta2 or higher. (You can also
type expressions and predicates such as
`parity = %x.(x:NATURAL|x mod 2) & parity[1..10] = res` directly into
the online version of the <<eval-console,Eval console>>).
---------
MACHINE InfiniteParityFunction
CONSTANTS parity
PROPERTIES
parity : NATURAL --> INTEGER &
parity = %x.(x:NATURAL|x mod 2)
VARIABLES c
INVARIANT
c: NATURAL
INITIALISATION c:=0
OPERATIONS
inc = BEGIN c:=c+1 END;
r <-- Parity = BEGIN r:= parity(c) END;
r <-- ParityImage = BEGIN r:= parity[0..c] END;
r <-- ParityHistory = BEGIN r:= (%i.(i:1..c+1|i-1) ; parity) END
END`
---------
You may also want to look at the tutorial page on
<<tutorial-modeling-infinite-datatypes,modeling infinite datatypes>>.
[[when-does-prob-treat-a-set-comprehension-or-lambda-abstraction-symbolically]]
=== When does ProB treat a set comprehension or lambda abstraction symbolically ?
Currently there are four cases when ProB tries to keep a function such
as `f = %x.(PRED|E)` symbolically rather than computing an explicit
representation:
* the domain of the function is obviously infinite; this is the case for
predicates such as `x:NATURAL`; in version 1.3.7-beta5 or later this has
been considerably improved. Now ProB also keeps those lambda
abstractions or set comprehensions symbolic where the constraint solver
cannot reduce the domain of the parameters to a finite domain. As such,
e.g., `{x,y,z| x*x + y*y = z*z}` or `{x,y,z| z:seq(NATURAL) & x^y=z}`
are now automatically kept symbolic.
* `f` is declared to be an `ABSTRACT_CONSTANT` and the equation is part
of the `PROPERTIES` with `f` on the left.
* the preference `SYMBOLIC` is set to true (e.g., using a `DEFINITION`
`SET_PREF_SYMBOLIC == TRUE`)
* a pragma is used to mark the lambda abstraction as symbolic as
follows: `f = /*@ symbolic */ %x.(PRED|E)`; this requires ProB version
1.3.5-beta10 or higher. In Event-B, pragmas are represented as Rodin
database attributes and one should use the
<<tutorial-symbolic-constants,symbolic constants plugin>>.
[[recursive-function-definitions-in-prob]]
== Recursive Function Definitions in ProB
As of version 1.3.5-beta7 ProB now accepts recursively defined
functions. For this:
* the function has to be declared an `ABSTRACT_CONSTANT`.
* the function has to be defined using a single recursive equation with
the name of the function on the left of the equation
* the right-hand side of the equation can make use of lambda
abstractions, set comprehensions, set union and other finite sets
Here is a full example:
---------
MACHINE Parity
ABSTRACT_CONSTANTS parity
PROPERTIES
parity : INTEGER <-> INTEGER &
parity = {0|->0} \/ %x.(x:NATURAL1|1-parity(x-1))
END
---------
As of version 1.6.1 you can also use IF-THEN-ELSE and LET constructs in
the body of a recursive function. The above example can for example now
be written as:
---------
MACHINE ParityIFTE
ABSTRACT_CONSTANTS parity
PROPERTIES
parity : INTEGER <-> INTEGER &
parity = %x.(x:NATURAL|IF x=0 THEN 0 ELSE 1-parity(x-1)END)
SEND
---------
[[operations-applicable-for-recursive-functions]]
=== Operations applicable for recursive functions
With such a recursive function you can:
* apply the function to a given argument, e.g., `parity(100)` will give
you 0;
* compute the image of the function, e.g., `parity[1..10]` gives
`{0,1}`.
* composing it with another function, notably finite sequences:
`([1,2] ; parity)` corresponds to the "map" construct of functional
programming and results in the output `[1,0]`.
Also, you have to be careful to avoid accidentally expanding these
functions. For example, trying to check `parity : INTEGER <-> INTEGER`
or `parity : INTEGER +-> INTEGER` will cause older version of ProB to
try and expand the function. ProB 1.6.1 can actually check
`parity:NATURAL --> INTEGER`, but it cannot check
`parity:NATURAL --> 0..1`.
There are the following further restrictions:
* ProB does not support mutual recursion yet.
* The function is not allowed to depend on other constants, unless those
other constants can be valued in a deterministic way (i.e., ProB finds
only one possible solution for them).
src/docs/chapter/user/12_BLanguage/13_Memoization.adoc deleted 100644 → 0
+ 0
− 48
View file @ b72bf27a
[[function-memoization]]
= Memoization for Functions
As of version 1.9.0-beta9 ProB allows you to annotate functions in the ABSTRACT_CONSTANTS section for memoization.
[https://en.wikipedia.org/wiki/Memoization Memoization] is a technique for storing results of function applications and reusing the result if possible to avoid re-computing the function for the same arguments again.
To enable memoization you either need to
* annotate the function in the ABSTRACT_CONSTANTS section with the pragma `/*@desc memo */`
* set the preference `MEMOIZE_FUNCTIONS` to true. In this case ProB will try to memoize all functions in the ABSTRACT_CONSTANTS section, unless they are obviously small and finite and can thus be precomputed completely.
Take the following example:
---------
MACHINE MemoizationTests
ABSTRACT_CONSTANTS
fib /*@desc memo */,
fact /*@desc memo */
PROPERTIES
fib = %x.(x:NATURAL |
(IF x=0 or x=1 THEN 1
ELSE fib(x-1)+fib(x-2)
END))
&
fact = %x.(x:NATURAL|(IF x=0 THEN 1 ELSE x*fact(x-1) END))
ASSERTIONS
fib(30)=1346269;
fib[28..30] = {514229,832040,1346269};
END
---------
Memoization means that the recursive Fibonacci function now runs in linear time rather than in exponential time.
Generally, memoization is useful for functions which are complex to compute but which are called repeatedly with the same arguments.
As can be seen above, memoization is active for
* function calls such as fib(30) (which in turn calls fib(29) and fib(28) which are also memoized)
* computation of relational image such as fib[28..30], which internally results in three function calls to fib
The following points are relevant:
* Memoization is currently only possible for functions declared in the ABSTRACT_CONSTANTS section
* Memoization means that all results of function calls are stored. The memoization table is reset when another B machine is loaded or the same B machine is re-loaded.
* Memoized functions are automatically marked as symbolic. If your function is finite and relatively small, it may be better to put the function into the CONCRETE_CONSTANTS section so that it gets computed in its entirety once.
* Memoization of a function f is currently <b>not</b> active for computations such as dom(f), ran(f) or x|->y:f.
With the command-line version probcli you can use the `-profile` command to obtain some statistics about memoization.
\ No newline at end of file
src/docs/chapter/user/12_BLanguage/20_Tips_B_Idioms.adoc deleted 100644 → 0
+ 0
− 242
View file @ b72bf27a
[[tips-b-idioms]]
= Tips: B Idioms
Also have a look at <<tips-writing-models-for-prob,Tips:_Writing_Models_for_ProB>>.
[[let]]
== Let
Classical B only has a LET substitution, no let construct for predicates
or expressions. Event-B has no let construct whatsoever.
[[probs-extended-syntax]]
=== ProB's Extended Syntax
Since version *1.6.1-beta* (28th of April 2016), ProB supports the use
of the `LET` substitution syntax in expressions and predicates.
[[examples-let]]
==== Examples:
----
>>> LET a BE a = 10 IN a + 10 END
Expression Value = 20
----
----
>>> LET a BE a=10 IN a END + 10
Expression Value = 20
----
----
>>> LET a BE a=10 IN a END = 10
Predicate is TRUE
----
----
>>> LET a BE a = 10 IN a < 10 END
Predicate is FALSE
----
----
>>> LET a BE a=10 IN a /= 10 END or 1=1
Predicate is TRUE
----
----
>>> LET a, b BE a = 10 & b = 1 IN a + b END
Expression Value = 11
----
[[let-for-predicates]]
=== Let for predicates
For predicates this encodes a let predicate:
`#x.(x=E & P)`
corresponds to something like
`let x=E in P`
Within set comprehensions one can use the following construct:
`dom({x,y|y=E & P})`
corresponds to something like
`{x|let y=E in P}`
One can also use the ran operator or introduce multiple lets in one go:
`dom(dom({x,y,z|y=E1 & z=E2 &P}))`
or
`ran({y,z,x|y=E1 & z=E2 &P})`
both encode
`{x|let y=E1 & z=E2 in P}`
[[let-for-expressions]]
=== Let for expressions
In case F is a set expression, then the following construct can be used
to encode a let statement:
`UNION(x).(x=E|F)`
corresponds to something like
`let x=E in F`
The following construct has exactly the same effect:
`INTER(x).(x=E|F)`
[[if-then-else]]
== If-Then-Else
Classical B only has an IF-THEN-ELSE substitution (aka statement), no
such construct for predicates or expressions.
[[nightly-builds]]
=== Nightly Builds
Since version *1.6.1-beta* (28th of April 2016), ProB supports the use
of the `LET` substitution syntax in expressions and predicates.
[[examples-if-then-else]]
==== Examples:
----
>>> IF 1 = 1 THEN 3 ELSE 4 END
Expression Value = 3
----
----
>>> IF 1 = 1 THEN 3 ELSE 4 END + 5
Expression Value = 8
----
----
>>> IF 1=1 THEN TRUE = FALSE ELSE TRUE=TRUE END
Predicate is FALSE
----
----
>>> IF 1=1 THEN TRUE = FALSE ELSE TRUE=TRUE END or 1=1
Predicate is TRUE
----
[[expressions]]
=== Expressions
The following construct
`%((x).(x=0 & PRED|C1)\/%(x).(x=0 & not(PRED)|C2)) (0)`
encodes an if-then-else for expressions:
`IF PRED THEN C1 ELSE C2 END`
The former lambda-construct is recognised by ProB and replaced
internally by an if-then-else construct. The latter syntax is actually
now recognised as well by ProB 1.6 (version 1.6.0 still requires
parentheses around the IF-THEN-ELSE; version 1.6.1 no longer requires
them).
[[finite]]
== finite
In classical B there is no counterpart to the Event-B `finite` operator.
However, the following construct has the same effect as `finite(x)` (and
is recognised by ProB):
`x : FIN(x)`
[[all-different]]
== all-different
One can encode the fact that n objects x1,...,xn are pair-wise different
using the following construct (recognised by ProB):
`card({x1,...,xn})=n`
[[map]]
== map
Given a function f and a sequence `sqce` one can map the function over
all elements of `sqce` using the relational composition operator `;`:
`(sqce ; f)`
For example, `([1,2,3] ; succ)` gives us the sequence `[2,3,4]`.
[[recursion-using-closure1]]
== Recursion using closure1
Even though B has no built-in support for recursion, one can use the
transitive closure operator `closure1` to compute certain recursive
functions. For this we need to encode the recursion as a step function
of the form:
`%(in,acc).(P|(inr,accr))`
where P is a predicate which in case we have not yet reached a base case
for the input value `in`. The computation result has to be stored in an
accumulator: `acc` is the accumulator before the recursion step, `accr`
after. `inr` is the new input value for the recursive call. In case the
base case is reached for `in`, the predicate P should be false and the
value of the recursive call should be the value of the accumulator.
The value of the recursive function can thus be obtained by calling:
`closure1(step)[{(in,ia)}](b)`
where `in` is the input value, `b` is the base case and `ia` is the
initial (empty) accumulator.
For example, to sort a set of integers into a ascending sequence, we
would define the step function as follows:
`step = %(s,o).(s/={} | (s\{min(s)},o<-min(s)))`
A particular call would be:
`closure1(step)[{({4,5,2},[])}]({})`
resulting in the sequence `[2,4,5]`.
Observe that, even though `closure1(step)` is an infinite relation, ProB
can compute the relational image of `closure1(step)` for a particular
set such as `{({4,5,2},[])}` (provided the recursion terminates).
[[recursion-using-abstract_constants]]
== Recursion using ABSTRACT:_CONSTANTS
Recursive functions can be declared using the `ABSTRACT_CONSTANTS`
section in B machines. Functions declared as `ABSTRACT_CONSTANTS` are
treated symbolically by ProB and not evaluated eagerly.
For example, to sort a set of integers into a ascending sequence, as
above, we would define a recursive function as follows:
----
ABSTRACT_CONSTANTS
Recursive_Sort
PROPERTIES
Recursive_Sort : POW(INTEGER) <-> POW(INTEGER*INTEGER)
& Recursive_Sort =
%in.(in : POW(INTEGER) & in = {} | [])
\/ %in.(in : POW(INTEGER) & in /= {}
| min(in) -> Recursive_Sort(in\{min(in)}))
----
By defining `Recursive_Sort` as an abstract constant we indicate that
ProB should handle the function symbolically, i.e. ProB will not try to
enumerate all elements of the function. The recursive function itself is
composed of two single functions: a function defining the base case and
a function defining the recursive case. Note, that the intersection of
the domains of these function is empty, and hence, the union is still a
function.
src/docs/chapter/user/12_BLanguage/21_Tips_Writing_Models_for_ProB.adoc deleted 100644 → 0
+ 0
− 122
View file @ b72bf27a
[[tips-writing-models-for-prob]]
= Tips: Writing Models for ProB
The most common issue is that ProB needs to find values for the
constants which satisfy the properties (aka axioms in Event-B). You
should read the tutorial pages on this (in particular
<<tutorial-setup-phases,Understanding the ProB Setup Phases>> and
<<tutorial-troubleshooting-the-setup,Tutorial Troubleshooting the
Setup>>)
* Try to use ProB as early as possible in the modeling process; this
will make it easier to identify the cause of problems (and also will
hopefully give you valuable feedback on your model as well).
* Try to put complicated properties into ASSERTIONS rather than
PROPERTIES. Something like `!s.(s<:S => P)` will have to check `P` for
all subsets of `S` (i.e., checking is exponential in the size of `S`)
* You may wish to give explicit values to certain constants. For
example, in Event-B, this can be done by refining a context.
* Try to set the symbolic preference of ProB to true (use
`-p SYMBOLIC TRUE` for probcli or set the Animation preference "Lazy
expansion ... (SYMBOLIC)" to true) if you have large or infinite
functions (see discussion about closure below). In symbolic mode, ProB
will keep lambda expressions and set comprehensions symbolic as much as
possible. In classical B, any `ABSTRACT_CONSTANT` will also at first be
kept symbolic. However, there are only limited things you can do with a
"symbolic" function without forcing an expansion: taking the value of
a function is fine, computing the image over a set is also possible as
is taking the union with another symbolic function.
[[effective-constraint-solving-with-prob]]
== Effective Constraint Solving with ProB
[[existential-quantifiers]]
=== Existential Quantifiers
Existential quantifiers can pose subtle problems when solving constraint
problems.
For an existential quantifier `#x.P` ProB will often wait until all
variables in P apart from x are known to evaluate the quantifier.
Indeed, if all variables apart from x are known, ProB can stop when it
finds one solution for x. Take for example:
`#x.(x:0..1000 & x=p) & p:101..104`
Here, ProB will wait until p is known (e.g., 101) before enumerating
possible values for x. However, it could be that the predicate P is
required to instantiate the outside variable, as in this example:
`#x.(x:100..101 & x=p) & p:NATURAL`
Here, the existential quantifier is required to narrow down the possible
values of p. Thus, before enumerating an unbounded variable, ProB will
start enumerating the existential variable x. Note, however, that the
priority with which it will be enumerated is much lower than if it was a
regular variable! Hence:
* Tip: Beware of putting important domain variables into existential
quantifiers.
One exception to the above treatment are existential quantifiers of the
form `#x.(x=E & P)`. They are recognised by ProB as LET-PREDICATES. This
is a good use of the existential quantifier. This quantifier will never
"block".
* Tip: use existential quantifiers as LET-PREDICATES `#x.(x=E & P)` to
avoid repeated computations
(<<common-subexpression-elimination,common-subexpression
elimination>>) and to make your predicates more readable.
[[universal-quantifiers]]
== Universal Quantifiers
The situation is very similar to the existential quantifier. In the
worst case ProB may delay evaluating a universal quantifier `!x.(P=>Q)`
until all variables in `P` are known so as to be able to determine all
values of `x` for which `Q` has to be checked.
There are a few optimisations:
* If ProB can determine that the domain of `x` is finite and small, then
the universal quantifier will be expanded into a conjunction. E.g.,
`!x.(x:1..3 & x<y => P(x))` will be expanded into
`(1<y => P(1)) & (2<y => P(2)) & (3<y => P(3))` even if `y` is not yet known.
Setting the preference `SMT` to true will increase the threshold for
which this expansion occurs.
* If the quantifier is of the form `!x.(x:S => P)`, then P will be
gradually checked for every new value that is added to `S`; ProB does
not wait for `S` to be completely known before checking the quantifier.
Tip: sometimes one can force expansion of a quantifier by using two
implications. E.g., suppose we know that the domain of `s` is a subset
of `1..10`, then we can rewrite `!x.(s(x)=5 => P(x))` into
`!x.(x:1..10 => (s(x)=5 => P(x)))`. This will ensure that the quantifier
is checked.
[[transitive-closure-in-event-b]]
== Transitive Closure in Event-B
Classical B contains the transitive closure operator `closure1`. It is
not available by default in Event-B, and axiomatisations of it may be
very difficult to treat by ProB. Indeed, if you define the transitive
closure in Event-B as a function `tclos` from relations to relations,
ProB will try to find a value for `tclos`. The search space for this
function is `(2\^n*n)^(2^n*n)`, where `n` is the size of the base set
(see <<tutorial-understanding-the-complexity-of-b-animation,Tutorial
Understanding the Complexity of B Animation>>). For n=3 this is already
way too big too handle (the search space has 1.40e+1387 relations).
Hence, in Event-B, you should use a theory of the transitive closure
which contains a special mapping file which instructs ProB to use the
classical B operator. See <<event-b-theories,the page on supporting
Event-B theories>> along with the links to theories that can be used
efficiently with ProB.
* Tip: within set comprehensions use the form `dom({x,y|P})` rather than
`{x|#y.P}`. This is generally more efficient.
src/docs/chapter/user/12_BLanguage/22_Debugging.adoc deleted 100644 → 0
+ 0
− 185
View file @ b72bf27a
[[debugging-prob]]
= Debugging Models with ProB
There are various ways in which you can debug your model.
We focus here on debugging performance issues
== Debugging with LibraryIO
The [[External Functions|standard library]] "LibraryIO.def" contains various external functions and predicates with which you can instrument your formal model.
To use the library in your model you need to include the following
....
DEFINITIONS
"LibraryIO.def"
....
With the external predicate <tt>printf</tt> you can view values of variables and identifiers. The printf predicate is always true and will print its arguments when all of them have been fully computed.
The printf predicate uses the format from SICStus Prolog for the format string.
The most important are <tt>~w</tt> for printing an argument and <tt>~n</tt>
for a newline. There must be exactly as many <tt>~w</tt> in the format string as there
are aguments.
Below is a small example, to inspect in which order ProB enumerates values.
The example is typed in the REPL of [[Using_the_Command-Line_Version_of_ProB|probcli]]
(started using the command <tt>probcli -repl File.mch</tt> where <tt>File.mch</tt> includes the definitions section above):
....
>>> {x,y | x:1..5 & y:1..2 & x+y=6 & printf("x=~w~n",[x]) & printf("y=~w~n",[y])}
y=1
x=5
y=2
x=4
Expression Value =
{(4|->2),(5|->1)}
....
As you can see, ProB has enumerated y before x, as its domain was smaller.
You can use the external function <tt>observe</tt> to inspect a list of
identifiers:
....
>>> {x,y | x:1..5 & y:1..2 & x+y=6 & observe((x,y))}
observing x
observing y
y = 1 (walltime: 562188 ms)
. x = 5 (walltime: 562188 ms)
..* Value complete: x |-> y = (5|->1) (walltime: 562188 ms)
------
y = 2 (walltime: 562188 ms)
. x = 4 (walltime: 562188 ms)
..* Value complete: x |-> y = (4|->2) (walltime: 562188 ms)
------
Expression Value =
{(4|->2),(5|->1)}
....
With the external function <tt>TIME</tt> you can get the current time in seconds:
....
>>> TIME("sec")
Expression Value =
11
>>> TIME("now")
Expression Value =
1581432376
>>> TIME("now")
Expression Value =
1581432377
....
With the external function <tt>DELTA_WALLTIME</tt> you can get the time in milliseconds since the last call to <tt>DELTA_WALLTIME</tt>.
== Performance Messages
By setting the preference <tt>PERFORMANCE_INFO</tt> to <tt>TRUE</tt> ProB will print various performance messages.
For example it may print messages when the evaluation of comprehension sets has exceeded a threshold. This threshold (in ms) can be influenced by setting the preference
<tt>PERFORMANCE_INFO_LIMIT</tt>.
== Debugging Constants Setup
By setting the preference <tt>TRACE_INFO</tt> to <tt>TRUE</tt> ProB will print additional messages when evaluating certain predicates, in particular the <tt>PROPERTIES</tt> clause of a B machine.
With this feature you can observe how constants get bound to values and can sometimes spot expensive predicates and large values.
Some additional information about debugging the PROPERTIES can be found in the [[Tutorial Troubleshooting the Setup]].
Let us take the following machine
....
MACHINE Debug
CONSTANTS a,b,c
PROPERTIES
a = card(b) &
b = %x.(x:1..c|x*x) &
c : 1000..1001 & c < 1001
VARIABLES x
INVARIANT x:NATURAL
INITIALISATION x:=2
OPERATIONS
Sqr = SELECT x:dom(b) THEN x := b(x) END;
Finished = SELECT x /: dom(b) THEN skip END
END
....
Here is how we can debug the constants setup:
....
$ probcli Debug.mch -p TRACE_INFO TRUE -init
% unused_constants(2,[a,c])
nr_of_components(1)
====> (1) c < 1001
====> (1) a = card(b)
====> (1) b = %x.(x : 1 .. c|x * x)
====> (1) c : 1000 .. 1001
finished_processing_component_predicates
grounding_wait_flags
:?: a int(?:0..sup)
:?: b VARIABLE: _31319 : GRVAL-CHECK
:?: c int(?:inf..1000)
--1-->> a
int(1000)
--1-->> b
AVL.size=1000
--1-->> c
int(1000)
% Runtime for SOLUTION for SETUP_CONSTANTS: 107 ms (walltime: 110 ms)
% Runtime to FINALISE SETUP_CONSTANTS: 0 ms (walltime: 0 ms)
=INIT=> x := 2
[=OK= 0 ms]
....
== Debugging Animation or Execution
By using the <tt>-animate_stats</tt> flag, you can see execution times for operations that are executed either using the <tt>-execute</tt> or <tt>-animate</tt> commands.
In verbose mode (<tt>-v</tt> flag) you also see the memory consumption.
....
$ probcli Debug.mch -execute_all -animate_stats
% unused_constants(2,[a,c])
% Runtime for SOLUTION for SETUP_CONSTANTS: 79 ms (walltime: 80 ms)
1 : SETUP_CONSTANTS
91 ms walltime (89 ms runtime), since start: 1107 ms
2 : INITIALISATION
5 ms walltime (4 ms runtime), since start: 1112 ms
3 : Sqr
10 ms walltime (10 ms runtime), since start: 1123 ms
4 : Sqr
0 ms walltime (0 ms runtime), since start: 1123 ms
5 : Sqr
1 ms walltime (0 ms runtime), since start: 1124 ms
6 : Sqr
0 ms walltime (0 ms runtime), since start: 1124 ms
7 : Finished
3 ms walltime (4 ms runtime), since start: 1127 ms
Infinite loop reached after 8 steps (looping on Finished).
% Runtime for -execute: 116 ms (with gc: 116 ms, walltime: 119 ms); time since start: 1132 ms
....
== Profiling ==
You can obtain some profiling information using the <tt>-prob_profile</tt> command.
This command unfortunately requires that ProB was compiled using special flags (<tt>-Dprob_profile=true</tt> and <tt>-Dprob_src_profile=true</tt>).
....
$ probcli ../prob_examples/public_examples/B/Tutorial/Debug.mch -execute_all -prob_profile
...
--------------------------
ProB profile info after 5685 ms walltime (5248 ms runtime)
----Source Location Profiler Information----
----Tracks number of times B statements (aka substitutions) are hit
1 hits at 9:15 -- 9:19 in /Users/leuschel/git_root/prob_examples/public_examples/B/Tutorial/Debug.mch
1 hits at 12:37 -- 12:41 in /Users/leuschel/git_root/prob_examples/public_examples/B/Tutorial/Debug.mch
4 hits at 11:29 -- 11:38 in /Users/leuschel/git_root/prob_examples/public_examples/B/Tutorial/Debug.mch
----
---- ProB Runtime Profiler ----
---- Tracks time spent in B operations and invariant evaluation
$setup_constants : 78 ms (80 ms walltime & 80 ms max. walltime; #calls 1)
Sqr : 9 ms (9 ms walltime & 9 ms max. walltime; #calls 1)
$initialise_machine : 5 ms (5 ms walltime & 5 ms max. walltime; #calls 1)
Finished : 3 ms (4 ms walltime & 4 ms max. walltime; #calls 1)
Total Walltime: 98 ms for #calls 4
....
src/docs/chapter/user/12_BLanguage/Tutorial_Modeling_Infinite_Datatypes.adoc deleted 100644 → 0
+ 0
− 73
View file @ b72bf27a
[[tutorial-modeling-infinite-datatypes]]
= Tutorial Modeling Infinite Datatypes
This tutorial describes how to model (and how not to model)
infinite datatypes so that they can be animated with ProB. (You may also
want to look at the manual page on
<<recursively-defined-functions,recursive functions>>.) We illustrate
this by modeling a Stack datatype.
Unfortunately, the following B machine does not work with ProB:
----
MACHINE StackAxioms1
SETS Stack
CONSTANTS pop, push,empty
PROPERTIES
empty:Stack &
pop : Stack \ {empty} --> Stack &
!s,x . (s : Stack & x : NAT => pop(push(s |-> x)) = s)
& push: Stack*NAT --> Stack \ {empty}
END
----
The problem with the above model is that the `PROPERTIES` can only be
satisfied if `Stack` is infinite. However, ProB does not presently
support infinite deferred sets. We need to do a more constructive
definition and use the infinite set ProB knows about: `INTEGER`. This is
done in the following machine, which is included in the
`examples/Tutorial` directory of the
https://www3.hhu.de/stups/prob/index.php/Download[ProB
distribution].
----
MACHINE StackConstructive
/* A machine that shows how to model a stack of type RANGE so that it can
be animated and validated with ProB */
/* We could have used the sequence operations instead;
our intention was also to show how you can model this in Event-B */
DEFINITIONS Stack == (INTEGER <-> RANGE)
SETS RANGE
CONSTANTS empty, push, pop, tops
PROPERTIES
empty : Stack & empty = {} &
push : (RANGE * Stack) <-> Stack &
push = %(x,s).(x:RANGE & s:Stack | s \/ {card(s)+1|->x}) &
pop: Stack <-> Stack &
pop = %s.(s:Stack| {card(s)} <<| s) &
tops: Stack <-> RANGE &
tops = %s.(s:Stack| s(card(s)))
ASSERTIONS
/* the assertions cannot be checked by ProB, they will trigger
the expansion of the infinite functions above */
tops: Stack \ {empty} --> RANGE;
push: (RANGE*Stack) --> Stack \ {empty};
pop: Stack \ {empty} --> Stack
VARIABLES cur
INVARIANT
cur: Stack
& cur : seq(RANGE) /* a slightly stronger invariant */
INITIALISATION cur := empty
OPERATIONS
Push(yy) = PRE yy:RANGE THEN cur:= push(yy,cur) END;
Pop = PRE cur /= empty THEN cur := pop(cur) END;
t <-- Top = PRE cur /= empty THEN t := tops(cur) END
END
----
As the screenshot illustrates, this model can now be animated with ProB.
Observe how the functions push, pop and tops are kept symbolic in the
State View.
image::StackConstructiveProB.png[]
src/docs/chapter/user/12_BLanguage/WD/00_section_header.adoc deleted 100644 → 0
+ 0
− 4
View file @ b72bf27a
[[well-definedness]]
= Well Definedness
:leveloffset: +1
src/docs/chapter/user/12_BLanguage/WD/01_Well-Definedness_Checking.adoc deleted 100644 → 0
+ 0
− 43
View file @ b72bf27a
[[well-definedness-checking]]
= Well-Definedness Checking
Well-definedness errors can occur in B in the following circumstances:
* a division by 0: `r=100/0`
* modulo by 0, modulo involving negative numbers: `r=100 mod -2`
* exponentiation using a negative exponent: `2**(-2)`
* application of a function outside of its domain: `f={1|->2} & r=f(3)`
* application of a relation which is not a function:
`f={1|->2,1|->3} & r=f(1)`
* application of the card operator to infinite sets: `card(NATURAL)`
* application of the min or max operator to empty sets:
`x={} & r=max(x)`
* application of the inter operator to empty sets: `x={} & r=inter(x)`
* wrong application of sequence operators
** taking the first, front, last, tail of an empty sequence:
`x=<> & r=first(x)`
** using negative indexes for prefix or suffix sequence: `x = s /|\ -1`
** using too large indexes for suffix sequence: `x= s \|/ (size(s)+1)`
* ...
To ensure that your models only contain well-defined formulas, Rodin
creates well-definedness proof obligations for Event-B and Atelier-B can
create them for classical B. ProB will check for well-definedness during
constraint solving, animation and model checking. However, by default
this check is not very extensive. You can force ProB to look more
aggressively for well-definedness issues in your formulas by setting the
following preference to true:
* `TRY_FIND_ABORT`
However, even with this, the search is not guaranteed to be exhaustive.
Also, ProB's constraint solving does not necessarily solve formulas from
left to right. Hence, the following formulas will be considered
well-defined (and on can argue that they are) by ProB:
* `r=1/x & x/=0`
Technically speaking, for disjunctions and implications ProB uses the
L-system of well-definedness (i.e., for P => Q, P should be well-defined
and if P is true then Q should also be well-defined).
src/docs/chapter/user/12_BLanguage/WD/ZZ_section_footer.adoc deleted 100644 → 0
+ 0
− 2
View file @ b72bf27a
:leveloffset: -1
src/docs/chapter/user/12_BLanguage/ZZ_section_footer.adoc deleted 100644 → 0
+ 0
− 2
View file @ b72bf27a
:leveloffset: -1
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment