From 6d5f351f1e3a6dad5235133cf6f30a9104087f28 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Thu, 24 Oct 2024 14:14:03 +0100 Subject: [PATCH] Fix for POGTests --- .../test/java/com/fujitsu/vdmj/junit/PogTest.java | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/vdmj/src/test/java/com/fujitsu/vdmj/junit/PogTest.java b/vdmj/src/test/java/com/fujitsu/vdmj/junit/PogTest.java index ebaaa92db..fc88558b4 100644 --- a/vdmj/src/test/java/com/fujitsu/vdmj/junit/PogTest.java +++ b/vdmj/src/test/java/com/fujitsu/vdmj/junit/PogTest.java @@ -90,11 +90,11 @@ protected void tearDown() throws Exception /* 24 */ "(forall mk_(i, $any1):(int) * (int) &\n 1 in set dom m)\n", /* 25 */ "(forall mk_(i, $any1):(int) * (int) &\n (forall x in set {m(1), 2, 3} &\n x in set dom m))\n", /* 26 */ "(forall mk_(i, $any1):(int) * (int) &\n (forall x in set {m(1), 2, 3} & (m(x) < i) =>\n x in set dom m))\n", - /* 27 */ "(let x:int = m(1) in\n 1 in set dom m)\n", + /* 27 */ "1 in set dom m\n", /* 28 */ "(let x:int = m(1) in\n x in set dom m)\n", - /* 29 */ "(let local: int -> int local(x) == m(x) in\n (forall x:int &\n x in set dom m))\n", - /* 30 */ "(let x = m(1) in\n 1 in set dom m)\n", - /* 31 */ "(let x = m(1) in\n (let y = m(2) in\n 2 in set dom m))\n", + /* 29 */ "(forall x:int &\n x in set dom m)\n", + /* 30 */ "1 in set dom m\n", + /* 31 */ "(let x = m(1) in\n 2 in set dom m)\n", /* 32 */ "(let x = m(1), y = m(2) in\n x in set dom m)\n", /* 33 */ "(let x = m(1), y = m(2) in\n y in set dom m)\n", /* 34 */ "exists1 x in set {1, 2, 3} & (x < 10)\n", @@ -128,10 +128,10 @@ protected void tearDown() throws Exception /* 62 */ "dom {1 |-> false} subset inds [2, true, 7.8]\n", /* 63 */ "is_(([2, true, 7.8] ++ {1 |-> false}), seq of (bool | nat))\n", /* 64 */ "(forall t:((nat) * (nat) * (nat)) | ((nat) * (nat)) &\n is_(t, (nat) * (nat) * (nat)))\n", - /* 65 */ "(forall u:U &\n (let mk_(a, b):U = u in\n exists mk_(a, b):U & mk_(a, b) = u))\n", - /* 66 */ "(forall u:U &\n (let mk_(a, b):U = u in\n is_(u, (nat) * (nat))))\n", + /* 65 */ "(forall u:U &\n exists mk_(a, b):U & mk_(a, b) = u)\n", + /* 66 */ "(forall u:U &\n is_(u, (nat) * (nat)))\n", /* 67 */ "(is_([1, 2, true], T1) and ((is_(1, bool)) and (is_(2, bool)))) or (is_([1, 2, true], T2) and inv_T2([1, 2, true]))\n", - /* 68 */ "(forall t:T1 | T2 &\n (let x:T1 | T2 = [1, 2, 3, true] in\n (is_([1, 2, 3, true], T1) and ((is_(1, bool)) and (is_(2, bool)) and (is_(3, bool)))) or (is_([1, 2, 3, true], T2) and inv_T2([1, 2, 3, true]))))\n", + /* 68 */ "(forall t:T1 | T2 &\n (is_([1, 2, 3, true], T1) and ((is_(1, bool)) and (is_(2, bool)) and (is_(3, bool)))) or (is_([1, 2, 3, true], T2) and inv_T2([1, 2, 3, true])))\n", /* 69 */ "(forall a:T1 | T2 | int &\n (is_(a, T1) and (is_(a, seq of bool))) or (is_(a, T2) and inv_T2(a)))\n", /* 70 */ "is_({1 |-> \"2\"}, inmap nat1 to seq1 of char)\n", /* 71 */ "(forall n:nat1, x:nat1 &\n (not (n < 2) =>\n (n - 1) > 0))\n",