1 files changed, 0 insertions, 76 deletions
diff --git a/Chalice/tests/permission-model/scaling.chalice b/Chalice/tests/permission-model/scaling.chalice
deleted file mode 100644
index ffe9aac1..00000000
--- a/Chalice/tests/permission-model/scaling.chalice
+++ /dev/null
@@ -1,76 +0,0 @@
-
-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) } // abstract read permission
-  predicate read2 { rd*(x) } // starred read permission
-  predicate read3 { rd(x,1) } // counting permission (1 epsilon)
-  
-  // --- permission scaling ---
-  
-  method s1()
-    requires rd(read1);
-  {
-    unfold rd(read1);
-    assert(rd*(x));
-    assert(rd(x)); // ERROR: should fail
-  }
-  
-  method s2() // INCOMPLETNESS: postcondition should hold, but fails at the moment
-    requires rd(read1);
-    ensures rd(read1);
-  {
-    unfold rd(read1);
-    fold rd(read1);
-  }
-  
-  method s3()
-    requires acc(x);
-    ensures rd(read1);
-  {
-    fold rd(read1);
-    assert(rd*(x));
-    assert(acc(x)); // ERROR: should fail
-  }
-  
-  method s4() // ERROR: postcondition does not hold
-    requires acc(x);
-    ensures read1;
-  {
-    fold rd(read1);
-  }
-  
-  method s5()
-    requires rd(read2);
-  {
-    unfold rd(read2);
-    assert(rd*(x));
-    assert(rd(x)); // ERROR: should fail
-  }
-
-  method s6()
-    requires acc(x);
-    ensures rd(read2);
-  {
-    fold rd(read2);
-    assert(rd*(x));
-    assert(acc(x)); // ERROR: should fail
-  }
-  
-  method s7() // ERROR: postcondition does not hold
-    requires acc(x);
-    ensures read2;
-  {
-    fold rd(read2);
-  }
-  
-  // --- helper functions ---
-  
-  method void() requires rd(x); ensures rd(x); {}
-  method dispose() requires rd(x); {}
-  
-}