|
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
|
|
|
10 $Id$
|
|
|
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
|
|
|
31 ex(13,exists(R,(R = p,keep(@R = R),fin(R = p)))).
|
|
|
32 %
|
|
|
33 ex(14,
|
|
|
34 exists(Q,(Q,
|
|
|
35 '[]'((Q ->
|
|
|
36 (((((a,skip) & (b,skip)), @ keep(~Q)) & Q)
|
|
|
37 ;empty))
|
|
|
38 )))
|
|
|
39 <-> *(((a,skip) & (b,skip) ; empty))
|
|
|
40 ).
|
|
|
41 ex(15,
|
|
|
42 while(q,((a,skip) & (b,skip)))
|
|
|
43 <-> exists(C,(C,
|
|
|
44 '[]'(
|
|
|
45 (C ->
|
|
|
46 (((q -> ((a,skip) & (b,skip)), @ keep(~C)) & C),
|
|
|
47 (~q -> empty))
|
|
|
48 ))))
|
|
|
49 ).
|
|
|
50 ex(16,even(p)<->evenp(p)).
|
|
|
51 % wrong example, but hard to solve
|
|
|
52 % ex(17,(p=>(q=>r)) <-> ((p=>q)=>r)).
|
|
|
53 % ex(18,exists(Q,(p=>Q & Q=>r)) <-> (p=>r)).
|
|
|
54 % dining philosopher
|
|
|
55 % note: unspecified resource increase states
|
|
|
56 % ex ((true & al,skip & al,ar,skip & ar,~al,skip) ;empty) *
|
|
|
57 ex(19,(more,
|
|
|
58 % three philosophers
|
|
|
59 *( ('[]'((~al, ~ar)) & @ (al, ~ar,@ (al,ar, @ (ar,'[]'( ~al)))) ;empty) ) ,
|
|
|
60 *( ('[]'((~bl, ~br)) & @ (bl, ~br,@ (bl,br, @ (br,'[]'( ~bl)))) ;empty) ) ,
|
|
|
61 *( ('[]'((~cl, ~cr)) & @ (cl, ~cr,@ (cl,cr, @ (cr,'[]'( ~cl)))) ;empty) ) ,
|
|
|
62 % shared resources
|
|
|
63 '[]'( ~ ( ar, bl)),
|
|
|
64 '[]'( ~ ( br, cl)),
|
|
|
65 '[]'( ~ ( cr, al))
|
|
|
66 )).
|
|
|
67 ex(20,(more,
|
|
|
68 % five philosophers
|
|
|
69 *( ('[]'((~al, ~ar)) & @ (al, ~ar,@ (al,ar, @ (ar,'[]'( ~al)))) ;empty) ) ,
|
|
|
70 *( ('[]'((~bl, ~br)) & @ (bl, ~br,@ (bl,br, @ (br,'[]'( ~bl)))) ;empty) ) ,
|
|
|
71 *( ('[]'((~cl, ~cr)) & @ (cl, ~cr,@ (cl,cr, @ (cr,'[]'( ~cl)))) ;empty) ) ,
|
|
|
72 *( ('[]'((~dl, ~dr)) & @ (dl, ~dr,@ (dl,dr, @ (dr,'[]'( ~dl)))) ;empty) ) ,
|
|
|
73 *( ('[]'((~el, ~er)) & @ (el, ~er,@ (el,er, @ (er,'[]'( ~el)))) ;empty) ) ,
|
|
|
74 % shared resources
|
|
|
75 '[]'( ~ ( ar, bl)), '[]'( ~ ( br, cl)), '[]'( ~ ( cr, dl)),
|
|
|
76 '[]'( ~ ( dr, el)), '[]'( ~ ( er, al))
|
|
|
77 )):-fail. % too big to verify (sigh...)
|
|
|
78
|
|
|
79 ex(21,(more,
|
|
|
80 share([ar,bl]),share([br,cl]),share([cr,dl]),
|
|
|
81 share([dr,el]),share([er,al]),
|
|
|
82 *( ((true && '[]'(al) && '[]'((al,ar)) && '[]'(ar));empty) ) ,
|
|
|
83 *( ((true && '[]'(bl) && '[]'((bl,br)) && '[]'(br));empty) ) ,
|
|
|
84 *( ((true && '[]'(cl) && '[]'((cl,cr)) && '[]'(cr));empty) ) ,
|
|
|
85 *( ((true && '[]'(dl) && '[]'((dl,dr)) && '[]'(dr));empty) ) ,
|
|
|
86 *( ((true && '[]'(el) && '[]'((el,er)) && '[]'(er));empty) ) ,
|
|
|
87 true)):-fail. % too big to verify (sigh...)
|
|
|
88
|
|
|
89 ex(22,(more,
|
|
|
90 % three philosophers with no iteration
|
|
|
91 ( ('[]'((~al, ~ar)) & @ (al, ~ar,@ (al,ar, @ (ar,'[]'( ~al)))) ;empty) ) ,
|
|
|
92 ( ('[]'((~bl, ~br)) & @ (bl, ~br,@ (bl,br, @ (br,'[]'( ~bl)))) ;empty) ) ,
|
|
|
93 ( ('[]'((~cl, ~cr)) & @ (cl, ~cr,@ (cl,cr, @ (cr,'[]'( ~cl)))) ;empty) ) ,
|
|
|
94 % shared resources
|
|
|
95 '[]'( ~ ( ar, bl)),
|
|
|
96 '[]'( ~ ( br, cl)),
|
|
|
97 '[]'( ~ ( cr, al))
|
|
|
98 )).
|
|
|
99 % These are not schema. Just check
|
|
|
100 % Linear Time Axioms, valid in ITL
|
|
|
101 ex(100,('[]'((a->b)) -> ('[]'(a) -> '[]'(b)))). % K
|
|
|
102 ex(101,('[]'(((a , '[]'(a))->b));'[]'(((b , '[]'(b))->a)))). % 4
|
|
|
103 ex(102,('[]'(a)-> '<>'(a))). % D
|
|
|
104 ex(103,('[]'(a)-> '[]'('[]'(a)))). % L
|
|
|
105 ex(104,(('[]'(a)) -> a)). % T
|
|
|
106 ex(105,('[]'('[]'((((a-> '[]'(a)))->a))) -> ((('<>'('[]'(a)))-> '[]'(a))))). % Diodorean discreteness
|
|
|
107 % Linear Time Axioms, not valid in ITL
|
|
|
108 ex(106,('[]'(('[]'(a)->a))-> ((('<>'('[]'(a)))-> '[]'(a))))). % Z discreteness
|
|
|
109 ex(107,('[]'(('[]'(a)->a))-> ('[]'(a)))). % W weak density
|
|
|
110 % Other Axioms, not valid in ITL
|
|
|
111 ex(108,(a-> '[]'('<>'(a)))). % B
|
|
|
112 ex(109,(('<>'a)-> '[]'('<>'(a)))). % 5
|
|
|
113
|
|
|
114 ex(110,(more-> (more&more))). % our dense time
|
|
|
115
|
|
|
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....)
|
|
|
215
|
|
|
216 ex(200,^r).
|
|
|
217 ex(201,true & ^r). % will terminate?
|
|
|
218 ex(202,((^r & ^r),not(^r))). % is non-local?
|
|
|
219 ex(203,(^r,length(4))). % distinguish different state?
|
|
|
220 ex(204,('[a]'(^r))). % non-deterministic?
|
|
|
221 ex(205,('[a]'(^r = length(2)))). % imitate length?
|
|
|
222 ex(206,('[a]'(^r = length(4)),(^r& ^r))).
|
|
|
223 ex(207,('[a]'(^r = (length(4);empty)),* ^r)).
|
|
|
224 ex(208,('[]'(^r = (
|
|
|
225 a,@ ^r;
|
|
|
226 not(a),c,@ @ ^r;
|
|
|
227 not(a),not(c),b,empty)),^r)). % RE
|
|
|
228 ex(209,('[a]'(^r = (
|
|
|
229 a,@((^r & @((b,empty)))) ;
|
|
|
230 not(a),b,empty)),
|
|
|
231 ^r)). % CFG
|
|
|
232
|
|
|
233 % Linear Time Axioms, valid in ITL
|
|
|
234 ex(210,('[]'((^a-> ^b)) -> ('[]'(^a) -> '[]'(^b)))). % K
|
|
|
235 ex(211,('[]'(((^a , '[]'(^a))-> ^b));'[]'(((^b , '[]'(^b))-> ^a)))). % 4
|
|
|
236 ex(212,('[]'(^a)-> '<>'(^a))). % D
|
|
|
237 ex(213,('[]'(^a)-> '[]'('[]'(^a)))). % L
|
|
|
238 ex(214,(('[]'(^a))-> ^a)). % T
|
|
|
239 % Diodorean discreteness
|
|
|
240 ex(215,('[]'('[]'((((^a-> '[]'(^a)))-> ^a))) -> ((('<>'('[]'(^a)))-> '[]'(^a))))).
|
|
|
241 % Linear Time Axioms, not valid in ITL
|
|
|
242 % Z discreteness
|
|
|
243 ex(216,('[]'(('[]'(^a)-> ^a))-> ((('<>'('[]'(^a)))-> '[]'(^a))))).
|
|
|
244 % W weak density
|
|
|
245 ex(217,('[]'(('[]'(^a)-> ^a))-> ('[]'(^a)))).
|
|
|
246 % Other Axioms, not v^alid in ITL
|
|
|
247 ex(218,(^a-> '[]'('<>'(^a)))). % B
|
|
|
248 ex(219,(('<>' ^a)-> '[]'('<>'(^a)))). % 5
|
|
|
249
|
|
|
250 % State Diagram Support
|
|
|
251
|
|
|
252 ex(300,(((length(2), @ '<>'(q)) proj true),
|
|
|
253 st(ns0)
|
|
|
254 )) :- ensure_loaded(kiss_ex).
|
|
|
255
|
|
|
256 /* end */
|
