DBAN というソフトウェアがよく使われているようだ．
現在の版 (2.2.x) は，CD の iso イメージとして配布されているが，
USBメモリを起動デバイスにすることもできる．
方法が書いてあるページ．
HeuristicSearch.java を見てみる．
キューには HeuristicState というものが入っている．
キューから hs をとりだして，
HeuristicSearch.restoreState(hs)を呼ぶと復元される．
この実体は，vm.restoreState(hs.getVMState())．(そのあと
depthを設定したりする)
getVMState() は，RestorableVMState 型で，この値は
保存しようとする時に vm.getRestorableState() を呼ぶことで，
RestorableState のコンストラクタを引数vmで呼んで作られる．
RestorableState クラスの注釈には，これを作るのは非常に
重い操作である，と書いてある．
RestorableState のコンストラクタでは，
Path path と
Backtracker.RestorableState bkstate
が，おのおの vm.getClonedPath() と
vm.getBacktracker().getRestorableState() で設定される．
前者はその時点の path の deep copy で，CGやtransaitionたちの
cloneが作られる．
後者は，
savedKstack = kstack;
savedSstack = sstack;
kcur = restorer.getRestorableData();
scur = ss.getRestoreData();
を実行．
savedKstack, SavedSstack,
kcur, scur
左辺にあるものたちは，DefaultBackTracker.RestorableStateImpl の
フィールド:
final ImmutableList<KState> savedKstack;
final ImmutableList<Object> savedSstack;
final KState kcur;
final Object scur;
右辺にあるものたちは，DefaultBackTracker クラスで
protected ImmutableList<KState> kstack; protected ImmutableList<Object> sstack; protected StateRestorer<KState> restorer; protected SystemState ss;
と定義されている．sstack は SystemState 関連であろう．
restorer.getRestorableData() は，いろいろ複雑にたどらされて
(何かのデザインパターンだろうか?) 結局，
threadsMemento = ks.threads.getMemento();
cloadersMemento = ks.classLoaders.getMemento();
heapMemento = ks.heap.getMemento();
を実行する．型は名前からわかるように以下の通り．
Memento<ThreadList> threadsMemento;
Memento<ClassLoaderList> cloadersMemento;
Memento<Heap> heapMemento;
ss.getRestoreData は，SystemState.RestorableMemento クラスの
オブジェクトを作る．
(…書きかけ…)
JPF の Choice Generator，というか，ChoiceGeneratorBase
protected ChoiceGenerator prev;
このフィールドには，現在のパス上で直前に設定されたChoiceGeneratorが入っている．
したがって，Heuristic Search のような場合には，CG の deep clone が走ることになって，重いということに
なる．
さらに，同一の transition で複数のCGがある場合には，親の方のCGのフィールド
boolean isCascaded;
にtrueが設定されることになっている．
データ定義部分を中心にいい加減に抜粋
class KernelState implements Restorable{ public Heap heap; public ThreadList threads; public ClassLoaderList classLoaders; private Stack listeners; // current listeners waiting for notification of next change. static class KsMemento implements Memento { Memento threadsMemento; Memento cloadersMemento; Memento heapMemento; public KernelState restore (KernelState ks) {...} } ... }
public class SystemState {
static class Memento {
ChoiceGenerator curCg;
ChoiceGenerator nextCg;
int atomicLevel;
ChoicePoint trace;
ThreadInfo execThread;
int id; // the state id
LinkedHashMap restorers;
...
void restore (SystemState ss) {...}
}
static class RestorableMemento extends Memento { // expensive
void backtrack (SystemState ss) {...}
void restore (SystemState ss) {...}
}
int id; /** the state id */
ChoiceGenerator nextCg;
ChoiceGenerator curCg;
ThreadInfo execThread;
LinkedHashMap restorers;
public KernelState ks;
public Transition trail; /** trace information */
boolean retainAttributes;
boolean isIgnored;
boolean isForced; // treat this as a new state
boolean isInteresting;
boolean isBoring;
boolean isBlockedInAtomicSection;
public UncaughtException uncaughtException;
boolean GCNeeded = false;
int maxAllocGC; // for an optimization
int nAlloc; // for an optimization
int atomicLevel;
int entryAtomicLevel;
SchedulerFactory schedulerFactory;
boolean recordSteps;
...
}
EclipseでのWindowsの分割方法 (1つのファイル) はこの記事にある．
水平方向は Ctrl-_ ，垂直方向は Ctrl-{ ．
元に戻すにはもう一度同じキーを打つ．
2つのファイルを表示するには，2つめを表示しているタブをdrag して，線が現れるところでdropすれば良い．
キーワード: eclipse window view split
myfaxというのを使ってみた．メッセージに日本語は書けないらしいが，一応使える．送るべきものをまずpdfにしておけばよい．
keyword: internet fax
Windows7 と ATOK2015 と Powerpoint 2013 との組み合わせで問題が生じた．
日本語 ON/OFF 機能をあるキー (Ctrl-0) に割り当てていたのだが，Powerpoint 2013の時だけ，このキーが効かない．Excel 2013 や Word 2013 だと，ちゃんと機能する．
また，標準の Alt-` は，ただしく動作する．いくつか他のキーの割当も試みたがうまくいかない．一方，Ctrl-0 を，他の機能 (たとえば日本語ON) に割り当てると，正しく動作する．
JUST system のサポートに問い合わせてみた．
(電話での問い合わせしかできないのに驚いた．)
問題が報告されていて，なんと，日本語 ON/OFF 機能が2回働いてしまう，とのこと．
Powerpoint側の問題だと言っていた．
ATOK側での対処が可能で，プロパティ -> 入力・変換 -> 設定項目 -> 入力補助 -> 特殊 -> テキストサービスの詳細設定 -> テキストサービスを使用する と設定すれば良いとのこと．
ただ，この項目のデフォルトは「使用する」であって，数年前 (ATOK2012の頃かな) にこれを「使用する」のままにしておくといろいろ不具合がある，ということで「使用しない」としたのだった．実際，「使用する」にしたら，タスクトレイにアイコンを出すことができなくなってしまった．
少し検索して実験して，この項目は「使用しない」のままで，以下のようにすれば良いことが判明: 言語バー -> 設定 -> インストールされているサービス -> Microsoft Office IME 2010 -> プロパティ-> その他 -> 詳細なテキストサービス -> 詳細なテキストサービスを使用しない．これでめでたくPowerpointも動き，タスクトレイアイコンも出すことができた．
要は「テキストサービス」なるものをできるだけ使わないようにすると良いということか?? しかし，これを「使用しない」にすると不具合が生じたという報告例もあるので，しばらく使ってみないとわからない．
Web meeting をしようと思ったのに，ThinkPad X240 のカメラが
動作しない．写真機上に斜めの線が入ったアイコン (右図) が表示されるだけ．
どこかで設定がOFFになっているのだろうと思ったが，見つからない．
いろいろ探してやっとわかった:
コントロールパネル -> デバイスとプリンター -> デバイス -> (ThinkPad本体)
-> Lenovo Think Vantage Tools -> Web会議 -> カメラの設定
-> ビデオ・イメージを表示する．
こんなところにあってもわかんないよ…
SSReflect の case タクティックは，否定 (not, ~ A) に関しても場合分けしてくれる．
だが，その前に，普通のを見てみる．
============================ forall b : bool, b -> G
という状況で，case. とすると，
2 subgoals, subgoal 1 (ID 10) G : Prop ============================ true -> G subgoal 2 (ID 11) is: false -> G
となる．そりゃそうだ．
inductive type を値の型とする関数も case ができるようだ．
実験してみるとなかなか不思議な仕様であるように思われる:
1 subgoals, subgoal 1 (ID 3) f : nat -> bool ============================ f 3 && f 2 == f 1
この状況で， case f. とすると，
2 subgoals, subgoal 1 (ID 4) f : nat -> bool ============================ true && f 2 == f 1 subgoal 2 (ID 5) is: false && f 2 == f 1
となる．うーむ．ま，それはそれとして，適用するものがないと，作れと要求される．
1 subgoals, subgoal 1 (ID 2) f : bool -> bool ============================ nat
この状況で，case f. とすると，
3 subgoals, subgoal 1 (ID 3) f : bool -> bool ============================ bool subgoal 2 (ID 4) is: nat subgoal 3 (ID 5) is: nat
となる．順に，場合分けに使うfの定義域の値の要求，値が true の場合と false の場合の
nat値の要求，となっている．実際，case f. の代わりに
case f; [exact true | exact 10 | exact 20]. とすると
定義ができて，Print してみると，
fun f : bool -> bool => if f true then 10 else 20
: (bool -> bool) -> nat
となる．
やっと本題．こういうわけなので，
============================ ~ A -> G
という状況で，case.すると，
~A は，関数 A -> False のことなので，
A のどの値で見るか，というのを尋ねる1個と，False の constructor の数 ( = 0 個) の
和の分だけの subgoal ができるわけで，
============================ A
となる．