FAQ

Revision as of 17:12, 18 January 2010 by Jens Bendisposto (talk | contribs) (Created page with 'Category:User Manual = How do I perform a self-check of ProB? = If you suspect something is wrong with your ProB installation, run the Perform Self Check command in the Debu…')
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)


How do I perform a self-check of ProB?

If you suspect something is wrong with your ProB 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 inital 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 FAQ entry about refinements below).

What about the 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 proably 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 animator seems slow

Be sure you have the "Runtime Type Checking" and "Debugging Info" flags set to off in the Debug menu. The next release of ProB will hopefully make use of the LOGEN partial evaluator to pre-compile B machines; this should make the animator much, much faster.

What do the funny question marks in the Operations Pane mean?

A question mark signifies a pending constraint or co-routine. This should not happen in normal mode of operations, but can be caused if a variable is not given a type (ProB needs the type to enumerate the variable in case it is not bound). Try typechecking your machine (e.g., using B4Free). If there is not type error, please send a bug report.

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 on how it works. It currently 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 sometimes suspended goals are discarded (this only seems to happen in the constraint based checker, not 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 recognised as a type, so 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 visualise the state space

Be sure to set up the viewer preferences and use / (even on Windows !) Be sure to have dot installed + either dotty or a Postscript viewer Also, on Windows, the path to the machine files should not contain spaces. Hence, put your machines for example into 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 an email to myself 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 myself. You can also use the Save State Comand 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 but 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. }}}