CSPM-cspm: cspm command line tool for analyzing CSPM specifications.

[ bsd3, concurrency, formal-methods, language, library, program ] [ Propose Tags ]

cspm is a small command line tool for analyzing CSPM specifications. It supports serveral 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.

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 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, 0.7.0.0, 0.8.0.0, 0.8.1.0
Dependencies base (>=4.0 && <5.0), cmdargs (>=0.7 && <0.8), containers (>=0.4 && <0.5), CSPM-CoreLanguage (>=0.3 && <0.4), CSPM-FiringRules (>=0.4 && <0.5), CSPM-Frontend (>=0.7 && <0.8), CSPM-Interpreter (>=0.5 && <0.6), CSPM-ToProlog (>=0.4 && <0.5), hslua (==0.3.3), parallel (>=3.1 && <3.2), pretty (>=1.0 && <1.1), syb (>=0.3 && <0.4), transformers (>=0.2 && <0.3), xml (>=1.3 && <1.4) [details]
License BSD-3-Clause
Author Marc Fontaine
Maintainer Marc Fontaine <fontaine@cs.uni-duesseldorf.de>
Category Language, Formal Methods, Concurrency
Uploaded by MarcFontaine at 2011-06-24T12:05:51Z
Distributions
Reverse Dependencies 1 direct, 0 indirect [details]
Executables cspm
Downloads 10858 total (30 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs uploaded by user
Build status unknown [no reports yet]