Hatena::ブログ(Diary)

yukobaのブログ このページをアンテナに追加 RSSフィード Twitter

2012年04月11日 AndroidでPOCO C++ Librariesの実行方法

AndroidでPOCO C++ Librariesの実行方法

http://pocoproject.org/ ですが、1.4.2 から Android 対応しているのですが、マニュアルドキュメント不足でいまいちわからなかったので、ここにメモしておきます。

ライブラリ自体のコンパイル方法

http://pocoproject.org/docs/99300-AndroidPlatformNotes.html どおりです。Ubuntu 12.04 (x64) でも MinGW でもどちらでもコンパイルできました。Ubuntu x64 の場合aptitude install ia32 する必要があります。

こんな感じで、my-android-toolchain を作って、

export NDK=$HOME/android-ndk-r7c
$NDK/build/tools/make-standalone-toolchain.sh --platform=android-8 --install-dir=$HOME/my-android-toolchain
export PATH=$HOME/my-android-toolchain/bin:$PATH

こんな感じでコンパイルできます。

cd poco-1.4.3p1
./configure --config=Android --no-samples --no-tests
make -s -j4
make -s -j4 ANDROID_ABI=armeabi-v7a

そして、--platform=android-8 を --arch=x86 に変え、ANDROID_ABI=x86 にすると、x86 Android でも動作します。エミュレータで高速に動作するようになります。

ndk-build との併用方法

この部分がドキュメント不足でした。

まず、Application.mk に

APP_STL      := gnustl_static

gnustl_static でも gnustl_shared でもどちらでも動作しますが、gnustl_shared の場合、Java 側から、System.loadLibrary("gnustl_shared"); する必要があります。

Android.mk に

LOCAL_CPP_FEATURES += exceptions rtti

を追加し、更に、

  • LOCAL_CFLAGS には -Ipoco-1.4.3p1/Foundation/include -Ipoco-1.4.3p1/Net/include -Ipoco-1.4.3p1/Xml/include -Ipoco-1.4.3p1/Util/include を追加します。
  • LOCAL_LDLIBS の先頭に、-Lpoco-1.4.3p1/lib/Android/armeabi-v7a -lPocoNet -lPocoXml -lPocoUtil -lPocoFoundation を追加します。
  • LOCAL_STATIC_LIBRARIES に、libgnustl_static を追加します。

poco-1.4.3p1 へのパスは適切に変えてください。exceptions rtti は動作させるのに必須です。それ故、APP_STL は gnustl を使わないとダメです。

NativeActivity を使っているのですが、AndroidManifest.xml は例えば、こんな感じにします。

<?xml version="1.0" encoding="utf-8"?>
<manifest xmlns:android="http://schemas.android.com/apk/res/android"
      package="com.example.hoge"
      android:versionCode="1"
      android:versionName="1.0">

    <uses-permission android:name="android.permission.INTERNET" />
    <uses-sdk android:minSdkVersion="10" />

    <application android:label="@string/app_name" android:hasCode="true" android:debuggable="true">
        <activity android:name="android.app.NativeActivity" android:label="@string/app_name">
            <meta-data android:name="android.app.lib_name" android:value="hoge" />
            <intent-filter>
                <action android:name="android.intent.action.MAIN" />
                <category android:name="android.intent.category.LAUNCHER" />
            </intent-filter>
        </activity>
    </application>
</manifest> 

HTTP 通信とか、StringTokenizer とかがちゃんと動作するところまで確認しました。

ただし、POCO の Thread.start() が Android NDK r7c + POCO 1.4.3p1 の組み合わせでは正常に動作しませんでした。原因不明。自分で Pthread を使う分には問題無いです。

(追記)最初にこのブログを書いた際、大幅に間違いを含んでいたので色々修正しました。

トラックバック - http://d.hatena.ne.jp/yukoba/20120411

2012年03月21日 SWT + JNA + Cairo

SWT + JNA + Cairo

Win32 ではこんな感じで出来ます。Cairo は http://www.gtk.org/download/win32.phpall-in-one bundle から入手するのがおすすめ

import com.sun.jna.Pointer;
import org.eclipse.swt.internal.win32.OS;
import org.eclipse.swt.widgets.Display;
import org.eclipse.swt.widgets.Shell;
import org.junit.Test;

public class SWTTest {
    @Test
    public void test() {
        Display display = new Display();
        Shell shell = new Shell(display);
        shell.setText("Shell");
        shell.setSize(200, 200);
        shell.open();

        int hWnd = shell.handle;
        int hdc = OS.GetDC(hWnd);
        try {
            Cairo cairo = Cairo.INSTANCE;
            Pointer surface = cairo.cairo_win32_surface_create(hdc);
            Pointer pattern = cairo.cairo_pattern_create_rgba(1, 0, 0, 0.1);
            Pointer cr = cairo.cairo_create(surface);
            cairo.cairo_set_source(cr, pattern);
            cairo.cairo_rectangle(cr, 0, 0, 100, 100);
            cairo.cairo_fill(cr);
            cairo.cairo_destroy(cr);
            cairo.cairo_pattern_destroy(pattern);
            cairo.cairo_surface_destroy(surface);
        } finally {
            OS.ReleaseDC(hWnd, hdc);
        }

        while (!shell.isDisposed()) {
            if (!display.readAndDispatch()) display.sleep();
        }
        display.dispose();
    }
}
import com.sun.jna.Library;
import com.sun.jna.Native;
import com.sun.jna.Pointer;

public interface Cairo extends Library {
    final Cairo INSTANCE = (Cairo) Native.loadLibrary("libcairo-2", Cairo.class);

    // cairo_t
    Pointer cairo_create(Pointer target);
    void cairo_destroy(Pointer cr);
    void cairo_set_source(Pointer cr, Pointer source);
    void cairo_fill(Pointer cr);
    void cairo_rectangle(Pointer cr, double x, double y, double width, double heigth);

    // pattern
    Pointer cairo_pattern_create_rgb(double red, double green, double blue);
    Pointer cairo_pattern_create_rgba(double red, double green, double blue, double alpha);
    void cairo_pattern_destroy(Pointer pattern);

    // Surface
    void cairo_surface_destroy(Pointer surface);

    // Win32
    Pointer cairo_win32_surface_create(int hdc);
}
トラックバック - http://d.hatena.ne.jp/yukoba/20120321

2012年03月15日 クラウドのベンチマーク、GMOクラウドの利用可能ポート

UnixBench dhry2reg (整数演算)の結果

サーバーdhry2reg
さくらのクラウド(1コア)2434.7
GMOクラウド(1コア KVM 深夜)3194.2
Core i5 ノートパソコン(2コア 2.4GHz)3216.5
さくらVPS (2コア 1GB)3607.1
Amazon EC2 m2.xlarge (2コア) 4312.2
名前.com VPS (3コア KVM)8712.0
さくらのクラウド12コア)29735.7
GMOクラウド(12コア KVM 深夜)37111.2
Amazon EC2 cc2.8xlarge(16コア 32スレッド38343.6

UnixBench 5.1.3 は最高16並列に制限されているので、Run の maxCopies を32に改変。

さくらのクラウドの数値は http://r2.ag/r612 より。中の人の計測。

新さくらのVPSは http://sakura.off-soft.net/blog/unixbench-new-sakura-vps.html より。Xeon E5645 2.40 GHzだそうです。お名前.com VPS は、おそらく Xeon X5675 3.06 GHz。

GMOクラウドやさくらのクラウドは時間帯の影響を受けるはずだと思います。空いている時間帯での調査です。

GMOクラウドの利用可能ポート

GMOクラウドは利用可能ポートに制限があります。TCP で使えるのは、以下のポート。この情報マニュアルには載っていません。要注意。Adobe Flash ソケット ポリシー サーバー (843) も閉じています。

20-22, 53, 80, 81, 110, 113, 119, 123, 143, 443, 444, 446-554, 587, 989, 990, 993, 995, 1024-65535

また、ICMP (ping) も使えません。

トラックバック - http://d.hatena.ne.jp/yukoba/20120315

2011年12月06日 Flashの未来をFLASH MEETUPで聞いてきた!

Flash未来をFLASH MEETUPで聞いてきた!

先ほどまで、FLASH MEETUP http://atnd.org/events/22297 があり、Adobe Flash の現状・未来についての質疑応答のイベントがありました。Flash の技術の偉い方のちゃんとわかっている人が3名アメリカから来ていて、超内容が濃かったです!7〜9時の予定が11時まで延長して、京都から来た方は泊まりこみになりました!

Flash 関係で、最近誤解を招いてしまったことについて解説があったのですが、まぁ、ネットではたくさん出ているので、Flash の今後について話していたことについてこの記事では書きます

あと、僕、間違ったことを書いていたらごめんなさい。私見も混じっています。アドビ太田禎一さん @ さんに聞くと色々と教えてくださると思います。

全体の方針

現状、Flash がよく使われているのは、「ゲーム」動画」「広告」なんですが、ゲームと動画に今後は注力していくとしていました。

Stage 3D

Flash Player 11.0 から入った GPU を呼び出せる Stage 3D ですが、方針としては、

  • 2D フレームワーク や 3D フレームワーク経由で使ってね。
    • 2D フレームワークは Starling などがあるのですが、(私見:3D 程は注目されていなく)ぜひぜひ使ってね、と言っていました。Angry Bird は Starling を使って書いた Flash 版を発表するそうです。
    • 2D でも結構フレームレート良くなるそうです
    • ソフトウェアレンダリングエンジンになってしまった場合でも、Flash 10.x の方式よりも速いそうです
  • Adobe 自前ではこれらのフレームワークを作ることはなく、その下のレイヤーだけに注力する。
  • 3D のオーサリングツールも作らない。Flare3D のオーサリングツールを紹介していました。

あと比較的高度な話として、

  • 11.0 では Pixel Bender 3D で for ループが出来なかったり、描画命令もすごく種類が少ないのは、広範にいろいろなコンピュータテストしてみたところ、あまりにもちゃんと動いてくれない GPU が多すぎて、その結果、こういう命令になった。GPU ベンダーバグ修正の要望を色々出している。
  • バグのある GPU は動作させないブラックリストを Flash Player は持っていて、統計的に 50% 近く弾いている。そのリストは今後公開予定。最新のドライバなら動く GPU でも、ドライバのバージョンが古かったりするとブラックリスト入りしている場合がある。最初のインキュベータ版では「2009年1月よりも前にリリースされたドライバ」を全て弾いていたそうです。
  • それでも、WebGL のブラックリストよりは広範囲のドライバをサポートしている。(例えば、WebGL の場合、第1世代 Core i の Intel HD Graphics ですらブラックリストに入っています)

モバイル関係としては、

  • モバイル Adobe AIR の Stage 3D 対応2012年頭までにはやります。たぶん、まもなく出る、Flash Player 11.2 でサポートするという意味だと思います。これのデモもやっていました。

HTML 5 向けのアニメーションツール

Adobe Edge で HTML 5 向けの2Dアニメーションオーサリングツールを公開していますが、スマートフォンが HTML 5 しか使えなくなった以上、これは積極的に投資してく方針みたいです。CS6 -> CS7 とどんどんこの手の機能を良くしてく感じみたいです。話の流れだと、Adobe 製のアニメーションツールで <canvas> 相手に生成できるのも積極的に作っていくみたいな感じでした(たぶん)。「この手の大型のオーサリングツールが市場に出ていないからね」という感じでポロッと言っていました。(でも、Flash と違って独占にはならないから、アメリカベンチャーから強いライバルが出る可能性もありそう…)

なんか、話の感じだと、ActionScript 3 → JavaScriptコンパイラ研究している感じでした。本当か?

ここらへんの話は特にデモがなく、詳細は不明です。

プロファイリングツール

Flash の新しいプロファインリグツール(ボトルネックを探すツール)のデモもやりました。フレームごとに、どの処理・スクリプトに何msかかったか見ることができる GUI ツールです。良い感じでしたよ!スマートフォン相手にも Wifi 経由でリモートプロファイリングができるそうです。

サイレントアップデート

Flash Player 11.2 からサイレントアップデートの機能が入り、ユーザーが拒否しない限り、Google Chrome みたく、勝手自動的にアップデートするようになりました。これを、Mac OS X にも近いうちに入れる予定だそうです。(Liunx は yumapt などに頼るのでしょう)

サウンド

現状200〜250ms 程度サウンドのレイテンシがあるそうですが、それを 40ms 程度まで短縮した Flash Player を今後出すそうです。

国際化

これは会場の質問から出たのですが、Flash が日本語など非英語圏でテストが甘くバグが多い、という文句が出たのですが、(日本語入力テキストフィールドでできなくなったり、マイク選択で英語以外のデバイス名が含んでいると動作がおかしくなるなど)、「頑張ります」的な回答しかなかったのですが、日本語でバグレポートを出来る場を作って欲しいと言われていて、これはそのとおりだと思います。

Alchemy 2

C/C++ ライブラリを Flash Player 内で動かす Alchemy ですが、一度死にかかった感じがあるのですが、Alchemy 2 としてちゃんと再生させることが発表されています。(技術的に何が変わるのか質問したかったのですが、タイムオーバーで質問出来なかった)。話によると、ネイティブと変わらないパフォーマンスで動いているよと言っていました。コンパイラは LLVM のコンパイラなので、最適化関係は LLVM の強力な最適化で行われるのですが、あとは、生成される命令がどの程度ちゃんと JIT されるかなんですが、まぁ、期待!

ネイティブエクステンションという選択肢も Adobe AIR ではありますが、

  • パーフォマンスが理由なら、Alchemy 2 を使って
  • OS の特殊な API を呼び出したいなら、ネイティブエクステンションを使って

という使い分け方を推奨していました。

Flex

Flex にさく予算は減らし、Apache 管轄で、コミュニティ主導で維持していくと発表していました。僕の意見として、HTML 4 でできることは Flash でやらないほうが良いことが多く(日本語入力にバグがあるなどの理由から)、Flex は HTML 4 と被る部分が多く、HTML 4 と被る部分は積極的に投資しないというのは正しい判断だと思います。

Text Layout Framework

Text Layout Framework は Flex の一部になっているけれど、純粋に一部というわけではないので、これはちゃんとメンテナンスしていくと言っていました。

こんな内容だったかな。少し上記、報道というよりは、私見も混じっていてすいません。動画関係も抜けています。

2011年10月14日 mixiアプリのユーザーIDプラットフォーム共通化の移行方法

mixiアプリユーザーIDプラットフォーム共通化の移行方法

mixi海外SNSとプラットフォーム共通化をするらしく、その関係で、今まで数字のIDだったのが、文字列のIDに切り替わります。その関係で、mixiアプリ提供者は今月中(2011年10月)に新方式に移行が必要です。

http://developer.mixi.co.jp/news/news_apps/009668.html

なんか、あまり手法とかブログで見かけなかったので、やり方とか書いておきます。手抜きしたい方の参考にどうぞ。

まず、変わるのは、ID だけで、API は変わりません。今まで、ID を文字列で管理していた人は、データベースの ID さえ、差し替えしまえば対応完了です。数値でやっていた人は、文字列にプログラムを書き換える必要があります。

一連の話、テストアプリで一通り練習してから、本番アプリで行ってくださいね。

ステップ1

http://developer.mixi.co.jp/appli/com/change/setting/trans_id/ にあるように、ID変換API の申請をします。アプリが稼働中の状態でやってしまっても、通常は大丈夫です。

ステップ2

まず、旧ID の一覧が必要です。in.csv は(1列のCSV、つまりカンマなし)で旧IDをずらずらと並べた形式にしました。

in.csv の作り方は、アプリ次第ですが、僕の場合は、PostgreSQL でこんな感じでした。

COPY (SELECT mixi_id FROM account_mixi) TO '/tmp/in.csv' CSV;

ステップ3

次は、旧ID → 新ID の変換です。RESTful API を使うと、変換表が手に入ります。こんな感じの Java のアプリでやりました。http://code.google.com/p/opensocial-java-client/ が必要です。

java -classpath .;opensocial-1.0.jar;commons-codec-1.3.jar;json_simple-1.1.jar;oauth-20090825.jar MixiOldIdConverter in.csv out.csv failed.csv

で実行します。一度実行したら、out.csv や failed.csv に保管するので、2回目は差分だけ実行できます。1回目は、アプリが動いた状況で実行し、その後必要なら、数回、アプリが実行している状態で行い、最後にアプリを停止して変換すると、アプリの停止時間を小さく出来ます。

import org.opensocial.Client;
import org.opensocial.Request;
import org.opensocial.RequestException;
import org.opensocial.Response;
import org.opensocial.auth.OAuth2LeggedScheme;
import org.opensocial.models.Model;
import org.opensocial.services.PeopleService;

import java.io.*;
import java.util.Date;
import java.util.HashSet;

public class MixiOldIdConverter {
    // 本番
    private static final String consumerKey = "fuga";
    private static final String consumerSecret = "barbar";
    // テスト
//    private static final String consumerKey = "fugaTest";
//    private static final String consumerSecret = "barTest";

    public static void main(String[] args) throws IOException {
        File inFile = new File(args[0]);
        File outFile = new File(args[1]);
        File failedFile = new File(args[2]);

        HashSet<String> converted = new HashSet<String>();
        readOutFile(outFile, converted);
        readOutFile(failedFile, converted);

        BufferedReader reader = new BufferedReader(new FileReader(inFile));
        PrintWriter writer = new PrintWriter(new FileWriter(outFile, true));
        PrintWriter failedWriter = new PrintWriter(new FileWriter(failedFile, true));

        int lineNo = 0;
        String line;
        while((line = reader.readLine()) != null) {
            if (line.length() == 0) continue;
            if (converted.contains(line)) continue;
            lineNo++;

            try {
                String platformUserId = convert(line);
                writer.println(line + "," + platformUserId);
            } catch (Exception e) {
                //e.printStackTrace(); // ここコメントアウトしてもあまり問題ない
                failedWriter.println(line);
            }

            if ((lineNo % 10) == 0) System.out.println(lineNo + " " + new Date());
        }

        failedWriter.close();
        writer.close();
        reader.close();
    }

    private static void readOutFile(File outFile, HashSet<String> converted) throws IOException {
        if (outFile.exists()) {
            BufferedReader reader = new BufferedReader(new FileReader(outFile));
            String line;
            while((line = reader.readLine()) != null) {
                if (line.length() == 0) continue;
                converted.add(line.split(",")[0]);
            }
            reader.close();
        }
    }

    public static String convert(String oldId) throws IOException, RequestException {
        OAuth2LeggedScheme authScheme = new OAuth2LeggedScheme(consumerKey, consumerSecret, oldId);
        Client client = new Client(new MixiProvider(), authScheme);

        Request viewer = PeopleService.getViewer();
        viewer.addParameter("fields", "platformUserId");
        Response response = client.send(viewer);
        Model person = response.getEntry();

        return (String) person.getField("platformUserId");
    }
}
import org.opensocial.providers.Provider;

public class MixiProvider extends Provider {
    public MixiProvider(){
        super();

        setName("mixi");
        setVersion("0.8");
        setSignBodyHash(false);
        setRestEndpoint("http://api.mixi-platform.com/os/0.8/");
    }
}

ステップ4

  1. Webアプリを停止する。
  2. データベースのバックアップをとる。
  3. in.csv の最終形を作る。
  4. 変換して、out.csv の最終形を作る。
  5. この後記載する SQL みたいな感じで、新 ID に置き換える。
  6. 念のため、別なファイル名で、再度、データベースのバックアップをとる。
  7. 「IDのプラットフォーム共通化対応完了」をクリック。これ以降、新 ID で mixi の方からは応答が来るようになります。
  8. Webアプリを再開する。
CREATE TABLE old_new_mixi_id_map (
  old_mixi_id VARCHAR(255) PRIMARY KEY,
  new_mixi_id VARCHAR(255) NOT NULL
);

COPY old_new_mixi_id_map FROM '/tmp/out.csv' CSV;

UPDATE account_mixi SET mixi_id = 
  (SELECT new_mixi_id FROM old_new_mixi_id_map 
    WHERE old_new_mixi_id_map.old_mixi_id = account_mixi.mixi_id)
  WHERE mixi_id in (SELECT old_mixi_id FROM old_new_mixi_id_map);

場合によっては、他にも関連するテーブルの情報を削除する場合がアプリによってはあると思います。(僕の場合は、他に2カ所、データを削除しました)

トラックバック - http://d.hatena.ne.jp/yukoba/20111014

2011年03月28日 福島県飯舘村は屋内退避させるべきか否か

福島県飯舘村は屋内退避させるべきか否か

ソフトバンク孫正義さんが、Twitterで、政府の出している避難指示に関して、http://twitter.com/masason/status/51832607117295616 以下のように書いていて、この問題についてです。

政府は飯舘村や南相馬市に明確な避難命令を出すべき。RT @mryoshi55: 政府が中途半端なことをするから、ここ米沢避難所から飯館村や南相馬市に戻る避難者が今日出てきた、今はまだ止めた方が良いと思う

http://twitter.com/masason/status/51836389716795392

「直ちに問題無し」「避難命令拡大不要」を連呼する政治家学者は自らの家族がそこにいても避難させないのだろうか? @dunce_jp @masason: 政府は飯舘村や南相馬市に明確な避難命令を出すべき。

僕は、政治哲学として、「平時に決めた緊急時マニュアルはちゃんと守るべき」というのが僕のスタンスです。国が決めた、ルールは以下の通りです。

対策外部被ばく内部被ばく
屋内退避10ミリシーベルト〜50ミリシーベルト100ミリシーベルト〜500ミリシーベルト
避難50ミリシーベルト以上500ミリシーベルト以上

この問題、色々な単位が飛び交っていて、ややこしいのですが、これは「累積量」です。混乱している方もいますが、「1時間あたりの」というやつではないです。なお、1ミリシーベルト以下なら、日常自然から浴びるレベルなので無視できるとされています。そして、健康被害が出るのは500ミリシーベルトといわれ、福島第一原発で命がけで作業に当たっている人たちで100ミリシーベルト以上被ばくしている人が多数いますが、今のところ大丈夫みたいです。国の基準の詳細は http://www.mext.go.jp/component/a_menu/other/detail/__icsFiles/afieldfile/2011/03/28/1304305_2810.pdf の末尾2ページをご覧ください。

現在は、

  • 半径20km以内 - 避難
  • 半径20〜30km以内 - 自主避難(元は屋内退避)

という指示が出ています。

あと、内部・外部とあるのですが、以下、「外部被ばく」の方で、計算します。なお、「内部被ばく」の方は、SPEEDIによるコンピューターによる概算の予測値があるのですが、外部被ばくの方は17日以降は実測値があり、より実際に近いはずなので、外部被ばくの方をみます。この違いも、ややこしいよね。

なお、僕はIT業界の人で、原子力素人ですが、一連の話、超ひも理論素粒子)を研究している友人に色々教えてもらいました。(ただし、彼も、厳密には原子力工学は専門じゃないです)。色々ありがとうね!あと、専門家の皆様、この記事に誤りを含んでいたら、訂正お願いいたします。m(_ _)m

次に、外部被ばくで問題となる、飛んでくる放射性物質ですが、風に流されて飛んできて、雨が降ると大量に地面に落ちてきて、地面に降りてくるとあまり動かなくなり、その場で放射線をまき散らすそうです。放射線には半減期というのがあり、例えば、今回、大量にばらまかれている、ヨウ素131だと、半減期が8日なので放射線の量は8日で1/2、16日で1/4とだんだん減っていきます。

そして、放射性物質が大量に飛散した原因は、3月15日あたりに、福島第一原発のバッテリーが切れた後、原子炉の格納容器内の圧力が高まったので、中の空気をそのまま外に逃がす作業を緊急的にやっていました。ここら辺の経緯は 福島第一原子力発電所事故 - Wikipedia をどうぞ。

ただし、この作業は、最近は行っていません。なので、

  • 新たに放射性物質を大量飛散させるような作業を原発で行わない
  • 雨が降っても、これ以上、放射性物質が大量に落ちてくることはない

ならば、あとは半減期で減っていくだけです。確証はもちろんないですが、現状の様子だと、この2つ、どっちも起きる可能性は低そうな気がします。(ちなみに、最近問題になっているのは、空気中ではなく、海に放射性物質をまき散らしています)

というわけで、新たに放射性物質が増えないなら、半減期を足し算(積分)すれば、放射線量の「累積量」がわかります。

その計算に必要なデータ文部科学省404error:文部科学省 で公開しています。風は北西方向に吹くことが多く、北西方向に多く放射性物質が飛んでしまったので、北西方向の以下の3地点を選びました。全て、30kmエリアの外です。自主避難などが出ていないOKとされている場所です。

場所距離計測地点番号
浪江町津島30km32
飯舘村40km62
福島市60km1

文部科学省が計測しているのは、役場や小学校があるなど、それぞれの集落の中心部です。今問題になっているのが「飯舘村」です。「浪江町津島」は自主避難してしまったのか、多くの人が残っているのか僕はよくわかりません。

結論

先に結論を書いてしまうと、以下の通りです。mSvはミリシーベルトです。

場所距離15日から積分17日から積分判定
浪江町津島30km39.4mSv30.4mSvたぶんアウト
飯舘村40km8.3mSv6.5mSvたぶんギリギリセーフ
福島市60km2.1mSv1.7mSvたぶんセーフ

計算方法

まず、文部科学省が発表している元データです。15日から飛散しているのですが、多くの地点で計測を始めたのは17日からなので、17日からのデータです。単位はマイクロシーベルト/時です。1000マイクロ=1ミリです。

日付経過日数浪江町津島飯舘村福島市
3月17日0 170 7
3月18日1 150308.5
3月19日2 13626.57.2
3月20日3 11025.85
3月21日4 9020.45
3月22日5 7515.33.5
3月23日6 7516.84
3月24日7 6513.23.6
3月25日8 6512.3
3月26日9 4610.22.5
3月27日10 5011.23.5

飯舘村の3/17のデータはおかしかったので空欄にしました。3/18のデータも30以上となっていますが、30としました。

これをグラフプロットすると以下のようになります。半減期は指数関数表現できるので、Excelの近似曲線は「指数近似」です。浪江町津島や飯舘村はかなり綺麗に近似曲線にフィットします。福島市は少し不正確です。

f:id:yukoba:20110328172648p:image

f:id:yukoba:20110328172649p:image

f:id:yukoba:20110328172650p:image

この近似曲線を積分すると、累積量がわかるのですが、3月15日は経過日数「-2」なので、「-2〜無限大」で積分すると累積量がわかります。ただし、3/15や3/16のデータがない部分をこのように予測値で埋めて良いのかどうかは、若干、不確実です。しかし、それにより、判定結果が変わるわけではないので、この手法を採用しても大丈夫だと思います。「結論」の「15日から積分」が「-2〜無限大」で「17日から積分」が「0〜無限大」です。

積分計算は WolframAlphaを使いました。計算結果のリンクは以下の通り。浪江町津島の分だけ、キャプチャ画像を張ります。

f:id:yukoba:20110328172647p:image

専門家へのお願い

原子力が専門家の方は、もっともっと、ブログなどでインターネットで、現状どうなっているか解説記事を書いていただけるとすごく嬉しいです!正確な情報が広まれば広まるほど、非科学的な行動をする人・デマに流される人・政府や電力会社のおかしな行動は相対的に減ります!

そして、一日8時間以上インターネットを使っている(笑)、インターネット業界の人は、難しめの専門的な記事は、クチコミで広がりにくいので、専門家による良質な記事を見つけられた際は、Twitter や はてなブックマーク などで、少しでも「拡散」するように、ぜひぜひ、ご協力をお願いします!

疑問点(半減期)

http://ja.wikipedia.org/wiki/%E5%8D%8A%E6%B8%9B%E6%9C%9F に半減期の計算方法があり、上記の近似式を使うと、半減期は以下の通りになります。

場所半減期
浪江町津島5.3日
飯舘村5.6日
福島市6.6日

5〜7日とヨウ素131の半減期の8日よりも少し短いです。原発に近いほど減るペースが速く「風で再拡散しているのでは?」という説を教えてもらったのですが、そういう物なのでしょうか?

ネコネコ 2011/03/28 19:17 これが正しいかどうかは専門家に任せますが、
表形式でとても分かりやすかったです。
マスコミにはどうやら「1時間の数値」が溢れているようです。
各自計算すればわかる話ですが、こうして可視化されていると
今どういう状況か、今後どう推移することが予測されるか、
がきちんと理解できますね。
できればマスコミにもこういう説明をしてほしいところです。

yukobayukoba 2011/03/28 20:15 ありがとうございます。
「各自計算」はかなり酷ですが、
可能な限りわかりやすく説明してもらえると嬉しいですよね。

naonao 2011/03/29 13:05 大変わかりやすい計算結果有難うございます。ご参考までに、福島県災害対策本部(http://www.pref.fukushima.jp/j/)が県内各地で測定していた実測データ(3/15以前の分もあり)に基づくグラフが、飯館村と福島市の積分線量値つきで公開されています。http://twitter.com/#!/hayano/status/52576806162808832

yukobayukoba 2011/03/29 14:29 福島県災害対策本部もデータを公開していたんですね。
気づいていませんでした。ありがとうございます!
3月15日0時〜3月29日10時の時点で、飯舘村は5.1mSvなんですね。

naonao 2011/03/29 18:19 お返事どうもありがとうございます。福島県と文部科学省の測定点の位置は必ずしも同じではないかもしれず、それも積算値の違いの原因の一つかもしれませんね。すでにお気づきかと存じますが、文部科学省のデータは測定点が福島原発の北西側に偏っています。福島県下全体の状況を知るには福島県災害対策本部のデータを合わせて読むか、県下全域から得られている牛乳の放射線測定データ(厚生労働省発表http://www.mhlw.go.jp/stf/houdou/2r98520000015m5f-att/2r98520000015m9w.pdf)を地図に重ねて読むかする必要があるのですが、まだ誰も実行していないようです。もっぱら奥羽山脈の東側の状況だけが福島県全体の状況として全国報道されて風評被害を生んでいます。奥羽山脈の西側は、空間線量率からも牛乳の測定値から見ても今のところほとんど影響を受けているとは思えないのに、牛乳の出荷停止は全県一律です。

2011年03月08日 JavaScriptでソフトウェアの正しさを数学的厳密に証明してみた

JavaScriptでソフトウェアの正しさを数学的厳密に証明してみた

現在Shibuya.js が開催中です!Ustreamhttp://www.ustream.tv/channel/shibuyajs にて放送されています。これから、このブログの内容をしゃべります!

今回「テスト」がテーマなうえ、Shibuya.js は「役に立つ話担当」「ネタ担当」に分かれていて、僕は「ネタ担当」なんですが(笑)、いつも通りネタです。でも、遠い未来の役立つネタです!

きっかけは、id:t-wada さんに、GUI自動テスト関係の質問をしたら、凄くいいことを教えてもらいました。

全てのテストはサンプリングテストである

(少し表現違ったらごめんなさい)話の流れで、部屋を移動しなくていけなくて、たしか、それしか話ができなかったのですが、要するに、サンプリングテストである以上、全ての入力パターンをテストすることは不可能であり、できることは、限られたコストの中で、効率よくテストする必要がある、という意味だと思います。だから、手動テスト vs 自動テスト、どっちが良いのかは、その文脈での効率性で決まるという、趣旨の発言だったと、僕は理解しました。(ちょっとしか会話できなかったので、ほとんど推測です。t-wada さんの意図は、全然違ったりして…)

この名言は、本当に凄くいい名言だと思うんですが、Shibuya.js の「ネタ担当」としては、あれ?全て?と引っかかりました (^^♪ 「例外のない規則はない」ということわざもありますしね!この、ことわざは自己矛盾しているんですが…(笑)

自動証明

というわけで、プログラムが与えられて、そのプログラムのテストプログラムが与えられて、数学的にその正しさを式変形を繰り返して、正しさを証明するプログラムを作りました

ターゲットは、一番やりやすそうな「挿入ソート」を選びました。(申し訳ないですが、挿入ソートとは何かは、検索してください。手抜きごめんなさい)

プログラムは以下の通りです。

function sortInner(ary) {
  if (ary.length < 2) {
    return ary;
  } else {
    if (head(ary) < head(tail(ary))) {
      return ary;
    } else {
      return append(head(tail(ary)), sortInner(tail(swap(ary)));
    }
  }
}

挿入ソートは2重ループなのですが、ループの内側の部分だけです。つまり、ary[1] 以降はソート済みで、ary[0] を適切な位置まで挿入する部分をターゲットにしました。

head(ary) = ary[0]、tail(ary) = ary.slice(1)、swap(ary) は ary[0] と ary[1] を入れ替えを非破壊で(新しい配列を生成して)行います。

ソートの正しさの判定

正しくソートされていることを証明するには、以下の2つを証明する必要があります。

  1. ary[i] < ary[i + 1]
  2. 「ソート前」「ソート後」で要素が1対1対応すること

扱う問題を小さくするために、今回は、1の方だけを扱います。

というわけで、判定プログラムは以下の通りです。(isOrdered の方が正確な名前かもしれません)

function isSorted(ary) {
  if (ary.length < 2) { 
    return true; 
  } else {
    return head(ary) < head(tail(ary)) && isSorted(tail(ary));
  }
}

証明すること

証明することは、isSorted(sortInner(ARY)) = true です。前提条件として、isSorted(tail(ARY)) = true が成立します。加えて、数学的帰納法を使い証明するので(まだ、この部分は自動化できませんでした)isSorted(sortInner(tail(ARY))) = true を条件に加えます。

証明時に、変数と定数を区別しているのですが、数学的帰納法において、配列の長さは制限が加えられていて、任意の配列というわけではないので、対象の配列を定数化し、ARY で表現しました。

プログラムの表現方法

Haskell のような純粋関数型言語は難しすぎて、人間には書きづらいと思うのですが、自動証明においては、凄く扱いやすく、採用しました。関数は全て副作用がありません。つまり、配列操作は、絶対に配列を破壊しません。なので、sortInner は以下の形になります。

sortInner(ary) = 
  if(lt(len(ary), 2),
    ary,
    if (lt(head(ary), head(tail(ary)),
      ary,
      append(head(tail(ary)),
        sortInner(tail(swap(ary))))))

DOM & XPath

これをひたすら式変形します。上記の通り、関数は木構造になっているので、パターンマッチングでひたすら木構造の変形になります。

木構造をどう扱うか悩んだんですが、最初正規表現を使おうかと思ったんですが、Perl の正規表現とは違って JavaScript の正規表現は再帰が扱えないので、木構造が扱いづらく、JavaScript (HTML) は DOM が使えて、木構造のための API があるので、関数を DOM に押し込みました!その上で、式変形のパターンマッチングを XPath を使って検索するようにしました。Firebug などを使うと、木構造の変形を追いやすく、便利でした!

定義公理

そのほか、使う定義や公理は以下の通り。

head(tail(swap(ary))) = head(ary)
tail(tail(swap(ary))) = tail(tail(ary))
tail(append(ary, v)) = ary
head(append(ary, v)) = v
if(true, a, b) = a
if(false, a, b) = b
if(a, b, b) = b
a && true = a
true && a = a

ちょっとズルなんですが、定義のような定理

len(append(ary, v)) < 2 = false

連結すると、長さが2以上になるよと言う件です。len と append の関係性を手抜きしました。

上手く扱えなかった数学的帰納法

昨日・今日でこの準備をしていて、発表までに間に合わなかった、数学的帰納法の取り扱いです。以下の2つは単独で証明できると思うのですが、うまく、自動証明の流れの中で証明できなかったので、定理に加えてしまいました。ごめんなさい。次の課題として、これをちゃんと自動証明できるようにしたいです!

  1. head(tail(ARY)) < head(tail(tail(ARY)))
  2. isSorted(sortInner(head(swap(ARY)))) = true

最初の方は、tail(ARY) はソート済みだから tail(ARY)[0] < tail(ARY)[1] という事です。

次の方は、head(swap(ARY)) は長さ n – 1 だから、数学的帰納法により証明済み という事です。

if 条件の伝搬

さらに、特殊な式変形が2つ必要です。一つ目は、if (A) { B } else { C } において、B の中で A = true であることを使うことが必須です。これが、「if 条件の伝搬」。

if (A, B, C) で

  • Bの中でAを使っていたら、A = true
  • Cの中でAを使っていたら、A = false

否定形も必要でした

  • Bの中でnot Aを使っていたら、not A = false
  • Cの中でnot Aを使っていたら、not A = true

if の親関数の繰り込み

2つ目は、if の親関数の繰り込みです。 f(A ? B : C) = A ? f(B) : f(C) です。fの引数の数が任意でも扱えると言うことを上手く表現する方法が思いつかなかったので、別枠でコードを書きました。

証明戦略

式変形において、次の一手は、たくさんあり、指数関数的に増えると思ったのですが、なんと、式変形に優先順位をつけたら、一直線で証明できました。

  1. ノード数が減る変形 や if 条件の伝搬。
  2. if の親関数の繰り込み
  3. ノード数が増える変形(定義の代入)

ノード数が減る方を優先して、それをやることがなくなったら、ノードを数を増える変形をやってみて、さらに、また、ノード数を減らす変形を繰り返して、というので、できました。でも、これは、今回の特例で、おそらく、次にどういう手を繰り出すかは上手い評価関数を作って、証明が分岐していくパターンは絶対に必要だと思います。

if の親関数の繰り込み は少しだけ、木構造が複雑になる方の変形です。

デモ

というわけで、デモです。http://yukoba.jp/autotest/sort.html をごらんください。出力は、console.log() に出ます。Internet Explorer 8は未対応です(XPath の扱いが違います)。細かいアルゴリズムhttp://yukoba.jp/autotest/js/sort.js をご覧ください。

というわけで、console.log() をみるとわかるのですが、なんと38回の式変形で証明できちゃうんです!

ログの出力は、「証明すべき対象の式」「使える変形式」を出力した後、そこから先は、式変形ごとに、「どの式を使って変形したか」「証明すべき対象の式の変化した結果」を繰り返し表示しています。

使用したスライド