mod LIBRARY-PETRI-NET is
  sorts Place Marking .
  subsort Place < Marking .
  op 1 : -> Marking .
  op __ : Marking Marking -> Marking [assoc comm id: 1] .
  ops a b n r j : -> Place .

  var M : Marking .

  rl [buy] : r r r r => j j j j j j j j .
  rl [file] : j => a .
  rl [borr] : a => b .
  rl [ret] : b => a .
  rl [lose] : b => n .
  rl [disc] : a => n .
  rl [req1] : n n => r r .
  rl [req2] : M => M r .       *** New requests can now placed.
endm

set trace on .

rew [10] 1 .

***(
rewrite [10] in LIBRARY-PETRI-NET : 1 .
*********** rule
rl [req2]: M => r M .
M:Marking --> 1
1
--->
r 1
*********** rule
rl [req2]: M => r M .
M:Marking --> r
r
--->
r r
*********** rule
rl [req2]: M => r M .
M:Marking --> r r
r r
--->
r r r
*********** rule
rl [req2]: M => r M .
M:Marking --> r r r
r r r
--->
r r r r
*********** rule
rl [buy]: r r r r => j j j j j j j j .
empty substitution
r r r r
--->
j j j j j j j j
*********** rule
rl [req2]: M => r M .
M:Marking --> j j j j j j j j
j j j j j j j j
--->
r j j j j j j j j
*********** rule
rl [req2]: M => r M .
M:Marking --> r j j j j j j j j
r j j j j j j j j
--->
r r j j j j j j j j
*********** rule
rl [req2]: M => r M .
M:Marking --> r r j j j j j j j j
r r j j j j j j j j
--->
r r r j j j j j j j j
*********** rule
rl [req2]: M => r M .
M:Marking --> r r r j j j j j j j j
r r r j j j j j j j j
--->
r r r r j j j j j j j j
*********** rule
rl [buy]: r r r r => j j j j j j j j .
empty substitution
r r r r j j j j j j j j
--->
j j j j j j j j j j j j j j j j
rewrites: 10 in -10ms cpu (0ms real) (~ rewrites/second)
result Marking: j j j j j j j j j j j j j j j j
)

set trace off .