RelView Examples - Algorithms on Petri Nets

```{************************************************************
Column-wise computation of the set of all markings of a C/E
Petri net with conditions C, events E, and two relations
R : C <-> E and S : E <-> C which are reachable from marking
m : C <-> 1 (see R. Behnke, 2nd ToolsWorkshop, Bremen, 1996)
************************************************************}

ReachMarkings(R,S,m)
DECL epsiB, e, res, x, h1, h2, n, vn, k, pk
BEG  epsiB = epsi(dom(R));
x = syq(epsiB,m);
res = O(x);
WHILE -empty(x) DO
res = res | x;
h1 = x;
x = O(x);
WHILE -empty(h1) DO
n = point(h1);
h1 = h1 & -n;
vn = epsiB * n;
h2 = Ln1(S);
WHILE -empty(h2) DO
e = point(h2);
h2 = h2 & -e;
IF incl(R * e,vn)
THEN IF incl(vn, -(S^ * e))
THEN k = (vn & -(R * e)) | S^ * e;
pk = syq(epsiB,k);
IF incl(pk,-res)
THEN x = x | pk
FI
FI
FI
OD
OD
OD
RETURN epsiB * inj(res)^
END.

{************************************************************
Computation of the reachability relation on the markings
for a C/E Petri net with conditions C, events E, relations
R : C <-> E and S : E <-> C (see TACAS 96)
************************************************************}

Trans(R,S,e)
DECL eps, L, res
BEG  eps = epsi(dom(R));
L = L1n(eps);
res = (R * e * L \ eps)^;
res = res & (S^ * e * L \ -eps)^;
res = res & syq((eps & -(R * e) * L) | S^ * e * L, eps)
RETURN res
END.

ReachRel(R,S)
DECL e, res
BEG  e = init(dom(S));
res = Trans(R,S,e);
WHILE -empty(next(e)) DO
e = next(e);
res = res | Trans(R,S,e)
OD
RETURN rtc(res)
END.

{************************************************************
Column-wise representation of the set of all markings of a
C/E Petri as above, which are reachable from a marking m :
************************************************************}

ReachVect(R,S,m)
DECL v, e, eps, res
BEG  eps = epsi(dom(R));
res = O(eps^ * eps);
v = Ln1(dom(S));
WHILE -empty(v) DO
e = point(v);
res = res | Trans(R,S,e);
v = v & -e
OD
RETURN rtc(res)^ * syq(eps,m)
END.

ReachList(R,S,m) = epsi(dom(R)) * inj(ReachVect(R,S,m))^.

{************************************************************
Column-wise representation of the set of live markings of a
************************************************************}

Enable(R,S)
DECL eps
BEG  eps = epsi(dom(R))
RETURN (eps^ / R^) & (-eps^ / S)
END.

LiveVect(R,S)