Haskell-Copilotによる時相の組み込みプログラミング

概要

時相とは時間的性質を指定する概念であり、多くのソフトウェアに設計時点から登場するものです。例えば「人を検知して数秒間はライトを着けたままにする」「数時間間隔でリクエストを投げる」「↓+➘+→+Pの順番入力で技を出す」などです。これらは多くの場合スレッドとスリープ関数や時間取得関数、割り込みなどを組み合わせて実現され、その結果の実装コードは設計で端的に書いた時相表現と見た目が離れ、更に並行した機能との兼ね合いからモノリシックになっていくことが多いです。例えば以下は組み込みプログラミングでLチカと呼ばれる「秒間隔でLEDのON-OFFを繰り返す」という時相要素を持つ一番初歩のコードです。

while (true) {
    sleep_ms(1000);
    led_on();
    sleep_ms(1000);
    led_off();
}

ここまで内容を細かに解きほぐして書かないと機能は実装出来ませんし、「一点間隔の繰り返し」という時相要素と「LEDのON-OFF」という入出力要素が一緒になっています。さらに並行してボタンも制御してほしい要望が来た場合は、スレッドか割り込みなどを必要とします。そのボタンを押されたら数秒間だけ点滅を停止したい、、、となった場合は？どんどん変数と条件の複雑さが増していき、設計の時相の言葉と実装コードでの表現が乖離していきます。結果は求めたものになるのでしょうけども。
一方、今回使用したHaskellのCopilotというライブラリは時相要素をモジュラリティを持って構成することとその合成、並行実行を可能とします。AVRなどのマイコンの単一スレッドで。時相を構成したコードの結果はC言語のモジュール(.cと.hファイル)として変換出力されるため、C言語が使える環境であればどこでも動きます。ただし出てくるCは以下のように人間には読めず長大で、コンパイル後のバイナリサイズはなかなか大きくなります。以降の動画に使ったプログラムのフラッシュサイズは26kbyte程です。大きい、、んですかね？

C言語への出力結果

#include <stdint.h>
#include <stdbool.h>
#include <string.h>
#include <stdlib.h>
#include <math.h>

#include "copilot_cords_types.h"
#include "copilot_cords.h"

static bool button_plus_cpy;
static bool button_minus_cpy;
static bool button_A_cpy;
static bool button_B_cpy;
static uint8_t s0[(2)] = {((uint8_t)(0)), ((uint8_t)(1))};
static int32_t s1[(1)] = {((int32_t)(0))};
static bool s2[(1)] = {(false)};
static int32_t s4[(1)] = {((int32_t)(0))};
static bool s5[(1)] = {(false)};
static int16_t s3[(1)] = {((int16_t)(0))};
static uint16_t s7[(1)] = {((uint16_t)(0))};
//省略
static uint8_t s0_get(size_t x) {
  return (s0)[((s0_idx) + (x)) % ((size_t)(2))];
}

static int32_t s1_get(size_t x) {
  return (s1)[((s1_idx) + (x)) % ((size_t)(1))];
}

static bool s2_get(size_t x) {
  return (s2)[((s2_idx) + (x)) % ((size_t)(1))];
}

static int32_t s4_get(size_t x) {
  return (s4)[((s4_idx) + (x)) % ((size_t)(1))];
}
//省略
void step(void) {
  uint8_t s0_tmp;
  int32_t s1_tmp;
  bool s2_tmp;
  int32_t s4_tmp;
  bool s5_tmp;
  int16_t s3_tmp;
  uint16_t s7_tmp;
  bool s6_tmp;
//省略
  if ((show_7seg_0_guard)()) {
    {(show_7seg_0_arg_temp0) = ((show_7seg_0_arg0)());
     (show_7seg_0_arg_temp1) = ((show_7seg_0_arg1)());
     (show_7seg)((show_7seg_0_arg_temp0), (show_7seg_0_arg_temp1));}
  };
  if ((change_led_1_guard)()) {
    {(change_led_1_arg_temp0) = ((change_led_1_arg0)());
     (change_led)((change_led_1_arg_temp0));}
  };
  (s0_tmp) = ((s0_gen)());
  (s1_tmp) = ((s1_gen)());
  (s2_tmp) = ((s2_gen)());
  (s4_tmp) = ((s4_gen)());
  (s5_tmp) = ((s5_gen)());
  (s3_tmp) = ((s3_gen)());
  (s7_tmp) = ((s7_gen)());
  (s6_tmp) = ((s6_gen)());
  (s9_tmp) = ((s9_gen)());
  (s10_tmp) = ((s10_gen)());
  (s11_tmp) = ((s11_gen)());
//省略
  (s51_idx) = (((s51_idx) + ((size_t)(1))) % ((size_t)(1)));
  (s58_idx) = (((s58_idx) + ((size_t)(1))) % ((size_t)(1)));
  (s57_idx) = (((s57_idx) + ((size_t)(1))) % ((size_t)(1)));
  (s60_idx) = (((s60_idx) + ((size_t)(1))) % ((size_t)(1)));
  (s59_idx) = (((s59_idx) + ((size_t)(1))) % ((size_t)(1)));
}

この記事では、主要な時相要素を持つ関数の定義と、その応用例をatmega328pを使用した回路の動作映像を使って紹介していきます。

開発環境

名前	バージョン
OS	Ubuntu 20.04
CPU	AMD Ryzen 9 3900XT
ghcup	0.1.50.2
stack	3.3.1
avr-gcc	5.4.0
avrdude	6.3-20171130

Githubリンク

stackの環境です。
https://github.com/yosukeueda33/temporal-practice

以下でC言語への変換からelf生成まで実行できます。

stack build
stack run
make

以下で実装したコードはapp/Main.hsとsrc/Lib.hsにあります。
main.cにLEDやボタン状態更新などのローレイヤのコードと、上記stack run時に出力されるHeaskell-Copilot側の出力モジュールcopilot_cords.cに記述される時相評価関数step()を呼ぶコードを記述しています。makeで一つのmain.elfとして出力されます。

回路構成

各関数の挙動を示すために構成しました。
マイコンはATMEGA328P-PU、7SEGLEDはSPI(っぽい)通信のシフトレジスタ(74hc595n)を経由して接続しています(桁制御はGPIO)。説明では主にA,Bと書かれたボタンと、OutputのLEDを使います。

回路図は余裕が出来た時に作りたい、、、

C言語とのインターフェース

CとCopilot用のHaskellコードは以下のようにグローバル変数参照のexternと関数参照のtriggerでインターフェースされます。第2引数がトリガ条件、triggerの第3引数が引数リストです。

buttonPlus = extern "button_plus" Nothing
buttonMinus = extern "button_minus" Nothing

trigger "show_7seg" true [arg digit, arg digitNum]
trigger "change_led" true progs

以下はC側です。

bool button_plus = false;
bool button_minus = false;
bool button_A = false;
bool button_B = false;

void update_inputs(){ // Called from main before timestep.
    button_plus = !(PINC & (1 << PC0));
    button_minus = !(PINC & (1 << PC1));
    button_A = !(PINC & (1 << PC3));
    button_B = !(PINC & (1 << PC2));
}

void change_led(bool x){
    if (x) {
        PORTB |= (1 << PB0);
    } else {
        PORTB &= ~(1 << PB0);
    }
}

void show_7seg(uint8_t digit, uint8_t data) {
    change_digit(digit);
    SPDR = digits_ca[data % 10];
    while (!(SPSR & (1 << SPIF)));       // Wait for completion
    latch();
}

時相論理の実装

時相論理はAND、ORなどの論理演算の仲間です。この実装ではその内LTL-b-pというカテゴリのものをTemporal Logic and State Systemsを参考に定義しました。
少々高いテキストですが、年末セールで1000円位で買えました。理論的に精緻化され、ド・モルガンの法則などと同様に組み合わせた同値関係の調査も進んでいます。実装向きには使いづらい面もあったので今回の実装では少々修正を施しています。

weakPrevious

前回の時間ステップでの入力sを出力します。サンプル時間を1msecとしているので、入力とほぼ同時に出力点灯している様に見えるかと思います。++は1項目を前の時間ステップでの出力、2項目を次の時間ステップでの出力とする演算子です。wPは別名として定義しています。

weakPrevious, wP :: Stream Bool -> Stream Bool
weakPrevious s = [True] ++ s
wP = weakPrevious

https://youtu.be/SKyVbCLY5s8?t=720

strongPrevious

これはweakPreviousとほぼ変わらないです。プログラム開始時の初期値がFalseになっています。sPは別名として定義しています。

strongPrevious, sP :: Stream Bool -> Stream Bool
strongPrevious s = [False] ++ s
sP = strongPrevious

https://youtu.be/SKyVbCLY5s8?t=771

alwaysBeen

これまでにONのままだったのかを出力します。もとの定義だと0ステップ目からの判定となっており使いづらかったので、遡る時間ステップを引数lenで指定できるようにしています。muxはif then elseと読み替えて下さい。ノイズが多い入力の場合のフィルタとして使えます。

alwaysBeen' :: Stream Int32 -> Stream Bool -> Stream Bool
alwaysBeen' len s = cnt >= (len - 1) -- && s
  where
    cnt = [0] ++ mux s (cnt + 1) 0

1秒間(使用しているハードクロックの精度が悪いので結果1.5くらいかも)ONだったらLEDがONになります。
https://youtu.be/SKyVbCLY5s8?t=593

once

これまでに入力ONがあったかを出力とします。alwaysBeenと同様にlenで区間指定できるようにしました。入力を保持する用途に使えます。

once' :: Stream Int32 -> Stream Bool -> Stream Bool
once' len s = cnt > 0
  where
    cnt = [0] ++ mux s len (lim 0 $ cnt - 1)
    lim l x = mux (l < x) x l

https://youtu.be/SKyVbCLY5s8?t=661

since

AとBの2入力を使います。Bが入力された状態でAが押され、それ以降Aが押されている期間中はONをキープします。もとのsinceの定義ではB入力時に出力が開始され気持ち悪いのでA入力時のみ反応するsince'を追加しました。

since, since' :: Stream Bool -> Stream Bool -> Stream Bool
since a b = v
  where
    v = [False] ++ b || (a && v)

since' a b = a && since a b

https://youtu.be/SKyVbCLY5s8?t=844

backTo

sinceと初期値以外変わらないです。

backTo :: Stream Bool -> Stream Bool -> Stream Bool
backTo a b = v
  where
    v = [True] ++ b || (a && v)

https://www.youtube.com/watch?v=SKyVbCLY5s8

atLast

最後にBが入力された時にAの入力されていたのかをAがOFFになっても保持します。BのみONとなったら出力OFFになります。オリジナルだと最初からONのままなので、atLast'で修正しています。

atLast, atLast' :: Stream Bool -> Stream Bool -> Stream Bool
atLast a b = v
  where
    v = [True] ++ (b ==> a) && (not b ==> v)

atLast' a b = v
  where
    v = [False] ++ (b ==> a) && (not b ==> v)

https://youtu.be/SKyVbCLY5s8?t=1002

after

B入力後のA入力かを判定出力します。B中のAは弾きます。atLastと同様にA入力が無くても出力を保持し、Bのみ入力で解除となります。

after, after' :: Stream Bool -> Stream Bool -> Stream Bool
after a b = v
  where
    v = [True] ++ (not b) && (a || v)

after' a b = v
  where
    v = [False] ++ (not b) && (a || v)

https://youtu.be/SKyVbCLY5s8?t=1094

その他の時相要素を持つ演算の実装

以降は、経験上これは必要だろうと思った時相演算を関数として実装した紹介です。実際は上記の関数の合成で行けるかも知れませんが。

oneShotRise

入力がOFFからONに変わった瞬間のみONとなります。oneShotRise, oneShotRise'は等価です。

oneShotRise, oneShotRise'  :: Stream Bool -> Stream Bool
oneShotRise s = s && not (sP s)
oneShotRise' s = s && not prev
  where
    prev = [False] ++ s

https://youtu.be/SKyVbCLY5s8?t=340

oneShotFall

入力がONからOFFに変わった瞬間のみONとなります。oneShotFall, oneShotFall'は等価です。

oneShotFall, oneShotFall' :: Stream Bool -> Stream Bool
oneShotFall s = not s && sP s
oneShotFall' s = not s && prev
  where
    prev = [False] ++ s

https://youtu.be/SKyVbCLY5s8?t=369

toggle

入力ONで毎回、出力がON/OFF切り替わります。 T-FFですね。単体だと入力ONが入り続けてしまうので、動画ではoneShotRiseと組み合わせて使っています。

toggle :: Stream Bool -> Stream Bool
toggle s = r
  where
    r = [False] ++ mux s (not r) r

https://youtu.be/SKyVbCLY5s8?t=431

srsFF

SR-FFをベースとしています。setSigのONで出力ON、resetSigのONで出力OFFとなります。どちらもONの場合はON側に寄せました。

srsFF :: Stream Bool -> Stream Bool -> Stream Bool
srsFF setSig resetSig = r
  where
    r = mux setSig true $ mux resetSig false prev
    prev = [False] ++ r

https://youtu.be/SKyVbCLY5s8?t=502

応用

上記の関数群を合成し、高度な時相による挙動をプログラミングした例です。モジュラリティを活かして平易に合成出来ていることが分かるかと思います。

debounce

動画に使用した回路のボタン含め、機械接点は安定しないものです。なので、ONからOFFに切り替わる際に値がバタつくので、例えば人流カウンタの様なものを作ろうとしたら一回のプッシュで10回カウントされたりします。このノイズを吸収するのがdebounceです。srsFF,oneShotRise,alwaysBeen'を合成して機能を実現しています。

debounce :: Stream Int32 -> Stream Bool -> Stream Bool 
debounce len s = srsFF trigRise trigFall
  where
    trigRise = oneShotRise $ alwaysBeen' len s
    trigFall = oneShotRise $ alwaysBeen' len $ not s

実は動画の4つのボタン入力には常にノイズ除去のために40msecのdebounceが入っています。
以下はその上で更に2secのdebounceを掛けています。
https://youtu.be/SKyVbCLY5s8?t=1321

時間制限付きの出力透過。忍耐付き。

Aの入力透過をBが押されて1秒のみ有効にするというものです。なお、有効なA後にBの時間から外れてもAが離されるまではONを保持します。

since' a $ once' 1000 b

https://youtu.be/SKyVbCLY5s8?t=1435

格ゲーのコマンド入力

動画の例ではBBAAという順番でボタンが押された時に出力をONとします。seriesPatternの引数のリスト内容を変えると内容が変更可能になっています。
seriesPatternは少々Haskell味が強いコードです。foldl(pythonやjavascriptのreduceみたいなもの)でsrsFFを再帰的にリストに適用し、連続的な状態遷移を表現しています。
与えるタプルリストのタプルの1要素目は求める入力、2番めは求めておらず入力されたらコマンドキャンセルとしたい入力です。
foldlがHaskellの基本関数なのに、後々CとなるCopilotのオブジェクトも有効に扱えてしまうのは、HaskellのDSLの良い所ですね。
もう少しやりようはある気がします。コマンド打ち終わった後aを続けても消えませんし。あとMonoidを構成できそうですね？というかMonadでは？環かも？別記事かきます。書きました

seriesPattern :: [(Stream Bool, Stream Bool)] -> Stream Bool
seriesPattern = foldl f true
  where
    f acc (s, cancel) = srsFF (sP acc && s) cancel

seriesPattern
    -- (wanted signal, signal for cancelation)
    [ (tr b, tr a)   
    , (tr b, tr a)
    , (tr a, tr b)
    , (tr a, tr b)]

https://youtu.be/SKyVbCLY5s8?t=1650

状態遷移

上記の状態遷移を行うものです。少々複雑化しますが、コアな箇所はmyStateFlowの引数のタプルリストにまとめられているため、保守性は高いはずです。動作のためには各状態でのLED制御部なども必要ですが、それはGithubを参照されて下さい。
以下は状態遷移の定義部です。

myStateFlow ::Stream Bool -> Stream Bool -> Stream Bool
            -> [(Stream Word8, [(Stream Bool, Stream Word8)])]
myStateFlow a b t = bmmap cvt (bmmap id cvt)
                $ [
                    (StayLit,  [ (a, BlinkSlow)
                                , (b, StayLit)])
                  , (BlinkSlow, [ (a, StayLit)
                                , (b, BlinkFast)])
                  , (BlinkFast, [ (a, BlinkSlow)
                                , (b, ResetTimer)
                                , (t, StayLit) ])
                  , (ResetTimer, [(true, BlinkFast)])
                  ]
  where
    cvt = Const . myStateToW8
    bmmap f1 f2 = map (BF.bimap f1 f2)

以下は、上記で定義した状態遷移を実際に信号として扱うコア部です。これもコマンド入力と同様にfoldlでmuxを適用しています。

stateFlow :: [(Stream Word8, [(Stream Bool, Stream Word8)])]
          -> Stream Word8 -> Stream Word8
stateFlow flow nowState =
    foldl (\acc (s, xs) -> mux  (s == nowState) (f xs) acc) nowState flow 
  where
    f :: [(Stream Bool, Stream Word8)] -> Stream Word8
    f = foldl (\acc (signal, s) -> mux signal s acc) nowState

https://youtu.be/SKyVbCLY5s8?t=1925

並行実行

すでにお見せした上記の動画の出力用LED,ボタン入力とその時相処理,7SEGのLED出力はすべて並行に実行出来ています。スレッドも割り込みも使っていません。これはStreamオブジェクトで時相要素としてタスク定義することで、ライブラリのC言語への変換処理により並行性が付加されることで実現されます。

おわりに

数年前所属していた会社で時相が絡む処理が多く、もっと楽に設計の言葉のままコード記述できないかと考え、退職後も継続して調べていました。それでようやくたどり着いた今回の成果には満足しています。しかし結局これにはHaskellという既存の組み込み系の企業では普通でない分野の理解が必要なわけで企業として採用するには厳しい面があると思います。
セラロックを使っているにしても、時間指定箇所のズレが感覚的に大きい気がします。処理が重いのか？→まあまあ重かったようで、水晶発振子にしてstep()の周期呼び出し待ちを_delay_ms(1)ではなく、タイマ割り込みによる正確な時間を参照し待つようにしたら改善しました。