Safe Haskell | None |
---|---|
Language | Haskell2010 |
Control.State.Transition.Extended
Contents
Description
Small step state transition systems.
Synopsis
- data RuleType
- class RuleTypeRep t
- type family RuleContext (t :: RuleType) = (ctx :: Type -> Type) | ctx -> t where ...
- newtype IRC sts = IRC (Environment sts)
- newtype TRC sts = TRC (Environment sts, State sts, Signal sts)
- type Rule sts rtype = F (Clause sts rtype)
- type TransitionRule sts = Rule sts 'Transition (State sts)
- type InitialRule sts = Rule sts 'Initial (State sts)
- data Assertion sts
- = PreCondition String (TRC sts -> Bool)
- | PostCondition String (TRC sts -> State sts -> Bool)
- data AssertionViolation sts = AssertionViolation {}
- 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
- class (STS sub, BaseM sub ~ BaseM super) => Embed sub super where
- wrapFailed :: PredicateFailure sub -> PredicateFailure super
- (?!) :: Bool -> PredicateFailure sts -> Rule sts ctx ()
- (?!:) :: Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
- failBecause :: PredicateFailure sts -> Rule sts ctx ()
- judgmentContext :: Rule sts rtype (RuleContext rtype sts)
- trans :: Embed sub super => RuleContext rtype sub -> Rule super rtype (State sub)
- liftSTS :: STS sts => BaseM sts a -> Rule sts ctx a
- data AssertionPolicy
- data ValidationPolicy
- data ApplySTSOpts = ApplySTSOpts {}
- applySTSOpts :: forall s m rtype. (STS s, RuleTypeRep rtype, m ~ BaseM s) => ApplySTSOpts -> RuleContext rtype s -> m (State s, [[PredicateFailure s]])
- applySTS :: forall s m rtype. (STS s, RuleTypeRep rtype, m ~ BaseM s) => RuleContext rtype s -> m (Either [[PredicateFailure s]] (State s))
- applySTSIndifferently :: forall s m rtype. (STS s, RuleTypeRep rtype, m ~ BaseM s) => 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)
- newtype Threshold a = Threshold a
Documentation
Constructors
Initial | |
Transition |
class RuleTypeRep t Source #
Minimal complete definition
rTypeRep
Instances
RuleTypeRep 'Initial Source # | |
Defined in Control.State.Transition.Extended | |
RuleTypeRep 'Transition Source # | |
Defined in Control.State.Transition.Extended Methods rTypeRep :: SRuleType 'Transition |
type family RuleContext (t :: RuleType) = (ctx :: Type -> Type) | ctx -> t where ... Source #
Equations
RuleContext 'Initial = IRC | |
RuleContext 'Transition = TRC |
Context available to transition rules.
Constructors
TRC (Environment sts, State sts, Signal sts) |
type TransitionRule sts = Rule sts 'Transition (State 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. |
data AssertionViolation sts Source #
Constructors
AssertionViolation | |
Instances
STS sts => Show (AssertionViolation sts) Source # | |
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 # | |
Defined in Control.State.Transition.Extended Methods toException :: AssertionViolation sts -> SomeException # fromException :: SomeException -> Maybe (AssertionViolation sts) # displayException :: AssertionViolation sts -> String # |
class (Eq (PredicateFailure a), Show (PredicateFailure a), Monad (BaseM a), Typeable a) => STS a where Source #
State transition system.
Minimal complete definition
Associated Types
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 PredicateFailure a = (b :: Type) | b -> a Source #
Descriptive type for the possible failures which might cause a transition to fail.
As a convention, PredicateFailure
s 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 PredicateFailure
s 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.
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
STS sts => Embed sts sts Source # | |
Defined in Control.State.Transition.Extended Methods wrapFailed :: PredicateFailure sts -> PredicateFailure sts Source # |
(?!) :: 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.
(?!:) :: Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx () Source #
Oh noes with an explanation
We interpret this as "What?" "No!" "Because:"
failBecause :: PredicateFailure sts -> Rule sts ctx () Source #
judgmentContext :: Rule sts rtype (RuleContext rtype sts) Source #
Get the judgment context
Apply STS
data AssertionPolicy Source #
Control which assertions are enabled.
Constructors
AssertionsAll | |
AssertionsPre | Only run preconditions |
AssertionsPost | Only run postconditions |
AssertionsOff |
Instances
Eq AssertionPolicy Source # | |
Defined in Control.State.Transition.Extended Methods (==) :: AssertionPolicy -> AssertionPolicy -> Bool # (/=) :: AssertionPolicy -> AssertionPolicy -> Bool # | |
Show AssertionPolicy Source # | |
Defined in Control.State.Transition.Extended Methods showsPrec :: Int -> AssertionPolicy -> ShowS # show :: AssertionPolicy -> String # showList :: [AssertionPolicy] -> ShowS # |
data ValidationPolicy Source #
Control which predicates are evaluated during rule processing.
Constructors
ValidateAll | |
ValidateNone |
Instances
Eq ValidationPolicy Source # | |
Defined in Control.State.Transition.Extended Methods (==) :: ValidationPolicy -> ValidationPolicy -> Bool # (/=) :: ValidationPolicy -> ValidationPolicy -> Bool # | |
Show ValidationPolicy Source # | |
Defined in Control.State.Transition.Extended Methods showsPrec :: Int -> ValidationPolicy -> ShowS # show :: ValidationPolicy -> String # showList :: [ValidationPolicy] -> ShowS # |
data ApplySTSOpts Source #
Constructors
ApplySTSOpts | |
Fields
|
Instances
Eq ApplySTSOpts Source # | |
Defined in Control.State.Transition.Extended | |
Show ApplySTSOpts Source # | |
Defined in Control.State.Transition.Extended Methods showsPrec :: Int -> ApplySTSOpts -> ShowS # show :: ApplySTSOpts -> String # showList :: [ApplySTSOpts] -> ShowS # |
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.
applySTS :: forall s m rtype. (STS s, RuleTypeRep rtype, m ~ BaseM s) => RuleContext rtype s -> m (Either [[PredicateFailure s]] (State s)) Source #
applySTSIndifferently :: forall s m rtype. (STS s, RuleTypeRep rtype, m ~ BaseM s) => RuleContext rtype s -> m (State s, [[PredicateFailure s]]) Source #
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.
Random thing
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
Eq a => Eq (Threshold a) Source # | |
Data a => Data (Threshold a) Source # | |
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 # | |
Defined in Control.State.Transition.Extended | |
Show a => Show (Threshold a) Source # | |
NoThunks a => NoThunks (Threshold a) Source # | |