This example demonstrates a strange result, found after simulating
10 steps.  The final result seems to allow members to rent out
more videos than exist in the current stockLevel.  However, this
turns out because addTitle(title, level) allows you to add 0
copies at a subsequent stage, which *resets* the stock level,
rather than adding to it!  It's a fault in the Z.



sal > (display-curr-trace)
Step 0:
--- Input Variables (assignments) ---
(= p? PERSON__1);
(= t? TITLE__2);
(= level? 3);
--- System Variables (assignments) ---
(= (members PERSON__1) false);
(= (members PERSON__2) false);
(= (members PERSON__3) false);
(= (rented (mk-tuple PERSON__1 TITLE__1)) false);
(= (rented (mk-tuple PERSON__2 TITLE__1)) false);
(= (rented (mk-tuple PERSON__3 TITLE__1)) false);
(= (rented (mk-tuple PERSON__1 TITLE__2)) false);
(= (rented (mk-tuple PERSON__2 TITLE__2)) false);
(= (rented (mk-tuple PERSON__3 TITLE__2)) false);
(= (rented (mk-tuple PERSON__1 TITLE__3)) false);
(= (rented (mk-tuple PERSON__2 TITLE__3)) false);
(= (rented (mk-tuple PERSON__3 TITLE__3)) false);
(= (rented (mk-tuple PERSON__1 TITLE__B)) false);
(= (rented (mk-tuple PERSON__2 TITLE__B)) false);
(= (rented (mk-tuple PERSON__3 TITLE__B)) false);
(= (stockLevel TITLE__1) 4);
(= (stockLevel TITLE__2) 4);
(= (stockLevel TITLE__3) 4);
(= (stockLevel TITLE__B) 4);
(= copies_ 1);
(= invariant__ true);
------------------------
Transition Information: 
(module instance at [Context: scratch, line(1), column(11)]
  (label AddTitle
    transition at [Context: video, line(61), column(10)]))
------------------------
Step 1:
--- Input Variables (assignments) ---
(= p? PERSON__2);
(= t? TITLE__3);
(= level? 3);
--- System Variables (assignments) ---
(= (stockLevel TITLE__2) 3);
------------------------
Transition Information: 
(module instance at [Context: scratch, line(1), column(11)]
  (label AddMember
    transition at [Context: video, line(87), column(10)]))
------------------------
Step 2:
--- Input Variables (assignments) ---
(= p? PERSON__2);
(= t? TITLE__2);
(= level? 2);
--- System Variables (assignments) ---
(= (members PERSON__2) true);
------------------------
Transition Information: 
(module instance at [Context: scratch, line(1), column(11)]
  (label RentVideo
    transition at [Context: video, line(45), column(10)]))
------------------------
Step 3:
--- Input Variables (assignments) ---
(= p? PERSON__2);
(= t? TITLE__1);
(= level? 2);
--- System Variables (assignments) ---
(= (rented (mk-tuple PERSON__2 TITLE__2)) true);
------------------------
Transition Information: 
(module instance at [Context: scratch, line(1), column(11)]
  (label AddTitle
    transition at [Context: video, line(61), column(10)]))
------------------------
Step 4:
--- Input Variables (assignments) ---
(= p? PERSON__2);
(= t? TITLE__1);
(= level? 2);
--- System Variables (assignments) ---
(= (stockLevel TITLE__1) 2);
------------------------
Transition Information: 
(module instance at [Context: scratch, line(1), column(11)]
  (label RentVideo
    transition at [Context: video, line(45), column(10)]))
------------------------
Step 5:
--- Input Variables (assignments) ---
(= p? PERSON__3);
(= t? TITLE__3);
(= level? 0);
--- System Variables (assignments) ---
(= (rented (mk-tuple PERSON__2 TITLE__1)) true);
------------------------
Transition Information: 
(module instance at [Context: scratch, line(1), column(11)]
  (label AddTitle
    transition at [Context: video, line(61), column(10)]))
------------------------
Step 6:
--- Input Variables (assignments) ---
(= p? PERSON__2);
(= t? TITLE__1);
(= level? 0);
--- System Variables (assignments) ---
(= (stockLevel TITLE__3) 0);
------------------------
Transition Information: 
(module instance at [Context: scratch, line(1), column(11)]
  (label AddTitle
    transition at [Context: video, line(61), column(10)]))
------------------------
Step 7:
--- Input Variables (assignments) ---
(= p? PERSON__1);
(= t? TITLE__2);
(= level? 1);
--- System Variables (assignments) ---
(= (stockLevel TITLE__1) 0);
------------------------
Transition Information: 
(module instance at [Context: scratch, line(1), column(11)]
  (label AddMember
    transition at [Context: video, line(87), column(10)]))
------------------------
Step 8:
--- Input Variables (assignments) ---
(= p? PERSON__1);
(= t? TITLE__2);
(= level? 2);
--- System Variables (assignments) ---
(= (members PERSON__1) true);
------------------------
Transition Information: 
(module instance at [Context: scratch, line(1), column(11)]
  (label RentVideo
    transition at [Context: video, line(45), column(10)]))
------------------------
Step 9:
--- Input Variables (assignments) ---
(= p? PERSON__3);
(= t? TITLE__2);
(= level? 1);
--- System Variables (assignments) ---
(= (rented (mk-tuple PERSON__1 TITLE__2)) true);
------------------------
Transition Information: 
(module instance at [Context: scratch, line(1), column(11)]
  else transition at [Context: video, line(112), column(6)])
------------------------
Step 10:
--- Input Variables (assignments) ---
(= p? PERSON__2);
(= t? TITLE__B);
(= level? 3);
--- System Variables (assignments) ---
(= (members PERSON__1) true);
(= (members PERSON__2) true);
(= (members PERSON__3) false);
(= (rented (mk-tuple PERSON__1 TITLE__1)) false);
(= (rented (mk-tuple PERSON__2 TITLE__1)) true);
(= (rented (mk-tuple PERSON__3 TITLE__1)) false);
(= (rented (mk-tuple PERSON__1 TITLE__2)) true);
(= (rented (mk-tuple PERSON__2 TITLE__2)) true);
(= (rented (mk-tuple PERSON__3 TITLE__2)) false);
(= (rented (mk-tuple PERSON__1 TITLE__3)) false);
(= (rented (mk-tuple PERSON__2 TITLE__3)) false);
(= (rented (mk-tuple PERSON__3 TITLE__3)) false);
(= (rented (mk-tuple PERSON__1 TITLE__B)) false);
(= (rented (mk-tuple PERSON__2 TITLE__B)) false);
(= (rented (mk-tuple PERSON__3 TITLE__B)) false);
(= (stockLevel TITLE__1) 0);
(= (stockLevel TITLE__2) 3);
(= (stockLevel TITLE__3) 0);
(= (stockLevel TITLE__B) 4);
(= copies_ 1);
(= invariant__ false);