Added external function STRING_APPEND

src/main/java/de/tlc4b/analysis/StandardMadules.java

@@ -249,6 +249,7 @@ public final class StandardMadules {
 	public static final String INT_TO_STRING = "INT_TO_STRING";
 	public static final String STRING_SPLIT = "STRING_SPLIT";
 	public static final String SORT_SET = "SORT_SET";
+	public static final String STRING_APPEND = "STRING_APPEND";
 
 	private static final ArrayList<String> ExternalFunctions = new ArrayList<String>();
 	static {
@@ -256,6 +257,7 @@ public final class StandardMadules {
 		ExternalFunctions.add(INT_TO_STRING);
 		ExternalFunctions.add(STRING_SPLIT);
 		ExternalFunctions.add(SORT_SET);
+		ExternalFunctions.add(STRING_APPEND);
 	}
 
 	public static boolean isKeywordInModuleExternalFunctions(String name){

src/main/resources/standardModules/ExternalFunctions.tla

 ------------------------------ MODULE ExternalFunctions ------------------------------
 EXTENDS Sequences, Integers, TLC, FiniteSets
 
+--------------------------------------------------------------------------------------
+                                (* Strings *)
 RECURSIVE SPLIT1(_,_,_,_)
 LOCAL SPLIT1(s,c,start,i) ==
     CASE i = Len(s)+1 -> IF i /= start 
@@ -46,6 +48,8 @@ SORT_SET(s) ==
     ELSE LET max == Max(s)
          IN SORT_SET(s\{max}) \cup {<<Cardinality(s), max>>}
          
+STRING_APPEND(a,b) == a \o b         
+-----------------------------------------------------------------------------
 printf(s,v) == PrintT(s) /\ PrintT(v)
     
 =============================================================================
\ No newline at end of file

src/test/resources/basics/ExternalFunctionsTest.mch

@@ -10,16 +10,27 @@ EXTERNAL_FUNCTION_REC(A,B) == (STRING * A)-->B;
   REC(F,A) == {};
   EXTERNAL_FUNCTION_REC_LET(A) == (STRING * A)-->A;
   REC_LET(F,A) == {};
+
+  STRING_APPEND(x,y) == "str";
+  EXTERNAL_FUNCTION_STRING_APPEND == (STRING*STRING) --> STRING;
+
 ABSTRACT_CONSTANTS SORT_SET
 PROPERTIES
   SORT_SET: POW(INTEGER) <-> POW(INTEGER*INTEGER) &
   SORT_SET = REC_LET("SORT_SET",%x.(x={}|<>) \/ %x.(x:POW1(INTEGER)|REC("SORT_SET",x-{max(x)})<-max(x)))
 ASSERTIONS
   printf("result", 2);
+
   INT_TO_STRING(123) = "123";
   INT_TO_STRING(-123) = "-123";
   STRING_SPLIT("foo bar", " ") = ["foo", "bar"];
   STRING_SPLIT(" foo", " ") = ["foo"];
   STRING_SPLIT("foo||bar", "||") = ["foo", "bar"];
-  SORT_SET({4,2,3,1}) = [1,2,3,4]
+  SORT_SET({4,2,3,1}) = [1,2,3,4];
+  SORT_SET({}) = [];
+  STRING_APPEND("a","bc") = "abc";
+  STRING_APPEND("abc","") = "abc";
+  STRING_APPEND("","abc") = "abc";
+  STRING_APPEND("","") = ""
+
 END