From 76dc1c3b53f2b79fddf3f96f7b1a394ae08f1b71 Mon Sep 17 00:00:00 2001 From: Neil Brown Date: Wed, 12 Dec 2007 17:21:25 +0000 Subject: [PATCH] Added another test for the Omega Test --- transformations/RainUsageCheckTest.hs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/transformations/RainUsageCheckTest.hs b/transformations/RainUsageCheckTest.hs index b2ad12b..83ed12e 100644 --- a/transformations/RainUsageCheckTest.hs +++ b/transformations/RainUsageCheckTest.hs @@ -311,6 +311,9 @@ testArrayCheck = TestList ,pass (4, [], [[0,1,1], [-8,4,0], [4,0,2]], []) -- - x_1 + x_2 = 0, 4x_1 = 8, 2x_2 = 4 ,pass (5, [], [[0,-1,1], [-8,4,0], [-4,0,2]], []) + -- -x_1 = -9, 3 + 2x_1 >= 0 --> 21 >= 0 + ,pass (6, [[21,0]], [[9,-1]], [[3,2]]) + -- From the Omega Test paper (x = x_1, y = x_2, z = x_3, sigma = x_1 (effectively)): ,pass (100, [[11,13,0,0], [28,-13,0,0], [47,-5,0,0], [53,5,0,0]], [[-17,7,12,31], [-7,3,5,14]],