Skip to content

Commit

Permalink
Fall back to TLA+ definition if Java module override of
Browse files Browse the repository at this point in the history 
`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)

[Refactor]

Signed-off-by: Markus Alexander Kuppe <[email protected]>
  • Loading branch information
@lemmy
lemmy committed Dec 19, 2024
1 parent e43de9c commit 55fbc99
Show file tree
Hide file tree
Showing 2 changed files with 54 additions and 4 deletions.
10 changes: 6 additions & 4 deletions modules/tlc2/overrides/SequencesExt.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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.
Expand All @@ -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.
Expand Down
48 changes: 48 additions & 0 deletions tests/SequencesExtTests.tla
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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>>,<<>>), <<>>)
Expand Down

1 comment on commit 55fbc99

@lemmy
Copy link
Member Author

@lemmy lemmy commented on 55fbc99 Dec 19, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Related: #59

Please sign in to comment.