diff --git a/.classpath b/.classpath index c5dd94f..bef7d18 100644 --- a/.classpath +++ b/.classpath @@ -1,11 +1,15 @@ + - + + + + diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml new file mode 100644 index 0000000..330749b --- /dev/null +++ b/.github/workflows/main.yml @@ -0,0 +1,56 @@ +name: CI + +on: [push] + +jobs: + build: + + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v2 + - name: Set up JDK 1.9 + uses: actions/setup-java@v1 + with: + java-version: 9.0.x + - name: Get current date + id: date + run: echo "::set-output name=date::$(date +'%Y%m%d%H%M')" + # Do not download and install TLAPS over and over again. + - uses: actions/cache@v1 + id: cache + with: + path: tlaps/ + key: tlaps1.4.5 + - name: Get TLAPS + if: steps.cache.outputs.cache-hit != 'true' # see actions/cache above + run: wget https://tla.msr-inria.inria.fr/tlaps/dist/current/tlaps-1.4.5-x86_64-linux-gnu-inst.bin + - name: Install TLAPS + if: steps.cache.outputs.cache-hit != 'true' # see actions/cache above + run: | + chmod +x tlaps-1.4.5-x86_64-linux-gnu-inst.bin + ./tlaps-1.4.5-x86_64-linux-gnu-inst.bin -d tlaps + - name: Run TLAPS + run: tlaps/bin/tlapm --cleanfp -I tlaps/ -I modules/ modules/SequencesExtTheorems_proofs.tla + - name: Build with Ant + run: ant -noinput -buildfile build.xml -Dtimestamp=${{steps.date.outputs.date}} + - name: Create Release + id: create_release + uses: actions/create-release@v1 + env: + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + with: + tag_name: ${{steps.date.outputs.date}} + release_name: ${{steps.date.outputs.date}} + draft: false + prerelease: false + - name: Upload Release Asset + id: upload-release-asset + uses: actions/upload-release-asset@v1.0.1 + env: + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + with: + upload_url: ${{ steps.create_release.outputs.upload_url }} + asset_path: dist/CommunityModules-${{steps.date.outputs.date}}.jar + asset_name: CommunityModules-${{steps.date.outputs.date}}.jar + asset_content_type: application/zip diff --git a/.gitignore b/.gitignore index 63169d8..f717858 100644 --- a/.gitignore +++ b/.gitignore @@ -1,4 +1,4 @@ -lib/ +tlc/ dist/ build/ *.toolbox/ diff --git a/CNAME b/CNAME new file mode 100644 index 0000000..bf1afc2 --- /dev/null +++ b/CNAME @@ -0,0 +1 @@ +modules.tlapl.us \ No newline at end of file diff --git a/README.md b/README.md index aad6994..783f70e 100644 --- a/README.md +++ b/README.md @@ -10,11 +10,10 @@ How to use it Just copy & paste the snippet, the operators or the set of modules you are interested in. -Being a community-driven repository we, as the TLA+ developers, do not take any -responsibility for the validity and correctness of the submissions. We will -try to keep this place in order, but we can't guarantee the quality of the -modules here available and therefore do not provide any assistance on eventual -malfunctions. +Alternatively, you can download a [library archive](https://github.com/tlaplus/CommunityModules/releases) and add it to TLC's or the Toolbox's *TLA+ library path*. The advantage of the library archive is that TLC will evaluate an operator faster if the operator comes with a (Java) implementation (see e.g. [SequencesExt.Java](https://github.com/tlaplus/CommunityModules/blob/master/modules/SequencesExt.java)). Run TLC with ```-DTLA-Library=/path/to/lib/archive``` or add the library archive to the Toolbox (```File > Preferences > TLA+ Preferences > TLA+ library path locations```). + +Being a community-driven repository puts the community in charge to check the validity and correctness of submissions. The maintainers of this repository will try to keep this place in order, but we can't guarantee the quality of the +modules and therefore cannot provide any assistance on eventual malfunctions. Contributing ------------ @@ -32,4 +31,4 @@ We take the discretion to approve or reject submissions at our will. Download -------- -[![Build Status](https://dev.azure.com/tlaplus/tlaplus/_apis/build/status/tlaplus.CommunityModules?branchName=master)](https://dev.azure.com/tlaplus/tlaplus/_build/latest?definitionId=4&branchName=master) \ No newline at end of file +![CI](https://github.com/tlaplus/CommunityModules/workflows/CI/badge.svg) diff --git a/azure-pipelines.yml b/azure-pipelines.yml deleted file mode 100644 index 797c71c..0000000 --- a/azure-pipelines.yml +++ /dev/null @@ -1,31 +0,0 @@ -trigger: - - master - -pool: - vmImage: 'Ubuntu-16.04' - -steps: - - task: Ant@1 - inputs: - buildFile: 'build.xml' - javaHomeOption: 'JDKVersion' - jdkVersionOption: '1.8' - jdkArchitectureOption: 'x64' - - - task: GitHubRelease@0 - inputs: - gitHubConnection: CommunityModules - #repositoryName: '$(Build.Repository.Name)' - #action: 'create' # Options: create, edit, delete - #target: '$(Build.SourceVersion)' # Required when action == Create || Action == Edit - tagSource: 'manual' # Required when action == Create# Options: auto, manual - tag: '$(Build.BuildNumber)' # Required when action == Edit || Action == Delete || TagSource == Manual - #title: # Optional - #releaseNotesSource: 'file' # Optional. Options: file, input - #releaseNotesFile: # Optional - #releaseNotes: # Optional - assets: 'dist/CommunityModules-*.jar' # Optional - #assetUploadMode: 'delete' # Optional. Options: delete, replace - #isDraft: false # Optional - #isPreRelease: false # Optional - #addChangeLog: true # Optional diff --git a/build.xml b/build.xml index 446c4f4..f74a91d 100644 --- a/build.xml +++ b/build.xml @@ -1,39 +1,99 @@ - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - + + + + + + - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/lib/jackson-annotations-2.10.2.jar b/lib/jackson-annotations-2.10.2.jar new file mode 100644 index 0000000..cf617f2 Binary files /dev/null and b/lib/jackson-annotations-2.10.2.jar differ diff --git a/lib/jackson-core-2.10.2.jar b/lib/jackson-core-2.10.2.jar new file mode 100644 index 0000000..b9163fc Binary files /dev/null and b/lib/jackson-core-2.10.2.jar differ diff --git a/lib/jackson-databind-2.10.2.jar b/lib/jackson-databind-2.10.2.jar new file mode 100644 index 0000000..4a8c353 Binary files /dev/null and b/lib/jackson-databind-2.10.2.jar differ diff --git a/modules/Bitwise.tla b/modules/Bitwise.tla new file mode 100644 index 0000000..d210e22 --- /dev/null +++ b/modules/Bitwise.tla @@ -0,0 +1,35 @@ +------------------------------- MODULE Bitwise ------------------------------- +LOCAL INSTANCE Integers + +\* https://en.wikipedia.org/wiki/Bitwise_operation#Mathematical_equivalents +RECURSIVE And(_,_,_,_) +LOCAL And(x,y,n,m) == + LET exp == 2^n + IN IF m = 0 + THEN 0 + ELSE exp * ((x \div exp) % 2) * ((y \div exp) % 2) + + And(x,y,n+1,m \div 2) + +x & y == + (***************************************************************************) + (* Bitwise AND of (non-negative) x and y (defined for Nat \cup {0}). *) + (***************************************************************************) + And(x, y, 0, x) \* Infix variant of And(x,y) + + +RECURSIVE shiftR(_,_) +shiftR(n,pos) == + (***************************************************************************) + (* Logical bit-shifting the (non-negative) n by pos positions to the right *) + (* shifting zeros in from the left/MSB (defined for Nat \cup {0}). *) + (***************************************************************************) + IF pos = 0 + THEN n + ELSE LET odd(z) == z % 2 = 1 + m == IF odd(n) THEN (n-1) \div 2 ELSE n \div 2 + IN shiftR(m, pos - 1) + +============================================================================= +\* Modification History +\* Last modified Thu April 25 10:56:12 CEST 2018 by markus +\* Created Mon May 16 15:09:18 CEST 2016 by markus diff --git a/modules/DifferentialEquations.tla b/modules/DifferentialEquations.tla new file mode 100644 index 0000000..b66b54c --- /dev/null +++ b/modules/DifferentialEquations.tla @@ -0,0 +1,36 @@ +----------------------- MODULE DifferentialEquations ------------------------ +LOCAL INSTANCE Reals +LOCAL INSTANCE Sequences +LOCAL PosReal == {r \in Real : r > 0} +LOCAL OpenInterval(a, b) == {s \in Real : a < s /\ s < b} +LOCAL Nbhd(r,e) == OpenInterval(r-e, r+e) +LOCAL IsFirstDeriv(df, f) == + /\ df \in [DOMAIN f -> Real] + /\ \A r \in DOMAIN f : + \A e \in PosReal : + \E d \in PosReal : + \A s \in Nbhd(r,d) \ {r} : + (f[s] - f[r])/(s - r) \in Nbhd(df[r], e) + +LOCAL IsDeriv(n, df, f) == + LET IsD[k \in 0..n, g \in [DOMAIN f -> Real]] == + IF k = 0 + THEN g = f + ELSE \E gg \in [DOMAIN f -> Real] : /\ IsFirstDeriv(g, gg) + /\ IsD[k-1, gg] + IN IsD[n, df] + +Integrate(D, a, b, InitVals) == + LET n == Len(InitVals) + gg == CHOOSE g : + \E e \in PosReal : + /\ g \in [0..n -> [OpenInterval(a-e, b+e) -> Real]] + /\ \A i \in 1..n : /\ IsDeriv(i, g[i], g[0]) + /\ g[i-1][a] = InitVals[i] + /\ \A r \in OpenInterval(a-e, b+e) : + D[ <> \o [i \in 1..(n+1) |-> g[i-1][r]] ] = 0 + IN [i \in 1..n |-> gg[i-1][b]] +============================================================================= + + + 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/Graphs.tla b/modules/Graphs.tla new file mode 100644 index 0000000..88af69c --- /dev/null +++ b/modules/Graphs.tla @@ -0,0 +1,34 @@ +------------------------------- MODULE Graphs ------------------------------- +LOCAL INSTANCE Naturals +LOCAL INSTANCE Sequences + +IsDirectedGraph(G) == + /\ G = [node |-> G.node, edge |-> G.edge] + /\ G.edge \subseteq (G.node \X G.node) + +DirectedSubgraph(G) == + {H \in [node : SUBSET G.node, edge : SUBSET (G.node \X G.node)] : + IsDirectedGraph(H) /\ H.edge \subseteq G.edge} +----------------------------------------------------------------------------- +IsUndirectedGraph(G) == + /\ IsDirectedGraph(G) + /\ \A e \in G.edge : <> \in G.edge + +UndirectedSubgraph(G) == {H \in DirectedSubgraph(G) : IsUndirectedGraph(H)} +----------------------------------------------------------------------------- +Path(G) == {p \in Seq(G.node) : + /\ p # << >> + /\ \A i \in 1..(Len(p)-1) : <> \in G.edge} + +AreConnectedIn(m, n, G) == + \E p \in Path(G) : (p[1] = m) /\ (p[Len(p)] = n) + +IsStronglyConnected(G) == + \A m, n \in G.node : AreConnectedIn(m, n, G) +----------------------------------------------------------------------------- +IsTreeWithRoot(G, r) == + /\ IsDirectedGraph(G) + /\ \A e \in G.edge : /\ e[1] # r + /\ \A f \in G.edge : (e[1] = f[1]) => (e = f) + /\ \A n \in G.node : AreConnectedIn(n, r, G) +============================================================================= diff --git a/modules/IOUtils.tla b/modules/IOUtils.tla new file mode 100644 index 0000000..af7d9b4 --- /dev/null +++ b/modules/IOUtils.tla @@ -0,0 +1,33 @@ +------------------------------ MODULE IOUtils ------------------------------ + +LOCAL INSTANCE TLC +LOCAL INSTANCE Integers + (*************************************************************************) + (* Imports the definitions from the modules, but doesn't export them. *) + (*************************************************************************) + +IOSerialize(val, absoluteFilename, compress) == TRUE + +IODeserialize(absoluteFilename, compressed) == CHOOSE val : TRUE + +---------------------------------------------------------------------------- + +IOExec(command) == + (*******************************************************************************) + (* Spawns the given command as a sub-process of TLC. The sequence of sequence *) + (* of strings `command' signifies the external program file to be invoked and *) + (* its arguments: IOExec(<<"ls", "-lah", "/tmp">>) *) + (* see https://docs.oracle.com/javase/7/docs/api/java/lang/ProcessBuilder.html *) + (*******************************************************************************) + CHOOSE r \in [exitValue : Int, stdout : STRING, stderr : STRING] : TRUE + +IOExecTemplate(commandTemplate, parameters) == + (*************************************************************************) + (* Spawns the given printf-style command as a sub-process of TLC. The *) + (* n-th flag in `commandTemplate' is substituted with the n-th element *) + (* of the sequence `parameters': IOExec("ls %s %s", <<"-lah", "/tmp">>) *) + (* see http://docs.oracle.com/javase/7/docs/api/java/util/Formatter.html *) + (*************************************************************************) + CHOOSE r \in [exitValue : Int, stdout : STRING, stderr : STRING] : TRUE + +============================================================================ diff --git a/modules/Json.tla b/modules/Json.tla index 009e4ba..dfd5edd 100644 --- a/modules/Json.tla +++ b/modules/Json.tla @@ -1,6 +1,7 @@ -------------------------------- MODULE Json -------------------------------- LOCAL INSTANCE Sequences +LOCAL INSTANCE FiniteSets LOCAL INSTANCE TLC (*************************************************************************) (* Imports the definitions from the modules, but doesn't export them. *) @@ -8,29 +9,83 @@ LOCAL INSTANCE TLC ----------------------------------------------------------------------------- -LOCAL ToJsonKeyValue(F, d) == +LOCAL IsSequence(F, D) == TRUE \/ FALSE + +LOCAL ToJsonKeyValue(F, d) == ToString(ToString(d)) \o ":" \o ToString(F[d]) -RECURSIVE ToJson(_,_) -LOCAL ToJson(F, D) == \* LOCAL just a hint for humans. +RECURSIVE ToJsonObjectString(_,_) +LOCAL ToJsonObjectString(F, D) == \* LOCAL just a hint for humans. LET d == CHOOSE d \in D: TRUE IN IF D = DOMAIN F THEN "{" \o ToJsonKeyValue(F, d) \o IF D \ {d} = {} THEN "}" - ELSE ToJson(F, D \ {d}) + ELSE ToJsonObjectString(F, D \ {d}) ELSE ", " \o ToJsonKeyValue(F, d) \o IF D \ {d} = {} - THEN "}" - ELSE ToJson(F, D \ {d}) + THEN "}" + ELSE ToJsonObjectString(F, D \ {d}) + +RECURSIVE ToJsonArrayString(_,_) +LOCAL ToJsonArrayString(F, D) == \* LOCAL just a hint for humans. + LET d == CHOOSE d \in D: TRUE + IN IF D = DOMAIN F + THEN "[" \o ToString(F[d]) \o IF D \ {d} = {} + THEN "]" + ELSE ToJsonArrayString(F, D \ {d}) + ELSE ", " \o ToString(F[d]) \o IF D \ {d} = {} + THEN "]" + ELSE ToJsonArrayString(F, D \ {d}) + +RECURSIVE ToJsonString(_,_) +LOCAL ToJsonString(F, D) == \* LOCAL just a hint for humans. + IF IsFiniteSet(F) \/ IsSequence(F, D) THEN + ToJsonArrayString(F, D) + ELSE + ToJsonObjectString(F, D) + +ToJson(value) == + (*************************************************************************) + (* Converts the given value to a JSON string. Records are converted to *) + (* JSON objects, tuples to JSON arrays, and scalar values as their JSON *) + (* representation. *) + (*************************************************************************) + IF DOMAIN value = {} THEN + "{}" + ELSE + ToJsonString(value, DOMAIN value) -ToJsonObject(F) == +ToJsonArray(value) == (*************************************************************************) - (* This equals a string that is the Json representation of the given *) - (* function F s.t. DOMAIN F \subseteq Nat and Range(F) \subseteq STRING *) - (* with Range(g) == { g[x] : x \in DOMAIN g }. *) + (* Converts the given tuple value to a JSON array. *) (*************************************************************************) - IF DOMAIN F = {} - THEN "{}" - ELSE ToJson(F, DOMAIN F) + IF DOMAIN value = {} THEN + "[]" + ELSE + ToJsonArrayString(value, DOMAIN value) +ToJsonObject(value) == + (*************************************************************************) + (* Converts the given tuple value to a JSON object. *) + (*************************************************************************) + IF DOMAIN value = {} THEN + "{}" + ELSE + ToJsonObjectString(value, DOMAIN value) + +JsonSerialize(absoluteFilename, value) == + (*************************************************************************) + (* Serializes a tuple of values to the given file as newline delimited *) + (* JSON. Records will be serialized as a JSON objects, and tuples as *) + (* arrays. *) + (*************************************************************************) + TRUE + +JsonDeserialize(absoluteFilename) == + (*************************************************************************) + (* Deserializes JSON values from the given file. JSON values must be *) + (* separated by newlines. JSON objects will be deserialized to records, *) + (* and arrays will be deserialized to tuples. *) + (*************************************************************************) + CHOOSE val : TRUE ============================================================================= diff --git a/modules/SVG.tla b/modules/SVG.tla new file mode 100644 index 0000000..c894d8e --- /dev/null +++ b/modules/SVG.tla @@ -0,0 +1,114 @@ +----------------------------- MODULE SVG ----------------------------- +EXTENDS Naturals, Sequences, SequencesExt, Integers, TLC, FiniteSets + +(******************************************************************************) +(* Helper Operators *) +(******************************************************************************) + +LOCAL Merge(r1, r2) == + (**************************************************************************) + (* Merge two records. *) + (* *) + (* If a field appears in both records, then the value from 'r1' is kept. *) + (**************************************************************************) + LET D1 == DOMAIN r1 + D2 == DOMAIN r2 IN + [k \in (D1 \cup D2) |-> IF k \in D1 THEN r1[k] ELSE r2[k]] + +LOCAL SVGElem(_name, _attrs, _children, _innerText) == + (**************************************************************************) + (* SVG element constructor. *) + (* *) + (* An SVG element like: *) + (* *) + (* [name |-> "elem", attrs |-> [k1 |-> "0", k2 |-> "1"], children |-> *) + (* <<>>, innerText |-> ""] *) + (* *) + (* would represent the SVG element '' *) + (**************************************************************************) + [name |-> _name, + attrs |-> _attrs, + children |-> _children, + innerText |-> _innerText ] + +(******************************************************************************) +(* *) +(* Core Graphic Elements. *) +(* *) +(* These primitives are TLA+ wrappers around SVG elements. We base them on *) +(* SVG since it is a widely used format and provides good features for *) +(* representing and laying out vector graphics. Each primitive below should *) +(* roughly correspond to a standard SVG element type. We represent a graphic *) +(* element as a record with the fields 'name', 'attrs', 'children', and *) +(* 'innerText'. 'name' is the name of the SVG element, 'attrs' is a record *) +(* mapping SVG attribute names to values, 'children' is a tuple containing *) +(* any children elements, and 'innerText' is a string that represents any raw *) +(* text that is contained directly inside the SVG element. The 'innerText' *) +(* field is only meaningful for text elements. *) +(* *) +(* All elements accept an 'attrs' argument, which must be a function mapping *) +(* string keys to string values. These key-value pairs describe any *) +(* additional SVG attributes of the element. To pass no attributes, just *) +(* pass attrs=<<>>. *) +(* *) +(******************************************************************************) + +Line(x1, y1, x2, y2, attrs) == + (**************************************************************************) + (* Line element. 'x1', 'y1', 'x2', and 'y2' should be given as integers. *) + (**************************************************************************) + LET svgAttrs == [x1 |-> ToString(x1), + y1 |-> ToString(y1), + x2 |-> ToString(x2), + y2 |-> ToString(y2)] IN + SVGElem("line", Merge(svgAttrs, attrs), <<>>, "") + +Circle(cx, cy, r, attrs) == + (**************************************************************************) + (* Circle element. 'cx', 'cy', and 'r' should be given as integers. *) + (**************************************************************************) + LET svgAttrs == [cx |-> ToString(cx), + cy |-> ToString(cy), + r |-> ToString(r)] IN + SVGElem("circle", Merge(svgAttrs, attrs), <<>>, "") + +Rect(x, y, w, h, attrs) == + (**************************************************************************) + (* Rectangle element. 'x', 'y', 'w', and 'h' should be given as *) + (* integers. *) + (**************************************************************************) + LET svgAttrs == [x |-> ToString(x), + y |-> ToString(y), + width |-> ToString(w), + height |-> ToString(h)] IN + SVGElem("rect", Merge(svgAttrs, attrs), <<>>, "") + +Text(x, y, text, attrs) == + (**************************************************************************) + (* Text element.'x' and 'y' should be given as integers, and 'text' given *) + (* as a string. *) + (**************************************************************************) + LET svgAttrs == [x |-> ToString(x), + y |-> ToString(y)] IN + SVGElem("text", Merge(svgAttrs, attrs), <<>>, text) + +Group(children, attrs) == + (**************************************************************************) + (* Group element. 'children' is a sequence of elements that will be *) + (* contained in this group. *) + (**************************************************************************) + SVGElem("g", attrs, children, "") + +SVGElemToString(elem) == + (**************************************************************************) + (* Convert an SVG element record into its string representation. *) + (* *) + (* This operator is expected to be replaced by a Java module override. *) + (* We do not implement it in pure TLA+ because doing non-trivial string *) + (* manipulation in TLA+ is tedious. Also, the performance of *) + (* implementing this in TLA+ has been demonstrated to be prohibitively *) + (* slow. *) + (**************************************************************************) + TRUE + +============================================================================= \ No newline at end of file diff --git a/modules/SequencesExt.tla b/modules/SequencesExt.tla index d6f864c..1778f01 100644 --- a/modules/SequencesExt.tla +++ b/modules/SequencesExt.tla @@ -2,6 +2,8 @@ LOCAL INSTANCE Sequences LOCAL INSTANCE Naturals +LOCAL INSTANCE FiniteSets +LOCAL INSTANCE Functions (*************************************************************************) (* Imports the definitions from the modules, but doesn't export them. *) (*************************************************************************) @@ -13,7 +15,7 @@ ToSet(s) == (* The image of the given sequence s. Cardinality(ToSet(s)) <= Len(s) *) (* see https://en.wikipedia.org/wiki/Image_(mathematics) *) (*************************************************************************) - { s[i] : i \in 1..Len(s) } + { s[i] : i \in DOMAIN s } IsInjective(s) == (*************************************************************************) @@ -23,7 +25,121 @@ 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 1..Len(s): i # j => s[i] # s[j] + \A i, j \in DOMAIN s: (s[i] = s[j]) => (i = j) + +SetToSeq(S) == + (**************************************************************************) + (* Convert a set to some sequence that contains all the elements of the *) + (* set exactly once, and contains no other elements. *) + (**************************************************************************) + CHOOSE f \in [1..Cardinality(S) -> S] : IsInjective(f) + +----------------------------------------------------------------------------- + +Contains(s, e) == + (**************************************************************************) + (* TRUE iff the element e \in ToSet(s). *) + (**************************************************************************) + \E i \in 1..Len(s) : s[i] = e + +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] ] + +Remove(s, e) == + (************************************************************************) + (* The sequence s with e removed or s iff e \notin Range(s) *) + (************************************************************************) + SelectSeq(s, LAMBDA t: t # e) + +ReplaceAll(s, old, new) == + (*************************************************************************) + (* Equals the sequence s except that all occurrences of element old are *) + (* replaced with the element new. *) + (*************************************************************************) + LET F[i \in 0..Len(s)] == + IF i = 0 THEN << >> + ELSE IF s[i] = old THEN Append(F[i-1], new) + ELSE Append(F[i-1], s[i]) + IN F[Len(s)] + +----------------------------------------------------------------------------- + +\* 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/modules/SequencesExtTheorems.tla b/modules/SequencesExtTheorems.tla new file mode 100644 index 0000000..e1c00f3 --- /dev/null +++ b/modules/SequencesExtTheorems.tla @@ -0,0 +1,27 @@ +------------------------ MODULE SequencesExtTheorems ------------------------ +LOCAL INSTANCE SequencesExt +LOCAL INSTANCE Sequences +LOCAL INSTANCE Functions + +LEMMA AppendTransitivityIsInjective + == ASSUME NEW S, NEW seq \in Seq(S), + IsInjective(seq), + NEW elt \in S, + elt \notin Range(seq) + PROVE IsInjective(Append(seq, elt)) + +LEMMA TailTransitivityIsInjective + == ASSUME NEW S, NEW seq \in Seq(S), + seq # <<>>, + IsInjective(seq) + PROVE IsInjective(Tail(seq)) + +LEMMA HeadTailRange == + ASSUME NEW S, NEW seq \in Seq(S), seq # << >>, IsInjective(seq) + PROVE /\ Head(seq) \in Range(seq) + /\ Range(Tail(seq)) = Range(seq) \ {Head(seq)} + +============================================================================= +\* Modification History +\* Last modified Thu Feb 27 11:38:41 PST 2020 by markus +\* Created Tue Feb 25 20:49:08 PST 2020 by markus diff --git a/modules/SequencesExtTheorems_proofs.tla b/modules/SequencesExtTheorems_proofs.tla new file mode 100644 index 0000000..fa7a700 --- /dev/null +++ b/modules/SequencesExtTheorems_proofs.tla @@ -0,0 +1,71 @@ +--------------------- MODULE SequencesExtTheorems_proofs --------------------- +LOCAL INSTANCE SequencesExt +LOCAL INSTANCE Sequences +LOCAL INSTANCE Naturals +LOCAL INSTANCE Functions +LOCAL INSTANCE TLAPS + +LEMMA AppendTransitivityIsInjective \* With TLAPS 1.4.4+ (3ed0cde) + == ASSUME NEW S, NEW seq \in Seq(S), + IsInjective(seq), + NEW elt \in S, + elt \notin Range(seq) + PROVE IsInjective(Append(seq, elt)) +BY DEF IsInjective, Range + +LEMMA TailTransitivityIsInjective \* With TLAPS 1.4.3 + == ASSUME NEW S, NEW seq \in Seq(S), + seq # <<>>, + IsInjective(seq) + PROVE IsInjective(Tail(seq)) + <1> DEFINE ts == Tail(seq) + <1>1. IsInjective(ts) + <2> SUFFICES ASSUME NEW i \in DOMAIN ts, NEW j \in DOMAIN ts, + ts[i] = ts[j] + PROVE i = j + BY DEF IsInjective + <2>1. ts[i] = seq[i + 1] /\ ts[j] = seq[j + 1] + BY SMT + <2>2. 1..Len(ts) = 1..Len(seq)-1 + BY SMT + <2>3. 1..Len(ts) \subseteq 1..Len(seq) + BY SMT + <2>4. DOMAIN ts = 1..Len(seq)-1 + BY SMT + <2>5. DOMAIN seq = 1..Len(seq) + BY SMT + <2>6. \A r, s \in 1..Len(seq): (seq[r] = seq[s]) => (r = s) + BY Isa, <2>5 DEF IsInjective + <2>7. seq \in [1..Len(seq) -> Range(seq)] + BY Isa, <2>5 DEF Range + <2>8. DOMAIN ts \subseteq DOMAIN seq + BY Isa, <2>2, <2>3, <2>4, <2>7 + <2>9. QED BY <2>1, <2>2, <2>3, <2>5, <2>6, <2>7, <2>8 DEF IsInjective + <1>2. QED BY <1>1 + +LEMMA HeadTailRange == \* With TLAPS 1.4.5 (but not 1.4.3) + ASSUME NEW S, NEW seq \in Seq(S), seq # << >>, IsInjective(seq) + PROVE /\ Head(seq) \in Range(seq) + /\ Range(Tail(seq)) = Range(seq) \ {Head(seq)} +<1>1. Head(seq) \in Range(seq) + BY SMT DEF Range +<1>2. Range(Tail(seq)) \subseteq Range(seq) + BY SMT DEF Range +<1>3. Head(seq) \notin Range(Tail(seq)) + BY SMT DEF Range, IsInjective +<1>4. ASSUME NEW x \in Range(seq), x # Head(seq) + PROVE x \in Range(Tail(seq)) + <2>1. PICK i \in DOMAIN seq : x = seq[i] + BY Isa DEF Range + <2>2. i # 1 + BY SMT, <2>1, <1>4 + <2>3. /\ i-1 \in DOMAIN Tail(seq) + /\ x = Tail(seq)[i-1] + BY SMT, <2>1, <2>2 + <2>. QED BY Isa, <2>3 DEF Range +<1>. QED BY Isa, <1>1, <1>2, <1>3, <1>4 + +============================================================================= +\* Modification History +\* Last modified Thu Feb 27 11:44:49 PST 2020 by markus +\* Created Thu Feb 27 11:27:48 PST 2020 by markus diff --git a/modules/ShiViz.tla b/modules/ShiViz.tla new file mode 100644 index 0000000..909bd02 --- /dev/null +++ b/modules/ShiViz.tla @@ -0,0 +1,54 @@ +u------------------------------- MODULE ShiViz ------------------------------- +EXTENDS Integers, Json, Toolbox, TLC + +----------------------------------------------------------------------------- + +\* Host below is different to the action predicate +\* CHOOSE p \in DOMAIN pc : pc[p] # pc'[p] +\* since Host evaluates for states n and n - 1 +\* whereas the CHOOSE evalutes for states n and n + 1. +\* This difference is most easily observed by looking +\* at off-by-one difference of the initial state. +LOCAL FnHost == + LET host[i \in DOMAIN _TETrace] == + (*************************************************************************) + (* The pc value that has been modified in (the current) state n compared *) + (* to the predecessor state n-1. *) + (*************************************************************************) + IF i = 1 THEN "--" + ELSE IF _TETrace[i-1].pc = _TETrace[i].pc + THEN host[i-1] \* pc variable has not changed. + ELSE CHOOSE p \in DOMAIN _TETrace[i-1].pc : + _TETrace[i-1].pc[p] # _TETrace[i].pc[p] + IN TLCEval(host) + +Host == FnHost[_TEPosition] + +----------------------------------------------------------------------------- + +LOCAL clock(n) == + IF n = 1 THEN [p \in DOMAIN _TETrace[n].pc |-> 0] \* In the init state, all clocks are 0. + ELSE [p \in DOMAIN _TETrace[n].pc |-> IF p = FnHost[n] + THEN 1 + ELSE 0] + +LOCAL sum(F, G) == + [d \in DOMAIN F |-> F[d] + G[d]] + +LOCAL FnClock == + LET vclock[i \in DOMAIN _TETrace] == + IF i = 1 + THEN clock(i) + ELSE sum(TLCEval(vclock[i-1]), clock(i)) + IN TLCEval(vclock) + +Clock == + (*************************************************************************) + (* The pc variable formatted as a Json object as required by ShiViz. *) + (*************************************************************************) + ToJsonObject(FnClock[_TEPosition]) + +============================================================================= +\* Modification History +\* Last modified Tue Sep 25 17:20:37 PDT 2019 by markus +\* Created Tue Aug 27 13:04:16 PDT 2019 by markus diff --git a/modules/TLCExt.tla b/modules/TLCExt.tla new file mode 100644 index 0000000..1f614d9 --- /dev/null +++ b/modules/TLCExt.tla @@ -0,0 +1,58 @@ +------------------------------- MODULE TLCExt ------------------------------- + +LOCAL INSTANCE TLC + (*************************************************************************) + (* Imports the definitions from the modules, but doesn't export them. *) + (*************************************************************************) + +----------------------------------------------------------------------------- + +\* AssertEq(a, b) is logically equivalent to the expression 'a = b'. If a and b are not equal, +\* however, AssertEq(a, b) will print out the values of 'a' and 'b'. If the two values are equal, +\* nothing will be printed. +AssertEq(a, b) == + IF a # b THEN + /\ PrintT("Assertion failed") + /\ PrintT(a) + /\ PrintT(b) + /\ a = b + ELSE a = b + + +AssertError(err, exp) == + LET FailsEval(e) == CHOOSE b \in BOOLEAN : TRUE \* Expression failed to evaluate. + TLCError == CHOOSE s \in STRING : TRUE \* TLC error string. + IN IF FailsEval(exp) THEN Assert(err = TLCError, TLCError) ELSE TRUE + +----------------------------------------------------------------------------- +(* HERE BE DRAGONS! The operators below are experimental! *) + +PickSuccessor(exp) == + (******************************************************************************) + (* When set as an action constraint in the configuration file, interactively *) + (* pick successor states during state exploration, iff the expression exp *) + (* evaluates to FALSE. To always pick successor states manually, use *) + (* PickSuccessor(FALSE). To pick successor states when the current prefix of *) + (* behaviors exceeds 22 states, use PickSuccessor(TLCGet("level") < 23). *) + (******************************************************************************) + IF (exp) + THEN TRUE + ELSE CHOOSE bool \in BOOLEAN : TRUE + +Trace == + (******************************************************************************) + (* The sequence of states (represented as a record whose DOMAIN is the set of *) + (* a spec's variables) from an initial state to the current state. In other *) + (* words, a prefix - of a behavior - ending with the current state. A way to *) + (* think about this operator is to see it as an implicit history variable *) + (* that does not have to be explicitly specified at the level of the spec. *) + (* Note that op is incompatible with TLC!RandomElement and Randomization (see *) + (* tlc2.tool.TLCTrace.getTrace(LongVec)) and will cause TLC to crash. This *) + (* technical limitation could be removed though. *) + (******************************************************************************) + TRUE \* TODO + +TraceFrom(state) == + TRUE \* TODO + +============================================================================= diff --git a/modules/tlc2/overrides/Bitwise.java b/modules/tlc2/overrides/Bitwise.java new file mode 100644 index 0000000..83f746e --- /dev/null +++ b/modules/tlc2/overrides/Bitwise.java @@ -0,0 +1,40 @@ +package tlc2.overrides; +/******************************************************************************* + * Copyright (c) 2019 Microsoft Research. All rights reserved. + * + * The MIT License (MIT) + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies + * of the Software, and to permit persons to whom the Software is furnished to do + * so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN + * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION + * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + * + * Contributors: + * Markus Alexander Kuppe - initial API and implementation + ******************************************************************************/ +import tlc2.value.impl.IntValue; + +public class Bitwise { + + @TLAPlusOperator(identifier = "And", module = "Bitwise", warn = false) + public static IntValue And(IntValue x, IntValue y, IntValue n, IntValue m) { + return IntValue.gen(x.val & y.val); + } + + @TLAPlusOperator(identifier = "shiftR", module = "Bitwise", warn = false) + public static IntValue shiftR(final IntValue n, final IntValue pos) { + return IntValue.gen(n.val >>> pos.val); + } +} diff --git a/modules/tlc2/overrides/IOUtils.java b/modules/tlc2/overrides/IOUtils.java new file mode 100644 index 0000000..a019671 --- /dev/null +++ b/modules/tlc2/overrides/IOUtils.java @@ -0,0 +1,152 @@ +/******************************************************************************* + * Copyright (c) 2020 Microsoft Research. All rights reserved. + * + * The MIT License (MIT) + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies + * of the Software, and to permit persons to whom the Software is furnished to do + * so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN + * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION + * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + * + * Contributors: + * Markus Alexander Kuppe - initial API and implementation + ******************************************************************************/ +package tlc2.overrides; + +import java.io.File; +import java.io.IOException; +import java.util.Arrays; + +import tlc2.output.EC; +import tlc2.tool.EvalException; +import tlc2.value.IValue; +import tlc2.value.ValueInputStream; +import tlc2.value.ValueOutputStream; +import tlc2.value.Values; +import tlc2.value.impl.BoolValue; +import tlc2.value.impl.IntValue; +import tlc2.value.impl.RecordValue; +import tlc2.value.impl.StringValue; +import tlc2.value.impl.TupleValue; +import tlc2.value.impl.Value; +import util.UniqueString; + +public class IOUtils { + + @TLAPlusOperator(identifier = "IODeserialize", module = "IOUtils", warn = false) + public static final IValue deserialize(final StringValue absolutePath, final BoolValue compress) + throws IOException { + final ValueInputStream vis = new ValueInputStream(new File(absolutePath.val.toString()), compress.val); + try { + return vis.read(UniqueString.internTbl.toMap()); + } finally { + vis.close(); + } + } + + @TLAPlusOperator(identifier = "IOSerialize", module = "IOUtils", warn = false) + public static final IValue serialize(final IValue value, final StringValue absolutePath, final BoolValue compress) + throws IOException { + final ValueOutputStream vos = new ValueOutputStream(new File(absolutePath.val.toString()), compress.val); + try { + value.write(vos); + } finally { + vos.close(); + } + return BoolValue.ValTrue; + } + + @TLAPlusOperator(identifier = "IOExec", module = "IOUtils", minLevel = 1, warn = false) + public static Value ioExec(final Value parameter) throws IOException, InterruptedException { + // 1. Check parameters and covert. + if (!(parameter instanceof TupleValue)) { + throw new EvalException(EC.TLC_MODULE_ONE_ARGUMENT_ERROR, + new String[] { "IOExec", "sequence", Values.ppr(parameter.toString()) }); + } + final TupleValue tv = (TupleValue) parameter; + + // 2. Build actual command by converting each parameter element to a string. + // No escaping or quoting is done so the process receives the exact string. + final String[] command = Arrays.asList(tv.getElems()).stream() + .map(IOUtils::convert) + .toArray(size -> new String[size]); + + // 3. Run command-line and receive its output. + final Process process = new ProcessBuilder(command)/*.inheritIO()*/.start(); + + final StringValue stdout = new StringValue(new String(process.getInputStream().readAllBytes())); + final StringValue stderr = new StringValue(new String(process.getErrorStream().readAllBytes())); + final IntValue exitCode = IntValue.gen(process.waitFor()); + + return new RecordValue(EXEC_NAMES, new Value[] {exitCode, stdout, stderr}, false); + } + + @TLAPlusOperator(identifier = "IOExecTemplate", module = "IOUtils", minLevel = 1, warn = false) + public static Value ioExecTemplate(final Value commandTemplate, final Value parameter) throws IOException, InterruptedException { + // 1. Check parameters and covert. + if (!(commandTemplate instanceof StringValue)) { + throw new EvalException(EC.TLC_MODULE_ONE_ARGUMENT_ERROR, + new String[] { "IOExec", "string", Values.ppr(commandTemplate.toString()) }); + } + if (!(parameter instanceof TupleValue)) { + throw new EvalException(EC.TLC_MODULE_ONE_ARGUMENT_ERROR, + new String[] { "IOExec", "sequence", Values.ppr(parameter.toString()) }); + } + final StringValue sv = (StringValue) commandTemplate; + final TupleValue tv = (TupleValue) parameter; + + // 2. Build actual command-line by merging command and parameter. + // XXX does not support multiple %s inside a template part + final String[] command = sv.val.toString().split("\\s+"); + int j = 0; + for (int i = 0; i < command.length; ++i) { + if (command[i].contains("%s")) { + if (j < tv.elems.length) { + command[i] = String.format(command[i], ((StringValue) tv.elems[j++]).val.toString()); + } else { + // Too many %s + // XXX throw proper exception + throw new EvalException(EC.TLC_MODULE_ONE_ARGUMENT_ERROR, + new String[] { "IOExec", "sequence", Values.ppr(parameter.toString()) }); + } + } + } + + // 3. Run command-line and receive its output. + final Process process = new ProcessBuilder(command)/*.inheritIO()*/.start(); + + final StringValue stdout = new StringValue(new String(process.getInputStream().readAllBytes())); + final StringValue stderr = new StringValue(new String(process.getErrorStream().readAllBytes())); + final IntValue exitCode = IntValue.gen(process.waitFor()); + + return new RecordValue(EXEC_NAMES, new Value[] {exitCode, stdout, stderr}, false); + } + + private static String convert(IValue v) { + if (! (v instanceof StringValue)) { + // XXX Proper exception + throw new EvalException(EC.TLC_MODULE_ONE_ARGUMENT_ERROR, + new String[] { "IOExec", "sequence", Values.ppr(v.toString()) }); + } + final StringValue sv = (StringValue) v; + + return sv.val.toString(); + } + + private static final UniqueString EXITVALUE = UniqueString.uniqueStringOf("exitValue"); + private static final UniqueString STDOUT = UniqueString.uniqueStringOf("stdout"); + private static final UniqueString STDERR = UniqueString.uniqueStringOf("stderr"); + private static final UniqueString[] EXEC_NAMES = new UniqueString[] { EXITVALUE, STDOUT, STDERR }; +} diff --git a/modules/tlc2/overrides/Json.java b/modules/tlc2/overrides/Json.java new file mode 100644 index 0000000..16c54eb --- /dev/null +++ b/modules/tlc2/overrides/Json.java @@ -0,0 +1,420 @@ +package tlc2.overrides; +/******************************************************************************* + * Copyright (c) 2019 Microsoft Research. All rights reserved. + * + * The MIT License (MIT) + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies + * of the Software, and to permit persons to whom the Software is furnished to do + * so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN + * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION + * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + * + * Contributors: + * Markus Alexander Kuppe - initial API and implementation + ******************************************************************************/ + +import java.io.BufferedReader; +import java.io.BufferedWriter; +import java.io.File; +import java.io.FileReader; +import java.io.FileWriter; +import java.io.IOException; +import java.util.ArrayList; +import java.util.HashMap; +import java.util.Iterator; +import java.util.List; +import java.util.Map; + +import com.fasterxml.jackson.databind.JsonNode; +import com.fasterxml.jackson.databind.ObjectMapper; +import com.fasterxml.jackson.databind.node.ArrayNode; +import com.fasterxml.jackson.databind.node.BooleanNode; +import com.fasterxml.jackson.databind.node.IntNode; +import com.fasterxml.jackson.databind.node.JsonNodeFactory; +import com.fasterxml.jackson.databind.node.ObjectNode; +import com.fasterxml.jackson.databind.node.TextNode; +import tlc2.value.IValue; +import tlc2.value.impl.BoolValue; +import tlc2.value.impl.FcnLambdaValue; +import tlc2.value.impl.FcnRcdValue; +import tlc2.value.impl.IntValue; +import tlc2.value.impl.IntervalValue; +import tlc2.value.impl.ModelValue; +import tlc2.value.impl.RecordValue; +import tlc2.value.impl.SetEnumValue; +import tlc2.value.impl.SetOfFcnsValue; +import tlc2.value.impl.SetOfRcdsValue; +import tlc2.value.impl.SetOfTuplesValue; +import tlc2.value.impl.StringValue; +import tlc2.value.impl.SubsetValue; +import tlc2.value.impl.TupleValue; +import tlc2.value.impl.Value; +import util.UniqueString; + +/** + * Module overrides for operators to read and write JSON. + */ +public class Json { + + /** + * Encodes the given value as a JSON string. + * + * @param value the value to encode + * @return the JSON string value + */ + @TLAPlusOperator(identifier = "ToJson", module = "Json", warn = false) + public static StringValue toJson(final IValue value) throws IOException { + return new StringValue(getNode(value).toString()); + } + + /** + * Encodes the given value as a JSON array string. + * + * @param value the value to encode + * @return the JSON array string value + */ + @TLAPlusOperator(identifier = "ToJsonArray", module = "Json", warn = false) + public static StringValue toJsonArray(final IValue value) throws IOException { + return new StringValue(getArrayNode(value).toString()); + } + + /** + * Encodes the given value as a JSON object string. + * + * @param value the value to encode + * @return the JSON object string value + */ + @TLAPlusOperator(identifier = "ToJsonObject", module = "Json", warn = false) + public static StringValue toJsonObject(final IValue value) throws IOException { + return new StringValue(getObjectNode(value).toString()); + } + + /** + * Deserializes a tuple of newline delimited JSON values from the given path. + * + * @param path the JSON file path + * @return a tuple of JSON values + */ + @TLAPlusOperator(identifier = "JsonDeserialize", module = "Json", warn = false) + public static IValue deserialize(final StringValue path) throws IOException { + ObjectMapper mapper = new ObjectMapper(); + List values = new ArrayList<>(); + try (BufferedReader reader = new BufferedReader(new FileReader(new File(path.val.toString())))) { + String line = reader.readLine(); + while (line != null) { + JsonNode node = mapper.readTree(line); + values.add(getValue(node)); + line = reader.readLine(); + } + } + return new TupleValue(values.toArray(new Value[0])); + } + + /** + * Serializes a tuple of values to newline delimited JSON. + * + * @param path the file to which to write the values + * @param value the values to write + * @return a boolean value indicating whether the serialization was successful + */ + @TLAPlusOperator(identifier = "JsonSerialize", module = "Json", warn = false) + public static BoolValue serialize(final StringValue path, final TupleValue value) throws IOException { + File file = new File(path.val.toString()); + file.getParentFile().mkdirs(); + try (BufferedWriter writer = new BufferedWriter(new FileWriter(new File(path.val.toString())))) { + for (int i = 0; i < value.elems.length; i++) { + writer.write(getNode(value.elems[i]).toString() + "\n"); + } + } + return BoolValue.ValTrue; + } + + /** + * Recursively converts the given value to a {@code JsonNode}. + * + * @param value the value to convert + * @return the converted {@code JsonNode} + */ + private static JsonNode getNode(IValue value) throws IOException { + if (value instanceof RecordValue) { + return getObjectNode((RecordValue) value); + } else if (value instanceof TupleValue) { + return getArrayNode((TupleValue) value); + } else if (value instanceof StringValue) { + return new TextNode(((StringValue) value).val.toString()); + } else if (value instanceof ModelValue) { + return new TextNode(((ModelValue) value).val.toString()); + } else if (value instanceof IntValue) { + return new IntNode(((IntValue) value).val); + } else if (value instanceof BoolValue) { + return BooleanNode.valueOf(((BoolValue) value).val); + } else if (value instanceof FcnRcdValue) { + return getObjectNode((FcnRcdValue) value); + } else if (value instanceof FcnLambdaValue) { + return getObjectNode((FcnRcdValue) ((FcnLambdaValue) value).toFcnRcd()); + } else if (value instanceof SetEnumValue) { + return getArrayNode((SetEnumValue) value); + } else if (value instanceof SetOfRcdsValue) { + return getArrayNode((SetEnumValue) ((SetOfRcdsValue) value).toSetEnum()); + } else if (value instanceof SetOfTuplesValue) { + return getArrayNode((SetEnumValue) ((SetOfTuplesValue) value).toSetEnum()); + } else if (value instanceof SetOfFcnsValue) { + return getArrayNode((SetEnumValue) ((SetOfFcnsValue) value).toSetEnum()); + } else if (value instanceof SubsetValue) { + return getArrayNode((SetEnumValue) ((SubsetValue) value).toSetEnum()); + } else if (value instanceof IntervalValue) { + return getArrayNode((SetEnumValue) ((IntervalValue) value).toSetEnum()); + } else { + throw new IOException("Cannot convert value: unsupported value type " + value.getClass().getName()); + } + } + + /** + * Returns a boolean indicating whether the given value is a valid sequence. + * + * @param value the value to check + * @return indicates whether the value is a valid sequence + */ + private static boolean isValidSequence(FcnRcdValue value) { + if (value.intv != null) { + return value.intv.low == 1 && value.intv.high == value.domain.length; + } + for (Value domain : value.domain) { + if (!(domain instanceof IntValue)) { + return false; + } + } + value.normalize(); + for (int i = 0; i < value.domain.length; i++) { + if (((IntValue) value.domain[i]).val != (i + 1)) { + return false; + } + } + return true; + } + + /** + * Recursively converts the given value to an {@code ObjectNode}. + * + * @param value the value to convert + * @return the converted {@code JsonNode} + */ + private static JsonNode getObjectNode(IValue value) throws IOException { + if (value instanceof RecordValue) { + return getObjectNode((RecordValue) value); + } else if (value instanceof TupleValue) { + return getObjectNode((TupleValue) value); + } else if (value instanceof FcnRcdValue) { + return getObjectNode((FcnRcdValue) value); + } else if (value instanceof FcnLambdaValue) { + return getObjectNode((FcnRcdValue) ((FcnLambdaValue) value).toFcnRcd()); + } else { + throw new IOException("Cannot convert value: unsupported value type " + value.getClass().getName()); + } + } + + /** + * Converts the given record value to a {@code JsonNode}, recursively converting values. + * + * @param value the value to convert + * @return the converted {@code ObjectNode} + */ + private static JsonNode getObjectNode(FcnRcdValue value) throws IOException { + if (isValidSequence(value)) { + return getArrayNode(value); + } + + Map entries = new HashMap<>(); + for (int i = 0; i < value.domain.length; i++) { + Value domainValue = value.domain[i]; + if (domainValue instanceof StringValue) { + entries.put(((StringValue) domainValue).val.toString(), getNode(value.values[i])); + } else { + entries.put(domainValue.toString(), getNode(value.values[i])); + } + } + return new ObjectNode(new JsonNodeFactory(true), entries); + } + + /** + * Converts the given record value to an {@code ObjectNode}. + * + * @param value the value to convert + * @return the converted {@code ObjectNode} + */ + private static JsonNode getObjectNode(RecordValue value) throws IOException { + Map entries = new HashMap<>(); + for (int i = 0; i < value.names.length; i++) { + entries.put(value.names[i].toString(), getNode(value.values[i])); + } + return new ObjectNode(new JsonNodeFactory(true), entries); + } + + /** + * Converts the given tuple value to an {@code ObjectNode}. + * + * @param value the value to convert + * @return the converted {@code ObjectNode} + */ + private static JsonNode getObjectNode(TupleValue value) throws IOException { + Map entries = new HashMap<>(); + for (int i = 0; i < value.elems.length; i++) { + entries.put(String.valueOf(i), getNode(value.elems[i])); + } + return new ObjectNode(new JsonNodeFactory(true), entries); + } + + /** + * Recursively converts the given value to an {@code ArrayNode}. + * + * @param value the value to convert + * @return the converted {@code JsonNode} + */ + private static JsonNode getArrayNode(IValue value) throws IOException { + if (value instanceof TupleValue) { + return getArrayNode((TupleValue) value); + } else if (value instanceof FcnRcdValue) { + return getArrayNode((FcnRcdValue) value); + } else if (value instanceof FcnLambdaValue) { + return getArrayNode((FcnRcdValue) ((FcnLambdaValue) value).toFcnRcd()); + } else if (value instanceof SetEnumValue) { + return getArrayNode((SetEnumValue) value); + } else if (value instanceof SetOfRcdsValue) { + return getArrayNode((SetEnumValue) ((SetOfRcdsValue) value).toSetEnum()); + } else if (value instanceof SetOfTuplesValue) { + return getArrayNode((SetEnumValue) ((SetOfTuplesValue) value).toSetEnum()); + } else if (value instanceof SetOfFcnsValue) { + return getArrayNode((SetEnumValue) ((SetOfFcnsValue) value).toSetEnum()); + } else if (value instanceof SubsetValue) { + return getArrayNode((SetEnumValue) ((SubsetValue) value).toSetEnum()); + } else if (value instanceof IntervalValue) { + return getArrayNode((SetEnumValue) ((IntervalValue) value).toSetEnum()); + } else { + throw new IOException("Cannot convert value: unsupported value type " + value.getClass().getName()); + } + } + + /** + * Converts the given tuple value to an {@code ArrayNode}. + * + * @param value the value to convert + * @return the converted {@code ArrayNode} + */ + private static JsonNode getArrayNode(TupleValue value) throws IOException { + List elements = new ArrayList<>(value.elems.length); + for (int i = 0; i < value.elems.length; i++) { + elements.add(getNode(value.elems[i])); + } + return new ArrayNode(new JsonNodeFactory(true), elements); + } + + /** + * Converts the given record value to an {@code ArrayNode}. + * + * @param value the value to convert + * @return the converted {@code ArrayNode} + */ + private static JsonNode getArrayNode(FcnRcdValue value) throws IOException { + if (!isValidSequence(value)) { + return getObjectNode(value); + } + + value.normalize(); + List elements = new ArrayList<>(value.values.length); + for (int i = 0; i < value.values.length; i++) { + elements.add(getNode(value.values[i])); + } + return new ArrayNode(new JsonNodeFactory(true), elements); + } + + /** + * Converts the given tuple value to an {@code ArrayNode}. + * + * @param value the value to convert + * @return the converted {@code ArrayNode} + */ + private static JsonNode getArrayNode(SetEnumValue value) throws IOException { + value.normalize(); + Value[] values = value.elems.toArray(); + List elements = new ArrayList<>(values.length); + for (int i = 0; i < values.length; i++) { + elements.add(getNode(values[i])); + } + return new ArrayNode(new JsonNodeFactory(true), elements); + } + + /** + * Recursively converts the given {@code JsonNode} to a TLC value. + * + * @param node the {@code JsonNode} to convert + * @return the converted value + */ + private static Value getValue(JsonNode node) throws IOException { + switch (node.getNodeType()) { + case ARRAY: + return getTupleValue(node); + case OBJECT: + return getRecordValue(node); + case NUMBER: + return IntValue.gen(node.asInt()); + case BOOLEAN: + return new BoolValue(node.asBoolean()); + case STRING: + return new StringValue(node.asText()); + case NULL: + return null; + default: + throw new IOException("Cannot convert value: unsupported JSON type " + node.getNodeType()); + } + } + + /** + * Converts the given {@code JsonNode} to a tuple. + * + * @param node the {@code JsonNode} to convert + * @return the tuple value + */ + private static TupleValue getTupleValue(JsonNode node) throws IOException { + List values = new ArrayList<>(); + for (int i = 0; i < node.size(); i++) { + values.add(getValue(node.get(i))); + } + return new TupleValue(values.toArray(new Value[0])); + } + + /** + * Converts the given {@code JsonNode} to a record. + * + * @param node the {@code JsonNode} to convert + * @return the record value + */ + private static RecordValue getRecordValue(JsonNode node) throws IOException { + List keys = new ArrayList<>(); + List values = new ArrayList<>(); + Iterator> iterator = node.fields(); + while (iterator.hasNext()) { + Map.Entry entry = iterator.next(); + keys.add(UniqueString.uniqueStringOf(entry.getKey())); + values.add(getValue(entry.getValue())); + } + return new RecordValue(keys.toArray(new UniqueString[0]), values.toArray(new Value[0]), false); + } + + + final static void resolves() { + // See TLCOverrides.java + } +} + diff --git a/modules/tlc2/overrides/SVG.java b/modules/tlc2/overrides/SVG.java new file mode 100644 index 0000000..b3fff17 --- /dev/null +++ b/modules/tlc2/overrides/SVG.java @@ -0,0 +1,113 @@ +package tlc2.overrides; +/******************************************************************************* + * Copyright (c) 2019 Microsoft Research. All rights reserved. + * + * The MIT License (MIT) + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies + * of the Software, and to permit persons to whom the Software is furnished to do + * so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN + * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION + * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + * + * Contributors: + * William Schultz - initial API and implementation + ******************************************************************************/ +import util.UniqueString; +import tlc2.value.impl.TupleValue; +import tlc2.value.impl.StringValue; +import tlc2.value.impl.RecordValue; +import tlc2.value.impl.Value; + +public final class SVG { + + private SVG() { + // no-instantiation! + } + + /** + * Converts an SVG element to its string representation. + * + * In TLA+, an SVG object must be represented as a record with the following format: + * + * [ name |-> + * attrs |-> + * children |-> + * innerText |-> ] + */ + @TLAPlusOperator(identifier = "SVGElemToString", module = "SVG", warn = false) + public static Value SVGElemToString(Value elem) throws Exception { + if (!(elem instanceof RecordValue) || elem.toRcd() == null) { + throw new Exception( + "An SVG element must be a record. Value given is of type: " + elem.getClass().getName()); + } + + RecordValue frv = (RecordValue) elem.toRcd(); + + // Get 'name'. + StringValue nameVal = (StringValue) frv.apply(new StringValue("name"), 0); + String name = nameVal.getVal().toString(); + + // Get 'attrs'. We convert it to 'RecordValue' type, which we expect should always be possible. + Value attrsVal = frv.apply(new StringValue("attrs"), 0); + RecordValue attrs = (RecordValue)(attrsVal.toRcd()); + if(attrs == null){ + throw new Exception("Was unable to convert element to a record: " + attrsVal.toString()); + } + String attrStr = ""; + for (UniqueString us : attrs.names) { + attrStr += " "; + attrStr += us.toString(); + attrStr += "="; + String v = ((StringValue) attrs.apply(new StringValue(us), 0)).getVal().toString(); + // Quote all SVG attribute values. Technically, attribute values in HTML + // don't always need to be quoted, but we use quotes so we can handle all + // possible values. We single quote them to play nice with TLC string formatting. + attrStr += "'" + v + "'"; + } + + // Get 'children'. We convert it to a TupleValue, which we expect should + // always be possible. + Value childrenVal = frv.apply(new StringValue("children"), 0); + TupleValue children = (TupleValue)(childrenVal.toTuple()); + if(children == null){ + throw new Exception("Was unable to convert element to a tuple: " + childrenVal.toString()); + } + String childStr = ""; + for (Value child : children.elems) { + StringValue cv = (StringValue)SVGElemToString(child); + childStr += cv.getVal().toString(); + } + + // Get 'innerText'. + // This is raw text placed inside the current SVG element. For example, if + // 'innerText' was "hello", then we would output an SVG element like: + // + // hello + // + // For SVG elements that are not of type , text inside an element is not + // rendered, so this property is only meaningful for elements. It is expected + // to be empty for all other element types, but since it's not rendered, we don't + // explicitly disallow it. + StringValue innerTextVal = (StringValue) frv.apply(new StringValue("innerText"), 0); + String innerText = innerTextVal.getVal().toString(); + + // Produce the SVG element string. + String svg = String.format("<%s%s>", name, attrStr); + svg += innerText; + svg += childStr; + svg += String.format("", name); + return new StringValue(svg); + } +} diff --git a/modules/SequencesExt.java b/modules/tlc2/overrides/SequencesExt.java similarity index 93% rename from modules/SequencesExt.java rename to modules/tlc2/overrides/SequencesExt.java index 2ad2ff9..975c67c 100644 --- a/modules/SequencesExt.java +++ b/modules/tlc2/overrides/SequencesExt.java @@ -1,3 +1,4 @@ +package tlc2.overrides; /******************************************************************************* * Copyright (c) 2019 Microsoft Research. All rights reserved. * @@ -38,6 +39,7 @@ private SequencesExt() { // no-instantiation! } + @TLAPlusOperator(identifier = "IsInjective", module = "SequencesExt", warn = false) public static BoolValue IsInjective(final Value val) { if (val instanceof TupleValue) { return isInjectiveNonDestructive(((TupleValue) val).elems); @@ -45,7 +47,7 @@ public static BoolValue IsInjective(final Value val) { final Value conv = val.toTuple(); if (conv == null) { throw new EvalException(EC.TLC_MODULE_ONE_ARGUMENT_ERROR, - new String[] { "IsASet", "sequence", Values.ppr(val.toString()) }); + new String[] { "IsInjective", "sequence", Values.ppr(val.toString()) }); } return isInjectiveDestructive(((TupleValue) conv).elems); } diff --git a/modules/tlc2/overrides/TLCExt.java b/modules/tlc2/overrides/TLCExt.java new file mode 100644 index 0000000..f77418e --- /dev/null +++ b/modules/tlc2/overrides/TLCExt.java @@ -0,0 +1,179 @@ +/******************************************************************************* + * Copyright (c) 2019 Microsoft Research. All rights reserved. + * + * The MIT License (MIT) + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies + * of the Software, and to permit persons to whom the Software is furnished to do + * so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN + * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION + * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + * + * Contributors: + * Markus Alexander Kuppe - initial API and implementation + ******************************************************************************/ +package tlc2.overrides; + +import java.io.IOException; +import java.util.Scanner; + +import tla2sany.semantic.ExprOrOpArgNode; +import tla2sany.semantic.StringNode; +import tlc2.TLCGlobals; +import tlc2.output.EC; +import tlc2.output.MP; +import tlc2.tool.Action; +import tlc2.tool.ConcurrentTLCTrace; +import tlc2.tool.EvalException; +import tlc2.tool.ModelChecker; +import tlc2.tool.StateVec; +import tlc2.tool.TLCState; +import tlc2.tool.TLCStateInfo; +import tlc2.tool.coverage.CostModel; +import tlc2.tool.impl.Tool; +import tlc2.util.Context; +import tlc2.value.impl.BoolValue; +import tlc2.value.impl.RecordValue; +import tlc2.value.impl.StringValue; +import tlc2.value.impl.TupleValue; +import tlc2.value.impl.Value; +import util.Assert; + +public class TLCExt { + + @Evaluation(definition = "AssertError", module = "TLCExt", warn = false) + public synchronized static Value assertError(final Tool tool, final ExprOrOpArgNode[] args, final Context c, + final TLCState s0, final TLCState s1, final int control, final CostModel cm) { + + // Check expected err is a string. + Assert.check(args[0] instanceof StringNode, "In computing AssertError, a non-string expression (" + args[0] + + ") was used as the err " + "of an AssertError(err, exp)."); + + try { + tool.eval(args[1], c, s0, s1, control, cm); + } catch (EvalException e) { + final StringValue err = (StringValue) tool.eval(args[0], c, s0); + if (err.val.equals(e.getMessage())) { + return BoolValue.ValTrue; + } + } + return BoolValue.ValFalse; + } + + private static final Scanner scanner = new Scanner(System.in); + + // This is likely only useful with a single worker, but let's synchronize + // anyway. + @Evaluation(definition = "PickSuccessor", module = "TLCExt", warn = false) + public synchronized static Value pickSuccessor(final Tool tool, final ExprOrOpArgNode[] args, final Context c, + final TLCState s0, final TLCState s1, final int control, final CostModel cm) { + + // Eval expression and only let user interactively pick successor states when it + // evaluates to FALSE. + final Value guard = tool.eval(args[0], c, s0, s1, control, cm); + if (!(guard instanceof BoolValue)) { + Assert.fail("In evaluating TLCExt!PickSuccessor, a non-boolean expression (" + guard.getKindString() + + ") was used as the condition " + "of an IF.\n" + args[0]); + } + if (((BoolValue) guard).val) { + return BoolValue.ValTrue; + } + + // Find the (first) Action this pair of states belongs to. If more than one + // Action match, we pick the first one. + // TODO: This is clumsy (we regenerate all next-states again) and incorrect if + // two actions generate the same successor states. It's good enough for now + // until the Action instance was passed down the call-stack. + Action action = null; + LOOP: for (Action act : tool.getActions()) { + StateVec nextStates = tool.getNextStates(act, s0); + if (nextStates.contains(s1)) { + action = act; + break LOOP; + } + } + + while (true) { + // TODO Add more commands such as continue/resume to pick every successor, + // randomly pick next N successors, terminate to stop state space exploration, + // ... + MP.printMessage(EC.TLC_MODULE_OVERRIDE_STDOUT, + String.format( + "Extend behavior of length %s with a \"%s\" step [%s]? (Yes/no/explored/states/diff):", + s0.getLevel(), action.getName(), action)); + + final String nextLine = scanner.nextLine(); + if (nextLine.trim().isEmpty() || nextLine.toLowerCase().startsWith("y")) { + return BoolValue.ValTrue; + } else if (nextLine.charAt(0) == 's') { + MP.printMessage(EC.TLC_MODULE_OVERRIDE_STDOUT, + String.format("%s\n~>\n%s", s0.toString().trim(), s1.toString().trim())); + } else if (nextLine.charAt(0) == 'd') { + MP.printMessage(EC.TLC_MODULE_OVERRIDE_STDOUT, s1.toString(s0)); + } else if (nextLine.charAt(0) == 'e') { + try { + ((ModelChecker) TLCGlobals.mainChecker).theFPSet.put(s1.fingerPrint()); + } catch (IOException notExpectedToHappen) { + notExpectedToHappen.printStackTrace(); + } + return BoolValue.ValTrue; + } else if (nextLine.charAt(0) == 'n') { + return BoolValue.ValFalse; + } + } + } + + @Evaluation(definition = "Trace", module = "TLCExt", minLevel = 1, warn = false) + public synchronized static Value getTrace(final Tool tool, final ExprOrOpArgNode[] args, final Context c, + final TLCState s0, final TLCState s1, final int control, final CostModel cm) throws IOException { + final ModelChecker mc = (ModelChecker) TLCGlobals.mainChecker; + final ConcurrentTLCTrace traceFile = mc.trace; + + if (s0.isInitial()) { + return new TupleValue(new Value[] { new RecordValue(s0) }); + } + + return getTrace0(s0, traceFile.getTrace(s0)); + } + + @Evaluation(definition = "TraceFrom", module = "TLCExt", minLevel = 1, warn = false) + public synchronized static Value getTraceFrom(final Tool tool, final ExprOrOpArgNode[] args, final Context c, + final TLCState s0, final TLCState s1, final int control, final CostModel cm) throws IOException { + final ModelChecker mc = (ModelChecker) TLCGlobals.mainChecker; + final ConcurrentTLCTrace traceFile = mc.trace; + + final Value v = tool.eval(args[0], c, s0, s1, control, cm); + if (!(v instanceof RecordValue)) { + Assert.fail("In evaluating TLCExt!TraceFrom, a non-record expression (" + v.getKindString() + + ") was used as the parameter.\n" + args[0]); + } + final TLCState from = ((RecordValue) v).toState(); + Assert.check(from.allAssigned(), EC.GENERAL, + "In evaluating TLCExt!TraceFrom, the given parameter could not be converted into a valid state."); + + if (s0.isInitial() || from.equals(s0)) { + return new TupleValue(new RecordValue(s0)); + } + return getTrace0(s0, traceFile.getTrace(from, s0)); + } + + private static final Value getTrace0(final TLCState s0, final TLCStateInfo[] trace) { + final Value[] values = new Value[trace.length + 1]; + for (int j = 0; j < (trace.length); j++) { + values[j] = new RecordValue(trace[j].state); + } + values[values.length - 1] = new RecordValue(s0); + return new TupleValue(values); + } +} diff --git a/modules/tlc2/overrides/TLCOverrides.java b/modules/tlc2/overrides/TLCOverrides.java new file mode 100644 index 0000000..5f31926 --- /dev/null +++ b/modules/tlc2/overrides/TLCOverrides.java @@ -0,0 +1,45 @@ +/******************************************************************************* + * Copyright (c) 2019 Microsoft Research. All rights reserved. + * + * The MIT License (MIT) + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies + * of the Software, and to permit persons to whom the Software is furnished to do + * so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN + * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION + * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + * + * Contributors: + * Markus Alexander Kuppe - initial API and implementation + ******************************************************************************/ +package tlc2.overrides; + +// tlc2.tool.impl.SpecProcessor's "api" only loads class +// "tlc2.overrides.TLCOverrides". +public class TLCOverrides implements ITLCOverrides { + + @SuppressWarnings("rawtypes") + @Override + public Class[] get() { + try { + Json.resolves(); + return new Class[] { TLCExt.class, IOUtils.class, SVG.class, SequencesExt.class, Json.class, Bitwise.class }; + } catch (NoClassDefFoundError e) { + System.out.println( + "com.fasterxml.jackson dependencies of Json overrides not found, Json module won't work unless " + + "the libraries in the lib/ folder of the CommunityModules have been added to the classpath of TLC."); + } + return new Class[] { TLCExt.class, IOUtils.class, SVG.class, SequencesExt.class, Bitwise.class }; + } +} diff --git a/tests/AllTests.cfg b/tests/AllTests.cfg new file mode 100644 index 0000000..d2f33b0 --- /dev/null +++ b/tests/AllTests.cfg @@ -0,0 +1 @@ +CONSTANT ModelValueConstant = ModelValue diff --git a/tests/AllTests.tla b/tests/AllTests.tla new file mode 100644 index 0000000..e91bb6f --- /dev/null +++ b/tests/AllTests.tla @@ -0,0 +1,13 @@ +------------ MODULE AllTests ------------- + +(***************************************************) +(* Add new tests (the ones with ASSUME statements) *) +(* to the comma-separated list of EXTENDS below. *) +(***************************************************) +EXTENDS SequencesExtTests, + SVGTests, + JsonTests, + BitwiseTests, + IOUtilsTests + +=========================================== \ No newline at end of file diff --git a/tests/BitwiseTests.tla b/tests/BitwiseTests.tla new file mode 100644 index 0000000..f939800 --- /dev/null +++ b/tests/BitwiseTests.tla @@ -0,0 +1,19 @@ +---------------------------- MODULE BitwiseTests ---------------------------- +EXTENDS Bitwise, TLCExt, Naturals + +ZeroToM == 0..99 + +LowBit(n) == IF n % 2 = 1 THEN 1 ELSE 0 + +----------------------------------------------------------------------------- + +ASSUME(\A n \in ZeroToM : AssertEq(n & 0, 0)) +ASSUME(\A n \in ZeroToM : AssertEq(0 & n, 0)) +ASSUME(\A n \in ZeroToM : AssertEq(n & n, n)) +ASSUME(\A n \in ZeroToM : AssertEq(n & 1, LowBit(n))) + +----------------------------------------------------------------------------- + +ASSUME(\A n \in ZeroToM : AssertEq(shiftR(n, 1), (n \div 2))) + +============================================================================= diff --git a/tests/GH005/TLCExtTrace.cfg b/tests/GH005/TLCExtTrace.cfg new file mode 100644 index 0000000..2bf4952 --- /dev/null +++ b/tests/GH005/TLCExtTrace.cfg @@ -0,0 +1,3 @@ +SPECIFICATION Spec +INVARIANT Inv +INVARIANT InvTraceFrom diff --git a/tests/GH005/TLCExtTrace.tla b/tests/GH005/TLCExtTrace.tla new file mode 100644 index 0000000..145fd6b --- /dev/null +++ b/tests/GH005/TLCExtTrace.tla @@ -0,0 +1,18 @@ +---- MODULE TLCExtTrace ---- + +EXTENDS Integers, TLCExt, Sequences + +VARIABLE x + +Spec == x = 1 /\ [][x < 10 /\ x' = x + 1]_x + +\* Assert that Trace is the sequence of states up to the current value of x. +Inv == /\ Len(Trace) = x + /\ \A i \in 1..x : Trace[i].x = i /\ DOMAIN Trace[i] = {"x"} + + +InvTraceFrom == \A i \in 1..x : + /\ Len(TraceFrom([x |-> i])) = x - i + 1 + /\ \A j \in 1..Len(TraceFrom([x |-> i])) : + /\ TraceFrom([x |-> i])[j].x = i + j - 1 +================================== diff --git a/tests/IOUtilsTests.tla b/tests/IOUtilsTests.tla new file mode 100644 index 0000000..9445468 --- /dev/null +++ b/tests/IOUtilsTests.tla @@ -0,0 +1,23 @@ +---------------------------- MODULE IOUtilsTests ---------------------------- +EXTENDS IOUtils, TLC + +\* Spaces and quotes should be passed directly to the program. +ASSUME(LET ret == IOExec(<<"echo", "'foo' ", " \"bar\"">>) IN /\ ret.exitValue = 0 + /\ ret.stdout = "'foo' \"bar\"\n" + /\ ret.stderr = "") +\* Exit values and standard error should be returned properly. +ASSUME(LET ret == IOExec(<<"cat", "/does/not/exist">>) IN /\ ret.exitValue = 1 + /\ ret.stdout = "" + /\ ret.stderr = "cat: /does/not/exist: No such file or directory\n") + +\* Spaces and quotes should be passed directly to the program. +ASSUME(LET ret == IOExecTemplate("echo '%s' \"%s\"", <<" foo", "bar ">>) IN /\ ret.exitValue = 0 + /\ ret.stdout = "' foo' \"bar \"\n" + /\ ret.stderr = "") + +\* Exit values and standard error should be returned properly. +ASSUME(LET ret == IOExecTemplate("cat /does/not/exist", <<>>) IN /\ ret.exitValue = 1 + /\ ret.stdout = "" + /\ ret.stderr = "cat: /does/not/exist: No such file or directory\n") + +============================================================================= diff --git a/tests/JsonTests.tla b/tests/JsonTests.tla index 740bc56..595ebcd 100644 --- a/tests/JsonTests.tla +++ b/tests/JsonTests.tla @@ -1,9 +1,101 @@ ----------------------------- MODULE JsonTests ----------------------------- -EXTENDS Json, TLC +EXTENDS Json, Integers, Sequences, TLC, TLCExt -ASSUME(ToJsonObject(<< >>) = "{}") -ASSUME(ToJsonObject([ i \in {0,1,3} |-> "a" ]) = "{\"0\":\"a\", \"1\":\"a\", \"3\":\"a\"}") -ASSUME(ToJsonObject([ i \in {0,1} |-> "a" ]) = "{\"0\":\"a\", \"1\":\"a\"}") -ASSUME(ToJsonObject([ i \in {1} |-> "a" ]) = "{\"1\":\"a\"}") +CONSTANT ModelValueConstant + +\* Empty values +ASSUME(AssertEq(ToJsonArray({}), "[]")) +ASSUME(AssertEq(ToJsonArray(<<>>), "[]")) + +\* Primitive values +ASSUME(AssertEq(ToJson(FALSE), "false")) +ASSUME(AssertEq(ToJson(1), "1")) +ASSUME(AssertEq(ToJson("a"), "\"a\"")) +ASSUME(AssertEq(ToJson(ModelValueConstant), "\"ModelValue\"")) +ASSUME(AssertEq(ToJson({TRUE, FALSE}), "[false,true]")) +ASSUME(AssertEq(ToJson({1}), "[1]")) +ASSUME(AssertEq(ToJsonArray({TRUE, FALSE}), "[false,true]")) +ASSUME(AssertEq(ToJsonArray({1}), "[1]")) +ASSUME(AssertEq(ToJsonArray({"foo"}), "[\"foo\"]")) +ASSUME(AssertEq(ToJsonObject([a |-> TRUE, b |-> FALSE]), "{\"a\":true,\"b\":false}")) +ASSUME(AssertEq(ToJsonObject([a |-> 1]), "{\"a\":1}")) +ASSUME(AssertEq(ToJsonObject([a |-> "b"]), "{\"a\":\"b\"}")) + +\* Structural values +ASSUME(AssertEq(ToJson({3, 2, 1}), "[1,2,3]")) +ASSUME(AssertEq(ToJson(<<3, 2, 1>>), "[3,2,1]")) +ASSUME(AssertEq(ToJson([x \in {3, 2, 1} |-> 2 * x + 1]), "[3,5,7]")) +ASSUME(AssertEq(ToJson(3 :> "c" @@ 2 :> "b" @@ 1 :> "a"), "[\"a\",\"b\",\"c\"]")) +ASSUME(AssertEq(ToJson([ {2, 1} -> {"a", "b"} ]), "[[\"a\",\"a\"],[\"a\",\"b\"],[\"b\",\"a\"],[\"b\",\"b\"]]")) +ASSUME(AssertEq(ToJson([ {1, 0} -> {"a", "b"} ]), "[{\"0\":\"a\",\"1\":\"a\"},{\"0\":\"a\",\"1\":\"b\"},{\"0\":\"b\",\"1\":\"a\"},{\"0\":\"b\",\"1\":\"b\"}]")) +ASSUME(AssertEq(ToJson([a: {2, 1}, b: {"a", "b"}]), "[{\"a\":1,\"b\":\"a\"},{\"a\":1,\"b\":\"b\"},{\"a\":2,\"b\":\"a\"},{\"a\":2,\"b\":\"b\"}]")) +ASSUME(AssertEq(ToJson({2, 1} \X {"b", "a"}), "[[1,\"a\"],[1,\"b\"],[2,\"a\"],[2,\"b\"]]")) +ASSUME(AssertEq(ToJson(SUBSET {2, 1}), "[[],[1],[2],[1,2]]")) +ASSUME(AssertEq(ToJson(1..3), "[1,2,3]")) +ASSUME(AssertEq(ToJsonArray({3, 2, 1}), "[1,2,3]")) +ASSUME(AssertEq(ToJsonArray(<<3, 2, 1>>), "[3,2,1]")) +ASSUME(AssertEq(ToJsonArray([x \in {3, 2, 1} |-> 2 * x + 1]), "[3,5,7]")) +ASSUME(AssertEq(ToJsonArray(3 :> "c" @@ 2 :> "b" @@ 1 :> "a"), "[\"a\",\"b\",\"c\"]")) +ASSUME(AssertEq(ToJsonArray([ {2, 1} -> {"a", "b"} ]), "[[\"a\",\"a\"],[\"a\",\"b\"],[\"b\",\"a\"],[\"b\",\"b\"]]")) +ASSUME(AssertEq(ToJsonArray([ {1, 0} -> {"a", "b"} ]), "[{\"0\":\"a\",\"1\":\"a\"},{\"0\":\"a\",\"1\":\"b\"},{\"0\":\"b\",\"1\":\"a\"},{\"0\":\"b\",\"1\":\"b\"}]")) +ASSUME(AssertEq(ToJsonArray([a: {2, 1}, b: {"a", "b"}]), "[{\"a\":1,\"b\":\"a\"},{\"a\":1,\"b\":\"b\"},{\"a\":2,\"b\":\"a\"},{\"a\":2,\"b\":\"b\"}]")) +ASSUME(AssertEq(ToJsonArray({2, 1} \X {"b", "a"}), "[[1,\"a\"],[1,\"b\"],[2,\"a\"],[2,\"b\"]]")) +ASSUME(AssertEq(ToJsonArray(SUBSET {2, 1}), "[[],[1],[2],[1,2]]")) +ASSUME(AssertEq(ToJsonArray(1..3), "[1,2,3]")) +ASSUME(AssertEq(ToJsonObject([a |-> FALSE, b |-> 1]), "{\"a\":false,\"b\":1}")) +ASSUME(AssertEq(ToJsonObject("a" :> 1 @@ "b" :> 2 @@ "c" :> 3), "{\"a\":1,\"b\":2,\"c\":3}")) +ASSUME(AssertEq(ToJsonObject(1 :> "b" @@ 0 :> "c"), "{\"0\":\"c\",\"1\":\"b\"}")) + +\* Nested values +ASSUME(AssertEq(ToJsonObject([a |-> {<<1, 2>>}, b |-> [c |-> 3]]), "{\"a\":[[1,2]],\"b\":{\"c\":3}}")) + +\* Serializing and deserializing objects +TestObjects == + LET output == <<[a |-> 1, b |-> "a"], [a |-> 2, b |-> "b"], [a |-> 3, b |-> "c"]>> + IN + /\ JsonSerialize("build/json/test.json", output) + /\ LET input == JsonDeserialize("build/json/test.json") + IN + /\ Len(input) = 3 + /\ input[1].a = 1 + /\ input[1].b = "a" + /\ input[2].a = 2 + /\ input[2].b = "b" + /\ input[3].a = 3 + /\ input[3].b = "c" +ASSUME(TestObjects) + +\* Serializing and deserializing arrays +TestArrays == + LET output == << <<1, 2, 3>>, <<4, 5, 6>>, <<7, 8, 9>> >> + IN + /\ JsonSerialize("build/json/test.json", output) + /\ LET input == JsonDeserialize("build/json/test.json") + IN + /\ Len(input) = 3 + /\ input[1][1] = 1 + /\ input[1][2] = 2 + /\ input[1][3] = 3 + /\ input[2][1] = 4 + /\ input[2][2] = 5 + /\ input[2][3] = 6 + /\ input[3][1] = 7 + /\ input[3][2] = 8 + /\ input[3][3] = 9 +ASSUME(TestArrays) + +\* Serializing and deserializing primitive values +TestPrimitives == + LET output == <<1, 2, 3, 4>> + IN + /\ JsonSerialize("build/json/test.json", output) + /\ LET input == JsonDeserialize("build/json/test.json") + IN + /\ Len(input) = 4 + /\ input[1] = 1 + /\ input[2] = 2 + /\ input[3] = 3 + /\ input[4] = 4 +ASSUME(TestPrimitives) ============================================================================= diff --git a/tests/SVGTests.tla b/tests/SVGTests.tla new file mode 100644 index 0000000..6caa753 --- /dev/null +++ b/tests/SVGTests.tla @@ -0,0 +1,112 @@ +------------------------- MODULE SVGTests ------------------------- +EXTENDS SVG, Sequences, Naturals, TLC, TLCExt + +(******************************************************************************) +(* Test conversion of SVG element records to strings. *) +(* *) +(* We aren't worried about using real SVG element names and attributes here, *) +(* since the logic only deals with converting the TLA+ record representing *) +(* the element into a string. The particular names of elements and *) +(* attributes aren't important. *) +(******************************************************************************) + +ASSUME(LET + elem == [name |-> "test", attrs |-> [a |-> "10"], children |-> <<>>, innerText |-> ""] + expected == "" IN + AssertEq(SVGElemToString(elem), expected)) + +\* Test empty 'attrs'. +ASSUME(LET + elem == [name |-> "test", attrs |-> <<>>, children |-> <<>>, innerText |-> ""] + expected == "" IN + AssertEq(SVGElemToString(elem), expected)) + +\* Specifying the 'attrs' value as a function instead of a record should also be allowed. +ASSUME(LET + elem == [name |-> "test", attrs |-> ("a" :> "10" @@ "b" :> "20"), children |-> <<>>, innerText |-> ""] + expected == "" IN + AssertEq(SVGElemToString(elem), expected)) + +\* Test an element with 1 child. +ASSUME(LET + child == [name |-> "child", attrs |-> [c |-> "10"], children |-> <<>>, innerText |-> ""] + elem == [name |-> "test", attrs |-> [a |-> "10"], children |-> <>, innerText |-> ""] + expected == "" IN + AssertEq(SVGElemToString(elem), expected)) + +\* Specifying the children as a function instead a tuple should also be allowed. +ASSUME(LET + child == [name |-> "child", attrs |-> [c |-> "10"], children |-> <<>>, innerText |-> ""] + elem == [name |-> "test", attrs |-> [a |-> "10"], children |-> (1 :> child), innerText |-> ""] + expected == "" IN + AssertEq(SVGElemToString(elem), expected)) + +\* Test an element with multiple children. +ASSUME(LET + child1 == [name |-> "child1", attrs |-> [c1 |-> "10"], children |-> <<>>, innerText |-> ""] + child2 == [name |-> "child2", attrs |-> [c2 |-> "10"], children |-> <<>>, innerText |-> ""] + elem == [name |-> "test", attrs |-> [a |-> "10"], children |-> <>, innerText |-> ""] + expected == "" IN + AssertEq(SVGElemToString(elem), expected)) + +\* Test an element with 'innerText'. +ASSUME(LET + elem == [name |-> "test", attrs |-> [a |-> "10"], children |-> <<>>, innerText |-> "hello"] + expected == "hello" IN + AssertEq(SVGElemToString(elem), expected)) + +\* Test an element with both children and 'innerText'. +\* It is not really meaningful/useful to have both 'children' and 'innerText', but +\* but we test it anyway since it is allowed. +ASSUME(LET + child == [name |-> "child", attrs |-> [c |-> "10"], children |-> <<>>, innerText |-> ""] + elem == [name |-> "test", attrs |-> [a |-> "10"], children |-> <>, innerText |-> "hello"] + expected == "hello" IN + AssertEq(SVGElemToString(elem), expected)) + +(******************************************************************************) +(* Test production of SVG element objects. *) +(******************************************************************************) + +ASSUME(LET + elem == Line(0, 1, 2, 3, [fill |-> "red"]) + expected == [ name |-> "line", + attrs |-> [x1 |-> "0", y1 |-> "1", x2 |-> "2", y2 |-> "3", fill |-> "red"], + children |-> <<>>, + innerText |-> ""] IN + AssertEq(elem, expected)) + +ASSUME(LET + elem == Circle(5, 5, 10, [fill |-> "red"]) + expected == [ name |-> "circle", + attrs |-> [cx |-> "5", cy |-> "5", r |-> "10", fill |-> "red"], + children |-> <<>>, + innerText |-> ""] IN + AssertEq(elem, expected)) + +ASSUME(LET + elem == Rect(0, 1, 2, 3, [fill |-> "red"]) + expected == [ name |-> "rect", + attrs |-> [x |-> "0", y |-> "1", width |-> "2", height |-> "3", fill |-> "red"], + children |-> <<>>, + innerText |-> ""] IN + AssertEq(elem, expected)) + +ASSUME(LET + elem == Text(0, 1, "hello", [fill |-> "red"]) + expected == [ name |-> "text", + attrs |-> [x |-> "0", y |-> "1", fill |-> "red"], + children |-> <<>>, + innerText |-> "hello"] IN + AssertEq(elem, expected)) + +ASSUME(LET + child == Rect(0, 1, 2, 3, [fill |-> "red"]) + elem == Group(<>, [fill |-> "blue"]) + expected == [ name |-> "g", + attrs |-> [fill |-> "blue"], + children |-> <>, + innerText |-> ""] IN + AssertEq(elem, expected)) + +============================================================================= diff --git a/tests/SequencesExtTests.tla b/tests/SequencesExtTests.tla index ac0564a..c61a27f 100644 --- a/tests/SequencesExtTests.tla +++ b/tests/SequencesExtTests.tla @@ -1,5 +1,14 @@ ------------------------- MODULE SequencesExtTests ------------------------- -EXTENDS Sequences, SequencesExt, Naturals, TLC +EXTENDS Sequences, SequencesExt, Naturals, TLC, TLCExt, FiniteSets + +ASSUME(ToSet(<<>>) = {}) +ASSUME(ToSet(<<1>>) = {1}) +ASSUME(ToSet(<<1,1>>) = {1}) +ASSUME(ToSet(<<1,2,3>>) = {1,2,3}) +ASSUME(ToSet([i \in 1..10 |-> 42]) = {42}) +ASSUME(ToSet([i \in 1..10 |-> i]) = 1..10) +ASSUME(ToSet(Tail([i \in 1..10 |-> i])) = 2..10) +ASSUME(ToSet([i \in 0..9 |-> 42]) = {42}) ASSUME(IsInjective(<<>>)) ASSUME(IsInjective(<<1>>)) @@ -12,4 +21,61 @@ ASSUME(IsInjective([i \in 1..10 |-> {i}])) ASSUME(IsInjective([i \in 1..10 |-> {i}])) ASSUME(~IsInjective([i \in 1..10 |-> {1,2,3}])) +ASSUME(AssertError("The argument of IsInjective should be a sequence, but instead it is:\n{}", IsInjective({}))) +ASSUME(AssertError("The argument of IsInjective should be a sequence, but instead it is:\n[a: 1, b: 2]", IsInjective([a: 1, b: 2]))) +ASSUME(AssertError("The argument of IsInjective should be a sequence, but instead it is:\n(0 :> 0 @@ 1 :> 1 @@ 2 :> 2)", IsInjective([i \in 0..2 |-> i]))) + +ASSUME(SetToSeq({}) = <<>>) +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(Remove(<<>>, "c") = <<>>) +ASSUME(Remove(<<"a","a","b">>, "a") = <<"b">>) +ASSUME(Remove(<<"a","a","a">>, "a") = <<>>) +ASSUME(Remove(<<"a","a","b">>, "c") = <<"a","a","b">>) +ASSUME(Remove(<<{"a", "b"}, {"a","c"}>>, {"c", "a"}) = <<{"a", "b"}>>) + +ASSUME(ReplaceAll(<<>>, 1, 4) = <<>>) +ASSUME(ReplaceAll(<<1,1,2,1,1,3>>, 1, 4) = <<4,4,2,4,4,3>>) + +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>>)) =============================================================================