libcspm-1.0.0: A library providing a parser, type checker and evaluator for CSPM.

Safe HaskellNone




Provides a set implementation for machine CSP sets. This relies heavily on the type checking and assumes in many places that the sets being operated on are suitable for the opertion in question.

We cannot just use the built in set implementation as FDR assumes in several places that infinite sets are allowed.



data ValueSet Source



Set of all integers


Set of all processes

ExplicitSet (Set Value)

An explicit set of values

IntSetFrom Int

The infinite set of integers starting at lb.

CompositeSet (Seq ValueSet)

A union of several sets.

AllSequences ValueSet

A set containing all sequences over the given set.

CartesianProduct [ValueSet] CartProductType

A cartesian product of several sets.

Powerset ValueSet

The powerset of the given set

AllMaps ValueSet ValueSet

The set of all maps from the given domain to the given image.

emptySet :: ValueSetSource

The empty set

fromList :: [Value] -> ValueSetSource

Converts a list to a set

toList :: ValueSet -> [Value]Source

Converts a set to list.

Basic Functions

compareValueSets :: ValueSet -> ValueSet -> Maybe OrderingSource

Compares two value sets using subseteq (as per the specification).

member :: Value -> ValueSet -> BoolSource

Is the specified value a member of the set.

card :: ValueSet -> IntegerSource

The cardinality of the set. Throws an error if the set is infinite.

empty :: ValueSet -> BoolSource

Is the specified set empty?

union :: ValueSet -> ValueSet -> ValueSetSource

Union two sets throwing an error if it cannot be done in a way that will terminate.

unions :: [ValueSet] -> ValueSetSource

Replicated union.

intersection :: ValueSet -> ValueSet -> ValueSetSource

Intersects two sets throwing an error if it cannot be done in a way that will terminate.

intersections :: [ValueSet] -> ValueSetSource

Replicated intersection.

Derived functions

cartesianProduct :: CartProductType -> [ValueSet] -> ValueSetSource

Produces a ValueSet of the carteisan product of several ValueSets, using vc to convert each sequence of values into a single value.

allSequences :: ValueSet -> ValueSetSource

Returns the set of all sequences over the input set. This is infinite so we use a CompositeSet.

Specialised Functions

singletonValue :: ValueSet -> Maybe ValueSource

Returns the value iff the set contains one item only.

unDotProduct :: ValueSet -> Maybe [ValueSet]Source

Attempts to decompose the set into a cartesian product, returning Nothing if it cannot.