Skip to content

Instantly share code, notes, and snippets.

View thpani's full-sized avatar
🦚

Thomas Pani thpani

🦚
19 followers · 5 following
View GitHub Profile
@thpani
thpani / 00_OutSanyParser.tla
Created June 30, 2023 10:47
--------------------------- MODULE 00_OutSanyParser ---------------------------
EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache
(*
@type: ((Set(a), a) => Set(a));
*)
add(s, e) == s \union {e}
(*
@thpani
thpani / 00_OutSanyParser.tla
Created June 30, 2023 10:41
--------------------------- MODULE 00_OutSanyParser ---------------------------
EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache
(*
@type: ((Set(a), a) => Set(a));
*)
add(s, e) == s \union {e}
(*
@thpani
thpani / River.tla
Created June 19, 2023 12:44
--------------------------- MODULE River ---------------------------
EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache
VARIABLE
(*
@type: Set(Str);
*)
origin
@thpani
thpani / Oracle.tla
Created April 27, 2022 10:14
------ MODULE Oracle --------
VARIABLES
\* @type: Set((Bool -> Int));
witness,
\* @type: Bool;
found
Init ==
/\ witness \in {[BOOLEAN -> {222521218, 0}], [{TRUE} -> {2147483647}]}
/\ found \in BOOLEAN
@thpani
thpani / Verifier.tla
Last active April 25, 2022 08:58
------ MODULE Verifier --------
EXTENDS Apalache, Integers
VARIABLES
\* @type: <<[oAPt: Set(Bool)], [zt48: Set(Bool)]>>;
result,
\* @type: Bool;
found
@thpani
thpani / profile.csv
Created March 30, 2022 13:12
# weight nCells nConsts nSmtExprs location
1363 786 476 10391 staking_apa.tla:473:5-490:55
1353 780 472 10351 staking_apa.tla:487:8-490:55
1339 772 466 10267 staking_apa.tla:487:8-490:55
1324 764 460 10183 staking_apa.tla:487:8-490:55
1321 762 459 10183 staking_apa.tla:487:8-490:55
1305 751 454 10117 staking_apa.tla:487:8-490:55
1182 677 411 8843 staking_apa.tla:487:8-490:55
1009 573 352 7105 staking_apa.tla:487:8-490:55
798 451 277 4909 staking_apa.tla:487:8-490:55
@thpani
thpani / config.mk
Created February 18, 2022 13:21
PREFIX=/usr/local/opt/python@3.9/Frameworks/Python.framework/Versions/3.9
CC=gcc
CXX=g++
CXXFLAGS= -D_MP_INTERNAL -DNDEBUG -D_EXTERNAL_RELEASE -std=c++17 -fvisibility=hidden -fvisibility-inlines-hidden -c -O3 -Wno-unknown-pragmas -Wno-overloaded-virtual -Wno-unused-value -fPIC -arch arm64
CFLAGS= -D_MP_INTERNAL -DNDEBUG -D_EXTERNAL_RELEASE -fvisibility=hidden -fvisibility-inlines-hidden -c -mfpmath=sse -msse -msse2 -O3 -Wno-unknown-pragmas -Wno-overloaded-virtual -Wno-unused-value -fPIC
EXAMP_DEBUG_FLAG=
CXX_OUT_FLAG=-o
C_OUT_FLAG=-o
OBJ_EXT=.o
LIB_EXT=.a
@thpani
thpani / # z3 - 2017-11-07_09-37-23.txt
Created November 7, 2017 08:39
z3 on macOS 10.11.6 - Homebrew build logs
Homebrew build logs for z3 on macOS 10.11.6
Build date: 2017-11-07 09:37:23
@thpani
thpani / minix.sh
Created March 3, 2014 16:30
# clone minix v3.2.1 to bench/minix
[[ -L bench/minix/include/machine ]] || ln -s arch/i386/include/ ./bench/minix/include/machine
[[ -L bench/minix/sys/machine ]] || ln -s arch/i386/include/ ./bench/minix/sys/machine
[[ -L bench/minix/sys/x86 ]] || ln -s arch/x86/include/ ./bench/minix/sys/x86
for f in $(find bench/minix/kernel/ -not -path 'bench/minix/kernel/arch/earm/*' -name '*.c') ; do bin/sloopy -allow-infinite-loops $f -- \
-Ibench/minix/ \
-Ibench/minix/include/ \
-Ibench/minix/kernel/ \
@thpani
thpani / rpi.md
Last active December 25, 2015 22:49
My Raspberry Pi setup routine

Raspberry Pi setup routine

Note I've started to transform my setup guide to Ansible playbooks at thpani/pi.

Headless boot to SSH over WiFi

/etc/network/interfaces