% Sat May 22 11:43:11 JST 1993

:- use_module('~/ITL/bdd/sicstus/bdd').

:-  module(lite,[
	ex/1,  			% ex(ITL)   verification predicate
	ex/2,			% ex(No,Example)
	diag/1,diag/0, 		% find counter example
	exe/1, exe/0,		% find sample execution
	verbose/1, 		% verbose mode
	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].

:-
  unix(system('make tmpa M=lite:')),
  ['.tmpc'],
  unix(system('make bdd M=lite:')),
  ['.tmpc'].

make :- unix(system('make M=lite: bdd')),consult(lite:['.tmpc','.tmpl']).

:- ensure_loaded([chop,diag,kiss,ex,cp]).
:- ensure_loaded([bdditl,bddcomp]).

% :-start.
% :-display.
% display(Host) :- start(Host),display.

% end