HydLaWiki
Hyrose
Start:
* Hyroseとは [#y08cb072]
- HydLaプログラムのシミュレータである
- 数式処理を用いて, 誤差のないシミュレーションを可能とする
- 記号実行を可能として、パラメータを含むシステムを扱える
- パラメータによってシステムの振る舞いが定性的に異なる際...
- 有限時間に対する性質検証が可能である
- HydLaプログラムに対するシミュレーション, パラメータ解析...
* インストール方法 [#cee9a99e]
[[Download]]ページからHyroseをダウンロード後, 数式処理ソ...
* 使用法 [#z98de6fd]
- HyroseにHydLaプログラムを入力すると, シミュレーション結...
- 出力は, 標準出力への出力の他にJSON形式でも出力される
- 出力されるファイル名は, <プログラム名>.hydatという形と...
** オプションと意味 [#ub30e628]
-h [--help] : Hyroseのヘルプを表示する
--version : Hyroseのバージョンを表示する
-d [--debug] : Hyroseのデバッグモードを有効にする
--parse_only : HydLaプログラムのパースのみを行う
--dump_parse_tree : HydLaプログラムのパース結果を出力する
--dump_module_set_list : HydLaプログラムの解候補となる...
--dump_relation_graph : HydLaプログラムの変数や制約の関...
--dump_in_progress : 各フェーズの計算が終わるごとにその...
(本来は, シミュレー...
--search arg (=d) : 全解探索時の探索方法を指定する
d : 深さ優先探索(Depth F...
b : 幅優先探索(Breadth F...
-s [ --solver ] arg (=m) : バックエンドで使用するソルバ...
m : Mathematica
r : Reduce
--nd : 全解探索を有効にする
有効にしない場合, 場合分けが発生すると自動的...
--in : インタラクティブモードを有効にする
--find_unsat_core : unsat coreを発見する
--use_unsat_core : unsat coreを用いたシミュレーションを...
--ha : HydLaプログラムのHA(Hybrid Automaton)への変換を...
--hs : HA(Hybrid Automaton)を用いたシミュレーションを行う
--parallel : 並列処理モードを有効にする
--pn arg (=2) : 並列処理の個数を設定する(デフォルトは2)
--reuse : シミュレーションにおける再利用を有効にする
--tm arg (=n) : 時間計測を行う.
n : 時間計測を行わない(デフォ...
s : 時間計測を行い, 標準の出力...
c : 時間計測を行い, csv形式で...
--csv arg : 時間計測を行いcsv形式で出力する(--tm c)の場...
このオプションが空の場合, 標準出力に...
-O [ --optimization-level ] arg (=0) : 最適化のレベルを...
--analysis_mode arg : 分析モードを有効にする
empty : 制約の分析...
use : 分析ファイル...
output : 制約を分析...
simulate : 制約を分...
--analysis_file arg : 分析ファイルを指定する
empty : 標準出力や標準...
-o [ --output_name ] arg : hydat形式でシミュレーション...
empty : ./hy...
-t [ --time ] arg : シミュレーションの時間制限を指定す...
empty : 時間の制限はない
--ignore_warnings : 主に計算において起きた警告を無視する
-p [ --phase ] arg (=-1) : シミュレーションのフェーズ制...
positive value :...
negative value :...
-a [ --approx ] : アフィン近似を用いたシミュレーション...
-c [ --change ] : 特定の場合に次の離散変化時刻を変更可...
-e [ --epsilon ] arg (=-1) : epsilonモードを有効にする
--timeout_calc arg (=-1) : バックエンドの計算において, ...
negative or zero ...
--fail_stop : assert違反が起きた場合に, 全てのシミュレ...
--math_name arg (=math) : Mathematicaのコマンドを指定する
* 数式処理ソフトウェアの利用方法 [#s7a4a3b3]
- 現在のHyroseでは, 求解時に数式処理ソフトウェアとしてMat...
- これらを利用するために, それぞれ下記の準備を行い, 使用...
** Mahtematica [#ad3804e7]
- バージョン7以降のインストールが必要(8を推奨)
-- Mathematica8でないとエラーの発生する例題も確認されてい...
- Mathematicaのパスが通っていれば使用可能
-- 具体的には, math コマンドによってMathematicaが起動可能...
--- math コマンド以外で起動する場合には, 「--mathlink」オ...
--- GUI環境なら, 起動するMathematicaの実行ファイルを毎回...
** Reduce [#bddfe27a]
- 20101007版(それ以降には未対応)のインストールが必要
- REDUCEを数式処理ソルバとして使用する場合, 以下の手順に...
+ REDUCEのインストール手順
-- Windows系OS
--- sourceforgeのサイトからソースコード(reduce-windows64-...
--- (64bit版のREDUCEを実行するにはmingw-w64-gcc-4.6.3-run...
-- linux系OS
--- sourceforgeのサイトからソースコード(reduce-algebra-20...
--- ソケット通信時にsleep関数が原因のボトルネックが存在す...
>
+ wget http://jaist.dl.sourceforge.net/project/reduce-alg...
+ bzip2 -dc reduce-algebra-20101007.tar.bz2 | tar xvf -
+ cd reduce-algebra-20101007/
+ (reduce-algebra-20101007/ディレクトリに filepatch.txt ...
+ patch -d csl/cslbase/ < patch.txt
+ ./configure --with-csl --without-gui
+ make
<
--- このmakeによって/cslbuild/[各OSの名前]/csl/reduce に...
+ REDUCEによるHyrose実行手順
-- hydla実行ファイルと同じディレクトリの sr.sh を使って, ...
-- [REDUCE_PATH]に生成したreduceのパスを設定すること
-- windows系の場合, cygwinを使って実行する
--- 例としてREDUCEの解凍場所を「C:\reduce-i686-pc-windows...
--- 実行例
> sh sr.sh examples/bouncing_particle.hydla -t 1
<
--- [補足] linux版のREDUCEサーバは非同期通信に対応してい...
--- サーバ起動例
> [REDUCE_PATH]/reduce -w -F- &
<
End:
* Hyroseとは [#y08cb072]
- HydLaプログラムのシミュレータである
- 数式処理を用いて, 誤差のないシミュレーションを可能とする
- 記号実行を可能として、パラメータを含むシステムを扱える
- パラメータによってシステムの振る舞いが定性的に異なる際...
- 有限時間に対する性質検証が可能である
- HydLaプログラムに対するシミュレーション, パラメータ解析...
* インストール方法 [#cee9a99e]
[[Download]]ページからHyroseをダウンロード後, 数式処理ソ...
* 使用法 [#z98de6fd]
- HyroseにHydLaプログラムを入力すると, シミュレーション結...
- 出力は, 標準出力への出力の他にJSON形式でも出力される
- 出力されるファイル名は, <プログラム名>.hydatという形と...
** オプションと意味 [#ub30e628]
-h [--help] : Hyroseのヘルプを表示する
--version : Hyroseのバージョンを表示する
-d [--debug] : Hyroseのデバッグモードを有効にする
--parse_only : HydLaプログラムのパースのみを行う
--dump_parse_tree : HydLaプログラムのパース結果を出力する
--dump_module_set_list : HydLaプログラムの解候補となる...
--dump_relation_graph : HydLaプログラムの変数や制約の関...
--dump_in_progress : 各フェーズの計算が終わるごとにその...
(本来は, シミュレー...
--search arg (=d) : 全解探索時の探索方法を指定する
d : 深さ優先探索(Depth F...
b : 幅優先探索(Breadth F...
-s [ --solver ] arg (=m) : バックエンドで使用するソルバ...
m : Mathematica
r : Reduce
--nd : 全解探索を有効にする
有効にしない場合, 場合分けが発生すると自動的...
--in : インタラクティブモードを有効にする
--find_unsat_core : unsat coreを発見する
--use_unsat_core : unsat coreを用いたシミュレーションを...
--ha : HydLaプログラムのHA(Hybrid Automaton)への変換を...
--hs : HA(Hybrid Automaton)を用いたシミュレーションを行う
--parallel : 並列処理モードを有効にする
--pn arg (=2) : 並列処理の個数を設定する(デフォルトは2)
--reuse : シミュレーションにおける再利用を有効にする
--tm arg (=n) : 時間計測を行う.
n : 時間計測を行わない(デフォ...
s : 時間計測を行い, 標準の出力...
c : 時間計測を行い, csv形式で...
--csv arg : 時間計測を行いcsv形式で出力する(--tm c)の場...
このオプションが空の場合, 標準出力に...
-O [ --optimization-level ] arg (=0) : 最適化のレベルを...
--analysis_mode arg : 分析モードを有効にする
empty : 制約の分析...
use : 分析ファイル...
output : 制約を分析...
simulate : 制約を分...
--analysis_file arg : 分析ファイルを指定する
empty : 標準出力や標準...
-o [ --output_name ] arg : hydat形式でシミュレーション...
empty : ./hy...
-t [ --time ] arg : シミュレーションの時間制限を指定す...
empty : 時間の制限はない
--ignore_warnings : 主に計算において起きた警告を無視する
-p [ --phase ] arg (=-1) : シミュレーションのフェーズ制...
positive value :...
negative value :...
-a [ --approx ] : アフィン近似を用いたシミュレーション...
-c [ --change ] : 特定の場合に次の離散変化時刻を変更可...
-e [ --epsilon ] arg (=-1) : epsilonモードを有効にする
--timeout_calc arg (=-1) : バックエンドの計算において, ...
negative or zero ...
--fail_stop : assert違反が起きた場合に, 全てのシミュレ...
--math_name arg (=math) : Mathematicaのコマンドを指定する
* 数式処理ソフトウェアの利用方法 [#s7a4a3b3]
- 現在のHyroseでは, 求解時に数式処理ソフトウェアとしてMat...
- これらを利用するために, それぞれ下記の準備を行い, 使用...
** Mahtematica [#ad3804e7]
- バージョン7以降のインストールが必要(8を推奨)
-- Mathematica8でないとエラーの発生する例題も確認されてい...
- Mathematicaのパスが通っていれば使用可能
-- 具体的には, math コマンドによってMathematicaが起動可能...
--- math コマンド以外で起動する場合には, 「--mathlink」オ...
--- GUI環境なら, 起動するMathematicaの実行ファイルを毎回...
** Reduce [#bddfe27a]
- 20101007版(それ以降には未対応)のインストールが必要
- REDUCEを数式処理ソルバとして使用する場合, 以下の手順に...
+ REDUCEのインストール手順
-- Windows系OS
--- sourceforgeのサイトからソースコード(reduce-windows64-...
--- (64bit版のREDUCEを実行するにはmingw-w64-gcc-4.6.3-run...
-- linux系OS
--- sourceforgeのサイトからソースコード(reduce-algebra-20...
--- ソケット通信時にsleep関数が原因のボトルネックが存在す...
>
+ wget http://jaist.dl.sourceforge.net/project/reduce-alg...
+ bzip2 -dc reduce-algebra-20101007.tar.bz2 | tar xvf -
+ cd reduce-algebra-20101007/
+ (reduce-algebra-20101007/ディレクトリに filepatch.txt ...
+ patch -d csl/cslbase/ < patch.txt
+ ./configure --with-csl --without-gui
+ make
<
--- このmakeによって/cslbuild/[各OSの名前]/csl/reduce に...
+ REDUCEによるHyrose実行手順
-- hydla実行ファイルと同じディレクトリの sr.sh を使って, ...
-- [REDUCE_PATH]に生成したreduceのパスを設定すること
-- windows系の場合, cygwinを使って実行する
--- 例としてREDUCEの解凍場所を「C:\reduce-i686-pc-windows...
--- 実行例
> sh sr.sh examples/bouncing_particle.hydla -t 1
<
--- [補足] linux版のREDUCEサーバは非同期通信に対応してい...
--- サーバ起動例
> [REDUCE_PATH]/reduce -w -F- &
<
Page:
