|
2
|
1 /*
|
|
|
2 Copyright (C) 1991, Shinji Kono, Sony Computer Science Laboratory, Inc.
|
|
|
3 The University, Newcastle upton Tyne
|
|
|
4
|
|
|
5 Everyone is permitted to copy and distribute verbatim copies
|
|
|
6 of this license, but changing it is not allowed. You can also
|
|
|
7 use this wording to make the terms for other programs.
|
|
|
8
|
|
|
9 send your comments to kono@csl.sony.co.jp
|
|
|
10 $Id$
|
|
|
11 */
|
|
|
12
|
|
|
13 % develop Local ITL formula into state diagram
|
|
|
14 %
|
|
|
15 % Mon May 20 17:24:23 BST 1991
|
|
|
16 % require([chop]).
|
|
|
17
|
|
|
18 ex :- ex1(_).
|
|
|
19
|
|
|
20 ex(N) :- number(N),!,ex1(N).
|
|
|
21 ex(demo(N)) :- number(N),!,ex1(N).
|
|
|
22 ex(X) :- verbose,!,time(deve(X)),itl_statistics,diag,!.
|
|
|
23 ex(X) :- time(deve(X)),itl_statistics.
|
|
|
24
|
|
|
25 ex1(N) :- ex(N,P),nl,write(P),write('.'),nl,ex(P),fail.
|
|
|
26 ex1(_) :- told.
|
|
|
27
|
|
|
28 exex :- verbose(off),tell(ex),(
|
|
|
29 ex(_,P),nl,write(P),write('.'),nl,ex(P),itl_statistics,fail;
|
|
|
30 told
|
|
|
31 ).
|
|
|
32
|
|
|
33 % cputime(X):-statistics(runtime,[X1,_]),!,X is X1/1000.
|
|
|
34 % cputime(X):-X is cputime. % for cprolog
|
|
|
35 time(X):- r_cputime(T0),call(X),r_cputime(T1),
|
|
|
36 T is T1-T0,
|
|
|
37 nl,write(T),write(' sec.').
|
|
|
38
|
|
|
39 state :- listing(state/3),lising(state/4).
|
|
|
40
|
|
|
41 % diagnosis
|
|
|
42 diag :- diag(X),
|
|
|
43 (X = counter_example(_), write('counter example:'),nl; true),!,
|
|
|
44 write_diag(X).
|
|
|
45
|
|
|
46 diag(X) :- number(X), % at most X length solution
|
|
|
47 links(false,_), % search false
|
|
|
48 diag_l(false,[],H,X),
|
|
|
49 make_hist(H,Hist),
|
|
|
50 write_diag(counter_example(Hist)).
|
|
|
51 diag(valid) :- \+(links(false,_)),!.
|
|
|
52 diag(counter_example(Hist)) :-
|
|
|
53 diag_l(false,[],H,0),
|
|
|
54 make_hist(H,Hist).
|
|
|
55
|
|
|
56 % execution exapmle.
|
|
|
57 exe :- exe(Z),
|
|
|
58 (Z=unsatisfiable, nl,write('unsatisfiable'),nl,!,fail;
|
|
|
59 nl,write('execution:'),nl,write_diag(Z)).
|
|
|
60
|
|
|
61 exe(X) :- number(X), % at most X length solution
|
|
|
62 possible_root(R),
|
|
|
63 diag_l(R,[],H,X),
|
|
|
64 make_hist(H,Hist),
|
|
|
65 write_diag(execution(Hist)).
|
|
|
66 exe(unsatisfiable) :- \+(possible_root(_)),!.
|
|
|
67 exe(execution(Hist)) :-
|
|
|
68 possible_root(R),
|
|
|
69 diag_l(R,[],H,0),
|
|
|
70 make_hist(H,Hist).
|
|
|
71
|
|
|
72 % possible root is non looping true or 0 node.
|
|
|
73 possible_root(true) :-
|
|
|
74 possible_root1(true).
|
|
|
75 possible_root(0) :-
|
|
|
76 possible_root1(0).
|
|
|
77
|
|
|
78 possible_root1(R) :- links(R,N),\+(N = true),!.
|
|
|
79
|
|
|
80 % Log order search
|
|
|
81
|
|
|
82 make_hist(S,C) :- detailed,!,
|
|
|
83 S = [P|L],itl_state(P1,P),
|
|
|
84 make_hist1(L,P,P1,[],_,C).
|
|
|
85 make_hist(S,C) :-
|
|
|
86 S = [P|L],
|
|
|
87 make_hist0(L,P,C).
|
|
|
88
|
|
|
89 make_hist0([],_,[]):-!.
|
|
|
90 make_hist0([D|L],S,[(D->Cond)|L1]):-!, % step by step
|
|
|
91 state(S,Cond,D),
|
|
|
92 !, %
|
|
|
93 make_hist0(L,D,L1).
|
|
|
94
|
|
|
95 % trace 2variable renamings
|
|
|
96
|
|
|
97 make_hist1([],_,_,R,R,[]):-!.
|
|
|
98 make_hist1([SN|L],S,P,R,R1,[(SN->Cond)|L1]):-!, % step by step
|
|
|
99 state(S,Cond,SN,P,P1,R,R0),
|
|
|
100 !,
|
|
|
101 make_hist1(L,SN,P1,R0,R1,L1).
|
|
|
102
|
|
|
103
|
|
|
104 diag(Hist,P) :-
|
|
|
105 diag_l(P,[],Hist,0).
|
|
|
106
|
|
|
107 % try to find interesting example
|
|
|
108 % reverse order back track
|
|
|
109 diag_ls(Ps,L,L1,D):-member(P,Ps),diag_l(P,L,L1,D).
|
|
|
110
|
|
|
111 % one minimum solution
|
|
|
112 diag_l(1,L,[1|L],D):-!,D=<0. % Initial State? Enough depth?
|
|
|
113 diag_l(E,L,L1,D) :-
|
|
|
114 setof(P,links(E,P),P1), % must be minimum first order
|
|
|
115 D1 is D-1,
|
|
|
116 member(P0,P1),
|
|
|
117 diag_l(P0,[E|L],L1,D1).
|
|
|
118
|
|
|
119
|
|
|
120 write_diag(counter_example(Hist)) :-!,write_ce(Hist,0).
|
|
|
121 write_diag(execution(Hist)) :-!,write_ce(Hist,0).
|
|
|
122 write_ce([],_):-!.
|
|
|
123 write_ce([(S->[E|L])|T],I) :- (E=more,L=L1;E=empty,L=L1;[E|L]=L1),!,
|
|
|
124 write(I),write(:),write_cond(L1),put(9),write(S),nl,
|
|
|
125 J is I+1,
|
|
|
126 write_ce(T,J).
|
|
|
127 write_diag(R):-!,write(R),nl.
|
|
|
128
|
|
|
129 % condition print
|
|
|
130
|
|
|
131 write_cond(X) :- sortC(X,Y),write_cond1(Y).
|
|
|
132 write_cond1([]):-!.
|
|
|
133 write_cond1([H|T]):-!,write_cond1(H),write_cond1(T).
|
|
|
134 write_cond1(not(P)):-!,put(45), % "-"
|
|
|
135 write(P).
|
|
|
136 write_cond1(P):- !,put(43), % "+"
|
|
|
137 write(P).
|
|
|
138
|
|
|
139 % bubble sort
|
|
|
140 sortC([],[]).
|
|
|
141 sortC([H|T],[Min|Y]):-
|
|
|
142 min(T,H,Min,Rest),
|
|
|
143 sortC(Rest,Y).
|
|
|
144
|
|
|
145 min([],X,X,[]).
|
|
|
146 min([H|T],X,Y,[H|S]) :- ord(H,X),!,min(T,X,Y,S).
|
|
|
147 min([H|T],X,Y,[X|S]) :- min(T,H,Y,S).
|
|
|
148
|
|
|
149 ord(not(X),not(Y)) :- !,X @> Y.
|
|
|
150 ord(X,not(Y)) :- !,X @> Y.
|
|
|
151 ord(not(X),Y) :- !,X @> Y.
|
|
|
152 ord(X,Y) :- !,X @> Y.
|
|
|
153
|
|
|
154 rev([],X,X).
|
|
|
155 rev([H|T],X,Y) :- rev(T,[H|X],Y).
|
|
|
156
|
|
|
157 member(H,[H|_]).
|
|
|
158 member(H,[_|T]):-member(H,T).
|
|
|
159
|
|
|
160 not_member(_,[]):-!.
|
|
|
161 not_member(H,[H|_]):-!,fail.
|
|
|
162 not_member(H,[_|T]):-not_member(H,T).
|
|
|
163
|
|
|
164 count(A) :- count(A,X),write(X),nl.
|
|
|
165 count(A, _) :-
|
|
|
166 init_var(tmp, 0),
|
|
|
167 call(A),
|
|
|
168 inc_var(tmp, _),
|
|
|
169 fail.
|
|
|
170 count(_, A) :-
|
|
|
171 retract(tmp(A)).
|
|
|
172
|
|
|
173 user_help :- write('?-ex(2).'),nl,
|
|
|
174 write('?-ex( [](p) -> <> p ).'),nl,
|
|
|
175 write(' Verify numbered examples or ITL formula.'),nl,
|
|
|
176 write('?-diag.'),nl,
|
|
|
177 write(' shows a counter example.'),nl,
|
|
|
178 write('?-exe.'),nl,
|
|
|
179 write(' This shows an execution of ITL formula.'),nl,
|
|
|
180 write('?-diag(N) or ?-exe(N) '),nl,
|
|
|
181 write(' shows at least N length examples. '),nl,
|
|
|
182 write(' 1: +p-q means "at clock 1, p is true and q is false". '),nl,
|
|
|
183 write('?-verbose(off). '),nl,
|
|
|
184 write(' generates one character per state transition condition.'),nl,
|
|
|
185 write(' e empty / t true / f false'),nl,
|
|
|
186 write(' 123. newly genrated state number'),nl,
|
|
|
187 write(' . transition to a registerd state'),nl,
|
|
|
188 write('?-verbose(on).'),nl,
|
|
|
189 write(' show ITL formula for each state. (Can be Very large)'),nl,
|
|
|
190 write('?-start, display.'),nl,
|
|
|
191 write(' starts X-Window Interface.'),nl,
|
|
|
192 write('?-ex. runs all examples in diag.pl. But it takes several hours.'),nl,
|
|
|
193 write(' Some of the examples are quite large.'),nl,
|
|
|
194 write('?-kiss.'),nl,
|
|
|
195 write(' generates KISS2 format for SIS.'),nl,
|
|
|
196 write('?-tgen.'),nl,
|
|
|
197 write(' generates Tokio language.'),nl,
|
|
|
198 write('?-read_kiss(File,In,Out,Empty).'),nl,
|
|
|
199 write(' reads KISS2 format. In and Out are list of variables in the order'),nl,
|
|
|
200 write(' of the KISS2 file. '),nl,
|
|
|
201 write('?-read_kiss(File).'),nl,
|
|
|
202 write(' => read_kiss(File,_,_,empty)'),nl,
|
|
|
203 write('?-read_kiss(File,Empty).'),nl,
|
|
|
204 write(' => read_kiss(File,_,_,Empty) '),nl,
|
|
|
205 true.
|
|
|
206
|
|
|
207 /* end */
|
