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.