Thu Jan 17 23:50:12 JST 2008

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 を作って、それを変更して行くと言うのでも
出来ないことはないんだが、それだと、計算の重複が
大きすぎる。