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

[pefribeiro]

Hi,

I've been trying to get to the bottom of an issue with a CSPM script for quite some time, where FDR just plainly crashes without providing any output. I then moved onto using cspmprofiler instead, cutting the script into simpler processes in the hope of getting something more amenable to analysis. I eventually got to the point where FDR accepts the script, but curiously cspmprofiler doesn't.

While I am currently not entirely sure of the cause for the crash, it looks like there is something missing in libcspm with regards to the built-in function RUN(). For example, I'm unable to run the assertion assert RUN(Events) :[deterministic] using the cspmprofiler binary included with FDR 4.2.0 (running on MacOS). This assertion runs ok in FDR version 4.2.0, though.

Similar assertions with RUN in some process P give similar results. The following is what I get as output when running through cspmprofiler:

Exploring RUN(Events) :[deterministic]
cspmexplorerprof: panic: the program has detected an inconsistent internal state.
    This means that there is a bug in libcspm, not a bug in your input script.

    Please report this bug using the contact link at https://www.cs.ox.ac.uk/projects/fdr/.
    In particular, please include the input script that caused this error and a brief
    description of how to reproduce the problem. Please also include the following message:

        /private/var/folders/85/ngg2dwf14sx4zbpx13_stt1m0000gn/T/tmp2Wjtow/src/dependencies/libcspm/src/CSPM/Evaluator/DeepSeq.hs:(49,5)-(67,47): Non-exhaustive patterns in function rnf

cspmprofiler: /var/folders/qd/_clksmkd2l32mw8g94d4djjr0000gp/T/cspmprofilerXXXXXXXX42476/cspmexplorerprof.cspm: openFile: does not exist (No such file or directory)

Defining my own RUN(E) as RUNME(E) = [] e : E @ e -> RUNME(E) works with cspmprofiler, though.

I shall be experimenting further with the script till I get a reproducible example in both cspmprofiler and FDR.

Thanks

[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!