NetNews Usenet Archive 1993 #3/NN_1993_3.iso/spool/sci/logic/2643

Internet Message Format | 1993-01-27 | 27.8 KB

Xref: sparky sci.logic:2643 sci.math:18780 comp.lang.prolog:2457
Newsgroups: sci.logic,sci.math,comp.lang.prolog
Path: sparky!uunet!inmos!fulcrum!bham!warwick!doc.ic.ac.uk!citycs!mb108
From: [e-mail] (omo ADELAKUN T K)
Subject: Temporal logic (re)sources: A summary (900+ lines!)
Message-ID: <[e-mail]>
Sender: [e-mail] (News)
Organization: City University, London
Date: Wed, 27 Jan 93 14:08:03 GMT
Lines: 895

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 [e-mail] 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: [e-mail] (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 [e-mail] 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: [e-mail] (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.
[e-mail] is his email address.




--
:-  Michael A. Covington     internet [e-mail] :    *****
:-  Artificial Intelligence Programs       phone [phone] :  *********
:-  The University of Georgia                fax [phone] :   *  *  *
:-  Athens, Georgia 30602-7415 U.S.A.     amateur radio N4TMI :  ** *** **

From [e-mail] 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: [e-mail] (Chris Menzel)
To: mb108

To: [e-mail] (omo ADELAKUN T K)
Subject: Re: Definitive temporal logic source
Newsgroups: sci.logic,comp.lang.prolog,sci.math

In article <[e-mail]> 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 [e-mail] 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: <[e-mail]>
To: mb108 (omo ADELAKUN T K)
Organization: Sony Computer Science Laboratory, Inc.
Reply-To: [e-mail]
Subject: Re: Definitive temporal logic source
Date: Mon, 25 Jan 93 15:03:26 +0900
From: Shinji Kono <[e-mail]>

>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 @           [e-mail]
Sony Computer Science Laboratory, Inc,Japan

From [e-mail] Mon Jan 25 09:55:20 1993
          id <[e-mail]>; Mon, 25 Jan 1993 09:48:39 +0000
          id <[e-mail]>; Mon, 25 Jan 1993 09:48:01 +0000
          Mon, 25 Jan 93 09:42:10 GMT
From: Jeremy Wilson <[e-mail]>
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: [e-mail]           !
! Room 3-07                       !     Telephone: [phone]             !
! BT Development and Procurement  !     International: [phone]      !
! Bibb Way              !     Facsimile: 0473-210182             !
! IPSWICH                         !     International: [phone]      !
! Suffolk  IP1 2EQ                !     Telex: 987705                      !
! United Kingdom                  !     International: [phone]          !
!                    !                        !
+---------------------------------+----------------------------------------+


From [e-mail] Mon Jan 25 14:59:29 1993
          with LOCAL SMTP (PP) id <[e-mail]>;
          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 <[e-mail]>
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: [phone] x6854 (work)
INTERNET: [e-mail] or via nsfnet-relay.ac.uk    FAX: [phone]
BANG!net: via mcsun and uknet     BITNET: via UKACRL    UUCP: [e-mail]


From [e-mail] Tue Jan 26 09:25:07 1993
  (5.65c8/IDA-1.4.4 for <[e-mail]>); 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: [e-mail] (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:  [phone]  Fax: [phone]   e-mail: [e-mail]
===============================================================

From [e-mail] 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: [e-mail] (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 [e-mail] Wed Jan 27 09:16:28 1993
From: [e-mail]
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 [e-mail] Wed Jan 27 09:26:31 1993
From: [e-mail]
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.