Explicit engine

[iram....@seecs.edu.pk]

Hi,

The system I am building is very huge and has several transition states. When I tried to build the model with MTBDD, Hybrid or Spare engine, it never build and crashes with Java overflow error even using the cuddmaxem and javamaxmen switch up-to 22g and 8g respectively. However when I tried to build the same system without any of the above two switches using explict engine it successfully builds in a split sec. The system after building has states 180955 and transitions are 545692. However I have few questions
 
 1. will it exhaustively check all states when checking properties if explicit engine is used?
 2. what could be the reason of not being able to build the code on other engines?

 3. is explicit engine usually recommended in probabilistic model checking?

Thanks,

Iram

[Joachim Klein]

Hi Iram,

> The system I am building is very huge and has several transition states.
> When I tried to build the model with MTBDD, Hybrid or Spare engine, it
> never build and crashes with Java overflow error even using the
> cuddmaxem and javamaxmen switch up-to 22g and 8g respectively. However
> when I tried to build the same system without any of the above two
> switches using explict engine it successfully builds in a split sec. The
> system after building has states 180955 and transitions are 545692.
> However I have few questions
>
>  1. will it exhaustively check all states when checking properties if
> explicit engine is used?

Yes. Similar to the symbolic engines, it starts with the initial
state(s) and explores all reachable states in the model and then
performs the model checking computations in that model.

>  2. what could be the reason of not being able to build the code on
> other engines?

The model building in the MTBDD, Hybrid and Sparse engines all relies on
the same symbolic building procedure. Here, at first a symbolic MTBDD
representation of the transition matrix (i.e., the effect/probabilities
of the various commands) is built for the whole possible state space
(i.e., all possible combinations of the individual state variable
valuations) and then a reachable state space analysis is performed to
determine which part of the state space is relevant.

Often, the symbolic model building can exploit structure in the model to
arrive at a surprisingly compact representation of the model (even for
huge state spaces). Other times, it does not work so well. For example,
if the reachable state space is relatively small compared to the
potential state space, the symbolic representation of the transition
matrix in the first build step can be huge. My guess would be that this
is the case in your model. If you don't mind, could you paste the
relevant log output when building your model with MTBDD? That might help
in checking that this is indeed the case and that there is not something
stranger going on :)

There are also effects where the order of modules and variables
definitions in the PRISM source file can have a huge effect on the size
of the symbolic representation (as that affects the MTBDD variable
ordering).

>  3. is explicit engine usually recommended in probabilistic model
> checking?

As usual, that depends. The explicit engine tends to work quite well for
models that have a reasonably small reachable state space (up to 1 mio
to 10 mio states, depending on your RAM). As it enumerates all reachable
states individually and has to compute the outgoing transitions, model
building can become slow if you have a huge number of commands in your
model, etc. One always has to experiment a bit which of the engine is
most suitable for a given model instance.


Cheers,
Joachim Klein

[Iram Tariq Bhatti]

Thank you for your detailed reply. Attached is the log file with 22g cudd and 8g java switch used.

[Joachim Klein]

Hi,

> Thank you for your detailed reply. Attached is the log file with 22g
> cudd and 8g java switch used.

Ok, thanks, that looks like a standard uncaught CUDD out-of-memory
situation. From the log it looks like you are using PRISM 4.3.1. In
PRISM 4.4, we improved the out-of-memory handling, so those errors are
detected and reported via an exception instead of completely crashing PRISM.

So, upgrading probably won't allow you to build the model, but the crash
will be softer :)


Cheers,
Joachim Klein