# HG changeset patch
# User kono
# Date 1200582027 -32400
# Node ID f6976310625795917ee7b251b35f54f81c5e6272
# Parent  e70b8c36ec0a413807ef9e8448dc5654dbf0a319
*** empty log message ***

diff -r e70b8c36ec0a -r f69763106257 Changes
--- a/Changes	Thu Jan 17 21:23:11 2008 +0900
+++ b/Changes	Fri Jan 18 00:00:27 2008 +0900
@@ -1,11 +1,39 @@
+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) ? 
 
-ってことにいまさら気づきましたが... 一般的には、
-(a & (b & c)) = ((a & b) & c) だが、&& の定義が
+ってことにいまさら気づきましたが...  xfy って、そういう意味か。
+逆に実装しちまったい。
+
+一般的には、(a & (b & c)) = ((a & b) & c) だが、&& の定義が
 だめ。
 
 Thu Jan 17 03:43:53 JST 2008
diff -r e70b8c36ec0a -r f69763106257 src/lite/MainLoop.java
--- a/src/lite/MainLoop.java	Thu Jan 17 21:23:11 2008 +0900
+++ b/src/lite/MainLoop.java	Fri Jan 18 00:00:27 2008 +0900
@@ -1,5 +1,6 @@
 package lite;
 
+
 import sbdd.BDDSatisfier;
 
 public class MainLoop {
@@ -7,7 +8,8 @@
 	public static void main(String arg[]) {
 		BDDSatisfier sat = new BDDSatisfier();
 		// read predefined examples
-		sat.p.parseFile("data/example");
+		if (!sat.p.getResource("/data/example"))
+			sat.p.parseFile("data/example");
 		sat.p.help();
 		sat.p.parse(System.in);
 	}
diff -r e70b8c36ec0a -r f69763106257 src/sbdd/SBDDTest.java
--- a/src/sbdd/SBDDTest.java	Thu Jan 17 21:23:11 2008 +0900
+++ b/src/sbdd/SBDDTest.java	Fri Jan 18 00:00:27 2008 +0900
@@ -1,6 +1,10 @@
 package sbdd;
 
 
+import java.io.IOException;
+import java.io.InputStream;
+import java.net.URL;
+
 import lite.BDDSolver;
 import lite.ITLNodeParser;
 import lite.ITLSolver;
@@ -17,8 +21,8 @@
 		SBDDTest test = new SBDDTest();
 		
 		//test.satTest();
-		test.verifyTest();
-		//test.mainLoop();
+		//test.verifyTest();
+		test.mainLoop();
 		//test.bddTest();
 	}
 	
@@ -94,15 +98,34 @@
 		sat.p.parse("include('data/example').");
 		//System.out.println(p.parseCommand.sat.state);
 		sat.showVerify("length(2),[]p");
+		sat.p.parse("do((length(10),fin(p)))");
+		sat.p.parse("exe");
 		sat.p.parse("do(10)");
-		sat.showVerify("do((length(10),fin(p)))");
-		sat.p.parse("exe");
+		sat.p.parse("diag");
 
 	}
+	
+	public boolean getResource(BDDSatisfier sat, String filename) {
+		System.out.println("try to get "+filename);
+	        try {
+				URL rsrc = getClass().getResource(filename);
+				if (rsrc==null) throw new IOException();
+				InputStream in = rsrc.openStream();
+				sat.p.parse(in);
+				return true;
+			} catch (IOException e) {
+				System.out.println("... failed.");
+				return false;
+			}
+		}
+
 
 	public void mainLoop() {
 		BDDSatisfier sat = new BDDSatisfier();
-		sat.p.parseFile("data/example");
+		if (getResource(sat,"/data/example")) {
+			System.out.println("read from jar file");
+		} else
+			sat.p.parseFile("data/example");
 		sat.p.parse(System.in);
 	}