Safe Haskell	None
Language	Haskell2010

Control.State.Transition.Simple

Description

Simple state transition system over the Identity monad.

Synopsis

applySTSIndifferently :: forall s rtype. (STS s, RuleTypeRep rtype, Identity ~ BaseM s) => RuleContext rtype s -> (State s, [[PredicateFailure s]])
applySTS :: forall s rtype. (STS s, RuleTypeRep rtype, BaseM s ~ Identity) => RuleContext rtype s -> Either [[PredicateFailure s]] (State s)
newtype Threshold a = Threshold a
data ApplySTSOpts = ApplySTSOpts {
- asoAssertions :: AssertionPolicy
- asoValidation :: ValidationPolicy
}
data ValidationPolicy
- = ValidateAll
- | ValidateNone
data AssertionPolicy
- = AssertionsAll
- | AssertionsPre
- | AssertionsPost
- | AssertionsOff
type Rule sts rtype = F (Clause sts rtype)
class (STS sub, BaseM sub ~ BaseM super) => Embed sub super where
- wrapFailed :: PredicateFailure sub -> PredicateFailure super
class (Eq (PredicateFailure a), Show (PredicateFailure a), Monad (BaseM a), Typeable a) => STS a where
- type State a :: Type
- type Signal a :: Type
- type Environment a :: Type
- type BaseM a :: Type -> Type
- type PredicateFailure a = (b :: Type) | b -> a
- initialRules :: [InitialRule a]
- transitionRules :: [TransitionRule a]
- assertions :: [Assertion a]
- renderAssertionViolation :: AssertionViolation a -> String
data AssertionViolation sts = AssertionViolation {
- avSTS :: String
- avMsg :: String
- avCtx :: TRC sts
- avState :: Maybe (State sts)
}
data Assertion sts
- = PreCondition String (TRC sts -> Bool)
- | PostCondition String (TRC sts -> State sts -> Bool)
type TransitionRule sts = Rule sts 'Transition (State sts)
type InitialRule sts = Rule sts 'Initial (State sts)
type family RuleContext (t :: RuleType) = (ctx :: Type -> Type) | ctx -> t where ...
newtype TRC sts = TRC (Environment sts, State sts, Signal sts)
newtype IRC sts = IRC (Environment sts)
class RuleTypeRep t
data RuleType
- = Initial
- | Transition
(?!) :: Bool -> PredicateFailure sts -> Rule sts ctx ()
failBecause :: PredicateFailure sts -> Rule sts ctx ()
(?!:) :: Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
trans :: Embed sub super => RuleContext rtype sub -> Rule super rtype (State sub)
liftSTS :: STS sts => BaseM sts a -> Rule sts ctx a
judgmentContext :: Rule sts rtype (RuleContext rtype sts)
applySTSOpts :: forall s m rtype. (STS s, RuleTypeRep rtype, m ~ BaseM s) => ApplySTSOpts -> RuleContext rtype s -> m (State s, [[PredicateFailure s]])
reapplySTS :: forall s m rtype. (STS s, RuleTypeRep rtype, m ~ BaseM s) => RuleContext rtype s -> m (State s)

Documentation

applySTSIndifferently :: forall s rtype. (STS s, RuleTypeRep rtype, Identity ~ BaseM s) => RuleContext rtype s -> (State s, [[PredicateFailure s]]) Source #

applySTS :: forall s rtype. (STS s, RuleTypeRep rtype, BaseM s ~ Identity) => RuleContext rtype s -> Either [[PredicateFailure s]] (State s) Source #

newtype Threshold a Source #

This can be used to specify predicate failures in STS rules where a value is beyond a certain threshold.

TODO move this somewhere more sensible

Constructors

Threshold a

Instances

Instances details

Eq a => Eq (Threshold a) Source #
Instance details Defined in Control.State.Transition.Extended Methods (==) :: Threshold a -> Threshold a -> Bool # (/=) :: Threshold a -> Threshold a -> Bool #
Data a => Data (Threshold a) Source #
Instance details Defined in Control.State.Transition.Extended Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Threshold a -> c (Threshold a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Threshold a) # toConstr :: Threshold a -> Constr # dataTypeOf :: Threshold a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Threshold a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Threshold a)) # gmapT :: (forall b. Data b => b -> b) -> Threshold a -> Threshold a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Threshold a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Threshold a -> r # gmapQ :: (forall d. Data d => d -> u) -> Threshold a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Threshold a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Threshold a -> m (Threshold a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Threshold a -> m (Threshold a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Threshold a -> m (Threshold a) #
Ord a => Ord (Threshold a) Source #
Instance details Defined in Control.State.Transition.Extended Methods compare :: Threshold a -> Threshold a -> Ordering # (<) :: Threshold a -> Threshold a -> Bool # (<=) :: Threshold a -> Threshold a -> Bool # (>) :: Threshold a -> Threshold a -> Bool # (>=) :: Threshold a -> Threshold a -> Bool # max :: Threshold a -> Threshold a -> Threshold a # min :: Threshold a -> Threshold a -> Threshold a #
Show a => Show (Threshold a) Source #
Instance details Defined in Control.State.Transition.Extended Methods showsPrec :: Int -> Threshold a -> ShowS # show :: Threshold a -> String # showList :: [Threshold a] -> ShowS #
NoThunks a => NoThunks (Threshold a) Source #
Instance details Defined in Control.State.Transition.Extended Methods noThunks :: Context -> Threshold a -> IO (Maybe ThunkInfo) Source # wNoThunks :: Context -> Threshold a -> IO (Maybe ThunkInfo) Source # showTypeOf :: Proxy (Threshold a) -> String Source #

data ApplySTSOpts Source #

Constructors

ApplySTSOpts
Fields asoAssertions :: AssertionPolicy Enable assertions during STS processing. If this option is enabled, STS processing will terminate on violation of an assertion. asoValidation :: ValidationPolicy Validation policy

Instances

Instances details

Eq ApplySTSOpts Source #
Instance details Defined in Control.State.Transition.Extended Methods (==) :: ApplySTSOpts -> ApplySTSOpts -> Bool # (/=) :: ApplySTSOpts -> ApplySTSOpts -> Bool #
Show ApplySTSOpts Source #
Instance details Defined in Control.State.Transition.Extended Methods showsPrec :: Int -> ApplySTSOpts -> ShowS # show :: ApplySTSOpts -> String # showList :: [ApplySTSOpts] -> ShowS #

data ValidationPolicy Source #

Control which predicates are evaluated during rule processing.

Constructors

ValidateAll
ValidateNone

Instances

Instances details

Eq ValidationPolicy Source #
Instance details Defined in Control.State.Transition.Extended Methods (==) :: ValidationPolicy -> ValidationPolicy -> Bool # (/=) :: ValidationPolicy -> ValidationPolicy -> Bool #
Show ValidationPolicy Source #
Instance details Defined in Control.State.Transition.Extended Methods showsPrec :: Int -> ValidationPolicy -> ShowS # show :: ValidationPolicy -> String # showList :: [ValidationPolicy] -> ShowS #

data AssertionPolicy Source #

Control which assertions are enabled.

Constructors

AssertionsAll
AssertionsPre	Only run preconditions
AssertionsPost	Only run postconditions
AssertionsOff

Instances

Instances details

Eq AssertionPolicy Source #
Instance details Defined in Control.State.Transition.Extended Methods (==) :: AssertionPolicy -> AssertionPolicy -> Bool # (/=) :: AssertionPolicy -> AssertionPolicy -> Bool #
Show AssertionPolicy Source #
Instance details Defined in Control.State.Transition.Extended Methods showsPrec :: Int -> AssertionPolicy -> ShowS # show :: AssertionPolicy -> String # showList :: [AssertionPolicy] -> ShowS #

type Rule sts rtype = F (Clause sts rtype) Source #

class (STS sub, BaseM sub ~ BaseM super) => Embed sub super where Source #

Embed one STS within another.

Methods

wrapFailed :: PredicateFailure sub -> PredicateFailure super Source #

Wrap a predicate failure of the subsystem in a failure of the super-system.

Instances

Instances details

STS sts => Embed sts sts Source #
Instance details Defined in Control.State.Transition.Extended Methods wrapFailed :: PredicateFailure sts -> PredicateFailure sts Source #

class (Eq (PredicateFailure a), Show (PredicateFailure a), Monad (BaseM a), Typeable a) => STS a where Source #

State transition system.

Minimal complete definition

initialRules, transitionRules

Associated Types

type State a :: Type Source #

Type of the state which the system transitions between.

type Signal a :: Type Source #

Signal triggering a state change.

type Environment a :: Type Source #

Environment type.

type BaseM a :: Type -> Type Source #

Monad into which to interpret the rules.

type BaseM a = Identity

type PredicateFailure a = (b :: Type) | b -> a Source #

Descriptive type for the possible failures which might cause a transition to fail.

As a convention, PredicateFailures which are "structural" (meaning that they are not "throwable" in practice, and are used to pass control from one transition rule to another) are prefixed with S_.

Structural PredicateFailures represent conditions between rules where the disjunction of all rules' preconditions is equal to True. That is, either one rule will throw a structural PredicateFailure and the other will succeed, or vice-versa.

Methods

initialRules :: [InitialRule a] Source #

Rules governing transition under this system.

transitionRules :: [TransitionRule a] Source #

assertions :: [Assertion a] Source #

Assertions about the transition system.

renderAssertionViolation :: AssertionViolation a -> String Source #

Render an assertion violation.

Defaults to using show, but note that this does not know how to render the context. So for more information you should define your own renderer here.

data AssertionViolation sts Source #

Constructors

AssertionViolation
Fields avSTS :: String avMsg :: String avCtx :: TRC sts avState :: Maybe (State sts)

Instances

Instances details

STS sts => Show (AssertionViolation sts) Source #
Instance details Defined in Control.State.Transition.Extended Methods showsPrec :: Int -> AssertionViolation sts -> ShowS # show :: AssertionViolation sts -> String # showList :: [AssertionViolation sts] -> ShowS #
STS sts => Exception (AssertionViolation sts) Source #
Instance details Defined in Control.State.Transition.Extended Methods toException :: AssertionViolation sts -> SomeException # fromException :: SomeException -> Maybe (AssertionViolation sts) # displayException :: AssertionViolation sts -> String #

data Assertion sts Source #

An assertion is a validation condition for the STS system in question. It should be used to define properties of the system as a whole that cannot be violated under normal circumstances - e.g. a violation implies a failing in the rule logic.

Assertions should not check for conditions that may differ between different rules in a system, since the interpreter may stop the system upon presence of a failed assertion.

Whether assertions are checked is a matter for the STS interpreter.

Constructors

PreCondition String (TRC sts -> Bool)	Pre-condition. Checked before the rule fires.
PostCondition String (TRC sts -> State sts -> Bool)	Post-condition. Checked after the rule fires, and given access to the resultant state as well as the initial context.

type TransitionRule sts = Rule sts 'Transition (State sts) Source #

type InitialRule sts = Rule sts 'Initial (State sts) Source #

type family RuleContext (t :: RuleType) = (ctx :: Type -> Type) | ctx -> t where ... Source #

Equations

RuleContext 'Initial = IRC
RuleContext 'Transition = TRC

newtype TRC sts Source #

Context available to transition rules.

Constructors

TRC (Environment sts, State sts, Signal sts)

Instances

Instances details

(Show (Environment sts), Show (State sts), Show (Signal sts)) => Show (TRC sts) Source #
Instance details Defined in Control.State.Transition.Extended Methods showsPrec :: Int -> TRC sts -> ShowS # show :: TRC sts -> String # showList :: [TRC sts] -> ShowS #

newtype IRC sts Source #

Context available to initial rules.

Constructors

IRC (Environment sts)

class RuleTypeRep t Source #

Minimal complete definition

rTypeRep

Instances

Instances details

RuleTypeRep 'Initial Source #
Instance details Defined in Control.State.Transition.Extended Methods rTypeRep :: SRuleType 'Initial
RuleTypeRep 'Transition Source #
Instance details Defined in Control.State.Transition.Extended Methods rTypeRep :: SRuleType 'Transition

data RuleType Source #

Constructors

Initial
Transition

(?!) :: Bool -> PredicateFailure sts -> Rule sts ctx () infix 1 Source #

Oh noes!

This takes a condition (a boolean expression) and a failure and results in a clause which will throw that failure if the condition fails.

failBecause :: PredicateFailure sts -> Rule sts ctx () Source #

(?!:) :: Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx () Source #

Oh noes with an explanation

We interpret this as "What?" "No!" "Because:"

trans :: Embed sub super => RuleContext rtype sub -> Rule super rtype (State sub) Source #

liftSTS :: STS sts => BaseM sts a -> Rule sts ctx a Source #

judgmentContext :: Rule sts rtype (RuleContext rtype sts) Source #

Get the judgment context

applySTSOpts :: forall s m rtype. (STS s, RuleTypeRep rtype, m ~ BaseM s) => ApplySTSOpts -> RuleContext rtype s -> m (State s, [[PredicateFailure s]]) Source #

Apply an STS with options. Note that this returns both the final state and the list of predicate failures.

reapplySTS :: forall s m rtype. (STS s, RuleTypeRep rtype, m ~ BaseM s) => RuleContext rtype s -> m (State s) Source #

Re-apply an STS.

It is assumed that the caller of this function has previously applied this STS, and can guarantee that it completed successfully. No predicates will be checked when calling this function.