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

Safe Haskell	None

CSPM.Evaluator.ValueSet

Contents

Construction
Basic Functions
Derived functions
Specialised Functions

Description

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.

Synopsis

Construction

data ValueSet Source

Constructors

Integers	Set of all integers
Processes	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.

Instances

Eq ValueSet
Ord ValueSet
NFData ValueSet
Hashable ValueSet
PrettyPrintable ValueSet
MonadicPrettyPrintable Identity ValueSet
MonadicPrettyPrintable EvaluationMonad ValueSet

emptySet :: ValueSet Source

The empty set

fromList :: [Value] -> ValueSet Source

Converts a list to a set

toList :: ValueSet -> [Value]Source

Converts a set to list.

toSeq :: ValueSet -> Seq Value Source

Basic Functions

compareValueSets :: ValueSet -> ValueSet -> Maybe Ordering Source

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

member :: Value -> ValueSet -> Bool Source

Is the specified value a member of the set.

card :: ValueSet -> Integer Source

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

empty :: ValueSet -> Bool Source

Is the specified set empty?

union :: ValueSet -> ValueSet -> ValueSet Source

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

unions :: [ValueSet] -> ValueSet Source

Replicated union.

infiniteUnions :: [ValueSet] -> ValueSet Source

intersection :: ValueSet -> ValueSet -> ValueSet Source

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

intersections :: [ValueSet] -> ValueSet Source

Replicated intersection.

difference :: ValueSet -> ValueSet -> ValueSet Source

Derived functions

data CartProductType Source

Constructors

CartDot
CartTuple

Instances

Eq CartProductType
Ord CartProductType

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

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 Source

allSequences :: ValueSet -> ValueSet Source

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

allMaps :: ValueSet -> ValueSet -> ValueSet Source

fastUnDotCartProduct :: ValueSet -> Maybe [ValueSet]Source

Specialised Functions

singletonValue :: ValueSet -> Maybe Value Source

Returns the value iff the set contains one item only.

valueSetToEventSet :: ValueSet -> EventSet Source

unDotProduct :: ValueSet -> Maybe [ValueSet]Source

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