diff --git a/src/main/java/de/tlc4b/analysis/StandardMadules.java b/src/main/java/de/tlc4b/analysis/StandardMadules.java index 1a9019f8ec220d20fa2b7fd3949ad25ddbaf6413..bcd4aaf60c7d3c823c9c67b354a866b48ca29cd4 100644 --- a/src/main/java/de/tlc4b/analysis/StandardMadules.java +++ b/src/main/java/de/tlc4b/analysis/StandardMadules.java @@ -240,7 +240,7 @@ public final class StandardMadules { * The typing definition (e.g. EXTERNAL_FUNCTION_STRING_SPLIT == ((STRING*STRING) --> (INTEGER<->STRING));) * is not mandatory. * - * The B definitions will be ignored in the {@link TLAPrinter}. + * The B definitions will be ignored in the {@link TLAPrinter}. * * */ @@ -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){ diff --git a/src/main/resources/standardModules/ExternalFunctions.tla b/src/main/resources/standardModules/ExternalFunctions.tla index ec85b011567c1575278ce597a5a9431da3b9a8d0..ca46e6a219bd64b9fb22874740fe037d81e4e384 100644 --- a/src/main/resources/standardModules/ExternalFunctions.tla +++ b/src/main/resources/standardModules/ExternalFunctions.tla @@ -1,6 +1,8 @@ ------------------------------ 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 +============================================================================= \ No newline at end of file diff --git a/src/test/resources/basics/ExternalFunctionsTest.mch b/src/test/resources/basics/ExternalFunctionsTest.mch index 01daf94cdb2a8cc8ed455d86a8d4e7fd2ffd92fc..c4f4af14bebd37ad2e1343446632bb74098ba28f 100644 --- a/src/test/resources/basics/ExternalFunctionsTest.mch +++ b/src/test/resources/basics/ExternalFunctionsTest.mch @@ -1,25 +1,36 @@ MACHINE ExternalFunctionsTest DEFINITIONS -printf(format_string,value) == TRUE=TRUE; -EXTERNAL_PREDICATE_printf(T) == STRING*T; -INT_TO_STRING(S) == "0"; -EXTERNAL_FUNCTION_INT_TO_STRING == (INTEGER --> STRING); -STRING_SPLIT(x,y) == ["foo"]; -EXTERNAL_FUNCTION_STRING_SPLIT == ((STRING*STRING) --> (INTEGER<->STRING)); -EXTERNAL_FUNCTION_REC(A,B) == (STRING * A)-->B; -REC(F,A) == {}; -EXTERNAL_FUNCTION_REC_LET(A) == (STRING * A)-->A; -REC_LET(F,A) == {}; + printf(format_string,value) == TRUE=TRUE; + EXTERNAL_PREDICATE_printf(T) == STRING*T; + INT_TO_STRING(S) == "0"; + EXTERNAL_FUNCTION_INT_TO_STRING == (INTEGER --> STRING); + STRING_SPLIT(x,y) == ["foo"]; + EXTERNAL_FUNCTION_STRING_SPLIT == ((STRING*STRING) --> (INTEGER<->STRING)); + 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))) + 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