Mercurial > hg > Applications > Lite
comparison liter.pl @ 19:e1d3145cff7a lite-verifier
*** empty log message ***
| author | kono |
|---|---|
| date | Thu, 30 Aug 2007 12:44:35 +0900 |
| parents | |
| children |
comparison
equal
deleted
inserted
replaced
| 18:a6adedccd5f6 | 19:e1d3145cff7a |
|---|---|
| 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 | |
| 7 exe/1, exe/0, % find sample execution | |
| 8 verbose/1, % verbose mode (default on) | |
| 9 renaming/1, % 2var renaming mode (default on) | |
| 10 singleton/1, % singleton removal mode (default on) | |
| 11 detail/1, % detailed trace of 2var | |
| 12 set_limit/1, % 2var state limit | |
| 13 lazy/1, % lazy mode (dvcomp only) | |
| 14 kiss/0, % kiss format geneartion | |
| 15 read_kiss/1, % read KISS2 format | |
| 16 read_kiss/4, % read KISS2 format | |
| 17 read_kiss/3, % read KISS2 format | |
| 18 tgen/0, % tokio clause geneartion | |
| 19 itl/1, % one step tableau expansion | |
| 20 itl/3, % " in detail | |
| 21 itl_statistics/0, % show number of state etc. | |
| 22 st/3, % external state machine | |
| 23 st_variables/2, % its variables | |
| 24 sbterm/0, % show sub term/ state database | |
| 25 display/0, large/0, small/0, % show state database | |
| 26 start/0, display_diag/1, display_exe/1, | |
| 27 state/0 % show state database | |
| 28 ]). | |
| 29 | |
| 30 %?-op(900,xfy,[(&),('&&')]). | |
| 31 %?-op(700,xfy,['<->','\=',proj]). | |
| 32 %?-op(60,fy,['~','#','<>', '@',^]). | |
| 33 %?-op(60,fy,[*]). | |
| 34 ?-[op]. | |
| 35 % :- use_module(library(gmlib)). | |
| 36 :- ensure_loaded([dvcomp,rstd,chop,diag,kiss,ex,cp]). | |
| 37 % ,display]). | |
| 38 | |
| 39 % end |