Streams, States, and Services

[stefjoosten]

Intro

What does the specification of a distributed information system look like? Besides being specified in Ampersand?

For distributed systems, we'll have to discuss streams of messages (see also issue #1164).

Assumptions, desires, requirements

1. A system is represented as a graph with services as nodes and streams as edges.
2. A stream has a type. I want A static type system on streams.
3. A session can launch temporary infrastructure, which is the case in this example. For that, we need to specify the temporary infrastructure between SESSION and ENDSESSION.
4. A service "sits on" a data space, which we will call the context of that service.
5. We need a structured type for messages for the purpose of static type checking. I have called it MsgType, but I have not designed it yet.
6. I want events that are triggered by widgets to be incorporated, so we can avoid the cumbersome button code that we see for example in RAP.

Example (for discussion)

I have made an example of a system for telephone calls on a mobile app to a specific customer service call center that must track caller locations. It allows the caller to chat with the operator in case the caller and the operator speak different languages. Translation is done by calling an online translate service. The specification has to define all components that constitute the system, and yet be simple. Here is a proposal:

ORCHESTRATION Telephony
STREAM Calls OF Call
PURPOSE CONCEPT Call
{+ This is a call that is made by the app on a mobile device. +}
STREAM Files OF File
PURPOSE CONCEPT File
{+ We want to allow users to upload files to the operator. +}
STREAM Notifications OF Notification
PURPOSE CONCEPT Notification
{+ We want the system or the operator to push notifications to the mobile device. +}
STREAM Speech OF BIT
PURPOSE CONCEPT BIT
{+ We want to do voice-over-IP, for which we need a bitstream +}

-- The following specifies how the services are interconnected.
SERVICE App PRODUCES Calls
SERVICE CallCenter CONSUMES Calls, Speech PRODUCES Notifications, Speech
SERVICE APIgateway CONSUMES AppCalls
SERVICE AppBackend CONSUMES AppCalls PRODUCES AppSessions

   ORCHESTRATION “Call”
   STREAM Locations OF Location
   REPRESENT Character TYPE UTF8
   STREAM Chat OF Character
   STREAM Translations OF Phrase
   ROLE Caller PRODUCES Chat, Files CONSUMES Chat
   ROLE Operator PRODUCES Chat CONSUMES Chat, Files, Locations
   SERVICE App PRODUCES Locations, Speech, Files, Chat
   SERVICE ChatService CONSUMES Chat, Translations PRODUCES Chat, Translations
   SERVICE ChatClient CONSUMES Chat, Speech PRODUCES Chat
   SERVICE TranslateService PRODUCES Translations CONSUMES Translations
   SERVICE Geo CONSUMES Locations
   ENDORCHESTRATION

ENDORCHESTRATION

Proposal

So let me do a proposal in the form of an Ampersand specification, in a spirit similar to issue #1164. The following code has been type checked by Ampersand.

CONTEXT "Messaging"

RELATION originatesFrom[Conjunct*Rule] [TOT] -- This rule is copied from FormalAmpersand

-- The following stuff is not (yet) in FormalAmpersand
RELATION context[Session*DataSpace] [UNI,TOT]
RELATION context[Service*DataSpace] [UNI,TOT]
RELATION context[SatComputation*DataSpace] [UNI,TOT]
RELATION context[Action*DataSpace] [UNI,TOT]
RELATION compatible[DataSpace*MsgType]
RELATION inst[Message*MsgType] [UNI,TOT]
RELATION produced[Service*Message] [INJ,SUR]
RELATION produces[Service*Stream]
RELATION consumed[Service*Message]
RELATION consumes[Service*Stream]
RELATION log[Event*Stream] [UNI]
MEANING "Every event that occurs is logged on one specific stream."
RELATION on[Interface*Service] [UNI,TOT]
RELATION type[Widget*EventType] [UNI,TOT]
RELATION type[Stream*MsgType] [UNI,TOT]
RELATION in[Widget*Interface] [UNI,TOT]
RELATION reaction[EventType*CodeFragment] [UNI,TOT]
RELATION reaction[Rule*CodeFragment] [UNI,TOT]
RELATION exec[Action*CodeFragment] [UNI,TOT]
RELATION trig[Event*Conjunct]
RELATION trig[Violation*Action] [UNI]
RELATION conjunct[SatComputation*Conjunct] [UNI]
RELATION compBy[Violation*SatComputation] [UNI,TOT]
RELATION occured[Event*Session] [UNI,TOT]

CLASSIFY Message ISA Event
PATTERN "Stream Type System"
    PURPOSE RULE "Type checking of produced streams"
    {+ We want statically typed streams. So, every stream has a type. The type checker must check for compatibility and generate appropriate error messages upon failure.
    +}
    RULE "Type checking of produced streams" :
         context~;produces;type |- compatible
    MEANING "The type of every stream must be compatible with the context of a service that produces it."
    RULE "Type checking of consumed streams" :
         context~;consumes;type |- compatible
    MEANING "The type of every stream must be compatible with the context of a service that consumes it."

    PURPOSE RULE "Type checking of consumed messages"
    {+ This relation allows the type checker to determine that there is precisely one match for every frame.
    If not, the compiler must signal a mistake and refrain from generating code.
    +}
    RULE "Type checking of produced messages" :
         produced;log |- produces
    MEANING "A message can be produced only by a service that produces the MsgType of that message."
    RULE "Type checking of consumed messages" :
         consumed;log |- consumes
    MEANING "A message can be consumed only by a service that consumes the MsgType of that message."
ENDPATTERN

PATTERN "Evaluation of actions"
    PURPOSE RULE "Evaluate whether a conjunct is satisfied"
    {+ This rule tells when the exec-engine must kick in. +}
    RULE "Evaluate whether a conjunct is satisfied" :
         trig~;occured;context |- conjunct~;context
    MEANING "A sat-computation is required if an event occurs that triggers (i.e. may violate) a conjunct."

    PURPOSE RULE "Evaluate which actions to take"
    {+ This rule specifies which actions are triggered. +}
    RULE "Evaluate which actions to take" :
         compBy;conjunct |- trig;exec;reaction~;originatesFrom~
    MEANING "Every violation triggers the action specified by the rules in which the conjunct occurs."

    PURPOSE RULE "Take action on a widget event"
    {+ This rule specifies which actions are triggered. +}
    RULE "Take action on a widget event" :
         reaction;exec~;context |- type~;in;on;I[Service];context
    MEANING "An event that has the type of a widget causes an action in that context."
ENDPATTERN


ENDCONTEXT

Here is the data model: