% Sat May 22 11:43:11 JST 1993

:-  module(lite,[
	ex/1,  			% ex(ITL)   verification predicate
	ex/2,			% ex(No,Example)
	diag/1,diag/0, 		% find counter example
	infinite/1,infinite/0, 	% omega interval satisfiability
	exe/1, exe/0,		% find sample execution
	verbose/1, 		% verbose mode (default on)
	renaming/1, 		% 2var renaming mode (default on)
	singleton/1, 		% singleton removal mode (default on)
	detailed/1, 		% detailed trace of 2var
	set_limit/1, 		% 2var state limit
	lazy/1,			% lazy mode (dvcomp only)
	kiss/0, 		% kiss format geneartion
	read_kiss/1,		% read KISS2 format
	read_kiss/4,		% read KISS2 format
	read_kiss/3,		% read KISS2 format
	tgen/0, 		% tokio clause geneartion
	itl/1,			% one step tableau expansion
	itl/3,			%     " in detail
	itl_statistics/0,  	% show number of state etc. 
	st/3,			% external state machine
	st_variables/2,		%     its variables
	sbterm/0,		% show sub term/ state database
	display/0, large/0, small/0, 	% show state database
	start/0, display_diag/1, display_exe/1,
	state/0 		% show state database
]).

%?-op(900,xfy,[(&),('&&')]).
%?-op(700,xfy,['<->','\=',proj]).
%?-op(60,fy,['~','#','<>', '@',^]).
%?-op(60,fy,[*]).
?-[op].
% :- use_module(library(gmlib)).
:- ensure_loaded([dvcomp,rstd,chop,diag,kiss,ex,cp,infinite]).
% ,display]).

% end