|
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
|
|
|
85 In case of a large formula, you may want to make output tarse.
|
|
|
86
|
|
|
87 ?-verbose(off).
|
|
|
88 generates one character per state transition condition.
|
|
|
89 e empty
|
|
|
90 t true
|
|
|
91 f false
|
|
|
92 123. newly genrated state number
|
|
|
93 . transition to a registerd state
|
|
|
94 ?-verbose(on).
|
|
|
95
|
|
|
96 ?-ex. runs all examples in diag.pl. But it takes several hours.
|
|
|
97 Some of the examples are quite large.
|
|
|
98 ?-exex. runs all examples and save state machine in file ``ex''.
|
|
|
99
|
|
|
100 0.1. X-Window Interace
|
|
|
101
|
|
|
102 If you want to run X-window version, you have to install InterViews
|
|
|
103 interface for SICSTUS. It requires ispgm binary and library/gmlib.
|
|
|
104 ?-[demoim]. % This loads and runs X-window interface.
|
|
|
105 Type-in a formula.
|
|
|
106 ex(1) or demo(1) for the example number in ex.pl.
|
|
|
107 Push verify buttom and execute buttom in order.
|
|
|
108 Execute and Counter Example buttons show an example in a graphical way.
|
|
|
109 Map button shows bitmap of the characteristic function.
|
|
|
110
|
|
|
111 0.1.1 Tcl/Tk Interface
|
|
|
112
|
|
|
113
|
|
|
114 0.2. KISS format interface
|
|
|
115
|
|
|
116 To generate KISS2 format for SIS, try run
|
|
|
117
|
|
|
118 ?-kiss.
|
|
|
119
|
|
|
120 right after verification. To specify input variables and
|
|
|
121 output variables assert this predicate:
|
|
|
122 st_variables(In,Out).
|
|
|
123 State machine description is also supported
|
|
|
124 in this system. You can read a KISS2 format state machine.
|
|
|
125 Only one state machine is accepted because of variable
|
|
|
126 declaration.
|
|
|
127
|
|
|
128 ?- read_kiss(File,In,Out,Empty).
|
|
|
129
|
|
|
130 reads KISS2 format. In and Out are list of variables in the order
|
|
|
131 of the KISS2 file. If Out is [], output variales are omitted.
|
|
|
132 If In or Out are uninstantiated variables, name 'i0' or 'o2'
|
|
|
133 are used. Empty is usually set to empty and it generates
|
|
|
134 empty condition for each state, for example:
|
|
|
135 st(st0,empty,empty).
|
|
|
136 To modify or to generate KISS format again, you have to
|
|
|
137 verify it.
|
|
|
138 ?- ex(st(st0)).
|
|
|
139 `st0' is the start state of automaton. The state machine can
|
|
|
140 be used in arbitrary temporal logic expression. But if you
|
|
|
141 generate very non-deterministic modification, the output
|
|
|
142 can be very large. For examle:
|
|
|
143 ?- ex(exists(i0,st(st0))).
|
|
|
144
|
|
|
145 ?- read_kiss(File).
|
|
|
146 => read_kiss(File,_,_,empty)
|
|
|
147 ?- read_kiss(File,Empty).
|
|
|
148 => read_kiss(File,_,_,Empty)
|
|
|
149
|
|
|
150 0.3
|
|
|
151 dvcomp.pl contains lazy state transition clause generation and binary
|
|
|
152 tree representation of ITL term. Reconsult it after [init]. It
|
|
|
153 reduces memory usage drastically. To control lazy generation, use:
|
|
|
154 ?-lazy(on).
|
|
|
155 ?-lazy(off).
|
|
|
156 kiss format generation is not supported for lazy generation.
|
|
|
157
|
|
|
158 1. Syntax of ITL Formula
|
|
|
159
|
|
|
160 Comma for conjunction, and semi-coron for disjunction as in Prolog.
|
|
|
161 & for chop operator. @ for strong next. next(P) for weak next.
|
|
|
162 Postfix * means weak closure, that is, it allows 0 times execution.
|
|
|
163 To use existential quantifier, a form exists(R,f(R)) is used,
|
|
|
164 here R have to be Prolog variable.
|
|
|
165
|
|
|
166 Other definitions are found in chop.pl. If you want to see the expanding
|
|
|
167 results ( chop normal form, cannot be readable...) use ?-expand(X,Y).
|
|
|
168
|
|
|
169 ~(P) = not(P)
|
|
|
170 P->Q = (not(P);Q)
|
|
|
171 P<->Q = ((not(P);Q),(P; not(Q)))
|
|
|
172 P=Q = ((not(P);Q),(P; not(Q)))
|
|
|
173 (P && Q) = ((not(empty),P) & Q) strong chop
|
|
|
174 <>(Q) = (true & Q)
|
|
|
175 #(Q) = not(true & not(Q))
|
|
|
176 [](Q) = not(true & not(Q))
|
|
|
177 '[a]'(Q) = not(true & not(Q) & true)
|
|
|
178 fin(Q) = (true & (empty,Q))
|
|
|
179 halt(Q) = [](empty=Q)
|
|
|
180 keep(Q) = not(true & not((empty ; Q)))
|
|
|
181 more = not(empty)
|
|
|
182 skip = @(empty)
|
|
|
183 length(I) expanded into series of strong next.
|
|
|
184 less(I) expanded into series of weak next.
|
|
|
185 next(P) = (empty; @(P))
|
|
|
186 gets(A,B) = keep(@A<->B)
|
|
|
187 stable(A) = keep(@A<->A)
|
|
|
188
|
|
|
189 P proj Q = Q is true using P as a clock period
|
|
|
190 *P = P&P&..&P.. chop infinite closure
|
|
|
191
|
|
|
192 Q=>P = exists(R,(Q = R,stable(R),fin(P = R)))
|
|
|
193 P<=Q = Q=>P
|
|
|
194 +A = (A & (empty;A) *) strong closure
|
|
|
195 while(Cond,Do) = ((Cond->Do) , (~Cond->empty)) *
|
|
|
196 exists(P,Q) = Exsistential Quantifier
|
|
|
197 all(P,Q) = not(exists(P,not(Q)))
|
|
|
198
|
|
|
199 even(P) = exists(Q,(Q, keep( @Q = ~Q),[](Q->P)))
|
|
|
200 evenp(P) = ((P,skip) & skip;empty,P)* & (empty;skip)
|
|
|
201 phil(L,R) = ([]((~L = ~R)) & @ (L, ~R,@ (L,R, @ (R,[]( ~L)))) )
|
|
|
202
|
|
|
203 For user define predicate use define/2. Ex.
|
|
|
204 define(yeilds(A,B), not(not(A) & B)).
|
|
|
205
|
|
|
206
|
|
|
207 1.1 Finte State Automaton support
|
|
|
208
|
|
|
209 1.1.1 Output.
|
|
|
210
|
|
|
211 This version supports Finite State Automaton I/O. The output of
|
|
|
212 our verifier is finite automaton.
|
|
|
213
|
|
|
214 ?-tgen.
|
|
|
215
|
|
|
216 generates automaton as Tokio Temporal Logic Programming Language.
|
|
|
217 KISS2 format output is also supported, see 0.2.
|
|
|
218
|
|
|
219 1.1.2 Input
|
|
|
220
|
|
|
221 It is possible to use automaton as a part of ITL formula.
|
|
|
222 Finite automaton is stored in Prolog clauses.
|
|
|
223
|
|
|
224 st(s0) starts Finite State Automaton (FSA) from s0 states.
|
|
|
225 This is a temporal logic term, so you can use this anywhere
|
|
|
226 in ITL formula, for example: st(s0) & not(st(s0)), <>(st(s0)).
|
|
|
227 FSA is defined as Prolog clauses in this way:
|
|
|
228
|
|
|
229 st_variables([q],[s]).
|
|
|
230 % st_varaibles(Input_variables,Output_variables)
|
|
|
231 % This is important only for KISS format generation
|
|
|
232
|
|
|
233 st(s0,((not(a);not(b)),q),s0).
|
|
|
234 % st(Current_State, Condition, Next_State)
|
|
|
235 st(s1,(not(c),q),s1).
|
|
|
236 st(s1, empty,empty).
|
|
|
237
|
|
|
238 Conditions can be non-deterministic. Actually it allows
|
|
|
239 arbitrary ITL formula, but if you use temporal condtions,
|
|
|
240 it is not a state machine any more. The automaton is
|
|
|
241 determinized during verfication, since generated state
|
|
|
242 machine is determinisc. Be careful, the output can be very large.
|
|
|
243
|
|
|
244 If a state machine contains no empty conditions, it is
|
|
|
245 not satisfiable in ITL, because our ITL only have finite
|
|
|
246 interval. But it may contains infinite clock periods.
|
|
|
247
|
|
|
248 2. Basic Algorithm of the Verifier
|
|
|
249
|
|
|
250 This program uses classic tableau method. So hold your breath, it is
|
|
|
251 exponential to the number of the variables in the formula and also
|
|
|
252 combinatorial to the nesting of temporal logic operator. I think it is
|
|
|
253 possible to reduce complexity for the nesting, but not for the
|
|
|
254 variables.
|
|
|
255
|
|
|
256 Major contribution (I think) is in the classification of ITL formula,
|
|
|
257 which is found in bdtstd.pl. I use binary decision tree (not diagram)
|
|
|
258 standard form among subterms in original formula. Since this program
|
|
|
259 always keep state machine deterministic, determinization of state
|
|
|
260 machine is done by outer-most loop.
|
|
|
261
|
|
|
262 The algorithm is quite simple. There are three stages. In the first
|
|
|
263 stage, an ITL formula is decomposed into three parts: empty, now and
|
|
|
264 next. In the second stage, next parts is classifyed using subterm bdt
|
|
|
265 and stored into database. In the third stage, decomposition is
|
|
|
266 repeatedly applied until no more new next parts are generated.
|
|
|
267
|
|
|
268 Since ITL assumes any interval is finite, no eventuality checking is
|
|
|
269 necessary. Diagnosis algorithm is linear to the number of the state.
|
|
|
270
|
|
|
271 3. Wish lists
|
|
|
272
|
|
|
273 It is possible to reduce complexity in somehow.
|
|
|
274
|
|
|
275 4. Brief description of this program.
|
|
|
276
|
|
|
277 File exdev.pl contains main driver of tableau based interval temporal
|
|
|
278 logic verifier. A developer deve(X) does tableau development.
|
|
|
279
|
|
|
280 deve(ITL) :-
|
|
|
281 init,!,
|
|
|
282 expand(ITL,ITL0),
|
|
|
283 itlstd(ITL0,StdNext),
|
|
|
284 check_state(StdNext,ITL0,_,S),!,
|
|
|
285 deve0((S,ITL0)).
|
|
|
286
|
|
|
287 In init, formula databases are initialized.
|
|
|
288 Usually ITL formula contains several macro definitions, expand(X,Y)
|
|
|
289 expands these macros form X to Y.
|
|
|
290 The formula is translated into standard form in itlstd(X,Y), where X is original
|
|
|
291 formula and Y is binary decision tree standard form (not diagram).
|
|
|
292 The formula databases are maintained in check_state(Stdoriginal,NewFlag,No).
|
|
|
293 Std is the standard form. We need original formula here for display.
|
|
|
294 Whether Std is already in database or not is shown in NewFlag and when
|
|
|
295 database sequence number (i.e. state number) is returned in No.
|
|
|
296
|
|
|
297 deve0((S,ITL)) :-
|
|
|
298 show_state(S,ITL),
|
|
|
299 setof(Next,itldecomp(ITL,Next,S),
|
|
|
300 Nexts),!,
|
|
|
301 deve1(Nexts).
|
|
|
302 deve0(_).
|
|
|
303
|
|
|
304 We are now in deve0(X) predicates. After displaying current states, it
|
|
|
305 gathers possible tableau expansion using setof predicates. Since not so
|
|
|
306 many formula is generated from one state, setof is not a bottle neck of
|
|
|
307 this program. The real bottle neck is total number of state/condition pair and
|
|
|
308 it's database looking up. Setof predicates returns only new candidates and
|
|
|
309 theses are stored in a list, in LIFO way.
|
|
|
310
|
|
|
311 deve1([]).
|
|
|
312 deve1([H|T]) :- deve0(H),deve1(T).
|
|
|
313
|
|
|
314 Here is a repetition part.
|
|
|
315
|
|
|
316 itldecomp(ITL,(NextS,Next),From) :-
|
|
|
317 itl(ITL,Next,Cond),
|
|
|
318 %% showing
|
|
|
319 itlshow(Next,NextS,Cond,From).
|
|
|
320
|
|
|
321 Actual tableau expansion is done by itl(ITL,Next,Cond). It generate
|
|
|
322 Sumof( Cond -> @(Next) ), where Cond is exclusive, that is, it generates
|
|
|
323 deterministic automaton. You can test itl predicates by hands, for example,
|
|
|
324 ?-itl(p & q,Next,Cond).
|
|
|
325
|
|
|
326 itlshow(Next,S,Cond,From):-
|
|
|
327 itlstd(Next,StdNext),
|
|
|
328 check_state(StdNext,Next,New,S),
|
|
|
329 assertz(state(From,Cond,S)),
|
|
|
330 !,itlshow1(S,Cond,Next,New).
|
|
|
331
|
|
|
332 In itlshow, standard form conversion and database checking is performed.
|
|
|
333 Rest of parts are related to state database and displaying.
|
|
|
334
|
|
|
335 That's all. There are more stories about itlstd and itl predicates, but it is
|
|
|
336 better to look source code rather than vague English...
|
|
|
337
|
