Mercurial > hg > Applications > JavaLite

changeset 84:e70b8c36ec0a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Almost completed.
author kono
date Thu, 17 Jan 2008 21:23:11 +0900
parents 66719d0834f3
children f69763106257
files Changes build.xml src/Lite.mf src/lite/ITLNodeParser.java src/sbdd/BDDDiagnosis.java src/sbdd/BDDSatisfier.java src/sbdd/SBDDTest.java
diffstat 7 files changed, 72 insertions(+), 16 deletions(-) [+]
line wrap: on
line diff
--- a/Changes	Thu Jan 17 20:56:31 2008 +0900
+++ b/Changes	Thu Jan 17 21:23:11 2008 +0900
@@ -1,3 +1,13 @@
+Thu Jan 17 19:05:42 JST 2008
+
+| ?- (a & b & c) = (P & Q ).
+P = a,
+Q = (b&c) ? 
+
+ってことにいまさら気づきましたが... 一般的には、
+(a & (b & c)) = ((a & b) & c) だが、&& の定義が
+だめ。
+
 Thu Jan 17 03:43:53 JST 2008
 
 order を出現順に直しました。
--- a/build.xml	Thu Jan 17 20:56:31 2008 +0900
+++ b/build.xml	Thu Jan 17 21:23:11 2008 +0900
@@ -16,6 +16,30 @@
         </java>
     </target>
 
+    <target name="jar" depends="build">
+<!--    <mkdir dir="dest/jar"/> -->
+<!--
+    <copy todir="dest/jar">
+    　<fileset dir="data">
+    　　<include name="*"/>
+    　</fileset>
+    </copy>
+ -->
+    <jar jarfile="../Lite.jar" basedir="." manifest="Lite.mf"/> 
+<!--    <jar jarfile="dest/jar/Lite.jar" basedir="dest" manifest="Lite.mf"/> -->
+<!-- <copy file="prop.properties.package" tofile="dest/jar/prop.properties"/> 
+   -->
+    </target>
+
+    <target name="srcJar">
+    <jar jarfile="src.jar">
+    　<fileset dir=".">
+    　　<include name="**/*.java"/>
+<!--    　　<exclude name="sample/**"/> -->
+    　</fileset>
+    </jar>
+    </target>
+
     <!-- clean -->
     <target name="clean">
         <delete>
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Lite.mf	Thu Jan 17 21:23:11 2008 +0900
@@ -0,0 +1,3 @@
+Manifest-Version: 1.0
+Created-By: 0.1.0 (Shinji KONO @ University of the Ryukyus)
+Main-Class: lite.MainLoop
--- a/src/lite/ITLNodeParser.java	Thu Jan 17 20:56:31 2008 +0900
+++ b/src/lite/ITLNodeParser.java	Thu Jan 17 21:23:11 2008 +0900
@@ -33,10 +33,13 @@
 		parseCommand = new ITLCommander<Node>(lf,this);
 		
 			define("not(P)","~P");                               // not
-			define("P->Q","(not(P);Q))");                         // imply
+			define("P->Q","(not(P);Q))",101);                         // imply
 			define("P<->Q","((not(P);Q),(P; not(Q)))");            // equiv
 			define("P=Q","((not(P);Q),(P; not(Q)))");              // equiv 
-			define("P && Q","((not(empty),P) & Q))");             // strong chop
+			// P&&Q have to be left associative ( xfy i.e. a&&b&&c = a&&(b&&c)
+			// odd order means xfy associativity. & is right associative (yfx) in this
+			// parser, but & has associative, so it is alright. (&& is not assosicative)
+			define("P && Q","((not(empty),P) & Q))",901);             // strong chop
 			define("'<>'(Q)","(true & Q))");                        // sometime
 			define("'#'(Q)"," not(true & not(Q)))");                // always
 			define("'[]'(Q)"," not(true & not(Q)))");               // always
--- a/src/sbdd/BDDDiagnosis.java	Thu Jan 17 20:56:31 2008 +0900
+++ b/src/sbdd/BDDDiagnosis.java	Thu Jan 17 21:23:11 2008 +0900
@@ -4,9 +4,6 @@
 import java.util.LinkedList;
 import java.util.TreeSet;
 
-import lite.ITLSolver;
-import verifier.ChoicePointList;
-
 public class BDDDiagnosis {
 
 	/*
@@ -68,19 +65,17 @@
 		SBDDEntry last = trace.getLast();
 		int i = 0;
 		for(SBDDEntry e: trace) {
-			System.out.print(i+":"+e.id+":\t");
-			if (e!=last) {
-				ChoicePointList<ITLSolver>cp = 
-					sat.findNext(e,trace.get(i++));
-				System.out.print(cp);
+			if (e!=last) { 
+				System.out.print(i+":"+e.id+":\t");
+				System.out.println(	sat.findNext(e,trace.get(++i)));
 			}
-			System.out.println();
 		}
 	}
 
 	private LinkedList<SBDDEntry> findTrueEntry(SBDDEntry e, int length) {
 		SBDDEntry dest = true_;
 		LinkedList<SBDDEntry> trace = new LinkedList<SBDDEntry>();
+		trace.addLast(dest);
 		makeReachableEntry(e);
 		if (specialCase()) return trace;
 		dest = trueSet.first();
@@ -90,6 +85,7 @@
 	private LinkedList<SBDDEntry> findFalseEntry(SBDDEntry e, int length) {
 		SBDDEntry dest = false_;
 		LinkedList<SBDDEntry> trace = new LinkedList<SBDDEntry>();
+		trace.addLast(dest);
 		makeReachableEntry(e);
 		if (specialCase()) return trace;
 		dest = falseSet.first();
@@ -200,6 +196,7 @@
 		trace.addFirst(e);
 		if (e==start) throw new Result();
 		for(SBDDEntry p: reachable) {   // linear serach ?! should we create reverse index?
+			if (trace.contains(p)) continue; 
 			if (p.nexts!=null && p.nexts.contains(e)) {
 				if (p==start)
 					if (length<=0) throw new Result();
--- a/src/sbdd/BDDSatisfier.java	Thu Jan 17 20:56:31 2008 +0900
+++ b/src/sbdd/BDDSatisfier.java	Thu Jan 17 21:23:11 2008 +0900
@@ -174,6 +174,7 @@
 		for(SBDDEntry e;(e = queue.poll())!=null; ) {
 			System.out.println(e.id+":"+(verbose?e.key+"->":"")); 
 			currentState = e; falsifiable=false; satisfiable = false;
+			cp.clear();                           // all choice point is searched and removed
 			develop(e.key, allNext);
 			// this flag is work on current state
 			// to check validity/unsatisfiability, full check is required.
@@ -186,10 +187,25 @@
 		return sf.hash.getEntry(key);
 	}
 
+	class FindOne implements Next {
+		SBDDEntry dest;
+		public ChoicePointList<ITLSolver> cp;
+		public FindOne(SBDDEntry next) {
+			this.dest = next;
+		}
+		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
+			if (value!=null && state.getEntry(value)==dest) {
+				cp = sat.cp; return null;
+			}
+			throw sat.backtrack;
+		}
+	}
 
-	public ChoicePointList<ITLSolver> findNext(SBDDEntry e, SBDDEntry entry) {
-		// TODO Auto-generated method stub
-		return null;
+	public ChoicePointList<ITLSolver> findNext(SBDDEntry now, SBDDEntry next) {
+		FindOne findOne = new FindOne(next);
+		cp.clear();
+		develop(now.key, findOne);
+		return findOne.cp;
 	}
 	
 }
--- a/src/sbdd/SBDDTest.java	Thu Jan 17 20:56:31 2008 +0900
+++ b/src/sbdd/SBDDTest.java	Thu Jan 17 21:23:11 2008 +0900
@@ -91,10 +91,13 @@
 		//sat.showVerify("a?(x;(b?x:c)):false");
 		// sat.showVerify("+(a & b)");
 		//System.out.println(sat.state);
-		//sat.p.parse("include('data/example').");
+		sat.p.parse("include('data/example').");
 		//System.out.println(p.parseCommand.sat.state);
-		//sat.p.parse("do(10)");
 		sat.showVerify("length(2),[]p");
+		sat.p.parse("do(10)");
+		sat.showVerify("do((length(10),fin(p)))");
+		sat.p.parse("exe");
+
 	}
 
 	public void mainLoop() {