Fall back to TLA+ definition if Java module override of

`SequencesExt!ReplaceFirstSubSeq` cannot load Apache Commons Lang3 StringUtils class. (Not done for `ReplaceAllSubSeqs` because the TLA+ def fails because it involves `DOMAIN str` that TLC doesn't handle) Related to Github PR #59 #59 [Refactor] Signed-off-by: Markus Alexander Kuppe <[email protected]>
tlaplus · Dec 19, 2024 · e88d04f · e88d04f
1 parent e43de9c
commit e88d04f
Show file tree

Hide file tree

Showing 2 changed files with 54 additions and 4 deletions.
diff --git a/modules/tlc2/overrides/SequencesExt.java b/modules/tlc2/overrides/SequencesExt.java
@@ -28,8 +28,6 @@
 
 import java.util.ArrayList;
 
-import org.apache.commons.lang3.StringUtils;
-
 import tla2sany.semantic.ExprOrOpArgNode;
 import tlc2.output.EC;
 import tlc2.tool.EvalControl;
@@ -357,7 +355,11 @@ public static Value replaceFirstSubSeq(final Tool tool, final ExprOrOpArgNode[]
 
 			if(ss.equals("")) { return new StringValue(sr+st); }
 
-			return new StringValue(StringUtils.replaceOnce(st, ss, sr));
+			try {				
+				return new StringValue(org.apache.commons.lang3.StringUtils.replaceOnce(st, ss, sr));
+			} catch (NoClassDefFoundError e) {
+				return null; // Handle with pure TLA+ definition of operator.
+			}
 		}
 
 		return null; // Non-string functions handled by pure TLA+ definition of operator.
@@ -384,7 +386,7 @@ public static Value replaceAllSubSeq(final Tool tool, final ExprOrOpArgNode[] ar
 				return new StringValue(result.toString());
 			}
 
-			return new StringValue(StringUtils.replace(st, ss, sr));
+			return new StringValue(org.apache.commons.lang3.StringUtils.replace(st, ss, sr));
 		}
 
 		return null; // Non-string functions handled by pure TLA+ definition of operator.

diff --git a/tests/SequencesExtTests.tla b/tests/SequencesExtTests.tla
@@ -291,6 +291,54 @@ ASSUME(ReplaceFirstSubSeq("\r", "%%", "Properly escape the %% char") = "Properly
 ASSUME ReplaceFirstSubSeq("\\\\", "\\", "Properly escape the \\quotes") = "Properly escape the \\\\quotes"
 ASSUME ReplaceFirstSubSeq("replaces", "%pattern%", "This %pattern% the pattern") = "This replaces the pattern"
 
+ReplaceFirstSubSeqPure(r, s, t) ==
+  (**************************************************************************)
+  (* The sequence  t  with its subsequence  s  replaced by the sequence  r  *)
+  (**************************************************************************)
+  IF s \in SubSeqs(t)
+  THEN ReplaceSubSeqAt(IndexFirstSubSeq(s, t), r, s, t)
+  ELSE t
+
+ASSUME ReplaceFirstSubSeqPure(<<>>,<<>>,<<>>) = <<>>
+ASSUME ReplaceFirstSubSeqPure(<<4>>,<<>>,<<>>) = <<4>>
+ASSUME ReplaceFirstSubSeqPure(<<4>>,<<4>>,<<>>) = <<>>
+ASSUME ReplaceFirstSubSeqPure(<<>>,<<>>,<<3,2,3,4>>) = <<3,2,3,4>>
+ASSUME ReplaceFirstSubSeqPure(<<4,4>>,<<3,2,3,4>>,<<3,2,3,4>>) = <<4,4>>
+ASSUME ReplaceFirstSubSeqPure(<<4,4>>,<<>>,<<3,2,3,4>>) = <<4,4,3,2,3,4>>
+
+ASSUME ReplaceFirstSubSeqPure(<<4,4>>,<<4>>,<<3,2,3,4>>) = <<3,2,3,4,4>>
+ASSUME ReplaceFirstSubSeqPure(<<>>,<<4>>,<<3,2,3,4>>) = <<3,2,3>>
+ASSUME ReplaceFirstSubSeqPure(<<>>,<<4>>,<<3,2,3,4,4>>) = <<3,2,3,4>>
+ASSUME ReplaceFirstSubSeqPure(<<4,4>>,<<3>>,<<3,2,3,4>>) = <<4,4,2,3,4>>
+ASSUME ReplaceFirstSubSeqPure(<<4>>, <<1,2>>, <<1,2,1,2>>) = <<4,1,2>>
+ASSUME ReplaceFirstSubSeqPure(<<4,4>>, <<1,2>>, <<1,2,1,2>>) = <<4,4,1,2>>
+ASSUME ReplaceFirstSubSeqPure(<<4,4,4>>, <<1,2>>, <<1,2,1,2>>) = <<4,4,4,1,2>>
+
+ASSUME ReplaceFirstSubSeqPure(<<1,2>>, <<1,2>>, <<1,2,2,1>>) = <<1,2,2,1>>
+ASSUME ReplaceFirstSubSeqPure(<<2,1>>, <<1,2>>, <<1,2,2,1>>) = <<2,1,2,1>>
+
+ASSUME \A seq \in (BoundedSeq(1..5, 5) \ {<<>>}):
+    /\ ReplaceFirstSubSeqPure(<<6>>, <<>>, seq) = <<6>> \o seq
+    /\ ReplaceFirstSubSeqPure(<<6>>, <<Head(seq)>>, seq) = <<6>> \o Tail(seq)
+
+ASSUME ReplaceFirstSubSeqPure("", "", "") = ""
+ASSUME ReplaceFirstSubSeqPure("a", "", "") = "a"
+ASSUME ReplaceFirstSubSeqPure("a", "b", "") = ""
+ASSUME ReplaceFirstSubSeqPure("a", "d", "abc") = "abc"
+ASSUME ReplaceFirstSubSeqPure("ddd", "ab", "abab") = "dddab"
+ASSUME ReplaceFirstSubSeqPure("ddd", "aa", "aaa") = "ddda"
+ASSUME ReplaceFirstSubSeqPure("ddd", "abab", "abab") = "ddd"
+
+ASSUME(ReplaceFirstSubSeqPure("\\", "%%", "Properly escape the %% char") = "Properly escape the \\ char")
+ASSUME(ReplaceFirstSubSeqPure("\"", "%%", "Properly escape the %% char") = "Properly escape the \" char")
+ASSUME(ReplaceFirstSubSeqPure("\n", "%%", "Properly escape the %% char") = "Properly escape the \n char")
+ASSUME(ReplaceFirstSubSeqPure("\t", "%%", "Properly escape the %% char") = "Properly escape the \t char")
+ASSUME(ReplaceFirstSubSeqPure("\f", "%%", "Properly escape the %% char") = "Properly escape the \f char")
+ASSUME(ReplaceFirstSubSeqPure("\r", "%%", "Properly escape the %% char") = "Properly escape the \r char")
+
+ASSUME ReplaceFirstSubSeqPure("\\\\", "\\", "Properly escape the \\quotes") = "Properly escape the \\\\quotes"
+ASSUME ReplaceFirstSubSeqPure("replaces", "%pattern%", "This %pattern% the pattern") = "This replaces the pattern"
+
 -----------------------------------------------------------------------------
 
 ASSUME AssertEq(ReplaceAllSubSeqs(<<4>>,<<1>>,<<>>), <<>>)