🚀 go-pugleaf

The number of responses I got seems to suggest much interest in the area -
which is why I'm posting a collated summary. Responders, thanx for your
responses (special thanx to Dr. Chris Johnson of York for the interpreter
implementation). To everyone else, enjoy (if you will):

From kym@bingsuns.cc.binghamton.edu Sun Jan 24 04:31:13 1993
	id AA08677; Sat, 23 Jan 93 23:23:31 EST
Date: Sat, 23 Jan 93 23:23:31 EST
From: kym@bingsuns.cc.binghamton.edu (R. Kym Horsell)
	id AA00797; Sat, 23 Jan 93 23:18:34 EST
To: mb108
Subject: Re: Definitive temporal logic source
Newsgroups: sci.logic,comp.lang.prolog,sci.math
Organization: Binghamton University
Cc: 

TOKIO is an old Prolog program that interprets some form
of temporal reasoning. You'll have to look it up in
either the Int Conf on Auto Deduction, or the Int/Nat
Conf on Sym Log; I don't know where I saw it.

-kym

From mcovingt@aisun3.ai.uga.edu Sun Jan 24 04:51:42 1993
	id AA08343; Sat, 23 Jan 93 23:45:25 EST
Date: Sat, 23 Jan 93 23:45:25 EST
From: mcovingt@aisun3.ai.uga.edu (Michael Covington)
To: mb108
Subject: Re: Definitive temporal logic source
Newsgroups: sci.logic,comp.lang.prolog,sci.math
Organization: AI Programs, University of Georgia, Athens
Cc: 

Ask Dr. Dov Gabbay over in Imperial College London.
dg@doc.ic.ac.uk is his email address.




-- 
:-  Michael A. Covington     internet mcovingt@uga.cc.uga.edu :    *****
:-  Artificial Intelligence Programs       phone 706 542-0358 :  *********
:-  The University of Georgia                fax 706 542-0349 :   *  *  *
:-  Athens, Georgia 30602-7415 U.S.A.     amateur radio N4TMI :  ** *** **

From cmenzel@kbssun1.tamu.edu Sun Jan 24 21:35:06 1993
	id AA18510; Sun, 24 Jan 93 15:31:11 CST
Date: Sun, 24 Jan 93 15:31:11 CST
From: cmenzel@kbssun1.tamu.edu (Chris Menzel)
To: mb108

To: mb108@cs.city.ac.uk (omo ADELAKUN T K)
Subject: Re: Definitive temporal logic source
Newsgroups: sci.logic,comp.lang.prolog,sci.math

In article <1993Jan23.114811.28054@city.cs> you write:
: Can anyone point me to a very good text on temporal logic?

J. van Bentham, {\it The Logic of Time: a model-theoretic
investigation into the varieties of temporal ontology and temporal
discourse} (Reidel, 1983), is about the best I've seen.

Chris Menzel

From kono@csl.sony.co.jp Mon Jan 25 06:09:46 1993
	id AA04755; Mon, 25 Jan 93 15:03:03 JST
	id AA10142; Mon, 25 Jan 93 15:03:28 JST
Return-Path: <kono@csl.sony.co.jp>
To: mb108 (omo ADELAKUN T K)
Organization: Sony Computer Science Laboratory, Inc.
Reply-To: kono@csl.sony.co.jp
Subject: Re: Definitive temporal logic source 
Date: Mon, 25 Jan 93 15:03:26 +0900
From: Shinji Kono <kono@csl.sony.co.jp>

>Can anyone point me to a very good text on temporal logic? 

I recomend Manna's Book (I forget its title....). 

And CSLI report
@book{Goldblatt87,
        author = "Robert Goldblatt",
        series =        "CSLI Lecture Notes",
        title =  "Logic of Time and Computation",
        publisher = "CSLI",
        volume = "7",
        year = 1987
}


>In the same
>vein, does anyone know of a temporal logic interpreter (something along
>the lines of Prolog or extensions thereto)?

There are many....
   Tokio (which has both interpreter and compiler) based on interval 
          temporal logic), which I wrote.. 
         Colse to Tempura, but supports non-deterministic execution.

@article{tokio86,
        author =        "M. Fujita and S. Kono and H. Tanaka",
        address =       "London",
        year =          "July 1986",
        journal =       "Proc. of Int. Conf. on Logic Programming",
        title =         "Tokio: Logic Programming Language based on Temporal Log
ic and its compilation to Prolog"
}

   Temporal Prolog
   IB-Templog
          Both supports Mcdamott's interval temporal logic.
          You can find an article in Journal of logic programing
   Sakura's Temporal Prolog
          supports linear time temporal logic
   Molog
          Modal logic extention of Prolog
          There is an article in "New generatoin computing".
   In CMU, some one working on CTL extention of Prolog.

>Thanx for any responses - which I'd prefer to come to me direct so I can 
>post a summary.

Please send it to me... :-)
---
Shinji Kono @           kono@csl.sony.co.jp
Sony Computer Science Laboratory, Inc,Japan

From jcrw@fmg.bt.co.uk Mon Jan 25 09:55:20 1993
          id <sg.05431-0@ben.uknet.ac.uk>; Mon, 25 Jan 1993 09:48:39 +0000
          id <17704-0@zaphod.axion.bt.co.uk>; Mon, 25 Jan 1993 09:48:01 +0000
          Mon, 25 Jan 93 09:42:10 GMT
From: Jeremy Wilson <jcrw@fmg.bt.co.uk>
Date: Mon, 25 Jan 93 09:48:24 GMT
To: mb108 (omo ADELAKUN T K)
Subject: Re: Definitive temporal logic source
Newsgroups: sci.logic,comp.lang.prolog,sci.math
Organization: British Telecom

I can't give you a definitivce text and would like to know one myself but 
  I can recommend Executing Temporal Logic by Moszkowski, 1986, published by 
 Cambridge Univeristy Press. If I remember correctly there is a language
 called Tempura fro which there exists an interpreter.


+---------------------------------+----------------------------------------+
! Jeremy Wilson			  !	email: jcrw@fmg.bt.co.uk           !
! Room 3-07                       !     Telephone: 0473-227822             !  
! BT Development and Procurement  !     International: +44 473-227822      !
! Bibb Way			  !     Facsimile: 0473-210182             !
! IPSWICH                         !     International: +44 473-210182      !
! Suffolk  IP1 2EQ                !     Telex: 987705                      !
! United Kingdom                  !     International: +51 987705          !
!  				  !     				   !
+---------------------------------+----------------------------------------+


From jack@dcs.gla.ac.uk Mon Jan 25 14:59:29 1993
          with LOCAL SMTP (PP) id <09263-0@goggins.dcs.gla.ac.uk>;
          Mon, 25 Jan 1993 14:52:51 +0000
          Mon, 25 Jan 93 14:52:45 GMT
Date: Mon, 25 Jan 93 14:52:45 GMT
From: jack <jack@dcs.gla.ac.uk>
To: mb108
Subject: Re: Definitive temporal logic source
Newsgroups: sci.logic,comp.lang.prolog,sci.math
Organization: COMANDOS Project, Glesga Yoonie, No Mean City

The best single book I know of is J.F.A.K. van Benthem: "The Logic of Time",
published by Elsevier.

cheers - jack



-- 
--  Jack Campin    room G092, Computing Science Department, Glasgow University,
17 Lilybank Gardens, Glasgow G12 8RZ, Scotland   TEL: 041 339 8855 x6854 (work)
INTERNET: jack@dcs.glasgow.ac.uk or via nsfnet-relay.ac.uk    FAX: 041 330 4913
BANG!net: via mcsun and uknet     BITNET: via UKACRL    UUCP: jack@glasgow.uucp


From maler@vercors.imag.fr Tue Jan 26 09:25:07 1993
  (5.65c8/IDA-1.4.4 for <mb108@cs.city.ac.uk>); Tue, 26 Jan 1993 10:18:17 +0100
	id AA28496; Tue, 26 Jan 93 10:18:42 +0100
	id AA02694; Tue, 26 Jan 93 10:18:27 +0100
Date: Tue, 26 Jan 93 10:18:27 +0100
From: maler@vercors.imag.fr (Maler)
To: mb108 (omo ADELAKUN T K)
Subject: Re: Definitive temporal logic source


Manna and Pnueli, The Temporal Logic of Concurrent and Reactive
Programs, Springer, 1991.

-- 
===============================================================
Oded Maler, LGI-IMAG (Campus), B.P. 53x, 38041 Grenoble, France
Phone:  76635846  Fax: 76446675   e-mail: maler@vercors.imag.fr
===============================================================

From rwsh@cam.sri.com Tue Jan 26 10:34:01 1993
	id AA24286; Tue, 26 Jan 93 10:26:24 GMT
Date: Tue, 26 Jan 93 10:26:24 GMT
From: rwsh@cam.sri.com (Roger Hale)
	id AA22339; Tue, 26 Jan 93 10:26:25 GMT
To: mb108
Subject: Definitive temporal logic source

Here are a few books on various aspects of temporal logic. How good you
think they are will depend to a very large extent on what you want them for
(logical theory, applications, survey, ...).

@book{prior:tl,
	author = "Prior, A. N.",
	title = "Past, Present and Future",
	publisher = "Clarendon Press",
	address = "Oxford",
	year = 1967
}

@book{manna-pnueli:tl-book-v1,
	author = "Manna, Z. and Pnueli, A.",
	title = "The Temporal Logic of Reactive and Concurrent Systems: 
        Specification",
	publisher = "Springer-Verlag",
	year = 1992
}

Rescher & Urquhart: Temporal Logic, Springer-Verlag.

Kroger: Temporal Logic of Programs, Springer-Verlag.

Goldblatt: Logics of Time and Computation, CSLI.

@inproceedings{
        ...
	booktitle = "Temporal Logics and Their Applications",
	editor = "Galton, A.",
	publisher = "Academic Press",
	address = "London",
	pages = "91--119",
	year = 1987
}

@inproceedings{
        ...
	booktitle = "Temporal Logic in Specification",
	editor = "Banieqbal, B. and Barringer, H. and Pnueli, A.",
	publisher = "Lecture Notes in Computer Science, number 398, Springer-Verlag",
	address = "Berlin",
	year = 1989
}

There are a number of designs for programming languages based on temporal
logic, some of them have resulted in interpreters. To my knowledge, the
best developed systems are those based on Interval Temporal Logic: Tempura
and Tokio. Tempura is imperative, Tokio is more prolog-like. Shinji Kono,
who implemented Tokio, is now working on a nice little verifier for
propositional ITL.  I think Howard Barringer has also worked on an
implementation of a conventional TL language, but I've no idea of its
status. I believe that Manna and Abadi's proposed language was never
implemented. Here are some refs.

@book{moszkowski:exec,
	author = "Moszkowski, B. C.",
	title = "Executing Temporal Logic Programs",
	publisher = "Cambridge University Press",
	address = "Cambridge, England",
	year = 1986
}

@techreport{hale:thesis,
	author = "Hale, R. W. S.",
	title = "Programming in Temporal Logic",
	institution = "Computer Laboratory",
	address = "University of Cambridge, England",
	number = "173",
	year = 1989
}

@inproceedings{abadi:templog,
	author = "Abadi, M. and Manna, Z.",
	title = "Temporal Logic Programming",
	booktitle = "Proc. IEEE Symposium on Logic Programming",
	year = 1987
}

@inproceedings{gabbay:manchester,
	author = "Gabbay, D. M.",
	title = "The Declarative Past and Imperative Future: Executable
Temporal Logic for Interactive Systems",
	booktitle = "Temporal Logic in Specification",
	editor = "Banieqbal, B. and Barringer, H. and Pnueli, A.",
	publisher = "Lecture Notes in Computer Science, number 398, Springer-Verlag",
	address = "Berlin",
	year = 1989
}

@inproceedings{fujita-etal:tokio,
	author = "Fujita, M. and Kono, S. and Tanaka, H. and Moto-oka, T.",
	title = "Tokio: Logic Programming Language based on Temporal Logic and Its Compilation to Prolog",
	booktitle = "Proceedings of the Third International Conference on Logic Programming",
	organisation = "",
	address = "London",
	year = 1986,
	month = jul
}

From jampel Tue Jan 26 11:26:26 1993
From: Michael Jampel <jampel>
Date: Tue, 26 Jan 1993 11:24:30 GMT
To: mb108
Subject: temporal logic


Rescher is in the City University library.

From jampel Tue Jan 26 11:27:28 1993
From: Michael Jampel <jampel>
Date: Tue, 26 Jan 1993 11:25:33 GMT
To: mb108
Subject: temporal logic


There is also a book on TEMPURA - a temporal logic language - its a thin
blue book, but I foregt who its by.

From johnson@minster.york.ac.uk Wed Jan 27 09:16:28 1993
From: johnson@minster.york.ac.uk
Date: Wed, 27 Jan 93 09:08:53
To: mb108

I've got a version of the Tokio interpreter.
I'll mail you the source - for references you
might try to get a copy of my thesis - there
is a huge lit survey in it.

Hope this helps,
  Chris.

@phdthesis{Johnson:92t,
        TITLE = "A Formal Approach To The Integration Of Human Factors And Systems Engineering",
        AUTHOR = "C.W. Johnson",
        SCHOOL = "Department Of Computer Science, University of York",
        ADDRESS = "York, United Kingdom",
        YEAR = "1992"}

or:

@incollection{Johnson:91a,
        TITLE = "Applying Temporal Logic To Support The Specification And Prototyping Of Concurrent Multi-User Interfaces",
        AUTHOR = "C.W. Johnson",
        BOOKTITLE = "People And Computers VI: Usability Now",
        PAGES = "145-156",
        EDITOR = "D. Diaper and N. Hammond",
        PUBLISHER = "Cambridge University Press",
        ADDRESS = "Cambridge, United Kingdom",
        YEAR = "1991"}




From johnson@minster.york.ac.uk Wed Jan 27 09:26:31 1993
From: johnson@minster.york.ac.uk
Date: Wed, 27 Jan 93 09:10:50
To: mb108

%------------------------------------------------------------%
%
%              TOKIO INTERPRETER 
%
%   File: tokio.pl
%   Author : S. Kono, T. Aoyagi, M. Fujita and H. Tanaka
%   Implemented by: C.W. Johnson,
%   Address: Department of Computer Science,
%            University of York,
%            Heslington,
%            England.
%            Y01 5DD.
%   Date: 23/11/89.
%
% NB Poorly documented in the original article, had to make
% ammendments to get it to work, specifically systemp()
% and tnot() - in order to expand non temporal predicates.
% 
% Source published in:
% 	Springer Verlag Notes on Computer Science No. 221
%
% Acknowledgement:
%       Chris Roast (at the above address) helped at many
% stages of the implementation of this code and helped to
% port it from CProlog to LPA Prolog to Sicstus Prolog.
%
% See:
%	C.W. Johnson and M.D. Harrison, Declarative
%	Graphics And Dynamic Interaction, F.H. Post
%	and W. Bath (eds.), EUROGRAPHICS'91, 
%	Elsevier, North Holland, 1991. pp 195-207.
%
%	C.W. Johnson, Applying Temporal Logic To
%	Support The Specification And Prototyping
%       Of Concurrent Multi-User Interfaces, 
%	D. Diaper and N. Hammond (eds.), People
%	And Computers VI: Usability Now, Cambridge
%	University Press, Cambrdige, U.K. pp 145-156.
%
%_________________________________________________________%

% Key to temporal operators:
%     @(X) is true if X is true in next interval.
%     #(X) is true if X is true in all intervals.
%     Y===X is true if X unifies with Y in present interval.
%     Y<--X is true if X unifies with Y in all intervals.
%     <>(Y) is true if Y is eventually true.
%     until(X, Y) is true if X is true until Y is true.
%
% TOKIO must be regarded as a hybrid form of temporal logic
% for example an assertion (X<--3) is not, in effect, a global
% temporal assignment because all variable are `lost' at the
% end of each clause.   One way of interprating it's behaviour
% is to regard the scope of the clause as an interval, so the 
% variable is globally assigned over the scope or interval
% of that clause.   This view leads to conflicts with the
% <> operator because in TOKIO this requires global termination,
% rather than clause completion, giving the operator an
% unorthodox interpretation in this implementation.

:- prolog_flag(single_var_warnings, X, off).
:- nl,nl,nl,
   write('TOKIO'), nl,
   write('Loading file...'),
   nl,nl,nl.

%_________________________________________________________%
%-Entry to TOKIO.
temp(A) :-
	t_reduce(A, 0, Fin).    
%_________________________________________________________%

%_________________________________________________________%
%-Define operator precedence. 
:- op(810,xfx, '<--').
:- op(810,fx,#).
:- op(810,fx,@).
:- op(810,xfx,'*u*').
:- op(810,xfx, '<-').
:- op(810,xfx, 'gets').
:- op(810,xfx,'&&').
:- op(100,xfx, '===').
%_________________________________________________________%

%_________________________________________________________%
%-Expand temporal formulae to reveal temporal operators in 
% bodies of dependent clauses.
t_reduce(true, Now, Fin) :-integer(Fin),Now>Fin,!.
t_reduce(Formula, Now, Fin) :-
	i_reduce(Formula,Next,Now,Fin,_),
	NextT is Now+1,
	t_reduce(Next,NextT,Fin).
%_________________________________________________________%

%_________________________________________________________%
%-Interval reducer reduces Formula Now and executes either
% finite queue or keep que.
i_reduce(Formula,Next1,Now,Fin,OuterFin):-
	qcl(Next,EmptyFlag,Q1,Q2),
	reduce(Formula,Q1,Now,Fin),
	force_finite(EmptyFlag,Now,Fin,OuterFin),
	exec_fin_keep(Next,Next1,Q1,Q2,Now,Fin).
%_________________________________________________________%

%_________________________________________________________%
%-Interval terminates.
exec_fin_keep(Next,true,Q1,Q2,Now,Fin) :-
	Now==Fin,!,
	get_fin(F,Q1),
	reduce(F,Q2,Fin,Fin).
exec_fin_keep(Next,Next,Q1,Q2,Now,Fin) :-
	get_keep(K,Q1),
	reduce(K,Q2,Now,Fin).
%_________________________________________________________%

%_________________________________________________________%
%-Cut off finite interval.
% NB TOKIO will terminate as soon as it can instantiate and 
% OuterFin and meet it's commitments.
force_finite(free,Now,Fin,OuterFin):-
  	var(Fin), Fin is Now+1,
	(nonvar(OuterFin),OuterFin=Fin,! ; true).
force_finite(_,Now,Fin,OuterFin).
%_________________________________________________________%

%_________________________________________________________%
%-Reduce temporal formula.
reduce((A,B),Q,Now,Fin):- 
	qap(Qa,Qb,Q),!,
	reduce(A,Qa,Now,Fin),
	reduce(B,Qb,Now,Fin).
reduce(A,Q,Now,Fin):-
	systemp(A),!,
	myexec(A,Q,Now,Fin).
reduce(A,Q,Now,Fin):-
	t_clause(A,B),
	reduce(B,Q,Now,Fin).
%_________________________________________________________%

%_________________________________________________________%
%-System predicates; added to original code.
%-These predicates are either temporal or need not be further
% expanded for temporal operators.

%PROLOG
%These are Sicstus system predicates which need not be expanded by TOKIO.
systemp(\+(A)).
systemp(nonvar(X)).
systemp(var(X)).
systemp(true).
systemp(fail).
systemp(A = B).
systemp(A =< B).
systemp(A - B).
systemp(A * B).
systemp(A + B).
systemp(A is B).
systemp(A \== B).
systemp(setof(X,Y,Z)).
systemp(write(X)).
systemp(writeq(St, X)).
systemp(close(St)).
systemp(open(St)).
systemp(open(F, Mode, St)).
systemp(read(X)).
systemp(read(St, X)).
systemp(!).
systemp(call(A)).
systemp([H|T]).
systemp(see(X)).
systemp(seen(X)).
systemp(tell(X)).
systemp(told(X)).
systemp(nl).

%UTILITIES
%These are general utilities which need not be expanded by TOKIO.
systemp(swap(X, Y, L1, L2)).
systemp(read_all_of_stream(St, X)).
systemp(write_all_of_list(St, L)).
systemp(to_string(X,Y)).
systemp(append(X,Y,L)).
systemp(member(X, L)).

%TEMPORAL
%These predicates are the temporal operators supported by TOKIO.
systemp(tnot(A)).                      % temporal not
systemp(#A).
systemp(A===B).
systemp(length(A)).
systemp(halt(A)).
systemp(empty).
systemp(notEmpty(A)).
systemp(wnext(A)).
systemp(fin(A)).
systemp(keep(A)).
systemp(A && B).
systemp('$int'(A,B,C)).
systemp(A<-- B).
systemp(t(A)).
systemp(@A).

%GRAPHICAL
%These predicates implement primitive system calls for graphics system Prelog
% for more on this see Johnson and Harrison `89.
%systemp(mtab(R)).                     %write tab to region R
%systemp(regborder(R, Width)).         %border of Width pixels for region R
%systemp(regwrite(R, Text)).           %write Text to region R
%systemp(regnl(R)).                    %write newline to region R
%systemp(regclear(R)).                 %clear region R of graphical content
%systemp(bread(Text)).                 %block on read from Prelog
%systemp(clear(R)).
%systemp(pswrite(R, T)).
%systemp(rnl(R)).
systemp(send(I)).
%systemp(clear(R)).
%_________________________________________________________%

%_________________________________________________________%
t_clause(A,B):-
	functor(A,Head,N),
	functor(AA,Head,N),
	clause(AA,B),
	unify_all(A,AA).
%_________________________________________________________%

%_________________________________________________________%
%-Execute system predicate and perform relevant queue
% manipulation.
myexec(true,Q,_,_):- 
	!,nonq(Q).
myexec(length(N),Q,Now,Fin):- 
	!, nonq(Q),
	Fin is Now+N.
myexec(empty,Q,Now,Fin) :- 
	nonq(Q),!,
	Now=Fin.
myexec(notEmpty,Q,Now,Fin) :- 
	!,enq_nonEmpty(halt(Fn),Q).
myexec(halt(F),Q,Now,Fin):-
	reduce(F,Q,Now,Fin),
	!,Now=Fin.
myexec(halt(F),Q,Now,Fin):- 
	unifyNext(F, RFn),
	enq_nonEmpty(halt(Fn),Q).
myexec(#F,Q,Now,Fin):-
	qap(Q1,Q2,Q),
	enq_nxt(#Fn,Q1),
	unifyNext(F,Fn),!,
	reduce(F,Q2,Now,Fin).
myexec(@F,Q,Now,Fin):-               % strong next
	!,enq_nonEmpty(Fn,Q),
	unifyNext(F,Fn).
myexec(wnext(F),Q,Now,Fin):-           % weak next
	enq_nxt(Fn,Q),
	unifyNext(F,Fn),!.
myexec(fin(F),Q,Now,Fin):-
	!,((Now==Fin,!,reduce(F,Q,Now,Fin));
	qap(Q1,Q2,Q),enq_fin(F,Q1),unifyNext(F, Fnn), enq_nxt(fin(Fnn),Q2)).
myexec(keep(F),Q,Now,Fin):-
	!,qap(Q1,Q2,Q),
	enq_nfin(F,Q1),
	unifyNext(F,Fnn),
	enq_nxt(keep(Fnn),Q2).
myexec((A && B),Q,Now,Fin):-
	!,sub_exec(A,B,Q,Now,Fin,SubFin).
myexec('$int'(A,B,SubFin),Q,Now,Fin):-
	!,sub_exec(A,B,Q,Now,Fin,SubFin).
myexec(A===B,Q,Now,Fin):- 
	qap(Q1,Q2,Q),!,
	eval(A,Va,Q1,Now,Fin),
	eval(B,Vb,Q2,Now,Fin),
	unifyNow(Va,V),
	unifyNow(Vb,V).
myexec(call(X),Q,Now,Fin):- 
	!, reduce(X,Q,Now,Fin),
	nonq(Q).
myexec(tnot(X),Q,Now,Fin):- 
	!, \+(reduce(X,Q,Now,Fin)),
	nonq(Q).
myexec(A<--B,Q,Now,Fin):-
	!,eval(B,Vb,Q,Now,Fin),
	unifyNow(Vb,A1),
	unify_all(A,A1).
myexec(S,Q,Now,Fin):-
	unifyNow(S,SN),!,
	SN,
	nonq(Q).
%_________________________________________________________%

%_________________________________________________________%
%-Execute subinterval Now.
sub_exec(F,L,Q,Now,Fin,SubFin):-
	i_reduce(F,Fnext,Now,SubFin,Fin),
	sub_exec_later(L,Fnext,Q,Now,Fin,SubFin).
%_________________________________________________________%

%_________________________________________________________%
%-Execute subinterval later.
sub_exec_later(L,Next,Q,Now,Fin,Subfin):-
	Now==SubFin,!,
	reduce(L,Q,Now,Fin).
sub_exec_later(L,Next,Q,Now,Fin,SubFin):-
	unifyNext(L,Ln),
	enq_finNext(L,'$int'(Next,Ln,SubFin),Q).
%_________________________________________________________%

%_________________________________________________________%
%-Evaluate functions.
eval(Atom,Atom,Q,Now,Fin):-
	(atomic(Atom) ; var(Atom); functor(Atom,'$t',2)),
	nonq(Q),!.
eval(@Var,Next,Q,Now,Fin):-
	!,eval(Var,NowValue,Q,Now,Fin),
	unifyNext(NowValue,Next).
eval(A+B,V,Q,Now,Fin):-
	!, qap(Q1,Q2,Q),
	eval(A,Va,Q1,Now,Fin),
	eval(B,Vb,Q2,Now,Fin),
	unifyNow(Va,Vna),
	unifyNow(Vb,Vnb),
	V is Vna+Vnb.

eval(A-B,V,Q,Now,Fin):-
	!, qap(Q1,Q2,Q),
	eval(A,Va,Q1,Now,Fin),
	eval(B,Vb,Q2,Now,Fin),
	unifyNow(Va,Vna),
	unifyNow(Vb,Vnb),
	V is Vna-Vnb.

eval(S,S,Q,_,_):-
	nonq(Q).
%_________________________________________________________%

%_________________________________________________________%
% NB. Difference lists used - very opaque code!!!
% In the TOKIO interpreter (as opposed to compiler) there is a
% single queue of the form: $t(N,F,K,C), where N is the next queue
% F is for the fin queue, K  is for the keep queue and C keeps
% the internal variables and current time.
%-Queue structure 1      2      3         4
%           q(Next-Next,Fin-Fin,Keep-Keep,Empty-Flag)
qcl(Next,EmptyFlag,
	q(Next-Next1,Fin0-true,Keep0-true,EmptyFlag),
	q(Next1-true,Fin1-true,Keep1-true,EmptyFlag)).
%_________________________________________________________%
%-Queue append the 1 2 and 3 of first two arguments
% so long as 4 is the same in both.
qap(q(Next2-Next1,Fin2-Fin1,Keep2-Keep1,EmptyFlag),
	q(Next1-Next,Fin1-Fin,Keep1-Keep,EmptyFlag),
	q(Next2-Next,Fin2-Fin,Keep2-Keep,EmptyFlag)).
%_________________________________________________________%

%_________________________________________________________%
%-This true for 1 2 and 3 being empty
nonq(q(Next-Next,Fin-Fin,Keep-Keep,EmptyFlag)).
%_________________________________________________________%

%_________________________________________________________%
%-Weak next
enq_nxt(N, q((N,Next)-Next,Fin-Fin,Keep-Keep,EmptyFlag)).
%_________________________________________________________%

%_________________________________________________________%
%-Strong next
enq_nonEmpty(N, q((N,Next)-Next,Fin-Fin,Keep-Keep,nonEmpty)).
%_________________________________________________________%

%_________________________________________________________%
enq_fin(F, q(Next-Next,(F,Fin)-Fin,Keep-Keep,EmptyFlag)).
%_________________________________________________________%

%_________________________________________________________%
enq_nfin(K, q(Next-Next,Fin-Fin,(K,Keep)-Keep,EmptyFlag)).
%_________________________________________________________%

%_________________________________________________________%
enq_finNext(F,N, q((N,Next)-Next,(F,Fin)-Fin,Keep-Keep,nonEmpty)).
%_________________________________________________________%

%_________________________________________________________%
get_fin(F,Q):-
	arg(2,Q,F-_).
%_________________________________________________________%

%_________________________________________________________%
get_keep(K,Q):-
	arg(3,Q,K-_).
%_________________________________________________________%

%_________________________________________________________%
get_nonEmpty(EmptyFlag,Q):-
	arg(4,Q,EmptyFlag).
%_________________________________________________________%

%_________________________________________________________%
nonEmpty(Q,Now,Fin):-
	Now==Fin,!,
	fail.
nonEmpty(Q,Now,Fin):-
	get_nonEmpty(nonEmpty,Q).
%_________________________________________________________%

%_________________________________________________________%
/* unifiers */
unify_all(G,D):-
	(var(G) ; var(D)),!,
	G=D.
unify_all(F1,D):-
	functor(F1,'$t',2),!,
	unify_flt(F1,D).
unify_all(D,F1):-
	functor(F1,'$t',2),!,
	unify_flt(F1,D).
unify_all(Sa,Sb):-
	functor(Sa,H,N),
	functor(Sb,H,N),
	unify_arg(N,N,Sa,Sb).
%_________________________________________________________%

%_________________________________________________________%
unify_arg(0,N,_,_):-!.
unify_arg(M,N,Sa,Sb):-
	arg(M,Sa,Aa),
	arg(M,Sb,Ab),
	unify_all(Aa,Ab),
	M1 is M-1,!,
	unify_arg(M1,N,Sa,Sb).
%_________________________________________________________%

%_________________________________________________________%
unify_flt('$t'(Now,Nxt),'$t'(Now,Nxt1)) :-
	!,unify_all(Nxt,Nxt1).
unify_flt('$t'(Now,Nxt),S) :-
	unifyNow(S,Now),
	unifyNext(S,Nxt1),
	unify_all(Nxt,Nxt1).
%_________________________________________________________%

%_________________________________________________________%
%-Unify present identity of variables and predicates
% (i.e. St(Y,X) and St(U,V) if Y===U).
unifyNow(X,X1):-
	myatomic(X),!,
	X=X1.
unifyNow('$t'(Now,_),Now1):-
	!,Now=Now1.
unifyNow(S,Sn):-
	functor(S,H,N),
	functor(Sn,H,N),
	unifyNowArg(N,N,S,Sn).
%_________________________________________________________%

%_________________________________________________________%
%-Unify present identity of predicate arguments
% (i.e. St(Y,X) and St(U,V) if Y===U).
unifyNowArg(0,_,_,_).
unifyNowArg(M,N,Sa,Sb):-
	arg(M,Sa,Aa),
	arg(M,Sb,Ab),
	unifyNow(Aa,Ab),
	M1 is M-1,!,
	unifyNowArg(M1,N,Sa,Sb).
%_________________________________________________________%

%_________________________________________________________%
%-Unify next identity of variables and predicates
% (i.e. St(Y,X) and St(U,V) if X===V).
unifyNext(X,X):-
	myatomic(X),!.
unifyNext('$t'(_,Next),Next1):-
	!,Next=Next1.
unifyNext(S,Sn):-
	functor(S,H,N),
	functor(Sn,H,N),
	unifyNextArg(N,N,S,Sn).
%_________________________________________________________%

%_________________________________________________________%
unifyNextArg(0,_,_,_).
unifyNextArg(M,N,Sa,Sb):-
	arg(M,Sa,Aa),
	arg(M,Sb,Ab),
	unifyNext(Aa,Ab),
	M1 is M-1,!,
	unifyNextArg(M1,N,Sa,Sb).
%_________________________________________________________%

%_________________________________________________________%
%-More modifications 
myatomic(X):-
	nonvar(X),
	atomic(X).
%_________________________________________________________%

%_________________________________________________________%
%-This clause is a loop hole back to PROLOG will suspend
% the tokio interpreter for duration of call.
t(X) :-
	X.
%_________________________________________________________%
%_________________________________________________________%
/* Predefined utilites */
<>(F):-
	(true && (F)).
A gets B:- 
	keep(B === (@A)).
stable(A):-
	keep(A === (@A)).
B<-A:-
	C<--A,
	fin(B===C).
tskip:-
	length(1).

until(P, Q) :- tnot(Q), P, @(until(P, Q)).
until(P, Q) :- Q.

%_________________________________________________________%


*********** END

Sincerely,
Toyin.

				pOBODY'S Nerfect	- Anon.