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ファイルをダウンロード）
　

---

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

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

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

　今、「総務省　電波利用　電子申請・届出システム 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インストールしちゃった後の画面なので、新規のときは、違った画面だったかも。
　既存のほうを選択した場合、横にあるフォルダアイコンをクリックすれば、ディスクが指定できる）