ウィリアムのいたずらの、まちあるき、たべあるき

ウィリアムのいたずらが、街歩き、食べ物、音楽等の個人的見解を主に書くブログです(たま~にコンピューター関係も)

初音ミクの式があるらしい・・・

2013-11-18 18:11:28 | Weblog
ほら


そんなこんなのお話のまとめが

【画像】計算グラフで二次絵書いたったwwwwwwwwwwwww
http://sonicch.com/archives/34147267.html

に載ってるらしいよ

P.S だれか、Rで作って欲しい。


  • X
  • Facebookでシェアする
  • はてなブックマークに追加する
  • LINEでシェアする

Event-Bは要求仕様の検証だけでなく、モデル検査やシミュレーションもできるみたい!

2013-11-18 14:42:54 | トピックス
TOPSEのEvent-B/RODIN集中セミナーに行ってきた!それについて、何回かに分けてメモメモ!

するけど、今回は、全体的な話。

Event-Bというと、普通の印象は、要求仕様の検証。
Rodinなんかが有名なわけなんだけど、このRodinがかなり進化したみたい。
検証だけでなく、モデル検査やシミュレーションもできる上、
記述に関しても、かなりの支援が付くようになった。
その結果、もしかすると、他の形式仕様、例えばVDMなんかよりも、
書きやすくなったかもしれない。

そのへんを、今日はご紹介してみる。
なお、以降紹介することは、このセミナー用のRodinだとできることで、普通にダウンロードしただけでは、ここまではできず、プラグインを入れまくると、こうなるらしい。




■書きやすくなったエディタ

昔のRodinは、たしか

みたいな、ふつうの感じのエディタと

のEbent-B用エディタしか、なかったんじゃなかったっけ?
ちがったっけ?
今は、Rodinエディタっていうのがあって、

な感じの画面になる。
そして、入力は、

のように、右クリックから、いろいろな要素を選んで行うことも出るし
上にウィザードがあって、そこをクリックすると、

のように、入力支援ダイアログがでてくる。




■自動的に検証しているみたい

で、書き終わると、

なんか、検証してくれているみたい(POのところに並ぶ)




■証明に何が足りないかがわかる。

いま、この記述は、
  不変条件 nは0より大きい
  初期値 n=5のとき
  イベント n=n+1
になっている。ここで、
  イベント n=n-1
にかえる。当然そうすると、証明できなくなる。
(イベントが6回起きると、nはマイナスになり、不変条件を満たさなくなる)

で、ここからがすごい。
その茶色の証明できないPOをダブルクリック!
証明できないところが出てくる。

ここで、Goalに注目!
n-1が0より大きいと出ている!
これが証明できない・・・そうそう、この条件がイベント1にないと、
確かに不変条件を満たさない。

ということで、この足りない条件を、ガードに入れると、
(ここ、コピーできる)

証明できた。




■さらに、シミュレーション?

右ボタンクリックで、Start Animation/Model Checking

を選択すると、

な感じになる。左上のINITIALIZATIONをクリックすると、
evt1が今度緑になってクリックでき、
緑の三角形(ここでは、evt1しかならないけど)
をクリックしていくと・・・



真ん中に値の変化、右側に履歴(クリックして実行したもの)
が出ている。




■モデル検査

ここで、Checksをクリックすると、Model Checkingとでてくるので、

これを選択。

デフォルトだと、デッドロックと不変条件のチェックを
してくれるらしい。真ん中下のボタンをクリック

なんかやらかしたらしい・・・Detailsをクリック

下に説明が出てくる。

なお、ここで言っている「デッドロック」とは、
いわゆる排他制御でおこるデッドロックだけでなく、
どのイベントにもいけなくなることをさしている
(排他制御のデッドロックもどこにもいけなくなるが、
 それ以外の理由も含む)

nが2になったとき、evt1に入るとn=1となる。
しかし、n=1となると、次に実行できるイベントがない
そのため、デッドロックになる。




なんか、知らぬ間にEvent-Bが進化して、シミュレーションまで出来るように
なってきた。これ、通信プロトコルのチェックとかにいいかも?

  • X
  • Facebookでシェアする
  • はてなブックマークに追加する
  • LINEでシェアする

ajaxでdocument.write→document.readyが通らない対策2つ

2013-11-18 10:47:43 | JavaとWeb
環境はIE、WindowsXP。
どうもAJAXで、読んできた内容をdocument.write()させると、
(いや、それ自体良くないという話も1つ2つあるが、まあ、それは置いておいて)

$(function(){

// ここの中が、通らない!

});

みたい。つまり、JQueryのdocument.ready()が通らない。
この下に、functionとか書くと、そこは通る。

このとき、上記の通らない部分を通す方法(対策)2つ




■まず、事例(御題)

たとえば、以下のdatepickerを表示するプログラムを実行すると

<!doctype html>
<html>
<head>
  <title>Datepicker</title>
  <link rel="stylesheet" 

href="http://code.jquery.com/ui/1.10.3/themes/smoothness/jquery-ui.css" />
  <script src="http://code.jquery.com/jquery-1.9.1.js"></script>
  <script src="http://code.jquery.com/ui/1.10.3/jquery-ui.js"></script>
  <link rel="stylesheet" href="/resources/demos/style.css" />
  <script>

$(function(){
    $( "#datepicker" ).datepicker({
	dateFormat: "yy/mm/dd"
    });
});

function getdate()
{
	val = $( "#datepicker" ).val();
	alert(val);
}
  </script>

</head>

<body>
<p>Date: <input type="text" id="datepicker" /></p>
<BUTTON onclick="getdate()">date</BUTTON>
 </body>
</html>



のように、当然のことながら、そこにカーソルを入れれば、
datepickerが出る。

ところが、以下のAJAXを使ったプログラム

<HTML>
<head>
<script src="http://code.jquery.com/jquery-1.9.1.js"></script>
<script>
$(function(){
$("#bt1").click(function () {
$.ajax({
type: "POST",
url: "date.htm",
dataType:"html",
success: function(msg){
document.write(msg);
}
});
});
});
</script>
</head>
<body>

<BUTTON id="bt1">AJAX</BUTTON>

</body>
</html>


を、(「AJAX」ボタンをクリックして)実行し、
AJAXから、上記プログラムを呼び出すと・・・

わかりにくいが、カーソルをテキストエリアにいれても、
datepickerにならない。
つまり、datepickerの設定をしている、
$(function(){
の部分、いいかえると、document.readyは通らないように見える。

一方、functionの部分は、「date」ボタンをクリックすると

のように表示されるので、プログラムは読まれているはず。




■原因らしきこと・・・?

ということは、document.write()では、document.ready
の状態(に対応するイベント)が起きないということ?





■対策1:外部参照させたら、なぜかうまく行った・・・

これは、偶然うまく行ったことで・・・
(対策2を紹介しようとしたら、
 いや、これで出来ますよ!といわれて、
 本当に出来たことなので、紹介)

(1).まず、ajaxの呼び出し側で、
document.open(),document.close()をして、
ちゃんと、documentを開いて、そこに書かせるようにする。

<HTML>
<head>
<script src="http://code.jquery.com/jquery-1.9.1.js"></script>
<script>
$(function(){
$("#bt1").click(function () {
$.ajax({
type: "POST",
url: "date1.htm",
dataType:"html",
success: function(msg){
document.open();
document.write(msg);
document.close();
}
});
});
});
</script>
</head>
<body>

<BUTTON id="bt1">AJAX</BUTTON>

</body>
</html>


(赤字が主要な変更点。青字は、都合上変更した点)

(2)そして、呼ばれるほう(data1.htm)は、
  document.ready部分を、外部ファイルに追いやる。
  以下のとおり

<!doctype html>
<html>
<head>
<title>Datepicker</title>
<link rel="stylesheet" href="http://code.jquery.com/ui/1.10.3/themes/smoothness/jquery-ui.css" />
<script src="http://code.jquery.com/jquery-1.9.1.js"></script>
<script src="http://code.jquery.com/ui/1.10.3/jquery-ui.js"></script>
<script src="datescript.js"></script>
<link rel="stylesheet" href="/resources/demos/style.css" />
<script>

function getdate()
{
val = $( "#datepicker" ).val();
alert(val);
}
</script>

</head>
<body>

<p>Date1: <input type="text" id="datepicker" /></p>
<BUTTON onclick="getdate()">date</BUTTON>

</body>
</html>


$(function(){
の部分が抜けて、そのかわり、datescript.jsを呼び出している。

(3)document.ready部分を別ファイルに記述
この別ファイル、datescript.jsの内容は、以下のとおり。

$(function() {
$( "#datepicker" ).datepicker({
dateFormat: "yy/mm/dd"
});
});



こうすると、なぜか動く。
(動作結果は、上記のイメージと同じく、
 datepickerが出るだけなので、省略)




■対策2:onloadで読み込む

対策1は、外部ファイルにしないといけないため、
動的に生成する場合に問題があるかも・・・

というか、はじめに、こっちのほうを思いついて、
これを紹介しようと思ったんだけど・・・

(1).まず、ajaxの呼び出し側で、
document.open(),document.close()をして、
ちゃんと、documentを開いて、そこに書かせるようにする。
(対策1とここまでは同じ)


<HTML>
<head>
<script src="http://code.jquery.com/jquery-1.9.1.js"></script>
<script>
$(function(){
$("#bt1").click(function () {
$.ajax({
type: "POST",
url: "date2.htm",
dataType:"html",
success: function(msg){
document.open();
document.write(msg);
document.close();
}
});
});
});
</script>
</head>
<body>

<BUTTON id="bt1">AJAX</BUTTON>

</body>
</html>


(赤字が主要な変更点。青字は、都合上変更した点)


(2)そして、呼ばれるほう(data2.htm)は、
$(functon()
部分を、関数にしてしまい、その関数をonloadで読み込む

<!doctype html>
<html>
<head>
<title>jQuery UI Datepicker</title>
<link rel="stylesheet" href="http://code.jquery.com/ui/1.10.3/themes/smoothness/jquery-ui.css" />
<script src="http://code.jquery.com/jquery-1.9.1.js"></script>
<script src="http://code.jquery.com/ui/1.10.3/jquery-ui.js"></script>
<link rel="stylesheet" href="/resources/demos/style.css" />
<script>
function syoki()

{
$( "#datepicker" ).datepicker({
dateFormat: "yy/mm/dd"
});
}

function getdate()
{
val = $( "#datepicker" ).val();
alert(val);
}
</script>

</head>
<body onload="syoki()" >

<p>Date2: <input type="text" id="datepicker" /></p>
<BUTTON onclick="getdate()">date</BUTTON>

</body>
</html>

(赤字が主要な変更点)

こうすると、動く。
(動作結果は、上記のイメージと同じく、
 datepickerが出るだけなので、省略)




■対策にならない(失敗)例:表示側を変更しない

document.open();、document.close();の追加だけを行い
(つまり、AJAXの呼び出し側だけ修正し)
呼ばれる側は、何の修正もしない(data.htmのまま)と、
$(function()
の部分は、実行されない(つまり、何も変わらない)。

  • X
  • Facebookでシェアする
  • はてなブックマークに追加する
  • LINEでシェアする