This module implements algorithms for analyzing dataflow process networks. In particular, for static DPNs it can decide whether there is a static periodic schedule and whether the DPN is bounded, and for dynamic DPNs, it can compute the product firing table for the entire DPN and can decide about the (weak) endochrony and Kahn criteria of its nodes.
Function or value  Description 




Full Usage:
GetTopologyMatrixAndRateVector dpn
Parameters:
CycloStaticDPN
Returns: rat[,] * int[] option



Parse a (cyclo)static DPN with its producer/consumer relationship. The expected input string may look as follows (having line breaks or ";" to separate single equations: (a0:1,a1:1,a4:2,a7:4) = init() (a0:1) = f0() (a2:1) = f1(a1:1) (a1:1,a3:1) = f2(a0:1,a2:1) (a5:2) = f3(a4:2) (a4:2,a6:2) = f4(a3:2,a5:2) (a8:3) = f5(a7:3) (a7:3,a9:3) = f6(a6:3,a8:3) () = out(a9:3)The numbers after the buffer names denote the number of tokens produced and consumed. For a cyclostatic DPN, one has to list the numbers of the corresponding periods separated by :. Note that every buffer must have no more than one producer and one consumer node, but we allow input and output buffers which have no producer and no consumer. The first equation is special, it is not a process node; instead, it defines the initial configuration of the DPN. You may also say that this node fires only at initial time while the rest fires afterwards. For its outputs, you may ignore those buffers that have initially zero tokens.

Full Usage:
PeriodicSchedule dpn rv s
Parameters:
CycloStaticDPN
rv : int[] option
s : int[]
Returns: bool * (Set<int> * int[]) list * int[]

Given a vector rv such that rv[i] is the number of desired firings of periods of process i, this function explores the state transition system starting from a state s until all nodes have fired according to rv[i] or none of the nodes that should still fire cannot fire anymore. To this end, all nodes that can fire in a state are fired at once, i.e., we compute an ASAP schedule which consists then in a sequence of states. The result is a pair (success,schedule,maxBuf) where success is true iff all firings have been scheduled, and schedule is a list of pairs (act,state) such that this list describes a path from the given state following act to a successor state. An action is thereby a set of process nodes (indices), and a state is an array mapping each buffer('s index) to the number of tokens it holds. Finally, maxBuf is an array that hold for every buffer b the maximal size maxBuf[b] required for the schedule.


