-
Notifications
You must be signed in to change notification settings - Fork 28
Pseudocode for SCION step algorithm
This document describes a canonical step algorithm which implements SCION's semantics. This is meant to provide a similar role to the "Algorithm for SCXML Interpretation" presented in the SCXML specification.
SCION semantics are defined as a configuration of the possible semantic options of big-step languages presented in "Big-Step Semantics", by Shahram Esmaeilsabzali, Nancy A. Day, Joanne M. Atlee, and Jianwei Niu.
This document is not meant to stand on its own. In particular, at least Section 2 of "Big-Step Semantics" should be read first for definitions of the terminology that will be used in this paper.
SCION implements the following semantic options from the semantic aspects described in "Big-Step Semantics":
- Concurrency:
- Number of transitions: Multiple
- Order of transitions: Explicitly defined, based on document order (which defines a total order).
- Transition Consistency:
- Small-step consistency: Arena Orthogonal
- Interrupt Transitions and Preemption: Non-preemptive
- Maximality: Take-Many
- Memory Protocols: Small-step
- Event Lifelines: Next small-step
- External Event Communication: Asynchronous
- Priority: Source-Child. If that is ambiguous, then document order is used.
Where possible, in the pseudocode algorithm, if a particular semantic option has influenced the pseudocode implementation, it is noted in the function description and the code.
The pseudocode is written using a python-inspired syntax. Indentation is used to delimit block scope. Tuples are often returned from functions, and simple destructuring assignments are used to initialize variables from the returned results. List data structures are initialized using the "[]" syntax.
- Set: An unordered set of objects. In particular, note that union and difference methods mutate the set, such that it is updated in-place.
- List: An ordered list of objects.
- Map: A map of string keys to object values.
- Queue: A First-in-First-Out (FIFO), ordered data structure.
- Event: A structure with the following properties:
- name : String
- data : Object
The following state types are considered enumerated constants:
- PARALLEL
- COMPOSITE
- HISTORY
- BASIC
- FINAL
- INITIAL
- configuration: Set containing only basic, final, or initial states.
- historyValue: Map from a history state id string to a basic configuration.
- innerEventQueue: Queue containing Sets of Events.
- isInFinalState: Boolean, is set to true when all states in the configuration are final states.
- datamodel: String-to-Object Map.
The following utility functions are used in the step algorithm. The implementation of these depends on the underlying representation of the Statecharts object model.
- getAncestors
- getDepth
- getLCA
- isOrthogonalTo
- evaluateAction
procedure init initializes the global data structures.
procedure init():
configuration = new Set()
historyValue = new Map()
innerEventQueue = []
isInFinalState = false
procedure start begins execution of the Statecharts model. This sets the initial configuration, executes top-level scripts, initializes the datamodel, and performs the initial big-step.
procedure start(model)
configuration.add(model.root.initial)
#initialize top-level datamodel expressions. simple eval
for script in model.scripts
evaluateScript(script)
for item in model.datamodel
if item.expr then datamodel[item.location] = eval(item.expr)
performBigStep()
procedure performBigStep accepts an event as input. It will loop, selecting transitions and performing small-steps, until no transitions are selected, at which point the big-step is complete.
procedure performBigStep(e)
if e then innerEventQueue.push(new Set([e]))
keepGoing = true
while keepGoing
if innerEventQueue.isEmpty()
eventSet = innerEventQueue.shift()
else
eventSet = new Set()
#create new datamodel cache for the next small step
datamodelForNextStep = new Map()
selectedTransitions = performSmallStep(eventSet,datamodelForNextStep)
keepGoing = not selectedTransitions.isEmpty()
if for every state in states, state.kind is FINAL
isInFinalState = true
procedure performSmallStep performs a single small step. First, it selects an active transitions, given the datamodel and active events for the current small-step. Next, it computes states that are exited and states that are entered. Then it will process states that are exited, in order of depth, which includes updating any history states of the states exited, and performs exit actions. Next, transition actions are executed in document order. Then, enter actions are executed in reverse depth order for the states entered. Next, the configuration is updated, such that basic states which are exited are removed from the configuration, and basic states that are entered are added to the configuration. Next, the set of internal events that have been sent by a <send>
are added to the innerEventQueue, so that they will be active in the next small-step. Finally, the datamodel is updated with the values that have been set in the current small-step.
procedure performSmallStep implements the following semantic options:
- Concurrency - Number of transitions: Multiple
- Concurrency - Order of transitions: Explicitly defined
- Event Lifelines: Next small-step
- Maximality: Take-Many
procedure performSmallStep(eventSet,datamodelForNextStep)
selectedTransitions = selectTransitions(eventSet,datamodelForNextStep)
if not selectedTransitions.isEmpty()
[basicStatesExited,statesExited] = getStatesExited(selectedTransitions)
[basicStatesEntered,statesEntered] = getStatesEntered(selectedTransitions)
eventsToAddToInnerQueue = new Set()
#update history states
for state in statesExited
#peform exit actions
for action in state.onexit
evaluateAction(action,eventSet,datamodelForNextStep,eventsToAddToInnerQueue)
#update history
if state.history
if state.history.isDeep
f = lambda s0 : s0.kind is BASIC and s0 in getDescendants(state)
else
f = lambda s0 : s0.parent is state
historyValue[state.history.id] = statesExited.filter(f)
# Semantic Choice : Concurrency: Number of transitions: Multiple
# Semantic Choice : Concurrency: Order of transitions: Explicitly defined
sortedTransitions = selectedTransitions.sort( lambda (t1,t2) : t1.documentOrder - t2.documentOrder)
for transition in sortedTransitions
for action in transition.actions
evaluateAction(action,eventSet,datamodelForNextStep,eventsToAddToInnerQueue)
for state in statesEntered
for action in state.onentry
evaluateAction(action,eventSet,datamodelForNextStep,eventsToAddToInnerQueue)
#update configuration by removing basic states exited, and adding basic states entered
configuration.difference(basicStatesExited)
configuration.union(basicStatesEntered)
#add set of generated events to the innerEventQueue
# Semantic Choice : Event Lifelines: Next small-step
if not eventsToAddToInnerQueue.isEmpty()
innerEventQueue.push(eventsToAddToInnerQueue)
#update the datamodel
for key in datamodelForNextStep.keys
datamodel[key] = datamodelForNextStep[key]
#if selectedTransitions is empty, we have reached a stable state, and the big-step will stop, otherwise will continue
# Semantic Choice : Maximality: Take-Many
return selectedTransitions
function getStatesExited computes the states that have been exited, given a set of transitions. This function loops through the given set of transitions, computes the Least Common Ancestor (LCA) of the transition's source and destination states, computes the descendants of the LCA, and adds to basicStatesExited states that are both in the current configuration and descendants of the LCA. Because the configuration contains only basic states, the states added to basicStatesExited will be basic states. To compute composite and parallel states exited, the ancestors of the basic states exited, up to, but not including the LCA, are added to statesExited, which contains both basic and non-basic states. The statesExited set is then sorted by depth and returned.
function getStatesExited(transitions)
statesExited = new Set()
basicStatesExited = new Set()
for transition in transitions
lca = getLCA(transition)
desc = getDescendants(lca)
for state in configuration
if state in desc
basicStatesExited.add(state)
statesExited.add(state)
for anc in getAncestors(state,lca)
statesExited.add(anc)
sortedStatesExited = statesExited.sort( lambda (s1,s2) : getDepth(s2) - getDepth(s1))
return [basicStatesExited,sortedStatesExited]
function getStatesEntered computes the states that have been entered, given a set of transitions. First, all state targets of the given transition set are added to statesToRecursivelyAdd. Next, the algorithm loops so that composite states with initial sub-states are added to statesToRecursivelyAdd. Furthermore, at each step of the loop, the algorithm searches for children of parallel states without descendants in states to enter, as it is possible that some descendants of parallel states had been added to statesToEnter, but other children of those parallel states had not yet been - this subroutine ensures that there will not exist any parallel states in statesToEnter whose children are not also in statesToEnter. If no such parallel states exist, then statesToRecursivelyAdd will be empty at the end of the loop, and the loop will terminate. Finally, all states in statesEntered are sorted by depth and returned.
function getStatesEntered(transitions)
statesToRecursivelyAdd = []
for transition in transitions
for state in transition.targets
statesToRecursivelyAdd.push(state)
statesToEnter = new Set()
basicStatesToEnter = new Set()
while not statesToRecursivelyAdd.isEmpty()
for state in statesToRecursivelyAdd
recursivelyAddStatesToEnter(state,statesToEnter,basicStatesToEnter)
#add children of parallel states that are not already in statesToEnter to statesToRecursivelyAdd
statesToRecursivelyAdd = []
for s in statesToEnter
if s.kind is PARALLEL
for c in s.children
if c.kind isnt HISTORY and not c in statesToEnter
statesToRecursivelyAdd.push(c)
sortedStatesEntered = statesToEnter.sort( lambda (s1,s2) : getDepth(s1) - getDepth(s2))
return [basicStatesToEnter,sortedStatesEntered]
procedure recursivelyAddStatesToEnter is called by procedure getStatesEntered. It accepts a state s, and lists of states statesToEnter and basicStatesToEnter, which get mutated in each recursive call. If s is a history state, then if its previous history value was set, the history value is added to statesToEnter and basicStatesToEnter; otherwise, the default history state is used. If s is not a history state, then s is added to statesToEnter. Furthermore, if s is a parallel state, then the children of s are also added, and s is called recursively. If s is a composite state, then the initial state of s is added recursively. Finally, if s is a basic, initial, or final state, then s is added to basicStatesToEnter.
procedure recursivelyAddStatesToEnter(s,statesToEnter,basicStatesToEnter)
if s.kind is HISTORY
if historyValue.hasKey(s.id)
for historyState in historyValue[s.id]
recursivelyAddStatesToEnter(historyState,statesToEnter,basicStatesToEnter)
else
statesToEnter.add(s)
basicStatesToEnter.add(s)
else
statesToEnter.add(s)
if s.kind is PARALLEL
for child in s.children
if not (child.kind is HISTORY) #don't enter history by default
recursivelyAddStatesToEnter(child,statesToEnter,basicStatesToEnter)
else if s.kind is COMPOSITE
recursivelyAddStatesToEnter(s.initial,statesToEnter,basicStatesToEnter)
else if s.kind is INITIAL or s.kind is BASIC or s.kind is FINAL
basicStatesToEnter.add(s)
function selectTransitions accepts an eventSet and a datamodel, and returns a set of priority-enabled transitions.
selectTransitions first computes a full configuration from the basic configuration. Transitions are then selected for each state given the set of events and the datamodel, and each transition in the returned set of enabled transitions is added to the set of all enabled transitions. Finally, selectPriorityEnabledTransitions is called to select transitions by their priority, and the result is returned.
function selectTransitions(eventSet,datamodelForNextStep)
states = new Set
#get full configuration, unordered
#this means we may select transitions from parents before children
for basicState in configuration
state.add(basicState)
for ancestor in getAncestors(basicState)
state.add(ancestor)
enabledTransitions = new Set()
for state in states
for transition in getActiveTransitions(state,eventSet)
enabledTransitions.add(transition)
return selectPriorityEnabledTransitions(enabledTransitions)
function getActiveTransitions accepts a state and a set of events, and returns a set of enabled transitions. For each state's transitions, the transitions which are either are default transitions (do not have an event attribute), or where the transition's specified event matches the name of an event in the given set of events, and where the transition either does not have a condition, or the transition does have a condition, and the condition evaluates to true, are added to the set of enabled transitions to return.
function getActiveTransitions(state,events)
transitions = new Set()
for t in state.transitions
if (t does not have a trigger or events.some(lambda e : nameMatch(e.name,t.event))) and (t does not have a condition or t's condition evaluates to true)
transitions.add(t)
return transitions
function selectPriorityEnabledTransitions accepts a set of transitions, and returns a set of priority-enabled transitions.
selectPriorityEnabledTransitions first gets consistentTransitions and inconsistentTransitionsPairs from function getInconsistentTransitions, and adds the consistentTransitions to the set of priorityEnabledTransitions. It then loops until inconsistentTransitionsPairs is empty, at each step creating a new set of transitions, and adding to it the transition with higher priority given each pair of transitions in inconsistentTransitionsPairs. getInconsistentTransitions is then called again to update consistentTransitions and inconsistentTransitionsPairs given the new transition set. The updated consistentTransitions will then be added to the set of priorityEnabledTransitions. This will eventually reach a stable state where there are no longer any transitions pairs which conflict, at which point the set of priority-enabled transitions will have been computed, and will be returned.
function selectPriorityEnabledTransitions(transitions)
priorityEnabledTransitions = new Set()
[consistentTransitions, inconsistentTransitionsPairs] = getInconsistentTransitions(transitions)
priorityEnabledTransitions.union(consistentTransitions)
while not inconsistentTransitionsPairs.isEmpty()
transitions = new Set()
for transitionPair in inconsistentTransitionsPairs
transitions.add(getTransitionWithHigherSourceChildPriority(transitionPair))
[consistentTransitions, inconsistentTransitionsPairs] = getInconsistentTransitions(transitions)
priorityEnabledTransitions.union(consistentTransitions)
return priorityEnabledTransitions
function getTransitionWithHigherSourceChildPriority accepts a pair of transitions, and compares them based first on depth, then based on document order, then returns the one with the highest priority.
This function implements the following semantic option:
- Priority: Source-Child
function getTransitionWithHigherSourceChildPriority(t1,t2)
if getDepth(t1.source) < getDepth(t2.source)
return t2
else if getDepth(t2.source) < getDepth(t1.source)
return t1
else
if t1.documentOrder < t2.documentOrder
return t1
else
return t2
function getInconsistentTransitions accepts a set of transitions, and returns a set of consistent transitions (consistentTransitions), and a set of pairs of inconsistent transitions. getInconsistentTransitions compares transitions pairwise to determine if the pair is arena orthogonal (if their LCAs are orthogonal). Those transitions that are not arena orthogonal are added to allInconsistentTransitions, and transition pairs that are not arena orthogonal with one-another are added to inconsistentTransitionsPairs. The transitions not in conflict are then computed through set difference operation with the set of all transitions, and the result is assigned to consistentTransitions. Finally, consistentTransitions and inconsistentTransitionsPairs are returned.
This function implements the following semantic options:
- Transition Consistency: Small-step consistency: Source/Destination Orthogonal
- Interrupt Transitions and Preemption: Non-preemptive
function getInconsistentTransitions(transitions)
allInconsistentTransitions = new Set()
inconsistentTransitionsPairs = new Set() #set of pairs of transitions
transitionList = transitions.toList()
for i in range(0,transitionList.length)
for j in range(i+1,transitionList.length)
t1 = transitionList[i]
t2 = transitionList[j]
if not isArenaOrthogonal(t1,t2)
allInconsistentTransitions.add(t1)
allInconsistentTransitions.add(t2)
inconsistentTransitionsPairs.add([t1,t2])
consistentTransitions = transitions.difference(allInconsistentTransitions)
return [consistentTransitions,inconsistentTransitionsPairs]
function isArenaOrthogonal takes two transitions and determines if they have the same arena. This means that the LCAs of the source of and target states of each transitions are orthogonal to one-another.
function isArenaOrthogonal(t1,t2)
t1LCA = getLCA(t1)
t2LCA = getLCA(t2)
return isOrthogonalTo(t1LCA,t2LCA)
procedure gen implement's the statechart instance's interface to the outside world. When implemented in single-threaded environments, and assuming a simple model of inter-statchart communication is used, this interface can be very simple, in essence passing the given event straight through to the performBigStep procedure. When implemented in multi-threaded environments, however, then more sophisticated concurrency constructs would be needed in order to enforce the chosen statechart semantics. These constructs will likely be platform-specific - for example, when running under the Java Virtual Machine, Java concurrency primitives would be used to synchronize procedure gen for a given Statecharts instance.
This section will likely be expanded later on.
procedure gen implements the following semantic option:
- External Event Communication: Asynchronous
procedure gen(e)
performBigStep(e)
This evaluates actions. Only pseudocode for the and actions are shown.
procedure evaluateAction(action,eventSet,datamodelForNextStep,eventsToAddToInnerQueue)
switch action.type
case "send"
eventsToAddToInnerQueue.add(new Event(action.event,data)
case "assign"
datamodelForNextStep[action.location] = evaluateAction(action.expr,datamodelForNextStep,eventSet)