Skip to content

Instantly share code, notes, and snippets.

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

Cheshire Cat y-taka-23

83 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 / alloy_git.als
Last active July 13, 2022 18:00
Alloy による Git のコミットグラフのモデリング
// ************************************
// Git のコミットグラフのモデル
// ************************************
open util/ordering[Time]
// ------------------------------------
// グラフの構成要素
// ------------------------------------
@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 / 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 / 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 / coq_quine.v
Last active November 15, 2019 20:44
Quine (Self-Reproducing Program) on Coq
Require Import Ascii String.
Open Scope string_scope.
Definition Q : string := "
Eval compute in ""
Require Import Ascii String.
Open Scope string_scope.
Definition Q : string := "" ++ """" ++ Q ++ """" ++ ""."" ++ Q.".
Eval compute in "
Require Import Ascii String.
Open Scope string_scope.
@y-taka-23
y-taka-23 / alloy_vender.als
Last active July 27, 2018 12:53
Alloy による自動販売機のモデリング
// ************************************
// ジュースの自動販売機のモデル
// ************************************
open util/ordering[Time]
// 時刻パラメータ
sig Time {}
// 簡略化のため、コインの額面とジュースの種類はそれぞれ 1 種類とする
@y-taka-23
y-taka-23 / coq_filter.v
Last active May 21, 2018 03:26
Validation of the filter Function (via "Software Foundations" http://www.cis.upenn.edu/~bcpierce/sf/Logic.html)
(******************************************************)
(** //// Validation of the "filter" Function //// *)
(******************************************************)
Require Import List Bool Lt.
Section Filter.
(*////////////////////////////////////////////////////*)
@y-taka-23
y-taka-23 / seminar_20140130.md
Created January 14, 2014 14:29

名古屋モデル検査勉強会 #2

前回の勉強会では Promela の文法要素と基本的な SPIN の使い方を眺めたので、今回は LTL 式を用いた性質検査およびハンズオンを行う。

LTL 式による検査

LTL 式の構文

SPIN の LTL は命題論理の拡張となっており、各論理式の真偽が状態に依存する。