diff --git a/src/docs/chapter/user/ZZ_Appendix/01_Team.adoc b/src/docs/chapter/user/ZZ_Appendix/01_Team.adoc
deleted file mode 100644
index a598bb8e9aaddae7908d09839a85d951dece0393..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/ZZ_Appendix/01_Team.adoc
+++ /dev/null
@@ -1,44 +0,0 @@
-[[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,
-* Michael Butler,
-* Jens Bendisposto,
-* Ivaylo Dobrikov,
-* Dominik Hansen,
-* Philipp Körner,
-* Sebastian Krings,
-* Lukas Ladenberger,
-* David Schneider,
-* Joshua Schmidt
-* Daniel Plagge,
-* Marc Fontaine,
-* Fabian Fritz,
-* Corina Spermann,
-* Michael Jastram,
-* Joy Clark,
-* David Geleßus,
-* Antonia Pütz,
-* Fabian Vu,
-* Yumiko Takahashi,
-* Michelle Werth,
-* Philip Hoefges,
-* Edward Turner,
-* Dennis Winter,
-* Sonja Holl,
-* Jens Krüger,
-* Michael Birkhoff,
-* Carla Ferreira,
-* Stéphane Lo Presti,
-* Leonid Mikhailov,
-* Laksono Adhianto
-* ...
-
-Part of the research and development was conducted within various
-research projects, such as the http://www.epsrc.ac.uk/default.htm[EPSRC]
-funded projects http://users.ecs.soton.ac.uk/phh/abcd/[ABCD] and
-http://users.ecs.soton.ac.uk/mal/ISM.html[iMoc], the EU funded projects
-http://rodin.cs.ncl.ac.uk/[Rodin], http://www.deploy-project.eu/[Deploy]
-and http://www.advance-ict.eu/[Advance] as well as the
-http://www.dfg.de/[DFG] project http://www.gepavas.de/[Gepavas].
diff --git a/src/docs/chapter/user/ZZ_Appendix/02_FAQ.adoc b/src/docs/chapter/user/ZZ_Appendix/02_FAQ.adoc
deleted file mode 100644
index a2ba12f1a8ab2c7ca2b1be8c0e62403847f667d6..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/ZZ_Appendix/02_FAQ.adoc
+++ /dev/null
@@ -1,197 +0,0 @@
-[[faq]]
-= FAQ : Frequently asked Questions
-
-== 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?
-
-There are several options:
-
-1. Try to reduce the amount of memory ProB uses per state: For probcli
-you can set the COMPRESSION preference to true, e.g., in the following
-way:
-`probcli MyMachine.mch --model-check -p COMPRESSION TRUE`
-You could also add a DEFINITION
-`SET_PREF_COMPRESSION == TRUE`
-to your B machine to set the preference. There is also the possibility
-to forget the state space of already visited states by setting the
-preferences FORGET_STATE_SPACE and IGNORE_HASH_COLLISIONS to TRUE.
-
-2. You can try to reduce the state space, e.g., via <<symmetry-reduction, symmetry reduction>>. Hash
-symmetry typically works best. Another possibility is in the paragraph partial order reduction of the section
-<<tutorial-various-optimizations, Tutorial Various Optimizations>>.
-
-3. Sometimes <<bounded-model-checking, bounded model checking>> works much better than explicit state model
-checking, especially when the branching factor is very high.
-
-4. You could try and use our <<tlc, TLC backend>>. It
-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?
-
-If you suspect something is wrong with your ProB Tcl/Tk installation,
-run the "Perform Self Check" command in the "Debug Menu". Note: run
-this command immediately after startup before opening new machines
-(otherwise you may get some errors because the machine will override
-some default definitions used for the tests). Normally, the console
-window should look like this (you may get some multiple solutions
-warnings; but you should not get errors):
-
-....
----------------------
-Performing Self-Check
-..........................................................
-..........................................................
-..........................................................
-..........................................................
-Self-Check Finished
--------------------
-....
-
-== 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
-the constants which satisfy the PROPERTIES clause). In the animation
-preferences you can specify how many valid initial states (or valid
-values for the constants) ProB will look for. Try decreasing that number
-(default value: 4). You can also try and simplify the INITIALISATION (or
-PROPERTIES) clause, or reduce the cardinality of the base sets and
-decrease MAXINT. ProB is could also be stuck in the parsing process. The
-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?
-
-ProB covers a large part of B, and we are striving towards full
-coverage. ProB supports B features such as non-deterministic operations,
-ANY statements, operations with complex arguments, sets, sequences,
-functions, lambda abstractions, set comprehensions, constants and
-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?
-
-For the moment, you have to give types to operation arguments in
-refinements; the types are not always extracted from the ancestor
-specification. Furthermore, the precondition of the operations again are
-not extracted from ancestor machines and are not propagated down. This
-is an important difference with classical B: it means that ProB may find
-an invariant violation in the refinement machine even though the
-Refinement can be proven correct with B4Free or AtelierB. This is
-because in those tools you only need to prove consistency within the
-precondition of all ancestor machines ! ProB checks the refinement
-machine on its own. Anyway, we believe that it is probably bad style to
-rely on preconditions from ancestor machines for correctness (as they
-may be expressed in terms of abstract variables no longer present,...).
-Finally, as ProB treats top-level PRE conditions as SELECTS, this also
-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 the least stable part of the system.
-First try it on simple machines to get a feel of how it works.
-Currently, it may still attempt infinite enumerations even for finite
-state machines. We are working on an improved version for the next
-release. Also, there is a bug in Sicstus Prolog 3.10, which means that
-suspended goals may sometimes be discarded (this only seems to happen in
-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
-
-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
-
-All variables should be given a type even though ProB may still work
-without them (but you are living dangerously). In the latest release,
-typing has become more flexible and previously defined variables are
-also recognized as a type. aa: POW(myset) & bb: POW(aa) is now ok
-(previously it was required to type aa: POW(myset) & bb: POW(aa) & bb:
-POW(POW(myset)) ). One can now also use subset for typing: bb <:
-COLOURS.
-
-== 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
-
-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
-messages (something like uncovered expression encountered:). If
-possible, send me an email with the Machine and the message. If there is
-no message, you may have encountered a genuine bug: please send the
-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?
-
-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
-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
-
-When launching ProB on Linux I get: ./prob: error while loading shared
-libraries: /usr/lib/libtk.so : invalid ELF header
-
-Solution:
-
-----
-Replace libtk.so with a symbolic link to the actual library,
-e.g., do something like that: # ln -s /usr/lib/libtk8.4.s
-/usr/lib/libtk.so
-(Probably best to make a backup of libtk.so before that.)
-----
-
-== 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
-according to various test coverage criteria. But ProB can only produce a
-single assertion violation at one time. Is there any option in ProB that
-can help in producing multiple assertion violations at one goal/command?
-
-For the moment the solution would be to put the assertions into the
-invariant and then model check the entire state space by disabling
-"Find Invariant Violations" in the dialog box for the Temporal Model
-Check command. Afterwards, you can use "Compute Coverage" in the
-"Analyse" menu to see how many states have violated the invariant.
-Another solution is to write a "dummy" operation for every assertion:
-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
-
-Can multiple LTL formulas be verified at a time?
-
-You can write multiple LTL assertions in the DEFINITIONS clause, e.g.,
-
-----
-ASSERT_LTL0 == "G (e(SetCruiseSpeed) -> e(CruiseBecomesNotAllowed))";
-ASSERT_LTL1 == "G (e(CruiseBecomesNotAllowed) -> e(SetCruiseSpeed))";
-ASSERT_LTL2 == "G (e(CruiseBecomesNotAllowed) -> e(ObstacleDisappears))"
-----
-
-They can then all be checked using the `Check LTL Assertions` command.
diff --git a/src/docs/chapter/user/ZZ_Appendix/03_Download.adoc b/src/docs/chapter/user/ZZ_Appendix/03_Download.adoc
deleted file mode 100644
index 3156f75c0746ae0998287e62daabd7b9c1331f00..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/ZZ_Appendix/03_Download.adoc
+++ /dev/null
@@ -1,4 +0,0 @@
-[[downloads]]
-= 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/ZZ_Appendix/04_DownloadPriorVersions.adoc b/src/docs/chapter/user/ZZ_Appendix/04_DownloadPriorVersions.adoc
deleted file mode 100644
index 24041c6479e0d27d7bba85c7e6354f03a45dda51..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/ZZ_Appendix/04_DownloadPriorVersions.adoc
+++ /dev/null
@@ -1,4 +0,0 @@
-[[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/ZZ_Appendix/05_Links.adoc b/src/docs/chapter/user/ZZ_Appendix/05_Links.adoc
deleted file mode 100644
index 4fc8f82535c8bc6fac746a5d26a8898854b400af..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/ZZ_Appendix/05_Links.adoc
+++ /dev/null
@@ -1,207 +0,0 @@
-[[links]]
-= Links
-
-[[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
-Jonathan Bowen)
-* http://www.palgrave.com/science/computing/schneider/[The B-Method: An
-Introduction, by Steve Schneider]
-* http://www.event-b.org/abook.html[Modeling in Event-B: System and
-Software Engineering, by Jean-Raymond Abrial] (the Bee book)
-
-[[papers]]
-== Papers
-
-* https://www3.hhu.de/stups/downloads/pdf/[ProB Publications]
-* http://en.wikipedia.org/wiki/B-Method[B-Method in Wikipedia]
-* http://www.bmethod.com/[B-Method Site] from ClearSy
-* http://www.fm4industry.org/index.php/Can_FM_tools_manage_large_industrial_problems%3F[Can
-FM tools manage large scale industrial problems ?]
-* http://www.data-validation.fr[Data Validation]
-
-[[prob]]
-== ProB
-
-* <<modelling-examples,Examples for ProB>> (along with screenshots and
-explanations)
-* http://www.ecs.soton.ac.uk/~mal/systems/prob.html[Old web page of
-ProB] (in Southampton; use for releases prior to 1.2)
-* http://www.fm4industry.org/index.php/Productivity_Improvement_of_Data_Consistency_in_Transportation_Models[Link
-to Success Story (written by Cetic)]
-* https://groups.google.com/d/forum/prob-users[prob-users group]
-
-[[tools-using-prob]]
-== Tools using ProB
-
-* https://www.clearsy.com/en/our-tools/clearsy-data-solver/[ClearSy Data Solver]
-* http://www.data-validation.fr/data-validation-in-the-railways/[DTVT -
-Data Table Validation Tool] for Alstom by ClearSy
-* OLAF data validation tool by ClearSy for Alstom and SNCF
-* Dave data validation tool by ClearSy for General Electric Transportation
-* https://github.com/plues/plues[PLUES] tool for university course
-validation
-* http://safecap.cs.ncl.ac.uk/index.php/Safecap_Project_Wiki[SafeCap]
-* http://wiki.event-b.org/index.php/IUML-B[iUML Statemachines]
-* http://users.ecs.soton.ac.uk/vs2/ac.soton.multisim.updatesite/[MultiSimulation
-Plug-In for Rodin]
-* http://www.beta-tool.info/user_guide.html[Beta]
-* http://www.macs.hw.ac.uk/~mtl4/Publications.html[HRemo (see PhD
-thesis)]
-* http://dx.doi.org/10.14279/depositonce-2502[Message Choreography Model
-Animation and Test Case Generation (see PhD thesis; Chapters 5 and 6)]
-http://link.springer.com/article/10.1007%2Fs10270-012-0272-x[SSM article
-(2014)]
-* http://b4msecure.forge.imag.fr[B4MSecure]
-* http://genisis.forge.imag.fr[GenISIS]
-* http://blog.aymericksavary.fr/?page_id=209[VTG] (Vulnerability Test
-Generator, see
-http://blog.aymericksavary.fr/wp-content/uploads/2011/10/presentation.pdf[Rodin
-Workshop 2012 presentation] and
-http://blog.aymericksavary.fr/wp-content/uploads/2014/06/Présentation.pdf[2014
-presentation])
-* CODA https://arxiv.org/abs/1305.6112v1[arXiv article]
-* There is also some intitial effort to
-http://pure.au.dk/portal/en/publications/interpreting-implicit-vdm-specifications-using-prob(19de7f9f-1d9a-483c-b2e7-285c0d0edc63).html[use
-ProB for implicit VDM specifications] presented at
-http://wiki.overturetool.org/index.php/12th_Overture_Workshop[the 12th
-Ouverture Workshop].
-* https://github.com/ValerioMedeiros/BEval[BEval]
-* https://github.com/ValerioMedeiros/BTestBox[BTestBox]
-* http://wiki.event-b.org/index.php/MBT_plugin[MBT plugin] for
-model-based testing within Rodin
-* https://rajivmurali.github.io/UsecasePro/[UseCasePro], see article in
-the
-http://eprints.ncl.ac.uk/file_store/production/229541/A4269E59-6B4A-485E-8E63-E164802DFADD.pdf[proceedings
-of the 2016 Workshop on Formal and Model-Driven Techniques for
-Developing Trustworthy Systems]
-* http://bibbase.org/network/publication/lausdahl-ishikawa-larsen-interpretingimplicitvdmspecificationsusingprob-2015[Animating
-implicit VDM specifications inside Ouverture]
-* http://www.ovado.net[Ovado] (as second tool chain)
-* https://github.com/tofische/cucumber-event-b/[Cucumber-Event-B] tool to run high-level tests
-
-[[related-tools]]
-== Related Tools
-
-* http://www.atelierb.eu/[Atelier B]
-* http://www.event-b.org/[Event-B and Rodin Wiki]
-(http://wiki.event-b.org/index.php/Rodin_Platform_Releases[Platform
-Releases], http://wiki.event-b.org/index.php/Main_Page[Documentation]),
-http://sourceforge.net/projects/rodin-b-sharp/[Rodin Sourceforge Site]
-* https://github.com/utwente-fmt/ltsmin/releases[LTSmin releases
-(including versions for prob)]
-* http://lifc.univ-fcomte.fr/~btatibouet/PERSO/JBTOOLS/InstallPlugIn/InstallPlugIn.html[jbtools]
-* http://www.b4free.com/[B4Free] tools for the development of B models
-* http://www.loria.fr/~cansell/cnp.html[Click n Prove]
-* https://github.com/edwardcrichton/BToolkit[B Toolkit]
-* http://www.ecs.soton.ac.uk/~cfs/umlb.html[U2B] UML to B translation
-tool
-* http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html[TLA+]
-(http://research.microsoft.com/en-us/um/people/lamport/tla/tools.html[tools
-for TLA+])
-* https://spivey.oriel.ox.ac.uk/mike/fuzz/[The fuzz type-checker for Z]
-* https://www.cs.ox.ac.uk/projects/fdr/[The FDR3 CSP refinement checker]
-* https://github.com/leuschel/bbedit-prob[BBedit Language modules for B,
-TLA+, CSP and Prolog]
-* https://en.wikipedia.org/wiki/List_of_model_checking_tools[Model
-checking tools]
-
-[[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
-great success. Thanks to the automatization and ProB, the wayside data
-validation is quicker, easier and complete." More details and academic
-papers can be found on our page
-<siemens-data-validation-with-prob,Siemens Data Validation with
-ProB>>.
-* http://dl.acm.org/citation.cfm?doid=2406336.2406351[Pacemaker model by
-Mery and Singh]: "ProB was very useful in the development of the
-pacemaker specification, and was able to animate all of our models and
-able to prove the absence of error (no counterexample exist). The ProB
-model checker also discovered several invariant violations, e.g.,
-related to incorrect responses or unordered pacing and sensing
-activities. It was also able to discover a deadlock in two of the
-models, which was due to the fact that “clock counter” were not properly
-recycled, meaning that after a while no pacing or sensing activities
-occur into the system. Such kind of errors would have been more
-difficult to uncover with the prover of RODIN tool.""
-* http://www.data-validation.fr/data-validation-reverse-engineering/[Reverse
-engineering using ProB at ClearSy]: "Data validation principles have
-been applied recently to a railways reverse-engineering project with
-great success. B and ProB have demonstrated again how efficient they are
-when used in combination."..."This problem was solved elegantly by
-using data validation principles: a B model representing the two graphs
-and their properties were elaborated, and ProB used for finding a
-solution."
-* http://www.ncl.ac.uk/computing/research/publication/197269[Safecap
-tool paper by Iliasov, Lopatkin and Romanovsky]: "One of the larger
-examples we have tackled is the Carlisle Citadel station with the North,
-South, and Caldew junctions. The modelled fragment is 2.6km long and
-comprises 70 train detection circuits, 63 points, 79 routes and 161
-valid paths. The translation from a scanned PDF drawing and printed
-control tables took 45 man-hours. The verification of the topology
-theory constraints using ProB took just over 6 minutes on a PC with i7
-3730 CPU and utilized just under 2GB of RAM. The Why3 verification of
-the same theory takes approximately 70 minutes. The control table theory
-is verified under 20 seconds by ProB and not verified completely, with
-the current translation of conditions, using Why3."
-* http://www.erts2014.org/Site/0R4UXE94/Fichier/erts2014_1B2.pdf[Innovative
-Approach for Requirements Verification of Closed Systems by Reis,
-Bicknell, Butler, Colley]: "The Event-B model can be animated within
-Rodin using the BMotion Studio tool, which is part of ProB. Using the
-tool, it is possible to generate an animated front-end to the simulation
-of the model in the form of a user-friendly graphical interface, which
-corresponds to the system’s GUI (see Figure 4). The user can interact
-directly with this animated front-end, while the tool continues to run
-the formal analysis in the background, reacting to user choices and
-checking the model and invariants at each step. This was utilised during
-the case study, to produce a representation of the GIU provided as part
-of the end-user system. As this graphical representation is tied to the
-underlying Event-B model, it can not only be used to run through the
-model and confirm that the model is the correct representation of the
-system, but can also be used to explore further scenarios. This
-graphical representation of the system can be used without necessarily
-requiring any experience with the Event-B language or the toolset."
-* http://dl.acm.org/citation.cfm?id=2480314[ProZ for Modelling Safety
-Properties of Interactive Medical Systems by Bowen and Reeves]: "In
-this paper we have shown how temporal logic and invariants describing
-safety properties of interactive medical devices can be investigated
-within the ProZ tool. We have given examples of checking for such
-properties against a model of the T34 syringe pump and discussed some of
-the results and challenges we have encountered using this approach. We
-believe that using techniques such as these, and other model-checking
-functionalities, contributes to supporting safer use of interactive
-medical devices. That is we can use such techniques not just to help
-develop better and safer systems (where such techniques are most
-typically used) but also, as we have shown here, to investigate existing
-devices to ensure they can be safely used within the clinical setting."
-* ProB has been used “out-of-the-box” for Rodin theories by Thales for
-railway interlocking models, building ProB BMotionStudio visualizations
-on top. According to the
-http://www.advance-ict.eu/sites/www.advance-ict.eu/files/Thales-Duesseldorf.pdf[Thales
-slides of the Advance Industry Day 2014] ProB has a high technology
-readiness level (TRL).
-* ProB
-http://smtcomp.sourceforge.net/2016/results-NIA.shtml?v=1467112059[wins
-the NIA (non-linear integer arithmetic) division of the 2016 SMT
-competition] (this is ProB out-of-the-box, without tuning and where SMT
-formulas are translated to B)
-
-[[other-links]]
-== Other Links
-
-* https://github.com/klar42/railground/[Railground Event-B Model]
-
-[[translating-to-logic]]
-== Translating to Logic
-
-* http://legacy.earlham.edu/~peters/courses/log/transtip.htm[Translation
-Tips]
-* http://pages.cs.wisc.edu/~dyer/cs540/notes/fopc.html[Lecture Notes on
-Translating to First-Order Logic]
-* http://cs.nyu.edu/faculty/davise/guide.html[Guide to Axiomatizing in
-First-Order Logic]
diff --git a/src/docs/chapter/user/ZZ_Appendix/06_ProB_Release_History.adoc b/src/docs/chapter/user/ZZ_Appendix/06_ProB_Release_History.adoc
deleted file mode 100644
index 5c863455f88de5697777da8c41c5c495478e0892..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/ZZ_Appendix/06_ProB_Release_History.adoc
+++ /dev/null
@@ -1,855 +0,0 @@
-[[release-history]]
-= ProB Release History
-
-Full ProB release history until release 1.8.3:
-
-....
-1.8.3-beta
- - size, ^, ->, <- do some well-definedness checks if TRY_FIND_ABORT is TRUE
- - operations view shows non-deterministically set variables also for
- subsidiary called operations
- - improve setting JAVA_PATH preference on Macs
- - performance improvements in kernel: intersection, STRING_JOIN, ...
- - new external function: BITS
- - allow Unicode to be used in projection diagrams
-
-1.10.2018: 1.8.2
- - allow deterministic trace replay to reduce memory consumption
- - fix potential variable clashes in nested B while loops with operation calls
- - improvements in kernel (improve symbolic treatment of set difference, avoid enumeration warnings
- for large but finite sets, ...)
- - improved error location detection for some error messages; provide possible alternatives for
- errors involving identifiers
- - support for loading Alloy models
- - improve pretty printing values in TLA+ mode
- - changes for external functions: DEC_STRING_TO_INT raises WD errors to avoid spurious error messages,
- improve READ_CSV to skip over empty lines
- - support /*@symbolic */ pragma for UNION
- - conversion to Unicode for B symbols in ProB Tcl/Tk Edit menu
-
-1.8.1-rc4 (not officially released)
- - support PNG images for ANIMATION_FUNCTION and ANIMATION_IMG, also look for images relative to
- the file in wich the ANIMATION_IMG is declared.
- Add horizontal scrolling for very wide visualizations and allow to scale visualization.
- Allow to specify font and size for strings (TK_CUSTOM_STATE_VIEW_FONT_NAME/_SIZE)
- - allow to choose dot layout engine via DOT_ENGINE preference
- - support Atelier-B's "ref" keyword in Event-B (.sys) models
- - better error messages for unknown identifiers (fuzzy matching and completion checking)
- - support Jupyter kernel https://gitlab.cs.uni-duesseldorf.de/dgelessus/prob2-jupyter-kernel
- - executing operations by predicate can now also specify post-conditions (e.g., on non-deterministically
- assigned variables)
- - CUSTOM_GRAPH_EDGES and CUSTOM_GRAPH_NODES can provide shape information and a much wider range of Tk/dot colours.
- - add CODES_TO_STRING, HASH, ... external functions in LibraryStrings.mch
- - improved error location feedback for expressions involving (nested) DEFINITION calls
- - improvements in kernel (detection of infinite sets, symbolic treatments of set difference, ...)
- - reduce console output in -silent mode
- - add optional ndjson error logging via NDJSON_ERROR_LOG_FILE preference
-
-20.03.2018: 1.8.0
- - add terminal colour output in probcli, can be disabled by setting NO_COLOR environment variable
- - improved performance of evaluation/state views in UI for large values
- - changed treatment of reflexive closure: now corresponds to the more usual
- mathematical definition: closure(X) = id(TypeOfX) \/ closure1(X)
- The previous definition closure(X) = id(ran(X)\/dom(X)) \/ closure1(X) and
- the definition in Atelier-B closure(X) = id(dom(X)) \/ closure1(X)
- are not compatible with the following law in the B-Book on page 169
- (r[a] <: a => closure(r)[a]=a)
- Note that closure({1|->2}) and iterate({1|->2},0) are now infinite.
- - improved constraint solving for closure/closure1 operators
- - static symmetry breaking uses partition predicates of deferred sets
- - allow LET expressions and predicates to introduce multiple, dependent identifiers in order
- (for LET substitutions this is only allowed if the preference ALLOW_COMPLEX_LETS is TRUE)
- - TYPE_CHECK_DEFINITIONS preference to type check definitions (also unused ones)
- - improved static checking for INITIALISATION order
- - add preference DETECT_LAMBDAS to detect set comprehensions that can be transformed into lambdas
- - added bitwise external functions in LibraryBits.def
- - add TYPED_STRING_TO_ENUM, SLEEP external functions
- - added random_subset and random_permutation external functions in LibraryRandom.def
- - improvements in constraint solving kernel, e.g., total function checking for range
- - allow to replay JSON trace files and to export to JSON trace files in ProB Tcl/Tk
-
-05.10.2017: 1.7.1
- - new feature to export history to HTML file with graphical visualizations
- - improved presentation of quantifiers in Tk Evaluation View
- - improved presentation of non-deterministically assigned variables in operations view
- (shown first for INITIALISATION, more variables shown for variables without parameters
- and return values)
- - made Z operation schema detection more flexible: schemas which work on part of
- the variables are allowed and extended to schemas which do not change the other variables,
- allow custom execution of Z operations by parameter values, improvements in kernel for Z types,
- allow opening .zed files in addition to .tex files
- - performance improvements in kernel
- - added SOLVER_STRENGTH preference (to increase strength of propagations for large
- sets, for reification of quantifiers, ...)
- - external predicate SCCS for computing strongly connected components
-
-11.07.2017: 1.7.0
- - ProB now assumes strings, machine files,... are all encoded using UTF-8
- - first (limited) support for VALUES clause for constants
- - printf, PRINTF now take a B sequence as arguments (e.g., printf("~w -> ~w",[2,3]))
- - result parameters of B operations can now also be read, as in Atelier-B
- - Warnings for potential variable captures of DEFINITIONS are issued
- - Parser now uses socket communication instead of standard input/output
- - Parser supports RULE DSL language for easier data validation
- - ALLOW_LOCAL_OPERATION_CALLS preference added, resulting in a topological
- sorting of the operations in a machine
- - improve RANDOMISE_ENUMERATION_ORDER for sets and for order of variables
- with same type priority
- - improve symmetry breaking for record variables and set extensions
- - speed up KODKOD predicate analysis
- - many improvements in kernel (UNION for singleton sets, member for domain/range restriction/subtraction,
- detect useless quantifiers, ...)
- - new external functions (WRITE_XML, INT_TO_DEC_STRING, STRING_CONTAINS_STRING, SHA_HASH, ...)
- - Tk graphical visualization can now react to clicks (ANIMATION_CLICK and ANIMATION_RIGHT_CLICK Definitions)
- - new features for Latex mode: LATEX_GREEK_IDENTIFIERS preference, better dot support, ...
- - some sequence operators can be applied to STRINGs (when preference STRING_AS_SEQUENCE set to TRUE)
-
-20.10.2016: 1.6.1
- - Parser supports IF-THEN-ELSE and LET without parentheses,
- IF-THEN-ELSE also allowed inside predicates
- - add -latex command to process Latex files and integrate B/ProB results
- - add -logxml FILE command to log probcli commands and result to XML file
- - add performance message logging
- - improvements in ProB kernel: AVL set-membership using CLPFD table constraint,
- function application of partially known function using CLPFD element constraint,
- better reification for quantifiers, better WD detection, better if-then-else
- solving, performance messages
- - add READ_XML external function to read in XML files and READ_CSV for files in CSV format
- - add LibraryMeta external functions to inspect ProB and model state
- - improve Kodkod backend: support more cardinality constraints, add preferences
- KODKOD_SAT_SOLVER, KODKOD_SYMMETRY, KODKOD_MAX_NR_SOLS, KODKOD_RAISE_WARNINGS
- - improvements in LTSMin bridge (guard splitting, partial order support)
- - improve pretty printer: prints fewer parentheses
- - better static name clash checking
- - add :replay FILE command and :list command to probcli -repl
- - fixed highlighting of syntax errors in ProB Tcl/Tk under Windows
- - improve Atom editor support: provide full error spans
- - add Definition call graph visualisation
- - add -dot Diagram File and -dotexpr Diagram Expr File commands for probcli,
- possible values for -dotexpr Diagram : expr_as_graph, transition_diagram
- possible values for -dot Diagram :
- machine_hierarchy, event_hierarchy, state_space, signature_merge,
- dfa_merge, state_as_graph, invariant, properties, assertions, deadlock,
- goal, enable_graph, dependence_graph, definitions, ....
-
-22.04.2016: 1.6.0
- - Parser supports full range of Atelier-B Unicode symbols for classical B machines,
- better support for /*@label LBL */ pragma,
- new description pragma /*@desc DESC */ following predicates or identifiers,
- line comments now supported: // line comment
- more precise error location within DEFINITIONS,
- improved error messages for certain common mistakes (extra & or ;)
- leaner error messages without duplicate information about location
- fixed bug on Windows concerning transfer of error messages (e.g., no error locations were displayed)
- - support for the Atelier-B tree operators
- - parser and ProB support using IF-THEN-ELSE and LET for expressions (have to be surrounded by parentheses)
- - directed model checking available: -mc_mode M with M:{hash,heuristic,random,breadth-first,depth-first,mixed}
- - new probcli command -disable_timeout to disable time-outs in model checking and animation
- (also results in performance improvements when time-outs not needed)
- - new commands in probcli REPL:
- :find LTL_Atomic_Property
- :source and :origin to get information about identifiers
- :e to open source file in external editor (and show error in Vim, Atom, BBedit,...)
- :kodkod E to evaluate formula E using Kodkod
- - Tk Coverage Table for expression accepts optional filter property (LTL atomic property)
- - added Event Refinement Hierarchy Diagram (Visualize Menu in ProB Tcl/Tk),
- state as dot graph diagram can represent records,
- added scalable force directed (sfdp) visualization of state space
- - ProB Tcl/Tk now has repeat last menu command (Cmd-Shift-R)
- - Rodin Disprover checks for inconsistency in hypothesis in case proof found
- (unless DOUBLE_EVALUATION preference is set to false)
- - improvements in kernel (better detection of identical predicates, symmetry breaking
- for X in card(X)>Nr, improved ground checks, improved constraint propagation for image,
- -->> / +->>, >->>, records containing infinite sets, (non-)emptiness checks of set comprehensions,
- improvement for quantifiers involving domain/range,...)
- - some static symmetry detection for universal and existential quantification (for first two identifiers)
- - improvement in memory consumption for storing state space
- - CSE deals correctly with associativity and commutativity, fixed issue with computing
- WD-guarded shared predicates
- - ProZ is more flexible in detecting initialisation schemas (containing Init in name),
- improved Z syntax highlighting, Z integer division is now floored division
- - guards embedded within Classical B actions are used in evaluation view and for enabling analyses
- - added CSV reader external function
- - more stringent static checking of LET substitutions
- - new symbolic model checking commands
- - Z3 interface available (use :Z3 predicate in REPL)
- - probcli supports dash (-) instead of underscore within commands
- - type checker can sometimes give hints (adding {.} for relational image, using |-> instead of ->,...)
- - $0 variable suffix can now be used within DEFINITIONS (PARSERLIB-47)
- - SETUP_CONSTANTS and INITIALISATION shown names of constants and variables in operations view
- - model checking test-case generation (-mcm_tests) xml files now include operation parameters
-
-19.02.2015 : 1.5.0
- - improved RANDOMISE_ENUMERATION_ORDER preference (many more enumerations can
- now happen with random ordering of elements)
- - improved constraint solver: e.g., partitioning of predicates into components
- can now inline simple equalities
- - added MACE/SEM style static symmetry reduction for constants element of deferred sets (<<symmetry-reduction,Symmetry Reduction>>)
- - improved prover/disprover capabilities; added -cbc_result_file FILE and -cbc_assertions_tautology_proof
- commands to probcli; probcli can now load PO files generated by
- ProB Rodin plugin and some SMTlib files (.smt2 extension)
- - added first version of Common-Subexpression-Elimination (CSE)
- - added bounded model checking command -bmc to probcli (<<bounded-model-checking,Bounded Model Checking>>)
- - cbc_tests has additional options: -cbc_cover_match E to match all events where E occurs
- in the name, and -cbc_cover_final to specify that all target events should only be
- used as final event in test cases (this option is also available in the Tcl/Tk dialog)
- - reduce memory consumption of CTL model checker
- - CTRL-C now works within probcli (in particular REPL)
- - added Tree View for CBC Tests in ProB Tcl/Tk
- - improved performance of CBC Test case generation using feasibility analysis and more enabling
- analysis results
- - added feasibility analysis (-feasibility)
- - added MC/DC coverage analysis for guards and invariants
- - added -scope PRED command
- - added -all_paths FILE command
- - the LTL model checker now supports fairness and deadlock and determinism properties
- - improved TLC interface: better replay of traces, features to set number of workers,
- enable symmetry detection and use ProB to set up constants
- - Parser now looks in stdlib folder for included machines/definition files; the
- ProB external function library machines come bundled with ProB in this way; the folder
- can be set via the PROBPATH environment variable
- - removed different parsers, removed preferences regarding
- parsers. Now, the Java parser is just with sane defaults as the only option.
- - switched to SICStus Prolog 4.3
-
-18.08.2014 : 1.4.0
- - Tcl/Tk new commands: find relative deadlock, find controller state violation,
- Value Coverage (evaluate expression over whole statespace; possible CSV export),
- evaluate expression over history
- - Tcl/Tk: re-organize the menus and improved progress bar for model checking
- - new command: evaluate expression over history and save as CSV (-csvhist in probcli or right-click on history in Tcl/Tk)
- - CLPFD now turned on by default; improvement in some default preferences (editor on Mac,...)
- - ProB now knows whether enumeration warning were triggered for computing enabled operations; in Tcl/Tk an orange "infinity" symbol lights up if this occurs
- - improved treatment of enumeration warnings for infinite sets
- - better enumeration strategy for large or infinite domain variables (trying to defer their enumeration)
- - improved detection of infinite set comprehensions, which are kept symbolic
- (e.g., {x,y,z| x*x + y*y = z*z} or {x,y,z| z:seq(NATURAL) & x^y=z} are
- now automatically kept symbolic)
- - the kernel can treat more operations symbolically, without the need to expand set comprehensions: composition ;, override <+, set difference and intersection
- - TLC can be used as external model checker for classical B machines in Tcl/Tk
- - additional external functions: ARGV, ARGC to provide command-line arguments to B machines, STRING_TO_ENUM,
- READ_LINE, EOF, ...
- - B machines can now be executed on Unix machines by using first Shebang line: #! PATH_TO_PROBCLI
- - bug fixes in the kernel (mainly relevant in SYMBOLIC mode)
- - bug fix in Event-B record detection for records with more than two fields
- - REPL of probcli and ProB Tcl/Tk allows definitions of auxiliary variables using let X = Expr, added other commands like :b for browse of definitions,...
- - probcli -repl now also accepts CTL and LTL formulas (with $ctl or $ltl prefix) and
- it is possible to pretty print the B formulas in Unicode
- - bug fixes in Tcl/Tk REPL (copy&paste) + Evaluation View uses Unicode
- - variants and theorems in guards are shown in Evaluation View and ProB for Rodin state view
- - improvements in constraint solver: domain, range, -->>, partition detection inside machines, ...
- - constraint-based refinement checking
- - Tcl/Tk GUI improvements: double click in History to go back
- - performance improvements, in particular for WHILE loops
- - control-flow graph and enabling analysis
- - new -execute command with filtering of unused constants, faster than -animate (does not store intermediate states)
- - improved performance of constraint-based test-case generation algorithm
- - Graphical Visualisation: allow multiple ANIMATION_FUNCTION[0-9]*, allow them in XTL mode, support for more animation functions: showing textual representation of values if not integer or no image or string available, support for ANIMATION_STR_JUSTIFY_LEFT and ANIMATION_STR_JUSTIFY_RIGHT
-
-01.03.2013: 1.3.6
- - improved constraint propagation for modulo and division
- - new format for .eventb files generated from ProB-Rodin; contains well-definedness
- condition information and fixes issue where model checker with Proof Info was unable
- to find certain invariant violations after an undefined invariant was encountered
- - probcli model checker (-mc) now also checks all states that were previously visited
- by other commands such as trace checking (-t)
- - other minor constraint propagation improvements ({x,y,..} <: 1..n supported better,...)
- - various performance improvements (e.g., in Event-B removed redundant checking for
- extended events)
- - prj1(A,B)(x,y) --> it is now checked that x:A and y:B; same for prj2; this can be overridden by setting the IGNORE_PRJ_TYPES preference to TRUE
- - CASE statement static checking for classical B has become more stringent: we require
- that all cases are literals (to be compliant with Atelier-B)
- - Eval console (both in probcli and ProB Tcl/Tk) now works with Kodkod (if Kodkod enabled);
- various bug fixes and improvements in the Kodkod translation
- - reduced statespace and DFA statespace now also works in CSP-M mode
- - Eval console now also supports deferred set identifiers generated by ProB
- - Tk REPL improvements: command-backspace clears, fix in copy&paste behaviour
- - bug fix in ProB kernel; solutions could be lost in context of bool(.)
- - improved Model Checking dialog: progress bar, number of checked nodes kept track of, ...
- - constraint-based refinement checking, enabling analysis, test-case generation available in expert mode of Tcl/Tk
- - new view neighbourhood in state space command
-
-30.09.2012: 1.3.5
- - performance improvement in model checking and constraint solving (CLPFD mode)
- - constant and operation value caching using the -cache DIRECTORY option
- - new Kodkod backend; enable using -p KODKOD TRUE in probcli or Preference menu in ProB Tcl/Tk
- - CSP|||B supports sequences and sets and performs (limited) static checking
- that synchronisation channels are properly typed
- - support for pragmas, e.g., /*@ symbolic */
- - first version of physical unit inference and checking plug-in
- - support for external functions (currently only those coded in Prolog)
- - improved detection of infinite functions (e.g., disjunctions of lambda expressions
- recognized as infinite if one of the disjuncts is)
- - support for recursive functions
- - support for the Event-B finite operator; within classical B the construct S:FIN(S)
- is recognized as equivalent to finite(S)
- - in addition to application f(x), we can now also compute the image f[S] and
- the composition (R;f) for an infinite function f; provided S and R are finite.
- - support for TLA, TLA2B translator can be installed from within Tcl/Tk version
- - improved default hash on 64-bit systems
- - Eval window now also recognises strings + faster syntax highlighting,
- multiline comments highlighting on the fly; added more contextual menus in editor
- and other panes
- - improved "Current state as graph" display, grouping deferred and enumerated sets
- - many new options for probcli, see <<using-the-command-line-version-of-prob,Using the Command-Line Version of ProB>>
- - many more tests, bug fixes, performance improvements
-
-21.11.2011: 1.3.4
- - Evaluation view (requires Tcl/Tk 8.5) providing hierarchical view and inspection of VARIABLES, CONSTANTS, INVARIANTS, PROPERTIES, ...; possibility to inspect complete value by double-clicking; possibility to save values of CONSTANTS and VARIABLES to file
- - Eval window allowing to enter expressions and predicates for B, CSP, and Z (albeit B syntax has to be used when querying Z); can be opened by either double clicking in State Properties pane or menu command Eval... in Analyse menu.
- - improved editor: current line number display + line numbers can be shown left, continuous syntax highlighting, parentheses highlighting
- - support for CSP exception operator
- - new feature: CSP in-situ refinement checking, divergence, determinism
- and deadlock checking,
- CSP assertions are parsed and can be checked,
- new dialog box (inspired by FDR GUI) for checking CSP assertions in a file
- - source code highlighting of well-definedness errors (does only highlight in the main file at the moment)
- - the Analyse -> Analyse Predicate commands provide feedback when infinite sets (such as NATURAL) had to be expanded
- - 64-bit version for Mac available, faster, better hashing + more memory available
- - usage of SICStus 4.2; hopefully fixing issues with CLP(FD) crashes,...
- - many improvements in constraint solving kernel
- - improved performance of hash symmetry markers: reduction in size + performance
- improvement
- - improved feature: constraint-based invariant checking
- - new feature: constraint-based sequence checking (in Verify -> Constraint-Based Checking menu)
- - added possibility to specify an animation function in Z, too
- - we allow the usage for x$0 in while loop invariants
- - bug fixes in CSP-M, ...
-
-10.2.2011: 1.3.3
- - new feature: constraint-based deadlock checking
- - improved debugging of unsatisfiable PROPERTIES: ability to minimise (computing unsat core)
- - improved boolean constraint solver, smt preference for reification of membership predicates
- - improved usage of CLP(FD) solver, added reification for certain predicates
- - updated parser to priorities in french version of Atelier B manual (priorities in english manual are wrong)
- - improved performance when displaying long counter examples (>10,000 steps)
- - record detection (compatible with Rodin Records plugin when using closed records; but also
- works with hand-coded records); improved treatment of some infinite sets
-
-30.7.2010: 1.3.2
- - Many improvements for Z mode: bags supported + many more Z operators ...
- - 64 bit version available for LTL model checker, nauty library
- - PROPERTIES are partitioned: better performance + debug feedback in case of inconsistency
- - complement sets (INTEGER - S) can sometimes be represented symbolically
- - ProB detects WD-error in some cases when card(.) applied to infinite set
- - integration of CLP(FD) solver for integer values
- - improved kernel performance for many kernel predicates, better waitflags store, optimized treatment for SIGMA(ID).(ID:SET|EXPR), and the same for PI
- - improvement in many B operations for large sets/relations (especially involving intervals)
- - optimized forall treatment now also available for multiple variables: !(x,y).(x|->y:SET => P)
- - model checker/animator can make use of previously computed operation effects
- - time-out per operation in B
- - exhaustive kernel checks: much more unit tests + some fixes
-
-Dec 2009 : 1.3.1
- - coloring of enabled operations: blue: skip operation; green: leads to open node; red: leads to error node
- - added option to force depth-first in model checker
- - timeout for invariant violation properly shown in status bar
- - improved inference of minimum required cardinality of deferred sets; certain constants are automatically added as if we had a partially enumerated set (performance improvement + better readability in animations)
- - detection of witness errors in multi-level animation mode for Event-B; many improvements to multi-level animation
- - well-definedness errors are stored along with the state and shown in the Properties Pane
- - adapted treatment of CSP interrupt operator, now conformant with ProBE (based on page 72
- of Steve Schneider's book, Concurrent and Real-time Systems)
- - support for Rodin 1.0 id, prj1, prj2, partition operators
- - support for Atelier B .sys files, SYSTEM & EVENTS keywords (not yet VARIANT, WITNESS)
- - added forward/backward buttons
- - added option to use constants for deferred set elements in DOT view
- - improved displaying of .eventb models in classical B style
- - Execute Specific Operation ... works again and now can also be used to guide machine
- initialisation and setting up of constants
- - improved treatment formulas of the form: !x.(x:SET => PRED)
- - performance improvements insided the kernel (Siemens San Juan case study: went from 17 minutes to 5 minutes; CruiseFinite1 went from 12 seconds to 5 seconds).
-
-March 20,2009: 1.3.0
- ProB 1.3.0-Final is available for download. Highlights: New parser and integrated typechecker, install as AtelierB plugin, improved kernel with support for large sets/relations, improved CSP support, faster LTL model checker, Undo/Redo in text editor, graphical formula viewer, user definable custom animations with gifs.
- - improved performance of signature-merge and DFA reduction viewing
- - added support for let (a,b,c) = E style expressions in CSP
- - added possibility to link Event-B models with CSP
- - can now animate .eventb files generated from Rodin EventB models
- - added parallel product
- - added AVL representation for more efficient representation of large sets
- - added new phase of kernel to priortise computation with fully known values
- - added support for STRING datatype (enumeration still limited to {STR1,STR2})
- - improved internal representation for BOOL type
- - speed improvement inside the B kernel
- - improved handling of abort conditions (application of function outside domain,
- division/mod by 0, first/last/... of empty sequence)
- - improved hashing inside model checker
- - graphical visulisation of INVARIANT and operation preconditions
- - added user-definable custom .gif Animation via ANIMATION_FUNCTION, ANIMATION_IMGn, and
- ANIMATION_STRn declarations in the DEFINITIONS section
- - added support for lambda expressions and currying, not yet fully tested
- - added nametype and subtype support for CSP
- - fixed a problem when using dotty viewer in Windows for B machines/CSP specs whose
- paths contained spaces; updated the dotty defaults, added new colours and shapes
- - PRE conditions of operations are propagated down to refinements and implementations if
- possible (that is, a conjunct is propagated down if the variables it refers to also
- exist in the refinement/implementation)
- - While loops: Invariant now also checked upon loop exit; multiple assignments to same
- variable also checked for INITIALISATION
- - Menu Command Key shortcuts now work
- - fixed bug with x::NAT1,...
- - added (partial) type checking on substitutions and highlighting of type (and some other errors)
- in the source code; reduced number of error messages when type errors occur
- - LTL model checking for all platforms, improved C-version (1-2 orders of magnitude faster)
- - LTL formulas with patterns
- - possibility to define LTL Assertions in the DEFINITIONS clause and command for checking them
- - more CSP-M features (records, recursive datatypes, tuples, non-associative tuples,...)
- - Debug Operations... command in Analyze menu
- - bug fixes in kernel (NatRange, empty closure sets,...)
- - moved to SICStus 4.0.2 (a bug in earlier version of SICStus could affect ProB with
- sets of sets in some circumstances)
- - improved type inference ( x|->y|->z : SomeRel,...)
- June, 2007: 1.2.7
- - LTL Model checking (only works in Sicstus4 built binaries)
- - move to Sicstus4 on Mac and Linux: no more 256 MB limit!, speed improvements in
- model checker (currently slow down in animation when things get printed on screen
- due to a problem in Sicstus4)
- - Almost fully CSP-M (FDR) compliant parser and animator; dropped support for old CIA-CSP
- syntax; visual highlighting of channel outputs (when single clicking on enabled operations in Pane)
- - Refinement checking for CSP-M, taking tau actions into account
-
-March 8, 2007: 1.2.6
- - added support for parameter passing to Included/Imported/... machines
- - added support for machine renaming (e.g., INCLUDES c1.M, c2.M)
-
-February 16, 2007: 1.2.5
- - a new, improved version of ProZ included
- - incorporated fuzz binary in ProB distribution (thanks to Mike Spivey)
- - added timeout feature + preference
- - added buttons for timeout, max. nr of operations reached and invariant violation
- - improved partial function/surjection/... so that infinite domains can be dealt with
- properly without expansion (NATURAL, NATURAL1,... closures,...)
- - added support for iterate(r,n) operator on relations
-
-December 4, 2006: 1.2.4
- - added support for WHILE loops and IMPORTS in Implementations
- - improved mixed DF/BF search (especially for infinite state spaces)
- - added support for pred,succ applied to numbers
-
-November 22, 2006: 1.2.3
- - added check for cyclic dependencies in machine hierarchy + check for
- multiple inclusions; added topological sort to determine correct
- initialisation order (before all initialisations were executed in
- parallel; now a machine can use the values of variables in used/included/seen
- machines for its own initialisation)
- - struct can be used for Struct
- - added graph canonicalisation option in Advanced Preferences
- - added symmetry markers in Advanced Preferences
- - fixed normalisation for set_up_constants
- - improved type inference when enumerated elements of SETs used
- - debug properties now shows SETS sizes and MININT and MAXINT
-
-October 2, 2006: 1.2.2
- - added a debug PROPERTIES feature; accessible when setting up of constants
- fails
- - added support for B4Free EventB syntax: MODELS in place of MACHINE
- and WHEN P THEN A END in place of SELECT P THEN A END
- - prj1,prj2 can now be used freely (before could only be used when applied
- directly to arguments)
- - added support for ASSERT P THEN S
- - improved type inference for explicit sets and sequences (x = {1,2} is now typed);
- or, => and <=> are also traversed
- - added menu command to view operation and their variable dependency as a graph
- - fixed type inference issue for Refinement machines
- - rearranged ProTest submenu
-
-August 31, 2006: 1.2.1
- - fixed bug in type inference (occured in some circumstances with closures
- containing operators * and - [where ProB is not sure about the type
- until the operands are known])
- - added error messages for Type Errors when comparing two objects for
- equality
-
-August 24, 2006: 1.2.0
- - CSP,XTL files can now be opened from the Open... command and are added to
- the Recent Files history
- - improved refinement checker in presence of constants: intialisation and
- set_up_constants get merged for refinement check
- - allowed parameters of type "element of SET" and BOOL
- - added support for MAXINT, MININT in expressions
- - NAT is treated differently from NATURAL (i.e., ProB checks that < MAXINT);
- same for INT and INTEGER
- - added view state as graph
- - added permutation reduction
- - new jbtools parser:
- - fixed performance problem
- - support for function application with multiple args f(a,b) instead of f(a|->b)
- - support for definitions with arguments
- - support for records: Struct, rec, '
- - support for some Event B syntax: SYSTEM, EVENTS, INITIALIZATION
- - added option to view top-level ANY arguments of EVENT B operations
- as arguments
-
-February 24, 2006: 1.1.9
- - fixed a problem whereby multiple variables in Set comprehensions, Lambdas,...
- were incorrectly bracketed: {x,y,z| ...} now generates couple(couple(X,Y),Z)
- terms rather than couple(X,couple(Y,Z))
- - CartesianProduct is now also kept symbolic (in addition to other basic types)
-
-February 14, 2006: 1.1.8
- - fixed a bug in the parser whereby some syntax errors lead to a looop
- in the Tcl
- - improved the treatment of universal quantification: if the condition
- of the quantification only has typing information then the forall is not
- delayed but expanded straight away, example:
- !(rr, ss) . (rr : ROAD & ss : RouteElement =>
- connectsAt(rr |-> ss) = {1})
- - added the support for recursive closures and functional style programming
- using set comprehensions:
- fact4 = {x,y| x:NAT & y:NAT & (x=0 => y=1) & (x>0 => (y=x*fact4(x-1)))} &
- fact4: INT <-> INT
- - improved treatment of existential quantifiers: they no longer cause unnecessary
- enumeration and can now be used inside lambda expressions and set comprehensions
- for local variables without much overhead
- - fixed a problem in the kernel where symbolic closures were prematurely
- expanded
- - CSP/B Integration: fixed a problem whereby arguments from the CSP were not
- passed directly to the B interpreter (i.e. unification was applied after
- computing the B operational semantics, resulting in unnecessary work).
- - improved type inference for refined machines: type inference for operation
- arguments will be applied at all levels and results merged
- - added the advanced option to ignore hash collisions
-
-September 23, 2005: 1.1.7
- - added the possibility to hide the B Source Pane (Animation preference)
- - added the option to treat outermost PRE conditions not as SELECT, but
- as PRE which can abort; abort state now leads to invariant violation
- - the preference file is now loaded/saved in the home directory if the
- applications' preference file is not writable
- - added the modulo operator "mod" to the CSP syntax, fixed problem that
- arguments to == and != were not evaluated
- - added "New..." command to File menu
- - added Files menu; allow to edit related Machines + CSP file
- - improved typing for refinement machines: types is obtained from
- ancestor machines as well
-
-June 16, 2005: 1.1.6
- - improved handling of set comprehensions when not kept as closures
- (also uses b_compiler.pl to reduce the number of variables one has to wait on)
-
-1.1.5
- - improved single failures checking (dramatically when non-determinism large)
- - made trace checking more flexible for setup_constants
- - fixed bug which prevented use of sequences in expressions such as xx:: seq(S)
-
-March 18, 2005: 1.1.4
- - boolean values are now displayed TRUE/FALSE (rather than true/false as before)
- - fixed bug for nested PRE's (jbtools parser does not allow them anyway; but
- one can tweak the XML files to obtain them)
- - added option in CSP (when guiding B) to query value of B variables and constants
- - improved animation for large sets/functions, improved type inference for
- equalities
- - allowed B machines to have no state and no initialisation
- - ability to select operations and arguments for reduced state view
-
-December 13, 2004: version 1.1.3
- - speed improvement: typing for operations is now cached
- - bug fix in Analyse Properties (ProB would claim no properties exist even though
- there was a properties clause)
- - better type extraction: types can now be extracted from equalities (e.g. x = 2..5)
- - improvements to refinement check: on the fly checking is possible, better
- detection when ancestor machine is not completely explored,
- new refinement check dialog box with better feedback,...
- - improvements to CSP guide: error channel (error-> ... is detected similar
- to invariant violation by the model checker), constants from global SETs
- can be used in CSP,...
-
-August 19, 2004: Version 1.1.2
- - ProB now remembers when not all transitions were computed for a node
- (because the max number of enablings or initialisations in the preferences
- is set too low); feedback is provided after model checking or in compute coverage
- - the LET x BE x=E IN ... END statement is now supported
- - added support to animate CSP files, with a brand new parser, and added the
- option to guide B machines using CSP files
- - fixed problem in error_manager where displaying error_messages (with
- clpfd variables or integers) could cause a type error exception
-
-July 29, 2004: Version 1.1.1
- - Windows version now compiled against Tcl Tk 8.4
- - fixed bug for recent documents list when file name contains spaces;
- Note: on Windows file names with spaces can still cause problems when
- viewing with dotty (but using PostScript viewer seems to work)
- - added advanced Find (allowing to redefine GOAL predicate)
- - Viewer: added option to colour nodes which satisfy GOAL
- - added a new view option: subgraph which can reach invariant violation
- - improved initialisation in presence of parts that cannot be satisfied
- (i.e., initialisation will succeed partially and user gets better feedback about
- what went wrong)
- - fixed bug in find_non_resetable_node when constants were present (only states after
- set_up_constants were marked as initial, but not those after initialise_machine)
-
-July 2, 2004: Version 1.1
- - added Recent Files list
- - ProB now finds out its own directory to locate the icons and .jar files; it should
- no longer be necessary to change into the ProB directory before executing the binary
- - fixed a bug whereby execute_trace_to_node could lead to the wrong node in the
- presence of non-determinism (e.g., model checking could present a correct counter
- example trace but leading to a wrong node, i.e. one satisfying the invariant)
- - added an option to open ProB in a small window (useful for dataprojectors)
- - added reduced state space viewing options
-
-June 16, 2004: Version 1.0.6
- - ProB now supports CHOICE with more than two choices
- - added simple type error detection at runtime for arguments of operations +
- some type checking for operation arguments, variables, constants
- - trying to assign to constants is detected and an error raised
- - added support for calling operations that return values: yy <-- CalOp(...)
- - improved enumeration for TotalFunction
- - added menu item "Refinement Check agains Ancestor" + added single failures refinement option
-
-May 11, 2004: Version 1.0.5
- - added support for ASSERTIONS clause (can be analysed in Analyse menu, can
- be searched for in Temporal Model check + can be checked using Constraint Based
- Checking)
- - fixed problem where multiple edges could be drawn (if print_self_loops=true)
- - added support for partial bijection (>+>>)
- - added improved treatment for size(Seq) if Seq is var and size known
-
-March 31 2004: Version 1.0.4
- - fixed bug whereby "not( xx : EXPR)" could loop if EXPR was not
- a basic expression (such as POW, ...)
- - added option to open external editor
- - added option to export to Promela/Spin
- - added option to export to CSP/FDR
- - fixed the problem with spaces in path for dotty, PS Viewer, ...
- - added menu command to analyse Properties + show inferred typing information
- - adapted menu structure so that on Mac it appears in the top menu bar (and not within
- the Windows; thanks to Mauricio Varea for doing this).
-
-March 26 2004: Version 1.0.3
- - added support for VAR v1,...vn IN ...
- - fixed a bug in the type extraction which would somtimes remove expressions with
- SetMinus in it (e.g., xx:POW(A-B) would extract a type for xx but the expression
- would be incorrectly removed).
- - allowed perm(.) to be used in other contexts than xx : perm(.) in non-symbolic mode;
- the same will be done for other sequence constructors.
- - the full detail of a syntax error can now be inspected
- - fixed a bug in Image of Relation (could generate multiset rather than set)
- - fixed equal_object + not_equal_object so that it works on two closures
- - option to view the conjuncts of the invariant that have been filtered (because
- of abstract variables in ancestor specifications that are no longer available in
- the current machine)
-
-March 23 2004: Version 1.0.2
- - added support for direct product ><
- - fixed problem with dot graphical viewer if display leaves was set to false =
- added new option to not view self-loops
- - prevented lazy expansion for CartesianProduct (as the parser cannot distinguish
- CartesianProduct from multiplication, this would sometimes lead to problems;
- in the long run this will be fixed more systematically by a better type inference)
- - fixed a problem with 'Minus' (sometimes the jbtools parser indicates integer minus but it is
- actually SetMinus)
- - variables given a type but not declared in VARIABLES are now reported (same for Constants)
- - better support for Refinement (SETS and Constants are now properly imported) +
- Invariant is imported from ancestor machine(s) and filtered
- - added platform specific preferences (for PS viewer,...)
- - fixed bug in kernel that could spuriously produce ill-typed instantiations (term(_))
- and lead to warning messages being printed (not_equal_object)
-
-March 16 2004: Version 1.0.1
- - ProB now recognises when a variable is not initialised (rather than failing
- and saying the machine cannot be initialised)
- - ProB now remembers the latest directory for opening (fix for Windows)
- - Paths in the preferences can now be "Pick"ed (but we still need to address
- a problem with paths containing spaces: for the moment all paths should
- not contain spaces otherwise ProB will not be able to call the auxilary
- programs)
-
-March 15 2004: Version 1.0.0
- - added a Beginner mode for ProB + made several menu commands more robust
- - new, improved menu structure
- - added a B Syntax summary sheet in About menu
- - model checking now puts the trace into the history
- - improved type extraction for ANY + error message displayed if no typing
- - added support for EXTENDS
- - added colour syntax highlighting
- - allowed simple editing and saving of B Machines
- - added highlighting of syntax errors
- - small bug fix for union_generalized (over sets of sets)
- - added support for conc(ss) (concatenation of sequences of sequences)
- - added generalized union and intersection over predicates: UNION(gg).(cond|expr) and INTER(gg).(cond|expr)
-
-February 2 2004: Version 0.9.8
- - added first support for multiple machines (USES, INCLUDES, SEES, PROMOTES)
- but without renaming and visibility checking
- - added an option to view the module hierarchy of multiple machines
- - added Safes_Chapter10 sample machines from Steve Schneider to test out the above
- - added lazy symbolic closures for binary type constructors (-->,...)
- - added support for <-> inside expressions (rather than as type)
- - replaced error message for /|\ prefix by warning (in AtelierB it is ok to have index > size of sequence)
- - added preference option to turn on/off lazy symbolic closures
- - fixed several bugs related to symbolic closures not being expanded,...
- - added support for type checking in expert mode only for the moment
- - bug fixes for symbolic closure in not equals /=
-
-January 28 2004: Version 0.9.7
- - added an option to check for updates
- - starting using symbolic "closure" representation of expensive structures
- (POWersets, ISeq, Seq, ... over some domain)
- - major reworking of the kernel: got rid of special representation for sequences
- (sequences are now represented as functions from integers to a range) + supported
- new symbolic "closure" representation
- - small improvements in interface: self-check only possible before opening a machine,
- analyse invariant will no longer throw error messages if called before machine
- has been initialised.
- - added a few more machines (Laws/....) to check that ProB is functioning properly
-
-January 20 2004: Version 0.9.6
- - improved type inference for CartesianProduct: xx,yy: T1 * T2 => xx:T1 & yy:T2
- - added support for CASE statement
- - fixed problem in SELECT statement (ELSE statement was always possible; now negation
- of all other conditions checked)
-
-January 14 2004: Version 0.9.5
- - added support for parameters which are scalars: parameters which are
- all UPPERCASE are treated as sets, the rest as scalars
- - added support for PrependSequence, AppendSequence, PrefixSequence, SuffixSequence
- - more machines from Steve Schneider's book added
-
-January 13 2004: Version 0.9.4
- - added TotalSurjection and PartialSurjection
- - added "Permutation Sequence": perm
- - added support for closure1 operator [transitive closure]
- (Note: the 'transitive and reflexive closure' operator requires information about
- the types of its argument; ProB does not have this information available and
- the type is not present in the B; more work is needed)
- - added some new machines taken from Steve Schneider's book on B
- (http://www.palgrave.com/science/computing/schneider/).
- These machines are distributed with kind permission by
- Steve Schneider, and have been tested with ProB. In some
- circumstances, minor changes were made to the machines to
- make them more suitable for use with ProB.
-
-December 30 2003: Version 0.9.3
- - added support for sequential composition of statements (;)
- - added support for calling operations (which do not return values)
- - added support for min,max and relational composition (;)
- - added missing enumeration for initialisation of machine
- - got rid of error message when true was evaluated within negation
- - added support for PI (var) . ( | )
- - some support for treating sequences as sets (element of sequence, dom, ran of sequence,
- using sequence as function and applying)
- - fixed bug in strict subset of <<:
- - fixed bug for extension sets: {aa,aa} is now converted into {aa}
- - fixed bug when checking for "not partial function"
- - State pane can now scroll horizontally
-
-December 16: Version 0.9.2
- - more efficient checking for cartesian product: xx : A * B
- - constants are extracted from *both* abstract and concrete constants
- - preferences manager: natural number preferences can be set to 0 & 1
- - internal: additions to prototype Z mode (enumerate sets)
-
-December 11: Version 0.9.1
- - added clearer message about multiple machines not yet being supported
- - fixed a bug concerning "filter failed message" for ForAll & Exists
- - provide better error messages when java ConsoleParser, dot, dotty, PSview do not work
-
-December 9:
- - introduce version numbering for ProB
- - new version: 0.9.0
-
-December 8:
- - improved the preferences management: preferences are now saved; paths to PS & Dot viewers
- can be typed in
- - added support for injective sequences iseq and iseq1 (xx : iseq1(S) or xx /:iseq(R) ...)
- - several improvements to the kernel, all self-checks now pass (but a few still have mutliple
- solutions which is not a problem)
- - find valid initial state now takes constants into account
-
-December 1:
- - added support for SIGMA
- - parameters are supported (handled as SETS)
- - .ref and .imp files can be opened; however ProB does not yet recognise the variables
- coming from the abstract machine (error messages will be printed when loading the machine;
- all unrecognised variables are assumed coming from the abstract machine and the bits of
- the invariant using that are removed.)
- - added a first version of refinement checking (to do a refinement check: 1. load the specification
- machine, 2. explore it, e.g., using temporal model checking and then 3. "Save the state for later
- refinement"; then 4. load the machine you believe to be a refinement; 5. explore the machine as much
- as you can, e.g., using temporal model checking; then 6. do the refinement check and select the
- _refine_spec.P file you generated above in 3.).
- - Note: some self-checks fail on this release; but this should not be a problem and will be fixed
- soon.
-
-November 28:
- - fixed the Cancel button in the Model check dialog
- - added a find non-resetable and find non-deterministic nodes option
-
-November 26:
- - added domain_restriction <| and range_restriction |>
- - type inference now recognises subset <:
- - better error feedback to TclTk GUI
- - outgoing transitions are no longer recomputed when revisiting a state
-
-November 24:
- - various speed improvements (unnecessary backtracking in kernel removed)
- - ProB is now more stringent about typing of set comprehensions, lambda abstractions and
- operations
- - a few bug fixes
- - new preference dialog
- - one can now set an upper bound for max number of initialisations and enablings that are
- computed
- - ProB now detects when part of a parallel assignment within the initialisation
- - an experimental mode has been added where set comprehensions and lambda abstractions are
- not expanded, but compiled into closures (not yet fully functional)
-
-November 17:
- - fixed a bug in how partial functions were enumerated (bug was introduced in last version).
-
-November 11:
- - added first support for CONSTANTS and PROPERTIES section
- - initialisation now shows chosen values in animator
-
-November 10:
- - added support for TotalBijection + NonEmptySubsets POW1
-
-November 10:
- - a single command line argument can now be supplied: ProB will try to open that file
- Improved efficiency of enumeration; operation arguments are now also typed and
- properly enumerated, Warning message printed if an operation argument is not typed;
- the "only label base types" option may thus become superfluous
- - fixed a problem with treating nested functions (e.g., xx :: a -> (b -> c) did not
- work properly before), the problem of multiple versions of the same value should
- also have disappeared
- - note that the jbtools parser (and Atelier B) treats a -> b -> c as (a->b)->c; so you have to use
- brackets if that is not what you wanted (which is likely; but that is the standard
- definition for B)
-
-November 7:
- - added support for generalized union (union), intersection (inter), FinitePowerSet (FIN),
- ForAll statements with multiple variables (!(xx,yy).(...) ) .
- Improved the Temporal model check dialog box.
- Added: "Ignore Types in Invariant" option in the Animate menu.
- Added hashing function to speedup lookup in larger state spaces.
-
-October 29:
- - added a new feature: one can ask ProB to only find one way for enabling
- every operation; also: the "only label base types" option has been turned
- off by default.
-
-October 27:
- - fixed a problem in the code for assignment from a set (xx :: COLOURS or
- yy:: POW(ID) ) which only worked for simple types or sets
-
-October 14:
- - fixed the Windows .exe file to work (hopefully) on more platforms
- replaced the ProWin.zip file
-
-October 10:
- - corrected a bug that prevent the use of the constraint based checker (which
- however still needs some work to be made more robust on larger machines)
-
-October 6:
- - made type extraction from invariant more flexible: previously defined variables are now allowed
- - added support for integer_set assignments: xx::NAT, xx::INT, ...
- - added a preferences manager (but preferences cannot yet be edited)
-
-October 3:
- - added support for division
- - added msvcr70.dll file for Windows distribution
-
-First Release:
-Version 0.7 - Alpha Release
-Released on October 1 2003
-....
diff --git a/src/docs/chapter/user/ZZ_Appendix/10_Bugs.adoc b/src/docs/chapter/user/ZZ_Appendix/10_Bugs.adoc
deleted file mode 100644
index 6b43847803cc794d43fd698f086b742c54841476..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/ZZ_Appendix/10_Bugs.adoc
+++ /dev/null
@@ -1,6 +0,0 @@
-[[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].
-
-We use a free http://www.atlassian.com/software/views/open-source-license-request/[Open Source license] from Atlassian!
diff --git a/src/docs/chapter/user/ZZ_Appendix/11_Troubleshooting.adoc b/src/docs/chapter/user/ZZ_Appendix/11_Troubleshooting.adoc
deleted file mode 100644
index 404fb9b22d0e01e835f185debe39a79f5a1491b8..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/ZZ_Appendix/11_Troubleshooting.adoc
+++ /dev/null
@@ -1,34 +0,0 @@
-[[troubleshooting]]
-= Troubleshooting
-
-* On macOS Catalina the Tcl/Tk menu bar is sometimes not working. Switching to another application and then back to ProB seems to solve the problem.
-
-* Avoid installing ProB in a path with spaces or other special
-characters in them. The same holds for B machines you wish to analyze
-with ProB.
-
-* You need Tcl/Tk (preferably 8.5 or newer) installed on your machine.
-On Linux you will get the error message: ./prob: error while loading
-shared libraries: libtk.so: cannot open shared object file: No such file
-or directory if Tcl/Tk is not proberly installed. You can get Tcl/Tk at
-http://www.tcl.tk/software/tcltk/.
-
-* For the very latest version of ProB (1.2.0 or newer), you need a Java
-1.5 Runtime environment or newer (you will get a message "Could not
-execute parser." with "Error: java.lang.UnsupportedClassVersionError"
-when opening a machine). You can obtain Java at
-http://java.sun.com/j2se/index.jsp[http://java.sun.com/j2se/index.jsp].
-
-* On Mac OS X, if you have trouble opening larger B machines this may be
-due to Mac OS X giving too little memory to ProB. Use 'limit data
-unlimited' (in tcsh) or 'ulimit -d unlimited' (in bash) before launching
-ProB from the command line.
-
-* ProB prior to version 1.3.0 may require more typing information than
-AtelierB, B4Free or the BToolkit. It is usually good style to explicitly
-type all variables and parameters. Hint: avoid using the same variable
-name for different variables (e.g., in two different set
-comprehensions). This way you will know which variable ProB is referring
-to in error messages. As of version 1.3.0, ProB performs full type
-inference and checking, using a unification based algorithm which is
-more powerful than the type inference in the other B tools.
diff --git a/src/docs/chapter/user/ZZ_Appendix/20_ProBLicence.adoc b/src/docs/chapter/user/ZZ_Appendix/20_ProBLicence.adoc
deleted file mode 100644
index 47600d802bc45a84c000c33b09ca85eeb4bdb148..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/ZZ_Appendix/20_ProBLicence.adoc
+++ /dev/null
@@ -1,22 +0,0 @@
-[[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].
-
-\(C) 2000-2018 Michael Leuschel and many others.
-
-ProB comes with ABSOLUTELY NO WARRANTY OF ANY KIND ! This software is
-distributed in the hope that it will be useful but WITHOUT ANY WARRANTY.
-The author(s) do not accept responsibility to anyone for the
-consequences of using it or for whether it serves any particular purpose
-or works at all. No warranty is made about the software or its
-performance.
-
-The ProB binary and source distributions contain the nauty library. You
-cannot use nauty symmetry reduction for applications with nontrivial
-military significance, see http://cs.anu.edu.au/~bdm/nauty/.
-
-For availability of commercial support, please contact
-http://stups.hhu.de/w/Prof._Dr._Michael_Leuschel[Michael Leuschel] or
-http://www.formalmind.com/[Formal Mind].
diff --git a/src/docs/chapter/user/ZZ_Appendix/B_preferences.adoc b/src/docs/chapter/user/ZZ_Appendix/B_preferences.adoc
deleted file mode 100644
index 3a28b02b2eb1779490ea9583f1d21862845246b1..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/ZZ_Appendix/B_preferences.adoc
+++ /dev/null
@@ -1,4 +0,0 @@
-
-= ProB Preferences
-
-A list of the current preferences available in ProB is available <<preferences-for-command-line,here>>.