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