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