Tempura, the C-Tempura interpreter version 2.7 developed originally by Roger Hale and now maintained by
Antonio Cau and Ben Moszkowski, is an interpreter for executable Interval Temporal Logic
formulae. The ﬁrst Tempura interpreter was programmed in Prolog by Ben Moszkowski, and was
operational around December 2, 1983. Subsequently he rewrote the interpreter in Lisp (mid Mar,
1984), and in late 1984 modiﬁed the program to handle a two-level memory and multi-pass
scanning. The C-Tempura interpreter was written in early 1985 by Roger Hale at Cambridge
AnaTempura, which is built upon C-Tempura, is a tool for the runtime veriﬁcation of systems using
Interval Temporal Logic (ITL) and its executable subset Tempura. The runtime veriﬁcation technique uses
assertion points to check whether a system satisﬁes timing, safety or security properties expressed in ITL.
The assertion points are inserted in the source code of the system and will generate a sequence of
information (system states), like values of variables and timestamps of value change, while the system is
running. Since an ITL property corresponds to a set of sequences of states (intervals), runtime veriﬁcation is
just checking whether the sequence generated by the system is a member of the set of sequences
corresponding to the property we want to check. The Tempura interpreter is used to do this membership
- Initial support for monitoring rmi based Java programs.
- Use internal variable runid to assign id to external processes.
- Tempura commands stable and output now allows lists of variables,
i.e., stable(V,W) and output(V,W).
- Use kitcreator to generate the anatempura binaries. The windows
binaries are generated using the mingw-w64 cross-compiler.
- Various other bug fixes, see ChangeLog for more details.
- The Tcl/Tk graphical user interface does not depend on Expect anymore.
- The lexer/parser now throws an error on encountering a unknown
character instead of silently discarding it.
- The read-only State_number variable can be used in Tempura programs
to determine the current state number.
- The monitoring of C# programs does not need a Java wrapper anymore.
- Support for monitoring of Java programs in the form of a jar file.
- Support of time-stamps in the form of seconds and microseconds.
- The GUI has now a different look/layout, history of commands window is
gone, the most commonly used menu entries are now buttons and one interacts
with Tempura using a shell-like interface.
- Added template .anatempurarc .
- Integers are now 64bits regardless of the machine architecture.
- Windows binaries are compiled using the msys2-mingw32/64 system.
- For Windows we have 32 bit (XP and beyond) and 64 bit (7 and beyond)
- Random numbers are now generated using xorshift128plus.
- Added support for monitoring Scala programs.
- Added option -stdio to start anatempura in cmdline mode.
- Various other bug fixes, see ChangeLog for more details.
- Rewritten the Tempura output capture/processing routine.
- Rewritten the external program data capture/processing routine.
- New implementation of memory/framed variables, existsf V : f, is now used
to indicate that V is memory/framed variable within f.
The previous syntax mem(V) is now deprecated.
- Fix bugs in the implementation of prev(L) where L is a list.
- Added Tempura binary for Arduino-Yun and Raspberry Pi, i.e.,
tempura_mips_openwrt_linux and tempura_arm_linux_gnueabihf.
- Added elapsed time in the statistics output at the end of a run.
- Added plc and sql injection detection examples.
- Various other bug fixes see ChangeLog for more details.
- Dropped pre-compiled Solaris binary.
- flex/bison based parser backward compatible with previous hard coded
version but with stricter syntactic checks
- changed from cvs to svn as version control system
- improved syntax error messages
- fixed memory leaks
- tidy up format command
- startup file .anatempurarc can also be in the current directory
- use kbs-0.4.4 to generate anatempura binaries
- anatempura binaries are using Tcl/Tk 8.6
- works again under Windows XP
- program assertions can have any symbol except control characters and !
- Dropped tempura_macosx binary but added tempura_linux64 and
- fixed some small bugs
- fixed memory leaks
- added command ‘winput’ that will wait for input from a file instead
of switching to the keyboard.
- added floats. Floats have the form $2.3e+10$ in Tempura. For output:
output($2.3$) will be $2.30000e+00$ , i.e., precision is 5 digits
after the ’.’. One can set this via the precision variable. With
precision of 2 one gets $2.30e+00$. The format command can output
floats in two forms: %f output will be of the form 2.33333, e output
will be of the form 2.33333e+01. The following operations on floats
are defined: unary, +, -; binary: +, -, div, mod, /, *, **, ceil,
floor, sqrt, itof, exp, log, log10, sin, cos, tan, asin, acos, atan,
atan2, sinh, cosh, tanh, fabs.
- anatempura is now using the new Tile interface
- when setting system variables with set, output both old and new
- Added ’frandom’ and ’fRandom’ for float random number between
- Added defaults command, X defaults 1 denotes when X is undefined
then take as value for X the value 1.
- Added prev(X) operator, the value of X in the previous state.
- Added mem(X) operator, X is a ’memory’ variable, i.e., when
undefined take the value in the previous state.
- Added #n history operator, used as option to exists when declaring a
variable, it will keep a history of n previous values of a variable.
- Added nprev(X,n) operator, nprev(X,3) for instance is an
abbreviation of prev(prev(prev(X))).
- When setting debug_level to 6 more usefull information is displayed
like the state of a variable and reduction rule being applied.
- Included tempura executables tempura_linux for Linux (compiled on
Ubuntu 9.10), tempura_solaris for Solaris (compiled on Sparc
Solaris 10u8), and tempura.exe for Windows (compiled on Windows XP SP3).
- Included anatempura executables anatempura_solaris, anatempura_linux
and anatempura.exe. These were built using the Tclkit Kitgen build
system (http://wiki.tcl.tk/18146). Now no need anymore to install
tcl/tk and expect in order to run anatempura.
- changed copyright license to GPLv3.0
- introduced various node accessor macros so that if one changes the node
structure we only have to change the macro.
- if formula can’t be reduced in the final state of the
prefix of a chop then we will evaluate ((prefix and empty);true)
and (suffix). This feature can be switched on/off with hopchop.
The default of hopchop is true.
- added integer overflow tests.
- unified/cleaned up the various node data structures.
- work around a recent misfeature of windows when started an external program.
- added the io redirections, set infile="some file name", set
outfile="some file name", where stdin and stdout can be used to
redirect to standard keyboard and screen i/o.
- added the infinite and randlen constructs for respectively an
infinite interval and a random length interval (less or equal
- added reset in file menu to restart tempura.
- open and reload now also load the file into Tempura.
- added showstate Tempura command. This will display what is
(un)defined in the current state.
- changed contact email address to email@example.com
This version is the first version that compiles both under
Windows and Unix/Linux type of machines. See Changelog for detailed
How to run AnaTempura?
Use the pre-compiled binary:
anatempura.exe: 32 bit binary and will run on Windows Xp, 7 and beyond, this will use
tempura.exe in the current directory
anatempura-win64.exe: 64 bit binary and will run on Windows 7 and beyond, this will use
tempura-win64.exe in the current directory
anatempura_linux: For 32bit Linux OS, this will use tempura_linux in the current directory
anatempura_linux64: For 64bit Linux OS, this will use tempura_linux64 in the current
anatempura_macosx: For MacOSX, this will use tempura_macosx in the current directory
you need to install Tempura, and Tcl/Tk (at least 8.5). Get Tcl/Tk and from Tcl/Tk site or
use the ActiveTcl package.
Tempura can be compiled using the Gnu C compiler under a Unix like operating system like
Ubuntu, GNU Debian, etc. For Windows you can use the MSYS2/MinGW-32/64 system,
see their website for downloading and installation. Install the MSYS2 system, and then,
using pacman, install the mingw-w64-i686-toolchain for compiling 32bit binaries and the
mingw-w64-x86_64-toolchain for compiling 64bit binaries.
Compile Tempura using the following commands
For convenience the following pre-compiled Tempura binaries are included in the distribution:
Figure 3 shows a graphical snapshot of a simulation of the EP/3 microprocessor speciﬁed in Tempura.
Figure 3: Graphical snapshot of simulation of the EP/3 microprocessor
6.2 FLCheck: Fusion Logic decision Procedure
Fusion Logic augments conventional Propositional Temporal Logic (PTL) with the fusion operator. Note:
the fusion-operator is basically a “chop” that does not have an explicit negation on the left hand (for right
fusion logic) side (as fusion expression) or the right hand (for left fusion logic). The negation is implicit, i.e.,
the negation is a derived fusion expression operator. The expressiveness of Fusion Logic is the same as
Propositional Interval Temporal Logic. The main diﬀerences concern computational complexity, naturalness
of expression for analytical purposes, and succinctness. Fusion Logic is closely related to Propositional
Dynamic Logic (PDL).
We have implemented above decision procedure for Fusion Logic in Tcl/Tk and the CUDD BDD
library. The tool allows one to check the validity or satisﬁability of a Fusion Logic formula.
If a formula is not valid it will produce a counter example and if a formula is satisﬁable it
will produce an example model. Figure 4 gives a screen dump of our tool which is available
Isabelle/HOL is a generic proof assistant. It allows mathematical formulas to be expressed in a formal
language and provides tools for proving those formulas in a logical calculus.
We have given a deep embedding of propositional ITL and a shallow embedding of ﬁrst order ITL in
Isabelle/HOL. A shallow embedding represents ITL using Isabelle/HOL predicates, while a deep embedding
would represent ITL formulas as mutually inductive datatypes. See, e.g.,  for a discussion about deep vs.
shallow embeddings in Isabelle/HOL. The shallow embedding of ﬁrst order ITL uses techniques developed
by Stefan Merz [175, 20] for the shallow embedding of Temporal Logic of Actions (TLA) in
Deep embedding: version 1.8 (08/12/2018, ﬁrst public release), gzipped tar ﬁle.
Shallow embedding: version 2.2 (08/12/2018, warning this is work in progress), gzipped tar ﬁle.
6.4 ITL Theorem Prover based on Prover9
Note: this work has been re-encoded in the deep embedding of propositional ITL in Isabelle/HOL.
Prover9 is a resolution/paramodulation automated theorem prover for ﬁrst-order and equational logic
developed by William McCune.
We have given an algebraic axiom system for Propositional Interval Temporal Logic (PITL): Interval
Temporal Algebra. The axiom system is a combination of a variant of Kleene algebra and Omega algebra
plus axioms for linearity and conﬂuence.
This algebraic axiom system for PITL has been encoded in Prover9. So we can use Prover9 to prove the
validity of various PITL theorems. The Prover9 encoding of PITL plus examples of more than 300 PITL
theorems are available for download as
The README in this tar ﬁle contains instructions how to use Prover9 for proving PITL theorems.
6.5 ITL Proof Checker based on PVS
Note: this work has been superseded by the deep and shallow embedding of ITL in Isabelle/HOL.
PVS is an interactive environment, developed at SRI, for writing formal speciﬁcations and checking
formal proofs. The speciﬁcation language used in PVS is a strongly typed higher order logic. The powerful
interactive theorem prover/proof checker of PVS has a large set of basic deductive steps and the facility to
combine these steps into proof strategies. PVS is implemented in Common Lisp –with ancillary functions
provided in C, Tcl/TK and LaTeX– and uses GNU Emacs for its interface. PVS is freely available for IBM
RS6000 machines as well as Sun Sparcs under license from SRI. See PVS homepage for more information.