.pl 10 
.ll 50 
.ul 1
1   What is Tokio
.sp 1
1.1 Preface
.sp 1
      Tokio is a hardware description language based on Interval Temporal
Logic (ITL) [1], which can also describe concurrency.
Although Tempura (by Moszkowski) [2], based on Interval Temporal Logic (ITL),
is well known as such a language,
ITL also completely includes First Order Predicate Logic,
and therefore Tokio includes Prolog, too .
.sp 1
1.2 Tokio Time
.sp 1
      Time in Tokio is discrete and represented by integers.
An interval I in Tokio has a finite length, its beginning time is I.beg
and its ending time is I.fin.
It is necessary that 'I.beg' =< 'I.fin' .
.sp 1
1.3 Temporal Operators
.sp 1
       In order to introduce the idea of time into Prolog, we need 
.ul 1
temporal operators. 
These operators describe time relationships.
A goal is executed in an interval 'I'. In fact,
a goal which has no temporal operators 
is executed at the beginning of the interval
ie. 'I.beg'.
    A Tokio program with no temporal
operator is executed in (the beginning of) the same
interval.
In this case, programs run in the same way as Prolog. For example,
the goals 'q','r' of the following clause
    p:-q,r.
.br
are executed in the same interval 'I' (exactly speaking, at the beginning 
of the interval 'I', that is 'I.beg').
.sp 1
    Here we introduce several temporal operators.
.sp 1
.ul 1
&&
    We introduce the
.ul 1 
chop operator
which describes the order of execution of two goals.
The chop operator is defined as '&&' .
    p:-q && r.
    The chop operator divides the interval 'Ip'
(in which 'p' is executed)
into two intervals. In the first one (that is in Iq) 'q' is executed,
and in the latter one (that is in Ir) 'r' is executed.
.sp 1
.ul 1
@
    The
.ul 1
next operator
\'@' means the execution at the next time.
While the present interval is between 'I.beg' and 'I.fin',
goals with a next operator are executed
at the beginning of the interval 
which is between 'I.beg+1' and 'I.fin'.
    p :- @q.
.br
\'q' is executed at the next time 'p' is executed.
    If I.beg = I.fin (that is length(I) = 0), @p will
.ul 1
fail.
.sp 1
.ul 1
next
    The
.ul 1
next operator
\'next' means almost same as '@'.
    But if I.beg = I.fin, next(p) is
.ul 1
true.
.sp 1
.ul 1
#
    Goals with the
.ul 1
always operator
\'#' are executed in all the subintervals of the interval.
    p :- #q.
.br 
\'q' is executed in all the subintervals of
the interval in which 'P' is executed. 
    The ends of all subintervals must be same.
This is the difference from another next operator '||'.
(See 1.6 Definition of Interval)
.sp 1
.ul 1
\'||'
    Goals with the
.ul 1
always operator
\'||' are executed in all the subintervals of the interval.
    p :- '||'q.
.br 
\'q' is executed in all the  subintervals of
the interval in which 'p' is executed. 
    The ends of all subintervals must
.ul 1
not
be same.
(See 1.6 Definition of Interval)
.sp 1
.ul 1
<>
    Goals with the
.ul 1
sometime oprator
\'<>' are executed at some time in the interval.
    p :- <>q.
.br
\'q' is executed at some time in the interval in which 'P' is executed.
.sp 1
.ul 1
keep
    Goals with the
.ul 1
keep operator	
are executed all times except the last one of the interval.
    p :- keep(q).
    'q' is executed all the time in interval 'Ip' in which 'p' is executed
except the last time 'I.fin'.
.sp 1
.ul 1
fin
    The
.ul 1
fin operator
is used when we execute the goal at the end of the interval.
    p :- fin(q).
    'q' is executed at the end time ('Ip.fin') of the interval
in which 'p' is executed.
.sp 1
1.4 Tokio Variables
.sp 1
.in 2
1.4.1 Form
    The
.ul 1
Tokio variable
has different values at every time
and each of them is logic variable in Prolog.
Tokio variable is considered a sequence of logic variables.
    A tokio variable is essentially only a logic variable,
there are some forms of variables in order to ease programming.
.sp 1
.ul 1
stable
    When the predicate stable(X) is executed,
variable 'X' has the same value throughout the interval
in which this predicate is executed.
stable(X) is defined as follows.
       stable(X) :- keep(@X = X).
.sp 1
.ul 1
global
    When the predicate 
global([atom1,atom2, ... ,atomN]) is defined,
atoms in the list are
recorded as variable names of global variables.
After the definition, the name is used as a normal Tokio variable
in the form of '*variableName'. With global variable, the following clauses
    a(X,Y) :- 
      X = 1, Y = 1, b(X), c(Y).
    b(X) :- X = ...
    c(Y) :- Y = ...
.br
can be translated as follows.
    global([x,y]).
    a :- *x = 1, *y = 1, b, c.
    b :- *x = ...
    c :- *y = ...
.sp 1
.ul 1
static
    A static variable keeps a value from an old binding until new binding.
This is the same as variables in Pascal etc.
.sp 1
.ul 1
:=, <=
    There are two ways to assign the static variables a value as follows.
    *s := 1. ---(1)
    *s <= 1. ---(2)
    A value is assigned at current time in (1),
but the value is assigned at the end of the interval in (2).
\':=' corresponds to '=' in the case of general Tokio variables,
and '<=' corresponds to '<-' in that case. (See 1.4.2)
.br
.sp 1
1.4.2 Evaluation
    Usually Tokio variables have all the values of each time.
In executing goals, unification is done from now to infinite future.
    On the other hand, some predicates are necessary
to deal with individual value of variable at a certain time.
Such predicates are called evaluable predicates.
.ul 1
=
    '=' unifies a value at current time and another at current time.
    X = Y.
.br
means to take out the value of Tokio variables 'X' and 'Y'
which have all the values of each time and unify them.
    '=' can unify static variables or function, too.
.ul 1
<-
    '<-' unifies a value at the beginning of an interval
and another value at the end of that interval.
    X <- Y.
.br
means to unify the value of 'Y' at the beginning of an interval
and the value of 'X' at the end of that interval.
.br
.ul 1
@
    '@' unifies a value at current time
and another value at the next time.
    @X = Y.
.br 
means to unify the value of 'Y' at current time
and the value of 'X' at the next time.
.sp 1
.in -2
1.5 Tokio Function
.br
.sp 1
gets : 
.in 8 
\'A gets B' means 'keep(B = @A)'.
The value of a Tokio variable B at current time
is unified with the value of Tokio variable A
at the next time, and this operation is
executed at all times of an interval
except at the end of that interval.
.in -8
.br
+,-,*,/,mod,^,int,var :
.in 8
These functions can be used.
.in -8
.br
size(U) :
.in 8
Return the number of arguments in the list U.
.in -8
I thof U :
.in 8
Return the I'th argument in the list U.
.br
Example; 2 thof [a,b,c,d] is c.
                 0 1 2 3
.in -8
slice(U,H,T) :
.in 8
Return a list consists of H'th, H+1'th, ... , T'th arguments
of the list U.
.br
Example; slice([a,b,c,[d,e]],2,3) is [c,[d,e]].
.in -8
Begin to End;
.in 8
Begin and End is integer.
Return the list of [Begin, Begin + 1, ... , End].
.in -8
.br
.sp 1
1.6 Definition of Interval
.sp 1
    Interval I is defined by a pair of integers <I.beg, I.fin>,
and the value of I.fin is decided nondeterminately.
    In Tokio, an execution of a goal G in the interval Ig starts at Ig.big
and ends at I.fin.(=I.beg + N). 
In this case, N is an integer which is larger than 0 or equal to 0 
and is decided nondeterminately. N varies by time backtrack.(See 1.7
Backtrack) 
.br
.ul 1
length
    In order to decide the length of an interval, there is 
a predicate 
.ul 1
length.
For example, the predicate length(N) sets the I.fin to 
satisfy I.fin = I.beg + N .  	   
.br 1
.ul 1
empty
    The predicate 
.ul 1
empty
means length(0).
.sp 1
    Temporal operators also decide intervals.
.br 1
.ul 1
chop operator
    For example; p && q. ----- (1)
    At first, we assume that I is an interval of 'p && q', Ip is that of 'p',
and Iq is that of 'q'.
Then I, Ip, and Iq are decided as follows.

    |----------|----------|
    \\_____________________/       I
    \\__________/\\_________/  
        Ip   	    Iq
.sp 1
    The execution is as follows.
.br
[1] 'p && q' is tried to be executed at I.beg.
.br
[2] Ip.beg is equal to I.beg, and 'p' is executed at Ip.beg(=I.beg).
.br
[3] Ip.fin = Ip.beg + Np, and Np is decided nondeteminately.
.br
[4] Iq.beg is equal to Ip.fin, and 
.br
'q' is executed at Iq.beg(=Ip.fin).
.br
[5] Iq.fin = Iq.beg + Nq.
.br
[6] The execution of the whole goal
'p && q' ends and I.fin is equal to Iq.fin.
    Then we consider the case of including the 'length' predicate.
    For example; length(2),p && q. ------(2)
    I.fin is decided as mentioned. Because of 'length(2)',
if I.fin is not equal to I.beg + 2, time backtrack arises
and Np and Nq are decided in another way.
    In Tokio, the length of an interval is decided in the following way.
.br
[1] If there is a length specification (such as length(2) )
it must be satisfied.
.br
[2] If there are no length appointment,
length is decided 1,2,3, ----,N.
N is smaller than the length of the parent interval.
That is, the length of 'p' is shorter than the length of 'p && q'.
.br
[3] The length is 0.
But if N in case [2] is infinite, length cannot be 0.
    In case of example(1),
Np and Nq are decided in following order.
    Np    Nq
    1	  1 
    1     2 
    1     3
    1     4 
    .     .
    .     .
.sp 1
    In case of example(2),
Np and Nq cannot be larger than 2, they are decided in following order.
    Np    Nq
    1     1
    2     0
.sp 1
.ul 1
next operator
    Examples;
    p,@q.
    At first, we assume the interval of 'p,@q' is I and that of 'q"
is Iq.
    The execution of 'p,@q' in the interval I consists of the
execution of 'p' in I and the execution of 'q' in Iq.
    I and Iq are as follows:

    |----|----|----|----|----|
    \\________________________/ I
         \\___________________/ Iq
 
    The execution is as follows:
.nf
[1] 'p,@q' is tried to be executed at I.beg.
[2] 'p' is executed at I.beg.
[3] '@q' is also tried to be executed at I.beg.
[4] 'q' is executed at Iq.beg(= I.beg + 1).
.fi
[5] The execution 
of whole goal 'p,@q' ends, and I.fin is equal to Iq.fin. 

.sp 1
.ul 1
always operators # , ||
    Examples;
.nf
test1 :- length(5),#bb.

test2 :- length(5),#aa.

test3 :- length(5),'||'aa.

aa    :- length(1),write(aa),nl.

bb    :- write(bb),nl.

.fi
    Test1 and test3 succeed but test2 fails.
    Subintervals in the case of test1 and test3 are as follows.
(See 1.3 Temporal Operator)

    |----|----|----|----|----|  
    \\________________________/ interval of test1 

    \\________________________/
         \\___________________/ subintervals 
 	      \\______________/ in which
                   \\_________/ bb is executed
                        \\____/	

    |----|----|----|----|----|  
    \\________________________/ interval of test3 

    \\____/
         \\____/                subintervals 
              \\____/  	        in which
                   \\____/      aa is executed
                        \\____/	

    
    In case of test2, the ends of subintervals in which aa is executed
cannot be same because of length specification, and so test2 fails.
@
.sp 1
1.7 Backtrack
.sp 1
    There are two kinds of backtrack in Tokio. 
One is the same as in Prolog, and 
the other is time backtrack. 
Time backtrack redefines the length of interval. 
    Time backtrack cause fail in prolog mode or repeat_fail mode.
(See 2.3 Modes)
.ul 1
.sp 1
2   Using Tokio
    The usage of Tokio is very similar to that of Prolog. 
.sp 1
2.1 Startup, Halt, and Reading-in programs
.sp 1
    These are same as in Prolog.
    Prompt in Tokio is 'tokio: ?-'. This is different from in Prolog.
.sp 1
2.2 Break and Abort
.sp 1
    The way to break or abort is
the same as in Prolog.
But when break or abort arises,
the prompt is turned into '| ?- ' and in this condition
Tokio cannot be executed.
    After a break or abort arises,
there are two ways to execute Tokio.
    One is to give the directive '| ?-
.ul 1
tokio.
\', and Tokio can be executed again and the prompt is turned
into 'tokio: ?- ' again. The other way is to give the directives
'| ?-
.ul 1
tokio aa.
\' and the Tokio predicate aa can be executed.
.sp 1
2.3 Modes
.sp 1
    There are three modes in Tokio. 
That is (1) recursion (2) repeat_fail (3) prolog.
    In prolog mode the system executes Prolog,
in repeat_fail mode the system executes Tokio without time backtrack,
and in recursion mode the system executes Tokio normally.
    When system gives us the message "out of global stack" in Tokio mode,
we may change the mode from recursion to repeat_fail, because 
in recursion mode system needs very large stack area for time backtrack.
.sp 1
.ul 1
2.4 Source files
    Executable file 'tokio' is made by 'makefile'.
Following is a list of makefile.

.nf
% makefile
tokio		: tokio.bin
	echo	'exec cprolog -q tokio.bin' > tokio
	chmod 755 tokio
tokio.bin	: tokio_src tokio_dat tokio_dbg
                  tokio_evl tokio_startup
                  tokio_sys tokio_uty
	cprolog < tokio_startup
.fi 
.sp 1
    Therefore following files are consulted in executing Tokio.
    tokio_dat : date structure
    tokio_dbg : debugger
    tokio_evl : function evaluator
    tokio_src : main routine
    tokio_startup : tokio startup
    tokio_sys : system predicate
    tokio_uty : utility
    xref.def  : prolog predicate
.sp 1
2.5 Operator declaration
.sp 1
    Operators in Tokio is declared as follows.

.nf
:-op(1170, xfx  ,( :: )).
                  % tokio formula  definition
:-op(1160, fx   ,(tokio)).         
          % tokio formula  interpreter
:-op(1150, fx   , [(if),(while)]).
:-op(1140, xfx  , [(else),(do)]).
:-op(1130, xfx  , (then)).
:-op(1120, xfy  , ('&&')).
:-op(900,  fx   ,
           ['<>',#,'|a|','|t|','||',beg,halt]).        
:-op(700,  xfy , [\=,===] ).
:-op(700,  xfy , [:=] ).
          % static assignment instanteanous
:-op(700,  xfy , [<=] ).          
          % static temporal assignment 
:-op(700,  xfy , [<-] ).
          % temporal assignment
:-op(700,  xfy , [<--] ).
          % force constrant
:-op(700,  xfy , gets ).
          % repeatedly assignment
:-op(600,  xfx , to ).         % range
:-op(150,  fy  , @).           % next oprator
:-op(140,  fx  , *).           % variables
.fi
.sp 1
.ul 1
3.  Debugging
    Debugging in Tokio is also very similar to that in Prolog.
Resemblance between Tokio and Prolog is almost omitted in this section.
.sp 1
3.1 The Procedure of Debugging 
.sp 1
    Debugging starts by the command 'tokiotrace'.
    For example, to debug a predicate 'ppp',
give the directives 'tokiotrace, ppp.'.
    Call, Fail, and Back are the same as those in Prolog.
Exit is a little different from that in Prolog.
In Tokio, any predicate "exit" at the time when it is called.
    Following is an example.
.sp 1
.nf
Script started on Thu Aug 29 17:48:07 1985
% tokio
C-Prolog version 1.5

A tokio interpreter 	Ver 7.0 8/26/85
		S.Kohno and M.Fujita  Tokyo Univ.


tokio: ?- [ab].
ab consulted 140 bytes 0.266669 sec.

yes
tokio: ?- tokiotrace,testd.

exit,t0:asserta(step(on)) 
exit,t0:setval(step,on) 
t0:tokiodebugon   h:s

exit,t0:tokiodebugon 
exit,t0:call((setval(step,on),tokiodebugon)) 
exit,t0:tokiotrace 
t0:testd   h:

t0:aa   h:

t0:write(aa)   h:
aa
exit,t0:write(aa) 
exit,t0:aa 
.ul 1
exit,t0:testd 
t1:bb   h:

t1:write(bb)   h:
bb
exit,t1:write(bb) 
exit,t1:bb 
yes

tokio: ?- halt.

[ Prolog execution halted ]
.sp 1
---------- list of file ab ----------

testd :- aa && bb.

aa    :- length(1),write(aa).
bb    :- length(1),write(bb).
.fi
.br
.sp 1
3.2 Options
.sp 1
    Options available during debugging are following.
       a : abort 		b : break
       d : dump 		h : help 
       l : leap 		s : skip
       q : quasi-skip           t : time skip
       End-of-Line : creep
    These are also the same as in Prolog except 'd' and 't'.
    Dump shows the value of static variables at each time
like the following.
    2 of addr is [a,s]
    1 of addr is [a]
.br
This expression means that the value of a static variable 'addr'
is [a,s] at time 2 and [a] at time 1.
    Time skip means to skip to the end of the time.
.sp 1
3.3 Time Trace
.sp 1
    There are three modes of tracing, that is tron, trtime, and troff.
    In 'tron' mode, system shows us the clauses 
which are executed at that time and outputs (if there are)
every time.
    In 'trtime' mode, the system shows us outputs (if there are) every time.
    'Troff' mode is the so called normal mode.
    To change mode, do as follows.
.br 
| ?- tron.

.sp 1
3.4 Help
.sp 1
    There is a 
.ul 1
help
command. Give the directive 'help', and following messages is echoed back.
    'tokiobreak	tokio break call'
    'tron 	     display queue in each clock'
    'trtime    	     display only time'
    'troff	     no display'
    'tokiodebugon    tokio spy mode on'
    'tokiodebugoff   tokio spy mode off'
    'tokiodebugall   trace all predicate'
    'tokiospy(X/N)   trace predicate X with arity N'
    'tokiospy(X)     trace predicate X'
    'tokionospy      remove all spy point'
    'tokionospy(X)   remove spy point of predicate X'
    'tokiotrace      trace mode on'
    'tokionotrace    trace mode off'
    'recursion       main loop is recursion'
    'repeat_fail     main loop is repeat fail'
    'prolog	     main loop is prolog'
    'tokio X	     execute X'
    'tokio	     main loop'