diff --git a/modules/tlc2/overrides/SequencesExt.java b/modules/tlc2/overrides/SequencesExt.java index ef4d810..3ccc28a 100644 --- 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 index e4bd246..a55305e 100644 --- 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>>, <>, 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>>,<<>>), <<>>)