summaryrefslogtreecommitdiff
path: root/omegalib/examples/old_test/tseng.oc-rt
diff options
context:
space:
mode:
Diffstat (limited to 'omegalib/examples/old_test/tseng.oc-rt')
-rw-r--r--omegalib/examples/old_test/tseng.oc-rt54
1 files changed, 54 insertions, 0 deletions
diff --git a/omegalib/examples/old_test/tseng.oc-rt b/omegalib/examples/old_test/tseng.oc-rt
new file mode 100644
index 0000000..53ff139
--- /dev/null
+++ b/omegalib/examples/old_test/tseng.oc-rt
@@ -0,0 +1,54 @@
+# Omega Calculator v1.2 (based on Omega Library 1.2, August, 2000):
+# symbolic n;
+#
+# symbolic LV,UV;
+#
+# D := {[ i,i+1] -> [i+1,k] : 1 <= i && i+1 < k <= n};
+#
+# local := {[i1,k1] -> [i2,k2] : LV <= k1,k2 <= UV };
+#
+# sameP := {[i1,k1] -> [i2,k2] : k1=k2 || LV <= k1,k2 <= UV };
+#
+# myIter := {[i,k] : LV <= k <= UV};
+#
+# lexPos := {[i1,k1] -> [i2,k2] : i1 = i2 && k1 < k2 || i1 < i2};
+#
+#
+# post := D restrictDomain myIter;
+#
+# wait := D restrictRange myIter;
+#
+# enforcedTime := sameP intersection lexPos;
+#
+# enforcedTime;
+
+{[i1,k1] -> [i1,k2] : LV <= k1 < k2 <= UV} union
+ {[i1,k1] -> [i2,k1] : i1 < i2} union
+ {[i1,k1] -> [i2,k2] : LV <= k1,k2 <= UV && i1 < i2}
+
+#
+# enforced := enforcedTime compose D union D compose enforcedTime union enforcedTime;
+#
+# enforced;
+
+{[i1,i1+1] -> [i2,k2] : 1 <= i1 <= n-2, UV-2, i2-2 && LV <= k2 <= UV && LV <= n} union
+ {[i1,k1] -> [i2,k2] : k1 = 1+i1 && 1 <= i1 <= i2-2, k2-2 && k2 <= n} union
+ {[i1,i1+1] -> [i1+1,k2] : 1 <= i1 <= n-2, k2-3 && LV < k2 <= UV && LV <= n} union
+ {[i1,k1] -> [i2,k2] : 2, LV, i1+2 <= i2 < k2 <= n && LV <= k1 <= UV && i2 <= UV} union
+ {[i1,k1] -> [k1,k2] : 2, i1+2 <= k1 < k2 <= n} union
+ {[i1,k1] -> [i1+1,k2] : LV <= k1 <= i1 <= k2-2, UV-1 && k2 <= n && 1 <= i1} union
+ {[i1,k1] -> [i2,k2] : LV <= k1,k2 <= UV && i1 < i2} union
+ {[i1,k1] -> [i2,k1] : i1 < i2} union
+ {[i1,k1] -> [i1,k2] : LV <= k1 < k2 <= UV}
+
+#
+# post - enforced;
+
+{[In_1,In_1+1] -> [In_1+1,Out_2] : 1, LV-1 <= In_1 < UV < Out_2 <= n}
+
+#
+# wait - enforced;
+
+{[In_1,In_1+1] -> [In_1+1,LV] : In_1+2 <= LV <= n, UV && 1 <= In_1}
+
+#