Learning to Order BDD Variables in VerificationOrna Grumberg Shlomi Livne Shaul Markovitch Computer Science Department Technion - Israel Institute of Technology Haifa 32000, Israel Abstract The size and complexity of software and hardware …
Step 1. * Download the choco-solver 4.0.4 from: https://github.com/chocoteam/choco-solver/releases/tag/4.0.4 * unzip the choco-4.0.4.zip, and place it in the directory.Step 2. Setting for Scala Eclipes IDE * Right click the target package,…
cat -e filename
複数あるファイルの中から特定の文字列を検索したいときのLinuxコマンド。 $ find ./ -type f -print | xargs grep ‘hoge’
Why the model checking technique is successful for HW verification, and failing for SW verification?
Why the model checking technique is successful for HW verification, and failing for SW verification? For HW verification, HW like digital circuits are easy to model checking. But for SW, SW is usually so huge, we can only apply MC for abst…
林晋さんのこと、根拠なきイチャモンのことhttp://d.hatena.ne.jp/m-hiyama/20151109/1447026954 いずれにしても、既存の方法や習慣とギャップがあると受け入れてもらえないので、今のやり方のなかに少しずつ形式性や厳密性を注入していくしかないような気が…
Incremental software development
Emacs はそのままでは redo に対応しておらず、redo をしようとすると拡張する必要がある。redo+ はその一つである。インストール方法は M-x install-packages でみようとしたが、"marmalade" にも、"melpa-stable"にも no match といわれ、少しはまった。今…
ensime とかあるようだが、まずはお試しで使うための手っ取り早い方法。emacs で scala mode をインストールすると、emacs メニューに「scala」が現れる。実行したバッファ上で、このメニューにある「scala->Run Interpreter」をクリック。以降は、C-c C-l …
ペリエ＠アーカイブ: ubuntu 12.04 LTS alt+grave(`)を有効にする方法
Interlocking - GNU Emacs Manual M-x diff-buffer-with-file
http://www.kabipan.com/computer/emacs/emacsのinteractiveの使い方を整理し理解してみました - むかぁ～ どっと こむ
Git - 作業のやり直し ファイルへの変更の取り消しbenchmarks.rb に加えた変更が、実は不要なものだったとしたらどうしますか? 変更を取り消す (直近のコミット時点の状態、あるいは最初にクローンしたり最初に作業ディレクトリに取得したときの状態に戻す) …
TeX Forum 例えば W32TeX をインストールした場所が C:\w32tex だったとすると、 C:\w32tex\share\texmf-local\tex以下に置けば読み込み可能になります。普通は pLaTeX 専用のものは C:\w32tex\share\texmf-local\tex\platex 以下 欧文 LaTeX でも可能のもの…
macにnkfコマンドがないだと！？じゃあ入れよう！ - Qiita
I have installed Texlive in Cygwin, but it is too slow for compilations. Thus, I have come back to W32Tex.
【未解決】 cygwin から、open コマンドで起動したemacsで、M-x shell や 'compile したら、「apply: Spawning child process: invalid argument」がでる。普通に起動すると出来る。なぜだ。Path の関係かな。どなたか教えてください。
Lyx を入れようとすると、Cygwin が壊れたので、再インストールを試みた。Cygwin のアンインストールはフォルダの削除ということで、削除を試みるも、Cygwin が消えない。ちなみに以下を試した。 フォルダのプロパティ→「セキュリティ」でアクセス権を設定 …
git push origin tag-name $ git tag -l 2.11 $ git push --tags --repo="git@bitbucket.org:our_repo/webrequest.git" site / master / issues / #3468 - BitBucket does not show tags in git repository — Bitbucket
vim のだめな点 コンパイルコマンドを呼ぶと、vim を一旦閉じて、コンパイルをして、再度Vim を呼ぶ設定となっている。このため、コンパイルをした後に、undo ができない コンパイルが編集をブロックする。 これらは頑張れば回避できるのかもしれないが、頑…
■ 改行コードを知る。catコマンド # 行末(LF)に「$」・表示不可文字(CRなど)を「^M」で表示 cat -e ファイル名 # 行末(LF)に「$」・表示不可文字(CRなど)を「^M」・タブを「^I」で表示 cat -A ファイル名 ■改行コードを変換する（nkf） 主要なオプションは以…
2004年に出たJUnit本が予想以上に勉強になった。 - 感謝のプログラミング
Caller & Callee each other between Scala & Java
scala> :help All commands can be abbreviated, e.g. :he instead of :help. Those marked with a * have more detailed help, e.g. :help imports. :cp add a jar or directory to the classpath :help [command] print this summary or command-specific …
Following the information in Scalaプログラミング入門以下のサンプルコードを実行するとすると。 1: object Hello { 2: def main(args: Array[String]) { 3: println("Hello Kobe!") 4: } 5: } REPL を起動して、以下を実行。 # 私の場合、emacs のScalaモ…
以下を参考にhttp://mymemo.weby117.com/develop/emacs_9.htmlhaskell-mode パッケージが配布されているため、apt-get コマンドでインストール可能。ターミナルより以下を実行。$ sudo apt-get install haskell-modeEmacs設定ファイル .emacs に以下を追加。…
文字コードと改行コード | UNIX & Linux コマンド・シェルスクリプト リファレンス 使用されている改行コードを調べる 以下を実行。 file textfile 実行結果。 $ file lf.txt lf.txt: ASCII text ※↑ファイルの改行コードは LF (UNIX / Linux 形式)。$ file c…
MaxSAT Problem(s) MaxSAT: All clauses are soft Maximize number of satisfied soft clauses Minimize number of unsatisfied soft clauses Partial MaxSAT: Hard clauses must be satisfied Minimize number of unsatisfied soft clauses Weighted MaxSAT…
Example. Consider the following weighted partial MaxSAT instance. \phi_h = { (x1 ∨ x 2 ∨ ~x3 ),(~x2 ∨ x3 ),(~x1 ∨ x3 )} \phi_s = { (~x3 ,6),(x1 ∨ x2 ,3),(x1 ∨ x3 ,2)} (2) According to the described encoding, the corresponding PBO instance …
MAXSAT (ms) (standard MAXSAT ): no hard clauses and all clause have weight 1. Solution maximizes the number of satisfied clauses. Weighted MAXSAT (wms): no hard clauses. Partial MAXSAT (pms): have hard clauses but all soft clauses have wei…
