From 84ca02a2c43ef53bb705ffb83da7f6f56ea78582 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Tue, 15 Oct 2019 14:10:32 -0700 Subject: [PATCH] Copy Functions.tla and useful operators from SequenceTheorems.tla from TLAPS modules. Adresses GitHub issue #2 https://github.com/tlaplus/CommunityModules/issues/2 --- modules/Functions.tla | 63 +++++++++++++++++++++++++++ modules/SequencesExt.tla | 85 +++++++++++++++++++++++++++++++++++++ tests/SequencesExtTests.tla | 39 +++++++++++++++++ 3 files changed, 187 insertions(+) create mode 100644 modules/Functions.tla diff --git a/modules/Functions.tla b/modules/Functions.tla new file mode 100644 index 0000000..a96195a --- /dev/null +++ b/modules/Functions.tla @@ -0,0 +1,63 @@ +------------------------------ MODULE Functions ----------------------------- +(***************************************************************************) +(* `^{\large\bf \vspace{12pt} *) +(* Notions about functions including injection, surjection, and bijection.*) +(* Originally contributed by Tom Rodeheffer, MSR. *) +(* \vspace{12pt}}^' *) +(***************************************************************************) + + +(***************************************************************************) +(* Restriction of a function to a set (should be a subset of the domain). *) +(***************************************************************************) +Restrict(f,S) == [ x \in S |-> f[x] ] + +(***************************************************************************) +(* Range of a function. *) +(* Note: The image of a set under function f can be defined as *) +(* Range(Restrict(f,S)). *) +(***************************************************************************) +Range(f) == { f[x] : x \in DOMAIN f } + + +(***************************************************************************) +(* The inverse of a function. *) +(***************************************************************************) +Inverse(f,S,T) == [t \in T |-> CHOOSE s \in S : t \in Range(f) => f[s] = t] + + +(***************************************************************************) +(* A map is an injection iff each element in the domain maps to a distinct *) +(* element in the range. *) +(***************************************************************************) +Injection(S,T) == { M \in [S -> T] : \A a,b \in S : M[a] = M[b] => a = b } + + +(***************************************************************************) +(* A map is a surjection iff for each element in the range there is some *) +(* element in the domain that maps to it. *) +(***************************************************************************) +Surjection(S,T) == { M \in [S -> T] : \A t \in T : \E s \in S : M[s] = t } + + +(***************************************************************************) +(* A map is a bijection iff it is both an injection and a surjection. *) +(***************************************************************************) +Bijection(S,T) == Injection(S,T) \cap Surjection(S,T) + + +(***************************************************************************) +(* An injection, surjection, or bijection exists if the corresponding set *) +(* is nonempty. *) +(***************************************************************************) +ExistsInjection(S,T) == Injection(S,T) # {} +ExistsSurjection(S,T) == Surjection(S,T) # {} +ExistsBijection(S,T) == Bijection(S,T) # {} + + +============================================================================= +\* Modification History +\* Last modified Wed Jul 10 20:32:37 CEST 2013 by merz +\* Last modified Wed Jun 05 12:14:19 CEST 2013 by bhargav +\* Last modified Fri May 03 12:55:35 PDT 2013 by tomr +\* Created Thu Apr 11 10:30:48 PDT 2013 by tomr diff --git a/modules/SequencesExt.tla b/modules/SequencesExt.tla index 0e79e23..6d95b7f 100644 --- a/modules/SequencesExt.tla +++ b/modules/SequencesExt.tla @@ -3,6 +3,7 @@ LOCAL INSTANCE Sequences LOCAL INSTANCE Naturals LOCAL INSTANCE FiniteSets +LOCAL INSTANCE Functions (*************************************************************************) (* Imports the definitions from the modules, but doesn't export them. *) (*************************************************************************) @@ -24,6 +25,8 @@ IsInjective(s) == (* *) (* This definition is overridden by TLC in the Java class SequencesExt. *) (* The operator is overridden by the Java method with the same name. *) + (* *) + (* Also see Functions!Injective operator. *) (*************************************************************************) \A i, j \in DOMAIN s: (s[i] = s[j]) => (i = j) @@ -34,4 +37,86 @@ SetToSeq(S) == (**************************************************************************) CHOOSE f \in [1..Cardinality(S) -> S] : IsInjective(f) +----------------------------------------------------------------------------- + +Reverse(s) == + (**************************************************************************) + (* Reverse the given sequence s: Let l be Len(s) (length of s). *) + (* Equals a sequence s.t. << S[l], S[l-1], ..., S[1]>> *) + (**************************************************************************) + [ i \in 1..Len(s) |-> s[(Len(s) - i) + 1] ] + +----------------------------------------------------------------------------- + +\* The operators below have been extracted from the TLAPS module +\* SequencesTheorems.tla as of 10/14/2019. The original comments have been +\* partially rewritten. + +InsertAt(s, i, e) == + (**************************************************************************) + (* Inserts element e at the position i moving the original element to i+1 *) + (* and so on. In other words, a sequence t s.t.: *) + (* /\ Len(t) = Len(s) + 1 *) + (* /\ t[i] = e *) + (* /\ \A j \in 1..(i - 1): t[j] = s[j] *) + (* /\ \A k \in (i + 1)..Len(s): t[k + 1] = s[k] *) + (**************************************************************************) + SubSeq(s, 1, i-1) \o <> \o SubSeq(s, i, Len(s)) + +ReplaceAt(s, i, e) == + (**************************************************************************) + (* Replaces the element at position i with the element e. *) + (**************************************************************************) + [s EXCEPT ![i] = e] + +RemoveAt(s, i) == + (**************************************************************************) + (* Replaces the element at position i shortening the length of s by one. *) + (**************************************************************************) + SubSeq(s, 1, i-1) \o SubSeq(s, i+1, Len(s)) + +----------------------------------------------------------------------------- + +Front(s) == + (**************************************************************************) + (* The sequence formed by removing its last element. *) + (**************************************************************************) + SubSeq(s, 1, Len(s)-1) + +Last(s) == + (**************************************************************************) + (* The last element of the sequence. *) + (**************************************************************************) + s[Len(s)] + +----------------------------------------------------------------------------- + +IsPrefix(s, t) == + (**************************************************************************) + (* TRUE iff the sequence s is a prefix of the sequence t, s.t. *) + (* \E u \in Seq(Range(t)) : t = s \o u. In other words, there exists *) + (* a suffix u that with s prepended equals t. *) + (**************************************************************************) + DOMAIN s \subseteq DOMAIN t /\ \A i \in DOMAIN s: s[i] = t[i] + +IsStrictPrefix(s,t) == + (**************************************************************************) + (* TRUE iff the sequence s is a prefix of the sequence t and s # t *) + (**************************************************************************) + IsPrefix(s, t) /\ s # t + +IsSuffix(s, t) == + (**************************************************************************) + (* TRUE iff the sequence s is a suffix of the sequence t, s.t. *) + (* \E u \in Seq(Range(t)) : t = u \o s. In other words, there exists a *) + (* prefix that with s appended equals t. *) + (**************************************************************************) + IsPrefix(Reverse(s), Reverse(t)) + +IsStrictSuffix(s, t) == + (**************************************************************************) + (* TRUE iff the sequence s is a suffix of the sequence t and s # t *) + (**************************************************************************) + IsSuffix(s,t) /\ s # t + ============================================================================= diff --git a/tests/SequencesExtTests.tla b/tests/SequencesExtTests.tla index 5acb9b8..63ccbc2 100644 --- a/tests/SequencesExtTests.tla +++ b/tests/SequencesExtTests.tla @@ -26,4 +26,43 @@ ASSUME(SetToSeq({1}) = <<1>>) ASSUME(LET s == {"t","l","a","p","l","u","s"} seq == SetToSeq(s) IN Len(seq) = Cardinality(s) /\ ToSet(seq) = s) + +ASSUME(Reverse(<<>>) = <<>>) +ASSUME(Reverse(<<1,2,3>>) = <<3,2,1>>) +ASSUME(Reverse(<<1,1,2>>) = <<2,1,1>>) +ASSUME(Reverse(<<"a","a","b">>) = <<"b","a","a">>) + +----------------------------------------------------------------------------- + +ASSUME(ReplaceAt(<<1>>, 1, 2) = <<2>>) +ASSUME(ReplaceAt(<<1,1,1>>, 1, 2) = <<2,1,1>>) + +----------------------------------------------------------------------------- + +ASSUME(IsPrefix(<<>>, <<>>)) +ASSUME(IsPrefix(<<>>, <<1>>)) +ASSUME(IsPrefix(<<1>>, <<1,2>>)) +ASSUME(IsPrefix(<<1,2>>, <<1,2>>)) +ASSUME(IsPrefix(<<1,2>>, <<1,2,3>>)) + +ASSUME(~IsPrefix(<<1,2,3>>, <<1,2>>)) +ASSUME(~IsPrefix(<<1,2,2>>, <<1,2,3>>)) +ASSUME(~IsPrefix(<<1,2,3>>, <<1,2,2>>)) +ASSUME(~IsPrefix(<<1>>, <<2>>)) +ASSUME(~IsPrefix(<<2>>, <<1>>)) +ASSUME(~IsPrefix(<<2,1>>, <<1,2>>)) +ASSUME(~IsPrefix(<<1,2>>, <<2,1>>)) + +ASSUME(~IsStrictPrefix(<<>>, <<>>)) +ASSUME(IsStrictPrefix(<<>>, <<1>>)) +ASSUME(IsStrictPrefix(<<1>>, <<1,2>>)) +ASSUME(~IsStrictPrefix(<<1,2>>, <<1,2>>)) +ASSUME(IsStrictPrefix(<<1,2>>, <<1,2,3>>)) + +ASSUME(IsSuffix(<<3>>, <<1,2,3>>)) +ASSUME(IsSuffix(<<2,3>>, <<1,2,3>>)) +ASSUME(~IsSuffix(<<3,2>>, <<1,2,3>>)) +ASSUME(IsSuffix(<<1,2,3>>, <<1,2,3>>)) + +ASSUME(~IsStrictSuffix(<<1,2,3>>, <<1,2,3>>)) =============================================================================