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