tomgr/libcspm

The library FDR3 uses for parsing, type checking and evaluating machine CSP.

libcspm's Issues

literate CSPm

Any plans to add support for literate CSPm - so we can embed it in LaTeX docs?
Just like Haskell's lhs but using the \begin{code}...\end{code} form, rather than bird-tracks.
For CSP it could be
\begin{cspm}
. . .
\end{cspm}

Segmentation fault?

Whilst doing the assignment I found an issue with the use of the Set function over large sets. I'm running on OSX (Mavericks). Perhaps the Set function isn't intended to be used in this way?

Not sure whether this is down to libcspm or deeper.

Welcome to FDR 3.0.0 (521b22cd118f0a02ade8a95ac96b294148a7c122)
Type :help for help

Set({1..25})
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:
stack overflow

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

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

cspmchecker fails on duplicate assertions

It seems that cspmchecker fails when a CSP file contains a duplicate assert check, even though fdr2 allows this. For instance, the following file:

$ cat checker_test.csp
assert STOP [T= STOP
assert STOP [T= STOP

Produces this output:

$ cspmchecker checker_test.csp
Checking checker_test.csp.....cspmchecker: user error (Pattern match failure in do expression at src/CSPM/TypeChecker/Compressor.hs:29:9-14)

This happens in the released version on Hackage, the WebCSPM app, and in the latest HEAD from github.