The CSPM-cspm package
cspm is a small command line tool for analyzing CSPM specifications. It supports several modes of operation. For example as:
'cspm --help' -> print a help message.
'cspm eval 3+4' -> evaluate an expression.
'cspm trace spec.csp' -> interactively trace a process.
'cspm assert spec.csp' -> check the assertions of a specification (only some assertions are supported).
'cspm lts spec.csp --dotOut spec.csp.dot' -> compute the labeled transition system of a process and dump it as dot-file.
'cspm lts spec.csp --fdrOut spec.csp.fdr' -> compute the LTS and dump it a fdr script suitable for refinement checking.
cspm is not a full featured FDR replacement. The main purpose of cspm is to show how the different CSPM-packages work together. LTS computation can demonstrate nice speed-ups on multi-core machines. Try for example 'cspm +RTS -N7 -RTS fdr spec.csp' to use 7 cores.
Properties
| Versions | 0.1.0.0, 0.2.0.0, 0.3.0.0, 0.4.0.0, 0.4.4.0, 0.4.4.1, 0.5.6.0, 0.6.0.4 |
|---|---|
| Dependencies | base (≥4.0 & <5.0), cmdargs (0.9.*), containers (0.4.*), CSPM-CoreLanguage (0.3.*), CSPM-FiringRules (0.4.*), CSPM-Frontend (0.9.*), CSPM-Interpreter (0.6.*), CSPM-ToProlog (0.5.*), hslua (0.3.4), parallel (3.2.*), pretty (1.1.*), prettyclass (1.0.*), syb (0.3.*), transformers (0.3.*), xml (1.3.*) |
| License | BSD3 |
| Author | Marc Fontaine |
| Maintainer | Marc Fontaine <Marc.Fontaine@gmx.de> |
| Stability | experimental |
| Category | Language, Formal Methods, Concurrency |
| Executables | cspm |
| Upload date | Mon Jul 2 14:43:11 UTC 2012 |
| Uploaded by | MarcFontaine |
| Built on | ghc-7.4 |
Modules
Downloads
- CSPM-cspm-0.6.0.4.tar.gz (Cabal source package)
- package description (included in the package)