CSP#

CSP# is the input language of PAT, the Process Analysis Toolkit from NUS: Hoare's CSP with shared variables, channels, and C#-style program blocks attached to events. This is not the model checker. It is a runtime verifier: it takes one trace and decides whether the model can produce it, by running the language's operational semantics forwards along the trace.

Because CSP# is nondeterministic (internal choice, hidden events, interleaving), the checker follows every state the model could be in at once, the way you would simulate an NFA. A trace is accepted if that set never empties. Only the states the trace reaches are ever explored, so this stays cheap on models whose full state space would not be.

The parser follows the grammar in the PAT 3.5 manual and the semantics follow its firing rules, including the parts that are easy to get wrong: data operations never synchronise, alphabets are computed once when a parallel composition is first reached, [] is resolved by any event while [*] needs a visible one, and atomic takes priority. Not covered: #import of C# libraries, user-defined types, and unbounded replication.