forsyde-atom-0.2.2.1: Shallow-embedded DSL for modeling cyber-physical systems

ForSyDe.Atom.MoC.SY

Description

The SY library implements the execution semantics for the atoms operating according to the synchronous model of computation. This module also provides a set of helpers for instantiating the MoC layer patterns described in the ForSyDe.Atom.MoC module as meaningful synchronous process constructors.

For an overview about atoms, layers and patterns, please refer to the ForSyDe.Atom module documentation, and for an overview of the MoC layer entities refer to the MoC layer section.

IMPORTANT!!! see the naming convention rules on how to interpret, use and develop your own constructors.

Synopsis

Synchronous (SY) event

According to [Lee98], "two events are synchronous if they have the same tag, and two signals are synchronous if all events in one signal are synchronous to an event in the second signal and vice-versa. A system is synchronous if every signals in the system is synchronous to all the other signals in the system."

The synchronous (SY) MoC defines no notion of physical time, its tag system suggesting in fact the precedence among events. To further demystify its mechanisms, we can say that:

The SY MoC
is abstracting the execution semantics of a system where computation is assumed to perform instantaneously (with zero delay), at certain synchronization instants, when data is assumed to be available.

Below is a possible behavior in time of the input and the output signals of a SY process, to illustrate these semantics:

Implementing the SY tag system is straightforward if we consider that the synchronous Signal is isomorphic to an infinite list. In this case the tags are implicitly defined by the position of events in a signal: $$t_0$$ would correspond with the event at the head of a signal, $$t_1$$ with the following event, etc... The only explicit parameter passed to a SY event constructor is the value it carries $$\in V$$. As such, we can state the following particularities:

1. tags are implicit from the position in the Stream, thus they are ignored in the type constructor.
2. the type constructor wraps only a value
3. being a timed MoC, the order between events is total [Lee98].
4. from the previous statement we can conclude that there is no need for an execution context and we can ignore the formatting of functions in ForSyDe.Atom.MoC, thus we can safely assume:

newtype SY a Source #

The SY event. It identifies a synchronous signal.

Constructors

 SY Fieldsval :: avalue wrapped by the SY event constructor.
Instances
 Source # Allows for mapping of functions on a SY event. Instance detailsDefined in ForSyDe.Atom.MoC.SY.Core Methodsfmap :: (a -> b) -> SY a -> SY b #(<$) :: a -> SY b -> SY a # Source # Allows for lifting functions on a pair of SY events. Instance detailsDefined in ForSyDe.Atom.MoC.SY.Core Methodspure :: a -> SY a #(<*>) :: SY (a -> b) -> SY a -> SY b #liftA2 :: (a -> b -> c) -> SY a -> SY b -> SY c #(*>) :: SY a -> SY b -> SY b #(<*) :: SY a -> SY b -> SY a # Source # Implenents the execution semantics for the SY MoC atoms. Instance detailsDefined in ForSyDe.Atom.MoC.SY.Core Associated Typestype Fun SY a b :: * Source #type Ret SY b :: * Source # Methods(-.-) :: Fun SY a b -> Stream (SY a) -> Stream (SY b) Source #(-*-) :: Stream (SY (Fun SY a b)) -> Stream (SY a) -> Stream (SY b) Source #(-*) :: Stream (SY (Ret SY b)) -> Stream (SY b) Source #(-<-) :: Stream (SY a) -> Stream (SY a) -> Stream (SY a) Source #(-&-) :: Stream (SY a) -> Stream (SY a) -> Stream (SY a) Source # Read a => Read (SY a) Source # Reads the value wrapped Instance detailsDefined in ForSyDe.Atom.MoC.SY.Core MethodsreadsPrec :: Int -> ReadS (SY a) #readList :: ReadS [SY a] #readPrec :: ReadPrec (SY a) # Show a => Show (SY a) Source # Shows the value wrapped Instance detailsDefined in ForSyDe.Atom.MoC.SY.Core MethodsshowsPrec :: Int -> SY a -> ShowS #show :: SY a -> String #showList :: [SY a] -> ShowS # Plottable a => Plot (Signal a) Source # SY signals. Instance detailsDefined in ForSyDe.Atom.Utility.Plot Methodssample :: Float -> Signal a -> Samples Source #takeUntil :: Float -> Signal a -> Signal a Source # type Ret SY b Source # Instance detailsDefined in ForSyDe.Atom.MoC.SY.Core type Ret SY b = b type Fun SY a b Source # Instance detailsDefined in ForSyDe.Atom.MoC.SY.Core type Fun SY a b = a -> b Aliases & utilities These are type synonyms and utilities provided for user convenience. They mainly concern the construction and usage of signals. type Signal a = Stream (SY a) Source # Type synonym for a SY signal, i.e. "an ordered stream of SY events" unit2 :: (a1, a2) -> (Signal a1, Signal a2) Source # Wraps a (tuple of) value(s) into the equivalent unit signal(s). A unit signal is a signal with one event, i.e. a singleton. Helpers: unit, unit2, unit3, unit4. signal :: [a] -> Signal a Source # Transforms a list of values into a SY signal. readSignal :: Read a => String -> Signal a Source # Reads a signal from a string. Like with the read function from Prelude, you must specify the tipe of the signal. >>> readSignal "{1,2,3,4,5}" :: Signal Int {1,2,3,4,5}  SY process constuctors These SY process constructors are basically specific instantiations of the atom patterns defined in ForSyDe.Atom.MoC. Some are also wrapping functions in an extended behavioural model to describe synchronous processes with predicate behavior. Simple Arguments  :: a initial value -> Signal a input signal -> Signal a output signal The delay process "delays" a signal with one event. Instantiates the delay pattern. >>> let s = signal [1,2,3,4,5] >>> delay 0 s {0,1,2,3,4,5}  Arguments  :: (a1 -> a2 -> (b1, b2)) function on values -> Signal a1 first input signal -> Signal a2 second input signal -> (Signal b1, Signal b2) two output signals comb processes map combinatorial functions on signals and take care of synchronization between input signals. It instantiates the comb pattern (see comb22 defined in ForSyDe.Atom.MoC). Constructors: comb[1-4][1-4]. >>> let s1 = signal [1..] >>> let s2 = signal [1,1,1,1,1] >>> comb11 (+1) s2 {2,2,2,2,2} >>> comb22 (\a b-> (a+b,a-b)) s1 s2 ({2,3,4,5,6},{0,1,2,3,4})  Arguments  :: Signal (a1 -> a2 -> (b1, b2)) signal carrying functions -> Signal a1 first input signal carrying arguments -> Signal a2 second input signal carrying arguments -> (Signal b1, Signal b2) two output signals reconfig creates an synchronous adaptive process where the first signal carries functions and the other carry the arguments. It instantiates the reconfig atom pattern (see reconfig22 defined in ForSyDe.Atom.MoC). Constructors: reconfig[1-4][1-4]. >>> let sf = signal [(+1),(*2),(+1),(*2),(+1),(*2),(+1)] >>> let s1 = signal [1..] >>> reconfig11 sf s1 {2,4,4,8,6,12,8}  Arguments  :: (b1, b2) values to be repeated -> (Signal b1, Signal b2) generated signals A signal generator which keeps a value constant. It is actually an instantiation of the stated0X constructor (check stated22). Constructors: constant[1-4]. >>> let (s1, s2) = constant2 (1,2) >>> takeS 3 s1 {1,1,1} >>> takeS 5 s2 {2,2,2,2,2}  Arguments  :: (b1 -> b2 -> (b1, b2)) function to generate next value -> (b1, b2) kernel values -> (Signal b1, Signal b2) generated signals A signal generator based on a function and a kernel value. It is actually an instantiation of the stated0X constructor (check stated22). Constructors: generate[1-4]. >>> let (s1,s2) = generate2 (\a b -> (a+1,b+2)) (1,2) >>> takeS 5 s1 {1,2,3,4,5} >>> takeS 7 s2 {2,4,6,8,10,12,14}  Arguments  :: (b1 -> b2 -> a1 -> a2 -> (b1, b2)) next state function -> (b1, b2) initial state values -> Signal a1 first input signal -> Signal a2 second input signal -> (Signal b1, Signal b2) output signals stated is a state machine without an output decoder. It is an instantiation of the state MoC constructor (see stated22 defined in ForSyDe.Atom.MoC). Constructors: stated[1-4][1-4]. >>> let s1 = signal [1,2,3,4,5] >>> stated11 (+) 1 s1 {1,2,4,7,11,16}  Arguments  :: (b1 -> b2 -> a1 -> a2 -> (b1, b2)) next state function -> (b1, b2) initial state values -> Signal a1 first input signal -> Signal a2 second input signal -> (Signal b1, Signal b2) output signals state is a state machine without an output decoder. It is an instantiation of the stated MoC constructor (see state22 defined in ForSyDe.Atom.MoC). Constructors: state[1-4][1-4]. >>> let s1 = signal [1,2,3,4,5] >>> state11 (+) 1 s1 {2,4,7,11,16}  Arguments  :: (st -> a1 -> a2 -> st) next state function -> (st -> (b1, b2)) output decoder -> st initial state -> Signal a1 -> Signal a2 -> (Signal b1, Signal b2) moore processes model Moore state machines. It is an instantiation of the moore MoC constructor (see moore22 defined in ForSyDe.Atom.MoC). Constructors: moore[1-4][1-4]. >>> let s1 = signal [1,2,3,4,5] >>> moore11 (+) (+1) 1 s1 {2,3,5,8,12,17}  Arguments  :: (st -> a1 -> a2 -> st) next state function -> (st -> a1 -> a2 -> (b1, b2)) outpt decoder -> st initial state -> Signal a1 -> Signal a2 -> (Signal b1, Signal b2) mealy processes model Mealy state machines. It is an instantiation of the mealy MoC constructor (see mealy22 defined in ForSyDe.Atom.MoC). Constructors: mealy[1-4][1-4]. >>> let s1 = signal [1,2,3,4,5] >>> mealy11 (+) (-) 1 s1 {0,0,1,3,6}  Predicate behavior These processes manipulate the behavior of a signal based on predicates on their status. Arguments  :: Signal (AbstExt Bool) Signal of predicates -> Signal (AbstExt a) Input signal -> Signal (AbstExt a) Output signal This process predicates the existence of values in a signal based on a signal of boolean values (conditions). It is similar to the when construct in the synchronous language Lustre [Halbwachs91], based on which clock calculus can be performed. OBS: this process assumes that all signals carry absent-extended values, which is appropriate in describing multi-clock systems. For a version which inputs signals of non-extended values, check when'. >>> let s1 = (signal . map Prst) [1,2,3,4,5] >>> let pred = (signal . map Prst) [False,False,False,True,True] >>> when pred s1 {⟂,⟂,⟂,4,5}  Arguments  :: Signal Bool Signal of predicates -> Signal a Input signal -> Signal (AbstExt a) Output signal Same as when but inputs signals of non-extended values. >>> let s1 = signal [1,2,3,4,5] >>> let pred = signal [False,False,False,True,True] >>> when' pred s1 {⟂,⟂,⟂,4,5}  is :: Signal (AbstExt a) -> (a -> Bool) -> Signal (AbstExt Bool) Source # Simple wrapper for applying a predicate function on a signal of absent-extended events. >>> let s1 = signal$ map Prst [1,2,3,4,5]
>>> s1 is (>3)
{False,False,False,True,True}


whenPresent :: Signal (AbstExt a1) -> Signal (AbstExt a2) -> Signal (AbstExt a2) Source #

Same as when but triggering the output events merely based on the presence of the first input rather than a predicate function.

>>> let s1   = signal \$ map Prst [1,2,3,4,5]
>>> let sp   = signal [Prst 1, Prst 1, Abst, Prst 1, Abst]
>>> whenPresent sp s1
{1,2,⟂,4,⟂}


Arguments

 :: (a -> Bool) Predicate function -> Signal (AbstExt a) Input signal -> Signal (AbstExt a) Output signal

Filters out values to Abst if they do not fulfill a predicate function.

OBS: this process assumes that all signals carry absent-extended values, which is appropriate in describing multi-clock systems. For a version which inputs signals of non-extended values, check filter'.

>>> let s1   = (signal . map Prst) [1,2,3,4,5]
>>> filter (>3) s1
{⟂,⟂,⟂,4,5}


Arguments

 :: (a -> Bool) Predicate function -> Signal a Input signal -> Signal (AbstExt a) Output signal

Same as filter but inputs signals of non-extended values.

>>> let s1   = signal [1,2,3,4,5]
>>> filter' (>3) s1
{⟂,⟂,⟂,4,5}


Arguments

 :: a Value to fill with -> Signal (AbstExt a) Input -> Signal a Output

Fills absent events with a pre-defined value.

>>> let s1   = signal [Abst, Abst, Prst 1, Prst 2, Abst, Prst 3]
>>> fill 0 s1
{0,0,1,2,0,3}


Arguments

 :: a Value to fill with in case there was no previous value -> Signal (AbstExt a) Input -> Signal a Output

Similar to fill, but holds the last non-absent value if there was one. It implements a state pattern (see state22 defined in ForSyDe.Atom.MoC).

>>> let s1   = signal [Abst, Abst, Prst 1, Prst 2, Abst, Prst 3]
>>> hold 0 s1
{0,0,1,2,2,3}


Arguments

 :: (Signal (AbstExt a1) -> Signal (AbstExt a2) -> Signal b) process which degenerates the absent extension, e.g. holds present values -> Signal (AbstExt a1) -> Signal (AbstExt a2) -> Signal (AbstExt b) absent-extended signal, properly reacting to the inputs

Creates a process wrapper which, from the outside it seems like a combinatorial process which reacts to present events (i.e. simply propagates absent events), but inside it allows, for example, the degeneration of the absent extension in order to describe state processes (e.g. state machines with ignore22 behavior).

Constructors: reactPres[1-4].

>>> let s1 = readSignal "{1,1,1,_,1,_,1}" :: Signal (AbstExt Int)
>>> let proc = stated11 (B.ignore11 (+)) 0
>>> proc s1
{0,1,2,3,3,4,4,5}
>>> reactPres1 proc s1
{0,1,2,⟂,3,⟂,4}


Interfaces

Arguments

 :: Signal TimeStamp SY signal carrying DE timestamps -> Signal a first input SY signal -> Signal b second input SY signal -> (Signal a, Signal b) two output DE signals

Wraps explicit timestamps to a (set of) SY signal(s), rendering the equivalent synchronized DE signal(s).

Constructors: toDE, toDE2, toDE3, toDE4.

>>> let s1 = SY.signal [0,3,4,6,9]
>>> let s2 = SY.signal [1,2,3,4,5]
>>> toDE s1 s2
{1@0s,2@3s,3@4s,4@6s,5@9s}


toSDF2 :: Signal a -> Signal b -> (Signal a, Signal b) Source #

Transforms a (set of) SY signal(s) into the equivalent SDF signal(s). The only change is the event consructor. The total order of SY is interpreted as partial order by the next SDF process downstream.

Constructors: toSDF, toSDF2, toSDF3, toSDF4.

>>> let s = SY.signal [1,2,3,4,5]
>>> toSDF s
{1,2,3,4,5}


zipx :: Vector (Signal a) -> Signal (Vector a) Source #

Synchronizes all the signals contained by a vector and zips them into one signal of vectors. It instantiates the zipx skeleton.

>>> let s1 = SY.signal [1,2,3,4,5]
>>> let s2 = SY.signal [11,12,13,14,15]
>>> let v1 = V.vector [s1,s1,s2,s2]
>>> v1
<{1,2,3,4,5},{1,2,3,4,5},{11,12,13,14,15},{11,12,13,14,15}>
>>> zipx v1
{<1,1,11,11>,<2,2,12,12>,<3,3,13,13>,<4,4,14,14>,<5,5,15,15>}


unzipx :: Integer -> Signal (Vector a) -> Vector (Signal a) Source #

Unzips the vectors carried by a signal into a vector of signals. It instantiates the unzipx skeleton. To avoid infinite recurrence, the user needs to provide the length of the output vector.

>>> let v1 = V.vector [1,2,3,4]
>>> let s1 = SY.signal [v1,v1,v1,v1,v1]
>>> s1
{<1,2,3,4>,<1,2,3,4>,<1,2,3,4>,<1,2,3,4>,<1,2,3,4>}
>>> unzipx 4 s1
<{1,1,1,1,1},{2,2,2,2,2},{3,3,3,3,3},{4,4,4,4,4}>


unzipx' :: Signal (Vector a) -> Vector (Signal a) Source #

Same as unzipx, but "sniffs" the first event to determine the length of the output vector. Has an unsafe behavior!

>>> let v1 = V.vector [1,2,3,4]
>>> let s1 = SY.signal [v1,v1,v1,v1,v1]
>>> s1
{<1,2,3,4>,<1,2,3,4>,<1,2,3,4>,<1,2,3,4>,<1,2,3,4>}
>>> unzipx' s1
<{1,1,1,1,1},{2,2,2,2,2},{3,3,3,3,3},{4,4,4,4,4}>