Markus Alexander Kuppe lemmy
lemmy
/ RiverCrossingFlashlight.cfg
Created
May 13, 2025 22:36
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| SPECIFICATION Spec | |
| CONSTANTS | |
| A = "A" | |
| B = "B" | |
| C = "C" | |
| D = "D" | |
| INVARIANT NotGoal |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| ----- MODULE MergeQueueProcess ----- | |
| EXTENDS Naturals | |
| CONSTANT PRs | |
| VARIABLE pullRequests, time | |
| Init == | |
| /\ pullRequests = [pr \in PRs |-> [state |-> "pending", t |-> 0]] | |
| /\ time = 0 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| import Foundation | |
| import CoreGraphics | |
| // Define the URL for the HTTP GET request | |
| let baseURL = "http://tasmota-f72dd5-3541.fritz.box/cm?cmnd=Power%20" | |
| // Create a URLSession | |
| let session = URLSession.shared | |
| // Define a function to create a task with a URL |
lemmy
/ bad_network.ndjson
Created
April 21, 2023 17:20
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {"h_ts":"4","thread_id":"100","level":"info","tag":"tla","file":"../src/consensus/aft/raft.h","number":"494","msg":{"configurations":[{"idx":0,"nodes":{"0":{"address":":"},"1":{"address":":"},"2":{"address":":"}},"rid":0}],"event":{"component":"raft","function":"add_configuration"},"leadership":"none","membership":"Active","node":"0","state":{"cft_watermark_idx":0,"commit_idx":0,"current_view":0,"last_idx":0,"my_node_id":"0"}}} | |
| {"h_ts":"8","thread_id":"100","level":"info","tag":"tla","file":"../src/consensus/aft/raft.h","number":"494","msg":{"configurations":[{"idx":0,"nodes":{"0":{"address":":"},"1":{"address":":"},"2":{"address":":"}},"rid":0}],"event":{"component":"raft","function":"add_configuration"},"leadership":"none","membership":"Active","node":"1","state":{"cft_watermark_idx":0,"commit_idx":0,"current_view":0,"last_idx":0,"my_node_id":"1"}}} | |
| {"h_ts":"12","thread_id":"100","level":"info","tag":"tla","file":"../src/consensus/aft/raft.h","number":"494","msg":{"configurations":[{"idx":0,"nodes":{"0":{"a |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| INIT Init | |
| NEXT Next | |
| INVARIANT Inv |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| No annotation found for Frob$1. Make sure that you've put one in front of Frob$1. E@18:30:44.591 | |
| ----- MODULE FoldSort ----- | |
| EXTENDS Integers, Sequences, Apalache | |
| \* @type: (Seq(Int), (a => Bool)) => Seq(Int); | |
| FilterSeq(seq, cmp(_)) == |
lemmy
/ TLAPlus2Grammar.tla
Last active
October 27, 2021 01:18
Created from Lamport's TLA+ grammar at http://lamport.azurewebsites.net/tla/TLAPlus2Grammar.tla
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| --------------------------- MODULE TLAPlus2Grammar --------------------------- | |
| EXTENDS Naturals, Sequences, BNFGrammars | |
| CommaList(L) == L & (tok(",") & L)^* | |
| AtLeast4(s) == Tok({s \o s \o s} & {s}^+) | |
| ReservedWord == | |
| { "ASSUME", "ELSE", "LOCAL", "UNION", | |
| "ASSUMPTION", "ENABLED", "MODULE", "VARIABLE", | |
| "AXIOM", "EXCEPT", "OTHER", "VARIABLES", |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| "saveAndRunExt": { | |
| "commands": [ | |
| { | |
| "match": "\\.tla$", | |
| "isShellCommand": false, | |
| "silent": true, | |
| "cmd": "tlaplus.debugger.smoke" | |
| } | |
| ] | |
| } |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| $ ./pluspy -s modules/other/Qsort.tla | |
| Enter input: poiuylkjhmnbvcdsxzafgtrewq | |
| abcdefghijklmnopqrstuvwxyz | |
| ----------------------------- MODULE Qsort ----------------------------- | |
| EXTENDS Naturals, Sequences, FiniteSets, TLC, Input | |
| \* Specification (works reasonably well for sets of cardinality <= 6 | |
| \* Takes a set as argument, produces a sorted tuple | |
| Sort(S) == CHOOSE s \in [ 1..Cardinality(S) -> S]: |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| -------------------------------- MODULE Echo -------------------------------- | |
| (***************************************************************************) | |
| (* The Echo algorithm for constructing a spanning tree in an undirected *) | |
| (* graph starting from a single initiator, as a PlusCal algorithm. *) | |
| (***************************************************************************) | |
| EXTENDS Naturals, FiniteSets, Relation, TLC | |
| CONSTANTS Node, \* set of nodes | |
| initiator, \* single initiator, will be the root of the tree | |
| R \* neighborhood relation, represented as a Boolean function over nodes |
NewerOlder