<html><head><meta name="color-scheme" content="light dark"></head><body><pre style="word-wrap: break-word; white-space: pre-wrap;">class Customer {

    int ticket;
    int phase = 0;
    static int max = 0;

    //@ static invariant max &gt;= 0;

    // only one customer in crit section
    /*@ static invariant
      @   (\forall Customer c1;
            (\forall Customer c2; 
      @      c1.phase == 2 &amp;&amp; c2.phase == 2 ==&gt; c1 == c2));
      @*/

    // customer in crit section is minimal
    /*@ static invariant
      @   (\forall Customer c1;  c1.phase==2;
      @      (\forall Customer c2;  c1!=c2 &amp;&amp; c2.phase &gt;= 1; 
      @         c2.ticket &gt; c1.ticket));
      @*/

    //@ invariant phase &gt;= 0 &amp;&amp; phase &lt;= 2;
    //@ invariant ticket &gt;= 0 &amp;&amp; ticket &lt;= max;

    /*@
      @ requires phase == 1 &amp;&amp; 
      @   (\forall Customer c;  c!=this &amp;&amp; c.phase &gt;= 1; 
      @       c.ticket &gt; ticket);
      @ ensures phase == 2;
      @*/
    void enter() {
	phase = 2;
    }

    /*@
      @ requires phase == 2;
      @ ensures phase == 0;
      @ ensures ticket == 0;
      @*/
    void leave() {
	phase = 0;
	ticket = 0;
    }

    /*@
      @ requires phase == 0;
      @ ensures phase == 1;
      @*/
    void request() {
	phase = 1;
	ticket = ++max;
    }
}</pre></body></html>