# 入江ミーティングノート(2023/3/10~2024-06-07)
## 2024-06-05
- なぜかmeetingのhackmdへの接続が悪い
- Progress after last meeting:
- ギアシフトの実装をして、学習させました　結果を見せます
- 注意点　オラクルはlexicographically minimalではない(がintervalの端っこを当てることができる)ため、学習によってqueryの回数が前後します
- 論文の全ての証明を清書しました 読んでいただきたいです　証明は全て付録送りにしているのでAppendixにある証明を読んでいただければ十分です
- S,R,E \subseteq \Sigma_E^*について
- 予備的な実験をやってきたが、結局本番の実験は何をするか決めたい
- 何をすれば良いというのは論文に載っけるRQ,設定を何にするか?
- (Waga et al., CAV'23): https://link.springer.com/chapter/10.1007/978-3-031-37706-8_1
- https://arxiv.org/pdf/2305.17742
- 前話していたrelated workの記録をいただきたいです
- https://hackmd.io/@MasWag/HJvhmmxBC
- introの初稿を書き上げたい
- 入力が大きくてmutliple outputなオートマトンの学習をmotivateするためにはどう書けばいいでしょうか? motivating exampleを上げる以外に思いついていません
- HSCCのれい 物理情報システムは一般に数値列を
- 値に応じて出力or状態が変わる例(金額,温度)
- 本文も適宜直していっています
- Waga: 何を読めば良いかを確認したいです
- Appendixにある証明を読む
- Short-term goal (~1 week):
- 本格的な実験を始めたい
- introの初稿を書き上げたい
- Middle-term goal (~1 month):
- 論文を完成まで持っていく
## 2024-05-31
- 進捗あまりない
- 160States10SigmaEでもequivは10
- 160States5SigmaEでようやくequivが5から変わる
- ギアシフトのベンチマークを作成中
- upshiftに移る時とギアが上がる時で<と<=で違うがこれは仕様でいいんですよね?
- <,<=はスピードだけか?スロットルも?
- 上げる時下げる時ってdown_th = 閾値, up_th = 閾値でいいですよね?
- スロットルに最大値はありますか?
- Gear1とGear4は状態数3で良いですよね?Gear2,3は状態数5
- 実験のゴールが欲しいが…

## 次回

- 和賀: MATLAB/SimulinkにあるAutomatic transmissionのgear shiftのモデルが何とか使えそうに思います
- 多分色々な意味で我々が作れるほぼ最大の "realistic" exampleだと思います
- なお実質ムーアではある
- 内容: オートマチックトランスミッションで、ギアを変速すべきかどうかを判断する部位
- 具体的には[これ](https://jp.mathworks.com/help/stateflow/ug/simplify-stateflow-chart-using-the-duration-operator.html)です
- 入力: throttle, speed (両方とも数値)
- 出力: Gear1, Gear2, Gear3, Gear4
- 全体的な挙動: speedが閾値を2ステップ連続して越えたらギアを変更
- ギアを上下するので、上下2つの閾値がある
- 「2ステップ連続して」の部分は上手くオートマトンの状態でエンコード
- ちなみに「2ステップ」はデフォルトのパラメタで、変更可能ではある
- 閾値の計算が割と面倒だがギリギリ可能か?というレベル
- 閾値の計算: ギアとthrottleからテーブルを引いて計算
- テーブルは以下 (列はthrottle, gear1, 2, 3, 4)
- interp_up (ギアを上げる用の閾値)

                0     10    30   50    1000000
                25    10    30   50    1000000
                35    15    30   50    1000000
                50    23    41   60    1000000
                90    40    70   100    1000000
                100   40    70   100    1000000

- interp_down (ギアを下げる用の閾値)

                0     0    5   20    35
                5     0    5   20    35
                40    0    5   25    40
                50    0    5   30    50
                90    0    30  50    80
                100   0    30  50    80

- 本当は区分線形補間で計算している模様
- 例えばギア3でthrottle=70ならinterp_upは(60+100)/2=80
- が、今回は簡単のために区分定数補間で良いと思います
- 例えばギア3なら35と50の間でずっとinterp_upは50, 50と90の間はずっと60
- 諸々の見積もり
- 状態数: 4 × 2で済む?
- SigmaEFinal: 7 × 16 = 112か? 関係ないペアが上手く潰れてくれたりしたら嬉しいけれど、そうはならないですよね?
- throttle: 0, 5, 25, 35, 40, 50, 90
- 90と100は区別されない (ですよね?)
- speed: 0,5,10,15,20,23,25,30,35,40,41,50,60,70,80,100
- 1000000はもう状態が切り変わらないので無視
- ↑ の設定ならほぼ equivalence query 勝負になりそう
- 和賀: 実は温度制御システムも扱えそうではあるんですが、実質symbolic automatonなのと、coolerも追加してもかなりシンプルなのでちょっとrealisticと言うには心苦しい感じがします
- https://jp.mathworks.com/help/stateflow/ug/bang-bang-control-using-temporal-logic.html

## 2024-05-24
- とりあえず証明の清書 lemma34~theorem47
- 証明は一旦すべてappendix送りにして良いでしょうか?
- 本文とappendix送りにした定理やら証明やらを対応させる方法はありますか?
- その上でsketchを書いた方が良い定理は書きます
- randomgeneratorの実装の変更をしました
- procyonのcpuとかosとかってどこで確認できますか?
- `cat /proc/cpuinfo`
- `free -h`
- `cat /proc/meminfo`
- `cat /etc/os-release`
- とりあえず試しに実験を回してみた結果
- output queryは状態数に比例し、SigmaEの二乗に比例する感じ
- equivalence queryはSigmaEと同じ値になる
- runtimeは参考記録
- なんか途中で実験が止まってしまった。shellスクリプトの実行が止まっているかどうか確認するlinuxコマンドってありますか?
- 恐らくsshで接続している通信が途中で切れている
- GNU screenを使って、実験を始めた後でdetachする
- https://ja.wikipedia.org/wiki/GNU_Screen
- nohupとかを使う
- https://atmarkit.itmedia.co.jp/ait/articles/1708/24/news022.html
- RQってこれでよかったのか?
- runtimeってequivalence queryの難しさにかなり依存していると思われるが良いか
- RQ2も同じようなスクリプトでよかったですか?
- 本文に本格的に取り組みたい
- とりあえず本文とintroの初稿を書くつもり、related workは最後でいいでしょうか?
- active automata learningのbenchmark論文@TACAS'24: https://link.springer.com/chapter/10.1007/978-3-031-57249-4_6
- 実装など https://gitlab.science.ru.nl/sws/lsharp/-/tree/testingstrategy
- 見ていた論文: https://www.sciencedirect.com/science/article/pii/S016764232100071X
## 2024-05-17
- ちゃんとできているかどうかはともかくとして、lemma34~theorem47まで青い本を参考に英語で清書しました。
- 読んでいただきたいです
- 帰納法の定型句はこれで良い?

## 2024-05-15

- 現状
- 証明は基本的に終わった
- 実験
- 実験周り
- Equivalence queryの回数は目視でもある程度状況がわかる
- Membership queryはplotしないとわからない
- とりあえずprocyonで実験を回して、様子を見る
- 最終的に実験を回すときは、ちゃんと事前にslackなどで排他的に使えるように工夫する
- 主にクエリの回数に興味があるので、繰り返しはなしで良い
- random生成は多くやった方が良いが、とりあえず 10-20 くらいか
- とりあえず全設定で実験を回してみて、そこから生成数を増やすと良さそう
- ランダム生成の組み合わせ
- 状態数 10 20 30 40
- Sigma_E 10 20 40 80
- 実装上使えるBoolean algebraは?
- Interval of
- integer
- character
- rational
- Equality algebra of
- integer
- character
- BDD algebra
- ↑ のProduct
- 今日の結論: 無理して使うというより、"Practical"なベンチマークの一部として使うのが良いのではないでしょうか
- "Practical"なベンチマークについて
- Q. そもそも動くのか?Black-boxなシステムを扱う必要はあるか?
- A. white-boxなシステムを扱うことにするので十分だと思います
- こうするとramdonな場合と同じようなequivalence oracleが使える
- 理由: Black-box systemに対して上手いequivalence testは何か?というのは今回の研究の範囲外だしそれ自体が十分非自明な研究として成立する
- Q. どうやって作るか?
- Fritzの研究から取ってくると、通信プロトコルとかが多い
- → 離散的であまり今回の旨味はない
- Etienneさんが扱っていたプログラムの例は?
- https://arxiv.org/pdf/2206.05438 が論文
- https://www.imitator.fr/data/ATVA19/ がベンチマーク一覧
- https://github.com/Apogee-Research/STAC/blob/master/Canonical_Examples/Source/Category1_vulnerable.java
- → どうやらパスワードと入力された数値の比較が主な内容。あまり我々がやりたいこととは関係なさそう?
- 今日の結論: practicalなbenchmarkでの実験はボーナスステージということにして、当面はそれ以外に注力する
- Writingについて
- そもそもの話: 論文として十分な品質の文書を書くのは (誰にとっても) 難しい
- 難しさ 1: 科学文書としての作法というか明確さは生まれながらにしてできるものではなく、十分な訓練を必要とする
- 難しさ 2: しかも英語で書かないといけないので、我々 non-native English user には難しい
- なので、ここからかなり赤の付いた原稿を返すことがあると思いますが、まあそういうものだと思ってください
- 定義・定理・証明
- 前提: この部分はほぼ定型みたいな書き方がある
- → 書きやすいはず
- 一度青い本を見ながら、できるだけあの本にある表現になるように通読しながら直していってみてください
- 和賀が読んだ方が良い部分を随時教えてください
- Introduction
- 前提: この部分は書き方の自由度が高いので、難易度も高い
- とはいえ、少なくとも初稿は書いてみてください
- 実験
- 前提: この部分も実はほぼ定型みたいな書き方があるので書きやすい
- が、そもそも実験がまだ全部は回っていないので、後回し
- 但し、ベンチマークの説明とかは書ける
- https://arxiv.org/abs/2305.17742 とかを見ると良いかも?

## 2024-05-10
- 状態数が増えることの証明を書きました(一部怪しいけど)
- evidence-closeはSigmaEだとLemma45が成り立たないかも?(それはそうとSigmaEにするとクエリの数は(当たり前だけど)減るなと実装を変えて動かしてみて思いました)ただL*にevidence-closeなんて存在しないので、多分回避できるはず
- シェルスクリプトを書いてみた
- 実験の設定について相談
- random生成なので到達不能な状態が生成されて、指定した状態数よりも小さくなることがあるがこれで良いのか
- どういう実験を回すと良さそうか?
- 繰り返しは少なくて良い5回くらいで良い(?)
- 時間がありそうなら追加で実験を回すか
- random生成は多くやった方が良いが、とりあえず5~10くらいか
- とりあえず全設定で実験を回してみて、そこから生成数を増やすと良さそう
- 状態数 10 20 30 40
- Sigma_E 10 20 40 80
- RQの案
- Equivalence queryの回数がちゃんと理論通り小さいか
- Evidence Mealy machineのalphabet sizeはtargetからわかるので、それでちゃんと抑えられるか
- Membership queryの回数の理論的なboundと実際にどうなるかの比較
- (上の二つに共通して) 最悪ケースと比べて平均的にどれくらいのquery数が要求されるか
- Practicalなcase study?
- 通信protocolとかだとsymbolic automataではなくregister automataとかの方が多い
- L* for Mealyで学習できるものは、提案手法でも学習できるはず
- L* for Mealy で学習できるpractical exampleをsymbolic Mealyで学習することによって、どれくらいコストが減るか
- アルファベットが無限なので、L* for Mealyでは学習できないベンチマークもあるとより良い
- 但し通信プロトコルのことをある程度わかっていないとそういうベンチマークは作れない
- どのくらいの大きさのSymbolic Mealy automataなら現実的な時間で学習が可能か
- 複雑さの異なるsymbolic Mealy automataで色々学習してみる → 「これくらいならtimeoutまでに学習できた」と言う + query数も報告
## 2024-04-19

- 和賀: AAAR論文のabstraction refinementの理解がかなり進みました
- 無限アルファベットを入力として扱うことのできるMealyの学習アルゴリズムとしては関係あるし、refinementを行っているという点でSigma*よりは近いが、今回の論文とは十分な差分がある
- この論文ではabstraction refinementの方法を固定して議論している
- どんなdomainにも適用可能ではありそう
- このabstraction refinementをpartitioning functionとして書くのは型が違うので不適
- そもそもautomata learningのcounterexample (i.e. concrete alphabet上の文字列) を使ってabstraction refinementをやっている
- cf. partitining functionはconcrete alphabetの集合の有限列 (というかリスト) のみを受け取る
- 一方ここで出てくるabstract alphabetを含むようなBoolean algebraは存在する模様
- Handwritten Note: https://drive.google.com/file/d/1ubOnLazDmSHZTur98CQPPsiAKjjgVVCE/view?usp=sharing

## 2024-04-18
- 聞きたいこと
- Mealyのoutput equivalenceの書き方
- followsの定義の相談
## 2024-04-12
- Preliminaries
- オートマトンの記号
- ミーリオートマトンの意味論の書き方
- relationで定義している　これはpartitioning functionをapplyするときに書きやすいから
- 一方で証明の時は関数記法を使いたい
- deterministic complete の統一
- generatorの厳密な定義
- リストの型はこれで良いか
## 2024-04-05
- ipadを返却したいです
- 論文のminimality証明の構成を変えたい
- 今現在の構成は同じ出力のものの中で最小
- compatibleの中で最小という感じにしたい
- Symbolic Finite Transducerとの比較
- 和賀: s-FTの特殊ケースとしてpreliminariesにsymbolic Mealy automatonを定義するのはどうでしょうか?
- Q. Minimalityの定義はどこに置くか?
- 具体的な定義がどこかの文献になくても、まあ皆普通に思いつくくらいの(i.e. folklore としてはある)定義ならPreliminariessに置いて良いです
1. In this paper, we study symbolic Mealy automata, which is a special case of \emph{symbolic finite transducers}~\cite{??}.
2. Def N. symbolic Mealy automatonの定義
3. (地の文) The miniality of symbolic Mealy automata is defined as follows.
4. Def N=+1. minimalityの定義
- これが今回の貢献だ、というつもりならLearning algorithmのsectionの冒頭に定義を置くのも可能です
- 共通点
- Boolean algebraを使う: https://pages.cs.wisc.edu/~loris/papers/cav17-tutorial とか
- 出力がある
- 異なる点
- 出力が一文字のみか否か
- 入出力のドメインが異なっても良いかどうか
- 但しこの違いはそんなに本質的ではなさそう
- 終了状態があるかどうか
- Preliminariesの構成(案)
- automata and Mealy automata
- 但し ↓ のsubsectionとまとめるのが良さそう
- Symbolic finite automata and symbolic Mealy automata
- The Λ* algorithm for learning symbolic finite automata
- Learnability of predicates

## 2024-03-29
- 富士通の内々定が出ました 最後sony(厳密にはsie)だけ記念受験して終わります。面接はあと高々1回だけです。
- 停止性のちゃんとした証明を書いています。(まだちゃんと書ききれてない)
- 証明の流れについて説明します
- 相談したいところ
- texの場合分けってどう書いたらいいんでしょうか
- output-closeとevidence-close停止性
- \Sigma_Eが増えるところの停止性
- 適宜preliminariesを書いています
- 通常のmealyはmealy automatonと呼ぼうと思っていますがいいでしょうか? evidence mealy automatonも同様です
- 定義のaとtheの違い
- genertorの節ってどの程度書けばいいでしょうか
- generator、s_g learnabilityの定義を書くのは確定
- learning classとか書くべきか
## 2024-03-21
- 明日最終面接なのでこれが通れば就活は終わりで研究に専念できると思います。(落ちたらもうちょっと続く)
- procyonでちょっとだけ動かしてみた結果
- 状態数:37 Sigma_E:77
- equiv: 75,output: 245997,run time: 6244654 ms

- どういう実験を回すと良さそうか?
- 繰り返しは少なくて良い5回くらいで良い(?)
- 時間がありそうなら追加で実験を回すか
- random生成は多くやった方が良いが、とりあえず5~10くらいか
- とりあえず全設定で実験を回してみて、そこから生成数を増やすと良さそう
- 状態数 10 20 30 40
- Sigma_E 10 20 40 80
- 和賀: 実験をAWSとかクラウドで並列で回したいかもしれないので、自動化を進めるのが当面良さそう
- 多分こういうスクリプトがあると良さそう
- 入力: 状態数、Sigma_E、(生成数)、繰り返し回数
- 重要なこと: 過去の実験ログを間違って上書き保存してしまわないように名前をちゃんと分ける + 名前から何の実験をやったかが判別できるようにする
- やること:
- 1. 適切にsymbolic mealyを自動生成
- ファイル名を見るだけでどういう設定でいつ生成したのかがわかるようにしたい
- 例: random-40-80-2024-03-21-12-00-00.java とか
- ここでもディレクトリを切っても良い
- random-40-80/2024-03-21-12-00-00.java とか
- 2. 適切にコンパイル: mvnを動かすだけ
- 3. 指定された回数だけ繰り返し実行
- 重要なこと: ログの名前も.javaと同様に重複させないように工夫
- 安直にはSymbolic Mealyのファイル名と実行時刻を繋げるだけ
- random-40-80-2024-03-21-12-00-00-2024-03-22-13-00-00.log とか
- ディレクトリを切る方が見やすいかも
- random-40-80-2024-03-21-12-00-00/2024-03-22-13-00-00.log とか
- 参考: https://github.com/MasWag/ProbBBC-experiments/blob/master/scripts/run-random_grid_world.sh

## 2024-03-14

- The Complexity of Satisfiability Checking for Symbolic Finite Automata
- https://arxiv.org/abs/2307.00151
- Demriのスライド: http://www.lsv.fr/~demri/slides-lecture3-mpri2015.pdf
- 適当に見つけた論文
- https://arxiv.org/abs/2311.03901
- Waga: Presburger算術の載ったsymbolic automatonの学習は面白そうですが、その前にPresburger算術自体の(active?) learningがどれくらい研究されているかを調べると良いと思います。Presburger算術の学習自体もそれなりに難しいかつ面白そうに思います

## 2024-2-23
- Progress after last meeting:
- procyonで~
- 雑談(時間があれば聞きたい)
- ksuenaga
5日前
@Masaki Waga
LTL3のためのオートマトン学習を作れば、データからLTL式を学習する手法作れないかな
Masaki Waga
5日前
LTL式を学習したい動機はよくわからないですが、(前にも同じことを言った記憶はありますが)LTLやFO[<]が認識するstar-free languageを学習したいのであれば、Nerode's congruenceが使えないので結構しっかり理論的な基盤を作る必要があると思います
## 2024-2-16
- 就活と重なっていてなかなか進まない
- Progress after last meeting:
- Automata Wiki
- https://link.springer.com/chapter/10.1007/978-3-642-18275-4_19 Howar et al. Automata Learning with Automated Alphabet Abstraction Refinement
- https://link-springer-com.kyoto-u.idm.oclc.org/chapter/10.1007/978-3-642-32759-9_4 Aarts et al. Automata Learning through Counterexample Guided Abstraction Refinement
- をざっと読んだ。Abstractionとは大きい入力アルファベットを小さい入力アルファベットにmapすること。元々人力でやってたけど、自動でやるぞというのが上二つのやっていること。
- Q. この論文との差分は何か?
- learnabilityの議論
- 遷移をmergeするかどうか
- 実装・実験
- 出力関数も上手く推論することで、Transducerへの拡張をやるという方向性もあるが、やったとしてもやや中途半端になるので、今回はやらない予定
- 下の方は無限状態を扱うextended finite state machineを対象にAutomated Abstractionしているので、benchmarkは使えない。
- https://link.springer.com/chapter/10.1007/978-3-642-18275-4_19 Howar et al. Automata Learning with Automated Alphabet Abstraction Refinement は我々の仕事と比較するなら、我々はMealy automata learningとparitining functionを使ったequivalence queryを通じた述語の学習をしているのに対して、HowarらはMealy automata learningと提案されたrefinement手法を使ったequivalence queryを通じた入力アルファベットのabstractionの学習をしている
- そういう意味で我々の仕事に相当近い
- Howarらの論文のexample runは我々の手法でも学習できそうであるのでpractical caseをやるのであればこれは使えそう
- Howarらのeqの計算量解析は我々と一致するが停止性をどう保証しているのかざっと読んだだけではよく分からなかった。(我々のs_g learnanbilityみたいな仮定がどこかにあるはずだが…)
- RQはここら辺が良いかなと考えています
- Equivalence queryの回数がちゃんと理論通り小さいか
- Evidence Mealy machineのalphabet sizeはtargetからわかるので、それでちゃんと抑えられるか
- Membership queryの回数の理論的なboundと実際にどうなるかの比較
- (上の二つに共通して) 最悪ケースと比べて平均的にどれくらいのquery数が要求されるか
- どのくらいの大きさのSymbolic Mealy automataなら現実的な時間で学習が可能か
- 複雑さの異なるsymbolic Mealy automataで色々学習してみる → 「これくらいならtimeoutまでに学習できた」と言う + query数も報告
- 具体的にどのBoolean algebraでbenchmarkの個数は幾つでみたいなのを詰めたい
- 繰り返しは少なくて良い5~10回で良い
- random生成は多くやった方が良い30~50
- 小さいものからやる　状態数5
- 状態数 100 200 300
- dnf-size 100 200 300(50 100 150)
- 実験はいつまでに終わらせればよいか? atvaの提出は4/19
- procyonなど、自分のマシン以外で実験を回すと良いです
- abstractとintroの構成を考え始めています。構成の段階から見せた方が良いですか? 最後の方にかく
- 本文は全てmealy automatonで統一したいと思っているがそれで良いか?
- 和賀: そろそろ本格的に writing をやるぞ、という状況なったらコメントがあります
- おすすめの書く順序: preliminaries, method, experiment → introduction, related work, conclusions → abstract
- introduction, related work, conclusions → abstract はそんなに時期的な違いはないかもしれないが、introを書く前に中身がある程度固まっていて欲しい
- introには貢献の概要とかを書くが、それを書くためにはfull versionの貢献がある程度ちゃんと固まってからが書きやすい
- grammarlyとか
- spell checker: ispellとかが有名 (https://texwiki.texjp.org/?Ispell)
- 対話的にspell checkができる
- grammarlyとかbrowser組み込みのスペルチェッカも良いが、たまに見過しがあるので最後の方に書けると良いです
- 最終的にはpdflatexで組む
- algorithm2eがおすすめですが、どっちでも良い
## 2024-2-9
- Progress after last meeting:
- returns lexicographically minimal counterexamplesの実装
- いいアルゴリズムが考えつかず効率の良い実装にはならなかった
- productをとって出現する全ての出力の食い違っている遷移までの最短経路を求めて、その中で最もlexicographically minimalなものを求めるというアルゴリズムにしている
- 和賀: 実験設定について確認したい
- RQの立て方とか何に答えるか、とか
- RQの案
- Equivalence queryの回数がちゃんと理論通り小さいか
- Evidence Mealy machineのalphabet sizeはtargetからわかるので、それでちゃんと抑えられるか
- Membership queryの回数の理論的なboundと実際にどうなるかの比較
- (上の二つに共通して) 最悪ケースと比べて平均的にどれくらいのquery数が要求されるか
- Practicalなcase study?
- 通信protocolとかだとsymbolic automataではなくregister automataとかの方が多い
- L* for Mealyで学習できるものは、提案手法でも学習できるはず
- L* for Mealy で学習できるpractical exampleをsymbolic Mealyで学習することによって、どれくらいコストが減るか
- アルファベットが無限なので、L* for Mealyでは学習できないベンチマークもあるとより良い
- 但し通信プロトコルのことをある程度わかっていないとそういうベンチマークは作れない
- どのくらいの大きさのSymbolic Mealy automataなら現実的な時間で学習が可能か
- 複雑さの異なるsymbolic Mealy automataで色々学習してみる → 「これくらいならtimeoutまでに学習できた」と言う + query数も報告
- 実装したBoolean algebraは?
- lexicography minimalは数値のintervalのみ
- そうでないなら
- 文字と数値のinterval
- BDD
- equivalence
- ↑ の直積
- 現実的な例を求めてAutomata Wikiを眺める
- https://automata.cs.ru.nl/BenchmarkCircuits/Description は入力alphabetがBDDとかで潰せるかも
- https://automata.cs.ru.nl/BenchmarkESMcontroller-SmeenkEtAl2015/Description は数値っぽい情報が遷移に載っている
- https://link.springer.com/chapter/10.1007/978-3-642-18275-4_19 Howar
- https://automata.cs.ru.nl/BenchmarkFromRhapsodyToDezyne-SchutsEtAl2018/Description はもしかすると数値が元なのかもしれないが不明

## 2024-2-2
- Progress after last meeting:
- 期末+就活で研究にあまり手が回ってません。すみません
- Preliminariesの先行研究って改変していいものなのか?
- 山本先生の授業で紹介されていた研究分野
- https://flann.super.site/resources
- https://aclanthology.org/2022.tacl-1.46/
## 2024-1-12
- Progress after last meeting:
- 通常のMealy machineにdeterminize やmake competeって定義されますか?
- Symbolic Mealy のMinimization algorithm
- 入力のMealyがdeterministic かつcompleteであることを仮定
- normalized + remove unreachable stateをする
- $D: Q \times Q$を区別された対の集合とする。
- Dの初期化は任意の状態p,qに対して、ある１文字を入れた時の出力が異なるとき,$(p,q),(q,p) \in D$とする
- 以下のようにDに要素を追加していく $(p',\varphi,p,a),(q',\psi,q,a')$の遷移があり、かつ$[\varphi \land \psi] \neq \emptyset$([]はdenotation function)であり、かつ$(p,q) \in D$のとき、$(p',q') \in D$とする
- 上の動作が停止した時、Dに入っていない対がつぶすべき状態
- Minimization of symbolic automataのbased on Moore algorithmを参考にしています
- based on Hopcroft algorithmもあってそっちの方が性能が良いっぽいけど、複雑なので今回は実装しない
- generatorの一回の挙動に何を含めるか generatorは挙動がabstractすぎて一回の挙動で何をするのか捉え方が色々ある generatorを我々の論文で説明するときに困る
- Drews et al.の本文を読む限り、generatorは反例が返ってきて、observation tableをcohesiveにした後の入力のリストの変化を一回の挙動にしているように読める(ただし、初期化は除く)。
- 2つの捉え方がある
- 1 generatorは反例が返ってきて、observation tableをcohesiveにした後の入力のリストの変化がgeneratorの1回の挙動 ただ、初期化だけは違う動作をおこすので注意
- 2 generatorはリストを何かしら更新した場合を1回の挙動
- 1の方がよさそう。Drews et al.のgeneratorにかかっている条件はよくできているのでこれをわざわざ変更しなくてもよい
- generatorは正解に到達したからといって停止するわけではない
- l_gの導入と証明すべき定理を決めました。これで最後まで行く予定です。
- 書く研究結果がほぼ決まってきたので論文を書き始めたい
- JSSSTのやつから大幅に本文を書き直す予定です
- ## 2024-1-5
- Progress after last meeting:
- 実験の内容
- Boolean algebraは1次元のintervalだけか? それとも? 多次元のintervalとかequality algebraとかもやる?
- oracleの実装について
- 多次元になった時lexicographically minimalはどう決まる?
- そもそもlexicographically minimalは条件として強くて、intervalの端っこを当てられれば、C\exists sizeになるのでは?(わからん)
- \Lambda*の実装は別にreturns lexicographically minimal counterexamplesでは(多分)なさそう
- 実装は(0,\infty)のinterval algebraに限りreturns lexicographically minimal counterexamplesにする方針 実装中です　
- (-\infty,\infty)のinterval algebraはそもそもlexicographically minimalが定義されるんだろうか?
- random生成のやり方
- random generateで設定する必要があるパラメータ
- Boolean algebra
- 状態数
- DNF-size(interval algebraの時のみ)
- 出力アルファベット(これは学習には特に影響しない、出力アルファベットが小さいとminimizationで状態数がちいさくなることが多くなるが、学習前にminimizationをかける予定なので問題ない)
- 先にありうる述語を生成して、それを各状態に割り当てる
- 各状態についてrandomに述語を生成する とりあえずこっちにした
- 出力アルファベットもrandom生成の方が良いか?
- teacherとtable manipulationの定義　
- 言いたいこと oracleが十分賢かったら学習は停止する
- 停止性をいうだけだったらgeneratorで良い気もする
- ただし\Lambda*よりも厳密な定義と正確な説明をつける
- equivalence queryは多めに見積もっていることを明示的に書く
- ただgeneratorはoracle以外の動作も入っているから、やっぱりイマイチかもしれない
- 計算量を厳密にboundするならteacherとtable manipulationに分けたほうがよい
- generator
- 利点
- 登場人物の数が減るので、simple
- 欠点
- 潰れていて、何か気が進まない
- 元の論文の説明がしっかりしていなかったことにも起因
- (どちらかというとわかりやすさとかの問題)
- 潰れていて大雑把に見積もってしまう
- 具体的にこういう欠点はある?
- Σ sg によるboundは ΣEfinal による議論と比べて、主に足し算とunionの違いでちょっと悪化する
- ΣEfinal による議論は、結構直観に沿っていてわかりやすそう + oracleの賢さを表現できる
- → **sgによる議論はやめたい**
- Q. ΣEfinalによる議論をするのに、generatorでは不十分か?
- generatorでも多分できる
- (どちらかというと理論的な結果の問題)
- Teacher/Table manipulation
- 利点
- 色々分かれているので、細かい議論がしやすい
- Q. generatorではできないが、分割したお陰でできるようになった(or やりやすくなった)議論はあるか・ありそうか?
- ΣEfinal に関する議論が、こっちの方が簡潔になる
- 欠点
- 登場人物が増えるので複雑になる
- 就活を始めました
- 進捗が悪くなりそう
- 最悪6月終わりくらいまで?

## 2023-12-22
- Progress after last meeting:
- s_g learnabilityについて
- 純粋なteacherによるiterative processと比べて、余計なものが入ってくることによる学習のiterative processの挙動が変わることはあり得る(その意味でiterative processにおいてteacherはalgorithmに依存する
- 自分は実装を動かしていた中でこの印象が強い
- 例えばteacherがlexicographically size minimal counterexamples(maler mensの論文で導入されたOracleの条件)だったら,teacherはalgorithmには依存しないので和賀先生のこの前の定義とも一致するが
- \Lambda*ではこの時C\exists sizeに対応すると言っている。この論じ方ではいきなりoracleが出てくるので、ここを明確にteacherという形で述べることができるのは良いことである
- teacherもalgorithmも導入し、algorithmの挙動を制限する(条件をつける)方向で行きたい
- algorithmの挙動につく制限は?
- 本来筆者がやりたかったことって、Learning classを純粋にequivalence queryを用いた述語の推論のeqの計算量で分類することだったのではという気がしている
- 余計なものが入っていくることを想定しているんだろうか?
- Learning classをteacherで分類するというのはやっても良いかもしれない
- C\exists \sizeの例で出てきているlexicographically size minimal counterexamplesという条件は、generatorにかかる条件ではなく、teacherにかかる条件である
- teacherをうまく選べば、algorithm関係なく停止性、計算量が決定する
- ただ結局C\forallのクラスに属するなら、余計なものが入ってきても停止するというのはその通りである
- 実験に必要なもの
- minimization
- unreachable stateの除外(というかreachable stateの数え上げ)
- oracleの性質 lexicographically minimalなものを返すようにする これによってs_g、もっと言えば\Sigma_E finalがDNF-size of cになる。
- BFS+ 各次元についてDNFにする。それぞれの述語が充足可能にする。それぞれの述語から最小なものを取ってきて、さらに最小のものを取ってくる。
- 遷移 遷移 述語　出力のrandom生成
- 年明けぐらいにはできると思います
- 関数まで学習する枠組みを考えるのであれば、TTT basedのSFA Learningを使った方が良いと思います。述語と出力関数の学習にmqとeqを使った学習アルゴリズムが使えるのでより複雑な述語が学習できるはず。出力関数をうまくまとめるあるいは学習させるというのが難しそう、というか貢献になりそう。\Lambda*の枠組みだとeqとparitioning functionを使わないといけない制限がある。
## 2023-12-15
- Progress after last meeting:
- s_g learnabilityについて
- generatorにかかっている制約の割に、provide counterexampleと言っているのが自分の混乱の原因だと思っています
- generator自体は必ずcounter exampleを返さなければいけないみたいな制約がかかっていない
- 正解に到達した時に停止するとも言っていない。多分generatorにかかっている制約的に、domainが有限集合だと挙動が未定義でバグるのでは?
- generatorは反例も追加するし、Observation tableにかかっている制約+cohesiveを満たすために追加することも考えられる(というか現に筆者が$s\cdot a \in R$を満たすための動作をgeneratorの動作の例として言っている)
- だから\Lambda*は停止するとは言えているっぽい
- ただgenerators which, informally, provide a sequence of counterexamplesと言っている説明と整合性はないので混乱する
- s_g learnableで停止性は証明できるけど…
- 自分は generatorを二つに分けたいと思っています
- i) teacher(名前要検討): これはリストを受け取ったら必ず反例でリストを更新するもの(ただし正解に辿り着いた場合はtrueを返す or リストを更新しない) つまりちゃんとしたeq
- ii) algorithm(名前要検討): oracleに問いた時以外に追加する動作 つまりObservation tableにかかっている制約+cohesiveを満たすためにリストを更新する動作
- i),ii)を閉じ込めれば良いので、当然s_g learnabilityの良い性質(Learning class等)も再利用可能
- ランダム生成ってどういうコードを書けば良いでしょうか
- javaコードをprintするぐらいしか思いついてないです
- dotファイルを読み込む機能を作れば、ランダムなものをdot形式で保存しておいて、それを読み込むみたいなことができるけど、時間かかりすぎる
- evidence Mealy machineの呼び方をどうしましょうか evidence Mealy automaton?
- Short-term goal (~1 week):
- 実験用のコードを書く
- Middle-term goal (~1 month):
- 実験評価をする
- Long-term goal (~0.5 year):
- 論文を書く
## 2023-12-8
- Progress after last meeting:
- Symbolic Mealy machineの名前が被ってしまった https://link.springer.com/chapter/10.1007/978-3-642-16573-3_14 の論文でsymbolic mealy machineが定義されている　我々の考えているものとは違うはず
- Waga: 他にもありました。どれも状態としてlocationとvectorを使っているものなので、今回のものとは異なる
- https://user.it.uu.se/~bengt/Papers/Full/isola10-2.pdf
- https://inria.hal.science/hal-00647576/document
- Waga: 「symbolic Mealy machineのlearning論文」という点で判別不能になるので、別の名前にしましょう
- 先行研究のまとめを作っています
- symbolic Mealy automaton: https://ieeexplore.ieee.org/document/246314
- 一応出てくるが、これは一般名詞としてのsymbolicのように見えるので、カウントしなくて良さそう
- remarkを書く
- もう少し時間がかかりそう
- Waga: Σ*については、多分こういう比較で良いです
- 関連するformalismは学習している
- 但し遷移中の述語をqueryから学習せずに、学習対象のシステムの内部状態から取ってきている点が大きく異なる
- (書かなくても良いが) 述語を学習しないで済むので、実質L*と同じ
- Waga: "Sanitizer" との比較
- 入力の一般性という点では、今回の方が強い
- 今回のアルゴリズムでは出力が遷移のみに依存するが、これは入出力が任意にとれるからしょうがないっちゃしょうがない。遷移と入力に依存するような出力のための一般的な枠組みの構築はfuture work
- 空文字とかaccepting stateとかも一応ある
- Waga: "Back in black" との比較
- 遷移に載っている述語の一般性という点では、今回の方が強い
- Λ*のrelated workを参照
- output-closednessはL*-styleだと必要
- ランダム生成の実験用
- parameterは状態数nと\Sigma_Eの大きさ(遷移の複雑さ?)でよかったか?
- でてくるintervalの個数
- dnf-sizeという枠組みでのsize
- s_g learnabilityをどうしようか?
- Waga: こういう方針をおすすめします
- s_g learnability を一字一句再利用はしない
- そもそも s_g learnabilityの定義がΛ*の文脈でも "the definition" という程良いものではなさそう
- s_g learnability の技術的なアイディアを使って、今回のアルゴリズムにとって使いやすいものを作る
- 一方で s_g learnability の **ような** 概念を基に学習可能性や停止性・計算複雑性を議論するのは良さそう
- 作るというほどの大工事ではないかも
- 仮定を増やすとか
- ちなみに、改良後のs_g learnabilityは別の名前にしないと混乱するので、名前を適宜与えてください
- こういう一般化も将来的にはできるかもしれない、の図
- 

- Short-term goal (~1 week):
- 先行研究をまとめ終える
- Middle-term goal (~1 month):
- 実験評価をする
- Long-term goal (~0.5 year):
- 論文を書く

## 2023-12-1
- 入江
- Progress after last meeting:
- l_gのきちんとした定義の仕方
- Short-term goal (~1 week):
- 英語を書く
- Middle-term goal (~1 month):
- 実験評価をする
- Long-term goal (~0.5 year):
- 論文を書く
- l_gをきちっと英語で言いたい　とりあえず日本語で書いてみた
-
- Theorem2との結果の違いがちょっと怖い
- 遷移の数がn^2になるからというのは
- automata learningのequivalence queryには複数回の述語の等価性判定が含まれますよね?
- 実験について
- そもそもsymbolic automataの理論自体がUnicode上の正規表現のために発展してきたものっぽい
- なぜsymbolic mealy machineなる新しい有限状態機械を考えたのか?みたいな疑問はそっちの分野の人は当然疑問に思うはず
- symbolic automata learningをcpsの方に持ってくるというのはこの研究の意義として重要(多分introductionやrelated workにも書くと思う)
- ということで、何か実験でcpsやらのpracticalな例はやりたいと思っています
- minimalityって必要か?

## 2023-11-24
- 停止性の証明の問題点
- generator(オラクル)による追加とアルゴリズムによる追加が区別できていない
## 2023-8-4
- 今日で期末が終わったので、論文を急いで書きます
## 2023-7-26
- 入江
- effective boolean algebraの定義 recursive enumerableを入れた方が良い
- all states are reachableを明示的に導入しました
- ただcompleteとcleanが成り立てば結局all states are reachableは成り立つのでは?という気もする
- 実験のベンチマーク https://automata.cs.ru.nl/Overview で実験はできそう
- 問題点?
- dotファイル形式なので、読み込む機能がない
- 手で写してもまあいいかなという気にはなっている
- dotファイルを読み込む機能を作るのは結構手間ではある
- Learnlibとかにdotファイルを読み込む機能とかないんでしょうか?
- 和賀: graphvizのファイルを読みこむのは適当なライブラリを使うと実装が簡単かも (https://mvnrepository.com/artifact/guru.nidi/graphviz-java)
- どれも普通のMealy machineなので、Boolean algebraとしてはequity algebraを使うことになるので、L*と性能は変わらないor若干悪化することが見込まれる
- 要するに$\Sigma_E$に結局全てのアルファベットが追加されることになってしまうということです。そうするとL*と変わらない
- for all と$\forall$って統一したほうがいいですか?
- $\forall$に統一してしまいたいと思っている。
- Lemma2の主張を変更+Lemmaとしてdeterministicかつcompleteになることの証明を追加
- well-definedって結局何を主張しているのか?
- 実験的にconsistentをなくしたらどうなるのか考えた結果
- 遷移を$\delta_1(q,w)$ 出力を$\delta_2(q,w)$みたいにしてみました
- 本文をとにかく書かないといけないけど、色々手が一杯であんまり進んでない
- 8/10に間に合うのか
- Learnability以降(termination + complexity)はカットでも良いかなという気はしている できれば書きたいけど
- また別の機会に
- symbolic mealyを使ったblack-box-checkingってevidence mealyを使ったblack-box-checkingに結局帰着されるよなと思いました
- $a_1x_1 + a_2x_2 + \ldots + a_nx_n \leq b$みたいな述語もsymbolic automatonに載っけて、これも学習できるようにしたい
- $a_1x_1 + a_2x_2 + \ldots + a_nx_n \leq b$をうまくオートマトンに変換して、membershipとequivalece queryで学習できるようにすれば、MAT*の枠組みで学習できるのではないかと考えています
- learnabilityがInferring symbolic automataという論文の枠組みでどうなるのかは不明　というかあんまりInferring symbolic automataの議論を理解できてないというのもある
- なぜ多項式時間にそんなにこだわるのか?
## 2023-7-3
- 入江
- 実験について
- とりあえず出来上がったものを見せます
- ランダムに実験用のベンチマーク生成するみたいな話があったがそれはどうやったらいいかあんまりわかっていません
- automatarkはdotファイル?形式でsvpaとかは入っていいた
- dotファイルを読み込んでsymbolic mealyを作るみたいな機能はない
- symbolic mealyを学習するjavaコードを生成するみたいな感じ?
- all states are reachableにするのが結構難しい
- 無視してしまって、普通にsymbolic mealyのsizeを数えることはできるので、別に問題ないか
- どのくらいの数のベンチマークを評価すれば良いか
- 和賀: 10くらい?いくつ作っても「なぜ20ではなく10なのか」と言ってくる人はいるので、気を強く持つ必要がある
- 実験の流儀(?)的なものの確認
- みなさんどんな感じでデータを保存しているんでしょう
- 出力の方法とか(csv形式)
- JavaだったらcsvWriterでできるか
- 四十坊さんとかどうやっていたか気になる
- これらのことがまとまっているような参考書があれば教えてほしいです
- 和賀: 多分決まった流儀はない
- とはいえ、できるだけ多くの情報を残しておくことがコツ
- 後で必要なデータだけを抽出することはできる
- 再実験の方が面倒
- できる限りログは取っておく
- 実験をまわすスクリプトを作って、誰でも再現できるようにしておくと良いです
- 半年後の自分は別人
- 計測するもの output query equivalence query だけで良い?
- simulinkにつなげるのは多分jssstには間に合わないのでまた今度でいいでしょうか?(海外用の論文にはできればpracticalなケースとして載せたいとは思っている)
- 論文について
- 結構時間的にやばいかも
- やり残していること
- 本文を書く
- 実験
- mealyのsemanticsを変更したことや、$\Sigma_E$の明示的な導入に伴う証明の変更
- 期末試験と被ってるのがヤバイ、8/10が締め切りですが結構ギリギリになりそうです。
- minipage: https://atatat.hatenablog.com/entry/cloud_latex18_subcaption
- jdot (生成): https://github.com/gboersma/jdot
- dot4j (両方?): https://github.com/teverett/dot4j
- gnu time: [https://qiita.com/__Attsun__/items/ecc97134b3f60a647f8c](https://qiita.com/__Attsun__/items/ecc97134b3f60a647f8c)
## 2023-6-9
- 入江
- $l_g(c)$という概念を作りたい
- 停止性の証明の確認
- 何を言えば停止したと証明できたことになるのかあんまりわかってないと思うので確認(というか$L^*$とか$L^*_{i/o}$の停止性の証明がなんでこれで停止することの証明になっているのかがわかっていない気がする)
- Observation tableに対する操作close,make-consistentのloopが停止する(これはclose,consistentでdistinct valuse of row(s)が増えることと、row(s)がtargetの状態数nを超えない ことから言える)
- main loop(反例が返ってきて更新するloop)が停止する(これは、反例が返ってきて更新するたび、状態数が増えていき、targetの状態数nを超えることがないことから言える)
- この二つが言えればOK?
- Theorem2は$\Lambda*$のアルゴリズム関係ない?
- 実験は全く進んでない
- メールも書き進んでない
## 2023-3-17
- compatibility(consistency)の証明について
- Angluinの証明も、Nieseの証明も$\delta$の定義が2番目の引数の長さが2以上の場合の定義がなされてないように思う。
- $\delta(q_0,s)$は$\delta(…\delta(\delta(q_0,s_0),s_1)…),s_k)(s=s_0s_1…s_k)$と読み替えろということか
- とりあえずevidence mealyのcompatibilityの証明を書いてみたが、そもそも証明すべきstatementがこれでいいのかとか、英語で証明を書くのに慣れていないため舌足らずなところが多いので、ちょっと相談が必要そう。https://www.overleaf.com/3288234714bhbmfmycnqck
- minimalityの証明について
- これもevidence mealyのものを書いてみたはいいものの、そもそも証明すべきstatementがこれでいいのかとか、英語で証明を書くのに慣れていないため舌足らずなところが多いので、ちょっと相談が必要そう。
- 結局$\Lambda*$のTheorem2は全ての頂点間の述語の分割を考えているだけだった
## 2023-3-10

- 記号的ミーリ、ムーアのwhiteboxなequivalence-queryについて
- [[Veanes+. POPL'12]](https://www.doc.ic.ac.uk/~livshits/papers/pdf/popl12.pdf)よりsingle-valuedなsymbolic finite transducerの等価性判定は決定可能
- 記号的ミーリ、ムーアはその特殊な(?)場合であるから、等価性判定は決定可能
- アルゴリズムについて
- [[Veanes+. POPL'12]](https://www.doc.ic.ac.uk/~livshits/papers/pdf/popl12.pdf)のFigure3のアルゴリズムがそのまま使えるはず。記号的ミーリ、ムーアでは起きえない場合も場合わけしているので、もうちょっと簡略化できそう。多分、productをとって、ミーリの場合は全ての遷移に乗っている出力のpairが等しかったらtrue ムーアの場合は全ての状態に乗っている出力のpairが等しかったらtrue みたいな感じになると思っている。
- 反例をどうやって返すか
- 出力のpairが等しくない状態or遷移までの経路の入力を返せば良い
- 実装は進んでいない
- 記号的ミーリムーアの学習アルゴリズムにおけるcompatibility(consistency)の証明も必要
- $\forall s \in (S\cup R), \forall e \in E$
$suffix(Mに入力としてs\cdot eが与えられた時の出力, |e|) = f(s,e)$
- これは[[Niese]](https://d-nb.info/969717474/34)(p196~)の証明(型がぐちゃぐちゃで読みづらい)で、Lemma8.13の証明は出力関係のwell-definedがoutput-closedに依存するから注意が必要 Lemma8.14はそのままで、Lemma8.15の証明でoutput-closeの操作で、$E$に長さ1の要素が加わることに注意すれば、ほぼそのままうまくいくはず。(結局証明を正確に書き出さないといけない)
- 学習アルゴリズムが停止した時、出力される記号的ムーア、ミーリはminimal number of statesかどうかについて
- [[Niese]](https://d-nb.info/969717474/34)(p198~)の証明も型がぐちゃぐちゃで読みづらいがこれを参考にする。
- Lemma8.16(left totalとinjective)はそのままで大丈夫
- Corollary8.17もそのままで大丈夫
- Lemma8.18は$a\in A_I$がoutput-closedで追加されるものに変わる
- Theorem8.19は全くそのまま
- 結局証明を正確に書き出す必要がある
- 以下別のアプローチ(結局同じような話に帰着されそうと思ったので、考えなくて良いが、一応メモしておく)
- symbolic finite transducerのminimalについて述べた論文は調べた限りなさそう
- だから、minimalについて、定義する必要がある。(以下の定義は[[D’Antoni+, POPL'14]](https://pages.cs.wisc.edu/~loris/papers/popl14.pdf)と[Switching and Finite Automata Theory](https://potharajuvidyasagar.files.wordpress.com/2019/01/zvi-kohavi-niraj-k.-jha-switching-and-finite-automata-theory-cambridge-university-press-2010.pdf)の10章を参考にしました)
- The states $S_i$ and $S_j$ of machine M are said to be equivalent if and only if, for every possible input sequence, the same output sequence is produced regardless of whether $S_i$ or $S_j$ is the initial state.
- 記号的ムーア、ミーリがminimalであるとは以下の5つの条件を満たすことである。
- deterministicである
- completeである
- cleanである
- normalizedである
- $\forall p,q ∈ Q$($p = q$ $\Leftrightarrow$ $p$ and $q$ are equivalent)
- deterministic, complete, clean, normalizedは機械のconstructionから自明にわかる
- 問題は$\forall p,q ∈ Q$($p = q$ $\Leftrightarrow$ $p$ and $q$ are equivalent)を証明すること
- $\forall p,q ∈ Q$($p = q$ $\Rightarrow$ $p$ and $q$ are equivalent)は明らか
- $\forall p,q ∈ Q$($p$ and $q$ are equivalent$\Rightarrow$ $p = q$)は対偶$\forall p,q ∈ Q$($p \neq q$ $\Rightarrow$ $p$ and $q$ are not equivalent)を考えると、Observation Tableがreducedであることから、明らか
- よって出力される機械はminimalである。問題はminimalな機械はminimal number of statesか(この証明はminimalな機械より状態数が同じか小さい機械がisomorphicであることを示せばよさそう)
- correctness
- equivalence-oracleの設定から自明
- termination+Learnability
- 手をつけていない　あんまり$\Lambda *$とやることは変わらん気がしている　$\Lambda *$のTheorem2がなぜ成り立つのかProofを読みたいが、(ここからは一般的な質問)どういう風に探せばいいのか?
- 証明を書き出すには記号的ムーアミーリ、学習アルゴリズムを英語でformalに書き出した方が書きやすいかなと思っている。

## 今の論文が終わってから

- 和賀: Active automata learningのquery complexityのboundを求める方法で、別方針のものがあるらしいです (https://proceedings.mlr.press/v125/chase20a)
- 良くわかっていないですが、この方針だとcounterexampleの長さにqueryの回数が依存しないらしい(?)