changed type checking of yield procedures so that they can only call other yielding procedures

1 files changed, 2 insertions, 2 deletions

diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl
index f875d6e5..68e308d0 100644
--- a/Test/og/ticket.bpl
+++ b/Test/og/ticket.bpl
@@ -33,7 +33,7 @@ function {:inline} Inv2(tickets: [int]bool, ticket: int, lock: X): (bool)
     if (lock == nil) then tickets == RightOpen(ticket) else tickets == RightClosed(ticket)

 }

 

-procedure Allocate({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X);

+procedure {:yields} {:layer 2} Allocate({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X);

 ensures {:layer 1} {:layer 2} xl != nil;

 

 procedure {:yields} {:layer 2} main({:linear_in "tid"} xls':[X]bool)

@@ -53,7 +53,7 @@ requires {:layer 2} xls' == mapconstbool(true);
     invariant {:layer 1} Inv1(T, t);

     invariant {:layer 2} Inv2(T, s, cs);

     {

-        call xls, tid := Allocate(xls);

+        par xls, tid := Allocate(xls) | Yield1() | Yield2();

         async call Customer(tid);

     	par Yield1() | Yield2();

     }