Skip to content

Instantly share code, notes, and snippets.

View y-taka-23's full-sized avatar

Cheshire Cat y-taka-23

88 followers · 31 following
View GitHub Profile
@y-taka-23
y-taka-23 / elmjp_2023.md
Last active July 22, 2023 07:11
Elm-jp 2023: Elm による大学入学共通テスト指南
@y-taka-23
y-taka-23 / signal.als
Last active December 3, 2021 15:49
Traffic signals with Alloy 6's temporal logic
module signal
enum LightState { On, Off, Blink }
abstract sig Light {
var state: one LightState
}
one sig Red, Green extends Light {}
@y-taka-23
y-taka-23 / mov-to-gif.sh
Created August 8, 2021 18:48
A script for converting mov to gif
#!/bin/bash
rm -f cut.mov
rm -f palette.png
rm -f encoded.gif
rm -f output.gif
ffmpeg -ss 10 -to 15 -i input.mov -c copy cut.mov
ffmpeg -i cut.mov -vf fps=30,scale=340:-1:flags=lanczos,palettegen palette.png
ffmpeg -i cut.mov -i palette.png -filter_complex "fps=30,scale=340:-1:flags=lanczos[x];[x][1:v]paletteuse" encoded.gif
@y-taka-23
y-taka-23 / Sample.hs
Created December 24, 2016 10:27
Samples of Verification by LiquidHaskell
module Sample where
import Language.Haskell.Liquid.Prelude ( liquidError )
{-@ safeHead :: { xs:[a] | len xs > 0 } -> a @-}
safeHead [] = liquidError "empty list"
safeHead (x : _) = x
-- badUsage = safeHead [] -- => Liquid Type Mismatch
@y-taka-23
y-taka-23 / alloy_kubernetes.als
Last active December 19, 2016 19:08
Alloy による Kubernetes のコンテナスケジューリングのモデリング
open util/ordering[Time]
sig Time {}
abstract sig Event {
pre, post : Time,
} {
post = pre.next
}
@y-taka-23
y-taka-23 / alloy_sequent.als
Last active December 23, 2015 10:04
Alloy による命題論理のシークエント計算のモデリング
// ************************************
// 命題論理のシークエント計算のモデル
// ************************************
// 論理式
abstract sig Formula {}
// 原子命題
sig Atom extends Formula {}
@y-taka-23
y-taka-23 / alloy_aws_security_group.als
Created December 6, 2015 14:31
Alloy による AWS セキュリティグループのモデリング
// **************************************************
// AWS セキュリティグループのモデル
// **************************************************
// 通信プロトコル
enum Protocol { TCP, UDP, ICMP }
// 通信ポート
sig Port {}
@y-taka-23
y-taka-23 / coq_uniq.v
Created September 12, 2015 06:31
An Implementation of the uniq Command Certified by Coq
Parameter A : Type.
Parameter beq_A : A -> A -> bool.
Section Uniq.
Require Import Arith List.
Hypothesis beq_A_true : forall x y : A,
beq_A x y = true -> x = y.
Hypothesis beq_A_false : forall x y : A,
@y-taka-23
y-taka-23 / promela_sharing.pml
Created December 14, 2014 14:58
An Invalid (Deadlocked) Model of Resource Sharing Problem
/*
* Resource Sharing Problem (Example for Deadlock)
*/
mtype = { LOCK, UNLOCK };
proctype Client(chan to_res1, to_res2) {
if
:: to_res1 ! LOCK(_pid);
to_res2 ! LOCK(_pid);
@y-taka-23
y-taka-23 / death_march_05.cob
Last active August 29, 2015 14:05
CodeIQ「第 5 回デスマコロシアム」の固定形式 COBOL 85 による実装
IDENTIFICATION DIVISION.
PROGRAM-ID. DEATH-MARCH-05.
DATA DIVISION.
WORKING-STORAGE SECTION.
77 FB-STR PIC X(153).
77 CNT PIC 9(2) VALUE 1.
77 QUOT PIC 9(2).
77 REM-3 PIC 9(1).
77 REM-5 PIC 9(1).