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
- emptySet :: ValueSet
- fromList :: [Value] -> ValueSet
- toList :: ValueSet -> [Value]
- compareValueSets :: ValueSet -> ValueSet -> Maybe Ordering
- member :: Value -> ValueSet -> Bool
- card :: ValueSet -> Integer
- empty :: ValueSet -> Bool
- union :: ValueSet -> ValueSet -> ValueSet
- unions :: [ValueSet] -> ValueSet
- intersection :: ValueSet -> ValueSet -> ValueSet
- intersections :: [ValueSet] -> ValueSet
- difference :: ValueSet -> ValueSet -> ValueSet
- cartesianProduct :: ([Value] -> Value) -> [ValueSet] -> ValueSet
- powerset :: ValueSet -> ValueSet
- allSequences :: ValueSet -> ValueSet
- singletonValue :: ValueSet -> Maybe Value
- valueSetToEventSet :: ValueSet -> Set Event
Set of all integers
Set of all processes
The infinite set of integers starting at lb.
Compares two value sets using subseteq (as per the specification).
The cardinality of the set. Throws an error if the set is infinite.
Union two sets throwing an error if it cannot be done in a way that will terminate.
Intersects two sets throwing an error if it cannot be done in a way that will terminate.
Produces a ValueSet of the carteisan product of several ValueSets,
vc to convert each sequence of values into a single value.
Returns the set of all sequences over the input set. This is infinite so we use a CompositeSet.
Returns the value iff the set contains one item only.