# HG changeset patch
# User kono
# Date 1200759176 -32400
# Node ID ec609dbb13a750f272a03f03cbcf6c854155c4f7
# Parent  df74b1a85d3a6eeec3211064b3664882d6c65185
*** empty log message ***

diff -r df74b1a85d3a -r ec609dbb13a7 README
--- a/README	Sat Jan 19 12:32:43 2008 +0900
+++ b/README	Sun Jan 20 01:12:56 2008 +0900
@@ -1,14 +1,17 @@
 LITE: A little LITL Verifier version 0.1
 
- Copyright (C) 1994,1991,2008
- Shinji Kono (kono@ie.u-ryukyu.ac.jp)
-   University of the Ryukyus
-   The University, Newcastle upton Tyne
-
- Everyone is permitted to copy and distribute verbatim copies
- of this license, but changing it is not allowed.  You can also
- use this wording to make the terms for other programs.
-
+************************************************************************
+** Copyright (C) 1994,1991,2008
+** Shinji Kono (kono@ie.u-ryukyu.ac.jp)
+**   University of the Ryukyus
+**
+**    Everyone is permitted to do anything on this program
+**    including copying, modifying, improving,
+**    as long as you don't try to pretend that you wrote it.
+**    i.e., the above copyright notice has to appear in all copies.
+**    Binary distribution requires original version messages.
+**    You don't have to ask before copying, redistribution or publishing.
+**    THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE.
 
 Files
     README		This file
diff -r df74b1a85d3a -r ec609dbb13a7 build.xml
--- a/build.xml	Sat Jan 19 12:32:43 2008 +0900
+++ b/build.xml	Sun Jan 20 01:12:56 2008 +0900
@@ -7,7 +7,8 @@
   <property name="test" value="sbdd/SBDDTest"/>
 
   <target name="build">
-    <javac encoding="UTF-8" srcdir="src" >
+    <mkdir dir="build"/> 
+    <javac encoding="UTF-8" srcdir="src" destdir="build">
         <sourcepath>
 	 <pathelement path="src"/>
         </sourcepath>
@@ -19,7 +20,7 @@
         <java classname="${main}" fork="yes" >
         <jvmarg value="-Dfile.encoding=UTF8"/>
         <classpath>
-	 <pathelement path="src"/>
+	 <pathelement path="build"/>
         </classpath>
         </java>
     </target>
@@ -29,35 +30,20 @@
         <java classname="${test}" fork="yes" >
         <jvmarg value="-Dfile.encoding=UTF8"/>
         <classpath>
-	 <pathelement path="src"/>
+	 <pathelement path="build"/>
         </classpath>
         </java>
     </target>
 
     <target name="jar" depends="build" >
-<!--    <mkdir dir="dest/jar"/> -->
-<!--
-    <copy todir="dest/jar">
-    　<fileset dir="data">
-    　　<include name="*"/>
-    　</fileset>
-    </copy>
- -->
-    <jar jarfile="jar/Lite.jar" basedir="src" manifest="src/Lite.mf"/> 
-<!--    <jar jarfile="dest/jar/Lite.jar" basedir="dest" manifest="Lite.mf"/> -->
+    <mkdir dir="build/data"/> 
+    <copy todir="build/data" file="src/data/README" />
+    <copy todir="build/data" file="src/data/example" />
+    <jar jarfile="jar/Lite.jar" basedir="build" manifest="src/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>
@@ -66,6 +52,8 @@
             </fileset>
         </delete>
     </target>
+   <!-- tar zcvf JavaLite.tgz \-\-exclude CVS JavaLite -->
+
 
 </project>
 
diff -r df74b1a85d3a -r ec609dbb13a7 src/data/README
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/data/README	Sun Jan 20 01:12:56 2008 +0900
@@ -0,0 +1,166 @@
+LITE: A little LITL Verifier version 0.1
+
+************************************************************************
+** Copyright (C) 1994,1991,2008
+** Shinji Kono (kono@ie.u-ryukyu.ac.jp)
+**   University of the Ryukyus
+**
+**    Everyone is permitted to do anything on this program
+**    including copying, modifying, improving,
+**    as long as you don't try to pretend that you wrote it.
+**    i.e., the above copyright notice has to appear in all copies.
+**    Binary distribution requires original version messages.
+**    You don't have to ask before copying, redistribution or publishing.
+**    THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE.
+
+Files
+    README		This file
+    Lite.jar            jar file
+                        java sources
+
+0. Installation
+
+    Put Lite.jar on some where. Java 1.5 or higher is required.
+
+    java -jar Lite.jar
+
+0.1 How to run
+
+    First, try preload examples.
+
+  do(2).
+
+    It generates state machine. It also accepts an ITL formula.
+
+  do( [](p) -> <> p ).
+
+  ls.
+    Show all preload examples.
+
+  diag.
+
+    This shows ``valid'' if it is a theorem, otherwise it shows you a counter
+    example.
+
+  exe.
+
+    This shows an execution of ITL formula, if it is satisfiable. It is
+    a counter example of negation of the original formula.   diag(N) or 
+      exe(N) shows at least N length examples.  
+   	1: +p-q   means "at clock 1, p is true and q is false". 
+    Please note exe(N)/diag(N) generate all possible state transition,
+    but it only shows one possible state transition conditon for a
+    state transition.
+
+    In case of a large formula, you may want to make output tarse.
+
+  verbose(off). 
+    generates one character per state transition condition.
+     e   empty
+     t   true
+     f   false
+     123. newly genrated state number
+     .   transition to a registerd state
+  verbose(on).
+
+  include('file name').
+     read from file.
+
+  ex(100,<> p).
+     define numbered example.
+
+  help.
+
+  show. 
+     show number of states.
+
+  clear.
+     Clear bdd database. Otherwise it remains for incremental
+     verification.
+
+  states.
+     show all subterm BDD, don't use it for large states.
+
+
+1. Syntax of ITL Formula
+
+Comma for conjunction, and semi-coron for disjunction as in Prolog.
+& for chop operator. @ for strong next. next(P) for weak next. 
+Postfix * means weak closure, that is, it allows 0 times execution.
+To use existential quantifier, a form exists(R,f(R)) is used,
+here R have to be Prolog variable.
+
+   a,b         a and b
+   a;b         a or b
+
+Other definitions are found in chop.pl. If you want to see the expanding
+results ( chop normal form, cannot be readable...) use   expand(X,Y).
+
+    ~(P) 	=   not(P)
+    P->Q 	=   (not(P);Q)
+    P<->Q 	=   ((not(P);Q),(P; not(Q)))
+    P=Q 	=   ((not(P);Q),(P; not(Q)))
+    (P && Q) 	=   ((not(empty),P) & Q)               strong chop
+                      Right associative. i.e.  P&&Q&&R = P&&(Q&&R)
+    <>(Q) 	=   (true & Q)
+    #(Q) 	=   not(true & not(Q))
+    [](Q) 	=   not(true & not(Q))
+    '[a]'(Q) 	=   not(true & not(Q) & true)
+    fin(Q) 	=   (true & (empty,Q))
+    halt(Q) 	=   [](empty=Q)
+    keep(Q) 	=   not(true & not((empty ; Q)))
+    more 	=   not(empty)
+    skip 	=   @(empty)
+    length(I)            expanded into series of strong next.
+    less(I)              expanded into series of weak next.
+    next(P) 	=   (empty; @(P))
+    gets(A,B)	=   keep(@A<->B)
+    stable(A) 	=   keep(@A<->A)
+
+    infinite    =   (true&false)
+    finite      =   ~infinite
+
+    pro(P, Q)  	=   Q is true using P as a clock period. True on empty.
+                    |-Q-------------|
+                    |-P-|-P-|-P-|-P-|
+    *P          =   P&P&..&P.. chop infinite closure 
+                    proj(P,true),fin(P)
+
+    Q=>P 	=   exists(R,(Q = R,stable(R),fin(P = R)))
+    +A  	=   (A & proj(A,true)                  strong closure
+    while(Cond,Do)	=   ((Cond->Do) , (~Cond->empty)) * 
+    exists(P,Q) =   Exsistential Quantifier
+    all(P,Q)   	=   not(exists(P,not(Q)))
+
+    even(P) 	=   exists(Q,(Q, keep( @Q = ~Q),[](Q->P)))
+    evenp(P) 	=   ((P,skip) & skip;empty,P)* & (empty;skip)
+    phil(L,R)  	=   ([]((~L  =    ~R)) & @ (L, ~R,@ (L,R, @ (R,[]( ~L)))) )
+
+For user define predicate use define/2. Ex.
+	def("yeilds(A,B)", "not(not(A) & B)").
+
+
+
+2. Basic Algorithm of the Verifier
+
+This program uses classic tableau method. So hold your breath, it is
+exponential to the number of the variables in the formula and  also
+combinatorial to the nesting of temporal logic operator. I think it is
+possible to reduce complexity for the nesting, but not for the
+variables.
+
+Major contribution is in the classification of ITL formula,
+which is found in SBDDSet.java . I use Ordered BDD
+standard form among subterms in original formula. Since this program
+always keep state machine deterministic, determinization of state
+machine is done by outer-most loop.
+
+The algorithm is quite simple. There are three stages. In the first
+stage, an ITL formula is decomposed into three  parts: empty, now and
+next. In the second stage, next parts is classifyed using subterm bdt
+and stored into database.  In the third stage, decomposition is
+repeatedly applied until no more new next parts are generated.
+
+Since ITL assumes any interval is finite, no eventuality checking is
+necessary.  Diagnosis algorithm is linear to the number of the state.
+
diff -r df74b1a85d3a -r ec609dbb13a7 src/lite/ITLCommander.java
--- a/src/lite/ITLCommander.java	Sat Jan 19 12:32:43 2008 +0900
+++ b/src/lite/ITLCommander.java	Sun Jan 20 01:12:56 2008 +0900
@@ -34,6 +34,7 @@
 			"diag.                      counter example of last verifed formula\n"+
 			"clear.                     clear state database\n"+
 			"show.                      show state statistics\n"+
+			"readme.                    show README\n"+
 			"help.                      show this\n"+
 			""
 				);
@@ -87,6 +88,8 @@
 			// System.out.println(i+":"+examples.get(i));
 			//}
 			parser.showResourceFile("data/example");
+		} else if (name == "readme") {
+			parser.showResourceFile("data/README");
 		} else if (name == "help") {
 			parser.help();
 		} else if (name == "def") {
diff -r df74b1a85d3a -r ec609dbb13a7 src/lite/ITLNodeParser.java
--- a/src/lite/ITLNodeParser.java	Sat Jan 19 12:32:43 2008 +0900
+++ b/src/lite/ITLNodeParser.java	Sun Jan 20 01:12:56 2008 +0900
@@ -9,8 +9,6 @@
 import parser.Token;
 import parser.TokenID;
 
-import sbdd.SBDDFactory;
-
 
 public class ITLNodeParser<Node extends ITLSolver> extends MacroNodeParser<Node> {
 
@@ -110,16 +108,17 @@
 			define("show","true",50,parseCommand);
 			define("states","true",50,parseCommand);
 			define("ls","true",50,parseCommand);
+			define("readme","true",50,parseCommand);
 			define("clear","true",50,parseCommand);
 			// only one of the is true (should allow all false case?)
 			define("share(L)","[](share0(L))");
 			define("share0(L)","true",50, new Command<Node>() {
 				@SuppressWarnings("unchecked")
 				public Node exec(Node predicate, Node value, LinkedList<Node> args) {
-					Node allElse = (Node)SBDDFactory.trueSolver;
-					Node allFalse = (Node)SBDDFactory.trueSolver;
-					value= (Node)SBDDFactory.falseSolver;
-					LinkedList<ITLSolver> list = args.get(0).arguments();
+					Node allElse = logicNodeFactory.trueNode();
+					Node allFalse = allElse;
+					Node falseNode = value= logicNodeFactory.falseNode();
+					LinkedList<? extends ITLSolver> list = args.get(0).arguments();
 					if (list==null) {
 						error("sahre: missing [] argument");
 						return value;
@@ -128,8 +127,7 @@
 					for(ITLSolver n:  list) {
 						Node n1 = (Node)n;
 						value = logicNodeFactory.bddNode(n1, allElse, value);
-						allElse = logicNodeFactory.bddNode(n1, 
-								(Node)SBDDFactory.falseSolver,allElse);
+						allElse = logicNodeFactory.bddNode(n1,falseNode,allElse); 
 						allFalse = logicNodeFactory.andNode(
 								logicNodeFactory.notNode(n1), allFalse);
 					}
@@ -169,6 +167,7 @@
 		dict.reserve("exe");
 		dict.reserve("show");
 		dict.reserve("ls");
+		dict.reserve("readme");
 		dict.reserve("states");
 		dict.reserve("clear");
 	}
diff -r df74b1a85d3a -r ec609dbb13a7 src/lite/ITLSolver.java
--- a/src/lite/ITLSolver.java	Sat Jan 19 12:32:43 2008 +0900
+++ b/src/lite/ITLSolver.java	Sun Jan 20 01:12:56 2008 +0900
@@ -35,7 +35,7 @@
 		return false;
 	}
 	
-	public LinkedList<ITLSolver> arguments() {
+	public LinkedList<? extends ITLSolver> arguments() {
 		return null;
 	}
 
diff -r df74b1a85d3a -r ec609dbb13a7 src/lite/MacroSolver.java
--- a/src/lite/MacroSolver.java	Sat Jan 19 12:32:43 2008 +0900
+++ b/src/lite/MacroSolver.java	Sun Jan 20 01:12:56 2008 +0900
@@ -46,7 +46,7 @@
 	}
 	
 	@Override
-	public LinkedList<ITLSolver> arguments() {
+	public LinkedList<? extends ITLSolver> arguments() {
 		return predicate.arguments();
 	}
 
diff -r df74b1a85d3a -r ec609dbb13a7 src/lite/PredicateSolver.java
--- a/src/lite/PredicateSolver.java	Sat Jan 19 12:32:43 2008 +0900
+++ b/src/lite/PredicateSolver.java	Sun Jan 20 01:12:56 2008 +0900
@@ -19,7 +19,7 @@
 	}
 
 	@Override
-	public LinkedList<ITLSolver> arguments() {
+	public LinkedList<? extends ITLSolver> arguments() {
 		return arg;
 	}
 	@Override