search

tomgr / libcspm

The library FDR3 uses for parsing, type checking and evaluating machine CSP.
https://www.cs.ox.ac.uk/projects/fdr/
Other
30 stars 6 forks source link

cspmchecker fails on duplicate assertions #1

Closed mcclurmc closed 12 years ago

mcclurmc commented 12 years ago

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.

tomgr commented 12 years ago

This should have been fixed in 47f9f90080f4592da63b817ba458ee69307441c7 (and indeed it works on my own local copy).

It might be worth checking that when building the library using HEAD that you also rebuild the cspmchecker package correctly - sometimes an extra cabal configure in the cspmchecker directory can be required to make it pick up the newer version.

I will release a new version on Hackage and update WebCSPM soon (tomorrow, if I've time!) but there are a number of other changes that I want to merge in first.

Thanks for the report!

mcclurmc commented 12 years ago

Confirmed, fixed for me. Thanks!