# The Symphony IDE

Formal Modelling for Systems of Systems

Go to our GitHub Profile ## DataFlow

Author: Jim Woodcock

The data flow machine transforms its sequence of values in its input channel into a sequence of computations in its output channel. It shows how the use of parallel processes can speed up the computation. An important idiom is introduced: the use of ghost variables and a ghost process to demonstrate the correctness of the computation. A second important idiom is the use of data independence in model checking: the behaviour of the data flow machine does not depend on decisions taken on the basis of its inputs, it merely transforms the data. This means that checks for deadlock and livelock freedom of the network of processes in the machine can be carried out with synchronisations rather than communications. In this case, the infinite state data flow machine can be easily model checked with only 24 states.

### DataFlow.cml

``````channels

left, left1, left2, mid, right : nat
diverge : nat

values

a : nat = 2

b : nat = 5

process DataFlow = begin

state

inseq : seq of nat := []

outseq : seq of nat := []

functions

StateInv: seq of nat * seq of nat -> bool
StateInv(inlist,outlist) ==
len inlist >= len outlist and
outlist = [a*inlist(i) + b * inlist(i+1) | i in set inds outlist]
--Func(inlist,outlist)

Func: seq of nat * seq of nat -> seq of nat
Func(inlist,outlist) ==
[a*inlist(i) + b * inlist(i+1) | i in set inds outlist]

actions

X21 = left1?x -> mid!(a * x) -> X21

X22 = left2?y -> mid?z -> (dcl r : nat := z + b*y @ right!r -> X22)

X23 = left?x -> left1!x -> X24

X24 = left?x -> left2!x -> left1!x -> X24

GHOST = (left?x -> inseq:= inseq ^[x]; GHOST
[] right?r -> outseq := outseq ^[r]; GHOST
[] INVBROKEN)

INVBROKEN = [not StateInv(inseq,outseq)] & Diverge
@

(X23 [| {| left1,left2 |} |]
( X21 [| {| mid |} |] X22 ) ) [| {| left, right |} |] GHOST

end
``````