Unable to run assertions on processes using built-in function RUN about libcspm

[tomgr]

Thanks for the report. I can see what the problem is with cspmprofiler and this is easy to fix. I will push a fix for this shortly.

I'm more concerned about the bug you're seeing with FDR4. What happens when you run card(Events)? If this also hangs, then this means you have an infinite number of events, which would explain why FDR is hanging!

[pefribeiro]

Thanks for the prompt reply!

I have narrowed down the problem with FDR4 to there being many machines being built when checking assertions. For example, I'm checking for determinism on a rather complex process P, and whenever I see on the FDR UI that more than roughly 170 machines have been created, eventually it just crashes. If I make my process slightly less complex, then not so many machines are built and the assertion passes nicely. (I would like to probe this further with cspmprofiler once the fix is available, though.)

I have tried using compression functions like sbisim(diamond(P)) and the problem with FDR4 goes away, as less machines are built when checking the original assertion. Is there some sort of resource ceiling being hit somewhere? Should I be tweaking something else, other than just compressing as much as possible?

Edit: Apologies, I forgot to answer your question. Yes Events is finite and so card(Events) terminates.

[tomgr]

So there should not be a problem with that many machines, in general. Presumably FDR is running out of memory? What does the status window say just before it crashes?

Compression is a useful tool, but it does explicitly construct the automata. If the compressed machine is very large, perhaps because of a large alphabet, this can make compression infeasible.

Determinism checking is one of the most expensive checks you can do. Are you doing this in the failures or the failures divergences model? You could try, as an experiment, running this in the failures model instead as FDR uses a different algorithm that runs faster.

In general: compressing is gopd, but don't compress things that are too big; keep the alphabets as small as possible; only use the stronger denotational models when you need them.

I might be able to give some more specific advice if I can see the script. Feel free to email me about this.

I'll close this issue as I don't think there is a bug in FDR as such, more of a performance issue which is, regrettably, something one can not always avoid!