|
2
|
1 LITE: A little LITL Verifier
|
|
|
2
|
|
|
3 Copyright (C) 1994,1991,
|
|
|
4 Shinji Kono (kono@csl.sony.co.jp)
|
|
|
5 Sony Computer Science Laboratory, Inc.
|
|
|
6 The University, Newcastle upton Tyne
|
|
|
7
|
|
|
8 Everyone is permitted to copy and distribute verbatim copies
|
|
|
9 of this license, but changing it is not allowed. You can also
|
|
|
10 use this wording to make the terms for other programs.
|
|
|
11
|
|
|
12 send your comments to kono@csl.sony.co.jp
|
|
|
13
|
|
|
14 Files
|
|
|
15 Makefile Makefile for *.ql/*.pl, "make" is called from Prolog
|
|
|
16 bdtstd.pl Binary Tree Database of Temporal Logic Formula
|
|
|
17 chop.pl Chop normal form expander
|
|
|
18 demoi Install Script for X-Window Interface
|
|
|
19 demoim " with module
|
|
|
20 diag.pl Diagnosis and Execution
|
|
|
21 display.pl X-Window Interface (GM and InterViews)
|
|
|
22 dvcomp.pl Lazy expansion version of ITL tableau
|
|
|
23 ex.pl Built-in Examples
|
|
|
24 exdev.pl Expansion Loop
|
|
|
25 init Install Script
|
|
|
26 initm Install Script with module
|
|
|
27 kiss.pl KISS2 format for UCB SIS
|
|
|
28 lite.pl Install Script
|
|
|
29 ndcomp.pl ITL tableau expansion
|
|
|
30 read.me This file
|
|
|
31
|
|
|
32 0. Installation
|
|
|
33
|
|
|
34 Edit Makefile and change
|
|
|
35 PROLOG your prolog path name, such as sicstus
|
|
|
36 PROLOG_TYPE SICSTUS, XSB, SBPROLOG, CPROLOG, CPROLOG15
|
|
|
37 see cp.pl.c for portbaliity information.
|
|
|
38
|
|
|
39 Run your Prolog. I use SICStus Prolog but Quintus Prolog or C-Prolog
|
|
|
40 will work. In case of SBPROLOG, you also need SB_START_FILE.
|
|
|
41
|
|
|
42 Then consult a file init.
|
|
|
43
|
|
|
44 ?-[init].
|
|
|
45
|
|
|
46 It runs unix make and compile and load necessary Prolog programs.
|
|
|
47 If you need a moduled version use ?-[initm].
|
|
|
48
|
|
|
49 In case of SB-Prolog, type
|
|
|
50 make
|
|
|
51 by hand. This create file named "lite". Then start SB-Prolog like this.
|
|
|
52 sbprolog lite
|
|
|
53 or you can use load(lite). Then you need to initialize by
|
|
|
54 ?- lite_start.
|
|
|
55
|
|
|
56 0.1 How to run
|
|
|
57
|
|
|
58 Try numbered examples in ex.pl.
|
|
|
59
|
|
|
60 ?-ex(2).
|
|
|
61
|
|
|
62 It generates state machine. It also accepts an ITL formula.
|
|
|
63
|
|
|
64 ?-ex( [](p) -> <> p ).
|
|
|
65
|
|
|
66 Please be careful about funny Prolog operator grammar.
|
|
|
67 Someday I will make a parser for Ben's notation. But not now...
|
|
|
68 After the state machine expansion, there are two diagnosis predicates.
|
|
|
69
|
|
|
70 ?-diag.
|
|
|
71
|
|
|
72 This shows ``valid'' if it is a theorem, otherwise it shows you a counter
|
|
|
73 example.
|
|
|
74
|
|
|
75 ?-exe.
|
|
|
76
|
|
|
77 This shows an execution of ITL formula, if it is possible. It is
|
|
|
78 a counter example of negation of the original formula. ?-diag(N) or
|
|
|
79 ?-exe(N) shows at least N length examples.
|
|
|
80 1: +p-q means "at clock 1, p is true and q is false".
|
|
|
81 Please note exe(N)/diag(N) generate all possible state transition,
|
|
|
82 but it only shows one possible state transition conditon for a
|
|
|
83 state transition.
|
|
|
84
|
|
16
|
85 ?-infinite.
|
|
|
86 Check satisfiability on infinite interval. Like exe, it shows
|
|
|
87 possible accept states with a loop marked by *. To check infinite
|
|
|
88 validity, use negation.
|
|
|
89
|
|
2
|
90 In case of a large formula, you may want to make output tarse.
|
|
|
91
|
|
|
92 ?-verbose(off).
|
|
|
93 generates one character per state transition condition.
|
|
|
94 e empty
|
|
|
95 t true
|
|
|
96 f false
|
|
|
97 123. newly genrated state number
|
|
|
98 . transition to a registerd state
|
|
|
99 ?-verbose(on).
|
|
|
100
|
|
|
101 ?-ex. runs all examples in diag.pl. But it takes several hours.
|
|
|
102 Some of the examples are quite large.
|
|
|
103 ?-exex. runs all examples and save state machine in file ``ex''.
|
|
|
104
|
|
|
105 0.1. X-Window Interace
|
|
|
106
|
|
|
107 If you want to run X-window version, you have to install InterViews
|
|
|
108 interface for SICSTUS. It requires ispgm binary and library/gmlib.
|
|
|
109 ?-[demoim]. % This loads and runs X-window interface.
|
|
|
110 Type-in a formula.
|
|
|
111 ex(1) or demo(1) for the example number in ex.pl.
|
|
|
112 Push verify buttom and execute buttom in order.
|
|
|
113 Execute and Counter Example buttons show an example in a graphical way.
|
|
|
114 Map button shows bitmap of the characteristic function.
|
|
|
115
|
|
|
116 0.1.1 Tcl/Tk Interface
|
|
|
117
|
|
|
118
|
|
|
119 0.2. KISS format interface
|
|
|
120
|
|
|
121 To generate KISS2 format for SIS, try run
|
|
|
122
|
|
|
123 ?-kiss.
|
|
|
124
|
|
|
125 right after verification. To specify input variables and
|
|
|
126 output variables assert this predicate:
|
|
|
127 st_variables(In,Out).
|
|
|
128 State machine description is also supported
|
|
|
129 in this system. You can read a KISS2 format state machine.
|
|
|
130 Only one state machine is accepted because of variable
|
|
|
131 declaration.
|
|
|
132
|
|
|
133 ?- read_kiss(File,In,Out,Empty).
|
|
|
134
|
|
|
135 reads KISS2 format. In and Out are list of variables in the order
|
|
|
136 of the KISS2 file. If Out is [], output variales are omitted.
|
|
|
137 If In or Out are uninstantiated variables, name 'i0' or 'o2'
|
|
|
138 are used. Empty is usually set to empty and it generates
|
|
|
139 empty condition for each state, for example:
|
|
|
140 st(st0,empty,empty).
|
|
|
141 To modify or to generate KISS format again, you have to
|
|
|
142 verify it.
|
|
|
143 ?- ex(st(st0)).
|
|
|
144 `st0' is the start state of automaton. The state machine can
|
|
|
145 be used in arbitrary temporal logic expression. But if you
|
|
|
146 generate very non-deterministic modification, the output
|
|
|
147 can be very large. For examle:
|
|
|
148 ?- ex(exists(i0,st(st0))).
|
|
|
149
|
|
|
150 ?- read_kiss(File).
|
|
|
151 => read_kiss(File,_,_,empty)
|
|
|
152 ?- read_kiss(File,Empty).
|
|
|
153 => read_kiss(File,_,_,Empty)
|
|
|
154
|
|
|
155 0.3
|
|
|
156 dvcomp.pl contains lazy state transition clause generation and binary
|
|
|
157 tree representation of ITL term. Reconsult it after [init]. It
|
|
|
158 reduces memory usage drastically. To control lazy generation, use:
|
|
|
159 ?-lazy(on).
|
|
|
160 ?-lazy(off).
|
|
|
161 kiss format generation is not supported for lazy generation.
|
|
|
162
|
|
|
163 1. Syntax of ITL Formula
|
|
|
164
|
|
|
165 Comma for conjunction, and semi-coron for disjunction as in Prolog.
|
|
|
166 & for chop operator. @ for strong next. next(P) for weak next.
|
|
|
167 Postfix * means weak closure, that is, it allows 0 times execution.
|
|
|
168 To use existential quantifier, a form exists(R,f(R)) is used,
|
|
|
169 here R have to be Prolog variable.
|
|
|
170
|
|
|
171 Other definitions are found in chop.pl. If you want to see the expanding
|
|
|
172 results ( chop normal form, cannot be readable...) use ?-expand(X,Y).
|
|
|
173
|
|
|
174 ~(P) = not(P)
|
|
|
175 P->Q = (not(P);Q)
|
|
|
176 P<->Q = ((not(P);Q),(P; not(Q)))
|
|
|
177 P=Q = ((not(P);Q),(P; not(Q)))
|
|
|
178 (P && Q) = ((not(empty),P) & Q) strong chop
|
|
|
179 <>(Q) = (true & Q)
|
|
|
180 #(Q) = not(true & not(Q))
|
|
|
181 [](Q) = not(true & not(Q))
|
|
|
182 '[a]'(Q) = not(true & not(Q) & true)
|
|
|
183 fin(Q) = (true & (empty,Q))
|
|
|
184 halt(Q) = [](empty=Q)
|
|
|
185 keep(Q) = not(true & not((empty ; Q)))
|
|
|
186 more = not(empty)
|
|
|
187 skip = @(empty)
|
|
|
188 length(I) expanded into series of strong next.
|
|
|
189 less(I) expanded into series of weak next.
|
|
|
190 next(P) = (empty; @(P))
|
|
|
191 gets(A,B) = keep(@A<->B)
|
|
|
192 stable(A) = keep(@A<->A)
|
|
|
193
|
|
16
|
194 infinite = (true&false)
|
|
|
195 finite = ~infinite
|
|
|
196
|
|
2
|
197 P proj Q = Q is true using P as a clock period
|
|
|
198 *P = P&P&..&P.. chop infinite closure
|
|
|
199
|
|
|
200 Q=>P = exists(R,(Q = R,stable(R),fin(P = R)))
|
|
|
201 P<=Q = Q=>P
|
|
|
202 +A = (A & (empty;A) *) strong closure
|
|
|
203 while(Cond,Do) = ((Cond->Do) , (~Cond->empty)) *
|
|
|
204 exists(P,Q) = Exsistential Quantifier
|
|
|
205 all(P,Q) = not(exists(P,not(Q)))
|
|
|
206
|
|
|
207 even(P) = exists(Q,(Q, keep( @Q = ~Q),[](Q->P)))
|
|
|
208 evenp(P) = ((P,skip) & skip;empty,P)* & (empty;skip)
|
|
|
209 phil(L,R) = ([]((~L = ~R)) & @ (L, ~R,@ (L,R, @ (R,[]( ~L)))) )
|
|
|
210
|
|
|
211 For user define predicate use define/2. Ex.
|
|
|
212 define(yeilds(A,B), not(not(A) & B)).
|
|
|
213
|
|
|
214
|
|
|
215 1.1 Finte State Automaton support
|
|
|
216
|
|
|
217 1.1.1 Output.
|
|
|
218
|
|
|
219 This version supports Finite State Automaton I/O. The output of
|
|
|
220 our verifier is finite automaton.
|
|
|
221
|
|
|
222 ?-tgen.
|
|
|
223
|
|
|
224 generates automaton as Tokio Temporal Logic Programming Language.
|
|
|
225 KISS2 format output is also supported, see 0.2.
|
|
|
226
|
|
|
227 1.1.2 Input
|
|
|
228
|
|
|
229 It is possible to use automaton as a part of ITL formula.
|
|
|
230 Finite automaton is stored in Prolog clauses.
|
|
|
231
|
|
|
232 st(s0) starts Finite State Automaton (FSA) from s0 states.
|
|
|
233 This is a temporal logic term, so you can use this anywhere
|
|
|
234 in ITL formula, for example: st(s0) & not(st(s0)), <>(st(s0)).
|
|
|
235 FSA is defined as Prolog clauses in this way:
|
|
|
236
|
|
|
237 st_variables([q],[s]).
|
|
|
238 % st_varaibles(Input_variables,Output_variables)
|
|
|
239 % This is important only for KISS format generation
|
|
|
240
|
|
|
241 st(s0,((not(a);not(b)),q),s0).
|
|
|
242 % st(Current_State, Condition, Next_State)
|
|
|
243 st(s1,(not(c),q),s1).
|
|
|
244 st(s1, empty,empty).
|
|
|
245
|
|
|
246 Conditions can be non-deterministic. Actually it allows
|
|
|
247 arbitrary ITL formula, but if you use temporal condtions,
|
|
|
248 it is not a state machine any more. The automaton is
|
|
|
249 determinized during verfication, since generated state
|
|
|
250 machine is determinisc. Be careful, the output can be very large.
|
|
|
251
|
|
|
252 If a state machine contains no empty conditions, it is
|
|
|
253 not satisfiable in ITL, because our ITL only have finite
|
|
|
254 interval. But it may contains infinite clock periods.
|
|
|
255
|
|
|
256 2. Basic Algorithm of the Verifier
|
|
|
257
|
|
|
258 This program uses classic tableau method. So hold your breath, it is
|
|
|
259 exponential to the number of the variables in the formula and also
|
|
|
260 combinatorial to the nesting of temporal logic operator. I think it is
|
|
|
261 possible to reduce complexity for the nesting, but not for the
|
|
|
262 variables.
|
|
|
263
|
|
|
264 Major contribution (I think) is in the classification of ITL formula,
|
|
|
265 which is found in bdtstd.pl. I use binary decision tree (not diagram)
|
|
|
266 standard form among subterms in original formula. Since this program
|
|
|
267 always keep state machine deterministic, determinization of state
|
|
|
268 machine is done by outer-most loop.
|
|
|
269
|
|
|
270 The algorithm is quite simple. There are three stages. In the first
|
|
|
271 stage, an ITL formula is decomposed into three parts: empty, now and
|
|
|
272 next. In the second stage, next parts is classifyed using subterm bdt
|
|
|
273 and stored into database. In the third stage, decomposition is
|
|
|
274 repeatedly applied until no more new next parts are generated.
|
|
|
275
|
|
|
276 Since ITL assumes any interval is finite, no eventuality checking is
|
|
|
277 necessary. Diagnosis algorithm is linear to the number of the state.
|
|
|
278
|
|
|
279 3. Wish lists
|
|
|
280
|
|
|
281 It is possible to reduce complexity in somehow.
|
|
|
282
|
|
|
283 4. Brief description of this program.
|
|
|
284
|
|
|
285 File exdev.pl contains main driver of tableau based interval temporal
|
|
|
286 logic verifier. A developer deve(X) does tableau development.
|
|
|
287
|
|
|
288 deve(ITL) :-
|
|
|
289 init,!,
|
|
|
290 expand(ITL,ITL0),
|
|
|
291 itlstd(ITL0,StdNext),
|
|
|
292 check_state(StdNext,ITL0,_,S),!,
|
|
|
293 deve0((S,ITL0)).
|
|
|
294
|
|
|
295 In init, formula databases are initialized.
|
|
|
296 Usually ITL formula contains several macro definitions, expand(X,Y)
|
|
|
297 expands these macros form X to Y.
|
|
|
298 The formula is translated into standard form in itlstd(X,Y), where X is original
|
|
|
299 formula and Y is binary decision tree standard form (not diagram).
|
|
|
300 The formula databases are maintained in check_state(Stdoriginal,NewFlag,No).
|
|
|
301 Std is the standard form. We need original formula here for display.
|
|
|
302 Whether Std is already in database or not is shown in NewFlag and when
|
|
|
303 database sequence number (i.e. state number) is returned in No.
|
|
|
304
|
|
|
305 deve0((S,ITL)) :-
|
|
|
306 show_state(S,ITL),
|
|
|
307 setof(Next,itldecomp(ITL,Next,S),
|
|
|
308 Nexts),!,
|
|
|
309 deve1(Nexts).
|
|
|
310 deve0(_).
|
|
|
311
|
|
|
312 We are now in deve0(X) predicates. After displaying current states, it
|
|
|
313 gathers possible tableau expansion using setof predicates. Since not so
|
|
|
314 many formula is generated from one state, setof is not a bottle neck of
|
|
|
315 this program. The real bottle neck is total number of state/condition pair and
|
|
|
316 it's database looking up. Setof predicates returns only new candidates and
|
|
|
317 theses are stored in a list, in LIFO way.
|
|
|
318
|
|
|
319 deve1([]).
|
|
|
320 deve1([H|T]) :- deve0(H),deve1(T).
|
|
|
321
|
|
|
322 Here is a repetition part.
|
|
|
323
|
|
|
324 itldecomp(ITL,(NextS,Next),From) :-
|
|
|
325 itl(ITL,Next,Cond),
|
|
|
326 %% showing
|
|
|
327 itlshow(Next,NextS,Cond,From).
|
|
|
328
|
|
|
329 Actual tableau expansion is done by itl(ITL,Next,Cond). It generate
|
|
|
330 Sumof( Cond -> @(Next) ), where Cond is exclusive, that is, it generates
|
|
|
331 deterministic automaton. You can test itl predicates by hands, for example,
|
|
|
332 ?-itl(p & q,Next,Cond).
|
|
|
333
|
|
|
334 itlshow(Next,S,Cond,From):-
|
|
|
335 itlstd(Next,StdNext),
|
|
|
336 check_state(StdNext,Next,New,S),
|
|
|
337 assertz(state(From,Cond,S)),
|
|
|
338 !,itlshow1(S,Cond,Next,New).
|
|
|
339
|
|
|
340 In itlshow, standard form conversion and database checking is performed.
|
|
|
341 Rest of parts are related to state database and displaying.
|
|
|
342
|
|
|
343 That's all. There are more stories about itlstd and itl predicates, but it is
|
|
|
344 better to look source code rather than vague English...
|
|
|
345
|
