Skip to content
Snippets Groups Projects
Commit 915e98c8 authored by dgelessus's avatar dgelessus
Browse files

Remove appendix pages that can also be found on wiki

parent 8848c592
Branches
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
Showing
with 0 additions and 1377 deletions
src/docs/chapter/user/ZZ_Appendix/01_Team.adoc deleted 100644 → 0
+ 0
− 44
View file @ 8848c592
[[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].
src/docs/chapter/user/ZZ_Appendix/02_FAQ.adoc deleted 100644 → 0
+ 0
− 197
View file @ 8848c592
[[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.
src/docs/chapter/user/ZZ_Appendix/03_Download.adoc deleted 100644 → 0
+ 0
− 4
View file @ 8848c592
[[downloads]]
= Download
If you click https://www3.hhu.de/stups/prob/index.php/Download[here] you will be redirected to our online Download page.
src/docs/chapter/user/ZZ_Appendix/04_DownloadPriorVersions.adoc deleted 100644 → 0
+ 0
− 4
View file @ 8848c592
[[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.
src/docs/chapter/user/ZZ_Appendix/05_Links.adoc deleted 100644 → 0
+ 0
− 207
View file @ 8848c592
[[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]
src/docs/chapter/user/ZZ_Appendix/06_ProB_Release_History.adoc deleted 100644 → 0
+ 0
− 855
View file @ 8848c592
[[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
....
src/docs/chapter/user/ZZ_Appendix/10_Bugs.adoc deleted 100644 → 0
+ 0
− 6
View file @ 8848c592
[[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!
src/docs/chapter/user/ZZ_Appendix/11_Troubleshooting.adoc deleted 100644 → 0
+ 0
− 34
View file @ 8848c592
[[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.
src/docs/chapter/user/ZZ_Appendix/20_ProBLicence.adoc deleted 100644 → 0
+ 0
− 22
View file @ 8848c592
[[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].
src/docs/chapter/user/ZZ_Appendix/B_preferences.adoc deleted 100644 → 0
+ 0
− 4
View file @ 8848c592
= ProB Preferences
A list of the current preferences available in ProB is available <<preferences-for-command-line,here>>.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment