|
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
|
|
22
|
10 $Id: ex.pl,v 1.5 2007/08/30 03:44:35 kono Exp $
|
|
2
|
11
|
|
|
12 Examples
|
|
|
13 */
|
|
|
14
|
|
|
15 ex(0,(p)).
|
|
|
16 ex(1,((p&q))).
|
|
|
17 ex(2,( (fin(p)&true) <-> '<>'p)).
|
|
|
18 ex(3,( fin(p) <-> '[]'( '<>' p) )).
|
|
|
19 ex(4,(~(true&q))).
|
|
|
20 ex(5,(~(true& ~q))).
|
|
|
21 ex(6,(((true& p),(true& q)))).
|
|
|
22 ex(7,('[]'((p -> '<>' q)))).
|
|
|
23 ex(8,( '<>' '[]'(p))).
|
|
|
24 ex(9,( '[]'( '<>'(p)))).
|
|
|
25 ex(10,((p && p && p && p && p && ~p && p)-> '[]'('<>'(p)))).
|
|
|
26 % weak closure (or finite closure)
|
|
|
27 ex(11,+ (a,@ (b,@ (c,@empty)))).
|
|
|
28 % quantifier
|
|
|
29 ex(12,exists(R,(R,keep(@R = ~R),'[]'((R->p))))).
|
|
|
30 % temporal assignment
|
|
22
|
31 ex(13,exists(R,(R = p,keep(@R = R),fin(R = q)))).
|
|
|
32
|
|
|
33 ex(133,
|
|
|
34 (exists(R,(q = R,stable(R),fin(p = R))))
|
|
|
35 =
|
|
|
36 (q & (empty,p); ~q & (empty, ~p))).
|
|
2
|
37 %
|
|
|
38 ex(14,
|
|
|
39 exists(Q,(Q,
|
|
|
40 '[]'((Q ->
|
|
|
41 (((((a,skip) & (b,skip)), @ keep(~Q)) & Q)
|
|
|
42 ;empty))
|
|
|
43 )))
|
|
|
44 <-> *(((a,skip) & (b,skip) ; empty))
|
|
|
45 ).
|
|
|
46 ex(15,
|
|
|
47 while(q,((a,skip) & (b,skip)))
|
|
|
48 <-> exists(C,(C,
|
|
|
49 '[]'(
|
|
|
50 (C ->
|
|
|
51 (((q -> ((a,skip) & (b,skip)), @ keep(~C)) & C),
|
|
|
52 (~q -> empty))
|
|
|
53 ))))
|
|
|
54 ).
|
|
|
55 ex(16,even(p)<->evenp(p)).
|
|
|
56 % wrong example, but hard to solve
|
|
|
57 % ex(17,(p=>(q=>r)) <-> ((p=>q)=>r)).
|
|
|
58 % ex(18,exists(Q,(p=>Q & Q=>r)) <-> (p=>r)).
|
|
|
59 % dining philosopher
|
|
|
60 % note: unspecified resource increase states
|
|
|
61 % ex ((true & al,skip & al,ar,skip & ar,~al,skip) ;empty) *
|
|
|
62 ex(19,(more,
|
|
|
63 % three philosophers
|
|
|
64 *( ('[]'((~al, ~ar)) & @ (al, ~ar,@ (al,ar, @ (ar,'[]'( ~al)))) ;empty) ) ,
|
|
|
65 *( ('[]'((~bl, ~br)) & @ (bl, ~br,@ (bl,br, @ (br,'[]'( ~bl)))) ;empty) ) ,
|
|
|
66 *( ('[]'((~cl, ~cr)) & @ (cl, ~cr,@ (cl,cr, @ (cr,'[]'( ~cl)))) ;empty) ) ,
|
|
|
67 % shared resources
|
|
|
68 '[]'( ~ ( ar, bl)),
|
|
|
69 '[]'( ~ ( br, cl)),
|
|
|
70 '[]'( ~ ( cr, al))
|
|
|
71 )).
|
|
|
72 ex(20,(more,
|
|
|
73 % five philosophers
|
|
|
74 *( ('[]'((~al, ~ar)) & @ (al, ~ar,@ (al,ar, @ (ar,'[]'( ~al)))) ;empty) ) ,
|
|
|
75 *( ('[]'((~bl, ~br)) & @ (bl, ~br,@ (bl,br, @ (br,'[]'( ~bl)))) ;empty) ) ,
|
|
|
76 *( ('[]'((~cl, ~cr)) & @ (cl, ~cr,@ (cl,cr, @ (cr,'[]'( ~cl)))) ;empty) ) ,
|
|
|
77 *( ('[]'((~dl, ~dr)) & @ (dl, ~dr,@ (dl,dr, @ (dr,'[]'( ~dl)))) ;empty) ) ,
|
|
|
78 *( ('[]'((~el, ~er)) & @ (el, ~er,@ (el,er, @ (er,'[]'( ~el)))) ;empty) ) ,
|
|
|
79 % shared resources
|
|
|
80 '[]'( ~ ( ar, bl)), '[]'( ~ ( br, cl)), '[]'( ~ ( cr, dl)),
|
|
|
81 '[]'( ~ ( dr, el)), '[]'( ~ ( er, al))
|
|
19
|
82 )). % :-fail. % too big to verify (sigh...)
|
|
2
|
83
|
|
|
84 ex(21,(more,
|
|
|
85 share([ar,bl]),share([br,cl]),share([cr,dl]),
|
|
|
86 share([dr,el]),share([er,al]),
|
|
|
87 *( ((true && '[]'(al) && '[]'((al,ar)) && '[]'(ar));empty) ) ,
|
|
|
88 *( ((true && '[]'(bl) && '[]'((bl,br)) && '[]'(br));empty) ) ,
|
|
|
89 *( ((true && '[]'(cl) && '[]'((cl,cr)) && '[]'(cr));empty) ) ,
|
|
|
90 *( ((true && '[]'(dl) && '[]'((dl,dr)) && '[]'(dr));empty) ) ,
|
|
|
91 *( ((true && '[]'(el) && '[]'((el,er)) && '[]'(er));empty) ) ,
|
|
19
|
92 true)). % :-fail. % too big to verify (sigh...)
|
|
2
|
93
|
|
|
94 ex(22,(more,
|
|
|
95 % three philosophers with no iteration
|
|
|
96 ( ('[]'((~al, ~ar)) & @ (al, ~ar,@ (al,ar, @ (ar,'[]'( ~al)))) ;empty) ) ,
|
|
|
97 ( ('[]'((~bl, ~br)) & @ (bl, ~br,@ (bl,br, @ (br,'[]'( ~bl)))) ;empty) ) ,
|
|
|
98 ( ('[]'((~cl, ~cr)) & @ (cl, ~cr,@ (cl,cr, @ (cr,'[]'( ~cl)))) ;empty) ) ,
|
|
|
99 % shared resources
|
|
|
100 '[]'( ~ ( ar, bl)),
|
|
|
101 '[]'( ~ ( br, cl)),
|
|
|
102 '[]'( ~ ( cr, al))
|
|
|
103 )).
|
|
|
104 % These are not schema. Just check
|
|
|
105 % Linear Time Axioms, valid in ITL
|
|
|
106 ex(100,('[]'((a->b)) -> ('[]'(a) -> '[]'(b)))). % K
|
|
|
107 ex(101,('[]'(((a , '[]'(a))->b));'[]'(((b , '[]'(b))->a)))). % 4
|
|
|
108 ex(102,('[]'(a)-> '<>'(a))). % D
|
|
|
109 ex(103,('[]'(a)-> '[]'('[]'(a)))). % L
|
|
|
110 ex(104,(('[]'(a)) -> a)). % T
|
|
|
111 ex(105,('[]'('[]'((((a-> '[]'(a)))->a))) -> ((('<>'('[]'(a)))-> '[]'(a))))). % Diodorean discreteness
|
|
|
112 % Linear Time Axioms, not valid in ITL
|
|
|
113 ex(106,('[]'(('[]'(a)->a))-> ((('<>'('[]'(a)))-> '[]'(a))))). % Z discreteness
|
|
|
114 ex(107,('[]'(('[]'(a)->a))-> ('[]'(a)))). % W weak density
|
|
|
115 % Other Axioms, not valid in ITL
|
|
|
116 ex(108,(a-> '[]'('<>'(a)))). % B
|
|
|
117 ex(109,(('<>'a)-> '[]'('<>'(a)))). % 5
|
|
|
118
|
|
|
119 ex(110,(more-> (more&more))). % our dense time
|
|
|
120
|
|
|
121 ex(demo(X),Y) :- demo(X,Y).
|
|
19
|
122 % Regular variable examples ( doesnot work now....)
|
|
|
123
|
|
|
124 ex(200,^r).
|
|
|
125 ex(201,true & ^r). % will terminate?
|
|
|
126 ex(202,((^r & ^r),not(^r))). % is non-local?
|
|
|
127 ex(203,(^r,length(4))). % distinguish different state?
|
|
|
128 ex(204,('[a]'(^r))). % non-deterministic?
|
|
|
129 ex(205,('[a]'(^r = length(2)))). % imitate length?
|
|
|
130 ex(206,('[a]'(^r = length(4)),(^r& ^r))).
|
|
|
131 ex(207,('[a]'(^r = (length(4);empty)),* ^r)).
|
|
|
132 ex(208,('[]'(^r = (
|
|
|
133 a,@ ^r;
|
|
|
134 not(a),c,@ @ ^r;
|
|
|
135 not(a),not(c),b,empty)),^r)). % RE
|
|
|
136 ex(209,('[a]'(^r = (
|
|
|
137 a,@((^r & @((b,empty)))) ;
|
|
|
138 not(a),b,empty)),
|
|
|
139 ^r)). % CFG
|
|
|
140
|
|
|
141 % Linear Time Axioms, valid in ITL
|
|
|
142 ex(210,('[]'((^a-> ^b)) -> ('[]'(^a) -> '[]'(^b)))). % K
|
|
|
143 ex(211,('[]'(((^a , '[]'(^a))-> ^b));'[]'(((^b , '[]'(^b))-> ^a)))). % 4
|
|
|
144 ex(212,('[]'(^a)-> '<>'(^a))). % D
|
|
|
145 ex(213,('[]'(^a)-> '[]'('[]'(^a)))). % L
|
|
|
146 ex(214,(('[]'(^a))-> ^a)). % T
|
|
|
147 % Diodorean discreteness
|
|
|
148 ex(215,('[]'('[]'((((^a-> '[]'(^a)))-> ^a))) -> ((('<>'('[]'(^a)))-> '[]'(^a))))).
|
|
|
149 % Linear Time Axioms, not valid in ITL
|
|
|
150 % Z discreteness
|
|
|
151 ex(216,('[]'(('[]'(^a)-> ^a))-> ((('<>'('[]'(^a)))-> '[]'(^a))))).
|
|
|
152 % W weak density
|
|
|
153 ex(217,('[]'(('[]'(^a)-> ^a))-> ('[]'(^a)))).
|
|
|
154 % Other Axioms, not v^alid in ITL
|
|
|
155 ex(218,(^a-> '[]'('<>'(^a)))). % B
|
|
|
156 ex(219,(('<>' ^a)-> '[]'('<>'(^a)))). % 5
|
|
|
157
|
|
|
158 % State Diagram Support
|
|
|
159
|
|
|
160 ex(300,(((length(2), @ '<>'(q)) proj true),
|
|
|
161 st(ns0)
|
|
|
162 )) :- ensure_loaded(kiss_ex).
|
|
|
163
|
|
|
164 % Infinite Interval
|
|
|
165
|
|
|
166 ex(400,infinite).
|
|
|
167 ex(401,*infinite).
|
|
|
168 ex(402,*skip).
|
|
|
169 ex(403,*length(5)).
|
|
|
170 ex(404,~('<>'(empty))).
|
|
|
171 ex(405,('<>'(empty))). % unsatisfiable
|
|
|
172 ex(406,(infinite-> @infinite)).
|
|
|
173 ex(407,((less(5),[](q))&(length(3)&([](<>(p)),[](<>(~p)),*length(6))))).
|
|
|
174 ex(408,(infinite -> ~(<>([](p)) = [](<>(p))))). % satisfiable
|
|
|
175 ex(409,finite). % unsatisfiable
|
|
|
176
|
|
|
177
|
|
2
|
178 demo(X) :- number(X),demo(X,ITL),nl,ex(ITL),nl,write(ITL).
|
|
|
179
|
|
|
180 % length 5 interval
|
|
|
181 demo(1, length(5)).
|
|
|
182
|
|
|
183 % p is trun at the top of a interval
|
|
|
184 demo(2, (length(5),p)).
|
|
|
185
|
|
|
186 % @ meas next time.
|
|
|
187 demo(3, (length(5),@p,@ @q,@ @ @r)).
|
|
|
188
|
|
|
189 % &(chop) devides an interval into to parts
|
|
|
190 demo(4, ((length(2),p)) & (length(3),q)).
|
|
|
191
|
|
|
192 % there are several ways of division.
|
|
|
193 demo(5, (length(5),(p&q))).
|
|
|
194
|
|
|
195 % sometime usinng chop
|
|
|
196 demo(6, (length(5),(true & p))).
|
|
|
197
|
|
|
198 % always: dual of sometime
|
|
|
199 demo(7, (length(5),not(true & not(p)))).
|
|
|
200
|
|
|
201 % counter intutive theorem
|
|
|
202 demo(8, '<>' '[]'(p) = '[]'('<>'(p))).
|
|
|
203
|
|
|
204 % shared resource / exclusive condition
|
|
|
205 demo(9, (length(5),
|
|
|
206 '[]'((( ac ,not(bc),not(cc),not(dc));
|
|
|
207 (not(ac), bc ,not(cc),not(dc));
|
|
|
208 (not(ac),not(bc), cc ,not(dc));
|
|
|
209 (not(ac),not(bc),not(cc), dc ))))).
|
|
|
210
|
|
|
211 % periodical task by Projection
|
|
|
212 demo(10, (more,
|
|
|
213 proj((@ '<>'(q),length(2)),true))).
|
|
|
214
|
|
|
215 % time sharing taks by Projection
|
|
|
216 demo(11, (more,length(7),
|
|
|
217 proj(true,('[]'(p),length(4))))).
|
|
|
218
|
|
|
219 % combination of periodical task
|
|
|
220 demo(12, (more,
|
|
|
221 proj(length(2),'[]'(ac)),
|
|
|
222 proj(length(3),'[]'(bc)),
|
|
|
223 proj(length(5),'[]'(cc)))).
|
|
|
224
|
|
|
225 % periodical task with shared resources
|
|
|
226 demo(13, (more,
|
|
|
227 proj((length(3),@ '<>'(ac)),true),
|
|
|
228 proj((length(5),@ '<>'(bc)),true),
|
|
|
229 proj((length(5),@ '<>'(cc)),true),
|
|
|
230 '[]'((not((ac,bc)),not((bc,cc)),not((cc,ac)))),
|
|
|
231 true)).
|
|
|
232
|
|
|
233 % combination of periodical taks and aperiodical task with shared resource
|
|
|
234 demo(14, (
|
|
|
235 ((proj(true,(length(5),'[]'(dc))),length(15) )&true),
|
|
|
236 proj((length(3),@ '<>'(ac)),true),
|
|
|
237 proj((length(5),@ '<>'(bc)),true),
|
|
|
238 proj((length(5),@ '<>'(cc)),true),
|
|
|
239 '[]'((( ac ,not(bc),not(cc),not(dc));
|
|
|
240 (not(ac), bc ,not(cc),not(dc));
|
|
|
241 (not(ac),not(bc), cc ,not(dc));
|
|
|
242 (not(ac),not(bc),not(cc), dc ))),
|
|
|
243 true)).
|
|
|
244 % combination of periodical taks and aperiodical task with shared resource
|
|
|
245 % schedulable case
|
|
|
246 demo(15, (
|
|
|
247 ((proj(true,(length(4),'[]'(dc))),length(15) )&true),
|
|
|
248 proj((length(3),@ '<>'(ac)),true),
|
|
|
249 proj((length(5),@ '<>'(bc)),true),
|
|
|
250 proj((length(5),@ '<>'(cc)),true),
|
|
|
251 '[]'((( ac ,not(bc),not(cc),not(dc));
|
|
|
252 (not(ac), bc ,not(cc),not(dc));
|
|
|
253 (not(ac),not(bc), cc ,not(dc));
|
|
|
254 (not(ac),not(bc),not(cc), dc ))),
|
|
|
255 true)).
|
|
|
256
|
|
|
257
|
|
|
258 % model restriction by share predicate ( a little smaller.... :-)
|
|
|
259 demo(16, (
|
|
|
260 share([ac,bc,cc,dc]),
|
|
|
261 ((proj(true,(length(4),'[]'(dc))),length(15) )&true),
|
|
|
262 proj((length(3),@ '<>'(ac)),true),
|
|
|
263 proj((length(5),@ '<>'(bc)),true),
|
|
|
264 proj((length(5),@ '<>'(cc)),true),
|
|
|
265 true)).
|
|
|
266 demo(17, (
|
|
|
267 ((proj(true,(length(5),'[]'(c))),length(15))&true),
|
|
|
268 (proj((length(3),@ '<>'(a)),true)&less(3)),
|
|
|
269 (proj((length(5),@ '<>'(b)),true)&less(5)),
|
|
|
270 '[]'(not((a,b))),
|
|
|
271 '[]'(not((b,c))),
|
|
|
272 '[]'(not((c,a)))
|
|
|
273 )).
|
|
|
274
|
|
14
|
275
|
|
2
|
276 /* end */
|
