--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/read.me	Thu Jan 18 23:27:24 2001 +0900
@@ -0,0 +1,337 @@
+LITE: A little LITL Verifier
+
+ Copyright (C) 1994,1991, 
+ Shinji Kono (kono@csl.sony.co.jp)
+   Sony Computer Science Laboratory, Inc.
+   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.
+
+ send your comments to kono@csl.sony.co.jp
+
+Files
+    Makefile		Makefile for *.ql/*.pl, "make" is called from Prolog
+    bdtstd.pl		Binary Tree Database of Temporal Logic Formula
+    chop.pl		Chop normal form expander
+    demoi		Install Script for X-Window Interface
+    demoim		    "  with module
+    diag.pl		Diagnosis and Execution
+    display.pl		X-Window Interface (GM and InterViews)
+    dvcomp.pl		Lazy expansion version of ITL tableau
+    ex.pl		Built-in Examples
+    exdev.pl		Expansion Loop
+    init		Install Script 
+    initm		Install Script with module
+    kiss.pl		KISS2 format for UCB SIS
+    lite.pl		Install Script 
+    ndcomp.pl		ITL tableau expansion
+    read.me		This file
+
+0. Installation
+
+    Edit Makefile and change
+          PROLOG               your prolog path name, such as sicstus
+          PROLOG_TYPE          SICSTUS, XSB, SBPROLOG, CPROLOG, CPROLOG15
+    see cp.pl.c for portbaliity information.
+
+    Run your Prolog. I use SICStus Prolog but Quintus Prolog or C-Prolog 
+    will work.  In case of SBPROLOG, you also need SB_START_FILE.
+
+    Then consult a file init. 
+
+?-[init].
+
+    It runs unix make and compile and load necessary Prolog programs.
+    If you need a moduled version use ?-[initm].
+
+    In case of SB-Prolog, type
+	make
+    by hand. This create file named "lite". Then start SB-Prolog like this.
+        sbprolog lite
+    or you can use load(lite). Then you need to initialize by
+        ?- lite_start.
+
+0.1 How to run
+
+    Try numbered examples in ex.pl.
+
+?-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).
+
+?-ex. runs all examples in diag.pl. But it takes several hours.
+      Some of the examples are quite large.
+?-exex. runs all examples and save state machine in file ``ex''.
+
+0.1. X-Window Interace
+
+    If you want to run X-window version, you have to install InterViews
+    interface for SICSTUS. It requires ispgm binary and library/gmlib.
+    ?-[demoim].    % This loads and runs X-window interface.
+    Type-in a formula. 
+       ex(1) or demo(1) for the example number in ex.pl.
+    Push verify buttom and execute buttom in order.
+    Execute and Counter Example buttons show an example in a graphical way.
+    Map button shows bitmap of the characteristic function.
+
+0.1.1 Tcl/Tk Interface
+
+
+0.2. KISS format interface
+
+    To generate KISS2 format for SIS, try run
+
+?-kiss.
+
+    right after verification. To specify input variables and
+    output variables assert this predicate:
+	st_variables(In,Out).
+    State machine description is also supported
+    in this system. You can read a KISS2 format state machine.
+    Only one state machine is accepted because of variable 
+    declaration.
+
+?- read_kiss(File,In,Out,Empty).
+
+    reads KISS2 format. In and Out are list of variables in the order
+    of the KISS2 file. If Out is [], output variales are omitted.
+    If In or Out are uninstantiated variables, name 'i0' or 'o2'
+    are used.  Empty is usually set to empty and it generates 
+    empty condition for each state, for example:
+	st(st0,empty,empty).
+    To modify or to generate KISS format again, you have to
+    verify it.
+	?- ex(st(st0)).
+    `st0' is the start state of automaton. The state machine can
+    be used in arbitrary temporal logic expression. But if you 
+    generate very non-deterministic modification, the output
+    can be very large. For examle:
+	 ?- ex(exists(i0,st(st0))).
+
+?- read_kiss(File).
+    =>  read_kiss(File,_,_,empty)
+?- read_kiss(File,Empty).
+    =>  read_kiss(File,_,_,Empty)
+
+0.3
+    dvcomp.pl contains lazy state transition clause generation and binary
+    tree representation of ITL term.  Reconsult it after [init].  It 
+    reduces memory usage drastically. To control lazy generation, use:
+       ?-lazy(on).
+       ?-lazy(off).
+    kiss format generation is not supported for lazy generation.
+
+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
+    <>(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)
+
+    P proj Q  	=   Q is true using P as a clock period
+    *P          =   P&P&..&P.. chop infinite closure 
+
+    Q=>P 	=   exists(R,(Q = R,stable(R),fin(P = R)))
+    P<=Q 	=   Q=>P
+    +A  	=   (A & (empty;A) *)                  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.
+	define(yeilds(A,B), not(not(A) & B)).
+
+
+1.1 Finte State Automaton support
+
+1.1.1 Output.
+
+This version supports Finite State Automaton I/O. The output of
+our verifier is finite automaton.
+
+?-tgen.
+
+generates automaton as Tokio Temporal Logic Programming Language.
+KISS2 format output is also supported, see 0.2.
+
+1.1.2 Input
+
+It is possible to use automaton as a part of ITL formula.
+Finite automaton is stored in Prolog clauses.
+
+st(s0) starts Finite State Automaton (FSA) from s0 states.
+This is a temporal logic term, so you can use this anywhere
+in ITL formula, for example: st(s0) & not(st(s0)), <>(st(s0)).
+FSA is defined as Prolog clauses in this way:
+
+st_variables([q],[s]).   
+%   st_varaibles(Input_variables,Output_variables)
+%   This is important only for KISS format generation
+	    
+st(s0,((not(a);not(b)),q),s0). 
+%    st(Current_State, Condition, Next_State)
+st(s1,(not(c),q),s1).
+st(s1, empty,empty).
+
+Conditions can be non-deterministic. Actually it allows
+arbitrary ITL formula, but if you use temporal condtions,
+it is not a state machine any more. The automaton is
+determinized during verfication, since generated state
+machine is determinisc. Be careful, the output can be very large.
+
+If a state machine contains no empty conditions, it is
+not satisfiable in ITL, because our ITL only have finite
+interval. But it may contains infinite clock periods. 
+
+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 (I think) is in the classification of ITL formula,
+which is found in bdtstd.pl. I use binary decision tree (not diagram)
+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.
+
+3. Wish lists
+
+It is possible to reduce complexity in somehow.
+
+4. Brief description of this program.
+
+File exdev.pl contains main driver of tableau based interval temporal 
+logic verifier. A developer deve(X) does tableau development.
+
+deve(ITL) :-
+	init,!,
+	expand(ITL,ITL0),
+	itlstd(ITL0,StdNext),
+	check_state(StdNext,ITL0,_,S),!,
+	deve0((S,ITL0)).
+
+In init, formula databases are initialized. 
+Usually ITL formula contains several macro definitions, expand(X,Y) 
+expands these macros form X to Y.
+The formula is translated into standard form in itlstd(X,Y), where X is original
+formula and Y is binary decision tree standard form (not diagram).
+The formula databases are maintained in check_state(Stdoriginal,NewFlag,No).
+Std is the standard form. We need original formula here for display.
+Whether Std is already in database or not is shown in NewFlag and when
+database sequence number (i.e. state number) is returned in No.
+
+deve0((S,ITL)) :-
+        show_state(S,ITL),
+	setof(Next,itldecomp(ITL,Next,S),
+	    Nexts),!,
+	deve1(Nexts).
+deve0(_).
+
+We are now in deve0(X) predicates. After displaying current states, it
+gathers possible tableau expansion using setof predicates. Since not so
+many formula is generated from one state, setof is not a bottle neck of
+this program. The real bottle neck is total number of state/condition pair and
+it's database looking up.  Setof predicates returns only new candidates and 
+theses are stored in a list, in LIFO way.
+
+deve1([]).
+deve1([H|T]) :- deve0(H),deve1(T).
+
+Here is a repetition part. 
+
+itldecomp(ITL,(NextS,Next),From) :-
+	itl(ITL,Next,Cond),
+	%% showing
+	itlshow(Next,NextS,Cond,From).
+
+Actual tableau expansion is done by itl(ITL,Next,Cond). It generate
+Sumof( Cond -> @(Next) ), where Cond is exclusive, that is, it generates
+deterministic automaton. You can test itl predicates by hands, for example,
+?-itl(p & q,Next,Cond).
+
+itlshow(Next,S,Cond,From):-
+	itlstd(Next,StdNext),
+	check_state(StdNext,Next,New,S),
+	assertz(state(From,Cond,S)),
+	!,itlshow1(S,Cond,Next,New).
+
+In itlshow, standard form conversion and database checking is performed.
+Rest of parts are related to state database and displaying.
+
+That's all. There are more stories about itlstd and itl predicates, but it is
+better to look source code rather than vague English...
+