From 9e914d6d1186c182ae74faf2a55e816d086e9f8b Mon Sep 17 00:00:00 2001 From: hansen <Dominik.Hansen@hhu.de> Date: Tue, 10 May 2016 16:20:34 +0200 Subject: [PATCH] improved function detection --- src/main/java/de/tlc4b/analysis/Typechecker.java | 3 +++ src/test/java/de/tlc4b/prettyprint/FunctionTest.java | 4 ++-- src/test/java/de/tlc4b/typechecking/FunctionTest.java | 11 +++++++++++ .../java/de/tlc4b/typechecking/RelationsTest.java | 2 +- 4 files changed, 17 insertions(+), 3 deletions(-) diff --git a/src/main/java/de/tlc4b/analysis/Typechecker.java b/src/main/java/de/tlc4b/analysis/Typechecker.java index 1e438a3..3aa9a36 100644 --- a/src/main/java/de/tlc4b/analysis/Typechecker.java +++ b/src/main/java/de/tlc4b/analysis/Typechecker.java @@ -1225,6 +1225,9 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker { } private boolean compareElementsOfList(ArrayList<Node> list) { + if(list.size() == 1){ + return true; + } try { if (list.get(0) instanceof AIntegerExpression) { HashSet<Integer> set = new HashSet<Integer>(); diff --git a/src/test/java/de/tlc4b/prettyprint/FunctionTest.java b/src/test/java/de/tlc4b/prettyprint/FunctionTest.java index 8aaa417..b3cfc02 100644 --- a/src/test/java/de/tlc4b/prettyprint/FunctionTest.java +++ b/src/test/java/de/tlc4b/prettyprint/FunctionTest.java @@ -62,8 +62,8 @@ public class FunctionTest { + "PROPERTIES {(1|->2|->3)} = %a,b.(a = b | a+b)\n" + "END"; String expected = "---- MODULE test ----\n" - + "EXTENDS Integers\n" - + "ASSUME {<<<<1, 2>>,3>>} = {<<<<a, b>>, a + b>> : <<a, b>> \\in { <<a, b>> \\in ((Int) \\times (Int)) : a = b}}\n" + + "EXTENDS Integers, TLC\n" + + "ASSUME (<<1, 2>>:>3) = [<<a, b>> \\in {<<a, b>> \\in ((Int) \\times (Int)) : a = b} |-> a + b] \n" + "===="; compare(expected, machine); } diff --git a/src/test/java/de/tlc4b/typechecking/FunctionTest.java b/src/test/java/de/tlc4b/typechecking/FunctionTest.java index b9a11aa..8a815cc 100644 --- a/src/test/java/de/tlc4b/typechecking/FunctionTest.java +++ b/src/test/java/de/tlc4b/typechecking/FunctionTest.java @@ -22,6 +22,17 @@ public class FunctionTest { assertEquals("FUNC(INTEGER,INTEGER)", t.constants.get("k").toString()); } + @Test + public void testOverride() throws BException { + String machine = "MACHINE test\n" + + "CONSTANTS k,k2,p \n" + + "PROPERTIES p = 1 & k = %x.(x : {1} | 1) & k2 = k <+ {1|->2}\n" + + "END"; + TestTypechecker t = new TestTypechecker(machine); + assertEquals("FUNC(INTEGER,INTEGER)", t.constants.get("k").toString()); + assertEquals("FUNC(INTEGER,INTEGER)", t.constants.get("k2").toString()); + } + @Test public void testSetOperatorOnFunction() throws BException { diff --git a/src/test/java/de/tlc4b/typechecking/RelationsTest.java b/src/test/java/de/tlc4b/typechecking/RelationsTest.java index a2adbd3..8216e68 100644 --- a/src/test/java/de/tlc4b/typechecking/RelationsTest.java +++ b/src/test/java/de/tlc4b/typechecking/RelationsTest.java @@ -85,7 +85,7 @@ public class RelationsTest { + "PROPERTIES k = {1} <| {(k2, TRUE)} \n" + "END"; TestTypechecker t = new TestTypechecker(machine); - assertEquals("POW(INTEGER*BOOL)", t.constants.get("k").toString()); + assertEquals("FUNC(INTEGER,BOOL)", t.constants.get("k").toString()); assertEquals("INTEGER", t.constants.get("k2").toString()); } -- GitLab