{************************************************************ 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 : C <-> 1 (see also TACAS 96) ************************************************************} 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 C/E Petri net as above (see also TACAS 96) ************************************************************} Enable(R,S) DECL eps BEG eps = epsi(dom(R)) RETURN (eps^ / R^) & (-eps^ / S) END. LiveVect(R,S) DECL reach, dead BEG reach = Reach(R,S); dead = -(reach * Enable(R,S)) RETURN -dom(reach * dead) END. LiveList(R,S) = epsi(dom(R)) * inj(LiveVect(R,S))^.