1 files changed, 81 insertions, 0 deletions
diff --git a/Chalice/tests/general-tests/triggers.chalice b/Chalice/tests/general-tests/triggers.chalice
new file mode 100644
index 00000000..08a6a7dd
--- /dev/null
+++ b/Chalice/tests/general-tests/triggers.chalice
@@ -0,0 +1,81 @@
+// this test is for the automatic trigger generation
+
+class Triggers
+{
+  var next : Triggers // to allow recursive definitions
+  
+  predicate valid { acc(next) && next != null && next.valid } // intentionally doesn't terminate - allows function definitions to be unknown
+ 
+  function f(x,y,z : int):bool
+    requires valid
+  {
+    unfolding valid in next.f(x,y,z) // unknown definition
+  }
+  
+  function h(x,y,z : int):bool
+    requires valid
+  {
+    unfolding valid in next.h(x,y,z) // unknown definition
+  }
+  
+  function g(x : int) : bool
+    requires valid
+  {
+    unfolding valid in next.g(x) // unknown definition
+  }
+  
+  function i(x:int, y:bool) : bool
+    requires valid
+  {
+    unfolding valid in next.i(x,y) // unknown definition
+  }
+  
+  
+  method triggers_one()
+    requires valid
+    requires (forall a : int :: !(g(a) ==> false))
+    ensures valid
+    ensures (forall b : int :: g(b))
+    { }
+    
+  method triggers_two()
+    requires valid
+    requires (forall a,b,c : int :: ( g(a) && f(a,b,c)))
+    ensures valid
+    ensures (forall x,y,z : int :: f(x,y,z))
+    ensures (forall w : int :: (g(w))) // fails because there isn't a good enough trigger for finding g(w)
+    { }
+    
+  method triggers_three()
+    requires valid
+    requires (forall a : int :: ( g(a) && (forall b,c : int :: f(a,b,c))))
+    ensures valid
+    ensures (forall x,y,z : int :: f(x,y,z)) // fails because of the trigger chosen for a (g(a)).
+    ensures (forall w : int :: (g(w)))
+    { }
+    
+  method triggers_four()
+    requires valid
+    requires (forall a,b,c,d,e:int :: f(a,b,c) && h(b,c,d) && f(c,d,e))
+    ensures valid
+    ensures (forall x,y,z : int :: f(x,y,z)) // fails - not enough triggers
+    ensures (forall x,y,z : int :: f(x,y,z) && f(z,y,x)) // succeeds - {f(a,b,c),f(c,d,e)} is one of the trigger sets which should be found
+    { }      
+
+  method triggers_five(c : bool, d : bool)
+    requires c ==> d
+    requires valid
+    requires (forall x : int :: i(x, (c ==> d))) // check that logical operators are suitably avoided in triggers
+    ensures valid
+    ensures i(4,true)
+    { }
+    
+  method triggers_six(c : int, d : int)
+    requires c > d
+    requires valid
+    requires (forall x : int :: i(x, (c > d))) // check that logical operators are suitably avoided in triggers
+    ensures valid
+    ensures i(4,true)
+    { }
+    
+}
+\ No newline at end of file