From a94c3d5fccae3088d9ef6e0f70699bc380c336ac Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Thu, 17 Sep 2015 10:08:48 +0200
Subject: [PATCH] Fixed tests
---
src/test/java/de/tlc4b/prettyprint/ArithmeticTest.java | 7 -------
src/test/resources/basics/BBuiltInsTest.mch | 4 ++--
src/test/resources/basics/BBuiltInsTest.prob | 3 ---
3 files changed, 2 insertions(+), 12 deletions(-)
delete mode 100644 src/test/resources/basics/BBuiltInsTest.prob
diff --git a/src/test/java/de/tlc4b/prettyprint/ArithmeticTest.java b/src/test/java/de/tlc4b/prettyprint/ArithmeticTest.java
index 0f2a130..961ad75 100644
--- a/src/test/java/de/tlc4b/prettyprint/ArithmeticTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/ArithmeticTest.java
@@ -127,13 +127,6 @@ public class ArithmeticTest {
compare(expected, machine);
}
- @Test
- public void testPower() throws Exception {
- String machine = "MACHINE test\n" + "PROPERTIES 1 = 1 ** 1\n" + "END";
- String expected = "---- MODULE test----\n" + "EXTENDS Naturals \n"
- + "ASSUME 1 = 1 ^ 1 \n" + "======";
- compare(expected, machine);
- }
@Test
public void testUnaryMinus() throws Exception {
diff --git a/src/test/resources/basics/BBuiltInsTest.mch b/src/test/resources/basics/BBuiltInsTest.mch
index b1bde6d..5fc7a79 100644
--- a/src/test/resources/basics/BBuiltInsTest.mch
+++ b/src/test/resources/basics/BBuiltInsTest.mch
@@ -48,8 +48,8 @@ PROPERTIES
& SIGMA(x).(x : {1,2,3}| x+1) = 9
/* Pi */
-& PI(z).(z : {1,2,3}| z+z) = 12
-& PI(z).(z : {1,2,3} & 1=1| z+z) = 12
+& PI(z).(z : {1,2,3}| z+z) = 48
+& PI(z).(z : {1,2,3} & 1=1| z+z) = 48
& PI(x).(x : {1,2,3}| x) = 6
/* Successor */
diff --git a/src/test/resources/basics/BBuiltInsTest.prob b/src/test/resources/basics/BBuiltInsTest.prob
deleted file mode 100644
index a7413e1..0000000
--- a/src/test/resources/basics/BBuiltInsTest.prob
+++ /dev/null
@@ -1,3 +0,0 @@
-parser_version('2015-09-11 09:12:44.923').
-classical_b('BBuiltInsTest',['/Users/hansen/git/tlc4b/src/test/resources/basics/BBuiltInsTest.mch']).
-machine(abstract_machine(pos(1,1,1,1,79,3),machine(pos(2,1,1,1,1,7)),machine_header(pos(3,1,1,9,1,21),'BBuiltInsTest',[]),[properties(pos(4,1,2,1,77,13),conjunct(pos(5,1,4,1,77,13),conjunct(pos(6,1,4,1,74,12),conjunct(pos(7,1,4,1,71,16),conjunct(pos(8,1,4,1,70,14),conjunct(pos(9,1,4,1,67,16),conjunct(pos(10,1,4,1,66,14),conjunct(pos(11,1,4,1,63,14),conjunct(pos(12,1,4,1,62,13),conjunct(pos(13,1,4,1,61,13),conjunct(pos(14,1,4,1,58,14),conjunct(pos(15,1,4,1,57,13),conjunct(pos(16,1,4,1,56,13),conjunct(pos(17,1,4,1,53,28),conjunct(pos(18,1,4,1,52,37),conjunct(pos(19,1,4,1,51,31),conjunct(pos(20,1,4,1,48,33),conjunct(pos(21,1,4,1,47,40),conjunct(pos(22,1,4,1,46,34),conjunct(pos(23,1,4,1,43,67),conjunct(pos(24,1,4,1,42,34),conjunct(pos(25,1,4,1,39,63),conjunct(pos(26,1,4,1,38,31),conjunct(pos(27,1,4,1,35,33),conjunct(pos(28,1,4,1,34,19),conjunct(pos(29,1,4,1,33,15),conjunct(pos(30,1,4,1,30,36),conjunct(pos(31,1,4,1,29,22),conjunct(pos(32,1,4,1,28,16),conjunct(pos(33,1,4,1,25,33),conjunct(pos(34,1,4,1,24,19),conjunct(pos(35,1,4,1,23,15),conjunct(pos(36,1,4,1,20,18),conjunct(pos(37,1,4,1,19,21),conjunct(pos(38,1,4,1,18,12),conjunct(pos(39,1,4,1,17,14),conjunct(pos(40,1,4,1,16,14),conjunct(pos(41,1,4,1,13,18),conjunct(pos(42,1,4,1,12,20),conjunct(pos(43,1,4,1,11,15),conjunct(pos(44,1,4,1,10,13),conjunct(pos(45,1,4,1,7,18),conjunct(pos(46,1,4,1,6,16),conjunct(pos(47,1,4,1,5,12),subset_strict(pos(48,1,4,1,4,13),set_extension(pos(49,1,4,1,4,3),[integer(pos(50,1,4,2,4,2),1)]),set_extension(pos(51,1,4,9,4,13),[integer(pos(52,1,4,10,4,10),1),integer(pos(53,1,4,12,4,12),2)])),subset_strict(pos(54,1,5,3,5,12),empty_set(pos(55,1,5,3,5,4)),set_extension(pos(56,1,5,10,5,12),[integer(pos(57,1,5,11,5,11),1)]))),negation(pos(58,1,6,3,6,16),subset_strict(pos(59,1,6,7,6,15),empty_set(pos(60,1,6,7,6,8)),empty_set(pos(61,1,6,14,6,15))))),negation(pos(62,1,7,3,7,18),subset_strict(pos(63,1,7,7,7,17),set_extension(pos(64,1,7,7,7,9),[integer(pos(65,1,7,8,7,8),1)]),set_extension(pos(66,1,7,15,7,17),[integer(pos(67,1,7,16,7,16),1)])))),not_subset(pos(68,1,10,3,10,13),set_extension(pos(69,1,10,3,10,5),[integer(pos(70,1,10,4,10,4),1)]),set_extension(pos(71,1,10,11,10,13),[integer(pos(72,1,10,12,10,12),2)]))),not_subset(pos(73,1,11,3,11,15),set_extension(pos(74,1,11,3,11,7),[integer(pos(75,1,11,4,11,4),1),integer(pos(76,1,11,6,11,6),2)]),set_extension(pos(77,1,11,13,11,15),[integer(pos(78,1,11,14,11,14),2)]))),negation(pos(79,1,12,3,12,20),not_subset(pos(80,1,12,7,12,19),set_extension(pos(81,1,12,7,12,9),[integer(pos(82,1,12,8,12,8),1)]),set_extension(pos(83,1,12,15,12,19),[integer(pos(84,1,12,16,12,16),1),integer(pos(85,1,12,18,12,18),2)])))),negation(pos(86,1,13,3,13,18),not_subset(pos(87,1,13,7,13,17),set_extension(pos(88,1,13,7,13,9),[integer(pos(89,1,13,8,13,8),1)]),set_extension(pos(90,1,13,15,13,17),[integer(pos(91,1,13,16,13,16),1)])))),not_subset_strict(pos(92,1,16,3,16,14),set_extension(pos(93,1,16,3,16,5),[integer(pos(94,1,16,4,16,4),1)]),set_extension(pos(95,1,16,12,16,14),[integer(pos(96,1,16,13,16,13),2)]))),not_subset_strict(pos(97,1,17,3,17,14),set_extension(pos(98,1,17,3,17,5),[integer(pos(99,1,17,4,17,4),1)]),set_extension(pos(100,1,17,12,17,14),[integer(pos(101,1,17,13,17,13),1)]))),not_subset_strict(pos(102,1,18,3,18,12),empty_set(pos(103,1,18,3,18,4)),empty_set(pos(104,1,18,11,18,12)))),negation(pos(105,1,19,3,19,21),not_subset_strict(pos(106,1,19,7,19,20),set_extension(pos(107,1,19,7,19,9),[integer(pos(108,1,19,8,19,8),1)]),set_extension(pos(109,1,19,16,19,20),[integer(pos(110,1,19,17,19,17),1),integer(pos(111,1,19,19,19,19),2)])))),negation(pos(112,1,20,3,20,18),not_subset_strict(pos(113,1,20,7,20,17),empty_set(pos(114,1,20,7,20,8)),set_extension(pos(115,1,20,15,20,17),[integer(pos(116,1,20,16,20,16),1)])))),equal(pos(117,1,23,3,23,15),pow1_subset(pos(118,1,23,3,23,10),empty_set(pos(119,1,23,8,23,9))),empty_set(pos(120,1,23,14,23,15)))),equal(pos(121,1,24,3,24,19),pow1_subset(pos(122,1,24,3,24,11),set_extension(pos(123,1,24,8,24,10),[integer(pos(124,1,24,9,24,9),1)])),set_extension(pos(125,1,24,15,24,19),[set_extension(pos(126,1,24,16,24,18),[integer(pos(127,1,24,17,24,17),1)])]))),equal(pos(128,1,25,3,25,33),pow1_subset(pos(129,1,25,3,25,13),set_extension(pos(130,1,25,8,25,12),[integer(pos(131,1,25,9,25,9),1),integer(pos(132,1,25,11,25,11),2)])),set_extension(pos(133,1,25,17,25,33),[set_extension(pos(134,1,25,18,25,20),[integer(pos(135,1,25,19,25,19),1)]),set_extension(pos(136,1,25,23,25,25),[integer(pos(137,1,25,24,25,24),2)]),set_extension(pos(138,1,25,28,25,32),[integer(pos(139,1,25,29,25,29),1),integer(pos(140,1,25,31,25,31),2)])]))),equal(pos(141,1,28,3,28,16),fin_subset(pos(142,1,28,3,28,9),empty_set(pos(143,1,28,7,28,8))),set_extension(pos(144,1,28,13,28,16),[empty_set(pos(145,1,28,14,28,15))]))),equal(pos(146,1,29,3,29,22),fin_subset(pos(147,1,29,3,29,10),set_extension(pos(148,1,29,7,29,9),[integer(pos(149,1,29,8,29,8),1)])),set_extension(pos(150,1,29,14,29,22),[empty_set(pos(151,1,29,15,29,16)),set_extension(pos(152,1,29,19,29,21),[integer(pos(153,1,29,20,29,20),1)])]))),equal(pos(154,1,30,3,30,36),fin_subset(pos(155,1,30,3,30,12),set_extension(pos(156,1,30,7,30,11),[integer(pos(157,1,30,8,30,8),1),integer(pos(158,1,30,10,30,10),2)])),set_extension(pos(159,1,30,16,30,36),[empty_set(pos(160,1,30,17,30,18)),set_extension(pos(161,1,30,21,30,23),[integer(pos(162,1,30,22,30,22),1)]),set_extension(pos(163,1,30,26,30,28),[integer(pos(164,1,30,27,30,27),2)]),set_extension(pos(165,1,30,31,30,35),[integer(pos(166,1,30,32,30,32),1),integer(pos(167,1,30,34,30,34),2)])]))),equal(pos(168,1,33,3,33,15),fin1_subset(pos(169,1,33,3,33,10),empty_set(pos(170,1,33,8,33,9))),empty_set(pos(171,1,33,14,33,15)))),equal(pos(172,1,34,3,34,19),fin1_subset(pos(173,1,34,3,34,11),set_extension(pos(174,1,34,8,34,10),[integer(pos(175,1,34,9,34,9),1)])),set_extension(pos(176,1,34,15,34,19),[set_extension(pos(177,1,34,16,34,18),[integer(pos(178,1,34,17,34,17),1)])]))),equal(pos(179,1,35,3,35,33),fin1_subset(pos(180,1,35,3,35,13),set_extension(pos(181,1,35,8,35,12),[integer(pos(182,1,35,9,35,9),1),integer(pos(183,1,35,11,35,11),2)])),set_extension(pos(184,1,35,17,35,33),[set_extension(pos(185,1,35,18,35,20),[integer(pos(186,1,35,19,35,19),1)]),set_extension(pos(187,1,35,23,35,25),[integer(pos(188,1,35,24,35,24),2)]),set_extension(pos(189,1,35,28,35,32),[integer(pos(190,1,35,29,35,29),1),integer(pos(191,1,35,31,35,31),2)])]))),equal(pos(192,1,38,3,38,31),quantified_intersection(pos(193,1,38,3,38,26),[identifier(pos(194,1,38,9,38,9),z)],member(pos(195,1,38,13,38,20),identifier(pos(196,1,38,13,38,13),z),set_extension(pos(197,1,38,16,38,20),[integer(pos(198,1,38,17,38,17),1),integer(pos(199,1,38,19,38,19),2)])),set_extension(pos(200,1,38,23,38,25),[identifier(pos(201,1,38,24,38,24),z)])),empty_set(pos(202,1,38,30,38,31)))),equal(pos(203,1,39,3,39,63),quantified_intersection(pos(204,1,39,3,39,53),[identifier(pos(205,1,39,9,39,10),x1)],member(pos(206,1,39,14,39,22),identifier(pos(207,1,39,14,39,15),x1),set_extension(pos(208,1,39,18,39,22),[integer(pos(209,1,39,19,39,19),2),integer(pos(210,1,39,21,39,21),4)])),comprehension_set(pos(211,1,39,25,39,52),[identifier(pos(212,1,39,26,39,27),y1)],conjunct(pos(213,1,39,31,39,51),member(pos(214,1,39,31,39,40),identifier(pos(215,1,39,31,39,32),y1),interval(pos(216,1,39,36,39,40),integer(pos(217,1,39,36,39,36),0),integer(pos(218,1,39,39,39,40),10))),less_equal(pos(219,1,39,44,39,51),identifier(pos(220,1,39,44,39,45),y1),identifier(pos(221,1,39,50,39,51),x1))))),set_extension(pos(222,1,39,57,39,63),[integer(pos(223,1,39,58,39,58),0),integer(pos(224,1,39,60,39,60),1),integer(pos(225,1,39,62,39,62),2)]))),equal(pos(226,1,42,3,42,34),quantified_union(pos(227,1,42,3,42,26),[identifier(pos(228,1,42,9,42,9),z)],member(pos(229,1,42,13,42,20),identifier(pos(230,1,42,13,42,13),z),set_extension(pos(231,1,42,16,42,20),[integer(pos(232,1,42,17,42,17),1),integer(pos(233,1,42,19,42,19),2)])),set_extension(pos(234,1,42,23,42,25),[identifier(pos(235,1,42,24,42,24),z)])),set_extension(pos(236,1,42,30,42,34),[integer(pos(237,1,42,31,42,31),1),integer(pos(238,1,42,33,42,33),2)]))),equal(pos(239,1,43,3,43,67),quantified_union(pos(240,1,43,3,43,53),[identifier(pos(241,1,43,9,43,10),x1)],member(pos(242,1,43,14,43,22),identifier(pos(243,1,43,14,43,15),x1),set_extension(pos(244,1,43,18,43,22),[integer(pos(245,1,43,19,43,19),2),integer(pos(246,1,43,21,43,21),4)])),comprehension_set(pos(247,1,43,25,43,52),[identifier(pos(248,1,43,26,43,27),y1)],conjunct(pos(249,1,43,31,43,51),member(pos(250,1,43,31,43,40),identifier(pos(251,1,43,31,43,32),y1),interval(pos(252,1,43,36,43,40),integer(pos(253,1,43,36,43,36),0),integer(pos(254,1,43,39,43,40),10))),less_equal(pos(255,1,43,44,43,51),identifier(pos(256,1,43,44,43,45),y1),identifier(pos(257,1,43,50,43,51),x1))))),set_extension(pos(258,1,43,57,43,67),[integer(pos(259,1,43,58,43,58),0),integer(pos(260,1,43,60,43,60),1),integer(pos(261,1,43,62,43,62),2),integer(pos(262,1,43,64,43,64),3),integer(pos(263,1,43,66,43,66),4)]))),equal(pos(264,1,46,3,46,34),general_sum(pos(265,1,46,3,46,29),[identifier(pos(266,1,46,9,46,9),z)],member(pos(267,1,46,13,46,23),identifier(pos(268,1,46,13,46,13),z),set_extension(pos(269,1,46,17,46,23),[integer(pos(270,1,46,18,46,18),1),integer(pos(271,1,46,20,46,20),2),integer(pos(272,1,46,22,46,22),3)])),add(pos(273,1,46,26,46,28),identifier(pos(274,1,46,26,46,26),z),identifier(pos(275,1,46,28,46,28),z))),integer(pos(276,1,46,33,46,34),12))),equal(pos(277,1,47,3,47,40),general_sum(pos(278,1,47,3,47,35),[identifier(pos(279,1,47,9,47,9),z)],conjunct(pos(280,1,47,13,47,29),member(pos(281,1,47,13,47,23),identifier(pos(282,1,47,13,47,13),z),set_extension(pos(283,1,47,17,47,23),[integer(pos(284,1,47,18,47,18),1),integer(pos(285,1,47,20,47,20),2),integer(pos(286,1,47,22,47,22),3)])),equal(pos(287,1,47,27,47,29),integer(pos(288,1,47,27,47,27),1),integer(pos(289,1,47,29,47,29),1))),add(pos(290,1,47,32,47,34),identifier(pos(291,1,47,32,47,32),z),identifier(pos(292,1,47,34,47,34),z))),integer(pos(293,1,47,39,47,40),12))),equal(pos(294,1,48,3,48,33),general_sum(pos(295,1,48,3,48,29),[identifier(pos(296,1,48,9,48,9),x)],member(pos(297,1,48,13,48,23),identifier(pos(298,1,48,13,48,13),x),set_extension(pos(299,1,48,17,48,23),[integer(pos(300,1,48,18,48,18),1),integer(pos(301,1,48,20,48,20),2),integer(pos(302,1,48,22,48,22),3)])),add(pos(303,1,48,26,48,28),identifier(pos(304,1,48,26,48,26),x),integer(pos(305,1,48,28,48,28),1))),integer(pos(306,1,48,33,48,33),9))),equal(pos(307,1,51,3,51,31),general_product(pos(308,1,51,3,51,26),[identifier(pos(309,1,51,6,51,6),z)],member(pos(310,1,51,10,51,20),identifier(pos(311,1,51,10,51,10),z),set_extension(pos(312,1,51,14,51,20),[integer(pos(313,1,51,15,51,15),1),integer(pos(314,1,51,17,51,17),2),integer(pos(315,1,51,19,51,19),3)])),add(pos(316,1,51,23,51,25),identifier(pos(317,1,51,23,51,23),z),identifier(pos(318,1,51,25,51,25),z))),integer(pos(319,1,51,30,51,31),12))),equal(pos(320,1,52,3,52,37),general_product(pos(321,1,52,3,52,32),[identifier(pos(322,1,52,6,52,6),z)],conjunct(pos(323,1,52,10,52,26),member(pos(324,1,52,10,52,20),identifier(pos(325,1,52,10,52,10),z),set_extension(pos(326,1,52,14,52,20),[integer(pos(327,1,52,15,52,15),1),integer(pos(328,1,52,17,52,17),2),integer(pos(329,1,52,19,52,19),3)])),equal(pos(330,1,52,24,52,26),integer(pos(331,1,52,24,52,24),1),integer(pos(332,1,52,26,52,26),1))),add(pos(333,1,52,29,52,31),identifier(pos(334,1,52,29,52,29),z),identifier(pos(335,1,52,31,52,31),z))),integer(pos(336,1,52,36,52,37),12))),equal(pos(337,1,53,3,53,28),general_product(pos(338,1,53,3,53,24),[identifier(pos(339,1,53,6,53,6),x)],member(pos(340,1,53,10,53,20),identifier(pos(341,1,53,10,53,10),x),set_extension(pos(342,1,53,14,53,20),[integer(pos(343,1,53,15,53,15),1),integer(pos(344,1,53,17,53,17),2),integer(pos(345,1,53,19,53,19),3)])),identifier(pos(346,1,53,23,53,23),x)),integer(pos(347,1,53,28,53,28),6))),equal(pos(348,1,56,3,56,13),function(pos(349,1,56,3,56,9),successor(pos(350,1,56,3,56,6)),[integer(pos(351,1,56,8,56,8),3)]),integer(pos(352,1,56,13,56,13),4))),equal(pos(353,1,57,3,57,13),function(pos(354,1,57,3,57,9),successor(pos(355,1,57,3,57,6)),[integer(pos(356,1,57,8,57,8),0)]),integer(pos(357,1,57,13,57,13),1))),equal(pos(358,1,58,3,58,14),function(pos(359,1,58,3,58,10),successor(pos(360,1,58,3,58,6)),[unary_minus(pos(361,1,58,8,58,9),integer(pos(362,1,58,9,58,9),1))]),integer(pos(363,1,58,14,58,14),0))),equal(pos(364,1,61,3,61,13),function(pos(365,1,61,3,61,9),predecessor(pos(366,1,61,3,61,6)),[integer(pos(367,1,61,8,61,8),3)]),integer(pos(368,1,61,13,61,13),2))),equal(pos(369,1,62,3,62,13),function(pos(370,1,62,3,62,9),predecessor(pos(371,1,62,3,62,6)),[integer(pos(372,1,62,8,62,8),1)]),integer(pos(373,1,62,13,62,13),0))),equal(pos(374,1,63,3,63,14),function(pos(375,1,63,3,63,9),predecessor(pos(376,1,63,3,63,6)),[integer(pos(377,1,63,8,63,8),0)]),unary_minus(pos(378,1,63,13,63,14),integer(pos(379,1,63,14,63,14),1)))),equal(pos(380,1,66,3,66,14),min(pos(381,1,66,3,66,10),set_extension(pos(382,1,66,7,66,9),[integer(pos(383,1,66,8,66,8),1)])),integer(pos(384,1,66,14,66,14),1))),equal(pos(385,1,67,3,67,16),min(pos(386,1,67,3,67,12),set_extension(pos(387,1,67,7,67,11),[integer(pos(388,1,67,8,67,8),1),integer(pos(389,1,67,10,67,10),2)])),integer(pos(390,1,67,16,67,16),1))),equal(pos(391,1,70,3,70,14),max(pos(392,1,70,3,70,10),set_extension(pos(393,1,70,7,70,9),[integer(pos(394,1,70,8,70,8),1)])),integer(pos(395,1,70,14,70,14),1))),equal(pos(396,1,71,3,71,16),max(pos(397,1,71,3,71,12),set_extension(pos(398,1,71,7,71,11),[integer(pos(399,1,71,8,71,8),1),integer(pos(400,1,71,10,71,10),2)])),integer(pos(401,1,71,16,71,16),2))),equal(pos(402,1,74,3,74,12),max_int(pos(403,1,74,3,74,8)),integer(pos(404,1,74,12,74,12),3))),equal(pos(405,1,77,3,77,13),min_int(pos(406,1,77,3,77,8)),unary_minus(pos(407,1,77,12,77,13),integer(pos(408,1,77,13,77,13),1)))))])).
--
GitLab