CSPM.Evaluator.ValueSet

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.

Construction

data ValueSet

Constructors

Integers

Set of all integers

Processes

Set of all processes

IntSetFrom Int

The infinite set of integers starting at lb.

Instances

Eq ValueSet

Ord ValueSet

Show ValueSet

PrettyPrintable ValueSet

emptySet :: ValueSet

The empty set

fromList :: [Value] -> ValueSet

Converts a list to a set

toList :: ValueSet -> [Value]

Converts a set to list.

Basic Functions

compareValueSets :: ValueSet -> ValueSet -> Maybe Ordering

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

member :: Value -> ValueSet -> Bool

Is the specified value a member of the set.

card :: ValueSet -> Integer

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

empty :: ValueSet -> Bool

Is the specified set empty?

union :: ValueSet -> ValueSet -> ValueSet

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

unions :: [ValueSet] -> ValueSet

Replicated union.

intersection :: ValueSet -> ValueSet -> ValueSet

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

intersections :: [ValueSet] -> ValueSet

Replicated intersection.

difference :: ValueSet -> ValueSet -> ValueSet

Derived functions

cartesianProduct :: ([Value] -> Value) -> [ValueSet] -> ValueSet

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

powerset :: ValueSet -> ValueSet

Returns the powerset of a ValueSet. This requires

allSequences :: ValueSet -> ValueSet

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

Specialised Functions

singletonValue :: ValueSet -> Maybe Value

Returns the value iff the set contains one item only.

valueSetToEventSet :: ValueSet -> Set Event