Mercurial > hg > Applications > Lite

comparison read.me @ 2:1c57a78f1d98

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Initial revision
author kono
date Thu, 18 Jan 2001 23:27:24 +0900
parents
children 4360c2030303
comparison
equal deleted inserted replaced
1:683efd6f9a81 2:1c57a78f1d98
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