ソフトウェア関連の個人的備忘録
ソフトウェア関連の個人的備忘録

SPIN環境

ソフトウェア関連の個人的備忘録内検索 / 「SPIN環境」で検索した結果

検索 :
  • SPIN環境
    SPINの支援環境ツールについて まずSPIN SPINを動かすには以下のものが必要spin.exe gcc.exe(多分Cコンパイラであればなんでも) cygwin1.dll(場合により) 本家サイトに行けば全部そろう Cygwinがインストールしてあれば楽 iSpin 本家が開発しているSPIN支援ツール xSpinの後継で、2010年12月に誕生 それに伴いxSpinのサポートは終了らしい SPINの検証を楽にしてくれるツールのようPromela記述を楽にはしてくれなさそう Editor部分はあるが、反例トレース用だと思う。Promelaをそこで書くものではなさそう したがって、Promela editorは別のを使うのが良い（今のところ） tcl/td(Active Tcl)のインストールが必要 xSpin iSpinに代わる が、まだ使えると思う jSpin Jav...
  • メニュー
    ...SPIN v6メモ SPIN環境 例その1 Promela覚書その1 Promela覚書その2 リンク @wiki @wikiご利用ガイド 他のサービス 無料ホームページ作成 無料ブログ作成 2ch型掲示板レンタル 無料掲示板レンタル お絵かきレンタル 無料ソーシャルプロフ ここを編集
  • SPINv6
    バージョンに関するメモ SPIN v6.0.0 2010年12月にv6になる 構文追加 for文の実装for(i 1..100){...} 便利 Multiple Never Claimのサポート Never Claimを一つのファイルに複数書くことができるようになったらしいnever ncname { ... }と名前付きで記述して、実行時に「./a -N ncname 」で指定 検証は一つずつ 複数のNCを一つにまとめることもできる「spin -e filename 」で複数のNCがあった場合1つにしてくれる GraphvizのDotのサポート 実行時に「./a -D」でDot言語に変換した形で出してくれるこれはつまり、図形化できるということだと思う 実際にできた。素晴らしい。 iSpinでも自動生成できるが、コマンドでやった方が図がきれい
  • SPIN例題1
    簡単な説明と簡単な例で簡単に雰囲気をつかみたい。 spinがインストールしてあるのが前提。 構造： 　Promelaが扱う主なデータタイプは以下の通り データタイプ 値の範囲 補足 bit 0..1 1bit bool false, true 1bitでfが0でtが1 byte 0..255 8bit short -2^15..-2^15-1 符号付16bit int -2^31..-2^31-1 符号付32bit 　すべてintで宣言すればいいわけではなく、状態が多くなりすぎて検査できない（いわゆる状態爆発）を防ぐために、intよりshort、shortよりbyte、byteよりbitなどと小さくしていくと無駄がなくなってモデル的にも良い、と言われている。 他には、mtypeやpid、unsignedがある。mtypeは良く使うので後に例を書きたいと思う。p...
  • モデル検査ツール/SPIN
    SPIN 概要メモ 分散・並列ソフトウェアを検証するために作られた検証器。 1980年頃からベル研究所で開発された。 Holzman氏が開発。 Promela(Process Meta Language)という仕様記述言語を持つ。 SPINはSimple Promela Interpreterの略。 Promela チャネル通信オートマトンをベースにしている。 オートマトンなので状態遷移系として記述する。 チャネル通信の記述部分はCSP/Occamライクで、括弧の使い方とかセミコロンはC言語ライク？
  • Promelaメモ1
    エラーが出て30秒以上なやんだところを覚え書き その1 ガード条件内のinline展開は括弧をつけるとエラー？ 追記ガード条件に副作用がある文は使えないとあるので、理由はそれ(多分) byte n = 0; inline under1(){ n 1} active proctype P1(){ if (under1()) - printf("pass"); fi;} エラー spin e1.pml 9, Error syntax errorsaw 'inline name' near 'under1' 直る byte n = 0; inline under1(){ n 1} active proctype P1(){ if ...
  • Promelaメモ2
    いつも確認したくなること その1 初期化しないと0が入る bit n1;bool n2;byte n3;short n4;int n5;mtype n6; active proctype P1(){ printf("bit %d\n", n1); printf("bool %d\n", n2); printf("byte %d\n", n3); printf("short %d\n", n4); printf("int %d\n", n5); printf("mtype %d\n", n6);} 結果($spinオプションなし) bit 0 bool 0 byte 0 short 0 ...
  • プラグイン/ニュース
    ニュース @wikiのwikiモードでは #news(興味のある単語) と入力することで、あるキーワードに関連するニュース一覧を表示することができます 詳しくはこちらをご覧ください。 ＝＞http //atwiki.jp/guide/17_174_ja.html たとえば、#news(wiki)と入力すると以下のように表示されます。 【グランサガ】リセマラ当たりランキング - グランサガ攻略wiki - Gamerch(ゲーマチ) マニュアル作成に便利な「画像編集」機能を提供開始！ - ナレッジ共有・社内wikiツール「NotePM」 (2021年12月6日) - エキサイトニュース マニュアル作成に便利な「画像編集」機能を提供開始！ - ナレッジ共有・社内wikiツール「NotePM」 - PR TIMES 「Wiki」創設者のPC 競売に - ...
  • プラグイン/人気商品一覧
    人気商品一覧 @wikiのwikiモードでは #price_list(カテゴリ名) と入力することで、あるカテゴリの売れ筋商品のリストを表示することができます。 カテゴリには以下のキーワードがご利用できます。 キーワード 表示される内容 ps3 PlayStation3 ps2 PlayStation3 psp PSP wii Wii xbox XBOX nds Nintendo DS desctop-pc デスクトップパソコン note-pc ノートパソコン mp3player デジタルオーディオプレイヤー kaden 家電 aircon エアコン camera カメラ game-toy ゲーム・おもちゃ全般 all 指定無し 空白の場合はランダムな商品が表示されます。 ※このプラグインは価格比較サイト@PRICEのデータを利用しています。 ...
  • @wiki全体から「SPIN環境」で調べる

更新順にページ一覧表示 | 作成順にページ一覧表示 | ページ名順にページ一覧表示 | wiki内検索