Java Path Finder(JPF)のありかなど

　JPFについて、今後、ちょっと書こうとおもっているんだけど（あと、CSPについても）、その前に、
　まず、JPFのありかについて。

ここ
http://sourceforge.net/projects/javapathfinder/files/
の「Download　Now!!」をクリック。

ZIPファイルがダウンロードできるので、ダウンロードしたら、それを解凍。

javapathfinder-r1258とかいうフォルダの下に、bin,libができている。

・・・ここから先の設定は、インストールのときに書く。

---

　それよりも、これだけダウンロードしたのでは、LTL式が使えない。
　（活性や公平性を見たい時に使う）

　LTLをJPFにするには、LTLをBüchiオートマトンにいったん変換して、そいつをJPFで扱う。
　このとき、LTLからBüchiオートマトンにするのにLTL2Buchiっていうのがあるらしいんだけど、
　みつからなかった。

　で、この部分、それ以外でもやってくれるものがある。そいつが
jpf-ltfで、

ここ　http://bitbucket.org/nacuong/jpf-ltl/downloads

から、ダウンロードできる（ZIPファイルをダウンロード）
　

---

具体的なインストールは別の機会に・・・

「ガチャピンに続き、“サンリオの萌えキャラ”がVOCALOID化」とか

　Twitterで、気になったもの。
　idがその発言のID,screen_nameが発言した人で、下の行が発言内容

---

id:24717411962 　　 screen_name:slashplus
[タレ]北朝鮮のハック: 北朝鮮に木製「ステルス機」 レーダー感知せず、米が警告 光が金属より木や布を透過しやすいという性質を考えれば当たり前のような気がするが、それらがこの分野に用いられたという話を聞いた事がない。 # ... http://buzzup.com/1a8za

id:24709114026 　　 screen_name:slashplus
[J][nemui4] いつの間にかAndroidがカーナビになってた http://is.gd/fe6VT 昨日の帰り道、土砂降りの中駅から図書館に行こうとしてAndroidのマップを開いてルート検索しようとしたらナビの文字が出てきてた。タップしてみると

id:24701822758 　　 screen_name:slashplus
[J][KAMUI] とらのあなが同人サークルを訴えたらしい。 http://is.gd/fdNlc http://goo.gl/u2Ro 訴えられたのは『同人音楽制作ガイド』などの著書もある同人サークル「うんちく商事」の冨井公 氏で

id:24696493298 　　 screen_name:slashplus
[J][shitamo] Flash Player "Square" Preview Release http://is.gd/fdUrK 10.2の64bit版が出てきたのでさっそく入れてみた。ibusでも日本語入力ができるようになった。

id:24668375874 　　 screen_name:slashplus
[J][90] ウェアラブル垂れ流しカメラヘッドセット Looxcie、$199 http://is.gd/fdpXE http://goo.gl/PGCF 本体に5時間まで自動録画。ボタンを押すと30秒前からの映像を転送。記録はBluetoothでスマートフォンへ。

id:24667222801 　　 screen_name:slashplus
[J][L.Entis] 二足歩行バイク http://is.gd/fdpRd ガンダムへ！１００キロ運べる二足歩行ロボット http://goo.gl/T985

id:24666926478 　　 screen_name:slashplus
[J][uhyorin] hylom編集者がつぶやいた…PVが8月から落ちてます http://is.gd/fdpBJ hylom編集長編集者の呟きを転載。 http://twitter.com/hylom/status/23150592629

id:24656428039 　　 screen_name:slashplus
[タレ]将来的に携帯電話は人のムードも認識できるようになる?: Slashdotの記事によると、Intel社のCTO、Justin Rattnerは、サンフランシスコで開かれたIntelの定例年次会議において、近い将来、人... http://buzzup.com/1a6o1

id:24656427853 　　 screen_name:slashplus
[タレ]Momonga Linux 7 リリース: 2010年9月14日、Momonga Linux 7がリリースされた。2009年7月にリリースされた Momonga Linux 6 から約14ヶ月ぶりのメジャーアップデ... http://buzzup.com/1a6o0

id:24649855536 　　 screen_name:slashplus
[タレ]Intelの新CPU「Sandy Bridge」は超高速？: Intelが米サンフランシスコで開催しているイベント「IDF 2010」にて、来年にも登場すると見られている新CPUアーキテクチャ「Sandy B... http://tinyurl.com/243k39l

id:24646997889 　　 screen_name:slashplus
[タレ]左利きゲーマーは不利？: タッチペンがコントローラやジョイスティックの代わりとなりつつあるが、左利きゲーマーの存在があまりにも見過ごされているのではないかとの記事が本家/.に掲載されている。 examiner.co... http://buzzup.com/1a69c

id:24646997673 　　 screen_name:slashplus
[タレ]IE9ベータ版リリース: すでに各所で報道されているが、9月15日、Internet Explorer 9のベータ版がリリースされた。今までリリースされていたPlatform Preview版とは異なり、完全なUI... http://buzzup.com/1a69a

id:24643984729 　　 screen_name:slashplus
[タレ]Google、バグ発見者達に報奨金を支払う: Slashdotの記事によると、報奨金プログラム「Bug Bounty Program」でセキュリティーの脆弱性改善が本格化しているGoogleから、Chromeの新バ... http://buzzup.com/1a639

id:24723535805 　　 screen_name:yukatan
VOCALOIDってオープンで多様でおもしろいねぇ　RT @itmedia_news: ガチャピンに続き、“サンリオの萌えキャラ”がVOCALOID化　^IT戦士　http://bit.ly/aV2Yhx

id:24655485776 　　 screen_name:yukatan
ひろゆき氏と勝間さんが同じぐらい早口であることに気付く http://nico.ms/lv26140520 #niconama_talk

id:24655372188 　　 screen_name:yukatan
勝間堀江ひろゆき対談がいい感じにｇｄｇｄ（ほめてる） http://nico.ms/lv26140520 #niconama_talk

id:24647314700 　　 screen_name:yukatan
なんと、ニコ動用語は私がしってるネット用語とだいぶ違うっぽい！凸は「ニコニコ動画では、「額の広い娘さん＝おで娘」の意味合いで用いられている」　http://dic.nicovideo.jp/a/凸

id:24647215726 　　 screen_name:yukatan
ニコ生用語のQAで、「僕は結構ツウですよ♪」と言いつつ「うｐ＝萌えー、かわいかったー」と説明。惜しい感じ。いやしかし、気持ち的には間違ってないかも　http://ow.ly/2F4Mi

id:24656552109 　　 screen_name:yamataka
そんなにいい音ではないかもしれないが、アプリの幅が広がるのは間違いない。 RT: "SilverlightにSRSのサラウンド技術を導入 - ITmedia News" http://bit.ly/dp1F7X

id:24656363222 　　 screen_name:yamataka
64ビット対応はうれしい RT: "Adobe、IE9と64ビットOS対応のFlash Player“Square”をプレビューリリース - ITmedia News" http://bit.ly/9SxX61

id:24722473444 　　 screen_name:topitmedia
Smarter Retailing Forumインタビュー・マイクロソフト編：「さらなるユーザー企業の参加が重要」──Smarter Retailing Forumとマイクロソフトの流通IT標準化活動 http://ow.ly/2FA2E

id:24711734873 　　 screen_name:topitmedia
未来の「Smart Connected City」：韓国政府も積極姿勢、仁川で見た未来都市の姿【後編】 http://ow.ly/2FxQU

id:24711718356 　　 screen_name:topitmedia
Twitterアプリのデモも：Microsoft、「Windows Phone Developer Tools」の最終版を公開 http://ow.ly/2FxRI

id:24724011691 　　 screen_name:ibucho
本日18:00に参加応募を締め切りますです。RT @ibucho: 第四回 ライブドア・テクニカルセミナーのお知らせ http://bit.ly/cMmES3

電子政府を体験してみる－その１－４ 電子申請・届出システム 驚愕の新事実

　電子政府とやらが、どんな感じなんだか・・・っていうのを、実体験してみないとわからないので、実際に使ってみたという、「電子政府を体験してみる」。

　今、「総務省　電波利用　電子申請・届出システム Lite」で、アマチュア無線局の設置場所の変更（＝住所変更）をしようとしている。これには、以下の手順

　（１）ユーザー登録する
　（２）変更する
　（３）返信用封筒を送る
　（４）新しい免許状が来たら、古い免許状を返す

が必要で、
　　前前回、「（２）変更する」で、変更届を出したはずなのに・・・
　　前回、検索してみたら・・・ない、届けが出ていない・・・

　なーぜー（；＿；）・・・

---

■驚愕の新事実！

　で、

「総務省　電波利用　電子申請・届出システム Lite」
http://www.denpa.soumu.go.jp/public2/list/index.html

　の操作手順をみて、なにか、おかしなことしたか、確認した。

　確認したら・・・驚愕の新事実！あれじゃ、終わっていない。

　ここをみると、「送信」ボタンを押したあとに、操作があるのだ。

　つまり、つまりですね、

前前回、送信ボタンをクリックして、
ログイン画面に戻ったから、これで、終わり！としてしまった。

　しかし、そこでは終わっていない。

　ここの「６．申請・届出内容の確認」の操作が終わっただけで、そのあと、ログイン画面がでるから、「７．申請・届出の送信 」の操作が必要なのだ！

つまり、

　ログイン画面に戻ったら、その画面から、ユーザーIDとパスワードを入れて、OKをクリックする。

　そうすると、問い合わせ番号が表示される。

　これで完了。

　この状態で、前回行った「照会」をすると、問い合わせ番号が表示されて、変更される。

---

■なんでこんなことに・・・

　そりゃーわかりませんわ。

　「送信」ボタン押して、メッセージダイアログでて、OKして、(エラーが出ずに）
　ログイン画面に戻ったら、送信できた！とおもうでしょ、普通・・・

　なぜもう一度、ログインさせる？？

　とおもいますよねえ。。。

　なんでこんなことに・・・

　たぶん、IPAの「安全なウェブサイトの作り方」が影響していると思う。
　チェックリストの「６　CSRF（クロスサイト・リクエスト・フォージェリ）」の

　根本的解決の２番目、

「処理を実行する直前のページで再度パスワードの入力を求め、実行ページでは、入力されたパスワードが正しい場合のみ処理を実行するようにする」


ここでさしているのは、証券会社やネットでの銀行振り込みで行う、第二暗証番号のこと、
つまり、ログインとのパスワードは変えている場合もおおいし、そもそも、ログイン画面に戻るわけではない。

でも、これを、文章そのまま実行しちゃったんですね、きっと。
そうすると、今回のように、ログイン画面にいったん戻って、パスワードということになる。
うーん、うーん、うーん・・・・

NECの「消費電力が見えるめがね」を作るとしたら・・・

　中央線のトレインチャンネルなんかで、NECが「消費電力の見えるめがね」の宣伝をしている。
　「こういうめがねはありませんが・・・」と宣伝ではなっていますが、あれをつくるとしたら・・・


＜＜CMを見ていない人に＞＞
　　ここのCM（リンク先、読み込み後、すぐ音声が出ます）
めがねをかけると、めがねから見えた電気製品（パソコンとかプリンタとか）が、
どれくらい電気を消費しているか、グラフ表示する。

---

・各電気機器のコンセントに、交流電流センサーをつける。
　(丸のところにコンセントを入れるのかしら？）

・電流がわかれば、X100Vで消費電力がわかるので、その結果を、
　Arduino Fio（旧：Funnel I/O）で処理して
　XBeeで各電気機器からPCへ無線でとばす。

・一方めがねのほうは、めがねの内側に一部電子ペーパーを貼ったり、
　エアスカウター（眼鏡型ディスプレイ）を入れる。
　めがねのどこかにカメラをつけて、めがねでどこを見ているかを明らかにさせる。
　この信号もパソコンに送る

・あとは、パソコン上で、

　　　カメラからの情報で、見ている場所を確定し

　　　そのなかに電子機器があるかどうかを判断し
　　　　　　電子機器が赤外線を発せさせれば、それを処理するだけだけど
　　　　　　画像だけからでも判断できそう

　　　その電子機器に対し、XBeeからきた消費電力をグラフ化して、

　　　電子ペーパーやエアスカウターに送る

　っていう感じかしら。

---

　うーん、それでも、めがねは大きくなっちゃうね。
　将来的にはできるって感じですかね・・・採算は合わないか・・・

　それよりも、あの宣伝に田中えみさんが出ていることのほうが重要？

Ubuntuを動かすために、Virtual Box入れたら、こんな画面が・・・

Windows上で、無料でUbuntuを動かすとすると、VMware Playerを使うか、VirtualBoxを使うかだけど、
(昔VMWare Playerでやったので）今回、VirtualBoxで作ろうと思ったわけ。

まずは、

Virtual Boxのダウンロードページ
http://www.virtualbox.org/wiki/Downloads

にいって、
「VirtualBox 3.2.8 for Windows hosts」の「x86/amd64」をクリックして、ダウンロード。
(いまだと）VirtualBox-3.2.8-64453-Win.exeがダウンロードできるので、実行すると、
まあ、Virtual Boxがインストールできるのはいいんだけど（SunがOracleにかわってるう・・）

途中、こんな画面が・・・



・・・うーん、まいくろそふとの嫌がらせ（＾＾；）？

---

ちなみに、このあと、Ubuntuの

VirtualBox用仮想マシンのダウンロード
http://www.ubuntulinux.jp/products/JA-Localized/virtualbox

の仮想マシン本体をクリックして、ダウンロード、

あとは、上記のページに書かれているように、Virtual boxを起動して「新規」をクリックして、
答えていけばいいんだけど、多少画面が変わってる。

OSタイプのところ


仮想ハードディスク

（もう、ubuntuインストールしちゃった後の画面なので、新規のときは、違った画面だったかも。
　既存のほうを選択した場合、横にあるフォルダアイコンをクリックすれば、ディスクが指定できる）

9月16日(木)のつぶやき

16:09 from web
クラウドはたぶん、中小零細はSaaSへ、大手はIaaSへいき、ミドルウエアをガンガン変えられて、構成管理が大変で、保守する必要があるPaaSは敬遠されていくんだろうな。結局、PaaSを入れたら、いくら儲かるのか？っていうことを、金額ベースで示せないのは痛い
by xmldtp on Twitter