Get deadlock states

[Mirainf]

Hi everybody,

Is there a way, in the ProB Java API,  to get a deadlock state(s) of a given machine and the operation(s) who leads to this state(s)?

thank you in advance

Mira

[Fabian Vu]

Hello Mira,

you can get traces ending in a deadlock state by applying Model Checking or LTL Model Checking.

To apply Model Checking, you can invoke the ConsistencyChecker with ModelCheckingOptions checking for a deadlock:

StateSpace stateSpace = ...; 

ModelCheckingOptions options = new ModelCheckingOptions().checkDeadlocks(true); 

ConsistencyChecker checker = new ConsistencyChecker(stateSpace, options); 

checker.execute();


In order to get another trace leading to a deadlock state, you could invoke:

options.recheckExisting(false);


Currently, LTL Model Checking is always applied from the initial state with rechecking the whole state space.

As result, you will always get the same trace by LTL Model Checking with the same formula.

The supported LTL syntax in ProB is:

• use {...} for B predicates,
• G,F,X,U,W,R,true,false,not,&,or and => are part of the supported LTL syntax,
• use e(op) to check if an operation op is enabled,
• use deadlock to check if a state is deadlocked,
• use deadlock(op1,...,opk) with k>0 to check if all operations in the brackets are disabled,
• use controller(op1,...,opk) with k>0 to check if exactly one of the operations in the brackets is enabled,
• use deterministic(op1,...,opk) with k>0 to check if maximum one of the operations in the brackets is enabled,
• use sink to check if no operation is enabled that leads to another state,
• use brackets to check what is the next operation, e.g. [reset] => X{db={}},
• Past-LTL is supported: Y,H,O,S,T are the duals to X,G,F,U,R.

So, you could write something like "G not(deadlock)". Comparing LTL Model Checking with Model Checking, there are more possibilities to check deadlocks on events (by using the pattern "deadlock(op1,...,opk)")

The corresponding code would look like:

StateSpace stateSpace = ...;

String formula = ...;

LTLChecker checker = new LTLChecker(stateSpace, formula);

IModelCheckingResult res = checker.call();

To calculate deadlock states, it would also be possible to apply symbolic model checking. 

However, it is then not possible to generate a trace containing events leading to the deadlock state.

Best regards, 

Fabian