Mercurial > hg > Applications > Lite

comparison ex.pl @ 19:e1d3145cff7a lite-verifier

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
*** empty log message ***
author kono
date Thu, 30 Aug 2007 12:44:35 +0900
parents 4360c2030303
children 29cf617f49db
comparison
equal deleted inserted replaced
18:a6adedccd5f6 19:e1d3145cff7a
72 *( ('[]'((~dl, ~dr)) & @ (dl, ~dr,@ (dl,dr, @ (dr,'[]'( ~dl)))) ;empty) ) , 72 *( ('[]'((~dl, ~dr)) & @ (dl, ~dr,@ (dl,dr, @ (dr,'[]'( ~dl)))) ;empty) ) ,
73 *( ('[]'((~el, ~er)) & @ (el, ~er,@ (el,er, @ (er,'[]'( ~el)))) ;empty) ) , 73 *( ('[]'((~el, ~er)) & @ (el, ~er,@ (el,er, @ (er,'[]'( ~el)))) ;empty) ) ,
74 % shared resources 74 % shared resources
75 '[]'( ~ ( ar, bl)), '[]'( ~ ( br, cl)), '[]'( ~ ( cr, dl)), 75 '[]'( ~ ( ar, bl)), '[]'( ~ ( br, cl)), '[]'( ~ ( cr, dl)),
76 '[]'( ~ ( dr, el)), '[]'( ~ ( er, al)) 76 '[]'( ~ ( dr, el)), '[]'( ~ ( er, al))
77 )):-fail. % too big to verify (sigh...) 77 )). % :-fail. % too big to verify (sigh...)
78 78
79 ex(21,(more, 79 ex(21,(more,
80 share([ar,bl]),share([br,cl]),share([cr,dl]), 80 share([ar,bl]),share([br,cl]),share([cr,dl]),
81 share([dr,el]),share([er,al]), 81 share([dr,el]),share([er,al]),
82 *( ((true && '[]'(al) && '[]'((al,ar)) && '[]'(ar));empty) ) , 82 *( ((true && '[]'(al) && '[]'((al,ar)) && '[]'(ar));empty) ) ,
83 *( ((true && '[]'(bl) && '[]'((bl,br)) && '[]'(br));empty) ) , 83 *( ((true && '[]'(bl) && '[]'((bl,br)) && '[]'(br));empty) ) ,
84 *( ((true && '[]'(cl) && '[]'((cl,cr)) && '[]'(cr));empty) ) , 84 *( ((true && '[]'(cl) && '[]'((cl,cr)) && '[]'(cr));empty) ) ,
85 *( ((true && '[]'(dl) && '[]'((dl,dr)) && '[]'(dr));empty) ) , 85 *( ((true && '[]'(dl) && '[]'((dl,dr)) && '[]'(dr));empty) ) ,
86 *( ((true && '[]'(el) && '[]'((el,er)) && '[]'(er));empty) ) , 86 *( ((true && '[]'(el) && '[]'((el,er)) && '[]'(er));empty) ) ,
87 true)):-fail. % too big to verify (sigh...) 87 true)). % :-fail. % too big to verify (sigh...)
88 88
89 ex(22,(more, 89 ex(22,(more,
90 % three philosophers with no iteration 90 % three philosophers with no iteration
91 ( ('[]'((~al, ~ar)) & @ (al, ~ar,@ (al,ar, @ (ar,'[]'( ~al)))) ;empty) ) , 91 ( ('[]'((~al, ~ar)) & @ (al, ~ar,@ (al,ar, @ (ar,'[]'( ~al)))) ;empty) ) ,
92 ( ('[]'((~bl, ~br)) & @ (bl, ~br,@ (bl,br, @ (br,'[]'( ~bl)))) ;empty) ) , 92 ( ('[]'((~bl, ~br)) & @ (bl, ~br,@ (bl,br, @ (br,'[]'( ~bl)))) ;empty) ) ,
112 ex(109,(('<>'a)-> '[]'('<>'(a)))). % 5 112 ex(109,(('<>'a)-> '[]'('<>'(a)))). % 5
113 113
114 ex(110,(more-> (more&more))). % our dense time 114 ex(110,(more-> (more&more))). % our dense time
115 115
116 ex(demo(X),Y) :- demo(X,Y). 116 ex(demo(X),Y) :- demo(X,Y).
117 demo(X) :- number(X),demo(X,ITL),nl,ex(ITL),nl,write(ITL).
118
119 % length 5 interval
120 demo(1, length(5)).
121
122 % p is trun at the top of a interval
123 demo(2, (length(5),p)).
124
125 % @ meas next time.
126 demo(3, (length(5),@p,@ @q,@ @ @r)).
127
128 % &(chop) devides an interval into to parts
129 demo(4, ((length(2),p)) & (length(3),q)).
130
131 % there are several ways of division.
132 demo(5, (length(5),(p&q))).
133
134 % sometime usinng chop
135 demo(6, (length(5),(true & p))).
136
137 % always: dual of sometime
138 demo(7, (length(5),not(true & not(p)))).
139
140 % counter intutive theorem
141 demo(8, '<>' '[]'(p) = '[]'('<>'(p))).
142
143 % shared resource / exclusive condition
144 demo(9, (length(5),
145 '[]'((( ac ,not(bc),not(cc),not(dc));
146 (not(ac), bc ,not(cc),not(dc));
147 (not(ac),not(bc), cc ,not(dc));
148 (not(ac),not(bc),not(cc), dc ))))).
149
150 % periodical task by Projection
151 demo(10, (more,
152 proj((@ '<>'(q),length(2)),true))).
153
154 % time sharing taks by Projection
155 demo(11, (more,length(7),
156 proj(true,('[]'(p),length(4))))).
157
158 % combination of periodical task
159 demo(12, (more,
160 proj(length(2),'[]'(ac)),
161 proj(length(3),'[]'(bc)),
162 proj(length(5),'[]'(cc)))).
163
164 % periodical task with shared resources
165 demo(13, (more,
166 proj((length(3),@ '<>'(ac)),true),
167 proj((length(5),@ '<>'(bc)),true),
168 proj((length(5),@ '<>'(cc)),true),
169 '[]'((not((ac,bc)),not((bc,cc)),not((cc,ac)))),
170 true)).
171
172 % combination of periodical taks and aperiodical task with shared resource
173 demo(14, (
174 ((proj(true,(length(5),'[]'(dc))),length(15) )&true),
175 proj((length(3),@ '<>'(ac)),true),
176 proj((length(5),@ '<>'(bc)),true),
177 proj((length(5),@ '<>'(cc)),true),
178 '[]'((( ac ,not(bc),not(cc),not(dc));
179 (not(ac), bc ,not(cc),not(dc));
180 (not(ac),not(bc), cc ,not(dc));
181 (not(ac),not(bc),not(cc), dc ))),
182 true)).
183 % combination of periodical taks and aperiodical task with shared resource
184 % schedulable case
185 demo(15, (
186 ((proj(true,(length(4),'[]'(dc))),length(15) )&true),
187 proj((length(3),@ '<>'(ac)),true),
188 proj((length(5),@ '<>'(bc)),true),
189 proj((length(5),@ '<>'(cc)),true),
190 '[]'((( ac ,not(bc),not(cc),not(dc));
191 (not(ac), bc ,not(cc),not(dc));
192 (not(ac),not(bc), cc ,not(dc));
193 (not(ac),not(bc),not(cc), dc ))),
194 true)).
195
196
197 % model restriction by share predicate ( a little smaller.... :-)
198 demo(16, (
199 share([ac,bc,cc,dc]),
200 ((proj(true,(length(4),'[]'(dc))),length(15) )&true),
201 proj((length(3),@ '<>'(ac)),true),
202 proj((length(5),@ '<>'(bc)),true),
203 proj((length(5),@ '<>'(cc)),true),
204 true)).
205 demo(17, (
206 ((proj(true,(length(5),'[]'(c))),length(15))&true),
207 (proj((length(3),@ '<>'(a)),true)&less(3)),
208 (proj((length(5),@ '<>'(b)),true)&less(5)),
209 '[]'(not((a,b))),
210 '[]'(not((b,c))),
211 '[]'(not((c,a)))
212 )).
213
214 % Regular variable examples ( doesnot work now....) 117 % Regular variable examples ( doesnot work now....)
215 118
216 ex(200,^r). 119 ex(200,^r).
217 ex(201,true & ^r). % will terminate? 120 ex(201,true & ^r). % will terminate?
218 ex(202,((^r & ^r),not(^r))). % is non-local? 121 ex(202,((^r & ^r),not(^r))). % is non-local?
265 ex(407,((less(5),[](q))&(length(3)&([](<>(p)),[](<>(~p)),*length(6))))). 168 ex(407,((less(5),[](q))&(length(3)&([](<>(p)),[](<>(~p)),*length(6))))).
266 ex(408,(infinite -> ~(<>([](p)) = [](<>(p))))). % satisfiable 169 ex(408,(infinite -> ~(<>([](p)) = [](<>(p))))). % satisfiable
267 ex(409,finite). % unsatisfiable 170 ex(409,finite). % unsatisfiable
268 171
269 172
173 demo(X) :- number(X),demo(X,ITL),nl,ex(ITL),nl,write(ITL).
174
175 % length 5 interval
176 demo(1, length(5)).
177
178 % p is trun at the top of a interval
179 demo(2, (length(5),p)).
180
181 % @ meas next time.
182 demo(3, (length(5),@p,@ @q,@ @ @r)).
183
184 % &(chop) devides an interval into to parts
185 demo(4, ((length(2),p)) & (length(3),q)).
186
187 % there are several ways of division.
188 demo(5, (length(5),(p&q))).
189
190 % sometime usinng chop
191 demo(6, (length(5),(true & p))).
192
193 % always: dual of sometime
194 demo(7, (length(5),not(true & not(p)))).
195
196 % counter intutive theorem
197 demo(8, '<>' '[]'(p) = '[]'('<>'(p))).
198
199 % shared resource / exclusive condition
200 demo(9, (length(5),
201 '[]'((( ac ,not(bc),not(cc),not(dc));
202 (not(ac), bc ,not(cc),not(dc));
203 (not(ac),not(bc), cc ,not(dc));
204 (not(ac),not(bc),not(cc), dc ))))).
205
206 % periodical task by Projection
207 demo(10, (more,
208 proj((@ '<>'(q),length(2)),true))).
209
210 % time sharing taks by Projection
211 demo(11, (more,length(7),
212 proj(true,('[]'(p),length(4))))).
213
214 % combination of periodical task
215 demo(12, (more,
216 proj(length(2),'[]'(ac)),
217 proj(length(3),'[]'(bc)),
218 proj(length(5),'[]'(cc)))).
219
220 % periodical task with shared resources
221 demo(13, (more,
222 proj((length(3),@ '<>'(ac)),true),
223 proj((length(5),@ '<>'(bc)),true),
224 proj((length(5),@ '<>'(cc)),true),
225 '[]'((not((ac,bc)),not((bc,cc)),not((cc,ac)))),
226 true)).
227
228 % combination of periodical taks and aperiodical task with shared resource
229 demo(14, (
230 ((proj(true,(length(5),'[]'(dc))),length(15) )&true),
231 proj((length(3),@ '<>'(ac)),true),
232 proj((length(5),@ '<>'(bc)),true),
233 proj((length(5),@ '<>'(cc)),true),
234 '[]'((( ac ,not(bc),not(cc),not(dc));
235 (not(ac), bc ,not(cc),not(dc));
236 (not(ac),not(bc), cc ,not(dc));
237 (not(ac),not(bc),not(cc), dc ))),
238 true)).
239 % combination of periodical taks and aperiodical task with shared resource
240 % schedulable case
241 demo(15, (
242 ((proj(true,(length(4),'[]'(dc))),length(15) )&true),
243 proj((length(3),@ '<>'(ac)),true),
244 proj((length(5),@ '<>'(bc)),true),
245 proj((length(5),@ '<>'(cc)),true),
246 '[]'((( ac ,not(bc),not(cc),not(dc));
247 (not(ac), bc ,not(cc),not(dc));
248 (not(ac),not(bc), cc ,not(dc));
249 (not(ac),not(bc),not(cc), dc ))),
250 true)).
251
252
253 % model restriction by share predicate ( a little smaller.... :-)
254 demo(16, (
255 share([ac,bc,cc,dc]),
256 ((proj(true,(length(4),'[]'(dc))),length(15) )&true),
257 proj((length(3),@ '<>'(ac)),true),
258 proj((length(5),@ '<>'(bc)),true),
259 proj((length(5),@ '<>'(cc)),true),
260 true)).
261 demo(17, (
262 ((proj(true,(length(5),'[]'(c))),length(15))&true),
263 (proj((length(3),@ '<>'(a)),true)&less(3)),
264 (proj((length(5),@ '<>'(b)),true)&less(5)),
265 '[]'(not((a,b))),
266 '[]'(not((b,c))),
267 '[]'(not((c,a)))
268 )).
269
270 270
271 /* end */ 271 /* end */