diff --git a/build.gradle b/build.gradle index 0a6f6881fc924c02273ad681fff36a34d1818930..0003d347f4b6d3027b77221d2ec487dbe0df1ab3 100644 --- a/build.gradle +++ b/build.gradle @@ -85,7 +85,7 @@ asciidoctor { options doctype: 'book' - backends = ['html5', 'pdf'] + backends = ['html5'] attributes = [ 'source-highlighter': 'coderay', diff --git a/config.yaml b/config.yaml index 533850dbd7d160c63dca3b27ca06a262a488dba4..d0acdd8cb3571250e4f85d04a6c32545bde29840 100644 --- a/config.yaml +++ b/config.yaml @@ -1,19 +1,10 @@ --- -file: prob_developer.adoc -title: ProB Developer Handbook +file: prob_handbook.adoc +title: ProB Handbook authors: - Jens Bendisposto - Joy Clark - Michael Leuschel -content: - - developer - - appendix ---- -file: prob_user_manual.adoc -title: ProB User Manual -authors: - - Jens Bendisposto - - Michael Leuschel content: - user - model_examples diff --git a/src/docs/chapter/user/01_The_ProB_Animator_and_Model_Checker.adoc b/src/docs/chapter/user/01_The_ProB_Animator_and_Model_Checker.adoc index 60a7985e509f7000cbfd543a666d35240b09f0b9..3cc978b6e9f6fd4deed6b4ad7a4810df6ac27960 100644 --- a/src/docs/chapter/user/01_The_ProB_Animator_and_Model_Checker.adoc +++ b/src/docs/chapter/user/01_The_ProB_Animator_and_Model_Checker.adoc @@ -1,4 +1,6 @@ + [[the-prob-animator-and-modelchecker]] += The ProB Animator and Modelchecker [width="100%",cols="60%,40%",] |======================================================================= diff --git a/src/docs/chapter/user/10_General/00_General.adoc b/src/docs/chapter/user/10_General/00_section_header.adoc similarity index 55% rename from src/docs/chapter/user/10_General/00_General.adoc rename to src/docs/chapter/user/10_General/00_section_header.adoc index 2778c83963319e29bf1daea1fe7711733787efa9..de736a0c9b12dc464bd0dea2640b3f5b1d212729 100644 --- a/src/docs/chapter/user/10_General/00_General.adoc +++ b/src/docs/chapter/user/10_General/00_section_header.adoc @@ -1,2 +1,4 @@ + [[general]] = General +:leveloffset: +1 diff --git a/src/docs/chapter/user/10_General/01_Installation.adoc b/src/docs/chapter/user/10_General/01_Installation.adoc index ee5c34e3e0db4dae3474b943bf9ab2dea706626b..c050d8ce70a63cf53d2f400531e6d814e460c314 100644 --- a/src/docs/chapter/user/10_General/01_Installation.adoc +++ b/src/docs/chapter/user/10_General/01_Installation.adoc @@ -1,8 +1,9 @@ + [[installation]] -== Installation += Installation [[what-are-the-available-versions]] -=== What are the available versions? +== What are the available versions? * The standalone Tcl/Tk Version of ProB (ProB Tcl/Tk) * The standalone command-line version of ProB @@ -31,7 +32,7 @@ We are also developing a new Java-based API called command-line version and <<using-the-command-line-version-of-prob, here>> is how to use it. [[which-version-should-i-use]] -=== Which version should I use? +== Which version should I use? The standalone version Tcl/Tk of ProB contains a richer set of features than the Rodin version and also works on other formalisms than Event-B @@ -43,7 +44,7 @@ ProB. Use the probcli version if you want to write batch scripts or prefer working from the command-line. [[installation-instruction-for-prob-standalone]] -=== Installation Instruction for ProB (Standalone) +== Installation Instruction for ProB (Standalone) NOTE: We have specific <<windows-installation-instructions, Windows installation instructions>>. These here are the generic instructions. @@ -92,7 +93,7 @@ animate them. Have a look at the supplied Machines in the examples directory. Have fun! Please report bugs! [[checklisttroubleshooting]] -==== Checklist/Troubleshooting +=== Checklist/Troubleshooting * Java: be sure to have Java 7 or newer installed. Otherwise you will not be able to parse your own classical B machines as our parser is @@ -115,6 +116,6 @@ dot viewer. See more information about the <<graphical-viewer,Graphical Viewer here>>. [[installation-instruction-for-prob-rodin-plugin]] -=== Installation Instruction for ProB (Rodin Plugin) +== Installation Instruction for ProB (Rodin Plugin) <<tutorial-rodin-first-step,This>> tutorial shows how to properly install ProB for Rodin. diff --git a/src/docs/chapter/user/10_General/02_Windows_Installation_Instructions.adoc b/src/docs/chapter/user/10_General/02_Windows_Installation_Instructions.adoc index 8c9d7b8a0b0bc4f0d5c374116022574e54b34e1e..bd38149f2ecc0e18c9cb7544272b8447af90c119 100644 --- a/src/docs/chapter/user/10_General/02_Windows_Installation_Instructions.adoc +++ b/src/docs/chapter/user/10_General/02_Windows_Installation_Instructions.adoc @@ -1,8 +1,9 @@ + [[windows-specific-download-instructions]] -== Windows Specific Download Instructions += Windows Specific Download Instructions [[go-to-the-prob-downloads-site]] -=== Go to the ProB Downloads site +== Go to the ProB Downloads site * Go to the page https://www3.hhu.de/stups/prob/index.php/Download[Download], @@ -11,7 +12,7 @@ this should look as follows: image::ProBWindowsDownload.png[] [[install-tcltk-8.5]] -=== Install Tcl/Tk 8.5 +== Install Tcl/Tk 8.5 If Tcl/Tk 8.5 is already installed you can skip this step. @@ -27,7 +28,7 @@ ProB. image::TkWindowsDownload.png[] [[install-java]] -=== Install Java +== Install Java If Java 7 or newer is already installed you can skip this step. @@ -36,7 +37,7 @@ newer)] link provided in the `Dependencies` column and the `Windows` row above * Follow the installation instructions [[download-the-prob-for-windows-zipfile]] -=== Download the ProB for Windows Zipfile +== Download the ProB for Windows Zipfile * Click on the https://www3.hhu.de/stups/downloads/[Zipfile (with probcli)] link in the `Downloads` column and `Windows` row @@ -51,20 +52,20 @@ The subfolder called `Microsoft.VC80.CRT` contains the DLLs for the Microsoft C runtime. [[optionally-download-graphviz]] -=== Optionally Download GraphViz +== Optionally Download GraphViz * Install the `dot` program and `dotty viewer` from http://www.graphviz.org/ or http://www.research.att.com/sw/tools/graphviz/[AT&T's Graphviz package] [[start-prob]] -=== Start ProB +== Start ProB * Start ProB by double-clicking on the ProBWin icon above * Try to open some of the examples provided in the Examples folder shown above * Contact us if you have problems [[checklist-troubleshooting]] -=== Checklist/Troubleshooting +== Checklist/Troubleshooting * Java: be sure to have Java 1.7 or newer installed. Otherwise you will not be able to parse your own classical B machines as our parser is diff --git a/src/docs/chapter/user/10_General/10_Animation.adoc b/src/docs/chapter/user/10_General/10_Animation.adoc index e89d8f0cece4632a7f611cba7bddf436691a627c..7e58319f7206c627fad6492e58dfb47ebb333419 100644 --- a/src/docs/chapter/user/10_General/10_Animation.adoc +++ b/src/docs/chapter/user/10_General/10_Animation.adoc @@ -1,5 +1,6 @@ + [[animation]] -== Animation += Animation The animation facilities of ProB allow users to gain confidence in their specifications. These features try to be as user-friendly as possible @@ -8,7 +9,7 @@ operation arguments or choice variables, and he uses the mouse to operate the animation). [[basic-animation]] -=== Basic Animation +== Basic Animation When the B specification is opened, the syntax and type checker analyses it and, if a syntax or type error is detected, it is then reported, @@ -21,7 +22,7 @@ performed in the Enabled Operations pane. These operations can be of two types described below. [[operations-from-the-b-machine]] -==== Operations from the B Machine +=== Operations from the B Machine These operations are the ones whose preconditions and guards are satisfiable in the current state. The parameter values that make true @@ -41,7 +42,7 @@ preconditions and guards. corresponds to a deadlock* [[virtual-operations]] -==== Virtual Operations +=== Virtual Operations There are three particular operations that correspond to specific tasks performed by ProB: @@ -64,7 +65,7 @@ pane. These enable the user to explore interactively the behaviour of the B machine. [[animating-the-b-machine]] -==== Animating the B machine +=== Animating the B machine If the B machine has constants, one or several initialise constants operations are displayed. The user selects one of these operations, then @@ -94,7 +95,7 @@ added to the History pane, the effect of the operation are computed and the state is updated in the State Properties pane. [[the-analyse-menu]] -=== The Analyse menu +== The Analyse menu At each point during the animation process, several useful commands displaying various information on the B machine are available in the @@ -122,7 +123,7 @@ properties and the Analyse Assertions plays this role for the assertions. [[animation-preferences]] -=== Animation Preferences +== Animation Preferences The animation process in ProB can be configured via several preferences set in the preference window Preferences|Animation Preferences. @@ -142,7 +143,7 @@ The preference Check invariant will toggle the display of the invariant status indicator in the State Properties pane. [[other-animation-features]] -=== Other Animation Features +== Other Animation Features Several other commands are provided by ProB in the _Animate_ menu for animating B specifications. The Reset command will set the state of the diff --git a/src/docs/chapter/developer/Building_ProB_on_Windows.adoc b/src/docs/chapter/user/10_General/Building_ProB_on_Windows.adoc similarity index 100% rename from src/docs/chapter/developer/Building_ProB_on_Windows.adoc rename to src/docs/chapter/user/10_General/Building_ProB_on_Windows.adoc index 20e968634aea5b3c2a1265a710e05f07d6053e2d..e263a076a1667a9e84f10094b1b4c0d593da7127 100644 --- a/src/docs/chapter/developer/Building_ProB_on_Windows.adoc +++ b/src/docs/chapter/user/10_General/Building_ProB_on_Windows.adoc @@ -1,7 +1,7 @@ + [[building-prob-on-windows]] = Building ProB on Windows - In case that you want to compile ProB from Source on Windows (XP), here are some information about the setup: diff --git a/src/docs/chapter/user/10_General/Colours_of_enabled_operations.adoc b/src/docs/chapter/user/10_General/Colours_of_enabled_operations.adoc index a1340c49ed27daf7ec83dd3cbc9abef15a51372d..aa892ebc05dd1929e571b82c6655a7c27d5ca1c6 100644 --- a/src/docs/chapter/user/10_General/Colours_of_enabled_operations.adoc +++ b/src/docs/chapter/user/10_General/Colours_of_enabled_operations.adoc @@ -1,5 +1,6 @@ + [[colours-of-enabled-operations]] -== Colours of enabled operations += Colours of enabled operations The enabled operations are shown in different colours, depending on the state where the operation leads to. If more than one rule of the diff --git a/src/docs/chapter/user/10_General/Controlling_ProB_Preferences.adoc b/src/docs/chapter/user/10_General/Controlling_ProB_Preferences.adoc index 95afae4379acbfb4684d6348a612dfaa5a63c1ab..7e3c80ae08e8f2d4122808b12afa239fc31670d1 100644 --- a/src/docs/chapter/user/10_General/Controlling_ProB_Preferences.adoc +++ b/src/docs/chapter/user/10_General/Controlling_ProB_Preferences.adoc @@ -1,5 +1,6 @@ + [[controlling-prob-preferences]] -== Controlling ProB Preferences += Controlling ProB Preferences ProB provides a variety of preferences to control its behaviour. A list of the most important preferences can be found @@ -8,7 +9,7 @@ page for probcli>>. We also have a separate <<deferred-sets,manual page about setting the sizes of deferred sets>>. [[setting-preferences-in-a-b-machine]] -=== Setting Preferences in a B machine +== Setting Preferences in a B machine This only works for classical B models. For a preference `P` you can add the following definition to the `DEFINITIONS` section of the main @@ -19,7 +20,7 @@ machine: This will set the preference `P` to the value `VAL` for this model only. [[setting-preferences-from-the-command-line]] -=== Setting Preferences from the command-line +== Setting Preferences from the command-line You can set a preference `P` to a value `VAL` for a particular run of probcli by adding the command-line switch `-p P VAL`, e.g., @@ -44,7 +45,7 @@ set>> `GS` using the following command-line switch: `-card GS Val` [[setting-preferences-from-prob-tcltk]] -=== Setting Preferences from ProB Tcl/Tk +== Setting Preferences from ProB Tcl/Tk ProB Tcl/Tk stores your preferences settings in a file `ProB_Preferences.pl`. diff --git a/src/docs/chapter/user/10_General/Current_Limitations.adoc b/src/docs/chapter/user/10_General/Current_Limitations.adoc index 3e1796e0d2b854a0f6842e27d48fdab5a2d5f79d..18d7d3273cea77c9c41dcaf7f6eccdc12aa0653e 100644 --- a/src/docs/chapter/user/10_General/Current_Limitations.adoc +++ b/src/docs/chapter/user/10_General/Current_Limitations.adoc @@ -1,5 +1,6 @@ + [[current-limitations]] -== 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 @@ -38,7 +39,7 @@ 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 +== 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 diff --git a/src/docs/chapter/user/10_General/Deferred_Sets.adoc b/src/docs/chapter/user/10_General/Deferred_Sets.adoc index 94e27517c369d3adcd41cc971231ab1f47c26b12..cff2e164f59ecc9e01b700e3ac7942bfe663dace 100644 --- a/src/docs/chapter/user/10_General/Deferred_Sets.adoc +++ b/src/docs/chapter/user/10_General/Deferred_Sets.adoc @@ -1,5 +1,6 @@ + [[deferred-sets]] -== 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 @@ -35,7 +36,7 @@ influence the size used for AA by ProB, for example: set the cardinality of AA to the constant. [[using-refinement-for-animation-preferences]] -=== 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 @@ -52,7 +53,7 @@ END .... [[setting-deferred-set-cardinalities-within-probcli]] -=== 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: diff --git a/src/docs/chapter/user/10_General/Editors_for_ProB.adoc b/src/docs/chapter/user/10_General/Editors_for_ProB.adoc index 735aaac7f65e6ce912370809bb6fc42b98148f39..532490ca1612f4d896bafb40a207c17e34285c94 100644 --- a/src/docs/chapter/user/10_General/Editors_for_ProB.adoc +++ b/src/docs/chapter/user/10_General/Editors_for_ProB.adoc @@ -1,8 +1,9 @@ + [[editors-for-prob]] -== Editors for ProB += Editors for ProB [[prob-tcltk-editor]] -=== ProB Tcl/Tk Editor +== ProB Tcl/Tk Editor ProB Tcl/Tk contains an editor in which syntax errors are displayed and which can be used to edit B, CSP, Z and TLA+ models. The editor of @@ -23,7 +24,7 @@ file with this editor. You can also use the command-key shortcut "Cmd-E" for this. [[launching-the-editor-in-probcli]] -=== Launching the editor in probcli +== Launching the editor in probcli The <<using-the-command-line-version-of-prob,probcli>> REPL (read-eval-print-loop) supports the command `:e` to open the current @@ -36,10 +37,10 @@ In case errors occurred with the last command, this will also try and move the cursor to the corresponding location in the file. [[external-editors]] -=== External Editors +== External Editors [[vim]] -==== VIM +=== VIM A https://github.com/bivab/prob.vim[VIM plugin for ProB is available]. It shows a quick fix list of parse and type errors for classical B @@ -49,7 +50,7 @@ VIM has builtin syntax highlighting support for https://github.com/vim/vim/blob/master/runtime/syntax/b.vim[B]. [[atom]] -==== Atom +=== Atom There is a package https://atom.io/packages/language-b-eventb[language-b-eventb] available @@ -58,12 +59,12 @@ specification languages B and Event-B to Atom. It integrates with probcli to obtain error markers for syntax and type errors. [[bbedit]] -==== BBEdit +=== BBEdit Some https://github.com/leuschel/bbedit-prob[BBedit Language modules for B, TLA+, CSP and Prolog] are available. [[emacs]] -==== Emacs +=== Emacs A package is available. //TODO: Downloadlink b-mode.el.zip[] diff --git a/src/docs/chapter/user/10_General/GeneralPresentation.adoc b/src/docs/chapter/user/10_General/GeneralPresentation.adoc index 0a4bfd345df5e8a71c15b2d1acd94d5c1d2fab91..3532ae58a43a05ee13dcf02952625025db4b9ae4 100644 --- a/src/docs/chapter/user/10_General/GeneralPresentation.adoc +++ b/src/docs/chapter/user/10_General/GeneralPresentation.adoc @@ -1,8 +1,9 @@ + [[general-presentation]] -== General Presentation += General Presentation [[the-prob-main-window]] -=== The ProB Main Window +== The ProB Main Window The menu bar contains the various commands to access the features of ProB. It includes the traditional _File_ menu with a sub-menu "Recent @@ -37,7 +38,7 @@ mean); 3. The history of operations leading to this state (History). [[general-presentation-preferences]] -=== Preferences +== Preferences The _Preferences_ menu allows the various features of ProB to be configured. When ProB is started for the first time, it creates a file diff --git a/src/docs/chapter/developer/Getting_Involved.adoc b/src/docs/chapter/user/10_General/Getting_Involved.adoc similarity index 100% rename from src/docs/chapter/developer/Getting_Involved.adoc rename to src/docs/chapter/user/10_General/Getting_Involved.adoc index cc0f620becdb0de76ab4fc8047821620585a8b7a..74d943b18bc45a36d831a7a3150ab55b464bf28b 100644 --- a/src/docs/chapter/developer/Getting_Involved.adoc +++ b/src/docs/chapter/user/10_General/Getting_Involved.adoc @@ -1,7 +1,7 @@ + [[getting-involved]] = Getting Involved - [[the-prob-java-core-and-ui]] == The ProB Java Core and UI diff --git a/src/docs/chapter/user/10_General/ProB_Logic_Calculator_old.adoc b/src/docs/chapter/user/10_General/ProB_Logic_Calculator_old.adoc index 76a8ec6ff246a56b07995a3e728d06a29d3bb60e..bea5ff3fd954e3676238cfb5b0aff3feb0f0e231 100644 --- a/src/docs/chapter/user/10_General/ProB_Logic_Calculator_old.adoc +++ b/src/docs/chapter/user/10_General/ProB_Logic_Calculator_old.adoc @@ -1,5 +1,8 @@ + [[prob-logic-calculator]] -== ProB Logic Calculator += ProB Logic Calculator + +WARNING: This section is relatively old and may contain errors. Below is a ProB-based http://research.microsoft.com/en-us/um/people/lamport/tla/logic-calculators.html[logic calculator]. You can enter predicates and expressions in the upper @@ -28,7 +31,7 @@ versions available for Linux and Mac (the above calculator only uses the 32-bit version). [[short-syntax-guide-for-b-constructs]] -=== Short syntax guide for some of B's constructs: +== Short syntax guide for some of B's constructs: * comments `/* ... */` * conjunction `P & Q`, disjunction `P or Q`, implication `P \=> Q`, @@ -91,7 +94,7 @@ https://www3.hhu.de/stups/downloads/pdf/PlaggeLeuschel_Kodkod2012.pdf[ProB-Kodko backend] instead of the default constraint-logic programming kernel. [[small-tutorial]] -=== Small Tutorial +== Small Tutorial Here is a small tutorial to get you started. B distinguishes expressions, which have a value, and predicates which can be either true @@ -209,7 +212,7 @@ will refine ProB's output to also indicate when the solution/counter-example is still guaranteed to be correct)! [[executing-the-calculator-locally]] -=== Executing the Calculator locally +== Executing the Calculator locally You can evaluate formulas on your machine in the same way as the calculator above, by <<downloads,downloading ProB>> (ideally a nightly diff --git a/src/docs/chapter/developer/30_tcltk/ZZ_section_footer.adoc b/src/docs/chapter/user/10_General/ZZ_section_footer.adoc similarity index 94% rename from src/docs/chapter/developer/30_tcltk/ZZ_section_footer.adoc rename to src/docs/chapter/user/10_General/ZZ_section_footer.adoc index 3b4360cb20797206e14fc3aa9803c4ff93a4b60d..909c09e0cbf5ccf1b361d16ff5dcdd73c14f6a69 100644 --- a/src/docs/chapter/developer/30_tcltk/ZZ_section_footer.adoc +++ b/src/docs/chapter/user/10_General/ZZ_section_footer.adoc @@ -1 +1,2 @@ + :leveloffset: -1 diff --git a/src/docs/chapter/user/11_BLanguage/00_BLanguage.adoc b/src/docs/chapter/user/11_BLanguage/00_section_header.adoc similarity index 60% rename from src/docs/chapter/user/11_BLanguage/00_BLanguage.adoc rename to src/docs/chapter/user/11_BLanguage/00_section_header.adoc index ba531e163d54a4ce11a58ee9ac4aad2ef29a733a..39d27f577895ad6096f02e355fc5bcf75505c140 100644 --- a/src/docs/chapter/user/11_BLanguage/00_BLanguage.adoc +++ b/src/docs/chapter/user/11_BLanguage/00_section_header.adoc @@ -1,2 +1,4 @@ + [[b-language]] = B Language +:leveloffset: +1 diff --git a/src/docs/chapter/user/11_BLanguage/01_Summary_of_B_Syntax.adoc b/src/docs/chapter/user/11_BLanguage/01_Summary_of_B_Syntax.adoc index 7b8bde09109b023eaab91451044de057bc9bdfe3..a81c1190a23de6ce9e42f7f11c9238d499c17c0f 100644 --- a/src/docs/chapter/user/11_BLanguage/01_Summary_of_B_Syntax.adoc +++ b/src/docs/chapter/user/11_BLanguage/01_Summary_of_B_Syntax.adoc @@ -1,8 +1,9 @@ + [[summary-of-b-syntax]] -== Summary of B Syntax += Summary of B Syntax [[logical-predicates]] -=== Logical predicates: +== Logical predicates: .... P & Q conjunction @@ -20,7 +21,7 @@ Note: you can also introduce multiple variables inside a universal or existential quantification, e.g., `!(x,y).(P => Q)`. [[equality]] -=== Equality: +== Equality: .... E = F equality @@ -28,7 +29,7 @@ existential quantification, e.g., `!(x,y).(P => Q)`. .... [[booleans]] -=== Booleans: +== Booleans: .... TRUE @@ -44,7 +45,7 @@ values `x` and `y` using conjunction you have to write value you have to use `bool(z>0)`. [[sets]] -=== Sets: +== Sets: .... {} empty set @@ -73,7 +74,7 @@ value you have to use `bool(z>0)`. .... [[numbers]] -=== Numbers: +== Numbers: .... INTEGER set of integers @@ -104,7 +105,7 @@ value you have to use `bool(z>0)`. .... [[relations]] -=== Relations: +== Relations: .... S<->T relation @@ -134,7 +135,7 @@ value you have to use `bool(z>0)`. .... [[functions]] -=== Functions: +== Functions: .... S+->T partial function @@ -151,7 +152,7 @@ value you have to use `bool(z>0)`. .... [[sequences]] -=== Sequences: +== Sequences: .... <> or [] empty sequence @@ -178,7 +179,7 @@ value you have to use `bool(z>0)`. .... [[records]] -=== Records: +== Records: .... struct(ID:S,...,ID:S) set of records with given fields and field types @@ -187,7 +188,7 @@ value you have to use `bool(z>0)`. .... [[strings]] -=== Strings: +== Strings: .... "astring" a specific (single-line) string value @@ -219,7 +220,7 @@ tabs and newlines. ProB assumes that all B machines and strings use the UTF-8 encoding. [[trees]] -=== 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 @@ -248,7 +249,7 @@ domain S. .... [[let-and-if-then-else]] -=== LET and IF-THEN-ELSE +== LET and IF-THEN-ELSE ProB allows the following for predicates and expressions: @@ -260,7 +261,7 @@ ProB allows the following for predicates and expressions: Note: The expressions E1,... defining x1,... are not allowed to use x1,... [[statements-aka-substitutions]] -=== Statements (aka Substitutions): +== Statements (aka Substitutions): .... skip no operation @@ -294,7 +295,7 @@ Note: The expressions E1,... defining x1,... are not allowed to use x1,... .... [[machine-header]] -=== Machine header: +== Machine header: .... MACHINE or REFINEMENT or IMPLEMENTATION @@ -307,7 +308,7 @@ Note: The expressions E1,... defining x1,... are not allowed to use x1,... .... [[machine-sections]] -=== Machine sections: +== Machine sections: ---- CONSTRAINTS P (logical predicate) @@ -325,7 +326,7 @@ Note: The expressions E1,... defining x1,... are not allowed to use x1,... ---- [[machine-inclusion]] -=== Machine inclusion: +== Machine inclusion: .... USES list of machines @@ -343,7 +344,7 @@ Note: The expressions E1,... defining x1,... are not allowed to use x1,... .... [[definitions]] -=== Definitions: +== Definitions: .... NAME1 == Expression; Definition without arguments @@ -378,7 +379,7 @@ There are a few Definitions which can be used to influence the animator: .... [[comments-and-pragmas]] -=== Comments and Pragmas +== Comments and Pragmas .... B supports two styles of comments: @@ -408,7 +409,7 @@ The whitespace between @ and PRAGMA is optional. ---- [[file-extensions]] -=== File Extensions +== File Extensions .... .mch for abstract machine files @@ -419,7 +420,7 @@ The whitespace between @ and PRAGMA is optional. .... [[differences-with-atelierbb4free]] -=== Differences with AtelierB/B4Free +== 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 @@ -466,7 +467,7 @@ AtelierB/ProB: - In AtelierB/ProB the BOOL type is pre-defined and cannot be redefined [[other-notes]] -=== 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. + diff --git a/src/docs/chapter/user/11_BLanguage/02_Types.adoc b/src/docs/chapter/user/11_BLanguage/02_Types.adoc index b7306b60e2341160e37a083acc3124401a9435bb..f400fc64a9ec0427d5a2a34f210ecba2df106ad2 100644 --- a/src/docs/chapter/user/11_BLanguage/02_Types.adoc +++ b/src/docs/chapter/user/11_BLanguage/02_Types.adoc @@ -1,5 +1,6 @@ + [[types]] -== 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 @@ -10,7 +11,7 @@ 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 +== What is a basic type in B * BOOL * INTEGER @@ -20,7 +21,7 @@ parameter of the machine * τ1 * τ2 (Cartesian product) for τ1 and τ2 being two types [[what-needs-to-be-typed]] -=== What needs to be typed +== What needs to be typed Generally speaking, any constant or variable. More precisely: @@ -46,7 +47,7 @@ ProB will warn you if a variable has not been given a type. inferred for your constants and global variables.* [[restriction-on-the-domains-of-the-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 @@ -72,7 +73,7 @@ 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 +== 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 diff --git a/src/docs/chapter/user/11_BLanguage/10_External_Functions.adoc b/src/docs/chapter/user/11_BLanguage/10_External_Functions.adoc index 57c2973c2d5eec6e6ad8fef97051c4d458707e9c..6190fff8af0e19807c58617f1a33d7d88d4832f8 100644 --- a/src/docs/chapter/user/11_BLanguage/10_External_Functions.adoc +++ b/src/docs/chapter/user/11_BLanguage/10_External_Functions.adoc @@ -1,5 +1,6 @@ + [[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: diff --git a/src/docs/chapter/user/11_BLanguage/11_Recursively_Defined_Functions.adoc b/src/docs/chapter/user/11_BLanguage/11_Recursively_Defined_Functions.adoc index 1fefb0d768dee2f814b23a2e4ad4ad624f1159a0..5acacdb992275cc28e922cf2d15c5145988a2041 100644 --- a/src/docs/chapter/user/11_BLanguage/11_Recursively_Defined_Functions.adoc +++ b/src/docs/chapter/user/11_BLanguage/11_Recursively_Defined_Functions.adoc @@ -1,8 +1,9 @@ + [[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: diff --git a/src/docs/chapter/user/11_BLanguage/20_Tips:_B_Idioms.adoc b/src/docs/chapter/user/11_BLanguage/20_Tips:_B_Idioms.adoc index 89f560dc72c3e26cefef0903ed37f5f1425a7b98..20138fe7fd57426d3f41a51399ef552a5313432d 100644 --- a/src/docs/chapter/user/11_BLanguage/20_Tips:_B_Idioms.adoc +++ b/src/docs/chapter/user/11_BLanguage/20_Tips:_B_Idioms.adoc @@ -1,23 +1,23 @@ + [[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 diff --git a/src/docs/chapter/user/11_BLanguage/21_Tips:_Writing_Models_for_ProB.adoc b/src/docs/chapter/user/11_BLanguage/21_Tips:_Writing_Models_for_ProB.adoc index bc0524752ba11997ff278c6210629f7991da93c0..6fb548d84b644f583618dfae5b316a48b1510e21 100644 --- a/src/docs/chapter/user/11_BLanguage/21_Tips:_Writing_Models_for_ProB.adoc +++ b/src/docs/chapter/user/11_BLanguage/21_Tips:_Writing_Models_for_ProB.adoc @@ -1,6 +1,6 @@ -[[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 diff --git a/src/docs/chapter/user/11_BLanguage/WD/00_section_header.adoc b/src/docs/chapter/user/11_BLanguage/WD/00_section_header.adoc new file mode 100644 index 0000000000000000000000000000000000000000..92a1941243d9f0d7ca0b3d39e584c0274c5c91f7 --- /dev/null +++ b/src/docs/chapter/user/11_BLanguage/WD/00_section_header.adoc @@ -0,0 +1,4 @@ + +[[well-definedness]] += Well Definedness +:leveloffset: +1 diff --git a/src/docs/chapter/user/11_BLanguage/WD/01_Well-Definedness_Checking.adoc b/src/docs/chapter/user/11_BLanguage/WD/01_Well-Definedness_Checking.adoc index 6d28aa617b8f18a40e8f3bb8f8991ac60d820a0c..86900536b03f7f18c677b8dc349d36f2e258a593 100644 --- a/src/docs/chapter/user/11_BLanguage/WD/01_Well-Definedness_Checking.adoc +++ b/src/docs/chapter/user/11_BLanguage/WD/01_Well-Definedness_Checking.adoc @@ -1,5 +1,6 @@ + [[well-definedness-checking]] -== Well-Definedness Checking += Well-Definedness Checking Well-definedness errors can occur in B in the following circumstances: diff --git a/src/docs/chapter/developer/10_java_api/ZZ_section_footer.adoc b/src/docs/chapter/user/11_BLanguage/WD/ZZ_section_footer.adoc similarity index 94% rename from src/docs/chapter/developer/10_java_api/ZZ_section_footer.adoc rename to src/docs/chapter/user/11_BLanguage/WD/ZZ_section_footer.adoc index 3b4360cb20797206e14fc3aa9803c4ff93a4b60d..909c09e0cbf5ccf1b361d16ff5dcdd73c14f6a69 100644 --- a/src/docs/chapter/developer/10_java_api/ZZ_section_footer.adoc +++ b/src/docs/chapter/user/11_BLanguage/WD/ZZ_section_footer.adoc @@ -1 +1,2 @@ + :leveloffset: -1 diff --git a/src/docs/chapter/developer/20_prolog/ZZ_section_footer.adoc b/src/docs/chapter/user/11_BLanguage/ZZ_section_footer.adoc similarity index 94% rename from src/docs/chapter/developer/20_prolog/ZZ_section_footer.adoc rename to src/docs/chapter/user/11_BLanguage/ZZ_section_footer.adoc index 3b4360cb20797206e14fc3aa9803c4ff93a4b60d..909c09e0cbf5ccf1b361d16ff5dcdd73c14f6a69 100644 --- a/src/docs/chapter/developer/20_prolog/ZZ_section_footer.adoc +++ b/src/docs/chapter/user/11_BLanguage/ZZ_section_footer.adoc @@ -1 +1,2 @@ + :leveloffset: -1 diff --git a/src/docs/chapter/user/20_Validation/00_section_header.adoc b/src/docs/chapter/user/20_Validation/00_section_header.adoc new file mode 100644 index 0000000000000000000000000000000000000000..af7d604be139e5e4c3c7097a4553f2ebb61bef07 --- /dev/null +++ b/src/docs/chapter/user/20_Validation/00_section_header.adoc @@ -0,0 +1,4 @@ + +[[validation]] += Validation +:leveloffset: +1 diff --git a/src/docs/chapter/user/20_Validation/CBC/00_section_header.adoc b/src/docs/chapter/user/20_Validation/CBC/00_section_header.adoc new file mode 100644 index 0000000000000000000000000000000000000000..0e592524558bbd8a95cac0853b99603960eed970 --- /dev/null +++ b/src/docs/chapter/user/20_Validation/CBC/00_section_header.adoc @@ -0,0 +1,19 @@ + +[[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>>. diff --git a/src/docs/chapter/user/20_Validation/CBC/01_Constraint_Based_Checking.adoc b/src/docs/chapter/user/20_Validation/CBC/01_Constraint_Based_Checking.adoc index 513ffb791e3fd8102da89a66c71d24998eaaec9a..6aa6a0e79032ad2efc771f5fd5fc6bd282849e34 100644 --- a/src/docs/chapter/user/20_Validation/CBC/01_Constraint_Based_Checking.adoc +++ b/src/docs/chapter/user/20_Validation/CBC/01_Constraint_Based_Checking.adoc @@ -1,23 +1,6 @@ -[[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 diff --git a/src/docs/chapter/user/20_Validation/CBC/10_Bounded_Model_Checking.adoc b/src/docs/chapter/user/20_Validation/CBC/10_Bounded_Model_Checking.adoc index f0ecea7186f38451e7624016faa483b98d34cb3d..9527e1692774191134a5b107a311637664269730 100644 --- a/src/docs/chapter/user/20_Validation/CBC/10_Bounded_Model_Checking.adoc +++ b/src/docs/chapter/user/20_Validation/CBC/10_Bounded_Model_Checking.adoc @@ -1,5 +1,6 @@ + [[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 diff --git a/src/docs/chapter/user/20_Validation/CBC/20_Symbolic_Model_Checking.adoc b/src/docs/chapter/user/20_Validation/CBC/20_Symbolic_Model_Checking.adoc index b74382345b15c090839df433a318b01de1bb7493..a6f2a333cc6133a44d59c15afec5d189ce341ff4 100644 --- a/src/docs/chapter/user/20_Validation/CBC/20_Symbolic_Model_Checking.adoc +++ b/src/docs/chapter/user/20_Validation/CBC/20_Symbolic_Model_Checking.adoc @@ -1,8 +1,9 @@ + [[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. diff --git a/src/docs/chapter/user/20_Validation/CBC/ZZ_section_footer.adoc b/src/docs/chapter/user/20_Validation/CBC/ZZ_section_footer.adoc new file mode 100644 index 0000000000000000000000000000000000000000..909c09e0cbf5ccf1b361d16ff5dcdd73c14f6a69 --- /dev/null +++ b/src/docs/chapter/user/20_Validation/CBC/ZZ_section_footer.adoc @@ -0,0 +1,2 @@ + +:leveloffset: -1 diff --git a/src/docs/chapter/user/20_Validation/MC/00_section_header.adoc b/src/docs/chapter/user/20_Validation/MC/00_section_header.adoc new file mode 100644 index 0000000000000000000000000000000000000000..11b94be55c4d250789587bc890f5aac8202945ab --- /dev/null +++ b/src/docs/chapter/user/20_Validation/MC/00_section_header.adoc @@ -0,0 +1,4 @@ + +[[model-checking]] += Model Checking +:leveloffset: +1 diff --git a/src/docs/chapter/user/20_Validation/MC/01_Consistency_Checking.adoc b/src/docs/chapter/user/20_Validation/MC/01_Consistency_Checking.adoc index 5bb6adc43990ec4868b73ce6de9dc116ce9aad08..37e3eeceaf75ada0e401670d2263e0df02d7bcbd 100644 --- a/src/docs/chapter/user/20_Validation/MC/01_Consistency_Checking.adoc +++ b/src/docs/chapter/user/20_Validation/MC/01_Consistency_Checking.adoc @@ -1,8 +1,9 @@ + [[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 diff --git a/src/docs/chapter/user/20_Validation/MC/10_Distributed_Model_Checking.adoc b/src/docs/chapter/user/20_Validation/MC/10_Distributed_Model_Checking.adoc index 183b9df102461b68f04729f50a7d4e7c4475c00b..3a98ff34494b23dac004708f07225a90c8acddea 100644 --- a/src/docs/chapter/user/20_Validation/MC/10_Distributed_Model_Checking.adoc +++ b/src/docs/chapter/user/20_Validation/MC/10_Distributed_Model_Checking.adoc @@ -1,12 +1,13 @@ + [[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 diff --git a/src/docs/chapter/user/20_Validation/MC/11_DMC.adoc b/src/docs/chapter/user/20_Validation/MC/11_DMC.adoc index 3000e179303349168c0dbfa4f9eec3d4083a4f69..a17d0cca82c0287acffbef8d62e5e86a1347cd31 100644 --- a/src/docs/chapter/user/20_Validation/MC/11_DMC.adoc +++ b/src/docs/chapter/user/20_Validation/MC/11_DMC.adoc @@ -1,4 +1,6 @@ -== 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]. diff --git a/src/docs/chapter/user/20_Validation/MC/12_ParB.adoc b/src/docs/chapter/user/20_Validation/MC/12_ParB.adoc index ae3850716f43f9eef570da7388c8869eccd06dee..a65002b4f162f4fee4058f0ccb2e7392311397b1 100644 --- a/src/docs/chapter/user/20_Validation/MC/12_ParB.adoc +++ b/src/docs/chapter/user/20_Validation/MC/12_ParB.adoc @@ -1,5 +1,6 @@ + [[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 diff --git a/src/docs/chapter/user/20_Validation/MC/20_LTL_Model_Checking.adoc b/src/docs/chapter/user/20_Validation/MC/20_LTL_Model_Checking.adoc index 44d4124f811580b8be8470555be7f1293aba220c..eb16c2c4a365dc1bdc5aabecf611e2ed1d70ae1f 100644 --- a/src/docs/chapter/user/20_Validation/MC/20_LTL_Model_Checking.adoc +++ b/src/docs/chapter/user/20_Validation/MC/20_LTL_Model_Checking.adoc @@ -1,5 +1,6 @@ + [[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 diff --git a/src/docs/chapter/user/20_Validation/MC/30_Symmetry_Reduction.adoc b/src/docs/chapter/user/20_Validation/MC/30_Symmetry_Reduction.adoc index 34450c6b0deb143e7df52b3565a98b27c840c133..69c0ef140f11e668121bb4d645893a82107b9019 100644 --- a/src/docs/chapter/user/20_Validation/MC/30_Symmetry_Reduction.adoc +++ b/src/docs/chapter/user/20_Validation/MC/30_Symmetry_Reduction.adoc @@ -1,10 +1,11 @@ + [[symmetry-reduction]] -== Symmetry Reduction += Symmetry Reduction ProB can make use of symmetries induced by the use of deferred sets in B (and given sets in Z). -=== Static Symmetry Reduction +== Static Symmetry Reduction ProB will perform a limited form of symmetry reduction for constants which are elements of deferred sets. Take the following example: @@ -84,7 +85,7 @@ A = {D1,D2,D3} B = {D4,D5,D6} ---- -=== Symmetry Reduction during Model Checking +== Symmetry Reduction during Model Checking In addition to the above, you can also turn of stronger symmetry reduction for model checking. @@ -128,4 +129,4 @@ Proceedings International Symmetry Conference,Januar,2007,Verlag, https://www3.hhu.de/stups/downloads/pdf/LeMa07_212.pdf]. This is typically the most efficient method. -=== References +== References diff --git a/src/docs/chapter/user/20_Validation/MC/40_LTSmin b/src/docs/chapter/user/20_Validation/MC/40_LTSmin index 9c1fd0098607ff48bc4655c825c063f88af45d3e..8cebdad97341fbffa9268aa947566f334ac2b764 100644 --- a/src/docs/chapter/user/20_Validation/MC/40_LTSmin +++ b/src/docs/chapter/user/20_Validation/MC/40_LTSmin @@ -1,4 +1,6 @@ -== LTSmin Extension + +[[lts-min-extension]] += LTSmin Extension In order to set up LTSmin, do the following: diff --git a/src/docs/chapter/user/20_Validation/MC/ZZ_section_footer.adoc b/src/docs/chapter/user/20_Validation/MC/ZZ_section_footer.adoc new file mode 100644 index 0000000000000000000000000000000000000000..909c09e0cbf5ccf1b361d16ff5dcdd73c14f6a69 --- /dev/null +++ b/src/docs/chapter/user/20_Validation/MC/ZZ_section_footer.adoc @@ -0,0 +1,2 @@ + +:leveloffset: -1 diff --git a/src/docs/chapter/user/20_Validation/00_ProB_Validation_Methods.adoc b/src/docs/chapter/user/20_Validation/ProB_Validation_Methods.adoc similarity index 99% rename from src/docs/chapter/user/20_Validation/00_ProB_Validation_Methods.adoc rename to src/docs/chapter/user/20_Validation/ProB_Validation_Methods.adoc index f666ae83797c69688057a422f0e38a39478c172a..f0a097e16777060d064c6b77b0e0881d0379f19d 100644 --- a/src/docs/chapter/user/20_Validation/00_ProB_Validation_Methods.adoc +++ b/src/docs/chapter/user/20_Validation/ProB_Validation_Methods.adoc @@ -1,3 +1,4 @@ + [[prob-validation-methods]] = ProB Validation Methods diff --git a/src/docs/chapter/user/20_Validation/Refinement_Checking.adoc b/src/docs/chapter/user/20_Validation/Refinement_Checking.adoc index 147bf53129e533d710c092ece90ab225c1b25e9a..8ad9ad95b577e4e63a5417e746c517fc9cc9aa11 100644 --- a/src/docs/chapter/user/20_Validation/Refinement_Checking.adoc +++ b/src/docs/chapter/user/20_Validation/Refinement_Checking.adoc @@ -1,5 +1,6 @@ + [[refinement-checking]] -== Refinement Checking += Refinement Checking ProB can be used for refinement checking of B, Z and CSP specifications. Below we first discuss refinement @@ -8,7 +9,7 @@ in ProB which can be viewed http://stups.hhu.de/ProB/w/Checking_CSP_Assertions[here]. [[what-kind-of-refinement-is-checked]] -=== What kind of refinement is checked? +== What kind of refinement is checked? ProB checks trace refinement. In other words, it checks whether every trace (consisting of executed operations with their parameter values and @@ -22,7 +23,7 @@ refinement checking has to be used with care for classical B machines, but it is well suited for EventB-style machines. [[how-does-it-work-refinement-checking]] -=== How does it work? +== How does it work? 1. Open the abstract specification, explore its state space (e.g.,using an exhaustive temporal model check). diff --git a/src/docs/chapter/user/20_Validation/ZZ_section_footer.adoc b/src/docs/chapter/user/20_Validation/ZZ_section_footer.adoc new file mode 100644 index 0000000000000000000000000000000000000000..909c09e0cbf5ccf1b361d16ff5dcdd73c14f6a69 --- /dev/null +++ b/src/docs/chapter/user/20_Validation/ZZ_section_footer.adoc @@ -0,0 +1,2 @@ + +:leveloffset: -1 diff --git a/src/docs/chapter/user/21_Testing/00_Testing.adoc b/src/docs/chapter/user/21_Testing/00_section_header.adoc similarity index 55% rename from src/docs/chapter/user/21_Testing/00_Testing.adoc rename to src/docs/chapter/user/21_Testing/00_section_header.adoc index f7cdbaa13482dd2e63f855670035bd933e58648a..b5ac8d96700c13f8624fa92e91d51f1c2a2b3d08 100644 --- a/src/docs/chapter/user/21_Testing/00_Testing.adoc +++ b/src/docs/chapter/user/21_Testing/00_section_header.adoc @@ -1,2 +1,4 @@ + [[testing]] = Testing +:leveloffset: +1 diff --git a/src/docs/chapter/user/21_Testing/10_State_Space_Coverage_Analyses.adoc b/src/docs/chapter/user/21_Testing/10_State_Space_Coverage_Analyses.adoc index 4eec9497eda788d123a58ddf423510723f2f1d55..e8fa3a76695b15a2844293a5ec04358930cd6bce 100644 --- a/src/docs/chapter/user/21_Testing/10_State_Space_Coverage_Analyses.adoc +++ b/src/docs/chapter/user/21_Testing/10_State_Space_Coverage_Analyses.adoc @@ -1,5 +1,6 @@ + [[state-space-coverage-analyses]] -== State Space Coverage Analyses += State Space Coverage Analyses ProB provides various ways to analyse the coverage of the state space of a model. In ProB Tcl/Tk these features reside in the Coverage submenu of @@ -48,7 +49,7 @@ The commands to determine vacuous guards and invariants rely on MC/DC coverage, which is detailed below. [[mcdc-coverage]] -=== MC/DC Coverage +== MC/DC Coverage MC/DC (Modified Condition/Decision Coverage) is a coverage criterion which is used in avionics. One core idea is ensure that for every diff --git a/src/docs/chapter/user/21_Testing/11_Test_Case_Generation.adoc b/src/docs/chapter/user/21_Testing/11_Test_Case_Generation.adoc index 3365ccefce645c386a2e1b2ab35f6d1686bef38b..87e0b2fac069bbb25ebbd9584c75fcafd9cdca22 100644 --- a/src/docs/chapter/user/21_Testing/11_Test_Case_Generation.adoc +++ b/src/docs/chapter/user/21_Testing/11_Test_Case_Generation.adoc @@ -1,8 +1,9 @@ + [[test-case-generation]] -== Test Case Generation += Test Case Generation [[introduction-to-test-case-generation]] -=== Introduction +== Introduction Testing aims at finding errors in a system or program. A set of tests is also called a test suite. Test case generation is the process of @@ -61,11 +62,11 @@ state space is finite it may run forever in case an operation cannot be covered (because it is infeasible). [[model-checking-based-test-case-generation]] -=== Model-Checking-Based Test Case Generation +== Model-Checking-Based Test Case Generation Model-checking-based test case generation will build the model's state space, starting from the initial states, until the coverage criterion is satisfied. ProB uses a "breadth-first" approach to search for the test cases. -==== How to run +=== How to run We will use the following B Machine as an example, which is stored in a file called `simplecounter.mch`. @@ -87,7 +88,7 @@ END To start the test case generation there are two alternatives: Using the tcl/tk-application or the command line. -===== From the command line +==== From the command line From the command line there are two commands to configure the test case generation: @@ -132,7 +133,7 @@ variables and constants where more than one possible initialisation exists are written into the trace file, as argument of an INITIALISATION event. -===== In the tcl/tk-application +==== In the tcl/tk-application In the tcl/tk-application the test case generation can be started by choosing _Analyse_ > "Testing" > "model-checking-based test case generation...". In the appearing window one can set the same parameters as described for the command line. @@ -157,7 +158,7 @@ You cannot look at the test cases in ProB. Instead you can open the file you jus .... [[constraint-based-test-case-generation]] -=== Constraint-Based Test Case Generation +== Constraint-Based Test Case Generation Constraint based test case generation allows to explore the state space for a machine and generate traces of operations that cover certain user @@ -178,7 +179,7 @@ typically grows exponentially with the depth of the feasible execution paths. [[example-when-constraint-based-test-case-generation-is-better]] -==== Example: When Constraint-based Test Case Generation is better +=== Example: When Constraint-based Test Case Generation is better Here is an example which illustrates when constraint-based test case generation is better. @@ -240,12 +241,12 @@ no state where BothOverflow is enabled): image::CBC_StateSpace_Example1.png[] [[how-to-run]] -==== How to run +=== How to run We will again use the machine `simplecounter.mch`. To start the test case generation there are three alternatives: Using the tcl/tk-application or using the command line by either providing all settings as command line arguments or in a test description file. -===== From the command line +==== From the command line From the command line there are six relevant settings to configure the test case generation: @@ -288,7 +289,7 @@ The generated test cases are stored in a file called `test_results.xml`. Just as with model-checking-based test case generation you can provide the empty filename `''`, in which case no file is generated, and an empty `EndPredicate` that will only lead to test cases of length 1. [[with-a-test-description-file]] -===== With a test description file +==== With a test description file The configuration for the test case generation can also be provided as an XML file. The format is shown below: @@ -339,7 +340,7 @@ with the following call. ./probcli.sh simplecounter.mch -test_description simple_counter_test_description.xml .... -===== In the tcl/tk-application +==== In the tcl/tk-application In the tcl/tk-application the test case generation can be started by choosing _Analyse > Testing > constraint-based test case generation..._. In the appearing window one can set the same parameters as described for the command line. diff --git a/src/docs/chapter/user/21_Testing/20_Tutorial_Model-Based_Testing.adoc b/src/docs/chapter/user/21_Testing/20_Tutorial_Model-Based_Testing.adoc index f87464a64fa13d4f28fe18e4c0a7411dd612fb3b..3b9610d5545c106ef6ee879724cb5185fccf24f5 100644 --- a/src/docs/chapter/user/21_Testing/20_Tutorial_Model-Based_Testing.adoc +++ b/src/docs/chapter/user/21_Testing/20_Tutorial_Model-Based_Testing.adoc @@ -1,5 +1,6 @@ + [[tutorial-model-based-testing]] -== Tutorial Model-Based Testing += Tutorial Model-Based Testing We assume that you have completed <<tutorial-complete-model-checking,Tutorial Complete Model @@ -36,7 +37,7 @@ There are two ways this coverage can be achieved systematically: using a model-checking-based or a constraint-based approach. [[model-checking-based-testcase-generation]] -=== Model-Checking Based Test Case Generation +== Model-Checking Based Test Case Generation To start the test case generation select _Analyse_ > "Testing" > "model-checking-based test case generation...". In the appearing window one can set some parameters: @@ -98,7 +99,7 @@ You cannot look at the test cases in ProB. Instead you can open the file you jus [[constraint-based-testcase-generation]] -=== Constraint-Based Test Case Generation +== Constraint-Based Test Case Generation The constraint-based test case generation can be started by selecting _Analyse_ > "Testing" > "constraint-based test case generation...". In the appearing window one can set the same parameters as described before (except for the maximum number of states). Clicking on _"View CBC Test Tree"_ in the window popping up will open another window showing the test cases. diff --git a/src/docs/chapter/user/21_Testing/ZZ_section_footer.adoc b/src/docs/chapter/user/21_Testing/ZZ_section_footer.adoc new file mode 100644 index 0000000000000000000000000000000000000000..909c09e0cbf5ccf1b361d16ff5dcdd73c14f6a69 --- /dev/null +++ b/src/docs/chapter/user/21_Testing/ZZ_section_footer.adoc @@ -0,0 +1,2 @@ + +:leveloffset: -1 diff --git a/src/docs/chapter/user/22_Visualisation/00_Visualisation.adoc b/src/docs/chapter/user/22_Visualisation/00_section_header.adoc similarity index 65% rename from src/docs/chapter/user/22_Visualisation/00_Visualisation.adoc rename to src/docs/chapter/user/22_Visualisation/00_section_header.adoc index 9c6ba91ed3a4cfe5becdab8f3c9c12d6d48889c3..cabf81b8d29cbff7d03d9178033abc6ad70762db 100644 --- a/src/docs/chapter/user/22_Visualisation/00_Visualisation.adoc +++ b/src/docs/chapter/user/22_Visualisation/00_section_header.adoc @@ -1,2 +1,4 @@ + [[visualisation]] = Visualisation +:leveloffset: +1 diff --git a/src/docs/chapter/user/22_Visualisation/10_Graphical_Viewer.adoc b/src/docs/chapter/user/22_Visualisation/10_Graphical_Viewer.adoc index 16bdf8160fc67fce8cb40fb9a58c23ddbc162dc6..c6b00bc1f4a49e57fc889ef912aa10aa2bf6447e 100644 --- a/src/docs/chapter/user/22_Visualisation/10_Graphical_Viewer.adoc +++ b/src/docs/chapter/user/22_Visualisation/10_Graphical_Viewer.adoc @@ -1,9 +1,9 @@ [[graphical-viewer]] -== Graphical Viewer += Graphical Viewer [[introduction-to-graphical-viewer]] -=== Introduction +== Introduction ProB can generate a wide range of visualizations for your models, e.g.: @@ -21,7 +21,7 @@ file with the ".ps" extension), or it uses a Dot-Viewer (such as "dotty") to view the file directly. [[setting-up-the-graphical-viewer]] -=== Setting up the Graphical Viewer +== Setting up the Graphical Viewer * GraphViz: in order to make use of the graphical visualization features, you need to install a version of GraphViz suitable for your diff --git a/src/docs/chapter/user/22_Visualisation/20_State_Space_Visualization.adoc b/src/docs/chapter/user/22_Visualisation/20_State_Space_Visualization.adoc index bec97b2dc6c13fa582092a688e13fae43bcc80d3..2b544f05b34e0201e848d3b5d091473105001e9c 100644 --- a/src/docs/chapter/user/22_Visualisation/20_State_Space_Visualization.adoc +++ b/src/docs/chapter/user/22_Visualisation/20_State_Space_Visualization.adoc @@ -1,5 +1,6 @@ + [[state-space-visualization]] -== State Space Visualization += State Space Visualization ProB provides several user-friendly visualization features to help the user to analyze @@ -27,7 +28,7 @@ currently explored by the animation in a separate window. image::Visualising_the_state_space.png[] [[graph-nodes]] -=== Graph Nodes +== Graph Nodes ProB displays the state space as a graph whose nodes correspond to states that are differentiated by their shapes and colors and arcs @@ -54,7 +55,7 @@ DEFINITION `GOAL == P` or by using a command such as "Find state satisfying predicate...") then those predicates are coloured in orange. [[statespace-projections]] -=== Statespace Projections +== Statespace Projections The sub-menu "Statespace Projections" contains several other commands that provide useful views on the state space. @@ -85,7 +86,7 @@ effectively. Some sample here>> [[other-visualization-commands]] -=== Other Visualization Commands +== Other Visualization Commands The "Visualize" menu contains several other sub-menus, to visualize traces and individual states. The command "Shortest Trace to Current @@ -94,7 +95,7 @@ starting from the root node and leading to the current node. The command "Current State" displays the current node and its successor nodes. [[preferences-of-the-visualization]] -=== Preferences of the Visualization +== Preferences of the Visualization Many aspects of the visualization can be configured in the "Graphical Viewer Preferences"... preference window of the "Preferences" menu. @@ -142,4 +143,4 @@ which is useful for examining large graphs. * Against Dotty: Dotty may crash if the graph is too big or complex (and on Solaris and Linux if non-standard mouse buttons are used). -=== References +== References diff --git a/src/docs/chapter/user/22_Visualisation/21_State_space_visualization_examples.adoc b/src/docs/chapter/user/22_Visualisation/21_State_space_visualization_examples.adoc index 48d42d3a6608af1b99d9af53f35b340e2a5253ec..89164bb07d028a7a78d567bc6be8c915ab500acf 100644 --- a/src/docs/chapter/user/22_Visualisation/21_State_space_visualization_examples.adoc +++ b/src/docs/chapter/user/22_Visualisation/21_State_space_visualization_examples.adoc @@ -1,8 +1,9 @@ + [[state-space-visualization-examples]] -== State space visualization examples += State space visualization examples [[alternating-bit-protocol]] -=== Alternating Bit Protocol +== Alternating Bit Protocol This is a visualisation of 3643 states and 11115 transitions of a TLA+ model of the alternating bit protocol, as distributed with the @@ -40,7 +41,7 @@ SeqConstraint == /\ Len(msgQ) \leq msgQLen /\ Len(ackQ) \leq ackQLen SentLeadsToRcvd == \A d \in Data : (sent = d) /\ (sBit # sAck) ~> (rcvd = d) -============================================================================== +============================================================================= ImpliedAction == [ABCNext]_cvars @@ -50,11 +51,11 @@ TProp == \A d \in Data : (sent = d) => [](sent = d) CSpec == ABSpec /\ TNext DataPerm == Permutations(Data) -=============================================================== +============================================================== .... [[mcinnerfifo]] -=== MCInnerFIFO +== MCInnerFIFO This is a visualisation of 3866 states and 9661 transitions of a TLA+ model of a FIFO, as distributed with the @@ -74,7 +75,7 @@ using the "Custom Transition Diagram" feature of ProB: image::MCInnerFIFO_proj_cardq.png[] [[rushhour]] -=== RushHour +== RushHour This is a visualisation of the <<rush-hour-puzzle, Rush @@ -90,7 +91,7 @@ transitions, using the scale option this time: image::RushHour_full_sfdp.png[] [[can-bus]] -=== CAN Bus +== CAN Bus This is a visualisation of the statespace of an Event-B model of a CAN Bus. The colours indicate the size of the BUSwrite variable @@ -99,7 +100,7 @@ Bus. The colours indicate the size of the BUSwrite variable image::CANBus_sfdp.png[] [[hanoi-6-discs]] -=== Hanoi (6 Discs) +== Hanoi (6 Discs) This is a visualisation of the statespace of a B model of the towers of Hanoi for 6 discs. The state space contains 731 nodes and 2186 nodes. @@ -117,7 +118,7 @@ ProB: image::Hanoi6_proj_cardondest.png[] [[threads---partial-order-reduction]] -=== Threads - Partial Order Reduction +== Threads - Partial Order Reduction This is the visualisation of a simple threads model, of two threads with n=51 steps before a synchronisation occurs and threads start again. The diff --git a/src/docs/chapter/user/22_Visualisation/30_Eval_Console.adoc b/src/docs/chapter/user/22_Visualisation/30_Eval_Console.adoc index 61233201f12bd54d6dec7cea07ca28904798b9a4..cd659b919f497eee4b02eff20cea336a0b8545cd 100644 --- a/src/docs/chapter/user/22_Visualisation/30_Eval_Console.adoc +++ b/src/docs/chapter/user/22_Visualisation/30_Eval_Console.adoc @@ -1,5 +1,6 @@ + [[eval-console]] -== Eval Console += Eval Console For this tutorial, load for example the file `StackConstructive.mch` included in the `examples/Tutorial` directory of the diff --git a/src/docs/chapter/user/22_Visualisation/31_Evaluation_View.adoc b/src/docs/chapter/user/22_Visualisation/31_Evaluation_View.adoc index 155be09326a64be7bdac5345870b75c6b8d76254..4db415eb033a676855c0273b54ca0f808d81bf45 100644 --- a/src/docs/chapter/user/22_Visualisation/31_Evaluation_View.adoc +++ b/src/docs/chapter/user/22_Visualisation/31_Evaluation_View.adoc @@ -1,5 +1,6 @@ + [[evaluation-view]] -== Evaluation View += Evaluation View This tutorial describes the use of ProB's evaluation view to explore single states of a model. The view shows the details of a @@ -15,7 +16,7 @@ the values of the sub-expressions. ProB. [[inspecting-the-state-variables-and-constants]] -=== Inspecting the State Variables and Constants +== Inspecting the State Variables and Constants As an example specification we use the Sieve.mch delivered with the ProB Distribution in the "Less Simple" folder. After opening the model do a @@ -44,7 +45,7 @@ B-Expression) to a file. You can also save the values of multiple variables (we will cover this later). [[understanding-the-invariant-and-properties]] -=== Understanding the Invariant and Properties +== Understanding the Invariant and Properties The second objective of the evaluation view is to help understanding why the invariant or the properties are true or false. Therefore the view @@ -124,7 +125,7 @@ introduced predicate it is very easy to see the reason why image::Eval_view6.png[] [[filtering-relevant-information-and-data-extraction]] -=== Filtering relevant information and Data Extraction +== Filtering relevant information and Data Extraction There are two different ways to filter out important information from a state. To demonstrate this feature we can use the model diff --git a/src/docs/chapter/user/22_Visualisation/40_Graphical_Visualization.adoc b/src/docs/chapter/user/22_Visualisation/40_Graphical_Visualization.adoc index ae128cd601a0bf879d03c07478417eedbc13a8fe..47cc70e070cfdacd04f4a826b503d706fd266e73 100644 --- a/src/docs/chapter/user/22_Visualisation/40_Graphical_Visualization.adoc +++ b/src/docs/chapter/user/22_Visualisation/40_Graphical_Visualization.adoc @@ -1,5 +1,6 @@ + [[graphical-visualization]] -== Graphical Visualization += Graphical Visualization The graphical visualization of ProB footnote:[M. Leuschel, M. Samia, J. Bendisposto and L. Luo: Easy Graphical Animation and Formula Viewing for Teaching B. @@ -14,7 +15,7 @@ function in B stipulates which pictures should be displayed. We now show how this animation can be done with very little effort. [[the-graphical-animation-model]] -=== The Graphical Animation Model +== The Graphical Animation Model The animation model is very simple. It is based on individual images and a user-defined animation function, which are both defined in the @@ -156,13 +157,13 @@ can directly handle user sets but does not work well if we need a special image for undefined,...) [[further-examples]] -=== Further Examples +== Further Examples Below we illustrate how the graphical animation model easily provides interesting animations for different models. [[scheduler]] -==== Scheduler +=== Scheduler The scheduler specification taken from footnote:[B. Legeard, F. Peureux, and M. Utting. Automated boundary testing from Z and B. Proceedings of @@ -245,7 +246,7 @@ ANIMATION_FUNCTION == ({r,c,i| r=1 & i:PID & c=i & i:waiting} \/ ---- [[sudoku]] -==== Sudoku +=== Sudoku Using ProB we can also solve Sudoku puzzles. The machine has the variable Sudoku9 of type `1..fullsize-->(1..fullsize+->NRS)`, where NRS is @@ -293,7 +294,7 @@ c:dom(Sudoku9(r)) & i:1.. fullsize & i = Sudoku9(r)(c)} ) ---- -=== Other Features +== Other Features One can define actions for right clicks and mouse clicks and drags: ---- @@ -321,7 +322,7 @@ The following preferences can be used to control padding around cells: SET_PREF_TK_CUSTOM_STATE_VIEW_STRING_PADDING == Nr SET_PREF_TK_CUSTOM_STATE_VIEW_PADDING == Nr ----- - + The following preference can be used to disable the custom graphical visualization view: ----- SET_PREF_TK_CUSTOM_STATE_VIEW_VISIBLE == FALSE @@ -332,4 +333,3 @@ One can control justification of animation strings using either of the two follo ANIMATION_STR_JUSTIFY_LEFT == TRUE ANIMATION_STR_JUSTIFY_RIGHT == TRUE ----- - diff --git a/src/docs/chapter/user/22_Visualisation/ZZ_section_footer.adoc b/src/docs/chapter/user/22_Visualisation/ZZ_section_footer.adoc new file mode 100644 index 0000000000000000000000000000000000000000..909c09e0cbf5ccf1b361d16ff5dcdd73c14f6a69 --- /dev/null +++ b/src/docs/chapter/user/22_Visualisation/ZZ_section_footer.adoc @@ -0,0 +1,2 @@ + +:leveloffset: -1 diff --git a/src/docs/chapter/user/25_CommandLine/00_CommandLine.adoc b/src/docs/chapter/user/25_CommandLine/00_section_header.adoc similarity index 64% rename from src/docs/chapter/user/25_CommandLine/00_CommandLine.adoc rename to src/docs/chapter/user/25_CommandLine/00_section_header.adoc index df5315fef3b49b8b0b6c63336853d0ceed8b5d2b..9b893ce6ba1ff986751228010873c18af76bf392 100644 --- a/src/docs/chapter/user/25_CommandLine/00_CommandLine.adoc +++ b/src/docs/chapter/user/25_CommandLine/00_section_header.adoc @@ -1,2 +1,4 @@ + [[command-line]] = Command Line +:leveloffset: +1 diff --git a/src/docs/chapter/user/25_CommandLine/01_ProB_Cli.adoc b/src/docs/chapter/user/25_CommandLine/01_ProB_Cli.adoc index 4924a74d6da7d9838b9ff85bf0a0aa2b54c90edc..7a9e48344cac975b0423d803c6514a52822550db 100644 --- a/src/docs/chapter/user/25_CommandLine/01_ProB_Cli.adoc +++ b/src/docs/chapter/user/25_CommandLine/01_ProB_Cli.adoc @@ -1,6 +1,6 @@ [[prob-cli]] -== ProB CLI += ProB CLI The ProB Cli (command-line interface) offers many of the ProB features via command-line. As such, you can run ProB from your shell scripts or diff --git a/src/docs/chapter/user/25_CommandLine/02_Using_the_Command-Line_Version_of_ProB.adoc b/src/docs/chapter/user/25_CommandLine/02_Using_the_Command-Line_Version_of_ProB.adoc index 7310f26b6ece5fafe849cbc8e60b03d68401dff6..e550cd84307e1ce20e7c165a56aea3cfcb0737d2 100644 --- a/src/docs/chapter/user/25_CommandLine/02_Using_the_Command-Line_Version_of_ProB.adoc +++ b/src/docs/chapter/user/25_CommandLine/02_Using_the_Command-Line_Version_of_ProB.adoc @@ -1,5 +1,6 @@ + [[using-the-command-line-version-of-prob]] -== Using the Command-Line Version of ProB += Using the Command-Line Version of ProB The command-line version of ProB, called probcli, offers many of the features of the standalone Tcl/Tk Version via the command-line. As such, @@ -14,7 +15,7 @@ groups of commands such as `-p MAXINT 127`). Any argument that is not recognised by `probcli` is treated as a filename to be analysed. [[conventions-used]] -=== Conventions used +== Conventions used The following conventions are used in this guide: @@ -25,7 +26,7 @@ The following conventions are used in this guide: |======================================================================= [[synopsis]] -=== Synopsis +== Synopsis .... |probcli [--help] @@ -45,19 +46,19 @@ probcli M.mch --model-check .... [[options-for-command-line]] -=== Options +== Options [[mc]] -==== -mc +=== -mc -===== Description +==== Description [cols="",] |==================================== |model check; checking at most <nr> states |==================================== -===== Example +==== Example .... probcli my.mch -mc 100 @@ -71,15 +72,15 @@ using the `-goal "PRED"` command and limit the scope of the model checking using the `-scope "PRED"` command. [[model_check]] -==== -model_check +=== -model_check The same as `-mc` but without a limit on the number of nodes checked. ProB will run until the entire state space is explored. [[no]] -==== -no <x> +=== -no <x> -===== Description +==== Description [cols="",] |======================================================================= @@ -91,16 +92,16 @@ ProB will run until the entire state space is explored. * `-nogoal` : do not stop if a state satisfying the GOAL predicate has been found * `-noass` : do not report assertion violations -===== Example +==== Example .... probcli my.mch -mc 1000 -nodead -nogoal .... [[disable_timeout]] -==== -disable_timeout +=== -disable_timeout -===== Description +==== Description [cols="",] |======================================================================= @@ -110,48 +111,48 @@ checking (-mc or -model_check) and animation (-animate). Available as of version 1.5.1-beta7. |======================================================================= -===== Example +==== Example .... probcli my.mch -model-check -disable-timeout .... [[bf]] -==== -bf +=== -bf -===== Description +==== Description [cols="",] |=========================================== |proceed breadth-first during model checking |=========================================== -===== Example +==== Example .... probcli my.mch -bf -mc 1000 .... [[df]] -==== -df +=== -df -===== Description +==== Description [cols="",] |========================================= |proceed depth-first during model checking |========================================= -===== Example +==== Example .... probcli my.mch -df -mc 1000 .... [[mc_mode]] -==== -mc_mode <M> +=== -mc_mode <M> -===== Description +==== Description [cols="",] |======================================================================= @@ -175,16 +176,16 @@ directed model checking>>. * `out_degree_hash` (prioritise nodes with fewer outgoing transitions; mainly useful for deadlock checking) -===== Example +==== Example .... probcli my.mch -model_check -mc_mode random .... [[timeout]] -==== --timeout <N> +=== --timeout <N> -===== Description +==== Description [cols="",] |======================================================================= @@ -196,39 +197,39 @@ as invariant checking or static assertion checking, where it is multiplied by a factor. See the description of the -p option. |======================================================================= -===== Example +==== Example .... probcli my.mch -timeout 10000 .... [[t]] -==== -t +=== -t -===== Description +==== Description [cols="",] |=============================================== |trace check (associated .trace file must exist) |=============================================== -===== Example +==== Example .... probcli my.mch -t .... [[init]] -==== -init +=== -init -===== Description +==== Description [cols="",] |======================== |initialise specification |======================== -===== Example +==== Example .... probcli my.mch -init @@ -255,25 +256,25 @@ ALL OPERATIONS COVERED .... [[cbc]] -==== -cbc <OPNAME> +=== -cbc <OPNAME> -===== Description +==== Description [cols="",] |==================================================================== |constraint-based invariant checking for an operation (also use <OPNAME>=all) |==================================================================== -===== Example +==== Example .... probcli my.mch -cbc all .... [[cbc_deadlock]] -==== -cbc_deadlock +=== -cbc_deadlock -===== Description +==== Description [cols="",] |======================================================================= @@ -288,9 +289,9 @@ state(s). If you want to find a reachable deadlock you have to use the model checker. [[cbc_deadlock_pred]] -==== -cbc_deadlock_pred <PRED> +=== -cbc_deadlock_pred <PRED> -===== Description +==== Description [cols="",] |=================================================== @@ -300,16 +301,16 @@ model checker. This is like -cbc_deadlock but you provide an additional predicate. ProB will only find deadlocks which also make this predicate true. -===== Example +==== Example .... probcli my.mch -cbc_deadlock_pred "n=15" .... [[cbc_assertions]] -==== -cbc_assertions +=== -cbc_assertions -===== Description +==== Description [cols="",] |==================================================== @@ -341,9 +342,9 @@ ASSERTION(s) are tautologies. Both commands can be useful to use ProB as a Prover/Disprover (as is done in Atelier-B 4.3). [[cbc_sequence]] -==== -cbc_sequence <SEQ> +=== -cbc_sequence <SEQ> -===== Description +==== Description [cols="",] |======================================================================= @@ -354,16 +355,16 @@ This will try to find a solution for the constants, initial variable values and parameters which make execution of the given sequence of operations possible. -===== Example +==== Example .... probcli my.mch -cbc_sequence "op1;op2" .... [[strict]] -==== -strict +=== -strict -===== Description +==== Description [cols="",] |======================================================================= @@ -372,16 +373,16 @@ model checking finds a counter example or trace checking fails or any unexpected error happens |======================================================================= -===== Example +==== Example .... probcli my.mch -t -strict .... [[expcterr]] -==== -expcterr <ERR> +=== -expcterr <ERR> -===== Description +==== Description [cols="",] |======================================================================= @@ -390,16 +391,16 @@ certain error to occur. Mainly useful for regression tests (in conjunction with the -strict option). |======================================================================= -===== Example +==== Example .... probcli examples/B/Benchmarks/CarlaTravelAgencyErr.mch -mc 1000 -expcterr invariant_violation -strict .... [[animate]] -==== -animate <Nr> +=== -animate <Nr> -===== Description +==== Description [cols="",] |=============================== @@ -411,16 +412,16 @@ deadlock is reached and report an error. You can also use the command `-animate_all`, which will only stop at a deadlock (and not report an error). Be careful: `-animate_all` could run forever. -===== Example +==== Example .... probcli my.mch -animate 100 .... [[execute]] -==== -execute <Nr> +=== -execute <Nr> -===== Description +==== Description [cols="",] |======================== @@ -444,16 +445,16 @@ operations in the B machine is thus important for -execute faster but after execution one only has access to the first state and the final state of execution -===== Example +==== Example .... probcli my.mch -execute 100 .... [[det_check]] -==== -det_check +=== -det_check -===== Description +==== Description [cols="",] |========================================== @@ -465,16 +466,16 @@ operation is possible, and it can only be executed in one possible way as far as parameters and result is concerned). Currently this option has only an effect for the -animate and the -init commands. -===== Example +==== Example .... probcli my.mch -animate 100 -det_check .... [[det_constants]] -==== -det_constants +=== -det_constants -===== Description +==== Description [cols="",] |========================================== @@ -485,16 +486,16 @@ Checks if the SETUP_CONSTANTS step is deterministic (i.e., only one way to set up the constants is possible). Currently this option has only an effect for the -animate and the -init commands. -===== Example +==== Example .... probcli my.mch -init -det_constants .... [[his]] -==== -his <FILE> +=== -his <FILE> -===== Description +==== Description [cols="",] |================================ @@ -510,7 +511,7 @@ initial state is written out. The -his command is executed after the -init, -animate, -t or -mc commands. See also the -sptxt command to only write the current values of variables and constants to a file. -===== Example +==== Example .... probcli -animate 5 -his history.txt supersimple.mch @@ -533,9 +534,9 @@ With -his_option trace_file as only option, probcli will write the history in Prolog format, which can later be used by the -t command. [[i]] -==== -i +=== -i -===== Description +==== Description [cols="",] |===================== @@ -545,23 +546,23 @@ history in Prolog format, which can later be used by the -t command. After performing the other commands, ProB stays in interactive mode and allows the user to manually animate the loaded specification. -===== Example +==== Example .... probcli my.mch -i .... [[repl]] -==== -repl +=== -repl -===== Description +==== Description [cols="",] |====================================== |start interactive read-eval-print-loop |====================================== -===== Example +==== Example .... probcli my.mch -p CLPFD TRUE -repl @@ -592,16 +593,16 @@ probcli -eval_file MyFormula.txt .... [[c]] -==== -c +=== -c -===== Description +==== Description [cols="",] |========================= |print coverage statistics |========================= -===== Example +==== Example .... probcli my.mch -mc 1000 -c @@ -621,9 +622,9 @@ probcli my.mch -mc 1000 --coverage_summary .... [[cc]] -==== -cc <Nr> <Nr> +=== -cc <Nr> <Nr> -===== Description +==== Description [cols="",] |======================================================================= @@ -631,16 +632,16 @@ probcli my.mch -mc 1000 --coverage_summary that the given number of nodes and transitions have been computed. |======================================================================= -===== Example +==== Example .... probcli my.mch -mc 1000 -cc 10 25 .... [[p]] -==== -p <PREFERENCE> <VALUE> +=== -p <PREFERENCE> <VALUE> -===== Description +==== Description [cols="",] |======================================================================= @@ -650,7 +651,7 @@ probcli my.mch -mc 1000 -cc 10 25 You can also use --pref instead of -p. -===== Example +==== Example .... probcli my.mch -p TIME_OUT 8000 -p CLPFD TRUE -mc 10000 @@ -658,9 +659,9 @@ probcli my.mch -p TIME_OUT 8000 -p CLPFD TRUE -mc 10000 [[prefs]] -==== -pref_group <PREFGROUP> <SETTING> +=== -pref_group <PREFGROUP> <SETTING> -===== Description +==== Description [cols="",] |======================================================================= @@ -668,7 +669,7 @@ probcli my.mch -p TIME_OUT 8000 -p CLPFD TRUE -mc 10000 |======================================================================= -===== Example +==== Example .... probcli my.mch -pref_group model_check unlimited @@ -680,9 +681,9 @@ Available groups and settings are: - PREFERENCE GROUP model_check : SETTINGS [disable_max,unlimited] : Model Checking Limits - PREFERENCE GROUP dot_colors : SETTINGS [classic,dreams,winter] : Colours for Dot graphs -==== -prefs <FILE> +=== -prefs <FILE> -===== Description +==== Description [cols="",] |======================================================================= @@ -693,16 +694,16 @@ please have a look at <<using-the-command-line-version-of-prob,Preferences>> |======================================================================= -===== Example +==== Example .... probcli my.mch -prefs ProB_Preferences.pl .... [[card]] -==== -card <GS> <VAL> +=== -card <GS> <VAL> -===== Description +==== Description [cols="",] |======================================================================= @@ -711,32 +712,32 @@ overrides the default cardinality (which can be set using `-p DEFAULT_SETSIZE`). |======================================================================= -===== Example +==== Example .... probcli my.mch -card PID 5 .... [[goal]] -==== -goal <PRED> +=== -goal <PRED> -===== Description +==== Description [cols="",] |==================================== |set GOAL predicate for model checker |==================================== -===== Example +==== Example .... probcli my.mch -mc 10000000 -goal "n=18"-strict -expcterr goal_found .... [[scope]] -==== -scope <PRED> +=== -scope <PRED> -===== Description +==== Description [cols="",] |======================================================================= @@ -745,64 +746,64 @@ SCOPE predicate will be ignored (invariant will not be checked and no outgoing transitions will be computed) |======================================================================= -===== Example +==== Example .... probcli my.mch -mc 10000000 -scope "n<18" .... [[s]] -==== -s <PORT> +=== -s <PORT> -===== Description +==== Description [cols="",] |================================= |start socket server on given port |================================= -===== Example +==== Example .... probcli my.mch ... .... [[ss]] -==== -ss +=== -ss -===== Description +==== Description [cols="",] |================================ |start socket server on port 9000 |================================ -===== Example +==== Example .... probcli my.mch ... .... [[sf]] -==== -sf +=== -sf -===== Description +==== Description [cols="",] |===================================== |start socket server on some free port |===================================== -===== Example +==== Example .... probcli my.mch ... .... [[sptxt]] -==== -sptxt <FILE> +=== -sptxt <FILE> -===== Description +==== Description [cols="",] |====================================== @@ -816,7 +817,7 @@ infinite sets may be written out symbolically). See also the -his command. -===== Example +==== Example .... probcli -animate 5 -sptxt state.txt supersimple.mch @@ -826,9 +827,9 @@ This will write the values of all variables and constants to the file state.txt after animating the machine 5 steps. [[cache]] -==== -cache <DIRECTORY> +=== -cache <DIRECTORY> -===== Description +==== Description [cols="",] |======================================================================= @@ -848,25 +849,25 @@ However, we do not support refinements at the moment. NOTE: this command can also be used when starting up the ProB Tcl/Tk version. [[logxml]] -==== -logxml <LogFile> +=== -logxml <LogFile> -===== Description +==== Description [cols="",] |====================================================== |log activities and results of probcli in XML format in <LogFile> |====================================================== -===== Example +==== Example .... probcli my.mch -mc 1000 -logxml log.xml .... [[logxml_write_vars]] -==== -logxml_write_vars <PREFIX> +=== -logxml_write_vars <PREFIX> -===== Description +==== Description [cols="",] |======================================================================= @@ -875,80 +876,80 @@ variables having prefix PREFIX in their name into the XML log file (if XML logging has been activated using the -logxml command) |======================================================================= -===== Example +==== Example .... probcli my.mch -execute 1000 -logxml log.xml -logxml_write_vars out .... [[l]] -==== -l <LogFile> +=== -l <LogFile> -===== Description +==== Description [cols="",] |===================================== |log activities <LogFile> in using Prolog format |===================================== -===== Example +==== Example .... probcli my.mch -mc 1000 -l my.log .... [[ll]] -==== -ll +=== -ll -===== Description +==== Description [cols="",] |========================================= |log activities in /tmp/prob_cli_debug.log |========================================= -===== Example +==== Example .... probcli my.mch -mc 1000 -ll .... [[lg]] -==== -lg <LogFile> +=== -lg <LogFile> -===== Description +==== Description [cols="",] |===================== |analyse <LogFile> using gnuplot |===================== -===== Example +==== Example .... probcli my.mch ... .... [[pp]] -==== -pp <FILE> +=== -pp <FILE> -===== Description +==== Description [cols="",] |======================================= |pretty-print internal representation to <FILE> |======================================= -===== Example +==== Example .... probcli my.mch -pp my_pp.mch .... [[ppf]] -==== -ppf <FILE> +=== -ppf <FILE> -===== Description +==== Description [cols="",] |======================================================================= @@ -956,32 +957,32 @@ probcli my.mch -pp my_pp.mch infos |======================================================================= -===== Example +==== Example .... probcli my.mch -ppf my_ppf.mch .... [[v]] -==== -v +=== -v -===== Description +==== Description [cols="",] |========================== |set ProB into verbose mode |========================== -===== Example +==== Example .... probcli my.mch -mc 1000 -v .... [[version]] -==== -version +=== -version -===== Description +==== Description [cols="",] |========================= @@ -991,7 +992,7 @@ probcli my.mch -mc 1000 -v There is also an alternate command called -svers which just prints the version number of ProB. -===== Example +==== Example .... probcli -version @@ -1011,9 +1012,9 @@ You can use `probcli -version -v` to obtain more information about your version of probcli. [[check_java_version]] -==== -check_java_version +=== -check_java_version -===== Description +==== Description [cols="",] |=========================================== @@ -1032,9 +1033,9 @@ Result of checking Java version: .... [[assertions]] -==== -assertions +=== -assertions -===== Description +==== Description [cols="",] |=================================== @@ -1055,16 +1056,16 @@ machine which are not linked (directly or indirectly) to the ASSERTIONS. This optimization will only be made if you provide no other switch, such as -mc or -animate which may require the computation of the variables. -===== Example +==== Example .... probcli my.mch -init -assertions .... [[properties]] -==== -properties +=== -properties -===== Description +==== Description [cols="",] |======================================================================= @@ -1073,16 +1074,16 @@ probcli my.mch -init -assertions will debug the properties. |======================================================================= -===== Example +==== Example .... probcli my.mch -init -properties .... [[dot_output]] -==== -dot_output <PATH> +=== -dot_output <PATH> -===== Description +==== Description [cols="",] |======================================================================= @@ -1096,7 +1097,7 @@ property or assertion. Assertions are numbered A0,A1,... and properties P0,P1,... You can also force to generate dot files for all properties (i.e., also the true ones) using the -dot_all command-line flag. -===== Example +==== Example .... probcli my.mch -init -properties -dot_output somewhere/ @@ -1106,103 +1107,103 @@ This will generate files somewhere/my_P0_false.dot, somewhere/my_P1_false.dot, ... [[rc]] -==== -rc +=== -rc -===== Description +==== Description [cols="",] |============================================== |runtime checking of types/pre-/post-conditions |============================================== -===== Example +==== Example .... probcli my.mch ... .... [[ltlfile]] -==== -ltlfile <FILE> +=== -ltlfile <FILE> -===== Description +==== Description [cols="",] |========================== |check LTL formulas in file <FILE> |========================== -===== Example +==== Example .... probcli my.mch ... .... [[ltlassertions]] -==== -ltlassertions +=== -ltlassertions -===== Description +==== Description [cols="",] |===================================== |check LTL assertions (in DEFINITIONS) |===================================== -===== Example +==== Example .... probcli my.mch ... .... [[ltllimit]] -==== -ltllimit <LIMIT> +=== -ltllimit <LIMIT> -===== Description +==== Description [cols="",] |============================================== |explore at most <LIMIT> states when model-checking LTL |============================================== -===== Example +==== Example .... probcli my.mch ... .... [[save]] -==== -save <FILE> +=== -save <FILE> -===== Description +==== Description [cols="",] |=========================================== |save state space for later refinement check |=========================================== -===== Example +==== Example .... probcli my.mch ... .... [[refchk]] -==== -refchk <FILE> +=== -refchk <FILE> -===== Description +==== Description [cols="",] |=================================================== |refinement check against previous saved state space |=================================================== -===== Example +==== Example .... probcli my.mch ... .... [[mcm_tests]] -==== -mcm_tests <Depth> <MaxStates> <EndPredicate> <FILE> +=== -mcm_tests <Depth> <MaxStates> <EndPredicate> <FILE> Generate test cases for the given specification. Each test case consists of a sequence of operations resp. events (a so-called trace) that @@ -1242,7 +1243,7 @@ EndPredicate:: FILE:: The found test cases a written to the XML file . -===== Example +==== Example .... probcli my.mch -mcm_tests 10 2000 EndStateVar=TRUE testcases.xml -mcm_cover op1,op2 @@ -1265,7 +1266,7 @@ exists are written into the trace file, as argument of an INITIALISATION event. [[mcm_cover]] -==== -mcm_cover <Operation(s)> +=== -mcm_cover <Operation(s)> Specify an operation or event that should be covered when generating test cases with the *-mcm_test* option. Multiple operations/events can @@ -1275,23 +1276,23 @@ several times. See <<mcm-tests, -mcm-tests>> for further details. [[spdot]] -==== -spdot <FILE> +=== -spdot <FILE> -===== Description +==== Description [cols="",] |======================================= |Write graph of the state space to a dot <FILE> |======================================= -===== Example +==== Example .... probcli my.mch -mc 100 -spdot my_statespace.dot .... [[cbc_tests]] -==== -cbc_tests <Depth> <EndPredicate> <File> +=== -cbc_tests <Depth> <EndPredicate> <File> Generate test cases by constraint solving with maximum length *Depth*, the last state satisfies *EndPredicate* and the test cases are written @@ -1300,7 +1301,7 @@ filename is the empty string no file is generated. See also the page on <<test-case-generation,Test_Case_Generation>>. [[cbc_cover]] -==== -cbc_cover <Operation> +=== -cbc_cover <Operation> When generating CB test cases, *Operation* should be covered. The option can be given multiple times to specify several operations. @@ -1315,12 +1316,12 @@ to match all operations whose name contains PartialName. See also the page about <<test-case-generation,Test_Case_Generation>>. [[test_description]] -==== -test_description <File> +=== -test_description <File> Read the options for constraint based test case generation from *File*. [[bmc]] -==== -bmc <Depth> +=== -bmc <Depth> [cols="",] |======================================================================= @@ -1329,27 +1330,27 @@ maximum trace depth specified. Looks for invariant violations using the constraint-based test case generation algorithm. |======================================================================= -===== Example +==== Example .... probcli my.mch -bmc 20 .... [[csp-guide]] -==== -csp-guide <File> +=== -csp-guide <File> Use the CSP File *File* to guide the B Machine ("CSP||B"). (This feature is included since version 1.3.5-beta7.) [[environment-variables-for-command-line]] -=== Environment Variables +== Environment Variables Set NO_COLOR environment variable to disable terminal colors. See also https://no-color.org[https://no-color.org]. [[preferences-for-command-line]] -=== Preferences +== Preferences You can use these preferences within the command: @@ -1478,14 +1479,14 @@ in conjunction with Ignore Hash Collisions) B substitutions |======================================================================= -==== Example +=== Example .... probcli my.mch -p TIME_OUT 5000 -p CLPFD TRUE -p SYMMETRY_MODE hash -mc 1000 .... [[some-probcli-examples]] -=== Some probcli examples +== Some probcli examples To load a file My.mch, setup the constants and initialize it do: @@ -1517,7 +1518,7 @@ probcli -p COMPRESSION -p IGNORE_HASH_COLLISIONS TRUE -p FORGET_STATE_SPACE TRUE .... [[command-line-arguments-for-prob-tcltk]] -=== Command-line Arguments for ProB Tcl/Tk +== Command-line Arguments for ProB Tcl/Tk Note that the stand-alone Tcl/Tk version also supports a limited form of command-line preferences: diff --git a/src/docs/chapter/user/25_CommandLine/ZZ_section_footer.adoc b/src/docs/chapter/user/25_CommandLine/ZZ_section_footer.adoc new file mode 100644 index 0000000000000000000000000000000000000000..909c09e0cbf5ccf1b361d16ff5dcdd73c14f6a69 --- /dev/null +++ b/src/docs/chapter/user/25_CommandLine/ZZ_section_footer.adoc @@ -0,0 +1,2 @@ + +:leveloffset: -1 diff --git a/src/docs/chapter/user/30_OtherLanguages/00_section_header.adoc b/src/docs/chapter/user/30_OtherLanguages/00_section_header.adoc new file mode 100644 index 0000000000000000000000000000000000000000..b6c828a7f176ff9b06a3241933fc9e9f4c4b2b75 --- /dev/null +++ b/src/docs/chapter/user/30_OtherLanguages/00_section_header.adoc @@ -0,0 +1,4 @@ + +[[other-languages]] += Other languages +:leveloffset: +1 diff --git a/src/docs/chapter/user/30_OtherLanguages/00_Other_languages.adoc b/src/docs/chapter/user/30_OtherLanguages/01_Other_languages.adoc similarity index 98% rename from src/docs/chapter/user/30_OtherLanguages/00_Other_languages.adoc rename to src/docs/chapter/user/30_OtherLanguages/01_Other_languages.adoc index 7db97cc83f0d237dc7f0951506b2ff7b2fef2b5a..21cab2877410e9c3295f2ae67c16a0a362c8525a 100644 --- a/src/docs/chapter/user/30_OtherLanguages/00_Other_languages.adoc +++ b/src/docs/chapter/user/30_OtherLanguages/01_Other_languages.adoc @@ -1,5 +1,6 @@ -[[other-languages]] -= Other languages + +[[other-languages-overview]] += Overview Since version 1.2.7 of ProB (July 2008) you can also open Promela files with ProB. @@ -96,7 +97,7 @@ the Rush Hour puzzle>> which also includes a graphical visualisation (using the `animation_function_result` predicate recognised by ProB as of version 1.4.0-rc3). -== Other recognised Prolog predicates += Other recognised Prolog predicates The following can be used to set up an animation image matrix with corresponding actions: * animation_image(Nr,Path) diff --git a/src/docs/chapter/user/30_OtherLanguages/Alloy.adoc b/src/docs/chapter/user/30_OtherLanguages/Alloy.adoc index f9844bb1e6ff53850938565aba4fdc5aa0611308..2db78e1afd799866092b1fe9d0cf215603948252 100644 --- a/src/docs/chapter/user/30_OtherLanguages/Alloy.adoc +++ b/src/docs/chapter/user/30_OtherLanguages/Alloy.adoc @@ -1,5 +1,6 @@ + [[alloy]] -== Alloy += Alloy As of version 1.8 ProB provides support to load http://alloy.mit.edu/alloy/[Alloy] models. The Alloy models are @@ -17,7 +18,7 @@ B language. In addition to basic Alloy constructs, our approach supports integers and orderings. [[installation-alloy]] -=== Installation +== Installation Alloy2B is included as of version 1.8.2 of ProB. @@ -29,10 +30,10 @@ on Github]. * put resulting alloy2b-*.jar file into ProB's lib folder. [[examples-alloy]] -=== Examples +== Examples [[n-queens-alloy]] -==== N-Queens +=== N-Queens .... module queens @@ -79,7 +80,7 @@ PROPERTIES x : queen --> INTEGER & x_ : queen --> INTEGER & y : queen --> INTEGER - & !this.(this : queen => x(this) >= 1 & y(this) >= 1 & x(this) <= card(queen) & y(this) <= + & !this.(this : queen => x(this) >= 1 & y(this) >= 1 & x(this) <= card(queen) & y(this) <= card(queen) & x_(this) >= 1 & x_(this) <= card(queen) & x_(this) = (card(queen) + 1) - x(this) ) & card(queen) = 4 @@ -88,8 +89,8 @@ PROPERTIES INITIALISATION skip OPERATIONS - run0 = - PRE + run0 = + PRE card(queen) = 4 & !(q,q_).(q_ : queen - {q} => not(x(q) = x(q_)) & not(y(q) = y(q_)) & not(x(q) + y(q) = x(q_) + y(q_)) & not(x_(q) + y(q) = x_(q_) + y(q_))) @@ -103,7 +104,7 @@ END [[river-crossing-puzzle]] -==== River Crossing Puzzle +=== River Crossing Puzzle .... module river_crossing open util/ordering[State] @@ -186,7 +187,7 @@ END .... [[proof-with-atelier-b-example]] -==== Proof with Atelier-B Example +=== Proof with Atelier-B Example .... sig Object {} @@ -243,7 +244,7 @@ image::AlloyAtelierB.png[] [[Alloy-Syntax]] -==== Alloy Syntax +=== Alloy Syntax .... Logical predicates: ------------------- @@ -266,8 +267,8 @@ Quantifiers: some DECL | P existential quantification one DECL | P existential quantification with exactly one solution lone DECL | P quantification with one or zero solutions - -where the DECL follow the following form: + +where the DECL follow the following form: x : S choose a singleton subset of S (like x : one S) x : one S choose a singleton subset of S x : S choose x to be any subset of S @@ -309,7 +310,7 @@ Relation Expressions: ~R relational inverse ^R transitive closure of binary relation *R reflexive and transitive closure - + Multiplicity Declarations: --------------------------- The following multiplicity annotations are supported for binary (sub)-relations: @@ -345,7 +346,7 @@ A signature S can be defined to be ordered: s/lte[s2] true if index(e1) =< index(e2) s/gt[s2] true if index(e1) > index(e2) s/gte[s2] true if index(e1) >= index(e2) - + Sequences: ---------- The longest allowed sequence length (maxseq) is set in the scope of a run or check command using the 'seq' keyword. diff --git a/src/docs/chapter/developer/30_tcltk/00_section_header.adoc b/src/docs/chapter/user/30_OtherLanguages/CSP/00_section_header.adoc similarity index 53% rename from src/docs/chapter/developer/30_tcltk/00_section_header.adoc rename to src/docs/chapter/user/30_OtherLanguages/CSP/00_section_header.adoc index ef810780f416f4a75e832338f2c841190535b6b2..e0d3ed9d1df15da89ad1c2df4cccd28891fc3d1a 100644 --- a/src/docs/chapter/developer/30_tcltk/00_section_header.adoc +++ b/src/docs/chapter/user/30_OtherLanguages/CSP/00_section_header.adoc @@ -1,2 +1,4 @@ -= Prolog + +[[csp]] += CSP :leveloffset: +1 diff --git a/src/docs/chapter/user/30_OtherLanguages/CSP/01_CSP-M.adoc b/src/docs/chapter/user/30_OtherLanguages/CSP/01_CSP-M.adoc index bf7ef7d55229573d6e415ea350458d8088cc643e..58c9a834dd771c79007c4c0dfefe92598862a0a1 100644 --- a/src/docs/chapter/user/30_OtherLanguages/CSP/01_CSP-M.adoc +++ b/src/docs/chapter/user/30_OtherLanguages/CSP/01_CSP-M.adoc @@ -1,8 +1,6 @@ -[[csp]] -== CSP [[csp-m]] -=== CSP-M += CSP-M ProB supports machine readable CSPfootnote:[M. Butler and M. Leuschel: _Combining CSP @@ -21,7 +19,7 @@ below) current B machine to control it [[limitations-of-csp-m-support]] -==== Limitations of CSP-M Support +== Limitations of CSP-M Support ProB now supports FDR and ProBE compatible CSP-M syntax, with the following outstanding issues @@ -50,7 +48,7 @@ We still need to tune the animator and model checker for efficiency deeply nested CSP synchronization constructs). [[guiding-b-machines-with-csp]] -==== Guiding B Machines with CSP +== Guiding B Machines with CSP To use this feature of ProB: first open a B Machine, then select "Use CSP File to Guide B..." or "Use Default CSP File" in the "Open @@ -116,4 +114,4 @@ guide the B machine with (This feature is included since version 1.3.5-beta7.) -==== References +== References diff --git a/src/docs/chapter/user/30_OtherLanguages/CSP/02_CSP-M_Syntax.adoc b/src/docs/chapter/user/30_OtherLanguages/CSP/02_CSP-M_Syntax.adoc index 504603935c547eb0a6f9cad75c2c5f55e8cbebed..0e33a0026169a6fdab73ad90ea757177c05b4049 100644 --- a/src/docs/chapter/user/30_OtherLanguages/CSP/02_CSP-M_Syntax.adoc +++ b/src/docs/chapter/user/30_OtherLanguages/CSP/02_CSP-M_Syntax.adoc @@ -1,23 +1,23 @@ [[csp-m-syntax]] -=== CSP-M Syntax += CSP-M Syntax [[details-of-supported-csp-m-syntax]] -==== Details of supported CSP-M syntax +== Details of supported CSP-M syntax Note: you can use the command "Summary of CSP syntax" in ProB's help menu to get an up-to-date list of the supported syntax, along with current limitations. [[process-definitions]] -==== PROCESS DEFINITIONS +== PROCESS DEFINITIONS * `Process = ProcessExpression` [[process-expressions]] -==== PROCESS EXPRESSIONS +== PROCESS EXPRESSIONS * `STOP` deadlocking process * `SKIP` terminating process @@ -54,7 +54,7 @@ empty) * `let f1=E1 ... fk=Ek within P` [[boolean-expressions]] -==== BOOLEAN EXPRESSIONS +== BOOLEAN EXPRESSIONS * `true` * `false` @@ -73,7 +73,7 @@ empty) * `elem(x,s)` sequence member check [[value-expressions]] -==== VALUE EXPRESSIONS +== VALUE EXPRESSIONS * `v+w`, `v-w` addition and subtraction * `v*w` multiplication @@ -106,13 +106,13 @@ explicit sequence for patterns) * `set(s)` convert sequence into set [[comments]] -==== COMMENTS +== COMMENTS * `-- comment until end of line` * `\{- arbitrary comment -}` [[pragmas]] -==== PRAGMAS +== PRAGMAS * `transparent f` where f is a unary function which will then on be ignored by ProB diff --git a/src/docs/chapter/user/30_OtherLanguages/CSP/03_Checking_CSP_Assertions.adoc b/src/docs/chapter/user/30_OtherLanguages/CSP/03_Checking_CSP_Assertions.adoc index 09e4c3afe0b1c5bb5029642c643911a8a043e0e5..d4f3ccfc88b85d34da4013606857b0d537faa656 100644 --- a/src/docs/chapter/user/30_OtherLanguages/CSP/03_Checking_CSP_Assertions.adoc +++ b/src/docs/chapter/user/30_OtherLanguages/CSP/03_Checking_CSP_Assertions.adoc @@ -1,6 +1,6 @@ [[checking-csp-assertions]] -=== Checking CSP Assertions += Checking CSP Assertions As of version 1.3.4, ProB provides support for refinement checking and various other assertions (deadlock, divergence, determinism, and LTL/CTL @@ -11,7 +11,7 @@ assembled and checked in the _CSP Assertions Viewer_. A description of the _CSP Assertions Viewer_ is also given. [[supported-csp-assertions-in-prob]] -==== Supported CSP Assertions in ProB +== Supported CSP Assertions in ProB ProB provides support for checking almost all types of CSP-M assertions that can be checked within FDR2. Besides the assertion types that can be @@ -144,7 +144,7 @@ syntax error. Bear in mind to remove or comment out such LTL/CTL assertions in the CSP-M file before loading it in FDR2. [[csp-assertions-viewer]] -==== CSP Assertions Viewer +== CSP Assertions Viewer When a CSP-M specification is loaded one can open the _CSP Assertion Viewer_ either from the menu bar of the main window by selecting the @@ -392,7 +392,7 @@ button command “Cancel” is replaced by another button command check when the button is clicked on. [[debugging-non-satisfied-assertions]] -==== Debugging Non-satisfied Assertions +== Debugging Non-satisfied Assertions In case an assertion check has failed the user can explore the reason for the assertion violation. If the corresponding assertion is not @@ -489,7 +489,7 @@ In the figure above, the nodes and the transitions of the respective counterexample "a -> (b -> a)+" are colored in red. [[checking-csp-assertions-with-probcli]] -==== Checking CSP Assertions with `probcli` +== Checking CSP Assertions with `probcli` It is also possible to check CSP assertions with the command line version of ProB. The command has the following syntax: @@ -513,4 +513,4 @@ formula by means of a backslash \. `probcli -csp_assertion "Q |= LTL: \"F [c]\"" example.csp` -==== References and Notes +== References and Notes diff --git a/src/docs/chapter/user/30_OtherLanguages/CSP/ZZ_section_footer.adoc b/src/docs/chapter/user/30_OtherLanguages/CSP/ZZ_section_footer.adoc new file mode 100644 index 0000000000000000000000000000000000000000..909c09e0cbf5ccf1b361d16ff5dcdd73c14f6a69 --- /dev/null +++ b/src/docs/chapter/user/30_OtherLanguages/CSP/ZZ_section_footer.adoc @@ -0,0 +1,2 @@ + +:leveloffset: -1 diff --git a/src/docs/chapter/user/30_OtherLanguages/EventB/00_section_header.adoc b/src/docs/chapter/user/30_OtherLanguages/EventB/00_section_header.adoc new file mode 100644 index 0000000000000000000000000000000000000000..65bf97042ab826cbea2b7126ee6b94e92c18eec8 --- /dev/null +++ b/src/docs/chapter/user/30_OtherLanguages/EventB/00_section_header.adoc @@ -0,0 +1,4 @@ + +[[eventb-and-rodin]] += Event B and Rodin +:leveloffset: +1 diff --git a/src/docs/chapter/user/30_OtherLanguages/EventB/01_Event-B.adoc b/src/docs/chapter/user/30_OtherLanguages/EventB/01_Event-B.adoc index 61f7b223c54c5f035466197c55f8464d55368142..68d8e0487d6e7342539abff28194082fbe4f6088 100644 --- a/src/docs/chapter/user/30_OtherLanguages/EventB/01_Event-B.adoc +++ b/src/docs/chapter/user/30_OtherLanguages/EventB/01_Event-B.adoc @@ -1,12 +1,13 @@ + [[event-b]] -== Event-B += Event-B -=== Installation and General Information +== Installation and General Information ProB supports animation and model-checking for Event-B specifications. [[installation-event-b]] -==== Installation +=== Installation To install the ProB plugin for http://www.event-b.org[Rodin], open the _Help_ menu in Rodin and click "Install new software". @@ -20,7 +21,7 @@ Alternativaly, one can use the Tcl/Tk version of ProB but Event-B models must be exported to an .eventb file first (see below). [[animation-and-modelchecking]] -==== Animation and Modelchecking +=== Animation and Modelchecking You can start animation of a model (machine or context) by right-clicking on the model in the Event-B explorer. Choose "Start @@ -29,7 +30,7 @@ Animation / Model Checking". //*TODO:* Here we should add more details about the ProB perspective and views. [[export-for-use-with-the-tcltk-version-of-prob]] -==== Export for use with the Tcl/Tk version of ProB +=== Export for use with the Tcl/Tk version of ProB You can export a model (machine or context) to an .eventb - file by right-clicking on the model in the Event-B explorer. You can find the @@ -39,7 +40,7 @@ Such a .eventb file can be opened by the command line and Tcl/Tk version of ProB. [[theories]] -==== Theories +=== Theories ProB has (limited) support for theories. @@ -54,7 +55,7 @@ Axiomatically defined operators are not supported without additional annotations. [[tagging-operators-event-b]] -===== Tagging operators +==== Tagging operators ProB has some extra support for certain operators. ProB expects an annotation to an operator that provides the information that it should diff --git a/src/docs/chapter/user/30_OtherLanguages/EventB/02_Event-B_Theories.adoc b/src/docs/chapter/user/30_OtherLanguages/EventB/02_Event-B_Theories.adoc index bbab389995a3183f3eb3b129f0762956830f160d..588fcd1596b95ec905b5b1132c10c1390811d5bd 100644 --- a/src/docs/chapter/user/30_OtherLanguages/EventB/02_Event-B_Theories.adoc +++ b/src/docs/chapter/user/30_OtherLanguages/EventB/02_Event-B_Theories.adoc @@ -1,5 +1,6 @@ + [[event-b-theories]] -=== Event-B Theories += Event-B Theories ProB has (limited) support for theories. @@ -14,7 +15,7 @@ Axiomatically defined operators are not supported without additional annotations. [[download-theories]] -==== Download Theories +== Download Theories //An example project with theories: theories2.zip[] TODO: Downloadlink @@ -57,7 +58,7 @@ BinaryTree:: Binary Trees are supported by ProB. [[tagging-operators-event-b-theories]] -==== Tagging operators +== Tagging operators [IMPORTANT] *Please note:* @@ -102,7 +103,7 @@ Nat |======================================================================= [[error-messages]] -===== Error Messages +=== Error Messages In case the .ptm file is missing, you will get an error message such as the following one: diff --git a/src/docs/chapter/user/30_OtherLanguages/EventB/ProB_for_Event-B.adoc b/src/docs/chapter/user/30_OtherLanguages/EventB/ProB_for_Event-B.adoc index d70712cdfbebfcdb53024e0283e61bc1fb9b192f..9f0ea98d52842a255f02ce05b4ab46a92e3693c6 100644 --- a/src/docs/chapter/user/30_OtherLanguages/EventB/ProB_for_Event-B.adoc +++ b/src/docs/chapter/user/30_OtherLanguages/EventB/ProB_for_Event-B.adoc @@ -1,5 +1,6 @@ + [[prob-for-event-b]] -=== ProB for Event-B += ProB for Event-B In addition to classical B (aka B for software development), ProB also supports Event-B and the Rodin platform. ProB can be installed as a diff --git a/src/docs/chapter/user/30_OtherLanguages/EventB/ProB_for_Rodin.adoc b/src/docs/chapter/user/30_OtherLanguages/EventB/ProB_for_Rodin.adoc index ffecd3204cdd349d7c0f3e0e14e02561d8cdaead..b38052ea81953c694dda24ce15bde7650ae0dd09 100644 --- a/src/docs/chapter/user/30_OtherLanguages/EventB/ProB_for_Rodin.adoc +++ b/src/docs/chapter/user/30_OtherLanguages/EventB/ProB_for_Rodin.adoc @@ -1,10 +1,11 @@ + [[prob-for-rodin]] -=== ProB for Rodin += ProB for Rodin Currently there are two versions of ProB available for Rodin. [[prob-1-for-rodin]] -==== ProB (1) for Rodin +== ProB (1) for Rodin The first one is based on the old Java API and supports http://wiki.event-b.org/index.php/Rodin_Platform_2.8_Release_Notes[Rodin @@ -16,7 +17,7 @@ Rodin>>. Nightly releases of this versions are also available on the <<download,Download>> page. [[prob-2.0-for-rodin]] -==== ProB 2.0 for Rodin +== ProB 2.0 for Rodin The second, still experimental, one is based on the new <<prob-java-api,ProB Java API>> (aka ProB 2.0). Because the UI @@ -30,7 +31,7 @@ releases of this versions is also available on the <<download,Download>> page. [[multi-simulation-for-rodin-based-on-prob]] -==== Multi-Simulation for Rodin based on ProB +== Multi-Simulation for Rodin based on ProB There is now also a http://users.ecs.soton.ac.uk/vs2/ac.soton.multisim.updatesite/[Multi-Simulation @@ -38,10 +39,10 @@ Plug-in] available for Rodin. It enables discrete/continuous co-simulation. [[other-plug-ins-for-rodin]] -==== Other Plug-Ins for Rodin +== Other Plug-Ins for Rodin [[prover-evaluation]] -===== Prover Evaluation +=== Prover Evaluation This Plug-in is available at the update site http://nightly.cobra.cs.uni-duesseldorf.de/rodin_provereval/[http://nightly.cobra.cs.uni-duesseldorf.de/rodin_provereval/] @@ -49,7 +50,7 @@ and is capable to evaluate a variety of provers or tactics on a selection of proof obligations. [[camille]] -===== Camille +=== Camille We also develop the Camille text-editor for Rodin. A preliminary version of Camille for Rodin 3.3 is available at the nightly update site: diff --git a/src/docs/chapter/user/30_OtherLanguages/EventB/ZZ_section_footer.adoc b/src/docs/chapter/user/30_OtherLanguages/EventB/ZZ_section_footer.adoc new file mode 100644 index 0000000000000000000000000000000000000000..909c09e0cbf5ccf1b361d16ff5dcdd73c14f6a69 --- /dev/null +++ b/src/docs/chapter/user/30_OtherLanguages/EventB/ZZ_section_footer.adoc @@ -0,0 +1,2 @@ + +:leveloffset: -1 diff --git a/src/docs/chapter/user/30_OtherLanguages/ProZ.adoc b/src/docs/chapter/user/30_OtherLanguages/ProZ.adoc index 6583324e0bbd8e45d65590a75722f8caf49f085a..9bd9df64f6e7ffa2c04505565ad322956aa90973 100644 --- a/src/docs/chapter/user/30_OtherLanguages/ProZ.adoc +++ b/src/docs/chapter/user/30_OtherLanguages/ProZ.adoc @@ -1,5 +1,6 @@ + [[proz]] -== ProZ += ProZ ProZ is a extension of the ProB animator and model checker to support Z specifications. It @@ -11,7 +12,7 @@ https://www3.hhu.de/stups/downloads/pdf/proz07.pdf[iFM'07 article on ProZ] contains more details about the implementation. [[preferences-for-proz]] -=== Preferences +== Preferences A Z specification frequently makes use of comprehension sets, which are often introduced by the underlying translation process from Z to B. @@ -25,10 +26,10 @@ Animation Preferences -> .... [[structure-of-the-z-specification]] -=== Structure of the Z Specification +== Structure of the Z Specification [[state-and-initialization]] -==== State and Initialization +=== State and Initialization To identify the components (like state, initialization, operations) of a Z specification, ProZ expects a certain structure of the specification: @@ -53,7 +54,7 @@ in the initialization, you can do that by including those schemas in the predicate part. [[operations]] -===== Operations +==== Operations ProZ identifies schemas as operations if they satisfy the following properties: @@ -79,7 +80,7 @@ Then the schemas A,B and E describe all the same operation. F is also identified as an operation that leaves the state unchanged. [[axiomatic-definitions]] -===== Axiomatic definitions +==== Axiomatic definitions If axiomatic definitions are present, the declared variables are treated like constants. In the first step of the animation, ProB searches for @@ -112,7 +113,7 @@ ProB will try to find a explicit set that will satisfy the given property. [[invariant]] -===== Invariant +==== Invariant You can add a B-style invariant to the specification by defining a schema "Invariant" that declares a subset of the state variables. In @@ -120,7 +121,7 @@ each explored state the invariant will be checked. The model checking feature of ProB will try to find states that violate the invariant. [[scope-proz]] -===== Scope +==== Scope It is possible to limit the search space of the model checker by adding a schema "Scope" that declares a subset of the state variables. If @@ -128,7 +129,7 @@ such a schema is present, each explored state is checked, if it satisfies the predicate. If not, the state is not further explored. [[abbreviation-definitions]] -===== Abbreviation Definitions +==== Abbreviation Definitions Abbreviation definitions (e.g. Abbr == {1,2,3}) are used like macros by ProZ. A reference to an abbreviation is replaced by its definition in a @@ -139,7 +140,7 @@ definitions (\defs instead of ==) when defining state, initialization, operations, etc. [[graphical-animation-proz]] -==== Graphical animation +=== Graphical animation (*Please note that this functionality is part of the next version. If you want to use graphical animation, please download a version from the @@ -191,10 +192,10 @@ Here is how the animation of the specification should look like: image::ProZ_jars.png[] [[special-constructs]] -==== Special constructs +=== Special constructs [[prozignore]] -===== prozignore +==== prozignore Sometimes it is not desired to check properties of some variables. E.g. ProZ checks if the square function in 2.3.a is a total function by @@ -236,7 +237,7 @@ It is also possible to append these lines to the "fuzzlib" in the fuzz distribution. [[translation-to-b]] -===== Translation to B +==== Translation to B You can inspect the result of the translation process with "Show internal representation" in the _Debug_ menu. Please note that the @@ -248,7 +249,7 @@ shown B machine is normally not syntactically correct because of * lack of support from the pretty printer for every construct [[known-limitations]] -==== Known Limitations +=== Known Limitations * Generic definitions are not supported yet. * Miscellaneous unsupported constructs @@ -257,22 +258,22 @@ shown B machine is normally not syntactically correct because of * The error messages are not very helpful yet. [[summary-of-supported-operators]] -==== Summary of Supported Operators +=== Summary of Supported Operators .... -=== Logical predicates: +== Logical predicates: P \land Q conjunction P \lor Q disjunction P \implies Q implication P \iff Q equivalence \lnot P negation -=== Quantifiers: +== Quantifiers: \forall x:T | P @ Q universal quantification (P => Q) \exists x:T | P @ Q existential quantification (P & Q) \exists_1 x:T | P @ Q exactly one existential quantification -=== Sets: +== Sets: \emptyset empty set \{E,F\} set extension \{~x:S | P~\} set comprehension @@ -288,13 +289,13 @@ shown B machine is normally not syntactically correct because of \bigcup A generalized union of sets of sets \bigcap A generalized intersection of sets of sets -=== Pairs: +== Pairs: E \mapsto F pair S \cross T Cartesian product first E first part of pair second E second part of pair -=== Numbers: +== Numbers: \nat Natural numbers \num Integers \nat_1 Positive natural numbers @@ -314,7 +315,7 @@ shown B machine is normally not syntactically correct because of **: modulo of negative numbers not supported -=== Functions: +== Functions: S \rel T relations S \pfun T partial functions from S to T S \fun T total functions from S to T @@ -331,7 +332,7 @@ shown B machine is normally not syntactically correct because of R \oplus Q overriding R \plus transitive closure -=== Sequences: +== Sequences: \langle E,... \rangle explicit sequence \seq S sequences over S \seq_1 S non-empty sequences diff --git a/src/docs/chapter/user/30_OtherLanguages/TLA.adoc b/src/docs/chapter/user/30_OtherLanguages/TLA.adoc index f43ed2cb03e99d8c02fddd284bae40b9e00f468d..2fb5a300b57de2d39d1b3062fc2c5133290df274 100644 --- a/src/docs/chapter/user/30_OtherLanguages/TLA.adoc +++ b/src/docs/chapter/user/30_OtherLanguages/TLA.adoc @@ -1,11 +1,12 @@ + [[tla]] -== TLA += TLA As of version 1.3.5, ProB supports http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html[TLA+]. [[using-prob-for-animation-and-model-checking-of-tla-specifications]] -=== Using ProB for Animation and Model Checking of TLA+ specifications +== Using ProB for Animation and Model Checking of TLA+ specifications The http://nightly.cobra.cs.uni-duesseldorf.de/tcl/[latest version of ProB] uses the translator TLA2B, which translates the non temporal part @@ -32,7 +33,7 @@ also supports TLA syntax and you can experiment with its predicate and expression evaluation capabilities. [[tla2b]] -=== TLA2B +== TLA2B The parser and semantic analyzer http://research.microsoft.com/en-us/um/people/lamport/tla/sany.html[SANY] @@ -63,7 +64,7 @@ under the ASSUME clause. TLA2B supports furthermore overriding of a constant or definition by another definition in the configuration file. [[supported-tla-syntax]] -=== Supported TLA+ syntax +== Supported TLA+ syntax .... Logic @@ -183,14 +184,14 @@ foo == ... Init == ... Next == ... Spec == ... -===================== +==================== .... Temporal formulas and unused definitions are ignored by TLA2B (they are also ignored by the type inference algorithm). [[limitations-of-the-translation]] -=== Limitations of the translation +== Limitations of the translation * due to the strict type system of the B method there are several restrictions to TLA+ modules. @@ -202,7 +203,7 @@ the tuple must have the same type operator with arguments as argument (e.g.: `foo(bar(_),p)`) [[tla-actions]] -=== TLA+ Actions +== TLA+ Actions ''''' @@ -216,7 +217,7 @@ by ProB are not necessarily identical with the actions determined by TLC. [[understanding-the-type-checker]] -=== Understanding the type checker +== Understanding the type checker Corresponding B types to TLA+ data values (let type(e) be the type of the expression e): diff --git a/src/docs/chapter/user/30_OtherLanguages/ZZ_section_footer.adoc b/src/docs/chapter/user/30_OtherLanguages/ZZ_section_footer.adoc new file mode 100644 index 0000000000000000000000000000000000000000..909c09e0cbf5ccf1b361d16ff5dcdd73c14f6a69 --- /dev/null +++ b/src/docs/chapter/user/30_OtherLanguages/ZZ_section_footer.adoc @@ -0,0 +1,2 @@ + +:leveloffset: -1 diff --git a/src/docs/chapter/user/40_AdvancedFeatures/00_Advanced_Features.adoc b/src/docs/chapter/user/40_AdvancedFeatures/00_section_header.adoc similarity index 92% rename from src/docs/chapter/user/40_AdvancedFeatures/00_Advanced_Features.adoc rename to src/docs/chapter/user/40_AdvancedFeatures/00_section_header.adoc index 9871f041dd6b8445699650d5ae80f590c63e2708..682deae961ed15b77b83662d4e29baefe69028a7 100644 --- a/src/docs/chapter/user/40_AdvancedFeatures/00_Advanced_Features.adoc +++ b/src/docs/chapter/user/40_AdvancedFeatures/00_section_header.adoc @@ -1,5 +1,7 @@ + [[advanced-features]] = Advanced Features +:leveloffset: +1 Over the years, the ProB Team developed a few features for advanced users. You can find further descriptions and tutorials on how to use them in the following sections. diff --git a/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/00_section_header.adoc b/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/00_section_header.adoc new file mode 100644 index 0000000000000000000000000000000000000000..df0714c37873281719bd0270263262c48136ba5f --- /dev/null +++ b/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/00_section_header.adoc @@ -0,0 +1,4 @@ + +[[feature-description]] += Feature Description +:leveloffset: +1 diff --git a/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/01_Bash_Completion.adoc b/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/01_Bash_Completion.adoc index 3bf16857bef494bdea5c96bb765e3db5894087c5..94353ac658bcaca277709b83e62a6c5efc2749d7 100644 --- a/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/01_Bash_Completion.adoc +++ b/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/01_Bash_Completion.adoc @@ -1,5 +1,6 @@ + [[bash-completion]] -== Bash Completion += Bash Completion For the http://en.wikipedia.org/wiki/Bash_(Unix_shell)[Bash] Unix Shell we provide command completion support. @@ -12,7 +13,7 @@ $ probcli -re .... [[installation-bash-completion]] -=== Installation +== Installation A generated version of the command completion for Bash is available http://nightly.cobra.cs.uni-duesseldorf.de/bash/prob_completion.sh[here]. @@ -28,7 +29,7 @@ settings, e.g. in the *.bashrc* or *.profile* files in your home directory. [[contributing]] -=== Contributing +== Contributing Bugs and improvements can be submitted on the project's https://github.com/bivab/prob_bash_completion[GitHub Page] diff --git a/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/02_Common_Subexpression_Elimination.adoc b/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/02_Common_Subexpression_Elimination.adoc index c969797a5726d0be2d8bce3101a6a7d0550a8912..269c27234ab8486b111bdb4046e8d169018d4e13 100644 --- a/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/02_Common_Subexpression_Elimination.adoc +++ b/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/02_Common_Subexpression_Elimination.adoc @@ -1,12 +1,13 @@ + [[common-subexpression-elimination]] -== Common Subexpression Elimination += Common Subexpression Elimination As of version 1.5.1 ProB supports https://en.wikipedia.org/wiki/Common_subexpression_elimination[common subexpression elimination (CSE)]. [[basics-of-cse]] -=== Basics of CSE +== Basics of CSE To enable CSE you need to set the advanced preference `CSE` to true (this can be done using the switch `-p CSE TRUE` when using the @@ -50,7 +51,7 @@ well-definedness (e.g., suppose a is not in the domain of f) and for performance. [[substitutions]] -=== Substitutions +== Substitutions To enable CSE also inside substitutions (aka B statements) you need to set the preference `CSE_SUBST` to true. By default, the CSE will only be @@ -59,7 +60,7 @@ the properties or individual predicates inside operations (but not the operation as a whole). [[sharing-predicates]] -=== Sharing Predicates +== Sharing Predicates By default ProB's CSE will also share predicates. You can turn off CSE for predicates, i.e., only expressions get shared, by setting the @@ -77,7 +78,7 @@ After setting `CSE_PRED` to `FALSE`, this will be translated into: `LET @0==(x + 1) IN @0 > 10 & (@0 > 10 => y = 22)` [[other-preferences]] -=== Other Preferences +== Other Preferences ProB will also share expressions which are potentially not well-defined, and takes extra care with those expressions (in particular in the @@ -96,7 +97,7 @@ and ProB will find the solution `x=4`. With `CSE_WD_ONLY` to `TRUE`, the predicate will be left unchanged (and ProB will find the same solution). [[tips]] -=== Tips +== Tips To inspect the effect of CSE, you do one of the following: diff --git a/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/03_PROBPATH.adoc b/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/03_PROBPATH.adoc index 6c9e950350c1b342886878774682b7fca3f73da1..8a4bbc75f9fd736b4339884179169951b1f86923 100644 --- a/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/03_PROBPATH.adoc +++ b/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/03_PROBPATH.adoc @@ -1,5 +1,6 @@ + [[probpath]] -== PROBPATH += PROBPATH Starting with version 1.5 of ProB, it is possible to customize where the parser will ProB will search for referenced files. diff --git a/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/04_TLC.adoc b/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/04_TLC.adoc index 18a2b529a5543eae8b0c3c593c065fd183d87c29..d5214c46c89662dd1b44fd4c0784baf434ddff52 100644 --- a/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/04_TLC.adoc +++ b/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/04_TLC.adoc @@ -1,5 +1,6 @@ + [[tlc]] -== TLC += TLC As of version 1.4.0, ProB can make use of http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html[TLC] @@ -13,10 +14,10 @@ http://research.microsoft.com/en-us/um/people/lamport/tla/license.html[MIT License]. [[how-to-use-tlc]] -=== How to use TLC +== How to use TLC [[using-tlc-in-prob-tcltk]] -==== Using TLC in ProB Tcl/Tk +=== Using TLC in ProB Tcl/Tk First you have to open a B specification in the ProB GUI. Then you can select the menu command "Model Check with TLC" in the @@ -43,7 +44,7 @@ pane) to give an optimal feedback. image::Model_Checking_With_TLC_Trace.png[] [[requirements]] -===== Requirements +==== Requirements On Linux the tlc-thread package is required to run TLC from the tcl/tk ui: @@ -51,7 +52,7 @@ ui: `sudo apt-get install tcl-thread` [[using-tlc-in-probcli]] -==== Using TLC in probcli +=== Using TLC in probcli You can use the following switch to use TLC rather than ProB's model checker: @@ -75,7 +76,7 @@ be used by TLC. So, a call might look like this: `probcli FILE.mch -mc_with_tlc -p TLC_WORKERS 2 -noltl` [[when-to-use-tlc]] -=== When to use TLC +== When to use TLC TLC is extremely valuable when it comes to explicit state model checking for large state spaces. Otherwise, TLC has no constraint solving @@ -100,7 +101,7 @@ http://stups.hhu.de/w/Special:Publication/HansenLeuschel_TLC4B_techreport[techni report] that describes our translation from B to TLA+. [[limitations-tlc]] -=== Limitations +== Limitations The following constructs are currently not supported by the TLC4B translator: @@ -110,7 +111,7 @@ translator: * Sequential composition statement (G;H) [[visited-states]] -=== Visited States +== Visited States Sometimes TLC will show a different number of visited states compared to the ProB model checker. The following example should illustrate this @@ -136,7 +137,7 @@ image::NumberOfStates.jpeg[] TLC will only report 10 distinct states (10 initialization states). [[more-information]] -=== More Information +== More Information More information can be found in our https://www3.hhu.de/stups/downloads/pdf/HansenLeuschel_ABZ14.pdf[ABZ'14 diff --git a/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/ZZ_section_footer.adoc b/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/ZZ_section_footer.adoc new file mode 100644 index 0000000000000000000000000000000000000000..909c09e0cbf5ccf1b361d16ff5dcdd73c14f6a69 --- /dev/null +++ b/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/ZZ_section_footer.adoc @@ -0,0 +1,2 @@ + +:leveloffset: -1 diff --git a/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/00_section_header.adoc b/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/00_section_header.adoc new file mode 100644 index 0000000000000000000000000000000000000000..de7acf42b5f29a88672d0706ad4cc811df14bba7 --- /dev/null +++ b/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/00_section_header.adoc @@ -0,0 +1,4 @@ + +[[using-prob]] += Using ProB +:leveloffset: +1 diff --git a/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Generating_Documents_with_ProB_and_Latex.adoc b/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Generating_Documents_with_ProB_and_Latex.adoc index 43868c24ce1c6d586899d05eab359305ee1d1024..5e70f08f5df899433fb12ea064d6e4a68f24cf64 100644 --- a/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Generating_Documents_with_ProB_and_Latex.adoc +++ b/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Generating_Documents_with_ProB_and_Latex.adoc @@ -1,12 +1,13 @@ + [[generating-documents-with-prob-and-latex]] -== Generating Documents with ProB and Latex += Generating Documents with ProB and Latex ProB can (as of version 1.6.1) be used to process Latex files, i.e., the command-line tool probcli scans a given Latex file and replaces certain commands by processed results. [[usage-generating-documents]] -=== Usage +== Usage A typical usage would be as follows: @@ -33,7 +34,7 @@ features: https://www3.hhu.de/stups/prob/images/7/7f/Prob_latex_doc.pdf[ProB Latex Documentation] [[commands]] -=== Commands +== Commands The commands are described in the PDF document above. Here is a short summary of some of the commands: @@ -94,7 +95,7 @@ for every element of the set expression, setting the identifier to a value of the set. [[some-examples]] -=== Some Examples +== Some Examples * Presentation held in Grenoble in September 2016 about "Constraint Programming Puzzles in B" diff --git a/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_Atelier_B.adoc b/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_Atelier_B.adoc index 6fd21b0826998ec054a9fd21b7b2015134a750cc..0fdd9576f1270dfd54be6aaaccc98da4fabfb72f 100644 --- a/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_Atelier_B.adoc +++ b/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_Atelier_B.adoc @@ -1,12 +1,13 @@ + [[using-prob-with-atelier-b]] -== Using ProB with Atelier B += Using ProB with Atelier B As of version 1.3, ProB contains a much improved parser which tries be compliant with Atelier B as much as possible. [[atelier-b-plugin]] -=== Atelier B Plugin +== Atelier B Plugin There is also a http://tools.clearsy.com/tools/atelier-b-4-0-gui/external-tools-integration/prob-etool-generation/[plugin @@ -14,10 +15,10 @@ for Atelier B] for use withthe standalone Tcl/Tk Version on http://www.atelierb.eu/[Atelier B] projects. [[differences-with-atelier-b]] -=== Differences with Atelier B +== Differences with Atelier B [[extra-features-of-prob]] -==== Extra Features of ProB +=== Extra Features of ProB * Identifiers: ProB also allows identifiers consisting of a single letter. ProB also accepts enumerated set elements to be used as @@ -59,7 +60,7 @@ machines around it: `(IF x<0 THEN -x ELSE x END)` [[limitations-with-atelierb]] -==== Limitations +=== Limitations * Parsing: ProB will require parentheses around the comma, the relational composition, and parallel product operators. For example, you diff --git a/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_KODKOD.adoc b/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_KODKOD.adoc index bcca0e0fb67ca87fd0eb099c041da6552657ed3e..bfea468d07c43ef17258cf6df2fdf396f3c32676 100644 --- a/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_KODKOD.adoc +++ b/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_KODKOD.adoc @@ -1,5 +1,6 @@ + [[using-prob-with-kodkod]] -== Using ProB with KODKOD += Using ProB with KODKOD As of version 1.3.5 ProB can make use of http://alloy.mit.edu/kodkod/[Kodkod] as an alternate way of solving @@ -7,7 +8,7 @@ constraints. Kodkod provides a relational interface to SAT solvers and is the heart of the http://alloy.mit.edu/alloy/[Alloy] tool. [[how-to-enable-kodkod]] -=== How to enable Kodkod +== How to enable Kodkod For the command-line version you need to call prob as follows: @@ -27,7 +28,7 @@ For the ProB Tcl/Tk Version you should select the menu command "Enable Kodkod for Properties" in the _Preferences_ menu. [[what-can-be-translated-kodkod]] -=== What can be translated +== What can be translated * Types: ** Basic Types: Deferred Sets, enumerated sets, integers, booleans @@ -53,7 +54,7 @@ analysis can estimate the interval of its possible values. unless you set the `KODKOD_ONLY_FULL` preference to FALSE. [[when-is-the-kokod-translation-used]] -=== When is the Kokod translation used +== When is the Kokod translation used Once enabled, the Kodkod translation will be used in the following circumstances: @@ -67,7 +68,7 @@ _Verify_ -> Constraint-Based Checking) * for the REPL in probcli (`probcli -p KODKOD TRUE -repl`) [[sat-solver]] -=== SAT solver +== SAT solver By default Kodkod in ProB uses the bundled SAT4J solver. You can switch to using minisat by putting a current version of `libminisat.jnilib` @@ -85,7 +86,7 @@ These files can be downloaded from the http://alloy.mit.edu/kodkod/download.html[Kodkod download site]. [[more-preferences]] -=== More Preferences +== More Preferences If you set `KODKOD_ONLY_FULL` to `FALSE`, then the Kodkod translation can be applied to part of a predicate. In other words, the predicate @@ -107,7 +108,7 @@ interested in only one solution and `KODKOD_ONLY_FULL` is `TRUE`, then you should set this value to 1. [[more-details-on-kodkod]] -=== More details +== More details * https://www3.hhu.de/stups/downloads/pdf/PlaggeLeuschel_Kodkod2012.pdf[Plagge, Leuschel. Validating B, Z and TLA+ using ProB and Kodkod. In Proceedings diff --git a/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_Z3.adoc b/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_Z3.adoc index c40f980ca6c0c3c542a09ca6682690160ef822af..4c663296a83e1b0b761e711adca4002fe4f387bf 100644 --- a/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_Z3.adoc +++ b/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_Z3.adoc @@ -1,12 +1,13 @@ + [[using-prob-with-z3]] -== Using ProB with Z3 += Using ProB with Z3 The current nightly versions of ProB can make use of https://github.com/Z3Prover/z3[Z3] as an alternate way of solving constraints. [[how-to-use-z3-within-prob]] -=== How to use Z3 within ProB +== How to use Z3 within ProB One can start a REPL (Read-Eval-Print-Loop) by starting probcli with the `-repl` command line option. Any predicate preceded with `:z3` will be @@ -18,7 +19,7 @@ enabled by setting the corresponding preference by passing on the command line. [[how-to-install-z3-for-prob]] -=== How to install Z3 for ProB +== How to install Z3 for ProB First of all, download a nightly build of ProB from the <<download,Downloads>> page. To connect Z3 to ProB you also need the @@ -47,7 +48,7 @@ can not be loaded, ProB will answer with "solver_not_available" when Z3 is queried. [[what-can-be-translated-z3]] -=== What can be translated +== What can be translated Currently, the Z3 translation is unable to cope with the following constructs: @@ -67,7 +68,7 @@ When used together with ProB, everything Z3 can not be coped with will be handled by ProB alone automatically. [[examples-z3]] -=== Examples +== Examples Using the repl, one can try out different examples. diff --git a/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/ZZ_section_footer.adoc b/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/ZZ_section_footer.adoc new file mode 100644 index 0000000000000000000000000000000000000000..909c09e0cbf5ccf1b361d16ff5dcdd73c14f6a69 --- /dev/null +++ b/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/ZZ_section_footer.adoc @@ -0,0 +1,2 @@ + +:leveloffset: -1 diff --git a/src/docs/chapter/user/40_AdvancedFeatures/ZZ_section_footer.adoc b/src/docs/chapter/user/40_AdvancedFeatures/ZZ_section_footer.adoc new file mode 100644 index 0000000000000000000000000000000000000000..909c09e0cbf5ccf1b361d16ff5dcdd73c14f6a69 --- /dev/null +++ b/src/docs/chapter/user/40_AdvancedFeatures/ZZ_section_footer.adoc @@ -0,0 +1,2 @@ + +:leveloffset: -1 diff --git a/src/docs/chapter/user/50_ProB2/00_ProB2.adoc b/src/docs/chapter/user/50_ProB2/00_section_header.adoc similarity index 56% rename from src/docs/chapter/user/50_ProB2/00_ProB2.adoc rename to src/docs/chapter/user/50_ProB2/00_section_header.adoc index 349d5b31fabd423e8ce893a67e1c12809f1fa09f..a26ea8732cd1984af2dbd31dfe4b14543c728ea7 100644 --- a/src/docs/chapter/user/50_ProB2/00_ProB2.adoc +++ b/src/docs/chapter/user/50_ProB2/00_section_header.adoc @@ -1,2 +1,4 @@ + [[prob2.0]] = ProB 2.0 +:leveloffset: +1 diff --git a/src/docs/chapter/user/50_ProB2/01_ProB_2.0_Development.adoc b/src/docs/chapter/user/50_ProB2/01_ProB_2.0_Development.adoc index a6e47a29c550e52e68f8831eb835857de1d1ca03..20943a1231da9cb8fe3920da78e4d0881ac88cde 100644 --- a/src/docs/chapter/user/50_ProB2/01_ProB_2.0_Development.adoc +++ b/src/docs/chapter/user/50_ProB2/01_ProB_2.0_Development.adoc @@ -1,11 +1,12 @@ + [[prob2.0_general]] -== General += General [[prob2.0-development]] -== ProB 2.0 Development += ProB 2.0 Development [[basic-design-principles]] -=== Basic Design Principles +== Basic Design Principles One of our main design goals was that we wanted to build our UI on top of a programmatic API. Our goal was to bring the ProB 2.0 API into a @@ -29,7 +30,7 @@ spent quite a bit of energy developing a developer friendly console for testing out features as they are being developed. [[why-groovy]] -=== Why Groovy? +== Why Groovy? The scripting language that we chose is Groovy. It is a dynamically typed JVM language. Because of the seamless integration between Java and @@ -45,7 +46,7 @@ ProB 2.0, we redefined the java.lang.String class so that we can specify the correct Parser with which a string should be parsed. [[explanation-of-the-basic-programmatic-abstractions]] -=== Explanation of the basic programmatic abstractions +== Explanation of the basic programmatic abstractions The basic programmatic abstractions that are available in the ProB 2.0 API are the Model, Trace, and StateSpace abstractions. The Model @@ -57,7 +58,7 @@ different is available <<programmatic-abstractions-in-the-prob-2.0-api,here>>. [[tutorial-of-the-current-features-of-prob-2.0]] -=== Tutorial of the Current Features of ProB 2.0 +== Tutorial of the Current Features of ProB 2.0 A tutorial for the current features of ProB 2.0 is available <<prob2-tutorial,here>>. diff --git a/src/docs/chapter/user/50_ProB2/02_ProB_2.0_within_Rodin_and_a_HTML_Visualization_Example.adoc b/src/docs/chapter/user/50_ProB2/02_ProB_2.0_within_Rodin_and_a_HTML_Visualization_Example.adoc index c4d450dd0f282d366587901ef8cce2e53e482a63..f8e2ec4b1ad7e07d1171abcc3576608beba27bfd 100644 --- a/src/docs/chapter/user/50_ProB2/02_ProB_2.0_within_Rodin_and_a_HTML_Visualization_Example.adoc +++ b/src/docs/chapter/user/50_ProB2/02_ProB_2.0_within_Rodin_and_a_HTML_Visualization_Example.adoc @@ -1,8 +1,9 @@ + [[prob2-within-rodin]] -== ProB 2.0 within Rodin += ProB 2.0 within Rodin [[installing-prob-2.0-from-rodin-2.7-or-later]] -=== Installing ProB 2.0 from Rodin 2.7 or later +== Installing ProB 2.0 from Rodin 2.7 or later ProB 2.0 for Rodin 3.1 can be installed from the update site, which is located http://nightly.cobra.cs.uni-duesseldorf.de/prob2/updates/releases/advance-final/[here]. @@ -19,7 +20,7 @@ image::Install_prob2.png[] and install the ProB 2.0 plugin [[obtaining-the-latest-prob-binary]] -=== Obtaining the latest ProB binary +== Obtaining the latest ProB binary Open a Groovy Console and type `upgrade latest`. @@ -31,14 +32,14 @@ binary and the lib directory into a `.prob` directory in your home directory. [[import-the-lift-project]] -=== Import the Lift Project +== Import the Lift Project Select the Rodin `Import…` menu command and import the #FIXME Lift.zip LINK. [[start-animating-the-lift]] -=== Start Animating the Lift +== Start Animating the Lift Right-click on the `MLift` model and select the `Start Animation` command: @@ -50,7 +51,7 @@ Click on setup_constants and initialise in the Events view: image::MLiftEventsView.png[] [[open-html-visualization]] -=== Open HTML Visualization +== Open HTML Visualization Go into the BMotion Studio Menu at the top and select `Open BMotion Studio Template`: diff --git a/src/docs/chapter/user/50_ProB2/Prob2-advance-release.adoc b/src/docs/chapter/user/50_ProB2/Prob2-advance-release.adoc index 078eaba30f8f48a986d5b7a7320959775095d09f..c91ac60ab9c665f524bda0762abc6c6819a5e0b5 100644 --- a/src/docs/chapter/user/50_ProB2/Prob2-advance-release.adoc +++ b/src/docs/chapter/user/50_ProB2/Prob2-advance-release.adoc @@ -1,4 +1,6 @@ -== ProB 2.0 Advanced Release + +[[prob2.0_advanced_release]] += ProB 2.0 Advanced Release ProB 2.0 for Rodin 3.1 can be installed from the update site located at: http://nightly.cobra.cs.uni-duesseldorf.de/prob2/updates/releases/advance-final/ diff --git a/src/docs/chapter/user/50_ProB2/ZZ_section_footer.adoc b/src/docs/chapter/user/50_ProB2/ZZ_section_footer.adoc new file mode 100644 index 0000000000000000000000000000000000000000..909c09e0cbf5ccf1b361d16ff5dcdd73c14f6a69 --- /dev/null +++ b/src/docs/chapter/user/50_ProB2/ZZ_section_footer.adoc @@ -0,0 +1,2 @@ + +:leveloffset: -1 diff --git a/src/docs/chapter/user/51_JavaFX/00_section_header.adoc b/src/docs/chapter/user/51_JavaFX/00_section_header.adoc new file mode 100644 index 0000000000000000000000000000000000000000..ee6bdf7147857ce531662c800212868baaf30e68 --- /dev/null +++ b/src/docs/chapter/user/51_JavaFX/00_section_header.adoc @@ -0,0 +1,4 @@ + +[[prob-2.0-javafx-ui]] += ProB 2.0 JavaFX UI +:leveloffset: +1 diff --git a/src/docs/chapter/user/50_ProB2/JavaFX/01_ProB2_JavaFX_UI.adoc b/src/docs/chapter/user/51_JavaFX/01_ProB2_JavaFX_UI.adoc similarity index 93% rename from src/docs/chapter/user/50_ProB2/JavaFX/01_ProB2_JavaFX_UI.adoc rename to src/docs/chapter/user/51_JavaFX/01_ProB2_JavaFX_UI.adoc index 8c4eff89d50e680fb96ee7656de911500f8560bc..90bc3607898a449809f697da6e509ee8eaf98c38 100644 --- a/src/docs/chapter/user/50_ProB2/JavaFX/01_ProB2_JavaFX_UI.adoc +++ b/src/docs/chapter/user/51_JavaFX/01_ProB2_JavaFX_UI.adoc @@ -1,11 +1,11 @@ -[[prob2-javafx-ui]] -== ProB 2.0 JavaFX UI +[[beta-version-download]] += Beta Version Download * A beta version of this new UI is available at https://www3.hhu.de/stups/downloads/prob2/[https://www3.hhu.de/stups/downloads/prob2/]. [[the-prob2-javafx-main-window]] -=== The ProB2 JavaFX Main Window +== The ProB2 JavaFX Main Window By default the main window is split into three vertical panes (see below). @@ -25,12 +25,12 @@ activate: image::ProB2JavaFX_UI_Overview.png[] [[the-prob2-javafx-main-menu-bar]] -=== The ProB2 JavaFX Main Menu Bar +== The ProB2 JavaFX Main Menu Bar The menu bar contains the various commands to access the features of ProB. It includes the following menus: -==== File +=== File image::File.png[] @@ -39,7 +39,7 @@ Project, open an existing project or a machine, open recent projects shown as list and/or clear the list of recent projects, close the ProB2 JavaFX UI, save your project or reload the currently running machine. -==== Edit +=== Edit image::Edit.png[] @@ -48,20 +48,20 @@ current machine (either in the editor provided by the ProB2 JavaFX UI or in the your operating systems standard editor) and allows to edit your general and global preferences by opening a seperate window. -==== Formula +=== Formula image::Formula.png[] Here you can add formulas for visualization and open the history chart window. -==== Consoles +=== Consoles image::Consoles.png[] This submenu leads to two consoles, one Groovy, one B. -==== Perspectives +=== Perspectives image::Perspectives.png[] @@ -73,13 +73,13 @@ windows. _Load_ allows you to make your own perspective by providing an FXML file containing the views but be aware that this might ruin the ability to detach components. -==== View +=== View image::View.png[] This submenu allows you to adjust font and button size in the ProB2 JavaFX UI. -==== Help +=== Help image::Help.png[] diff --git a/src/docs/chapter/user/50_ProB2/JavaFX/11_History_View.adoc b/src/docs/chapter/user/51_JavaFX/11_History_View.adoc similarity index 97% rename from src/docs/chapter/user/50_ProB2/JavaFX/11_History_View.adoc rename to src/docs/chapter/user/51_JavaFX/11_History_View.adoc index 7eabba273e0339bb4155b9b6f043dfd8e464148f..97f456ceabbf86e4395cf63b3df280f4361ad678 100644 --- a/src/docs/chapter/user/50_ProB2/JavaFX/11_History_View.adoc +++ b/src/docs/chapter/user/51_JavaFX/11_History_View.adoc @@ -1,5 +1,6 @@ + [[javafx-history-view]] -== History View += History View image::History.png[] diff --git a/src/docs/chapter/user/50_ProB2/JavaFX/12_Project_View.adoc b/src/docs/chapter/user/51_JavaFX/12_Project_View.adoc similarity index 95% rename from src/docs/chapter/user/50_ProB2/JavaFX/12_Project_View.adoc rename to src/docs/chapter/user/51_JavaFX/12_Project_View.adoc index e946856208976c17a7bada28ab6feed181b47a00..ac1820b50859069c1a28b01ba6eabd14bcc961af 100644 --- a/src/docs/chapter/user/50_ProB2/JavaFX/12_Project_View.adoc +++ b/src/docs/chapter/user/51_JavaFX/12_Project_View.adoc @@ -1,5 +1,6 @@ + [[javafx-project-view]] -== Project View += Project View If no machine or no project has been opened, the Project View will allow you to create a project. If you choose to open a machine without having @@ -15,7 +16,7 @@ The Project View contains several tabs: (each pair has its own entry) [[javafx-project-tab]] -=== Project Tab +== Project Tab image::Project_Tab.png[] @@ -25,7 +26,7 @@ opening a machine or chosen by the user who manually created the project and can be changed by double clicking on each respectively. [[javafx-machines-tab]] -=== Machines Tab +== Machines Tab image::Machines_Tab.png[] @@ -35,7 +36,7 @@ the project. By clicking right on a specific machine this machine can be edited or removed from the project. [[javafx-verifications-tab]] -=== Verifications Tab +== Verifications Tab image::Verifications_Tab.png[] This tab shows the status of each type of verification run on the machines contained by the project. If no test @@ -45,7 +46,7 @@ green check will be displayed. If a test failed, a red x sign will be shown. [[javafx-preferences-tab]] -=== Preferences Tab +== Preferences Tab image::Preferences_Tab.png[] @@ -59,7 +60,7 @@ image::Add_Preference.png[] The screenshot above shows the window for adding and editing preferences. [[javafx-run-configurations-tab]] -=== Run Configurations Tab +== Run Configurations Tab image::Runconfigurations_Tab.png[] diff --git a/src/docs/chapter/user/50_ProB2/JavaFX/13_Verification_View.adoc b/src/docs/chapter/user/51_JavaFX/13_Verification_View.adoc similarity index 92% rename from src/docs/chapter/user/50_ProB2/JavaFX/13_Verification_View.adoc rename to src/docs/chapter/user/51_JavaFX/13_Verification_View.adoc index 6a557e41ab0a3ad846b99b2edb763c26696f10d4..6f88c4e5b1200c35fa85f4e7a528d0456ec168b2 100644 --- a/src/docs/chapter/user/50_ProB2/JavaFX/13_Verification_View.adoc +++ b/src/docs/chapter/user/51_JavaFX/13_Verification_View.adoc @@ -1,5 +1,6 @@ + [[javafx-verification-view]] -== Verification View += Verification View The Verification View provides 3 different methods to test a machine: @@ -12,7 +13,7 @@ machine and interrupt the checking process by pressing the "Cancel" button. [[javafx-modelchecking]] -=== Modelchecking +== Modelchecking image::Modelchecking.png[] @@ -28,7 +29,7 @@ By pushing the `Model Check` button your selected variant will be added to the list shown at the top of the Modelchecking Tab. [[javafx-ltl-verifications]] -=== LTL Verifications +== LTL Verifications image::LTL.png[] @@ -37,7 +38,7 @@ Pattern` buttons an editor for each respectively will be opened and you can add LTL formulas or patterns to the lists to be checked for. [[javafx-constraint-based-checking]] -=== Constraint Based Checking +== Constraint Based Checking image::CBC.png[] diff --git a/src/docs/chapter/user/50_ProB2/JavaFX/14_Statistics_View.adoc b/src/docs/chapter/user/51_JavaFX/14_Statistics_View.adoc similarity index 93% rename from src/docs/chapter/user/50_ProB2/JavaFX/14_Statistics_View.adoc rename to src/docs/chapter/user/51_JavaFX/14_Statistics_View.adoc index 2f49b23d465995bda9dc4f13786b3c70850f82ef..5525b4ce42420c2d06d80c48355fd12d9a5b53f8 100644 --- a/src/docs/chapter/user/50_ProB2/JavaFX/14_Statistics_View.adoc +++ b/src/docs/chapter/user/51_JavaFX/14_Statistics_View.adoc @@ -1,5 +1,6 @@ + [[javafx-statistics-view]] -== Statistics View += Statistics View The Statistics View provides some state and transition data: The main view shows the quantity of processed states and total transitions, the diff --git a/src/docs/chapter/user/51_JavaFX/ZZ_section_footer.adoc b/src/docs/chapter/user/51_JavaFX/ZZ_section_footer.adoc new file mode 100644 index 0000000000000000000000000000000000000000..909c09e0cbf5ccf1b361d16ff5dcdd73c14f6a69 --- /dev/null +++ b/src/docs/chapter/user/51_JavaFX/ZZ_section_footer.adoc @@ -0,0 +1,2 @@ + +:leveloffset: -1 diff --git a/src/docs/chapter/developer/20_prolog/00_section_header.adoc b/src/docs/chapter/user/52_Prolog/00_section_header.adoc similarity index 61% rename from src/docs/chapter/developer/20_prolog/00_section_header.adoc rename to src/docs/chapter/user/52_Prolog/00_section_header.adoc index a6ef14638b32375f0c4263d66a6ce723019a2aec..c51697cc4f0510d693709e704fde40f2769e7638 100644 --- a/src/docs/chapter/developer/20_prolog/00_section_header.adoc +++ b/src/docs/chapter/user/52_Prolog/00_section_header.adoc @@ -1,2 +1,4 @@ + +[[prob-prolog-guide]] = ProB Prolog Guide :leveloffset: +1 diff --git a/src/docs/chapter/developer/20_prolog/Organization_of_ProB_Sources.adoc b/src/docs/chapter/user/52_Prolog/Organization_of_ProB_Sources.adoc similarity index 98% rename from src/docs/chapter/developer/20_prolog/Organization_of_ProB_Sources.adoc rename to src/docs/chapter/user/52_Prolog/Organization_of_ProB_Sources.adoc index 7ad66470cd7b98ff18d671928a52b9d5a28a1960..c38d374e956273fba47cb1e57e8d68b4ceaa1fde 100644 --- a/src/docs/chapter/developer/20_prolog/Organization_of_ProB_Sources.adoc +++ b/src/docs/chapter/user/52_Prolog/Organization_of_ProB_Sources.adoc @@ -1,3 +1,4 @@ + [[organization-of-prob-sources]] = Organization of ProB Sources diff --git a/src/docs/chapter/developer/20_prolog/ProB's_Prolog_Datastructures.adoc b/src/docs/chapter/user/52_Prolog/ProB's_Prolog_Datastructures.adoc similarity index 99% rename from src/docs/chapter/developer/20_prolog/ProB's_Prolog_Datastructures.adoc rename to src/docs/chapter/user/52_Prolog/ProB's_Prolog_Datastructures.adoc index a396eee0ebaa6b7b9e7548e0736ebcbfc250f8af..db586077738b7c7ef4d59e3176365ff92edc19de 100644 --- a/src/docs/chapter/developer/20_prolog/ProB's_Prolog_Datastructures.adoc +++ b/src/docs/chapter/user/52_Prolog/ProB's_Prolog_Datastructures.adoc @@ -1,3 +1,4 @@ + [[probs-prolog-datastructures]] = ProB's Prolog Datastructures diff --git a/src/docs/chapter/developer/20_prolog/Prolog_Coding_Guidelines.adoc b/src/docs/chapter/user/52_Prolog/Prolog_Coding_Guidelines.adoc similarity index 98% rename from src/docs/chapter/developer/20_prolog/Prolog_Coding_Guidelines.adoc rename to src/docs/chapter/user/52_Prolog/Prolog_Coding_Guidelines.adoc index 818ae06ba0a22d52ed25dd476a8d26cd04b620da..e88baad0b16d15fc2bd50e4b928419c6c16919a0 100644 --- a/src/docs/chapter/developer/20_prolog/Prolog_Coding_Guidelines.adoc +++ b/src/docs/chapter/user/52_Prolog/Prolog_Coding_Guidelines.adoc @@ -1,3 +1,4 @@ + [[prolog-coding-guidelines]] = Prolog Coding Guidelines @@ -97,7 +98,7 @@ especially when you only have one real commit. * avoid merge bombs with many changed files: a Git merge can hide unintended changes, e.g., accidentally reverting previous commits because of editor issues (editor out of sync with file system). * provide good commit messages. If a commit is related to a JIRA ticket -reference the identifier of the ticket in the commit message. +reference the identifier of the ticket in the commit message. https://chris.beams.io/posts/git-commit/[This web page] provides the following seven rules: * Separate subject from body with a blank line * Limit the subject line to 50 characters @@ -106,7 +107,7 @@ https://chris.beams.io/posts/git-commit/[This web page] provides the following s * Use the imperative mood in the subject line * Wrap the body at 72 characters * Use the body to explain what and why vs. how - + [[useful-bash-aliases]] Useful Bash Aliases diff --git a/src/docs/chapter/developer/20_prolog/Running_ProB_from_source.adoc b/src/docs/chapter/user/52_Prolog/Running_ProB_from_source.adoc similarity index 99% rename from src/docs/chapter/developer/20_prolog/Running_ProB_from_source.adoc rename to src/docs/chapter/user/52_Prolog/Running_ProB_from_source.adoc index a5385d79796d75618854f47a031f7995d585bbd0..53a6c930b2d3c7eef919696b218a90458ee3794b 100644 --- a/src/docs/chapter/developer/20_prolog/Running_ProB_from_source.adoc +++ b/src/docs/chapter/user/52_Prolog/Running_ProB_from_source.adoc @@ -1,3 +1,4 @@ + [[running-prob-from-source]] = Running ProB from source diff --git a/src/docs/chapter/developer/20_prolog/Why_Prolog.adoc b/src/docs/chapter/user/52_Prolog/Why_Prolog.adoc similarity index 99% rename from src/docs/chapter/developer/20_prolog/Why_Prolog.adoc rename to src/docs/chapter/user/52_Prolog/Why_Prolog.adoc index dacdfb8c2d593b23085c78c4bfefafd9c1b7b0f7..bbde80b8fefa321678957c857693bcc1a5da2059 100644 --- a/src/docs/chapter/developer/20_prolog/Why_Prolog.adoc +++ b/src/docs/chapter/user/52_Prolog/Why_Prolog.adoc @@ -1,5 +1,4 @@ - [[why-prolog]] = Why Prolog? diff --git a/src/docs/chapter/user/52_Prolog/ZZ_section_footer.adoc b/src/docs/chapter/user/52_Prolog/ZZ_section_footer.adoc new file mode 100644 index 0000000000000000000000000000000000000000..909c09e0cbf5ccf1b361d16ff5dcdd73c14f6a69 --- /dev/null +++ b/src/docs/chapter/user/52_Prolog/ZZ_section_footer.adoc @@ -0,0 +1,2 @@ + +:leveloffset: -1 diff --git a/src/docs/chapter/user/55_JavaAPI/00_JavaAPI.adoc b/src/docs/chapter/user/55_JavaAPI/00_JavaAPI.adoc deleted file mode 100644 index fef9815b962ab400b522f2448f9e50ec9337844f..0000000000000000000000000000000000000000 --- a/src/docs/chapter/user/55_JavaAPI/00_JavaAPI.adoc +++ /dev/null @@ -1,2 +0,0 @@ -[[prob-java-api]] -= ProB Java API diff --git a/src/docs/chapter/user/60_JavaAPI/00_section_header.adoc b/src/docs/chapter/user/60_JavaAPI/00_section_header.adoc new file mode 100644 index 0000000000000000000000000000000000000000..43a534483239e121953e8dd23ca590c772958d8d --- /dev/null +++ b/src/docs/chapter/user/60_JavaAPI/00_section_header.adoc @@ -0,0 +1,4 @@ + +[[prob2-java-api]] += ProB 2.0 Java API +:leveloffset: +1 diff --git a/src/docs/chapter/user/55_JavaAPI/01_ProB_Java_API.adoc b/src/docs/chapter/user/60_JavaAPI/01_ProB_Java_API.adoc similarity index 94% rename from src/docs/chapter/user/55_JavaAPI/01_ProB_Java_API.adoc rename to src/docs/chapter/user/60_JavaAPI/01_ProB_Java_API.adoc index 1e43835b90b42ed902477f15f1a81c9c29aecbf5..b17f1cc49e37184391ac2b8fb3f7f6c702f237de 100644 --- a/src/docs/chapter/user/55_JavaAPI/01_ProB_Java_API.adoc +++ b/src/docs/chapter/user/60_JavaAPI/01_ProB_Java_API.adoc @@ -1,14 +1,15 @@ + [[general-java-api]] -== General += General [[prob-java-api-documentation]] -=== Documentation +== Documentation * <<prob-java-api-tutorial,Tutorial>> * https://www3.hhu.de/stups/handbook/prob2/handbook.html[Developer Manual] -=== Additional Material +== Additional Material * <<prob2.0-development,ProB 2.0 Development>> * https://github.com/bendisposto/prob2_tooling_template[ProB 2.0 Tooling @@ -26,7 +27,7 @@ Tutorial Presentation>> * <<prob-2.0-within-rodin-and-a-html-visualization-example,ProB 2.0 within Rodin and a HTML Visualization Example>> -=== Download +== Download Nightly builds of ProB 2 for Rodin 3 can be obtained from within Rodin using the update site diff --git a/src/docs/chapter/user/55_JavaAPI/02_ProB_Java_API_Tutorial.adoc b/src/docs/chapter/user/60_JavaAPI/02_ProB_Java_API_Tutorial.adoc similarity index 94% rename from src/docs/chapter/user/55_JavaAPI/02_ProB_Java_API_Tutorial.adoc rename to src/docs/chapter/user/60_JavaAPI/02_ProB_Java_API_Tutorial.adoc index 2241dc7e50e4dbc17217630b27dc4a0fbaf56b8e..ef3480a01b148f0b55988f026f50499f30719e2f 100644 --- a/src/docs/chapter/user/55_JavaAPI/02_ProB_Java_API_Tutorial.adoc +++ b/src/docs/chapter/user/60_JavaAPI/02_ProB_Java_API_Tutorial.adoc @@ -1,5 +1,6 @@ + [[prob-java-api-tutorial]] -== ProB Java API Tutorial += ProB Java API Tutorial ProB 2.0 is currently experimental. This means that the implementation may change during the course of development. However, we have reached @@ -8,7 +9,7 @@ certain level of stability. Therefore, we are writing this tutorial to explain what those features are. [[how-to-get-started-developing-with-prob-2.0]] -=== How to get started developing with ProB 2.0 +== How to get started developing with ProB 2.0 The source code for ProB 2.0 is available via GitHub. Click https://github.com/bendisposto/prob2[here] to view the prob2 repository. @@ -20,7 +21,7 @@ can view the features that we are currently working on and can submit new feature requests. [[how-to-open-the-groovy-shell]] -=== How to open the Groovy Shell +== How to open the Groovy Shell The ProB Groovy shell is available in the Eclipse application. To open it, select @@ -34,7 +35,7 @@ Then select and hit `ok`. [[open-the-prob-api-from-sourcejar-file]] -=== Open the ProB API from Source/JAR file +== Open the ProB API from Source/JAR file In order to access the console from source or from a JAR file, start the application with the parameters -s (short for --shell) and -local (which @@ -46,10 +47,10 @@ can then be accessed at the following address: localhost:PORTNR/sessions/GroovyConsoleSession [[how-to-load-a-model]] -=== How to load a model +== How to load a model [[java-api-classical-b]] -==== Classical B +=== Classical B You can load a Classical B model into the groovy console using the `api` variable that is available. There is a method `b_load` that is available @@ -60,7 +61,7 @@ to load Classical B models. For example: will load example.mch into the variable `m`. [[java-api-event-b]] -==== Event B +=== Event B To load an Event B model into ProB, right click on the model and select @@ -73,12 +74,12 @@ command in the Api object. The eventb_load command accepts .bcm and .bcc files. [[how-to-animate-models]] -=== How to animate models +== How to animate models The Trace abstraction is available to carry out animations. [[in-the-console]] -==== In The Console +=== In The Console There are several different ways that a new transition can be added to the current trace. The most important thing to remember is that each @@ -141,7 +142,7 @@ Move forwards: `t = t.forward()` [[in-the-ui]] -==== In The UI +=== In The UI In order to animate a loaded model in the UI, double-click on an enabled event in the `Events` view. Then, the resulting trace will automatically @@ -150,7 +151,7 @@ move backwards and forwards in the trace, use the buttons in the upper right hand corner of the `Events` view. [[how-to-switch-from-ui-to-groovy-console]] -=== How to switch from UI to groovy console +== How to switch from UI to groovy console There is an easy way to switch from the UI to the groovy console and back. It all happens using the "animations" global variable in the @@ -158,7 +159,7 @@ groovy console. What is important to remember, is that in this case, there is no distinction between an animation and a trace. [[from-ui-to-console]] -==== From UI to Console +=== From UI to Console In the UI, switch to the `Current Animations` view. Here you can view the different animations that are available. If the desired animation is @@ -172,7 +173,7 @@ into the groovy console and the current animation will be loaded into the variable `x`. [[from-the-console-to-the-ui]] -==== From the Console to the UI +=== From the Console to the UI If you have a trace saved into variable `trace_0` in the groovy console, you can easily add it to the UI. Simply type @@ -183,7 +184,7 @@ into the groovy console and the trace will automatically be added to the list of current animations and all of the views will be updated. [[how-to-carry-out-evaluations]] -=== How to carry out evaluations +== How to carry out evaluations It is very simple to evaluate strings in the groovy console. There is a build in eval method in both the Trace and the StateSpace. In the trace, @@ -229,7 +230,7 @@ extract a StateId from a StateSpace, you can use the notation StateId that you want to view. [[how-to-convert-between-the-main-abstractions]] -=== How to convert between the main abstractions +== How to convert between the main abstractions There is a connection between all of the main abstractions. You can easily convert between them by using the `as` operator. @@ -266,7 +267,7 @@ StateSpace or Model to a Trace, a new trace from the root state is created. [[how-to-save-a-trace]] -=== How to save a trace +== How to save a trace ProB currently supports a mechanism to save a trace in a script so that the same trace can be recreated. We are currently working on some @@ -304,7 +305,7 @@ TraceConverter `trace = TraceConverter.restore(modelForThisTrace,"/pathToFile/fileName.xml")` [[how-to-run-a-groovy-script]] -=== How to run a groovy script +== How to run a groovy script You can use the build in `run` command to run a groovy script. Simply type @@ -314,7 +315,7 @@ type into the console. [[how-to-animate-with-only-the-statespace-abstraction]] -=== How to animate with only the StateSpace abstraction +== How to animate with only the StateSpace abstraction It is also possible to carry out animations without using a trace object. @@ -335,7 +336,7 @@ the event. If there are no parameters, the predicate "TRUE = TRUE" will automatically be added. [[how-to-use-a-different-probcli-binary-for-prob2]] -=== How to use a different probcli binary for ProB2 +== How to use a different probcli binary for ProB2 You need to start ProB2 or the respective Java application with: diff --git a/src/docs/chapter/user/55_JavaAPI/10_Programmatic_Abstractions_in_the_ProB_2.0_API.adoc b/src/docs/chapter/user/60_JavaAPI/10_Programmatic_Abstractions_in_the_ProB_2.0_API.adoc similarity index 96% rename from src/docs/chapter/user/55_JavaAPI/10_Programmatic_Abstractions_in_the_ProB_2.0_API.adoc rename to src/docs/chapter/user/60_JavaAPI/10_Programmatic_Abstractions_in_the_ProB_2.0_API.adoc index ba955b876f325a26837af7117aa432717a0d849c..fcca19257dc86b0d78c16502319f7026a90e6b9d 100644 --- a/src/docs/chapter/user/55_JavaAPI/10_Programmatic_Abstractions_in_the_ProB_2.0_API.adoc +++ b/src/docs/chapter/user/60_JavaAPI/10_Programmatic_Abstractions_in_the_ProB_2.0_API.adoc @@ -1,11 +1,12 @@ + [[programmatic-abstractions-in-prob-api]] -== Programmatic Abstraction in the ProB 2.0 API += Programmatic Abstraction in the ProB 2.0 API [[overview-programmatic-abstractions-in-prob-api]] -=== Overview +== Overview [[background]] -==== Background +=== Background The original ProB plug-in for Rodin introduced one basic abstraction: developers can create Java commands specifying calculations that are to @@ -14,7 +15,7 @@ can then be interpreted and manipulated by the developer. Each Java command corresponds to one prolog instruction in the ProB kernel. [[current-implementation]] -==== Current Implementation +=== Current Implementation We have maintained the abstractions of the commands in order to communicate with the ProB kernel. However, as we were considering how @@ -24,7 +25,7 @@ Therefore, we created the programmatic abstractions that will be described in the following sections. [[java-api-model]] -=== Model +== Model The Model is an abstraction that provides static information about the current model that is being animated or checked. For Classical B and @@ -45,7 +46,7 @@ information about the model. TLA+ specifications can be represented in the API as Classical B models. [[java-api-statespace]] -=== StateSpace +== StateSpace There is a one-to-one relationship between a StateSpace and a model. The StateSpace is the corresponding label transition system for a particular @@ -65,7 +66,7 @@ not accessed for a given period of time, the garbage collector can clean them up. [[java-api-trace]] -=== Trace +== Trace For some tools, the StateSpace abstraction may be sufficient. But when it comes to animation and the concept of a "current state", a further diff --git a/src/docs/chapter/user/55_JavaAPI/20_Rodin_User_and_Developer_Workshop_2013_-_Tutorial.adoc b/src/docs/chapter/user/60_JavaAPI/20_Rodin_User_and_Developer_Workshop_2013_-_Tutorial.adoc similarity index 98% rename from src/docs/chapter/user/55_JavaAPI/20_Rodin_User_and_Developer_Workshop_2013_-_Tutorial.adoc rename to src/docs/chapter/user/60_JavaAPI/20_Rodin_User_and_Developer_Workshop_2013_-_Tutorial.adoc index 48f121ba1ee3501a1442d1ffe62298479f3c4279..9ac986f3d215418c2c3df619fd8d9cbe90ab7c59 100644 --- a/src/docs/chapter/user/55_JavaAPI/20_Rodin_User_and_Developer_Workshop_2013_-_Tutorial.adoc +++ b/src/docs/chapter/user/60_JavaAPI/20_Rodin_User_and_Developer_Workshop_2013_-_Tutorial.adoc @@ -1,5 +1,6 @@ + [[rodin-user-and-developer-workshop-2013]] -== Rodin User and Developer Workshop 2013 += Rodin User and Developer Workshop 2013 Here are the information we have shown you at the tutorial. If you want to follow this tutorial on your computer you will have to install ProB @@ -11,7 +12,7 @@ This page was updated in May of 2015 to reflect changes made to the ProB 2.0 API. [[java-api-setup]] -=== Setup +== Setup You will need a fresh copy of ProB 2.0 installed to your Rodin or the sourcecode. @@ -31,7 +32,7 @@ snippets. We assume that you execute all the code snippets. Some of the snippets rely on the previous execution of other snippets. [[java-api-preparation]] -=== Preparation +== Preparation 1. Import the Scheduler project. 2. Start an animation for Scheduler0 @@ -43,7 +44,7 @@ variable. space that is associated with `trace` [[java-api-the-model]] -=== The Model +== The Model A model gives you access to the static properties of a Rodin development. Such as contexts, machines, constants, variables, @@ -87,7 +88,7 @@ access to axioms, constants and sets. Let's explore machines. `ne.getGuards()` [[java-api-the-state-space]] -=== The State Space +== The State Space The state space represents the whole currently known world for an @@ -183,7 +184,7 @@ run it at the beginning. `run new File("myAwesomeScript.groovy")` [[java-api-traces]] -=== Traces +== Traces A trace represents a path through the state space. It can move forward and backward through the Trace and can be extended with a new @@ -231,7 +232,7 @@ decision in the past, the trace drops the future. It behaves in the same way your browser history does. [[java-api-evaluation]] -=== Evaluation +== Evaluation Evaluation is done by passing an instance of the interface IEvalElement to an evaluator. Each formalism has its own descendant of IEvalElement. @@ -304,7 +305,7 @@ of predicates into a conjunction. In Groovy collect means map and inject means reduce. [[java-api-constraint-solver]] -=== Constraint solver +== Constraint solver *Evaluation is fine, but can I use ProB's solver?* @@ -349,7 +350,7 @@ cbc_solve(s, i & i.implies(g)) .... [[java-api-notification-and-ui-access]] -=== Notification and UI Access +== Notification and UI Access Clients can register themself to receive a notification if an animation step occured, new states were discovered or the model has changed. The @@ -382,6 +383,6 @@ in the future to something more meaningful, e.g., loader. `animations.addNewAnimation(t)` [[java-api-additional-resources]] -=== Additional Resources +== Additional Resources Further information can be found in the ProB Developer_Manual. diff --git a/src/docs/chapter/user/60_JavaAPI/ZZ_section_footer.adoc b/src/docs/chapter/user/60_JavaAPI/ZZ_section_footer.adoc new file mode 100644 index 0000000000000000000000000000000000000000..909c09e0cbf5ccf1b361d16ff5dcdd73c14f6a69 --- /dev/null +++ b/src/docs/chapter/user/60_JavaAPI/ZZ_section_footer.adoc @@ -0,0 +1,2 @@ + +:leveloffset: -1 diff --git a/src/docs/chapter/developer/10_java_api/00_section_header.adoc b/src/docs/chapter/user/65_Java_2-0_API/00_section_header.adoc similarity index 98% rename from src/docs/chapter/developer/10_java_api/00_section_header.adoc rename to src/docs/chapter/user/65_Java_2-0_API/00_section_header.adoc index 572c6826baeb11ab7cb249780ff930f69b3345c3..ec4a27c279dda233b2b20220fb27cc2f7434e492 100644 --- a/src/docs/chapter/developer/10_java_api/00_section_header.adoc +++ b/src/docs/chapter/user/65_Java_2-0_API/00_section_header.adoc @@ -1,3 +1,4 @@ + [[developer-prob-java-api]] = ProB 2.0 Java API :leveloffset: +1 diff --git a/src/docs/chapter/developer/10_java_api/01_introduction.adoc b/src/docs/chapter/user/65_Java_2-0_API/01_introduction.adoc similarity index 99% rename from src/docs/chapter/developer/10_java_api/01_introduction.adoc rename to src/docs/chapter/user/65_Java_2-0_API/01_introduction.adoc index 32300983386c2f2aba30d8bee22318ec85ddc9f3..0e9932178d32c23898945cf2000c890ca6d19fe0 100644 --- a/src/docs/chapter/developer/10_java_api/01_introduction.adoc +++ b/src/docs/chapter/user/65_Java_2-0_API/01_introduction.adoc @@ -1,3 +1,4 @@ + [[developer-introduction]] = Introduction diff --git a/src/docs/chapter/developer/10_java_api/02_architecture.adoc b/src/docs/chapter/user/65_Java_2-0_API/02_architecture.adoc similarity index 98% rename from src/docs/chapter/developer/10_java_api/02_architecture.adoc rename to src/docs/chapter/user/65_Java_2-0_API/02_architecture.adoc index db0d731ae67442876190cf2cfbbeb9f6f3e31540..b43f74b11d1dcb95a7ad67bbcdd232f44f4f5646 100644 --- a/src/docs/chapter/developer/10_java_api/02_architecture.adoc +++ b/src/docs/chapter/user/65_Java_2-0_API/02_architecture.adoc @@ -1,3 +1,5 @@ + +[[developer-architecture]] = Architecture In this chapter we will give an overview of the tool's architecture. First we will explain the base components and then we will explain how these components interact with each other. diff --git a/src/docs/chapter/developer/10_java_api/03_installation.adoc b/src/docs/chapter/user/65_Java_2-0_API/03_installation.adoc similarity index 96% rename from src/docs/chapter/developer/10_java_api/03_installation.adoc rename to src/docs/chapter/user/65_Java_2-0_API/03_installation.adoc index 243412bc764c12a92d11b6e8b1195eb3c435b878..fc215cfc86f15cc67a134bdfac81c7dffda99fc6 100644 --- a/src/docs/chapter/developer/10_java_api/03_installation.adoc +++ b/src/docs/chapter/user/65_Java_2-0_API/03_installation.adoc @@ -1,3 +1,5 @@ + +[[developer-installation]] = Installation You can use the ProB 2.0 archive. diff --git a/src/docs/chapter/developer/10_java_api/04_lowlevelapi.adoc b/src/docs/chapter/user/65_Java_2-0_API/04_lowlevelapi.adoc similarity index 99% rename from src/docs/chapter/developer/10_java_api/04_lowlevelapi.adoc rename to src/docs/chapter/user/65_Java_2-0_API/04_lowlevelapi.adoc index 1e22bce075c8e9a30cf4b22d78610dc5a9330d02..91f0bffe7baecc1b2d0a3c9b4bc173571d74fa64 100644 --- a/src/docs/chapter/developer/10_java_api/04_lowlevelapi.adoc +++ b/src/docs/chapter/user/65_Java_2-0_API/04_lowlevelapi.adoc @@ -1,3 +1,5 @@ + +[[developer-low-level-api]] = Low Level API The ProB core has two different APIs. One is suited for high level usage and one directly interacts with the Prolog binary. The latter (low level) API is used to extend the functionality of ProB 2.0 and this is the API that we are introducing in this chapter. It is typically only used within the development team because it often requires changing parts of the Prolog kernel. However, it still may be useful to know where one can look for low level features. This is particulary helpful when some of the features are not yet accessible to a higher level API. diff --git a/src/docs/chapter/developer/10_java_api/05_probcore.adoc b/src/docs/chapter/user/65_Java_2-0_API/05_probcore.adoc similarity index 99% rename from src/docs/chapter/developer/10_java_api/05_probcore.adoc rename to src/docs/chapter/user/65_Java_2-0_API/05_probcore.adoc index 2ab98c18162eb9e4a89661c70b1afb602e570da2..94167695dce63cfd05e61f1eef799b5421659312 100644 --- a/src/docs/chapter/developer/10_java_api/05_probcore.adoc +++ b/src/docs/chapter/user/65_Java_2-0_API/05_probcore.adoc @@ -1,3 +1,5 @@ + +[[developer-high-level-api]] = High Level API We have introduced a high level API in ProB 2.0 which allows much nicer interaction with ProB. Before 2.0, all interaction was done using commands. There were no abstractions that represent typically used concepts such as a model, a state space, or a trace. Together with this high level API, we introduced a scripting interface that makes it very easy to tweak ProB and implement new features. Almost everything in ProB can be manipulated through Groovy scripts. This chapter will introduce the programmatic abstractions now available in ProB 2.0, and will briefly describe their function. Later chapters will cover in greater depth how to use the abstractions. <<animation>> covers the topic of animation, and <<evaluation>> discusses how to evaluate formulas using the API. In the following sections we will introduce the main abstractions that are available in ProB 2.0, that is, the model, state space and trace abstractions. diff --git a/src/docs/chapter/developer/10_java_api/06_animation.adoc b/src/docs/chapter/user/65_Java_2-0_API/06_animation.adoc similarity index 99% rename from src/docs/chapter/developer/10_java_api/06_animation.adoc rename to src/docs/chapter/user/65_Java_2-0_API/06_animation.adoc index 0408aaf140ca1957c2355502b13976562b02ca96..2772f4218ca730797015185b6a2628a3a24ee5b8 100644 --- a/src/docs/chapter/developer/10_java_api/06_animation.adoc +++ b/src/docs/chapter/user/65_Java_2-0_API/06_animation.adoc @@ -1,3 +1,5 @@ + +[[developer-animation]] = Animation It is possible for the user to perform animation manually using the state and transition abstractions, or to use the trace abstraction which allows the user access to previously executed transitions, and the ability to move within the trace. This chapter will describe in detail all of the different ways that it is possible to perform animation using the provided abstractions. diff --git a/src/docs/chapter/developer/10_java_api/07_evaluation.adoc b/src/docs/chapter/user/65_Java_2-0_API/07_evaluation.adoc similarity index 99% rename from src/docs/chapter/developer/10_java_api/07_evaluation.adoc rename to src/docs/chapter/user/65_Java_2-0_API/07_evaluation.adoc index 1eb2e43ac491ebf405dcae1a1174498a045bafe7..8c6af3f92f9c5c8f2457539bd7eacfa845fee07d 100644 --- a/src/docs/chapter/developer/10_java_api/07_evaluation.adoc +++ b/src/docs/chapter/user/65_Java_2-0_API/07_evaluation.adoc @@ -1,3 +1,5 @@ + +[[developer-evaluation-and-constraint-solving]] = Evaluation and Constraint Solving This chapter will demonstrate how we evaluate formulas in the context of a formal model. It also demonstrates how we can use ProB's constraint solver. diff --git a/src/docs/chapter/developer/10_java_api/08_cosimulation.adoc b/src/docs/chapter/user/65_Java_2-0_API/08_cosimulation.adoc similarity index 97% rename from src/docs/chapter/developer/10_java_api/08_cosimulation.adoc rename to src/docs/chapter/user/65_Java_2-0_API/08_cosimulation.adoc index 725dc608128338caeec1fcd966ad2faef2beec74..6c08fd7e1659deaa4f619ca94fa57cbee89c0929 100644 --- a/src/docs/chapter/developer/10_java_api/08_cosimulation.adoc +++ b/src/docs/chapter/user/65_Java_2-0_API/08_cosimulation.adoc @@ -1,3 +1,5 @@ + +[[co-simulation]] = Co-Simulation ProB 2.0 contains some classes for cosimulating discrete models specified in one of the formalisms that are supported by ProB, and continuous models that are implemented using the https://fmi-standard.org/[functional mockup interface] standard. A so called functional mockup unit (FMU) can, for example, be created in C using the FMI SDK or exported from third party tools such as Dymola. The framework is built on top of https://ptolemy.berkeley.edu/java/jfmi//[JFMI] from the Ptolemy Project. In fact, we only added a thin wrapper on top of the JFMI library. diff --git a/src/docs/chapter/developer/10_java_api/09_dependencyinjection.adoc b/src/docs/chapter/user/65_Java_2-0_API/09_dependencyinjection.adoc similarity index 99% rename from src/docs/chapter/developer/10_java_api/09_dependencyinjection.adoc rename to src/docs/chapter/user/65_Java_2-0_API/09_dependencyinjection.adoc index dec1dbd0512743cb6e24cdced76e8aff4bb9957c..3ed8328d2074fb2324e45d352bb9c9d171233c8d 100644 --- a/src/docs/chapter/developer/10_java_api/09_dependencyinjection.adoc +++ b/src/docs/chapter/user/65_Java_2-0_API/09_dependencyinjection.adoc @@ -1,3 +1,5 @@ + +[[dependency-injection]] = Dependency Injection We have decided to use the Guice framework for dependency injection. Although this is just an implementation detail it is important to get a basic understanding of how it works and why we use it in order to build tools on top of ProB 2.0. A more complete introduction to dependency injection and the Guice framework can be found in cite:[Prasanna:2009:DI:1795686] and https://github.com/google/guice[the Guice website]. diff --git a/src/docs/chapter/user/65_Java_2-0_API/ZZ_section_footer.adoc b/src/docs/chapter/user/65_Java_2-0_API/ZZ_section_footer.adoc new file mode 100644 index 0000000000000000000000000000000000000000..909c09e0cbf5ccf1b361d16ff5dcdd73c14f6a69 --- /dev/null +++ b/src/docs/chapter/user/65_Java_2-0_API/ZZ_section_footer.adoc @@ -0,0 +1,2 @@ + +:leveloffset: -1 diff --git a/src/docs/chapter/user/70_TclTk/00_section_header.adoc b/src/docs/chapter/user/70_TclTk/00_section_header.adoc new file mode 100644 index 0000000000000000000000000000000000000000..c68e1ae467eca1deb650d654d0f74563412f8bac --- /dev/null +++ b/src/docs/chapter/user/70_TclTk/00_section_header.adoc @@ -0,0 +1,4 @@ + +[[tcltk]] += Tcl/Tk +:leveloffset: +1 diff --git a/src/docs/chapter/developer/30_tcltk/Tk_Architecture.adoc b/src/docs/chapter/user/70_TclTk/Tk_Architecture.adoc similarity index 100% rename from src/docs/chapter/developer/30_tcltk/Tk_Architecture.adoc rename to src/docs/chapter/user/70_TclTk/Tk_Architecture.adoc diff --git a/src/docs/chapter/user/70_TclTk/ZZ_section_footer.adoc b/src/docs/chapter/user/70_TclTk/ZZ_section_footer.adoc new file mode 100644 index 0000000000000000000000000000000000000000..909c09e0cbf5ccf1b361d16ff5dcdd73c14f6a69 --- /dev/null +++ b/src/docs/chapter/user/70_TclTk/ZZ_section_footer.adoc @@ -0,0 +1,2 @@ + +:leveloffset: -1 diff --git a/src/docs/chapter/user/YZ_Tutorials/00_section_header.adoc b/src/docs/chapter/user/YZ_Tutorials/00_section_header.adoc new file mode 100644 index 0000000000000000000000000000000000000000..0afe68c34c6249ee55fded13f2eb38b61530b951 --- /dev/null +++ b/src/docs/chapter/user/YZ_Tutorials/00_section_header.adoc @@ -0,0 +1,4 @@ + +[[tutorials]] += Tutorials +:leveloffset: +1 diff --git a/src/docs/chapter/user/10_General/Tutorial_Animation_Tips.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Animation_Tips.adoc similarity index 93% rename from src/docs/chapter/user/10_General/Tutorial_Animation_Tips.adoc rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Animation_Tips.adoc index e2eca0051f6a77f0128b12b69b8c8a2981629ee9..f0d880821bcc79d5ef38f6324faeb1211a073a50 100644 --- a/src/docs/chapter/user/10_General/Tutorial_Animation_Tips.adoc +++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Animation_Tips.adoc @@ -1,12 +1,13 @@ + [[tutorial-animation-tips]] -== Tutorial Animation Tips += Tutorial Animation Tips Make sure you have the Lift.mch model from the first part of the tutorial: <<tutorial-first-step,Starting ProB and first animation steps>>. [[operation-with-many-solutions-for-the-parameters]] -=== Operation with many solutions for the parameters +== Operation with many solutions for the parameters Add the following operation to the Lift model: @@ -27,7 +28,7 @@ all possible parameter values for the operations were computed. There are several solutions to overcome this. [[increasing-max_operations]] -==== Increasing MAX_OPERATIONS +=== Increasing MAX_OPERATIONS First, you could increase the "MAX_OPERATIONS" preference of ProB by selecting the "Animation Preferences" command in the _Preferences_ @@ -41,7 +42,7 @@ the B machine. image::ProB_Lift_OpPane_WithJump101.png[] [[executing-an-operation-by-predicate]] -==== Executing an Operation by Predicate +=== Executing an Operation by Predicate The alternative is to provide the parameter value for `level` yourself. For this, select the "Execute an Operation..." command in the _Animate_ @@ -71,7 +72,7 @@ value `98` for level. When there are multiple solutions, ProB will only execute the operation for the first solution found. [[using-random-enumeration]] -==== Using Random enumeration +=== Using Random enumeration You can also tell ProB to try and perform random enumerations. This feature is available in ProB 1.5.0 or newer. You add the following lines @@ -87,10 +88,10 @@ you should see a picture similar to the following one: image::ProB_Lift_Randomise.png[] [[using-constraint-based-validation-techniques]] -==== Using Constraint-Based Validation Techniques +=== Using Constraint-Based Validation Techniques [[find-sequence]] -===== Find Sequence +==== Find Sequence You can also use the constraint solver to construct sequences which are of interest to you. Let us add the following operation to the lift @@ -119,7 +120,7 @@ it: image::FindSequenceResult.png[] [[constraint-based-model-based-testing]] -===== Constraint-Based Model-Based Testing +==== Constraint-Based Model-Based Testing Alternatively, you could for example use the constraint-based test-case generator to find for every operation the shortest trace that enables diff --git a/src/docs/chapter/user/30_OtherLanguages/CSP/04_Tutorial_CSP_First_Step.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_CSP_First_Step.adoc similarity index 96% rename from src/docs/chapter/user/30_OtherLanguages/CSP/04_Tutorial_CSP_First_Step.adoc rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_CSP_First_Step.adoc index e500f9d2ea54ec2fba6c4b5c928e7476f0abe0bb..99becf315c3bba35ff583e225e8d94869ddd5e6c 100644 --- a/src/docs/chapter/user/30_OtherLanguages/CSP/04_Tutorial_CSP_First_Step.adoc +++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_CSP_First_Step.adoc @@ -1,12 +1,11 @@ - [[tutorial-csp-first-step]] -=== Tutorial CSP First Step += Tutorial CSP First Step [Category:User Manual] [[startup]] -==== Startup +== Startup Start off by installing the standalone Tcl/Tk version of ProB. Follow the instructions in <<installation,Installation>>. Start ProB by @@ -14,7 +13,7 @@ double-clicking on `ProBWin` (for Windows users), or by launching `StartProB.sh` from a Terminal (for Linux and Mac users). [[loading-a-first-csp-specification]] -==== Loading a first CSP specification +== Loading a first CSP specification Use the "Open..." command in the _File_ menu and then navigate to the "Examples" directory that came with your ProB installation. Inside @@ -24,7 +23,7 @@ ProB window should now look as follows: image::ProB_BusesAfterLoad.png[] [[first-steps-in-animation-csp]] -==== First Steps in Animation +== First Steps in Animation We have now loaded a first simple CSP model. Let us look at the contents of the ProB window (ignoring the menu bar). @@ -71,7 +70,7 @@ source locations). The source highlighting should look as follows: image::ProB_CSPAfterBoardSingleClick.png[] [[first-steps-in-model-checking]] -==== First Steps in Model Checking +== First Steps in Model Checking You can use the model checker to search for certain errors. Execute the "Model Check..." command in the _Verify_ menu. The following dialog @@ -91,7 +90,7 @@ insert the counter-example into the history as follows: image::ProB_CSPAfterModelCheck.png[] [[error-highlighting]] -==== Error Highlighting +== Error Highlighting Now edit the definition of the BUS37 process and add an illegal output of value 1 on the alight37B channel: @@ -116,7 +115,7 @@ error location in the source as follows: image::ProB_CSPAfterModelCheck2.png[] [[other-features]] -==== Other Features +== Other Features You can check more sophisticated temporal properties using the LTL model checker of ProB; see the <<ltl-model-checking,corresponding part of diff --git a/src/docs/chapter/user/40_AdvancedFeatures/10_Tutorials/Tutorial_Co-Simulation.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Co-Simulation.adoc similarity index 96% rename from src/docs/chapter/user/40_AdvancedFeatures/10_Tutorials/Tutorial_Co-Simulation.adoc rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Co-Simulation.adoc index e354cdc8996063eebdffe79cd5ac851f913a3f4d..d61c5ada65520f5c3908c3ef9c90d5533073fdb9 100644 --- a/src/docs/chapter/user/40_AdvancedFeatures/10_Tutorials/Tutorial_Co-Simulation.adoc +++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Co-Simulation.adoc @@ -1,10 +1,11 @@ + [[tutorial-co-simulation]] -== Tutorial Co-Simulation += Tutorial Co-Simulation You can create Co-Simulations using FMI with ProB. [[overview-tutorial-co-simulation]] -=== Overview +== Overview The ProB 2.0 Java API contains some classes for cosimulating discrete models specified in one of the formalisms that are supported by ProB, diff --git a/src/docs/chapter/user/20_Validation/MC/Tutorial_Complete_Model_Checking.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Complete_Model_Checking.adoc similarity index 97% rename from src/docs/chapter/user/20_Validation/MC/Tutorial_Complete_Model_Checking.adoc rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Complete_Model_Checking.adoc index cea4ec9444408159cdb71cce6791c491dcd2ae5b..5095a17d1847a17e906099cf611e2767ea4024b3 100644 --- a/src/docs/chapter/user/20_Validation/MC/Tutorial_Complete_Model_Checking.adoc +++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Complete_Model_Checking.adoc @@ -1,5 +1,6 @@ + [[tutorial-complete-model-checking]] -== Tutorial Complete Model Checking += Tutorial Complete Model Checking We assume that you have completed <<tutorial-first-model-checking,Tutorial First Model Checking>>. @@ -33,7 +34,7 @@ will compute at most 5 possible ways to execute any given operation (i.e., Increase and Reset in this case). We return to this issue below. [[successful-model-checking]] -=== Successful Model Checking +== Successful Model Checking Now select the "Model Check..." command in the _Verify_ menu which brings up the model checking dialog box: @@ -55,7 +56,7 @@ about interpreting a completed model check. Below we examine several issues that have to be considered. [[computing-all-transitions]] -=== Computing All Transitions +== Computing All Transitions Let us now adapt the above B machine by changing the DEFINITION of MAX to 6. Now repeat the model checking exercise above. This time ProB will @@ -95,7 +96,7 @@ a counter example: image::ProBSimpleCounterForMC_InvViol.png[] [[tutorial-deferred-sets]] -=== Deferred Sets +== Deferred Sets Let us now use the following simple machine: @@ -155,7 +156,7 @@ SETS ID={id1,id2,id3,id4,id5} .... [[infinite-types]] -=== Infinite Types +== Infinite Types It could be that your B machine makes use of the mathematical integers (`INTEGER`) or infinite subsets thereof (`NATURAL`, `NATURAL1`). Note @@ -176,7 +177,7 @@ it. This information is not yet fed back to the graphical user interface (but we are working on it). [[model-checking-and-proof]] -=== Model Checking and Proof +== Model Checking and Proof Finally, even if ProB was able to successfully check the entire state space of your model, this does not imply that you can prove your machine diff --git a/src/docs/chapter/user/11_BLanguage/WD/10_Tutorial_Debugging_Well-Definedness_and_Transition_Errors.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Debugging_Well-Definedness_and_Transition_Errors.adoc similarity index 96% rename from src/docs/chapter/user/11_BLanguage/WD/10_Tutorial_Debugging_Well-Definedness_and_Transition_Errors.adoc rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Debugging_Well-Definedness_and_Transition_Errors.adoc index 118753361aadb64d01f570e7df16abcf2dcd1317..d0eac527f8efc02bfaa51d056cd2a1945702e7fe 100644 --- a/src/docs/chapter/user/11_BLanguage/WD/10_Tutorial_Debugging_Well-Definedness_and_Transition_Errors.adoc +++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Debugging_Well-Definedness_and_Transition_Errors.adoc @@ -1,5 +1,6 @@ + [[tutorial-debugging-well-definedness-and-transition-errors]] -== Tutorial Debugging Well-Definedness and Transition Errors += Tutorial Debugging Well-Definedness and Transition Errors We assume that you have grasped the way that ProB setups up the initial states of a B machine as outlined in @@ -10,7 +11,7 @@ Understanding the Complexity of B Animation>>. You may also want to have a look at the explanation of <<well-definedness-checking,well-definedness in B>>. -=== A simple example +== A simple example Let us use the following B machine as starting point: diff --git a/src/docs/chapter/user/20_Validation/MC/Tutorial_Directed_Model_Checking.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Directed_Model_Checking.adoc similarity index 98% rename from src/docs/chapter/user/20_Validation/MC/Tutorial_Directed_Model_Checking.adoc rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Directed_Model_Checking.adoc index 513fc0eac34c64c267d5729a34ba1a64d5394b5e..fdd8745d443a50e4e8272be3e7a2c986e4795aec 100644 --- a/src/docs/chapter/user/20_Validation/MC/Tutorial_Directed_Model_Checking.adoc +++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Directed_Model_Checking.adoc @@ -1,5 +1,6 @@ + [[tutorial-directed-model-checking]] -== Tutorial Directed Model Checking += Tutorial Directed Model Checking We assume that you have completed <<tutorial-first-model-checking,Tutorial First Model Checking>> and @@ -102,7 +103,7 @@ Below we show the output of the above command for the various choices of . [[breadth-first]] -=== Breadth-First +== Breadth-First `$ probcli phonebook7.mch -p MAX_OPERATIONS 99 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode bf` @@ -115,7 +116,7 @@ requirements can be very large and it can take very long to find long counter examples. [[depth-first]] -=== Depth-First +== Depth-First `$ probcli phonebook7.mch -p MAX_OPERATIONS 99 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode df` @@ -132,7 +133,7 @@ and possibly hard to understand for the user. The next search strategy, tries to combine the advantages of breadth-first and depth-first search. [[mixed-dfbf]] -=== Mixed DF/BF +== Mixed DF/BF The mixed search strategy, tries to combine the advantages of breadth-first and depth-first search. It is the default setting for @@ -156,7 +157,7 @@ It is interesting to compare this result with the random search strategy, which we show next. [[random]] -=== Random +== Random `$ probcli phonebook7.mch -p MAX_OPERATIONS 99 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode random` @@ -170,7 +171,7 @@ Compared to the `mixed` option one can notice that the mixed option has more of a tendency to explore certain branches in depth. [[hash]] -=== Hash +== Hash `$ probcli phonebook7.mch -p MAX_OPERATIONS 99 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode hash` @@ -181,7 +182,7 @@ the same result, as the hash value of the states do not change from one run of ProB to another. [[out-degree]] -=== Out-Degree +== Out-Degree `$ probcli phonebook7.mch -p MAX_OPERATIONS 99 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode dlk` @@ -194,7 +195,7 @@ and delete). Note: here it is important to set the `MAX_OPERATIONS` high enough, otherwise the resulting state space could be different. [[more-examples]] -=== More examples +== More examples A further illustration of directed model checking can be found in our <<blocks-world-directed-model-checking,"Blocks World" example>>. diff --git a/src/docs/chapter/user/40_AdvancedFeatures/10_Tutorials/Tutorial_Disprover.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Disprover.adoc similarity index 95% rename from src/docs/chapter/user/40_AdvancedFeatures/10_Tutorials/Tutorial_Disprover.adoc rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Disprover.adoc index 4ab91a9e2ed846a4e561ef2927921a907c04cd31..9c7a062e54a4121388b4d6e3fba915def2e02263 100644 --- a/src/docs/chapter/user/40_AdvancedFeatures/10_Tutorials/Tutorial_Disprover.adoc +++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Disprover.adoc @@ -1,8 +1,9 @@ + [[tutorial-disprover]] -== Tutorial Disprover += Tutorial Disprover [[warning]] -=== WARNING +== WARNING We believe the Disprover to be useful. The disprover plugin is currently still experimental when used as a prover. Please keep in mind, that you @@ -10,7 +11,7 @@ might run into some rough edges or even get wrong results (please inform us about any issues). [[introduction-tutorial-disprover]] -=== Introduction +== Introduction The ProB Disprover plugin for RODIN utilizes the ProB animator and model checker to automatically find counterexamples or proofs for a given @@ -28,14 +29,14 @@ proof. See https://www3.hhu.de/stups/downloads/pdf/disprover_eval.pdf[the paper describing the disprover as a prover] for more details. [[installation-tutorial-disprover]] -=== Installation +== Installation The ProB Disprover is currently only available through the ProB Nightly Build Update Site (http://nightly.cobra.cs.uni-duesseldorf.de/rodin/updatesite/). [[how-to-use-it]] -=== How to use it +== How to use it image::Disprover-all.png[] @@ -46,7 +47,7 @@ the tool bar alongside the other provers: image::Disprover_proof_control.png[] [[how-it-works]] -=== How it works +== How it works Upon selecting the Disprover, it builds a formula from the Hypotheses and the negated Goal. The ProB model checker then tries to find a model diff --git a/src/docs/chapter/user/20_Validation/CBC/30_Tutorial_Enabling_Analysis.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Enabling_Analysis.adoc similarity index 99% rename from src/docs/chapter/user/20_Validation/CBC/30_Tutorial_Enabling_Analysis.adoc rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Enabling_Analysis.adoc index 2a327d0ba9ae1a08c9579649dc7b22321d7f8f89..936e414c42418a37a5073d34ab9809d9200cb5c5 100644 --- a/src/docs/chapter/user/20_Validation/CBC/30_Tutorial_Enabling_Analysis.adoc +++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Enabling_Analysis.adoc @@ -1,5 +1,6 @@ + [[tutorial-enabling-analysis]] -== Tutorial Enabling Analysis += Tutorial Enabling Analysis The B-method and in particular its successor Event-B are methodologies for formal development and verification of systems. In Event-B, a @@ -25,7 +26,7 @@ a table or by means of a graph. For simplicity, we will concentrate mainly on B and use the terminology of the formalism. [[enabling-relations]] -=== Enabling Relations +== Enabling Relations What we want to find out is how the operations influence each other within a B model. In other words, for each pair (op1, op2) of operations @@ -205,7 +206,7 @@ and deduce some properties. For example, we can clearly see that `Op4` cannot occur after the execution of another operation. [[summary-of-the-enabling-relations]] -=== Summary of the Enabling Relations +== Summary of the Enabling Relations In the following, we summarize most of the enabling relations that we think can provide a useful feedback to the user. For each of the @@ -273,7 +274,7 @@ image::PossibleDisableExample.png[] image::InfeasibleExample.png[] [[performing-enabling-analysis-within-prob]] -=== Performing Enabling Analysis within ProB +== Performing Enabling Analysis within ProB The enabling analysis has been implemented in the ProB toolset. The computation of the enabling relations is based on syntactic and @@ -387,4 +388,4 @@ whether a single event is in principle possible (given the invariant): $ probcli file.mch -feasibility_analysis_csv FILE .... -=== References and Footnotes +== References and Footnotes diff --git a/src/docs/chapter/user/20_Validation/MC/Tutorial_First_Model_Checking.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_First_Model_Checking.adoc similarity index 97% rename from src/docs/chapter/user/20_Validation/MC/Tutorial_First_Model_Checking.adoc rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_First_Model_Checking.adoc index 0b5774488d15858d4a2588f76a8d602c567027b4..8018e4be893dfd26c614b460147e22b69df864c7 100644 --- a/src/docs/chapter/user/20_Validation/MC/Tutorial_First_Model_Checking.adoc +++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_First_Model_Checking.adoc @@ -1,5 +1,6 @@ + [[tutorial-first-model-checking]] -== Tutorial First Model Checking += Tutorial First Model Checking We assume that you have loaded the "Lift.mch" B machine from the ProB Examples folder as outlined in <<tutorial-first-step,Tutorial First @@ -7,7 +8,7 @@ Step>>. There we have also seen how to execute operations on a B machine by double clicking on the items in the "Enabled Operations" pane. [[simple-model-checking]] -=== Simple Model Checking +== Simple Model Checking The model checker can be used to systematically execute the operations and tries to find an erroneous state (e.g., where the invariant is @@ -39,7 +40,7 @@ sequence that leads to an error or to this error. However, by selecting the shortest paths are found.) [[coverage-statistics]] -=== Coverage Statistics +== Coverage Statistics We can obtain some statistics about how many states ProB has explored by selecting the "Compute Coverage" command in the _Analyse_ menu: @@ -69,7 +70,7 @@ transitions: we have one initialization, 8 `inc` operations and 8 `dec` operations. [[view-statespace]] -=== View Statespace +== View Statespace We can obtain a graphical visualization of the state space explored by ProB. For this, be sure that you have correctly diff --git a/src/docs/chapter/user/10_General/Tutorial_First_Step.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_First_Step.adoc similarity index 97% rename from src/docs/chapter/user/10_General/Tutorial_First_Step.adoc rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_First_Step.adoc index 18720dfb391f684a08ff9986e4eab2ce2b0493a8..a79c1518b9e65dff631e8b4f0ba711d55e674494 100644 --- a/src/docs/chapter/user/10_General/Tutorial_First_Step.adoc +++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_First_Step.adoc @@ -1,14 +1,15 @@ + [[tutorial-first-step]] -== Tutorial First Step += Tutorial First Step [[installation-tutorial-first-step]] -=== Installation +== Installation Start off by installing the standalone Tcl/Tk version of ProB. Follow the instructions in <<installation,Installation>>. [[starting-prob-tutorial-first-step]] -=== Starting ProB +== Starting ProB Start ProB by double-clicking on `ProBWin` (for Windows users), or by launching `StartProB.sh` from a Terminal (for Linux and Mac users). @@ -32,7 +33,7 @@ Normally, it should look as follows (on Windows): image::ProBStartTerminal.png[] [[loading-a-first-b-machine]] -=== Loading a first B machine +== Loading a first B machine Use the "Open..." command in the _File_ menu @@ -48,7 +49,7 @@ window should now look as follows: image::ProB_LiftAfterLoad.png[] [[first-steps-in-animation]] -=== First Steps in Animation +== First Steps in Animation We have now loaded a first simple B model. Let us look at the contents of the ProB window (ignoring the menu bar). diff --git a/src/docs/chapter/user/20_Validation/MC/Tutorial_LTL_Counter-example_View.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_LTL_Counter-example_View.adoc similarity index 98% rename from src/docs/chapter/user/20_Validation/MC/Tutorial_LTL_Counter-example_View.adoc rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_LTL_Counter-example_View.adoc index 5147cc951d72b1c34eb988964e9c0a5f3efb6650..10c8f0c0dde4dee4c70617636d2cbd68ce0dd9b5 100644 --- a/src/docs/chapter/user/20_Validation/MC/Tutorial_LTL_Counter-example_View.adoc +++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_LTL_Counter-example_View.adoc @@ -1,5 +1,6 @@ + [[tutorial-ltl-counter-example-view]] -== Tutorial LTL Counter-example View += Tutorial LTL Counter-example View In this tutorial a quick overview will be given describing the LTL counter-example visualization plug-in in Rodin. The functionality of the @@ -8,7 +9,7 @@ different properties will be checked that are not satisfied by the model. [[ltl-model-checking-and-the-meaning-of-counter-examples]] -=== LTL Model Checking and the Meaning of Counter-examples +== LTL Model Checking and the Meaning of Counter-examples Model checking is a technique for checking in an automatic way whether a model satisfies a property expressed in formal logic. LTL (standing for @@ -50,7 +51,7 @@ is a counter-example for each LTL formula latexmath:[$X^{n} (true)$], with latexmath:[$n\geq 1$].] property, whereas the path in Figure 3 represents usually a counter-example for a safety property. -=== Visualization of Counter-examples in Rodin +== Visualization of Counter-examples in Rodin *Coloring and highlighting nodes in a counter-example* Each state of a path in the LTL counter-example view is marked by a @@ -163,7 +164,7 @@ image::LTLViewVisualisation4.png[] In order to view the visualizations of the sub-formulas, one should click on one of the states of the source-formula. -=== Use Case for the LTL Counter-example Viewer +== Use Case for the LTL Counter-example Viewer Consider an Event-B model formalizing an algorithm for mutual exclusion with semaphores for two concurrent processes latexmath:[$P_1$] and @@ -258,7 +259,7 @@ state ‘p1=wait1’ becomes true. Once a state is encountered where will hold. This is apparently not fulfilled as in all successor states _p1_ will not become equal to _crit1_. -=== Literature Sources +== Literature Sources For more detailed information on visualizing counter-examples in the LTL counter-example view in Rodin refer to footnote:[Andriy Tolstoy, @@ -272,4 +273,4 @@ Checking_. MIT Press, 2008.]. The Event-B model used in this tutorial can be downloaded from http://www.stups.uni-duesseldorf.de/~dobrikov/modelchecking/MUTEX.zip[here]. -=== References +== References diff --git a/src/docs/chapter/user/20_Validation/CBC/31_Tutorial_Model_Checking,_Proof_and_CBC.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Model_Checking_Proof_and_CBC.adoc similarity index 97% rename from src/docs/chapter/user/20_Validation/CBC/31_Tutorial_Model_Checking,_Proof_and_CBC.adoc rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Model_Checking_Proof_and_CBC.adoc index fbac05819fdd109e6b08d80f5452364d71d6f5e5..e35c2314a35c37a4e0bd618bf1952b700565a1f9 100644 --- a/src/docs/chapter/user/20_Validation/CBC/31_Tutorial_Model_Checking,_Proof_and_CBC.adoc +++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Model_Checking_Proof_and_CBC.adoc @@ -1,5 +1,6 @@ + [[tutorial-model-checking-proof-and-cbc]] -== Tutorial Model Checking, Proof and CBC += Tutorial Model Checking, Proof and CBC We assume that you have completed <<tutorial-complete-model-checking,Tutorial Complete Model @@ -28,7 +29,7 @@ Is this model correct? As you will see, this depends on your point of view. [[state-space]] -=== State Space +== State Space If you look purely at the state space of the machine (choose the View State Space command in the Animate menu) you get the following picture: @@ -43,7 +44,7 @@ However, you will not be able to prove the system correct using AtelierB or Rodin. [[constraint-based-checking-cbc-for-the-invariant]] -=== Constraint Based Checking (CBC) for the Invariant +== Constraint Based Checking (CBC) for the Invariant In addition to model checking, ProB also offers constraint-based checking (CBC), which is particularly useful when used in conjunction @@ -118,7 +119,7 @@ operation must preserve the invariant for the state with `counter=65`, which it does not. [[how-to-correct-problems-found]] -=== How to correct problems found +== How to correct problems found Below is a small guide on how to correct invariant violations found by constraint-based checking and model checking. diff --git a/src/docs/chapter/user/11_BLanguage/30_Tutorial_Modeling_Infinite_Datatypes.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Modeling_Infinite_Datatypes.adoc similarity index 98% rename from src/docs/chapter/user/11_BLanguage/30_Tutorial_Modeling_Infinite_Datatypes.adoc rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Modeling_Infinite_Datatypes.adoc index 1094ccba181ce0c796ec3955c08b27bed18ccdab..bac81b125574beb2d7416361365845f11a396fc1 100644 --- a/src/docs/chapter/user/11_BLanguage/30_Tutorial_Modeling_Infinite_Datatypes.adoc +++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Modeling_Infinite_Datatypes.adoc @@ -1,7 +1,6 @@ - [[tutorial-modeling-infinite-datatypes]] -== 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 diff --git a/src/docs/chapter/user/30_OtherLanguages/EventB/Tutorial_Rodin_Exporting.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Rodin_Exporting.adoc similarity index 94% rename from src/docs/chapter/user/30_OtherLanguages/EventB/Tutorial_Rodin_Exporting.adoc rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Rodin_Exporting.adoc index a640e78786120d084a983ec02955eff376d5bc0e..5a5dbb45381458b3be0018c7289d6b6206c56056 100644 --- a/src/docs/chapter/user/30_OtherLanguages/EventB/Tutorial_Rodin_Exporting.adoc +++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Rodin_Exporting.adoc @@ -1,8 +1,9 @@ + [[tutorial-rodin-exporting]] -=== Tutorial Rodin Exporting += Tutorial Rodin Exporting [[introduction-to-tutorial-rodin-exporting]] -==== Introduction +== Introduction Many features of ProB are currently only available in ProB Tcl/Tk or the <<using-the-command-line-version-of-prob,probcli>> command-line @@ -10,7 +11,7 @@ version]. Luckily you can export Rodin models for use with those tools. Below we explain how. [[exporting-for-prob-classic]] -==== Exporting for ProB classic +== Exporting for ProB classic Start by right clicking (control Click on the Mac) on the machine or context in the "Event-B Explorer" view you wish to export and select @@ -23,7 +24,7 @@ default one will do) for the file. The file should have the extension ".eventb" (as suggested by default). [[loading-an-event-b-project-into-prob-classic]] -==== Loading an Event-B Project into ProB classic +== Loading an Event-B Project into ProB classic You can now use the ".eventb" file directly for probcli. For example, the following command will perform standard model checking on the file @@ -57,7 +58,7 @@ into a single ".eventb" project file. image::ProBRodinLoadedInTclTk.png[] [[starting-up-prob-classic-directly]] -==== Starting up ProB Classic Directly +== Starting up ProB Classic Directly You can also start up ProB Classic (aka ProB Tcl/Tk) directly, without first generating an ".eventb" file. For this, start by right clicking diff --git a/src/docs/chapter/user/30_OtherLanguages/EventB/Tutorial_Rodin_First_Step.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Rodin_First_Step.adoc similarity index 97% rename from src/docs/chapter/user/30_OtherLanguages/EventB/Tutorial_Rodin_First_Step.adoc rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Rodin_First_Step.adoc index c601db62a4d80e7961b8bad5a36af5f41288cedd..c646bb06c69b63388f7a9d1ddbf271c278879435 100644 --- a/src/docs/chapter/user/30_OtherLanguages/EventB/Tutorial_Rodin_First_Step.adoc +++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Rodin_First_Step.adoc @@ -1,8 +1,9 @@ + [[tutorial-rodin-first-step]] -=== Tutorial Rodin First Step += Tutorial Rodin First Step [[installation-rodin]] -==== Installation +== Installation First you need to download the Rodin platform (e.g, http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.3/[Rodin @@ -30,7 +31,7 @@ A detailed of the installation is available here>>. [[starting-prob-tutorial-rodin-first-step]] -==== Starting ProB +== Starting ProB Start by right clicking (control Click on the Mac) on the machine or context you wish to animate and select "Start Animation/Model diff --git a/src/docs/chapter/user/30_OtherLanguages/EventB/Tutorial_Rodin_Parameters.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Rodin_Parameters.adoc similarity index 94% rename from src/docs/chapter/user/30_OtherLanguages/EventB/Tutorial_Rodin_Parameters.adoc rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Rodin_Parameters.adoc index 7f063802a25e970658bcd2e97940523a8b3886d6..367b6a8ffa7ee7cfc3eb20231987b931770bdb90 100644 --- a/src/docs/chapter/user/30_OtherLanguages/EventB/Tutorial_Rodin_Parameters.adoc +++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Rodin_Parameters.adoc @@ -1,8 +1,9 @@ + [[tutorial-rodin-parameters]] -=== Tutorial Rodin Parameters += Tutorial Rodin Parameters [[preferences-tutorial-rodin-parameters]] -==== Preferences +== Preferences You can modify the most important parameters of ProB by going to the Rodin preferences. @@ -18,7 +19,7 @@ image::ProBRodinPrefs.png[] We explain the most important preferences below. [[minint-and-maxint]] -==== Minint and Maxint +== Minint and Maxint We first explain the first two entries in the screenshot above. Within classical B this provides the range for the implementable integer type. @@ -28,7 +29,7 @@ if it cannot determine the value of an integer variable in order to know in which range it should be enumerated. [[size-of-unspecified-sets-carrier-sets]] -==== Size of unspecified sets (carrier sets) +== Size of unspecified sets (carrier sets) This is the third entry in the screen shot above. ProB requires all carrier sets to be finite and ProB has to know the cardinality before @@ -44,7 +45,7 @@ specify a maximum cardinality, or `card(S)>n` to specify a minimum cardinality. [[using-contexts-for-prob-animation]] -===== Using contexts for ProB animation +=== Using contexts for ProB animation Note that you can create a new context with those axioms just for animation or model checking with ProB. For this you can simply diff --git a/src/docs/chapter/user/10_General/Tutorial_Setup_Phases.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Setup_Phases.adoc similarity index 98% rename from src/docs/chapter/user/10_General/Tutorial_Setup_Phases.adoc rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Setup_Phases.adoc index 266d92b1010f8b5aafbd2fab19a11315f46edd4e..f14b8d9c3b0c2ba74ec03b6250227ae98168f721 100644 --- a/src/docs/chapter/user/10_General/Tutorial_Setup_Phases.adoc +++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Setup_Phases.adoc @@ -1,5 +1,6 @@ + [[tutorial-setup-phases]] -== Tutorial Setup Phases += Tutorial Setup Phases We assume that you have grasped the first steps of opening and animating a B machine as outlined in <<tutorial-first-step,Tutorial First @@ -30,7 +31,7 @@ image::ProB_AnimationPhases.png[] We now examine these phases on the Jukebox machine in more detail [[loading]] -=== 1. Loading +== 1. Loading Here ProB parses and type checks the machine. @@ -71,7 +72,7 @@ a "Reopen" command in the _File_ menu: image::ProB_JukeboxReopenCommand.png[] [[setup_constants]] -=== 2. SETUP_CONSTANTS +== 2. SETUP_CONSTANTS In this phase ProB will try and find values for the constants and parameters of your machine, so that the `PROPERTIES` and `CONSTRAINTS` @@ -90,7 +91,7 @@ phase: image::ProB_JukeboxAfterSETUPCONSTANTS.png[] [[initialisation]] -=== 3. INITIALISATION +== 3. INITIALISATION In this phase the values for the constants have been found, but the initial values of the variables still remain to be determined. For this, diff --git a/src/docs/chapter/user/40_AdvancedFeatures/10_Tutorials/Tutorial_Symbolic_Constants.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Symbolic_Constants.adoc similarity index 91% rename from src/docs/chapter/user/40_AdvancedFeatures/10_Tutorials/Tutorial_Symbolic_Constants.adoc rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Symbolic_Constants.adoc index 395c72b4e657d2f1fc98b6f68ac43c78139dd919..7762b69411c07c3760700515345b3afb02517e7e 100644 --- a/src/docs/chapter/user/40_AdvancedFeatures/10_Tutorials/Tutorial_Symbolic_Constants.adoc +++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Symbolic_Constants.adoc @@ -1,8 +1,9 @@ + [[tutorial-symbolic-constants]] -== Tutorial Symbolic Constants += Tutorial Symbolic Constants [[introduction-to-tutorial-symbolic-constants]] -=== Introduction +== Introduction ProB Tcl/Tk as well as the <<using-the-command-line-version-of-prob,probcli command-line @@ -14,14 +15,14 @@ complex ones. Through a plugin, this behaviour is extended to ProB for Rodin. [[installing-the-prob-symbolic-constants-plugin]] -=== Installing the ProB Symbolic Constants Plugin +== Installing the ProB Symbolic Constants Plugin The plugin is available from the ProB for Rodin Updatesite. The package is called "ProB for Rodin2 - Symbolic Constants Support". It is not bundled with ProB for Rodin itself. [[marking-constants-to-be-kept-symbolic]] -=== Marking Constants to be kept symbolic +== Marking Constants to be kept symbolic Once the plugin is installed, a toggle button "symbolic" / "not symbolic" should appear next to each constant in the Rodin editor. diff --git a/src/docs/chapter/user/10_General/Tutorial_Troubleshooting_the_Setup.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Troubleshooting_the_Setup.adoc similarity index 98% rename from src/docs/chapter/user/10_General/Tutorial_Troubleshooting_the_Setup.adoc rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Troubleshooting_the_Setup.adoc index e77e4fa2095f9eb146ea566a61197d028e744cdb..9bc968f557233dcd818b277332cd0ddee42912c2 100644 --- a/src/docs/chapter/user/10_General/Tutorial_Troubleshooting_the_Setup.adoc +++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Troubleshooting_the_Setup.adoc @@ -1,5 +1,6 @@ + [[tutorial-troubleshooting-the-setup]] -== Tutorial Troubleshooting the Setup += Tutorial Troubleshooting the Setup We assume that you have grasped the way that ProB setups up the initial states of a B machine as outlined in @@ -15,7 +16,7 @@ We will also learn to use the various predicate analysis features provided by ProB. [[simple-inconsistency-in-the-properties]] -=== Simple Inconsistency in the PROPERTIES +== Simple Inconsistency in the PROPERTIES First, open the machine "Jukebox.mch" which can be found in the SchneiderBook/Jukebox_Chapter13 subdirectory of the ProB Examples @@ -70,7 +71,7 @@ we can proceed with animation of the machine: image::ProB_JukeboxAfterLoad2.png[] [[a-more-involved-inconsistency]] -=== A more involved inconsistency +== A more involved inconsistency Let us add diff --git a/src/docs/chapter/user/10_General/Tutorial_Understanding_ProB's_Constraint_Solver.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Understanding_ProB's_Constraint_Solver.adoc similarity index 98% rename from src/docs/chapter/user/10_General/Tutorial_Understanding_ProB's_Constraint_Solver.adoc rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Understanding_ProB's_Constraint_Solver.adoc index 9a1680124596e5ddaf7bf3b2c2055a26b942b8f9..b5e4ac75a936ee753efc4d13b4cc9834d8c60a71 100644 --- a/src/docs/chapter/user/10_General/Tutorial_Understanding_ProB's_Constraint_Solver.adoc +++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Understanding_ProB's_Constraint_Solver.adoc @@ -1,5 +1,6 @@ + [[tutorial-understanding-probs-constraint-solver]] -== Tutorial Understanding ProB's Constraint Solver += Tutorial Understanding ProB's Constraint Solver We assume that you have grasped the way that ProB setups up the initial states of a B machine as outlined in @@ -71,7 +72,7 @@ The following picture provides a very rough picture of this process: image::ProB_Propagation.png[] -=== A simple example +== A simple example Let us use the following B machine as starting point: @@ -161,7 +162,7 @@ and fi are correct (by looking at the "State Properties" pane): image::ProB_PropagationAfterInit.png[] [[complicating-the-example]] -=== Complicating the Example +== Complicating the Example To make the example more challenging, let us increase `up` to 100 and remove the equality for `f`. In other words, the PROPERTIES will now @@ -246,7 +247,7 @@ ms)"" in the "Animation Preferences". You can also control it using a definition for `SET_PREF_TIME_OUT` in the DEFINITIONS clause. [[adding-universally-quantified-formulas]] -=== Adding universally quantified formulas +== Adding universally quantified formulas Let us replace `f=fi` by the following property: diff --git a/src/docs/chapter/user/10_General/Tutorial_Understanding_the_Complexity_of_B_Animation.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Understanding_the_Complexity_of_B_Animation.adoc similarity index 98% rename from src/docs/chapter/user/10_General/Tutorial_Understanding_the_Complexity_of_B_Animation.adoc rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Understanding_the_Complexity_of_B_Animation.adoc index 0352f01865a55a843868724c5978edd3c2106b87..fb4efe7085717f642cb626c32b173364d58c9042 100644 --- a/src/docs/chapter/user/10_General/Tutorial_Understanding_the_Complexity_of_B_Animation.adoc +++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Understanding_the_Complexity_of_B_Animation.adoc @@ -1,5 +1,6 @@ + [[tutorial-understanding-the-complexity-of-b-animation]] -== Tutorial Understanding the Complexity of B Animation += Tutorial Understanding the Complexity of B Animation We assume that you have grasped the way that ProB setups up the initial states of a B machine as outlined in @@ -10,7 +11,7 @@ general, how ProB solves this problem, and what the ramification for users are. [[undecidability]] -=== Undecidability +== Undecidability In general, animation of a B model is undecidable. More precisely, it is undecidable to find out @@ -72,7 +73,7 @@ deferred set to a finite number before animation (see also you can control the cardinality of the deferred sets). [[complexity-of-animation]] -=== Complexity of Animation +== Complexity of Animation However, after addressing the undecidability issue, there is still the problem of complexity. The animation task can be arbitrarily complex diff --git a/src/docs/chapter/user/40_AdvancedFeatures/10_Tutorials/Tutorial_Unit_Plugin.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Unit_Plugin.adoc similarity index 95% rename from src/docs/chapter/user/40_AdvancedFeatures/10_Tutorials/Tutorial_Unit_Plugin.adoc rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Unit_Plugin.adoc index 40d3e0b49149ae48533d0633de5d5be987b02f85..6f416f6dba165b35b99c3367f7994ede130f309d 100644 --- a/src/docs/chapter/user/40_AdvancedFeatures/10_Tutorials/Tutorial_Unit_Plugin.adoc +++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Unit_Plugin.adoc @@ -1,5 +1,6 @@ + [[tutorial-unit-plugin]] -== Tutorial Unit Plugin += Tutorial Unit Plugin This tutorial describes, how ProB's integrated plugin for unit analysis can be used to verify the usage of physical units throughout a B @@ -17,7 +18,7 @@ We assume that you have a general understanding of B and the usage of ProB. [[activating-the-plugin-and-setting-preferences]] -=== Activating the Plugin and setting preferences +== Activating the Plugin and setting preferences Currently, the plugin can only be used with classical B machines. Therefore, a B machine needs to be loaded before the plugin can be @@ -41,7 +42,7 @@ a fix point state, in which possible unit errors are presented to the user through ProB's error reporting facilities. [[annotating-variables-and-animating-a-machine]] -=== Annotating variables and animating a machine +== Annotating variables and animating a machine To connect a variable with an expected physical unit, a special comment is placed before the variable. @@ -73,7 +74,7 @@ enables the plugin to be used in conjunction with the evaluation view, the dot output and most other ProB features. [[converting-between-units]] -=== Converting between units +== Converting between units To distinct between a numerical multiplication, that changes the values without changing the unit and a multiplication meant to convert between @@ -101,7 +102,7 @@ END .... [[static-analysis]] -=== Static analysis +== Static analysis If activated, the results of the static analysis can be accessed from the plugin menu. Currently, the results include the inferred unit of diff --git a/src/docs/chapter/user/40_AdvancedFeatures/10_Tutorials/Tutorial_Unit_Plugin_With_Rodin.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Unit_Plugin_With_Rodin.adoc similarity index 92% rename from src/docs/chapter/user/40_AdvancedFeatures/10_Tutorials/Tutorial_Unit_Plugin_With_Rodin.adoc rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Unit_Plugin_With_Rodin.adoc index 8fb62aede877de2a81c4d968f151e365207bd973..14e1c5ee7d1aa449c94f0fad7252384a8975fb0a 100644 --- a/src/docs/chapter/user/40_AdvancedFeatures/10_Tutorials/Tutorial_Unit_Plugin_With_Rodin.adoc +++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Unit_Plugin_With_Rodin.adoc @@ -1,5 +1,6 @@ + [[tutorial-unit-plugin-with-rodin]] -== Tutorial Unit Plugin With Rodin += Tutorial Unit Plugin With Rodin This tutorial describes, how ProB's integrated plugin for unit analysis can be used with Event-B machines from inside the Rodin platform. This @@ -18,7 +19,7 @@ We assume that you have a general understanding of Event-B and the usage of ProB / Rodin. [[installing-physical-units-support-for-prob-for-rodin]] -=== Installing Physical Units Support for ProB for Rodin +== Installing Physical Units Support for ProB for Rodin You can follow the <<tutorial-rodin-first-step,First Steps Instructions>> or the @@ -30,7 +31,7 @@ Rodin2 - Physical Units Support" plugin at out Rodin update site. You have to install both to enable physical units support for Rodin. [[attaching-physical-units-to-variables-and-constants]] -=== Attaching Physical Units to Variables and Constants +== Attaching Physical Units to Variables and Constants Once both plugins are installed, ProB allows to annotate both variables and constants with physical units: @@ -47,7 +48,7 @@ Units can be supplied in two forms: "10^2 * m^2". [[starting-the-analysis]] -=== Starting the Analysis +== Starting the Analysis The supplied units can now be used by ProB to infer missing units, verify the supplied units and detect unit errors. To start the analysis @@ -60,7 +61,7 @@ Once the analysis is finished, the "inferred unit" text fields are filled with the resulting units. [[possible-errors]] -=== Possible Errors +== Possible Errors Inside the Rodin Errors view, several errors might occur: diff --git a/src/docs/chapter/user/20_Validation/MC/Tutorial_Various_Optimizations.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Various_Optimizations.adoc similarity index 99% rename from src/docs/chapter/user/20_Validation/MC/Tutorial_Various_Optimizations.adoc rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Various_Optimizations.adoc index a8333861ad5e730746d0aaac9a969ba0a4d9388c..2a20d48688fad20c904f034b3c093ae6a248e915 100644 --- a/src/docs/chapter/user/20_Validation/MC/Tutorial_Various_Optimizations.adoc +++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Various_Optimizations.adoc @@ -1,5 +1,6 @@ + [[tutorial-various-optimizations]] -== Tutorial Various Optimizations += Tutorial Various Optimizations The ordinary model checker of ProB enables the user to verify automatically whether a B model contains any errors such as deadlocks @@ -20,7 +21,7 @@ additionally gives hints when it is recommendable to use these optimizations. [[partial-order-reduction]] -=== Partial Order Reduction +== Partial Order Reduction Partial order reduction (POR) is a method proposed for combating the state space explosion problem by means of state space reduction. The @@ -220,7 +221,7 @@ models. The evaluation can be obtained https://www3.hhu.de/stups/downloads/[here]. [[partial-guard-evaluation]] -=== Partial Guard Evaluation +== Partial Guard Evaluation When checking for consistency a B model the ProB model checker traverses the state space of the model beginning in some of the initial states and @@ -534,4 +535,4 @@ These and various other benchmarks used for evaluating partial guard evaluation (PGE) can be viewed https://www3.hhu.de/stups/downloads/[here]. -=== References +== References diff --git a/src/docs/chapter/user/YZ_Tutorials/ZZ_section_footer.adoc b/src/docs/chapter/user/YZ_Tutorials/ZZ_section_footer.adoc new file mode 100644 index 0000000000000000000000000000000000000000..47b3e87fa988d762de4f62225f8c99efe8f56565 --- /dev/null +++ b/src/docs/chapter/user/YZ_Tutorials/ZZ_section_footer.adoc @@ -0,0 +1,3 @@ + + +:leveloffset: -1 diff --git a/src/docs/chapter/user/70_Appendix/00_Appendix.adoc b/src/docs/chapter/user/ZZ_Appendix/00_section_header.adoc similarity index 57% rename from src/docs/chapter/user/70_Appendix/00_Appendix.adoc rename to src/docs/chapter/user/ZZ_Appendix/00_section_header.adoc index 2f15ee7bd613e957607cc99e59ee2f08acc9c03d..b5aa2d0eeac6c6df5ad9315dfcda3e1fa4dbb8b8 100644 --- a/src/docs/chapter/user/70_Appendix/00_Appendix.adoc +++ b/src/docs/chapter/user/ZZ_Appendix/00_section_header.adoc @@ -1,2 +1,4 @@ + [[appendix]] = Appendix +:leveloffset: +1 diff --git a/src/docs/chapter/user/70_Appendix/01_Team.adoc b/src/docs/chapter/user/ZZ_Appendix/01_Team.adoc similarity index 99% rename from src/docs/chapter/user/70_Appendix/01_Team.adoc rename to src/docs/chapter/user/ZZ_Appendix/01_Team.adoc index 17e2ef74c73b3a0c20610d8596a32bc3bfd01d00..a598bb8e9aaddae7908d09839a85d951dece0393 100644 --- a/src/docs/chapter/user/70_Appendix/01_Team.adoc +++ b/src/docs/chapter/user/ZZ_Appendix/01_Team.adoc @@ -1,5 +1,5 @@ [[team]] -== Team += Team ProB is based on research and implemention effort by our https://www.cs.hhu.de/lehrstuehle-und-arbeitsgruppen/softwaretechnik-und-programmiersprachen/unser-team.html[team]: * Michael Leuschel, diff --git a/src/docs/chapter/user/70_Appendix/02_FAQ.adoc b/src/docs/chapter/user/ZZ_Appendix/02_FAQ.adoc similarity index 91% rename from src/docs/chapter/user/70_Appendix/02_FAQ.adoc rename to src/docs/chapter/user/ZZ_Appendix/02_FAQ.adoc index a66f8eafbd71d115d756086b5460fe4859f5cbfc..a2ba12f1a8ab2c7ca2b1be8c0e62403847f667d6 100644 --- a/src/docs/chapter/user/70_Appendix/02_FAQ.adoc +++ b/src/docs/chapter/user/ZZ_Appendix/02_FAQ.adoc @@ -1,13 +1,13 @@ [[faq]] -== FAQ : Frequently asked Questions += FAQ : Frequently asked Questions -=== Can I use transitive closure for Event-B models? +== Can I use transitive closure for Event-B models? Yes, you need to use a theory of the transitive closure which contains a special mapping file. See <<event-b-theories,the section about Event-B theories>> along with the links to theories that can be used efficiently with ProB. -=== How can I reduce the memory consumption for model-checking? +== How can I reduce the memory consumption for model-checking? There are several options: @@ -32,7 +32,7 @@ checking, especially when the branching factor is very high. will not work for refinements and only has limited support for machine inclusion, but it can be very fast and the state space is kept on disk. -=== How do I perform a self-check of ProB? +== How do I perform a self-check of ProB? If you suspect something is wrong with your ProB Tcl/Tk installation, run the "Perform Self Check" command in the "Debug Menu". Note: run @@ -53,7 +53,7 @@ Self-Check Finished ------------------- .... -=== ProB seems stuck when loading a machine +== ProB seems stuck when loading a machine After parsing a machine, ProB is attempting to find valid initial states of your machine (or in case your machine has constants, valid values of @@ -67,7 +67,7 @@ jbtools parser sometimes behaves badly when syntax errors are present and can take a very long time to return the syntax error. [This has been fixed in the release 1.2.0] -=== Which features of B are covered? +== Which features of B are covered? ProB covers a large part of B, and we are striving towards full coverage. ProB supports B features such as non-deterministic operations, @@ -77,7 +77,7 @@ properties, and many more. It has limited support for multiple machines and refinements (see the <<Current_Limitations.adoc, Current_Limitations>> section and the FAQ entry about refinements below). -=== Is there support for refinement? +== Is there support for refinement? For the moment, you have to give types to operation arguments in refinements; the types are not always extracted from the ancestor @@ -96,7 +96,7 @@ affects refinement checking. [ProB's refinement checker is more suited for EventB than classical B, but we are working to fully support both styles of refinement.] -=== The constraint based checker is very slow and does not always work +== The constraint based checker is very slow and does not always work The constraint based checker is the least stable part of the system. @@ -109,12 +109,12 @@ the constraint based checker, not in the temporal model checker or the animator). Running ProB on Sicstus Prolog 3.9 seems to get rid of this problem (at least partially). -=== I can animate your machine files but I am not able to open my own machine files +== I can animate your machine files but I am not able to open my own machine files Be sure to have Java installed and set up the CLASSPATH as stipulated above. -=== ProB complains that some variables are not given a proper type +== ProB complains that some variables are not given a proper type All variables should be given a type even though ProB may still work without them (but you are living dangerously). In the latest release, @@ -124,14 +124,14 @@ also recognized as a type. aa: POW(myset) & bb: POW(aa) is now ok POW(POW(myset)) ). One can now also use subset for typing: bb <: COLOURS. -=== I cannot visualize the state space +== I cannot visualize the state space Be sure to set up the viewer preferences and use / (even on Windows!) Be sure to have dot installed and either dotty or a Postscript viewer. Also, on Windows the path to the machine files should not contain spaces. A good example directory would be C:/Machines/ -=== Some of my machines do not behave as expected +== Some of my machines do not behave as expected Maybe you are using a feature of B not yet supported by ProB. Have a look at the console window and see whether ProB displays any warning @@ -142,7 +142,7 @@ Machine and a description of the problem to me. You can also use the Save State Command in the File Menu and then send me the *.saved.P file (this way you do not have to tell me how to reach the buggy state). -=== How does ProB treat INT and NAT as opposed to INTEGER and NATURAL? +== How does ProB treat INT and NAT as opposed to INTEGER and NATURAL? As of version 1.2 ProB treats INT differently from INTEGER (the same is true for NAT and NAT1). A variable x:INT is now required to lie between @@ -150,7 +150,7 @@ MININT..MAXINT (which can be changed in the preferences; you can also change the setting on a per machine basis by adding DEFINITIONS likeSET_PREF_MININT == -10; SET_PREF_MAXINT == 100; to your machine.) -=== Problem with libtk.so on Linux +== Problem with libtk.so on Linux When launching ProB on Linux I get: ./prob: error while loading shared libraries: /usr/lib/libtk.so : invalid ELF header @@ -164,7 +164,7 @@ e.g., do something like that: # ln -s /usr/lib/libtk8.4.s (Probably best to make a backup of libtk.so before that.) ---- -=== Finding Multiple Assertion Violations +== Finding Multiple Assertion Violations I want to generate multiple assertion violations in ProB in order to generate the customized test cases for a particular B specfication @@ -182,7 +182,7 @@ my_assertion_N = SELECT not(Assertion_N) THEN skip END After model checking, you can again use "Compute Coverage" to see how often every assertion has been violated. -=== Checking Multiple LTL Formulas +== Checking Multiple LTL Formulas Can multiple LTL formulas be verified at a time? diff --git a/src/docs/chapter/user/70_Appendix/03_Download.adoc b/src/docs/chapter/user/ZZ_Appendix/03_Download.adoc similarity index 91% rename from src/docs/chapter/user/70_Appendix/03_Download.adoc rename to src/docs/chapter/user/ZZ_Appendix/03_Download.adoc index 1d689d3afb6622a9b092ee483944e3af0a642dce..3156f75c0746ae0998287e62daabd7b9c1331f00 100644 --- a/src/docs/chapter/user/70_Appendix/03_Download.adoc +++ b/src/docs/chapter/user/ZZ_Appendix/03_Download.adoc @@ -1,4 +1,4 @@ [[downloads]] -== Download += Download If you click https://www3.hhu.de/stups/prob/index.php/Download[here] you will be redirected to our online Download page. diff --git a/src/docs/chapter/user/70_Appendix/04_DownloadPriorVersions.adoc b/src/docs/chapter/user/ZZ_Appendix/04_DownloadPriorVersions.adoc similarity index 87% rename from src/docs/chapter/user/70_Appendix/04_DownloadPriorVersions.adoc rename to src/docs/chapter/user/ZZ_Appendix/04_DownloadPriorVersions.adoc index 80dc5f5384ff6c9bba2066e2f7cd6d3e046bccc9..24041c6479e0d27d7bba85c7e6354f03a45dda51 100644 --- a/src/docs/chapter/user/70_Appendix/04_DownloadPriorVersions.adoc +++ b/src/docs/chapter/user/ZZ_Appendix/04_DownloadPriorVersions.adoc @@ -1,4 +1,4 @@ [[prior-versions-of-prob]] -== Prior Versions of ProB += Prior Versions of ProB If you click https://www3.hhu.de/stups/prob/index.php/DownloadPriorVersions[here] you will be redirected to the Download Prior Versions of ProB page. diff --git a/src/docs/chapter/user/70_Appendix/05_Links.adoc b/src/docs/chapter/user/ZZ_Appendix/05_Links.adoc similarity index 98% rename from src/docs/chapter/user/70_Appendix/05_Links.adoc rename to src/docs/chapter/user/ZZ_Appendix/05_Links.adoc index 51a11c0c346b33a036acad7656b16270dcc8b932..c5ba633af16c629424532e308971e13679b36711 100644 --- a/src/docs/chapter/user/70_Appendix/05_Links.adoc +++ b/src/docs/chapter/user/ZZ_Appendix/05_Links.adoc @@ -1,8 +1,8 @@ [[links]] -== Links += Links [[books]] -=== Books +== Books * http://www.jpbowen.com/publications/thes-b.html[The B-Book: Assigning programs to meanings, by Jean-Raymond Abrial] (link is to a review by @@ -13,7 +13,7 @@ Introduction, by Steve Schneider] Software Engineering, by Jean-Raymond Abrial] (the Bee book) [[papers]] -=== Papers +== Papers * https://www3.hhu.de/stups/downloads/pdf/[ProB Publications] * http://en.wikipedia.org/wiki/B-Method[B-Method in Wikipedia] @@ -23,7 +23,7 @@ FM tools manage large scale industrial problems ?] * http://www.data-validation.fr[Data Validation] [[prob]] -=== ProB +== ProB * <<modelling-examples,Examples for ProB>> (along with screenshots and explanations) @@ -34,7 +34,7 @@ to Success Story (written by Cetic)] * https://groups.google.com/d/forum/prob-users[prob-users group] [[tools-using-prob]] -=== Tools using ProB +== Tools using ProB * https://github.com/plues/plues[PLUES] tool for university course validation @@ -79,7 +79,7 @@ implicit VDM specifications inside Ouverture] * http://www.ovado.net[Ovado] (as second tool chain) [[related-tools]] -=== Related Tools +== Related Tools * http://www.atelierb.eu/[Atelier B] * http://www.event-b.org/[Event-B and Rodin Wiki] @@ -105,7 +105,7 @@ TLA+, CSP and Prolog] checking tools] [[testimonials]] -=== Testimonials +== Testimonials * http://www.deploy-project.eu/pdf/D41-Siemens-final-full.pdf[Data validation at Siemens, Jérôme Falampin]: "The work done with ProB is a @@ -188,12 +188,12 @@ competition] (this is ProB out-of-the-box, without tuning and where SMT formulas are translated to B) [[other-links]] -=== Other Links +== Other Links * https://github.com/klar42/railground/[Railground Event-B Model] [[translating-to-logic]] -=== Translating to Logic +== Translating to Logic * http://legacy.earlham.edu/~peters/courses/log/transtip.htm[Translation Tips] diff --git a/src/docs/chapter/user/70_Appendix/06_ProB_Release_History.adoc b/src/docs/chapter/user/ZZ_Appendix/06_ProB_Release_History.adoc similarity index 99% rename from src/docs/chapter/user/70_Appendix/06_ProB_Release_History.adoc rename to src/docs/chapter/user/ZZ_Appendix/06_ProB_Release_History.adoc index 60e92681d7447b820a6bec1abf2873f7c52e9dae..5c863455f88de5697777da8c41c5c495478e0892 100644 --- a/src/docs/chapter/user/70_Appendix/06_ProB_Release_History.adoc +++ b/src/docs/chapter/user/ZZ_Appendix/06_ProB_Release_History.adoc @@ -1,5 +1,5 @@ [[release-history]] -== ProB Release History += ProB Release History Full ProB release history until release 1.8.3: diff --git a/src/docs/chapter/user/70_Appendix/10_Bugs.adoc b/src/docs/chapter/user/ZZ_Appendix/10_Bugs.adoc similarity index 97% rename from src/docs/chapter/user/70_Appendix/10_Bugs.adoc rename to src/docs/chapter/user/ZZ_Appendix/10_Bugs.adoc index 70df84d58dc2674f3069d09727ddcaf4881d7545..6b43847803cc794d43fd698f086b742c54841476 100644 --- a/src/docs/chapter/user/70_Appendix/10_Bugs.adoc +++ b/src/docs/chapter/user/ZZ_Appendix/10_Bugs.adoc @@ -1,5 +1,5 @@ [[bugs]] -== Bugs += Bugs If you want to submit a bug report, please use our https://probjira.atlassian.net/projects/PROBCORE/issues/[bug tracker]. You may also want to ask questions within our https://groups.google.com/forum/#!forum/prob-users[prob-users group]. diff --git a/src/docs/chapter/user/70_Appendix/11_Troubleshooting.adoc b/src/docs/chapter/user/ZZ_Appendix/11_Troubleshooting.adoc similarity index 98% rename from src/docs/chapter/user/70_Appendix/11_Troubleshooting.adoc rename to src/docs/chapter/user/ZZ_Appendix/11_Troubleshooting.adoc index 12cce018bf10773d8819d4d7bc1ad80467602d15..68821889914837547270a39f570cbe143fe48037 100644 --- a/src/docs/chapter/user/70_Appendix/11_Troubleshooting.adoc +++ b/src/docs/chapter/user/ZZ_Appendix/11_Troubleshooting.adoc @@ -1,5 +1,5 @@ [[troubleshooting]] -== Troubleshooting += Troubleshooting * Avoid installing ProB in a path with spaces or other special characters in them. The same holds for B machines you wish to analyze diff --git a/src/docs/chapter/user/70_Appendix/20_ProBLicence.adoc b/src/docs/chapter/user/ZZ_Appendix/20_ProBLicence.adoc similarity index 98% rename from src/docs/chapter/user/70_Appendix/20_ProBLicence.adoc rename to src/docs/chapter/user/ZZ_Appendix/20_ProBLicence.adoc index a4bc7d2411f71f5b178ee77baf4aa24fcced8f57..159f856926964b0e2d4ee4481900ac5d8eae9eea 100644 --- a/src/docs/chapter/user/70_Appendix/20_ProBLicence.adoc +++ b/src/docs/chapter/user/ZZ_Appendix/20_ProBLicence.adoc @@ -1,5 +1,5 @@ [[prob-licence]] -== ProB Licence += ProB Licence The ProB source code is distributed under the http://www.eclipse.org/org/documents/epl-v10.html[EPL v1.0 license] (see diff --git a/src/docs/chapter/appendix/A_literature.adoc b/src/docs/chapter/user/ZZ_Appendix/A_literature.adoc similarity index 97% rename from src/docs/chapter/appendix/A_literature.adoc rename to src/docs/chapter/user/ZZ_Appendix/A_literature.adoc index 1092fb5713b4ed477f11a45f8e18725ae8998cd0..a73a7344f6375079b2025d0c7b9a47fc893b28a3 100644 --- a/src/docs/chapter/appendix/A_literature.adoc +++ b/src/docs/chapter/user/ZZ_Appendix/A_literature.adoc @@ -1,3 +1,4 @@ + = Additional Literature bibliography::[] diff --git a/src/docs/chapter/appendix/B_preferences.adoc b/src/docs/chapter/user/ZZ_Appendix/B_preferences.adoc similarity index 99% rename from src/docs/chapter/appendix/B_preferences.adoc rename to src/docs/chapter/user/ZZ_Appendix/B_preferences.adoc index 7dab0dc8f5720b1423a0ec8406f7e0cbf0edf485..3a28b02b2eb1779490ea9583f1d21862845246b1 100644 --- a/src/docs/chapter/appendix/B_preferences.adoc +++ b/src/docs/chapter/user/ZZ_Appendix/B_preferences.adoc @@ -1,3 +1,4 @@ + = ProB Preferences A list of the current preferences available in ProB is available <<preferences-for-command-line,here>>. diff --git a/src/docs/chapter/user/ZZ_Appendix/ZZ_section_footer.adoc b/src/docs/chapter/user/ZZ_Appendix/ZZ_section_footer.adoc new file mode 100644 index 0000000000000000000000000000000000000000..47b3e87fa988d762de4f62225f8c99efe8f56565 --- /dev/null +++ b/src/docs/chapter/user/ZZ_Appendix/ZZ_section_footer.adoc @@ -0,0 +1,3 @@ + + +:leveloffset: -1