Skip to content

Instantly share code, notes, and snippets.

@lemmy
lemmy / SwitchLights.swift
Created December 26, 2023 18:34
Turn of lights when the display sleeps
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
{"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
@lemmy
lemmy / Simple.cfg
Last active December 24, 2022 04:28
INIT Init
NEXT Next
INVARIANT Inv
@lemmy
lemmy / FoldSort.tla
Created March 5, 2022 18:32
FoldSort.tla
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(_)) ==
--------------------------- 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",
@lemmy
lemmy / settings.json
Created October 7, 2021 02:00
VSCode settings.json
"saveAndRunExt": {
"commands": [
{
"match": "\\.tla$",
"isShellCommand": false,
"silent": true,
"cmd": "tlaplus.debugger.smoke"
}
]
}
@lemmy
lemmy / Qsort.tla
Created June 12, 2021 03:06
A toy program to sort characters with QuickSort (implemented" in TLA+)
$ ./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]:
@lemmy
lemmy / Echo.tla
Created August 3, 2020 19:43
Echo.tla
-------------------------------- 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
/*******************************************************************************
* Copyright (c) 2018 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
@lemmy
lemmy / Installation
Last active December 11, 2019 17:19
TLC Execution Statistics Ingress into SQL for Analytics (Metabase)
apt-get install postgresql postgresql-11 postgresql-common postgresql-client-11 postgresql-client-common
apt-get install psycopg2 libpq-dev python-dev
apt-get install libapache2-mod-wsgi-py3 python-dev
apt-get install python3-flask
apt-get install python3-psycopg2