/*
 Copyright (C) 1991, Shinji Kono, Sony Computer Science Laboratory, Inc.
                                  The University, Newcastle upton Tyne

 Everyone is permitted to copy and distribute verbatim copies
 of this license, but changing it is not allowed.  You can also
 use this wording to make the terms for other programs.

 send your comments to kono@csl.sony.co.jp
 $Id: ex.pl,v 1.5 2007/08/30 03:44:35 kono Exp $

 Examples
*/

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 = q)))).

ex(133,
    (exists(R,(q = R,stable(R),fin(p = R))))
   =
    (q & (empty,p); ~q & (empty, ~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).

% length 5 interval
demo(1, length(5)).

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

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

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

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

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

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

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

% shared resource / exclusive condition
demo(9, (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(10, (more,
	proj((@ '<>'(q),length(2)),true))).

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

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

% periodical task with shared resources
demo(13, (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(14, (
	((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(15, (
	((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(16, (
	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(17, (
((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 */