{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":50906927,"defaultBranch":"master","name":"tlaplus","ownerLogin":"tlaplus","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2016-02-02T08:48:27.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/2684289?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1718215620.0","currentOid":""},"activityList":{"items":[{"before":"4613109641676389d97b8df209d6cf4d90d31c1c","after":null,"ref":"refs/heads/cal-gh835-bufferedrandomaccessfile","pushedAt":"2024-06-12T18:07:00.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"Calvin-L","name":"Calvin Loncaric","path":"/Calvin-L","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1393639?s=80&v=4"}},{"before":"10033c2fd3528ec9d6a20f552f4e1f4a2dba1394","after":"4613109641676389d97b8df209d6cf4d90d31c1c","ref":"refs/heads/master","pushedAt":"2024-06-12T18:06:32.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Calvin-L","name":"Calvin Loncaric","path":"/Calvin-L","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1393639?s=80&v=4"},"commit":{"message":"Rework `BufferedRandomAccessFile`\n\nThis commit makes major alterations to `BufferedRandomAccessFile` to\nbring it in line with the general `RandomAccessFile` contract:\n\n - Invariant V1 has been strengthened to include a contract for the\n   `length` and `diskPos` fields.\n\n - Invariants V2-V5 have been altered to account for cases where\n   `curr > length`, which the `RandomAccessFile` contract allows.\n\n - Additionally, invariant V5 has been adjusted to clarify that\n   `dirty=true` does not imply that there are unflushed bytes.  The\n   implication is only one-way: if there are unflushed bytes, then\n   `dirty=true`.\n\n - The `hi` and `maxHi` fields have been removed.  These largely\n   duplicate information that can be quickly recomputed, meaning they\n   add additional complexity to the class invariants.  Without those\n   fields, invariant V6 can be removed.\n\n - The `close()` method now closes the underlying file descriptor even\n   if `flush()` throws an exception.\n\nDue to the complexity of this change, I have added a TLA+ specification\nfor `BufferedRandomAccessFile` to enable model checking of its design.\n\nTo ensure that the code is correct, this commit also adds a substantial\namount of test infrastructure:\n\n - Several new regression tests have been added.  These are a little\n   cryptic because they were randomly generated, but they do reflect\n   true behaviors of the `RandomAccessFile` contract.\n\n - A fuzz test has been added.  This test ensures that many sequences\n   of random operations behave correctly.  It also minimizes failures\n   so they can be easily converted to regression tests.\n\nThis commit also makes some whitespace and formatting adjustments.\n\nFixes #835.  I have verified that the tests now pass under Java 21.\n\nSigned-off-by: Calvin Loncaric <calvin.loncaric@oracle.com>","shortMessageHtmlLink":"Rework <code>BufferedRandomAccessFile</code>"}},{"before":"aa11c4240b11adeee0c8e962bf3fdd76eaa7bacc","after":"4613109641676389d97b8df209d6cf4d90d31c1c","ref":"refs/heads/cal-gh835-bufferedrandomaccessfile","pushedAt":"2024-06-12T17:50:27.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Calvin-L","name":"Calvin Loncaric","path":"/Calvin-L","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1393639?s=80&v=4"},"commit":{"message":"Rework `BufferedRandomAccessFile`\n\nThis commit makes major alterations to `BufferedRandomAccessFile` to\nbring it in line with the general `RandomAccessFile` contract:\n\n - Invariant V1 has been strengthened to include a contract for the\n   `length` and `diskPos` fields.\n\n - Invariants V2-V5 have been altered to account for cases where\n   `curr > length`, which the `RandomAccessFile` contract allows.\n\n - Additionally, invariant V5 has been adjusted to clarify that\n   `dirty=true` does not imply that there are unflushed bytes.  The\n   implication is only one-way: if there are unflushed bytes, then\n   `dirty=true`.\n\n - The `hi` and `maxHi` fields have been removed.  These largely\n   duplicate information that can be quickly recomputed, meaning they\n   add additional complexity to the class invariants.  Without those\n   fields, invariant V6 can be removed.\n\n - The `close()` method now closes the underlying file descriptor even\n   if `flush()` throws an exception.\n\nDue to the complexity of this change, I have added a TLA+ specification\nfor `BufferedRandomAccessFile` to enable model checking of its design.\n\nTo ensure that the code is correct, this commit also adds a substantial\namount of test infrastructure:\n\n - Several new regression tests have been added.  These are a little\n   cryptic because they were randomly generated, but they do reflect\n   true behaviors of the `RandomAccessFile` contract.\n\n - A fuzz test has been added.  This test ensures that many sequences\n   of random operations behave correctly.  It also minimizes failures\n   so they can be easily converted to regression tests.\n\nThis commit also makes some whitespace and formatting adjustments.\n\nFixes #835.  I have verified that the tests now pass under Java 21.\n\nSigned-off-by: Calvin Loncaric <calvin.loncaric@oracle.com>","shortMessageHtmlLink":"Rework <code>BufferedRandomAccessFile</code>"}},{"before":"345ffd2fae856e2b577fe43f92ddf283db3e0840","after":"aa11c4240b11adeee0c8e962bf3fdd76eaa7bacc","ref":"refs/heads/cal-gh835-bufferedrandomaccessfile","pushedAt":"2024-06-12T17:26:57.000Z","pushType":"push","commitsCount":6,"pusher":{"login":"Calvin-L","name":"Calvin Loncaric","path":"/Calvin-L","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1393639?s=80&v=4"},"commit":{"message":"Factor out `restoreInvariantsAfterIncreasingCurr()`\n\nSigned-off-by: Calvin Loncaric <calvin.loncaric@oracle.com>","shortMessageHtmlLink":"Factor out <code>restoreInvariantsAfterIncreasingCurr()</code>"}},{"before":"225f50ffb4cbfe498e3a1de19705fa92e81f2062","after":"10033c2fd3528ec9d6a20f552f4e1f4a2dba1394","ref":"refs/heads/master","pushedAt":"2024-06-11T00:57:36.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"},"commit":{"message":"Expand CONTRIBUTING.md (#936)\n\nSigned-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>","shortMessageHtmlLink":"Expand CONTRIBUTING.md (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2341245092\" data-permission-text=\"Title is private\" data-url=\"https://github.com/tlaplus/tlaplus/issues/936\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/tlaplus/tlaplus/pull/936/hovercard\" href=\"https://github.com/tlaplus/tlaplus/pull/936\">#936</a>)"}},{"before":"35ed7b685ccb7e8dc869c0ad78834901db912c3e","after":null,"ref":"refs/heads/mku-easymock2.4.0","pushedAt":"2024-06-10T22:33:31.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"}},{"before":"2c4b67b7c20c52e34ada410a9f74a40da0e280bf","after":"225f50ffb4cbfe498e3a1de19705fa92e81f2062","ref":"refs/heads/master","pushedAt":"2024-06-10T22:33:25.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"},"commit":{"message":"Fix compiler error introduced by recent refactoring that assumes a newer\nversion of Easymock than what TLAToolbox.target defines.\n\n[Build][TLC][Test]\n\nSigned-off-by: Markus Alexander Kuppe <github.com@lemmster.de>","shortMessageHtmlLink":"Fix compiler error introduced by recent refactoring that assumes a newer"}},{"before":"a3c593ca4dc535defd908f6130e4d66f93182829","after":"2c4b67b7c20c52e34ada410a9f74a40da0e280bf","ref":"refs/heads/master","pushedAt":"2024-06-10T22:23:48.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"},"commit":{"message":"Remove e4 tools from the Eclipse development environment setup.\n\nDevelopment on the Toolbox has essentially stopped, making the e4 tools\nunnecessary.\n\n[Refactor][IDE]\n\nSigned-off-by: Markus Alexander Kuppe <github.com@lemmster.de>","shortMessageHtmlLink":"Remove e4 tools from the Eclipse development environment setup."}},{"before":"d1215cfac07d956257607b928ef0c8a8155c4b2f","after":null,"ref":"refs/heads/mku-RemoveAOP","pushedAt":"2024-06-10T22:15:59.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"}},{"before":"2bfa142d595e54487b74a793cfb5578f091f2b82","after":"a3c593ca4dc535defd908f6130e4d66f93182829","ref":"refs/heads/master","pushedAt":"2024-06-10T22:15:55.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"},"commit":{"message":"Remove everything AspectJ from the TLA Tools+ and Toolbox projects. (#940)\n\nRemove AspectJ dependencies from the TLA Tools+ and the Toolbox projects.\r\n\r\nThese aspects never provided user-visible functionality. Instead, they\r\noffered functionality that was only used during development, and have\r\nnot been utilized for many years.\r\n\r\n[Refactor][TLC]\r\n\r\nSigned-off-by: Markus Alexander Kuppe <github.com@lemmster.de>","shortMessageHtmlLink":"Remove everything AspectJ from the TLA Tools+ and Toolbox projects. (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2344804864\" data-permission-text=\"Title is private\" data-url=\"https://github.com/tlaplus/tlaplus/issues/940\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/tlaplus/tlaplus/pull/940/hovercard\" href=\"https://github.com/tlaplus/tlaplus/pull/940\">#…</a>"}},{"before":"071c0e462c2da4395bc35fbe63ff248e1e8fe9fe","after":"d1215cfac07d956257607b928ef0c8a8155c4b2f","ref":"refs/heads/mku-RemoveAOP","pushedAt":"2024-06-10T21:07:50.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"},"commit":{"message":"Remove AspectJ dependencies from the Toolbox projects.\n\nThese aspects never provided user-visible functionality. Instead, they\noffered functionality that was only used during development.\n\n[Refactor][TLC]\n\nSigned-off-by: Markus Alexander Kuppe <github.com@lemmster.de>","shortMessageHtmlLink":"Remove AspectJ dependencies from the Toolbox projects."}},{"before":"5d9c591d046f766f41e03f2fa845d9ff80d5ac49","after":"071c0e462c2da4395bc35fbe63ff248e1e8fe9fe","ref":"refs/heads/mku-RemoveAOP","pushedAt":"2024-06-10T21:03:25.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"},"commit":{"message":"Remove AspectJ dependencies from the Toolbox projects.\n\nThese aspects never provided user-visible functionality. Instead, they\noffered functionality that was only used during development.\n\n[Refactor][TLC]\n\nSigned-off-by: Markus Alexander Kuppe <github.com@lemmster.de>","shortMessageHtmlLink":"Remove AspectJ dependencies from the Toolbox projects."}},{"before":null,"after":"5d9c591d046f766f41e03f2fa845d9ff80d5ac49","ref":"refs/heads/mku-RemoveAOP","pushedAt":"2024-06-10T20:51:17.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"},"commit":{"message":"Remove AspectJ dependencies from the TLA Tools+ project.\n\nThese aspects never provided user-visible functionality. Instead, they\noffered functionality that was only used during development, and have\nnot been utilized for many years.\n\n[Refactor][TLC]\n\nSigned-off-by: Markus Alexander Kuppe <github.com@lemmster.de>","shortMessageHtmlLink":"Remove AspectJ dependencies from the TLA Tools+ project."}},{"before":"99e6322cd152c44dec03677c51f45728a4041539","after":"345ffd2fae856e2b577fe43f92ddf283db3e0840","ref":"refs/heads/cal-gh835-bufferedrandomaccessfile","pushedAt":"2024-06-10T20:31:55.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"Calvin-L","name":"Calvin Loncaric","path":"/Calvin-L","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1393639?s=80&v=4"},"commit":{"message":"Simplify and document the definition of `BuffMask`\n\nSigned-off-by: Calvin Loncaric <calvin.loncaric@oracle.com>","shortMessageHtmlLink":"Simplify and document the definition of <code>BuffMask</code>"}},{"before":null,"after":"35ed7b685ccb7e8dc869c0ad78834901db912c3e","ref":"refs/heads/mku-easymock2.4.0","pushedAt":"2024-06-10T18:50:30.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"},"commit":{"message":"Fix compiler error introduced by recent refactoring that assumes a newer\nversion of Easymock than what TLAToolbox.target defines.\n\n[Build][TLC][Test]\n\nSigned-off-by: Markus Alexander Kuppe <github.com@lemmster.de>","shortMessageHtmlLink":"Fix compiler error introduced by recent refactoring that assumes a newer"}},{"before":"b567b6b405179bf927c73147e39a3df8db55f802","after":"2bfa142d595e54487b74a793cfb5578f091f2b82","ref":"refs/heads/master","pushedAt":"2024-06-05T23:22:25.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"},"commit":{"message":"Change compilation warning message\n\nSigned-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>","shortMessageHtmlLink":"Change compilation warning message"}},{"before":"5991ab165c84c5dcc6cdfba90fe40f1250f63377","after":"b567b6b405179bf927c73147e39a3df8db55f802","ref":"refs/heads/master","pushedAt":"2024-06-02T18:47:54.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"},"commit":{"message":"Fixed miscellaneous warnings\n\nSigned-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>","shortMessageHtmlLink":"Fixed miscellaneous warnings"}},{"before":"72793369891dd72d31d6d48444df18b33434c966","after":"5991ab165c84c5dcc6cdfba90fe40f1250f63377","ref":"refs/heads/master","pushedAt":"2024-05-30T16:19:26.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"},"commit":{"message":"ISSUE_TEMPLATE: moving \"expected behavior\" to after \"to reproduce\"\n\nIt's more natural for \"expected behavior\" to go after the \"steps to\nreproduce\" were described.","shortMessageHtmlLink":"ISSUE_TEMPLATE: moving \"expected behavior\" to after \"to reproduce\""}},{"before":"72c23c95cbf1ae61908628d9dd65b712f1e4e2e0","after":"72793369891dd72d31d6d48444df18b33434c966","ref":"refs/heads/master","pushedAt":"2024-05-20T18:19:04.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"Calvin-L","name":"Calvin Loncaric","path":"/Calvin-L","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1393639?s=80&v=4"},"commit":{"message":"Fix usage of mavent-antrun-plugin\n\nSigned-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>","shortMessageHtmlLink":"Fix usage of mavent-antrun-plugin"}},{"before":"fa4968f60a0a460da4b7e182330680ce93bd96aa","after":"72c23c95cbf1ae61908628d9dd65b712f1e4e2e0","ref":"refs/heads/master","pushedAt":"2024-05-08T15:11:19.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"},"commit":{"message":"Algorithm variant has been proven in \"Refinement Proofs in Rust Using Ghost Locks\"\n\nAddresses Github issue #916\r\nhttps://github.com/tlaplus/tlaplus/issues/916\r\n\r\n[Documentation][TLC]","shortMessageHtmlLink":"Algorithm variant has been proven in \"Refinement Proofs in Rust Using…"}},{"before":"03c7bf4f35ccf1217ac2c53e5bf60d1220c8b0d8","after":"fa4968f60a0a460da4b7e182330680ce93bd96aa","ref":"refs/heads/master","pushedAt":"2024-04-27T22:40:18.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"},"commit":{"message":"Use Java 11 but not specific version in CI\n\nSigned-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>","shortMessageHtmlLink":"Use Java 11 but not specific version in CI"}},{"before":"e44242262b02d6c28127171fc8be0ca3249267fd","after":"99e6322cd152c44dec03677c51f45728a4041539","ref":"refs/heads/cal-gh835-bufferedrandomaccessfile","pushedAt":"2024-04-24T22:01:33.000Z","pushType":"push","commitsCount":4,"pusher":{"login":"Calvin-L","name":"Calvin Loncaric","path":"/Calvin-L","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1393639?s=80&v=4"},"commit":{"message":"Add a focused, well-documented test for setLength pointer interaction\n\nSigned-off-by: Calvin Loncaric <calvin.loncaric@oracle.com>","shortMessageHtmlLink":"Add a focused, well-documented test for setLength pointer interaction"}},{"before":"197b11a7b0ac17afcdd01f36b680be848d55e8de","after":"e44242262b02d6c28127171fc8be0ca3249267fd","ref":"refs/heads/cal-gh835-bufferedrandomaccessfile","pushedAt":"2024-04-23T21:36:18.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Calvin-L","name":"Calvin Loncaric","path":"/Calvin-L","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1393639?s=80&v=4"},"commit":{"message":"Simplify `TruncateOrExtendFile`\n\nSigned-off-by: Calvin Loncaric <calvin.loncaric@oracle.com>","shortMessageHtmlLink":"Simplify <code>TruncateOrExtendFile</code>"}},{"before":"297c4c8350a2c6cf76830f20e89b0618cd8bcfb7","after":"197b11a7b0ac17afcdd01f36b680be848d55e8de","ref":"refs/heads/cal-gh835-bufferedrandomaccessfile","pushedAt":"2024-04-23T21:01:43.000Z","pushType":"push","commitsCount":6,"pusher":{"login":"Calvin-L","name":"Calvin Loncaric","path":"/Calvin-L","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1393639?s=80&v=4"},"commit":{"message":"Note a potential optimization opportunity\n\nSigned-off-by: Calvin Loncaric <calvin.loncaric@oracle.com>","shortMessageHtmlLink":"Note a potential optimization opportunity"}},{"before":"4b513adab1fc94f4cdfffbcff4e39f1fe3e8932b","after":"03c7bf4f35ccf1217ac2c53e5bf60d1220c8b0d8","ref":"refs/heads/master","pushedAt":"2024-04-20T13:10:30.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"},"commit":{"message":"Fix CI in response to breaking changes in tlaplus/examples repo\n\nSigned-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>","shortMessageHtmlLink":"Fix CI in response to breaking changes in tlaplus/examples repo"}},{"before":"6fb13e9d0e5d35ac7ad6d5beab8ae94e3dcdde96","after":"4b513adab1fc94f4cdfffbcff4e39f1fe3e8932b","ref":"refs/heads/master","pushedAt":"2024-04-18T00:25:49.000Z","pushType":"pr_merge","commitsCount":5,"pusher":{"login":"Calvin-L","name":"Calvin Loncaric","path":"/Calvin-L","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1393639?s=80&v=4"},"commit":{"message":"Use nio file API in pcal.trans\n\nSigned-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>","shortMessageHtmlLink":"Use nio file API in pcal.trans"}},{"before":"0cbbd06847de6f2d47b631f55806ce20baa7541b","after":null,"ref":"refs/heads/mku-DebuggerINotInModelFunctor","pushedAt":"2024-04-11T22:04:31.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"}},{"before":"f135b2c6db08b31be45e3ab217213d9a03d75414","after":"6fb13e9d0e5d35ac7ad6d5beab8ae94e3dcdde96","ref":"refs/heads/master","pushedAt":"2024-04-11T21:12:52.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"},"commit":{"message":"'constrained' states not added to e.g. dot output if TLC runs under TLA+\ndebugger.\n\nRelated to git commit c2713def38aa1d3255a6c2fe2aa037253e00e361\n\nHave DebugTool implement INotInModelFunctor.\n\n[Bug][TLC]\n\nSigned-off-by: Markus Alexander Kuppe <github.com@lemmster.de>","shortMessageHtmlLink":"'constrained' states not added to e.g. dot output if TLC runs under TLA+"}},{"before":"8fa1f19c4d4a1da46d4212208cd9249e96f14fb5","after":"f135b2c6db08b31be45e3ab217213d9a03d75414","ref":"refs/heads/master","pushedAt":"2024-04-11T20:57:18.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"Calvin-L","name":"Calvin Loncaric","path":"/Calvin-L","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1393639?s=80&v=4"},"commit":{"message":"Fix unit test error reporting and support `-Dthreads=N` parameter (#903)\n\nSigned-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>","shortMessageHtmlLink":"Fix unit test error reporting and support <code>-Dthreads=N</code> parameter (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2234089946\" data-permission-text=\"Title is private\" data-url=\"https://github.com/tlaplus/tlaplus/issues/903\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/tlaplus/tlaplus/pull/903/hovercard\" href=\"https://github.com/tlaplus/tlaplus/pull/903\">#903</a>)"}},{"before":null,"after":"0cbbd06847de6f2d47b631f55806ce20baa7541b","ref":"refs/heads/mku-DebuggerINotInModelFunctor","pushedAt":"2024-04-11T18:56:55.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"},"commit":{"message":"'constrained' states not added to e.g. dot output if TLC runs under TLA+\ndebugger.\n\nRelated to git commit c2713def38aa1d3255a6c2fe2aa037253e00e361\n\nHave DebugTool implement INotInModelFunctor.\n\n[Bug][TLC]\n\nSigned-off-by: Markus Alexander Kuppe <github.com@lemmster.de>","shortMessageHtmlLink":"'constrained' states not added to e.g. dot output if TLC runs under TLA+"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEY54C0AA","startCursor":null,"endCursor":null}},"title":"Activity · tlaplus/tlaplus"}