Mercurial > hg > Applications > Lite

comparison infinite.pl @ 6:9b86eb10b61c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
*** empty log message ***
author kono
date Fri, 19 Jan 2001 09:16:27 +0900
parents
children bd06de5e669a
comparison
equal deleted inserted replaced
5:75a40129f638 6:9b86eb10b61c
1 /*
2 Copyright (C) 2001, Shinji Kono, University of the Ryukyus
3
4 Everyone is permitted to copy and distribute verbatim copies
5 of this license, but changing it is not allowed. You can also
6 use this wording to make the terms for other programs.
7
8 send your comments to kono@ie.u-ryukyu.ac.jp
9 $Header$
10
11 Infinite satisfiability/validity checker
12
13 A set of non-empty-exit looping states represents infinite
14 interval in ITL. The loop can contains deterministic state
15 choice. This should correspond Rabin/Strreet Automaton
16 that is non-deterministic Buchi automaton.
17
18 The algorith works in depth first way.
19
20 */
21
22 :-dynamic found_infinite/0.
23
24 infinite:-
25 retract_all(found_infinite),
26 infinite(L),
27 write_infinite_seq(L).
28 infinite:-
29 found_infinite,!.
30 infinite:-
31 write('unsatisfiable in infinite interval.'),nl.
32
33 write_infinite_seq(L) :-
34 write('satisfiable in infinite interval: '),
35 write(L),nl.
36
37 retract_all(X) :-
38 retract(X),fail.
39 retract_all(_).
40
41 infinite([S|L]) :-
42 links(_,S),
43 more_only(S), % search more only node
44 more_only_loop(S,S,L,[]),
45 assert(found_infinite).
46 infinite([]) :-
47 found_infinite.
48
49 more_only(S) :-
50 state(S,[empty|_],true),!,fail.
51 more_only(S) :- number(S).
52
53 more_only_loop(S,S0,L,L1) :-
54 links(N,S),
55 more_only_loop1(N,S0,L,L1).
56
57 more_only_loop1(S,S,L,L) :-!.
58 more_only_loop1(N,S,[N|L],L1) :-
59 more_only(N),
60 more_only_loop(N,S,L,L1).
61
62 /* end */