class Cell {
  var x: int;
  
  // --- some predicates ---
  
  predicate write1 { acc(x) } // full permission in a predicate
  predicate write2 { acc(x,10) } // 10%
  predicate read1 { rd(x) } // fractional read permission
  predicate read2 { rd*(x) } // starred fractional read permission
  predicate read3 { rd(x,1) } // counting permission (1 epsilon)
  
  // --- invalid permission scaling ---
  
  method error()
    requires rd(read3,1);
  {
    unfold rd(read3,1); // ERROR: scaling epsilons is not possible
  }
  
}