1 Introduction * Big step = response to external event, consisting of many small steps. * Deconstruction of modeling languages by analysis of the "big step". -> big step = orthongonal aspect #1 + orthogonal aspect #3 + ... * Higher level of abstraction than previous work on "template semantics" ("micro-step <-> macro-step"): to isolate semantic differences between languages more clearly ( * Additional semantic concerns -> external events & variables -> interface events & variables -> combo-step maximality (what is this?)) 2 Normal-Form Syntax and Basic Semantics 2.1 Syntax * Normal form = Composed Hierarchical Transition System (CHTS) syntax: A model consists of: -> a composition tree, nodes = control states -> set of transitions between control states Control state "Named artifact of noteworthy moment in execution of model" -> has type: if leaf node: Basic if hierarchical (has children): Or, And -> state relations: parent, ancestor, child, descendant -> states "overlap" if they are the same or if one is an ancestor of the other -> "least common ancestor" "most leaf state" that is ancestor of both (-> can be And state!) -> Orthogonal states if neither is ancestor of the other and their least common ancestor is an And control state. -> Default control state = child of Or state -> Arena arena of transition is lowest Or state in hierarchy that is ancestor of both src and dst. -> Root of composition hierarchy always Or -> arena of every transition guaranteed to exist Transitions Always has Source and Destination ctrl states Optional parts -> Event trigger -> [Guard condition] -> /Assignments Left-hand side variable Right-hand side expresssion -> ^Generated events Variables & Events Global Model locality by renaming. * Syntax Feature diagram -> Always notion of Transition (to specify behavior) -> All other features optional However, syntax of useful BSMLs support at least events or variables 2.2 Basic semantics * Initially: -> model is in Default control states (of each of the Or states) -> variables have their initial values. * model reacts to "environmental input" via Big Step. Environmental input = set of - Events - Variable assignments received from environment Big Step consists of Small Steps, alternated by Snapshots Small Step = execution of a set of transitions t_i Snapshot = tuple that stores information consists of 1) a Configuration (set of control states) 2) a Variable Evaluation (set of pairs) 3) a Set of Events T_i (1 <= i <= n) are Small Steps of Big Step T ~ T is represented as sp, sp', sp_i (1 <= i < n) Snapshots of T sp: source snapshot of T sp': destination snapshot of T sp_i: intermediary? "Combo Step" intermediate grouping of sequence of small steps -> to hide some effects Enabled transitions In each Small Step, a set of Enabled Transitions is chosen to be executed. A transition is enabled if -> Event trigger is satisfied -> Guard condition is satisfied -> Src Control State is in the Src Configuration of the small step. Execution Execution of transitions of a small step leads to Destination Snapshot. When entering (exiting) Or state: its Default is entered (exited) And state: all its children are entered (exited) Execution of small step is Atomic <=> None of the variable assignments and events generated by one transition can be seen by another. Types of "ability to response to (sequences of) environmental input" - Fast Computation system never misses input (but no buffering) - Helpful Environment system lets environment (e.g. a human being) wait until it can process input - Asynchronous Communication system buffers input, never misses NOT DISCUSSED IN PAPER 2.3 Representing BSMLs in Normal-Form Syntax * Control States No control states necessary if model's reaction to input does not depend on past behavior. can be modeled in Normal Form Syntax as a single state being the src and dst of all transitions. * Transitions No event triggers with disjunctions can be split into multiple transitions Multiple-Src - Multiple-Dst transitions (e.g. Petri nets) can be split into multiple single-src, single-dst transitions -> need to extend for concurrency and consistency -> future work 3 Semantic Aspects Semantic Aspects * Big-Step Maximality specifies when a big step ends Options: -> Syntactic: define stable state as "end point" of arena of transition that brought us to "stable" -> Take One: 1 transition per non-overlapping arena -> Take Many: sequence of small steps continues until no more enabled transitions Characteristics: Scope: Take One, Take Many: Not obvious what Dst Snapshot will be <-> Syntactic Sequential transitions (but also non-termination of big step): Syntactic, Take Many <-> Take One Some BSMLs require "else" transitions such that a stable state is always reached. * Combo-Step Maximality specifies when a combo step ends * Event Lifeline specifies how far within big step event can be sensed Options: -> Present in Whole: Event is present throughout big step. -> Present in Remainder: Event is present in snapshot after which is is generated and remains present until end of big step. -> Present in Next Combo Step: Event only present during next Combo Step. -> Persent in Next Small Step: Event only present in next snapshot. -> Present in Same: Event only present in small step during which it was generated. ==> Small steps are independent! Characteristics: Synchrony (Big Step == "Hardware tick" ~ Causal Block Diagrams): Present in Whole Causality (Big Step is causal if any event that triggers transition in small step was generated in earlier small step): Remainder, Next (...) Step <-> Present in Whole, Present in Same (non-causal) (Causality can still be enforced in "Present in Whole" BSMLs by e.g. compiler) Orderedness: Present in Next Small Step <-> Present in Remainder (no rigorous causal ordering) Modularity: Present in Whole (generated events same visibility as environmental events) <-> other Multiple-instance events (multiple instances of same event (generated by different small steps) existing in same big step): Present in Next (...) Step, Present in Same <-> other Global Inconsistency (big step is globally inconsistent if it contains a transition that generates an event and contains another transition that triggers by the absense of that event): Present in Remainder (although max. 1 instance of each event, event can be sensed as present and absent in same big step) <-> other Sub-aspects: * Internal Events environment cannot see these * External Events for communication with environment Options to distinguish external events from internal events: -> Syntactic Input Events: Environmental input is syntactically distinguished. -> Received Events as Environmental: Events received at beginning of big step are environmental. -> Hybrid Input Events: Event received at beginning of big step are environmental only if it is not generated by any transitions in the model. + must also specify Lifeline * Interface Events inter-component communication Options: -> Strong Synchronous Event: Interface event sensed as present throughout big step in which it was generated (~ Present in Whole) -> Weak Synchronous Event: Interface event is present in big step, but not until it is generated. (~ Present in Remainder) -> Asynchronous Event: Interface event is present in next big step. * Enabledness Memory Protocol specifies values read to determine enabledness of guard conditions of transitions Options: -> GC Big Step: Read values are determined at beginning of big step. -> GC Small Step: Read values are determined at beginning of small step. -> GC Combo Step: Read values are determined at beginning of combo step. Characteristics: Modularity ("does new component behave like environment?"): GC Big Step (just like environmental events, variable values only "change" at beginning of big step) <-> GC Small Step, GC Combo Step (variable values "change" during big step) Non-interference (early assignment does not affect later read): GC Big Step <-> sequentiality in small steps: GC Small Step. GC Combo Step: Non-interference only within combo step. Variable operators: to obtain different value than protocol specifies. -> pre: big-step source snapshot, Total -> cur: small-step source snapshot, Total -> new: small-step source snapshot, Not Total -> new_small: small-step destination snapshot, Total * External Variables If a BSML distinguishes external from internal variables, this usually happens semantically. Memory control only applies to internal variables. * Interface Variables requirement: each variable can be written by only one component and read by multiple components. Options (just like with Interface Events): -> GC Strong Synchronous Variable: write to interface is read by GC right from beginning of big step -> GC Weak Synchronous Variable: variable doesn't contain "new value" until it is written to. -> GC Asynchronous Variable: Effects of a "write" become visible in next big step. Characteristics: Blocking read: GC Strong Synch (enforces "dataflow order", "blocking component", deadlock) <-> communication delay: GC Asynchronous (never blocks) Modularity with respect to interface variables: GC Strong Synch, GC Asynchronous (values same througout big step) <-> GC Weak Synchronous Variable (values may change in big step) * Order of Small Steps specifies options for order of transitions in big step Options: -> None: Small step is non-deterministically picked. -> Explicit Ordering: Order is syntactically determined. -> Dataflow: Transitions that write to a variable are executed before transitions that read from a variable. Danger: Cycles! * Concurrency and Consistency specifies set of potential Small Steps (from set of enabled transitions): 1) "can multiple transitions be taken in 1 small step?" 2) ^ if so: "what consistency criteria must be taken?" Options: -> Simple: 1 transition per 1 small step -> Many: all enabled transitions that can be taken together are in 1 small step Characteristics: Undeterminism: Simple <-> Race conditions: Many: If more than 1 transition assigns values to a variable. Sub-aspects: * (Many:) Small Step Consistency specifies how non-preempting transitions should happen Options: -> Src/Dst Orthogonal: transitions whose Srcs and Dsts are pairwise orthogonal are taken in 1 small step -> Arena Orthogonal: transitions with non-overlapping arenas are taken in 1 small step (~ "Take One" in "Big Step Max.") * (Many:) Preemption specifies how a pair of transitions should happen if one is an interrupt of the other. t is interrupt of t' if -> t.Src and t'.Src are orthogonal and either: -> t'.Dst is orthogonal with t.Src, and t.Dst is not orthogonal with t.Src or t'.Src -> t.Dst is not orthogonal with t.Src or t'.Src and t'.Dst is not orthogonal with t.Src or t'.Src but t.Dst is descendant of t'.Dst Options: -> Non-Preemptive: t and t' allowed to be executed in same Small Step. effect of executing {t,t'} includes variable assignments + event generations but destination configuration of small step is as if only t has been executed. "respects last wishes" of children of interrupted state. -> Preemptive: t and t' not allowed to be executed in same Small Step. * Priority specifies small step from set of potential small steps Options (can be combined): -> Hierarchical: -> basis: Src/Dst/Arena -> scheme: Parent/Child -> Explicit: Priority is syntactically determined. -> Negation of Triggers: t1 + not t2.enabled > t2 Characteristics: Exhaustiveness: Explicit, Negation of Triggers <-> Simplicity: Hierarchical * Assignment Memory Protocol specifies the values read from variables in RHS expressions assigned to variables. Options: -> RHS Big Step: See Enabledness Memory Protocol -> RHS Small Step: See Enabledness Memory Protocol -> RHS Combo Step: See Enabledness Memory Protocol Sub-aspects: * Internal Variables (environment cannot see these) * Interface Variables (communication between differnt components of model) Options: -> RHS Strong Synchronous Variable: See GC Synchronous Variable -> RHS Weak Synchronous Variable: See GC Weak Synchronous Variable -> RHS Asynchronous Variable: See GC Asynchronous Variable Dependencies between Features