--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/README	Fri Jan 18 00:32:39 2008 +0900
@@ -0,0 +1,143 @@
+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.
+
+
+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
+
+    Try preload examples.
+
+  ex(2).
+
+    It generates state machine. It also accepts an ITL formula.
+
+  ex( [](p) -> <> p ).
+
+    Please be careful about funny Prolog operator grammar.
+    Someday I will make a parser for Ben's notation. But not now...
+    After the state machine expansion, there are two diagnosis predicates.
+
+  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 possible. 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).
+
+
+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.
+
+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.
+