Rearrange handbook files and merge developer handbook and user manual

src/docs/chapter/user/11_BLanguage/10_External_Functions.adoc

+
 [[external-functions]]
-== 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
@@ -15,7 +16,7 @@ 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
+== 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:
@@ -76,7 +77,7 @@ DEFINITIONS
 -------------
 
 [[overview-of-the-external-function-definition-mechanism]]
-=== 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:

src/docs/chapter/user/11_BLanguage/11_Recursively_Defined_Functions.adoc

+
 [[recursively-defined-functions]]
-== Recursively Defined Functions
+= Recursively Defined Functions
 
 [[symbolic-functions-and-relations]]
-=== Symbolic Functions and Relations
+== Symbolic Functions and Relations
 
 Take the following function:
 
@@ -113,7 +114,7 @@ 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 ?
+=== 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
@@ -137,7 +138,7 @@ database attributes and one should use the
 <<tutorial-symbolic-constants,symbolic constants plugin>>.
 
 [[recursive-function-definitions-in-prob]]
-=== 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:
@@ -171,7 +172,7 @@ SEND
 ---------
 
 [[operations-applicable-for-recursive-functions]]
-==== Operations applicable for recursive functions
+=== Operations applicable for recursive functions
 
 With such a recursive function you can:
 

src/docs/chapter/user/11_BLanguage/20_Tips:_B_Idioms.adoc

+
 [[tips-b-idioms]]
-== Tips: B Idioms
+= Tips: B Idioms
 
-Also have a look at
-/Tips:_Writing_Models_for_ProB[Tips:_Writing_Models_for_ProB].
+Also have a look at <<tips-writing-models-for-prob,Tips:_Writing_Models_for_ProB>>.
 
 [[let]]
-=== 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
+=== 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:
+==== Examples:
 
 ----
 >>> LET a BE a = 10 IN a + 10 END
@@ -50,7 +50,7 @@ Expression Value = 11
 ----
 
 [[let-for-predicates]]
-==== Let for predicates
+=== Let for predicates
 
 For predicates this encodes a let predicate:
 
@@ -81,7 +81,7 @@ both encode
 `{x|let y=E1 & z=E2 in P}`
 
 [[let-for-expressions]]
-==== 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:
@@ -97,19 +97,19 @@ The following construct has exactly the same effect:
 `INTER(x).(x=E|F)`
 
 [[if-then-else]]
-=== 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
+=== 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:
+==== Examples:
 
 ----
 >>> IF 1 = 1 THEN 3 ELSE 4 END
@@ -131,7 +131,7 @@ Predicate is FALSE
 Predicate is TRUE
 ----
 [[expressions]]
-==== Expressions
+=== Expressions
 
 The following construct
 
@@ -148,7 +148,7 @@ parentheses around the IF-THEN-ELSE; version 1.6.1 no longer requires
 them).
 
 [[finite]]
-=== 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
@@ -157,7 +157,7 @@ is recognised by ProB):
 `x : FIN(x)`
 
 [[all-different]]
-=== 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):
@@ -165,7 +165,7 @@ using the following construct (recognised by ProB):
 `card({x1,...,xn})=n`
 
 [[map]]
-=== 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 `;`:
@@ -175,7 +175,7 @@ all elements of `sqce` using the relational composition operator `;`:
 For example, `([1,2,3] ; succ)` gives us the sequence `[2,3,4]`.
 
 [[recursion-using-closure1]]
-=== 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
@@ -214,7 +214,7 @@ 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
+== Recursion using ABSTRACT:_CONSTANTS
 
 Recursive functions can be declared using the `ABSTRACT_CONSTANTS`
 section in B machines. Functions declared as `ABSTRACT_CONSTANTS` are

src/docs/chapter/user/11_BLanguage/21_Tips:_Writing_Models_for_ProB.adoc

-[[tips-writing-models-for-prob]]
-== Tips: Writing Models for ProB
 
+[[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
@@ -32,10 +32,10 @@ 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
+== Effective Constraint Solving with ProB
 
 [[existential-quantifiers]]
-==== Existential Quantifiers
+=== Existential Quantifiers
 
 Existential quantifiers can pose subtle problems when solving constraint
 problems.
@@ -73,7 +73,7 @@ avoid repeated computations
 elimination>>) and to make your predicates more readable.
 
 [[universal-quantifiers]]
-=== 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)`
@@ -100,7 +100,7 @@ of `1..10`, then we can rewrite `!x.(s(x)=5 => P(x))` into
 is checked.
 
 [[transitive-closure-in-event-b]]
-=== 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

src/docs/chapter/user/11_BLanguage/WD/00_section_header.adoc

+
+[[well-definedness]]
+= Well Definedness
+:leveloffset: +1

src/docs/chapter/user/11_BLanguage/WD/01_Well-Definedness_Checking.adoc

+
 [[well-definedness-checking]]
-== Well-Definedness Checking
+= Well-Definedness Checking
 
 Well-definedness errors can occur in B in the following circumstances:
 

src/docs/chapter/developer/10_java_api/ZZ_section_footer.adoc → src/docs/chapter/user/11_BLanguage/WD/ZZ_section_footer.adoc

+
 :leveloffset: -1

src/docs/chapter/developer/20_prolog/ZZ_section_footer.adoc → src/docs/chapter/user/11_BLanguage/ZZ_section_footer.adoc

+
 :leveloffset: -1

src/docs/chapter/user/20_Validation/00_section_header.adoc

+
+[[validation]]
+= Validation
+:leveloffset: +1

src/docs/chapter/user/20_Validation/CBC/00_section_header.adoc

+
+[[constraint-based-checking]]
+= Constraint Based Checking
+:leveloffset: +1
+
+ProB also offers an alternative checking method, inspired by the Alloy
+footnote:[D. Jackson: Alloy: A lightweight object modeling notation. ACM
+Transactions Software Engineering and Methodology (TOSEM),
+11(2):256–290, 2002.] analyser. In this mode of operation, ProB does not
+explore the reachable states starting from the initial state(s), but
+checks whether applying a single operation can result in a property
+violation (invariant and assertion) independently of the particular
+initialization of the B machine. This is done by symbolic constraint
+solving, and we call this approach constraint based checking (another
+sensible name would be model finding).
+
+More details and examples can be found in the
+<<tutorial-model-checking-proof-and-cbc,tutorial page on model
+checking, proof and CBC>>.

src/docs/chapter/user/20_Validation/CBC/01_Constraint_Based_Checking.adoc

-[[constraint-based-checking]]
-== Constraint Based Checking
-
-ProB also offers an alternative checking method, inspired by the Alloy
-footnote:[D. Jackson: Alloy: A lightweight object modeling notation. ACM
-Transactions Software Engineering and Methodology (TOSEM),
-11(2):256–290, 2002.] analyser. In this mode of operation, ProB does not
-explore the reachable states starting from the initial state(s), but
-checks whether applying a single operation can result in a property
-violation (invariant and assertion) independently of the particular
-initialization of the B machine. This is done by symbolic constraint
-solving, and we call this approach constraint based checking (another
-sensible name would be model finding).
-
-More details and examples can be found in the
-<<tutorial-model-checking-proof-and-cbc,tutorial page on model
-checking, proof and CBC>>.
 
 [[difference-between-constraint-based-checking-and-model-checking]]
-=== Difference between Constraint Based Checking and Model Checking
+= Difference between Constraint Based Checking and Model Checking
 
 <<consistency-checking,Model checking>> tries to find a sequence of
 operations that, starting from an initial state, leads to a state which
@@ -37,7 +20,7 @@ A comparison between all <<prob-validation-methods,ProB validation
 methods can be found on a separate manual section>>.
 
 [[commands-of-the-constraint-based-checker]]
-=== Commands of the Constraint Based Checker
+= Commands of the Constraint Based Checker
 
 These commands are only accessible in the "Normal" mode of ProB (see
 <<the-prob-main-window,the general
@@ -71,4 +54,4 @@ The following command is related to the above:
 
 * <<using-the-command-line-version-of-prob,cbc_sequence>> to find a sequence of operations using the constraint solver
 
-=== References
+= References

src/docs/chapter/user/20_Validation/CBC/10_Bounded_Model_Checking.adoc

+
 [[bounded-model-checking]]
-== Bounded Model Checking
+= Bounded Model Checking
 
 As of version 1.5, ProB provides support for constraint-based bounded
 model checking (BMC). As opposed to

src/docs/chapter/user/20_Validation/CBC/20_Symbolic_Model_Checking.adoc

+
 [[symbolic-model-checking]]
-== Symbolic Model Checking
+= Symbolic Model Checking
 
 [[overview-symbolic-model-checking]]
-=== Overview
+== Overview
 
 The current nightly builds of ProB support different symbolic model
 checking algorithms:
@@ -26,7 +27,7 @@ checking algorithm based on a different technique is available in Prob.
 See <<bounded-model-checking,its wiki page>> for details.
 
 [[usage]]
-=== Usage
+== Usage
 
 Take the following example:
 
@@ -85,7 +86,7 @@ The algorithms are also available from within ProB Tcl/Tk. They can be
 found inside the "Symbolic Model Checking" sub-menu of the _Analyse_ menu.
 
 [[more-details]]
-=== More details
+== More details
 
 A paper describing the symbolic model checking algorithms and how they
 are applied to B and Event-B machines has been submitted to ABZ 2016.

src/docs/chapter/user/20_Validation/CBC/ZZ_section_footer.adoc

+
+:leveloffset: -1

src/docs/chapter/user/20_Validation/MC/00_section_header.adoc

+
+[[model-checking]]
+= Model Checking
+:leveloffset: +1

src/docs/chapter/user/20_Validation/MC/01_Consistency_Checking.adoc

+
 [[consistency-checking]]
-== Model Checking Consistency
+= Model Checking Consistency
 
 [[checking-consistency-via-model-checking]]
-=== Checking Consistency via Model Checking
+== Checking Consistency via Model Checking
 
 By manually animating a B machine, it is possible to discover problems
 with the specification, such as invariant violations or deadlocks. The
@@ -19,7 +20,7 @@ spaces and will then explore the state space until it finds an error or
 runs out of memory.
 
 [[basics]]
-==== Basics
+=== Basics
 
 During the initial draft of a specification, it is often useful to
 utilize the model checker to determine if there are any invariant
@@ -53,7 +54,7 @@ model checker does find errors quite quickly. On that basis, it remains
 a useful tool even for specifications whose state space is infinite.
 
 [[using-the-model-checker]]
-==== Using the Model Checker
+=== Using the Model Checker
 
 To model check a B machine loaded in ProB, launch the command from
 "Verify| Model Check".
@@ -91,7 +92,7 @@ entire state space has been checked. The user can interrupt the model
 checking at any time by pressing the "Cancel" button.
 
 [[incremental-model-checking]]
-===== Incremental Model Checking
+==== Incremental Model Checking
 
 It is important to understand that the computation of and search in the
 state space is an incremental process. The model checking can be done by
@@ -120,7 +121,7 @@ the change of the model checking settings may not affect the state space
 already computed.
 
 [[results-of-the-model-checking]]
-===== Results of the Model Checking
+==== Results of the Model Checking
 
 When the state space has been computed by ProB, the pop-up window is
 replaced by a dialog window stating "No error state found". All new
@@ -137,7 +138,7 @@ property violation) in the "Enabled Operations" pane, and the trace
 pane.
 
 [[preferences-of-the-model-checking]]
-===== Preferences of the Model Checking
+==== Preferences of the Model Checking
 
 The preferences "Nr of Initialisations shown" and "Max Number of
 Enablings shown" (described in
@@ -165,7 +166,7 @@ Specification and Development in Z and B, LNCS 3455. Springer-Verlag,
 https://www3.hhu.de/stups/downloads/pdf/LeTu05_8.pdf].
 
 [[machines-with-invariant-violations-and-deadlocks]]
-==== Machines with Invariant Violations and Deadlocks
+=== Machines with Invariant Violations and Deadlocks
 
 When the two properties (invariant and deadlock-freeness) are checked
 and a state violates both, only the invariant violation is reported. In
@@ -186,7 +187,7 @@ simply compute the entire state space until the user presses the Cancel
 button or until the specified number of nodes is reached.*
 
 [[two-phase-verification]]
-===== Two Phase Verification
+==== Two Phase Verification
 
 If the state space of the specification can be exhaustively searched,
 check for deadlocks and invariant violations in two phases. To do this,
@@ -204,7 +205,7 @@ HINT: At any time during animation and model checking, the user can
 reopen the the B specification to purge the state space.
 
 [[interleaved-deadlock-and-invariant-violation-checking]]
-===== Interleaved deadlock and invariant violation checking
+==== Interleaved deadlock and invariant violation checking
 
 If you wish to determine if an already encountered invariant violation
 is also a deadlocked node, turn the option "Inspect Existing Nodes"
@@ -217,7 +218,7 @@ WARNING: Enabling "Inspect Existing Nodes" will continually report
 the first error it encounters until that error is corrected.
 
 [[specifying-goals-and-assertions]]
-=== Specifying Goals and Assertions
+== Specifying Goals and Assertions
 
 The ASSERTIONS clause of a B machine enables the user to define
 predicates that are supposed to be deducible from the INVARIANT or
@@ -242,4 +243,4 @@ a goal without defining it explicitly in the B specification. The
 directly in a text field. ProB then searches for a state of the state
 space currently computed that satisfies this goal.
 
-=== References
+== References

src/docs/chapter/user/20_Validation/MC/10_Distributed_Model_Checking.adoc

+
 [[distributed-model-checking]]
-== Distributed Model Checking
+= Distributed Model Checking
 
 Distributed Model Checking allows to check invariants and
 deadlock-freedom (and assertions) with additional computational power.
 The distributed version of ProB is named _distb_. In the following, we
 will document how to run it.
 
-=== Overview
+== Overview
 
 _distb_ consists of three components.
 
@@ -19,7 +20,7 @@ is close to the amount of available (physical) CPU cores of a
 participating machine.
 
 [[setting-up-shared-memory]]
-=== Setting up shared memory
+== Setting up shared memory
 
 It might be necessary to increase the limits of how much shared memory
 may be allocated, both per segment and overall. This is, to our
@@ -45,7 +46,7 @@ sudo sysctl -w kern.sysv.shmseg=4096
 sudo sysctl -w kern.sysv.shmall=18446744073692774399
 ----
 
-=== Running _distb_
+== Running _distb_
 
 Run once per machine:
 
@@ -64,7 +65,7 @@ Run as many workers as you want:
 
 `/path/to/prob/probcli -zmq_worker <unique identifier> &`
 
-=== Additional Preferences
+== Additional Preferences
 
 You can fine-tune the following parameters by adding `-p NAME VALUE` to
 the corresponding call (e.g.: `./probcli -zmq_worker worker1 -p port 5010

src/docs/chapter/user/20_Validation/MC/11_DMC.adoc

-== Distributed Model Checking : Experimental evaluation
+
+[[distributed-model-checking-experimental-evaluation]]
+= Distributed Model Checking : Experimental evaluation
 
 We used three different setups to evaluate the distributed version of ProB.
 
@@ -6,14 +8,14 @@ We used three different setups to evaluate the distributed version of ProB.
 * Amazon EC2 Instances
 * The HILBERT cluster
 
-=== Multicore Computer
+== Multicore Computer
 
 We used a hexacore 3.33GHz Mac Pro with 16GB of RAM. On this computer we
 benchmarked all models regardless whether we expected them to be
 scalable or not. We varied the number of used cores from 1 up to 12
 hyperthreads. Each experiment was repeated at least 5 times.
 
-=== Amazon EC2 Instances
+== Amazon EC2 Instances
 
 We used c3.8xlarge instances, each of which has 32 virtual CPUs and is
 equipped with 64 GB of RAM. We used the Mac Pro to get an impression if
@@ -24,7 +26,7 @@ the Mac Pro were not considered as they would not scale on more
 processors. We used 2 or 4 instances connected with 10 GBit ethernet
 connection. Each experiment was repeated at least 5 times.
 
-=== HILBERT
+== HILBERT
 
 We used the high performance cluster at the university of Düsseldorf
 (HILBERT) for a single model. The model could not be cheked using a
@@ -36,13 +38,13 @@ executed the experiments once but all experiments on the other platforms
 indicated that the variation between experiments could be ignored. Also
 the execution times of all 6 experiments seem to be consistent.
 
-=== Models
+== Models
 
 We cannot make all models public, because they we provided by industrial
 partners from various research projects. The models that could be make
 available can be downloaded https://www3.hhu.de/stups/models/parb/[here].
 
-=== Results
+== Results
 
 The results of the experiments are shown in Jens Bendisposto's
 dissertation. The dissertation is available https://docserv.uni-duesseldorf.de/servlets/DocumentServlet?id=34472[here].

src/docs/chapter/user/20_Validation/MC/12_ParB.adoc

+
 [[parb]]
-== ParB
+= ParB
 
 This page explains how to run the distributed model checking prototype.
 
@@ -37,7 +38,7 @@ Example usage:
 `$ ./parB.sh 2 ~/parB.log scheduler.mch`
 
 [[running-in-the-cloudcluster]]
-=== Running in the Cloud/Cluster
+== Running in the Cloud/Cluster
 
 The script can only be used for computation on a single physical
 computer. If you want to use multiple computers, the setup is a bit more
@@ -71,7 +72,7 @@ logical network in a more convenient way and running the model checker
 from within ProB.
 
 [[options-for-parb]]
-=== Options
+== Options
 
 You can use preferences in parB.sh (and the master) :
 
@@ -85,7 +86,7 @@ otherwise parB will explore the full state space (up to the maximal
 number of states)
 
 [[cleaning-up]]
-=== Cleaning up
+== Cleaning up
 
 If something goes wrong it may be necessary to clean up your shared
 memory. You can find out if there are still memory blocks occupied using

src/docs/chapter/user/20_Validation/MC/20_LTL_Model_Checking.adoc

+
 [[ltl-model-checking]]
-== LTL Model Checking
+= LTL Model Checking
 
 ProB provides
 support for LTL (linear temporal logic) model checking. For an
@@ -65,7 +66,7 @@ The old LTL and CTL dialogs can be accessed from "OldLtlViewers" in
 the menu bar.
 
 [[ltl-preferences]]
-=== LTL Preferences
+== LTL Preferences
 
 There is a set of options coming with the LTL model checker. In this
 section we give a brief overview of the preferences. The LTL preferences
@@ -126,7 +127,7 @@ Note: Whereas `Y true` is always false when checked with option 1 or 2,
 it is usually true (but not in all cases) for option 3.
 
 [[supported-syntax]]
-==== Supported Syntax
+=== Supported Syntax
 
 ProB supports LTL^[e]^, an extended version of LTL. In contrast to the
 standard LTL, LTL^[e]^ provides also support for propositions on
@@ -195,7 +196,7 @@ the operations starts.
 ** `SEF`: strong fairness for all possible operations
 
 [[setting-fairness-constraints]]
-=== Setting Fairness Constraints
+== Setting Fairness Constraints
 
 Fairness is a notion where the search for counterexamples is restricted
 to paths that do not ignore infinitely the execution of a set of enabled
@@ -274,7 +275,7 @@ sfair ::= sf(a) | ( sfair ) | sfair & sfair | sfair or sfair
 where "a" is a transition proposition.
 
 [[storing-ltl-assertions-in-the-model]]
-=== Storing LTL Assertions in the Model
+== Storing LTL Assertions in the Model
 
 *Storing LTL formulas in B machines* +
 LTL formulas can be stored in the DEFINITIONS section of a B machine.
@@ -320,7 +321,7 @@ where `P` is an arbitrary process and `ltl-formula` an LTL formula.
 
 
 [[ltl-formulas-in-a-separate-file]]
-=== LTL Formulas in a Separate File
+== LTL Formulas in a Separate File
 
 With the command line version of ProB it is possible to check several
 LTL^[e]^ formulae with one call. The command has the following syntax:
@@ -343,7 +344,7 @@ One also can check a single LTL^[e]^ formula _F_ using the option
 `probcli -ltlformula "F"...`
 
 [[ltl-formulae-in-a-separate-file]]
-=== LTL Formulae in a Separate File
+== LTL Formulae in a Separate File
 
 With the command line version of ProB it is possible to check several
 LTL^[e]^ formulae with one call. The command has the following syntax:
@@ -366,7 +367,7 @@ One also can check a single LTL^[e]^ formula _F_ using the option
 `probcli -ltlformula "F"...`
 
 [[ltl-model-checker-output]]
-=== LTL Model Checker Output
+== LTL Model Checker Output
 
 The output provided by the LTL model checker can sometimes reveal some
 interesting statistical facts about the model and the property being
@@ -511,7 +512,7 @@ a counter-example for "GF [eat.0]" in case no fairness constraints
 were imposed.
 
 [[other-relevant-tutorials-about-ltl-model-checking]]
-=== Other Relevant Tutorials about LTL Model Checking
+== Other Relevant Tutorials about LTL Model Checking
 
 A brief tutorial on visualizing LTL counter-examples in the Rodin tool
 can be found <<tutorial-ltl-counter-example-view,here>>.
@@ -520,4 +521,4 @@ A tutorial of a simple case study, where setting fairness constraints to
 some of the LTL properties is required, can be found
 <<mutual-exclusion-fairness,here>>.
 
-=== References
+== References