（鍵エアリプ）
防護無線が仮にもし遠くで発報されて、回送のほうだけぎりぎり届いたとかだと、対策を考えるにもさらにややこしい話になりそう＞＜；
orange
さんがブースト
眉に唾を大量につけながら見てほしんだけど…もしこんな「そんなことあるゥ！？」なことが東急田園都市線梶が谷駅で起きてしまったとすれば…
すべて正常動作した状態で進路開通できてしまう…
orange
さんがブースト
決められた位置の手前で回送列車が停止か 田園都市線、再開見通せず（朝日新聞） - Yahoo!ニュース
https://news.yahoo.co.jp/articles/fcaf0ae8e1059e5e1d9c86589b66052e057378aa
"...回送列車は留置線に入る際、オーバーランを防止する信号が作動し、決められた停止位置より手前で止まった。見習い運転士はブレーキを解除して所定の位置まで進もうとしたが、衝突を避けるため周囲に異常を知らせる「防護無線」を受信したため、そのまま停止していた。..."
なんで防護無線が発報されてて各停側は走ってたの？＞＜；
orange
さんがブースト
なので、梶が谷駅の設備は本当に健全だったのか、という疑いが出てしまい、たとえ脱線した車両を撤去できたとしても、ちゃんと情報を集め切るまで再開はムリでは？というわけ。
orange
さんがブースト
腑に落ちないのは、ふつうは軌道回路（車両の存在を検知する回路）はこんな感じで分割して、そのうち問題の赤で示した部分に車輪が載っていた場合は、上本→3番の進路は構成できないようインターロックがかかっているはず、というので…
運転士が見習いだろうが、停止位置が間違ってようが、これが安全を担保するための原則のはずなのに、実際は赤の部分にまだ車両が居たのに3番への進路が開通してしまったという…
Rustばっかり流行って、Ada/SPARKみたいな形式検証環境が全然流行らないのが謎・・・＞＜
orange
さんがブースト
全部コンパイラに自動でやらせようとするから悪い プログラマが証明を書け！
orange
さんがブースト
もちろんこれは危険なメモリ操作を「自動で」検出しようと考えた場合なので、「プログラマが安全性の形式的証明を手動で書かない限り全て危険とみなす」なら可能だと思う
orange
さんがブースト
整数オーバーフローくらいなら……いやどうなんだろ、結局篩型みたいなの使う羽目になって SAT/SMT の計算量が嫌すぎる〜みたいな話になるか？
orange
さんがブースト
文脈わからないけど、たとえばチューリング完全な言語では無限ループがないことの証明はできない (停止性問題)
orange
さんがブースト
「どれだけコンパイラが賢くても、警告し切れないケースが存在する」ことは数学的に証明できそうな気がする
orange
さんがブースト
今の軌道回路の設計ってどうなってるんだろうねえ、分岐器のない本線上は無絶縁にして減衰考慮で設計っていう考えで合ってるとは思うんだけど、分岐器のある駅構内までそれやっちゃうとしっちゃかめっちゃかになるので、信用ならない技術使うのではなくて単純に絶縁してると思いたい…
トンネル出た直後あたりに気づいて決断できたらぎりぎり停まれる？＞＜；
ちょっと古い動画だけどどんな風に見えるのかの参考＞＜
31:56～
東急8590系前面展望 田園都市線各停 中央林間-押上 - YouTube
https://youtu.be/Nga0pLoSNSU?si=rNaJmjLs4MzRNCu2&t=1916
そもそも、ポイント周辺で車体が接触限界からはみ出てるかどうかって軌道回路で検出可能な範囲なの・・・？＞＜
今回の事故、運転士が目視可能な位置ではみ出てる事に気づいてもどっちにしても止まれない気がする＞＜
ていうか、CS-ATCの軌道回路の仕組み自体がいまいちよくわからない・・・＞＜
- ＠orange_in_space
2017年 4月に登録
