comparison bddi @ 2:1c57a78f1d98

Initial revision
author kono
date Thu, 18 Jan 2001 23:27:24 +0900
parents
children
comparison
equal deleted inserted replaced
1:683efd6f9a81 2:1c57a78f1d98
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