Sun Jan 20 10:44:41 JST 2008

うーん、たぶん、class Continuation を取り除くことは可能なんだろうな。

	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
		return sat.empty.sat(sat, new Continuation(sat,next,this));
	}

	@Override
	public ITLSolver next(ITLSatisfier sat,Continuation next, ITLSolver value) throws Backtrack { } ....

とかの代わりに、

	public ITLSolver sat(ITLSatisfier sat, Next next) throws Backtrack {
		return sat.empty.sat(sat, new Chop1(next));
       }

       class Chop1 implements Next {
            Next next;
            Chop1(Next next) {
                  this.next = next;
            }
            public ITLSolver next(ITLSolver value) {
                   if(value==null) 
		       return next.next(myValue);   // return case
                   return  var.sat(sat, new Chop2(next)); // call case
           }
       }

ぐらい? next を自分で持っていれば、いらない? Recursive call が
なければ。いや、あるか。この方が new Continuation がなくなる分、
速いよね。割と簡単に直せる?!

Chop1 とかが増えるのを嫌って汎用のContinuationを入れたんだけど、
どうせたくさんあるから、関係ないってことなのか。

done in 30032msec
-> show.
All Edges: 324099
Number of BDD: 12273
Number of Subterm: 70
Reachable state: 1366
-> 

done in 26869msec
-> show.
All Edges: 324099
Number of BDD: 12273
Number of Subterm: 70
Reachable state: 1366

あぁ、やっぱり少し速くはなるのか。

Sun Jan 20 01:30:04 JST 2008

とりあえず Release 。Release の時に Changes を入れないように
注意すること。

Sat Jan 19 12:18:24 JST 2008

　　　　public interface ITLNodeFactoryInterface<T> 

　　　　public class ITLNodeParser<Node extends ITLSolver>　　{
　　　　　　　　public ITLNodeParser(ITLNodeFactoryInterface<Node> lf) ;
　　　　}
　　　　public class ITLNodeFactory implements ITLNodeFactoryInterface<ITLSolver > ;

で、

　　　　p = new ITLNodeParser<ITLSolver>(new ITLNodeFactory());

だと、Eclipse で生成すると動く。実行時エラーはでない。でも、ant でbuildすると、
実行時に、

　　　　 [java] Exception in thread "main" java.lang.VerifyError: (class: lite/ITLNodeParser, method: <init> signature: (Llite/ITLNodeFactoryInterface;)
V) Bad type in putfield/putstatic

うーん、これは何故だ。 動くわけなの
で、一応、Generic は合ってはいるんだよな。

　　　　public interface ITLNodeFactoryInterface<T extends ITLSolver> 

とすると動くので、一種の型推論不足らしい。


Fri Jan 18 22:44:54 JST 2008

jar を作るようにCVSを直したが、危うくparser を消すところだった...

Fri Jan 18 14:19:49 JST 2008

SBDDSet をクリアするには、new SBDDFactory() すれば良いらしい。
subterms は、既に、ITLSolver (SBDDSet のkey)にセットされていて、
それをclear するのは難しいが、そのまま放置すれば重なることはない
ので、害はない。

new SBDDFactory() して、old SBDDSet の key order を修正して、
新しくBDDを構築してやれば、key のreorder が可能。key order 
を修正しても hash は変わらないので、hash table 中の位置は変
わらない。と言うことは、variable reorder では、SBDDSet を新
しく作る必要はないということか... 

ということは、BDDの大きさはHashTable の大きさとは関係ない
ということか! すべてのBDDがHashに登録されるんじゃないの?
reorder で使われなくなるBDDがあるってことなのか。ということは、
やっぱり、SBDDSet は変更されるということなのね。いや、
subterm は不変であって、pure BDD term は変わるということか。
確かに、
Number of BDD: 223
Number of Subterm: 81
なので、Subterm の方が少ない。

done in 36751msec
-> show.
All Edges: 283053
Number of BDD: 1802
Number of Subterm: 176
Reachable state: 1366

あ、なんか遅くなった。

Thu Jan 17 23:50:12 JST 2008

do(20).
done in 18762msec
exe.
0:483:  [~empty,al,~ar,~bl,~br,cl,~cr,~dl,~dr,~el,~er]
1:495:  [~empty,~bl,~br,ar,al,cl,cr,~dl,~dr,el,~er]
2:515:  [~empty,~bl,~br,ar,~al,cr,~cl,~dl,~dr,el,er]
3:565:  [~empty,bl,~br,~ar,~al,~cl,~cr,dl,~dr,er,~el]
4:666:  [~empty,~al,~ar,~cl,~cr,br,bl,dr,~el,dl,er]
5:1112: [empty,~al,ar,~cl,cr,~bl,br,~dl,dr,~el]

diag, exe も、なんとなく動いているし、MainLoop に、jar のresource
からの読み込みも出来たし。ほとんど、終った気がする。いろいろ謎な
部分は残っているけど。

jar にも出来たし。

MainLoop のプロンプトとか。

README と Licence か。

あと、何が可能かと言うと...

    LTTL version (QPTL も)   Eventurity flags とsatisfiability checker
    Characteristic Function Version
          Implicit State Enumeration
    外部BDD Library との接続
    並列version

    KISS format の読み込み/生成
    VHDL/Verilog の生成
    CbC の生成

かな。

Thu Jan 17 19:05:42 JST 2008

| ?- (a & b & c) = (P & Q ).
P = a,
Q = (b&c) ? 

ってことにいまさら気づきましたが...  xfy って、そういう意味か。
逆に実装しちまったい。

一般的には、(a & (b & c)) = ((a & b) & c) だが、&& の定義が
だめ。

Thu Jan 17 03:43:53 JST 2008

order を出現順に直しました。

BDDSolver は、ITLSolver と違うので、継承したらだめなのね。

Wed Jan 16 14:32:09 JST 2008

diag も書きましたが、テストする気がしない...

free arity なマクロが欲しいかな... def("ex(...)","true")  みたいな?
define_varargs() かな。

Tue Jan 15 16:20:05 JST 2008

途中で、既に展開したnodeが出て来たときに、satisfiable のflag
を間違えるらしい。state 毎にflagを持っている方がいいのかな。

Lite 自体は、logicNode とかverifierに縮退する必要はないので、
そちらを切り離した方が良いかも知れない。

weak next をbaseにすると、~empty,next() がたくさん出て来る。
strong next base の方が合理的なのかも。そういえば、always とかも
持っていた方が良いと言う考え方も出来るけど...

Sun Jan 13 19:20:10 JST 2008

あぁ、ordered BDD になってないよ〜

一応、出来たかな? まだ、少しsyntax error とか残っているけど。

あとは、GUI と、diag (valid,unsatisfiable,counter example, execute)
かな。そのためには、
   on-demaned state generator 
がいるね。そうしないと、巨大な状態遷移を二つ持つことが必要になる。

Fri Jan 11 14:23:21 JST 2008

(empty & Hoge)が、なんかはびこって、項の大きさを大きくしているらしい。
つうか、これがあると収束しないです。でも、それを取るぐらいではだめ
ならしい。

projection(C,I) のtermination は、I 項のverification が収束すること
に依存しているので、I項に Projection が入っていると、projection の
ネストの帰納法で証明する必要がある。

ということは、I の方がちゃんと正規形になって有限の項の組合
せであることを示す必要がある。I の方を前もって展開してしま
うという手もあるけど。つまり、安易な最適化を入れて収束して
も、それがtermination の証明にならないということ。

SDDEntry.expanded は、展開されたのはなくて生成されてqueueに
入れた時点でtrueにして良い。こうすれば、queue の中には unique
な項しか入らないことになる。

どうも、BDDのor で、うまく (empty & true ) を処理できてないっぽい。

Thu Jan 10 13:28:26 JST 2008

hasChoicePoint は、variable 毎にフラグで持っても良い。
その方が linear search しなくて良いので少し速い。
けど、exists との相性は悪い。(かな?)

exists は、true/false にセットしたところで、try/catchしないと
だめらしい。(chop はいいのか? 悪いとしたら、それをテストする
例は?)

weak next をbaseにした方が
     @p =  next(p),~empty
で、~empty が他と共有されるので調子が良い。

Wed Jan  9 20:42:17 JST 2008

あぁ、そうか。
    define("forall(x,body)","~exists(x,~body)");
    forall(a,(a;~a))
では、 body は、exists に入る前に、(a;~a) に換えられちゃうので、
exits は、その既に換えられてしまったa をlocal 変数にするこ
とが出来ないわけね。名前は同じなんだけど。

なので、変数を扱う時には、一旦、var = lf.variableNode(var.name);
みたいなことをやっていたわけか。まぁ、それがいいのかなぁ。


Tue Jan  8 02:16:17 JST 2008

    Sat 
    Parser 
    Macro
    Scanner test
    ITL
    SBDD

まぁ、結構書いたね。

Mon Jan  7 15:11:55 JST 2008

verifier まで動きました。

empty はparserでvariable に変換していたのを忘れてました。

何故か同じ形で二度展開されるものがある。

あとは、例題を全部動かせば良いだけか。Interval variable
もやるか?

この方法だと、variable をtryする順序が固定なので、order的には、
2^v * (sbdd term の組合せ) となる。これは、遅いよね。
印刷すると遅いけど、印刷されたものをすべてたどっているわけではないん
だが...

variable の順序を見つけるのにだけ、SATを使えばいいんじゃないか?
といっても、sbdd term の組合せだけ用意しないとだめか。

     develop
       find sat variable order by SAT

という感じか?

Sun Jan  6 23:09:31 JST 2008

まぁ、一応、展開できるところまでできたか...

empty の扱いがまだおかしい。local なものがちゃんと restore されてる?

CPS なプログラムの debug の方法が良くわからない。

BDD を外部(JavaBDD)にするかどうかよりも、先に、このあたりを片付けないと
だめか。BDD を外部に出すのは、それほど難しくなさそう。

state queue を持たずに、それも BDD で行う、Charcteristic function を
使う方法もあるのだが、BDDがでかくなるんだよな〜

CbC のプログラムを吐くのも難しくはないはず。

Sat Jan  5 14:26:35 JST 2008

BDDSolver が自分がTrue/False かどうか判断できないって、どうよ...

Wed Jan  2 12:16:38 JST 2008

Quantifier の変数だけど、classical logic の場合は、quantifierに
別な変数を割り振っておけば良いんだが、tableau 展開する場合は、
同じものが含まれてしまうことがある。新しい変数を、その場で
獲得する方が良いだろう...

でも、state に登録するときには、形を同じにしないとだめ。

Wed Jan  2 04:16:08 JST 2008

あとは、itlstd に相当するものを書けば良いだけ。sat のlf を
呼んでいるので、factory 側で、登録してやれば良いらしい。
prestate とかも、そこで出来るかな。

Tue Jan  1 22:49:40 JST 2008

まぁ、だいたいパーサは出来たんですが... LogicSolver と 構文木が
一緒なのは無理がある。まぁ、あとで別なものを生成してもいいか。

Token <-> LogicNode という双方向リンクにしても良い。C と違って、
String は、たぶん、hash されているので、string eq でプログラミング
しても別にいいかも。

NodeFactory のInterface が多すぎる。predicateNode だけにして、
後は、中で判定する方が良いだろう。

そうすれば、expr* も減るはず。

Mon Dec 31 10:04:14 JST 2007

   LinkedList<? extends LogicNode> という技があるらしいです。

Simple Loic Node は String name を持っているが、Token を
持つ方が良い。Operator order は、そっちにあるので。

Sat Dec 29 18:29:41 JST 2007

えーと、Node にアクセスせずに Parser するのは無理だよね?
     Parser<Node>
という形だと、Node の中にアクセスできない。 
     Parser<Node extends LogicNode>
とすると、

     LogicSolver extends LogicNode

とする必要があるが、そうすると、

    LinkedList<LogicNode> arguments();
    LinkedList<LogicSolver> arguments();

が衝突してしまう。なので、今までは、

     LogicSolver extends LogicNode

とはしてなかった。(これが結構変...)


	// @Override
    public LinkedList<LogicSolver> arguments(LogicSolver n) {		return null;	}
	

で通るけど、それも変だなぁ。

Fri Dec 28 04:10:45 JST 2007

Macro 展開と、Scanner は出来たけど...

infix operator をどうしようか? まぁ、それが終れば、
あとは、難しくないはず。

Operator の順位を入れるんだけど... どうすれば良いのか
わからん。

    a + b * c  ==>  a + (b * c)
          n1 = expr*();
	  if ( next == '+' ) {
	      n2 = expr+();
	      return op+(n1,n2);
	  } 
	  return n1;

    a + b * c  ==>  (a + b) * c
          n1 = expr*();
          while( op == '+') {
	      next();
	      n2 = expr*();
	      n1 = op+(n1,n2);
	  }
          return n1;

じゃぁ、while でbreakすれば良いだけか。(違うな...)

          n1 = expr*();
          if (op.order(n1,'+')) {
		while( op == '+' ) {
		    n2 = expr*();
		    if (op.order(n2,'+')) {
                        return op+(n1,n2);
                    }
                    n1 = op+(n1,n2);
                }
          } else {
              n2 = expr+();
              return op+.order(n1,n2);
          }

こうかな?

うぅ、わからん。

Macroを入力ファイル側で定義するようにすることも、まぁ、
可能だけどね。


	private Node exprM3() {
		Node n1 = expr3();
		while (nextToken!=null && !nextToken.isInfix()) {
			Node op = makeVariable(nextToken);
			LinkedList<Node> arg = new LinkedList<Node>();
			if (nextToken.order(n1)) {
				nextToken();
				Node n2 = expr3();
				arg.add(n1);
				arg.add(n2);
				n1 = logicNodeFactory.predicateNode(op, arg);
			} else {
				arg.add(n1); arg.add(exprM3());
				return logicNodeFactory.predicateNode(op, arg);
			}
		}
		return n1;
	}

こんな感じ?

Thu Dec 27 00:47:45 JST 2007

あぁ、なんか、はまりすぎ。ITLのparserだけで、まだ、
かなりかかりそう。で、その後に、展開器と、状態の
格納か。そういえば、JBDDってのがあったはずだが...

Thu Dec 20 12:53:23 JST 2007

Boolean Satisfier は出来ました。
((not a) or a) is satisfiable.
(not ((not a) or a)) is unsatisfiable.
exists(a,((not a) or a)) is satisfiable.
(not exists(a,((not a) or a))) is unsatisfiable.

Backtrack をProlog流にやろうとすると、Tree walk をCPS変換す
る必要があるってのに気づいた後は楽勝でした。しかし、普通の
言語でそれをやろうとすると面倒だよなぁ。

backtrack base depth first search をtry/catch で実装したが、
Iterrator とか Thread Pool で実装することも可能だと思った。
try/catch が余りに遅いなら書き直すでしょう>。(実際、遅いん
だけどさ) 

Parser に二種類のノードを生成させるようにするので、ちょっと
はまる。まぁ、コピペしても良いんだけどさ。Node の生成をFactory
経由にすれば良いんだが... 

CPS変換はInner Class を使っていたんだけど、やっぱり外部が良
いなと思って書き直しました。Inner Class の方が記述が一ヶ所
に集まるので読みやすい感じもするけどね。

Factory はInterfaceにするのかClass にするのかで、2,3回往復
したらしい。Down cast > を実行時に拒否するので、アドホック
に書かせてくれない。で、結局、Generic に書き直>す羽目に。そ
んなところで時間を取られるのは本質的でない気がする。学生だ
ったら絶対> コピペで済ますだろうな。Generic にRefactoringす
るってのは、Eclipse には存在しないらしいです。(そりゃそうだ
ろう...) 

　      public TreeMap<String,Token<Node>> scope;

とか書くと、C++ みたいで嫌な感じ。(と思う人は多いだろう...)
1.5 以前は、Java はca stしまくりだったんだけどね。

ATVAで聞いた話ではSATは「簡単なことは全部その場でやる」「難
しいものは出来るだけ後回しにする」手法が良いようです。一種
のShort Job First だね。

Thu Dec 20 05:16:45 JST 2007

Inner class を取り除きました。

探索順序とか変数の順序とかを自由に扱える方がいいんだけど。

Parser にマクロがあった方が良い。

Thu Dec 20 04:13:36 JST 2007

なんか動いた。try/catch continuation based だが...

Parser が CSE を見るべきだよね。そして、link count を見て、
link があるなら、value を keep するべきでしょう。

木の大きさ、変数の数を見て、より小さいものを先に計算する方が良い。
これも、Parse 時にわかるはず。

valid/unsatifsiable なノードは、true/false に置き換える。

ぐらいは、やるか...

ということは、部分項からbottom up に計算する方がいいのか? (まさか...)

Wed Dec 19 18:35:35 JST 2007

Parser をgenericにしないと、Specialize されたノードを作れない...

Mon Dec 17 13:18:25 JST 2007

LogicNode 自体を拡張するなら継承するべきでしょ。

だとすると、Parser とかではFactory経由でオブジェクトを作らないとだめ。
ということか。まぁ、それはあとで。

もっとも、satifier の作り方自体が良くわからない。Iterator を返すのは
悪いとは思わないが... 

staifier はIterator のリストを管理して、その端から可能な選択肢を探す
という感じか?

Sun Dec 16 21:32:38 JST 2007

単純なsat checker でも難しいね。

Lite のを正確にたどろうとしているわけだが...

まぁ、varlist を作って、それを変更して行くと言うのでも
出来ないことはないんだが、それだと、計算の重複が
大きすぎる。