ex(0,(p)).
ex(1,((p&q))).
ex(2,( (fin(p)&true) <-> '<>'p)).
ex(3,( fin(p) <-> '[]'( '<>' p) )).
ex(4,(~(true&q))).
ex(5,(~(true& ~q))).
ex(6,(((true& p),(true& q)))).
ex(7,('[]'((p -> '<>' q)))).
ex(8,( '<>' '[]'(p))).
ex(9,( '[]'( '<>'(p)))).
ex(10,((p && p && p && p && p && ~p && p)-> '[]'('<>'(p)))).
% weak closure (or finite closure)
ex(11,+ (a,@ (b,@ (c,@empty)))).
% quantifier
ex(12,exists(R,(R,keep(@R = ~R),'[]'((R->p))))).
% temporal assignment
ex(13,exists(R,(R = p,keep(@R = R),fin(R = p)))).
%
ex(14,
	exists(Q,(Q, 
	  '[]'((Q -> 
	          (((((a,skip) & (b,skip)), @ keep(~Q)) & Q)
	          ;empty))
	  )))
   <->  *(((a,skip) & (b,skip) ; empty))
).
ex(15,
        while(q,((a,skip) & (b,skip)))
   <->  exists(C,(C, 
          '[]'(
             (C -> 
                  (((q -> ((a,skip) & (b,skip)), @ keep(~C)) & C),
                    (~q -> empty))
             ))))
).
ex(16,even(p)<->evenp(p)).
% wrong example, but hard to solve
% ex(17,(p=>(q=>r)) <-> ((p=>q)=>r)).
% ex(18,exists(Q,(p=>Q & Q=>r)) <-> (p=>r)).
% dining philosopher
%   note: unspecified resource increase states
%   ex ((true & al,skip & al,ar,skip & ar,~al,skip) ;empty) * 
ex(19,(more,
% three philosophers 
        *( ('[]'((~al, ~ar)) & @ (al, ~ar,@ (al,ar, @ (ar,'[]'( ~al)))) ;empty) ) ,
        *( ('[]'((~bl, ~br)) & @ (bl, ~br,@ (bl,br, @ (br,'[]'( ~bl)))) ;empty) ) ,
        *( ('[]'((~cl, ~cr)) & @ (cl, ~cr,@ (cl,cr, @ (cr,'[]'( ~cl)))) ;empty) ) ,
% shared resources
	'[]'( ~ ( ar, bl)),
	'[]'( ~ ( br, cl)),
	'[]'( ~ ( cr, al))
)).
ex(20,(more,
%% five philosophers 
        *( ('[]'((~al, ~ar)) & @ (al, ~ar,@ (al,ar, @ (ar,'[]'( ~al)))) ;empty) ) ,
        *( ('[]'((~bl, ~br)) & @ (bl, ~br,@ (bl,br, @ (br,'[]'( ~bl)))) ;empty) ) ,
        *( ('[]'((~cl, ~cr)) & @ (cl, ~cr,@ (cl,cr, @ (cr,'[]'( ~cl)))) ;empty) ) ,
        *( ('[]'((~dl, ~dr)) & @ (dl, ~dr,@ (dl,dr, @ (dr,'[]'( ~dl)))) ;empty) ) ,
        *( ('[]'((~el, ~er)) & @ (el, ~er,@ (el,er, @ (er,'[]'( ~el)))) ;empty) ) ,
%% shared resources
	'[]'( ~ ( ar, bl)), '[]'( ~ ( br, cl)), '[]'( ~ ( cr, dl)),
	'[]'( ~ ( dr, el)), '[]'( ~ ( er, al))
)). % :-fail.  % too big to verify (sigh...)
%
ex(21,(more,
	share([ar,bl]),share([br,cl]),share([cr,dl]),
	share([dr,el]),share([er,al]),
        *( ((true && '[]'(al) && '[]'((al,ar)) && '[]'(ar));empty) ) ,
        *( ((true && '[]'(bl) && '[]'((bl,br)) && '[]'(br));empty) ) ,
        *( ((true && '[]'(cl) && '[]'((cl,cr)) && '[]'(cr));empty) ) ,
        *( ((true && '[]'(dl) && '[]'((dl,dr)) && '[]'(dr));empty) ) ,
        *( ((true && '[]'(el) && '[]'((el,er)) && '[]'(er));empty) ) ,
true)).  % :-fail.  % too big to verify (sigh...)

ex(22,(more,
%% three philosophers  with no iteration
        ( ('[]'((~al, ~ar)) & @ (al, ~ar,@ (al,ar, @ (ar,'[]'( ~al)))) ;empty) ) ,
        ( ('[]'((~bl, ~br)) & @ (bl, ~br,@ (bl,br, @ (br,'[]'( ~bl)))) ;empty) ) ,
        ( ('[]'((~cl, ~cr)) & @ (cl, ~cr,@ (cl,cr, @ (cr,'[]'( ~cl)))) ;empty) ) ,
% shared resources
	'[]'( ~ ( ar, bl)),
	'[]'( ~ ( br, cl)),
	'[]'( ~ ( cr, al))
)).
% These are not schema. Just check
% Linear Time Axioms, valid in ITL
ex(100,('[]'((a->b)) -> ('[]'(a) -> '[]'(b)))).  		%   K
ex(101,('[]'(((a , '[]'(a))->b));'[]'(((b , '[]'(b))->a)))).    %   4
ex(102,('[]'(a)-> '<>'(a))).                           	%   D
ex(103,('[]'(a)-> '[]'('[]'(a)))).                      	%   L
ex(104,(('[]'(a)) -> a)).                              	%   T
ex(105,('[]'('[]'((((a-> '[]'(a)))->a))) -> ((('<>'('[]'(a)))-> '[]'(a))))). %   Diodorean discreteness
% Linear Time Axioms, not valid in ITL
ex(106,('[]'(('[]'(a)->a))-> ((('<>'('[]'(a)))-> '[]'(a))))).   	%   Z discreteness
ex(107,('[]'(('[]'(a)->a))-> ('[]'(a)))).                	%   W weak density
% Other Axioms, not valid in ITL
ex(108,(a-> '[]'('<>'(a)))).                          	%   B
ex(109,(('<>'a)-> '[]'('<>'(a)))).                    	%   5

ex(110,(more-> (more&more))).                   	%   our dense time

% ex(demo(X),Y) :- demo(X,Y).
% Regular variable examples ( doesnot work now....)

ex(200,^r).
ex(201,true & ^r).   		% will terminate?
ex(202,((^r & ^r),not(^r))).	% is non-local?
ex(203,(^r,length(4))).		% distinguish different state?
ex(204,('[a]'(^r))).		% non-deterministic?
ex(205,('[a]'(^r = length(2)))). 		% imitate length?
ex(206,('[a]'(^(r) = length(4)),(^(r)& ^(r)))).
ex(207,('[a]'(^r = (length(4);empty)),* ^r)).
ex(208,('[]'(^r = (
         a,@ ^r;
         not(a),c,@ @ ^r;
         not(a),not(c),b,empty)),^r)).        % RE
ex(209,('[a]'(^r = (
         a,@((^r & @((b,empty)))) ;
         not(a),b,empty)),
      ^r)).                                   % CFG

% Linear Time Axioms, valid in ITL
ex(210,('[]'((^a-> ^b)) -> ('[]'(^a) -> '[]'(^b)))).            	%   K
ex(211,('[]'(((^a , '[]'(^a))-> ^b));'[]'(((^b , '[]'(^b))-> ^a)))).   	%   4
ex(212,('[]'(^a)-> '<>'(^a))).                             		%   D
ex(213,('[]'(^a)-> '[]'('[]'(^a)))).                         		%   L
ex(214,(('[]'(^a))-> ^a)).                                	%   T
%   Diodorean discreteness
ex(215,('[]'('[]'((((^a-> '[]'(^a)))-> ^a))) -> ((('<>'('[]'(^a)))-> '[]'(^a))))). 
% Linear Time Axioms, not valid in ITL
%   Z discreteness
ex(216,('[]'(('[]'(^a)-> ^a))-> ((('<>'('[]'(^a)))-> '[]'(^a))))).
%   W weak density
ex(217,('[]'(('[]'(^a)-> ^a))-> ('[]'(^a)))).
% Other Axioms, not v^alid in ITL
ex(218,(^a-> '[]'('<>'(^a)))).                              %   B
ex(219,(('<>' ^a)-> '[]'('<>'(^a)))).                         %   5

% State Diagram Support

%ex(300,(((length(2), @ '<>'(q)) proj true),
%      st(ns0)
%      )) :- ensure_loaded(kiss_ex).

% Infinite Interval

ex(400,infinite).
ex(401,*infinite).
ex(402,*skip).
ex(403,*length(5)).
ex(404,~('<>'(empty))).
ex(405,('<>'(empty))).   % unsatisfiable 
ex(406,(infinite-> @infinite)).
% ex(407,((less(5),[](q))&(length(3)&([](<>(p)),[](<>(~p)),*length(6))))).
ex(408,(infinite -> ~(<>([](p)) = [](<>(p))))).  % satisfiable
ex(409,finite).   % unsatisfiable


% demo(X) :- number(X),demo(X,ITL),nl,ex(ITL),nl,write(ITL).
def("demo(X,Y)","ex(X,Y)").
% def("demo(X,Y)","true").
% length 5 interval
demo(1001, length(5)).

% p is trun at the top of a interval
demo(1002, (length(5),p)).

% @ meas next time.
demo(1003, (length(5),@p,@ @q,@ @ @r)).

% &(chop) devides an interval into to parts
demo(1004, ((length(2),p)) & (length(3),q)).

%  there are several ways of division.
demo(1005, (length(5),(p&q))).

% sometime usinng chop
demo(1006, (length(5),(true & p))).

% always: dual of sometime
demo(1007, (length(5),not(true & not(p)))).

% counter intutive theorem
demo(1008, '<>' '[]'(p) = '[]'('<>'(p))).

% shared resource / exclusive condition
demo(1009, (length(5),
        '[]'(((    ac ,not(bc),not(cc),not(dc));
            (not(ac),    bc ,not(cc),not(dc));
            (not(ac),not(bc),    cc ,not(dc));
            (not(ac),not(bc),not(cc),    dc ))))).

% periodical task by Projection
demo(1010, (more,
	proj((@ '<>'(q),length(2)),true))).

% time sharing taks by Projection
demo(1011, (more,length(7),
	proj(true,('[]'(p),length(4))))).

% combination of periodical task
demo(1012, (more,
	proj(length(2),'[]'(ac)),
	proj(length(3),'[]'(bc)),
	proj(length(5),'[]'(cc)))).

% periodical task with shared resources
demo(1013, (more,
	proj((length(3),@ '<>'(ac)),true),
	proj((length(5),@ '<>'(bc)),true),
	proj((length(5),@ '<>'(cc)),true),
	'[]'((not((ac,bc)),not((bc,cc)),not((cc,ac)))),
	true)).

% combination of periodical taks and aperiodical task with shared resource
demo(1014, (
	((proj(true,(length(5),'[]'(dc))),length(15) )&true),
	proj((length(3),@ '<>'(ac)),true),
	proj((length(5),@ '<>'(bc)),true),
	proj((length(5),@ '<>'(cc)),true),
	'[]'(((    ac ,not(bc),not(cc),not(dc));
	    (not(ac),    bc ,not(cc),not(dc));
	    (not(ac),not(bc),    cc ,not(dc));
	    (not(ac),not(bc),not(cc),    dc ))),
	true)).
% combination of periodical taks and aperiodical task with shared resource
%  schedulable case
demo(1015, (
	((proj(true,(length(4),'[]'(dc))),length(15) )&true),
	proj((length(3),@ '<>'(ac)),true),
	proj((length(5),@ '<>'(bc)),true),
	proj((length(5),@ '<>'(cc)),true),
	'[]'(((    ac ,not(bc),not(cc),not(dc));
	    (not(ac),    bc ,not(cc),not(dc));
	    (not(ac),not(bc),    cc ,not(dc));
	    (not(ac),not(bc),not(cc),    dc ))),
	true)).


% model restriction by share predicate ( a little smaller.... :-)
demo(1016, (
	share([ac,bc,cc,dc]),
	((proj(true,(length(4),'[]'(dc))),length(15) )&true),
	proj((length(3),@ '<>'(ac)),true),
	proj((length(5),@ '<>'(bc)),true),
	proj((length(5),@ '<>'(cc)),true),
	true)).
demo(1017, (
((proj(true,(length(5),'[]'(c))),length(15))&true),
(proj((length(3),@ '<>'(a)),true)&less(3)),
(proj((length(5),@ '<>'(b)),true)&less(5)),
'[]'(not((a,b))),
'[]'(not((b,c))),
'[]'(not((c,a)))
)).

end.