Temporal logic (re)sources: A summary (900+ lines!)
omo ADELAKUN T K
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 k...@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: k...@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 mcov...@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: mcov...@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.
d...@doc.ic.ac.uk is his email address.
--
:- Michael A. Covington internet mcov...@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 cme...@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: cme...@kbssun1.tamu.edu (Chris Menzel)
To: mb108
To: mb...@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.1...@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 ko...@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: <ko...@csl.sony.co.jp>
To: mb108 (omo ADELAKUN T K)
Organization: Sony Computer Science Laboratory, Inc.
Reply-To: ko...@csl.sony.co.jp
Subject: Re: Definitive temporal logic source
Date: Mon, 25 Jan 93 15:03:26 +0900
From: Shinji Kono <ko...@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 @ ko...@csl.sony.co.jp
Sony Computer Science Laboratory, Inc,Japan
From jc...@fmg.bt.co.uk Mon Jan 25 09:55:20 1993
id <sg.05...@ben.uknet.ac.uk>; Mon, 25 Jan 1993 09:48:39 +0000
id <177...@zaphod.axion.bt.co.uk>; Mon, 25 Jan 1993 09:48:01 +0000
Mon, 25 Jan 93 09:42:10 GMT
From: Jeremy Wilson <jc...@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: jc...@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 ja...@dcs.gla.ac.uk Mon Jan 25 14:59:29 1993
with LOCAL SMTP (PP) id <092...@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 <ja...@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: ja...@dcs.glasgow.ac.uk or via nsfnet-relay.ac.uk FAX: 041 330 4913
BANG!net: via mcsun and uknet BITNET: via UKACRL UUCP: ja...@glasgow.uucp
From ma...@vercors.imag.fr Tue Jan 26 09:25:07 1993
(5.65c8/IDA-1.4.4 for <mb...@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: ma...@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: ma...@vercors.imag.fr
===============================================================
From rw...@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: rw...@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 joh...@minster.york.ac.uk Wed Jan 27 09:16:28 1993
From: joh...@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 joh...@minster.york.ac.uk Wed Jan 27 09:26:31 1993
From: joh...@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.