|
19
|
1 % Sat May 22 11:43:11 JST 1993
|
|
|
2
|
|
|
3 :- module(lite,[
|
|
|
4 ex/1, % ex(ITL) verification predicate
|
|
|
5 ex/2, % ex(No,Example)
|
|
|
6 diag/1,diag/0, % find counter example
|
|
|
7 exe/1, exe/0, % find sample execution
|
|
|
8 verbose/1, % verbose mode (default on)
|
|
|
9 renaming/1, % 2var renaming mode (default on)
|
|
|
10 singleton/1, % singleton removal mode (default on)
|
|
|
11 detail/1, % detailed trace of 2var
|
|
|
12 set_limit/1, % 2var state limit
|
|
|
13 lazy/1, % lazy mode (dvcomp only)
|
|
|
14 kiss/0, % kiss format geneartion
|
|
|
15 read_kiss/1, % read KISS2 format
|
|
|
16 read_kiss/4, % read KISS2 format
|
|
|
17 read_kiss/3, % read KISS2 format
|
|
|
18 tgen/0, % tokio clause geneartion
|
|
|
19 itl/1, % one step tableau expansion
|
|
|
20 itl/3, % " in detail
|
|
|
21 itl_statistics/0, % show number of state etc.
|
|
|
22 st/3, % external state machine
|
|
|
23 st_variables/2, % its variables
|
|
|
24 sbterm/0, % show sub term/ state database
|
|
|
25 display/0, large/0, small/0, % show state database
|
|
|
26 start/0, display_diag/1, display_exe/1,
|
|
|
27 state/0 % show state database
|
|
|
28 ]).
|
|
|
29
|
|
|
30 %?-op(900,xfy,[(&),('&&')]).
|
|
|
31 %?-op(700,xfy,['<->','\=',proj]).
|
|
|
32 %?-op(60,fy,['~','#','<>', '@',^]).
|
|
|
33 %?-op(60,fy,[*]).
|
|
|
34 ?-[op].
|
|
|
35 % :- use_module(library(gmlib)).
|
|
|
36 :- ensure_loaded([dvcomp,rstd,chop,diag,kiss,ex,cp]).
|
|
|
37 % ,display]).
|
|
|
38
|
|
|
39 % end
|
