diff liter.pl @ 19:e1d3145cff7a lite-verifier

*** empty log message ***
author kono
date Thu, 30 Aug 2007 12:44:35 +0900
parents
children
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/liter.pl	Thu Aug 30 12:44:35 2007 +0900
@@ -0,0 +1,39 @@
+% 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
+	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)
+	detail/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]).
+% ,display]).
+
+% end