Comment by tombert

This was fun to port over to PlusCal to verify it myself:

    EXTENDS Naturals, Sequences
    
    (*--algorithm StateStore {
    
    variables
      n = 0; completions = <<>>; 
    
    define {
        Invar == Len(completions) = 2 => n # 2
    }
    
    fair process (thing \in {"p", "q"})
    variables i = 0, temp = 0; 
      {
       Loop:
            while (i < 10) {
               First:
                   temp := n + 1;
               Second:
                   n := temp;
               Last: 
                   i := i + 1; 
        };
        
        Complete:
            completions := Append(completions, 1)
      }
    }*)

(I acknowledge that this isn't the most elegant Pluscal but I think it is a roughly accurate?)