Activity (RSS)

(from [2a3f31e387e7b41c1856ff79a47ad5bfebdea5cc]) CSPM environments

An environment is the symbol table that hold CSPM definitions. They provide a standard mappi...

My initial implementation for CSPM sets used Haskell's “set-like” list functions (nub, union, etc). This works fine for constructing lists that don't contain d...

(from [015d87c470e1e67cba3de830767d2413aa3f78a7]) Cabal build infrastructure

This patch introduces a Cabal package description for the current HST library. Th...

(from [2b108c39f9179982b3d2447a980928aeb81e99d5]) Initial Haskell CSPM implementation

This is an initial patch implementing the CSPM language in Haskell. I've ...

Identifier references in CSPM are staticly scoped. Before implementing let bindings, λ abstractions, and variable references, I'll have to create an implementa...

I need to create a Cabal package for the Haskell CSPM code. It should interface in with the QuickCheck test suite.

I've decided to use Haskell as the implementation language for the CSPM bits of HST. (Thanks to David Faitelson for the idea!) Since it's a lazy functional la...

(from [7c29484dc2c66b9afc90f23782049eacf5e1c6ec]) Adding comments to CSP₀ scripts

This patch adds support for comments in CSP₀ scripts. They use the

same sy...

(from [8317134761619c5c0b768c2c2d0493936913e5db]) Adding failures refinement option to csp0 script

A previous patch added support for failures refinement, but...

(from [d9c7dc294b48e2f3a5009e26a27a96b33f562db8]) Fixed superset proof for integer sets

The is_superset_with_proof method would return incorrect proof in

cer...

The is_superset_with_proof function doesn't always return the correct proof when the superset test fails. For instance,

{2} ?>= {1}

should return 1 as the p...

(from [4754d168e43124cb467c6c82b6333905bd208a7c]) Failures refinement

This patch adds support for checking failures refinement. The Refiner

class checks tha...

(from [fb172a05812c6f2ed5ffa44f088c5ab0f822a41a]) Refactoring refinement code to support multiple semantic models

As another step towards implementing failure...

(from [272fa182e899bc777bf57e13e9c53257c549f608]) Replicated external choice

This patch introduces the “replicated external choice” operator. This

has the s...

CSP_M includes replicated versions of several operators. For instance, instead of

P □ Q □ R □ S

you can do

□ {P,Q,R,S}

It would be nice for CSP₀ to have th...

(from [61b37e197ef47a91949befb3fc773ee79ce9a31d]) CSP₀ can now contain internal underscores

The CSP₀ parser was only accepting underscores in an identifier na...

The CSP₀ parser currently only accepts underscores as the first character of an identifier. The spec says they can appear anywhere.

(from [35472266389a85d5aef424ec8e4b804d7dce659f]) Failures normalization

With this patch, the normalization code now works in the failures

model as well as t...