Mercurial > hg > Applications > Lite
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 |