-- A sample file to try out failures and divergences in FDR

channel a, b

diva = a -> diva
div = diva \{a}

DF(X) = |~| x:X @ x -> DF(X)

RUN(X) = [] x:X @ x -> RUN(X)

P1 = a -> div

P2 = a -> STOP


-- assert the following items (they should be true)
assert P1 [FD= P2

assert P2 :[ divergence free ]



-- assert the following items (they should be false)

assert P1 [F= P2
assert P2 :[ deadlock free ]

assert P1 :[ divergence free ]