FAQ
|
Warning This page has not yet been reviewed. Parts of it may no longer be up to date |
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 the page on supporting 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 and 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 reduce the state space, e.g., via Symmetry_Reduction symmetry. Hash symmetry typically works best. Another possibility is Tutorial_Various_Optimizations partial order reduction.
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 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.so /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.