DataflowDesynchronization Module
This module implements data types and functions to reason about dataflow process networks. Among others, there are functions to classify a node concerning sequentiality, (weak) endochrony, Kahn criteria and to run a network of nodes on a given input state.
Types
| Type | Description |
InputPatValue describes one possible element in an input pattern which is either a variable, a constant or the absent value. |
|
|
InputPattern is matched against one input FIFO buffer and is either a prefix pattern or a fixed size pattern. Prefix patterns match if the FIFO buffer's prefix will match, while fixed size patterns must match with the entire content of the buffer |
|
|
A node is defined by its name, the declarations of its input and output variables, rules for the initial reaction, and the other rules for the remaining reactions. |
Functions and values
| Function or value | Description |
Full Usage:
ComputeOverlaps node
Parameters:
NodeDPN
Returns: (int * int * (Map<Expr, InputPatValue> * InputPatValue[][]))[]
|
This function checks whether a given node has overlapping firing rules. The function computes an array of triples (i,j,(rho,pl)) meaning two rules node.rules[i] and node.rules[j]that overlap with pattern pl when applying substitution rho to their input patterns.
|
|
This function shall be called by the html page.
|
|
Desynchronize a node, i.e., remove all PatAbsent values in its input patterns.
|
Full Usage:
OverlappingRuleRaces node (i, j, arg4)
Parameters:
NodeDPN
i : int
j : int
arg3 : 'a * 'b
Returns: int[] * int[]
|
This function computes for two two overlapping rules the indices of the inputs and outputs that suffer under races of these rules.
|
|
parse a node
|
|
print a node as a html firing table
|
Full Usage:
SubstPatValue rho p
Parameters:
Map<Expr, InputPatValue>
p : InputPatValue
Returns: InputPatValue
|
substitute pattern values with a substitution rho
|
Full Usage:
SubstPattern rho p
Parameters:
Map<Expr, InputPatValue>
p : InputPattern
Returns: InputPattern
|
substitute patterns with a substitution rho
|
Full Usage:
UnifyRules (inp1, act1) (inp2, act2)
Parameters:
InputPattern[]
act1 : 'a
inp2 : InputPattern[]
act2 : 'b
Returns: (Map<Expr, InputPatValue> * InputPatValue[][]) option
|
UnifyRules computes for two given rules (inp1,act1) and (inp2,act2) a substitution rho and a pattern list such that the two rules are applicable to the pattern list when the substitution rho is applied to their patterns. If the two rules are non-overlapping, the function returns None, otherwise, Some(rho,pl) with the substitution rho and the pattern array pl.
|